Commit 1b3ebb18 authored by Sylvain Dailler's avatar Sylvain Dailler

Add well_formed for type invariant

This is an attempt at adding predicate well_formed in the builtins
theories (adding it to bool as the bool type is necessary).
This also adds a strategy to always unfold this predicate in eval_match.
parent cbd77699
......@@ -24,6 +24,8 @@ Language
* identifiers used for record constructor `mk foo` have been renamed to `foo'mk` :x:
* the `alias` clause can now be used in program functions to force the aliasing
of function parameters and/or named returns
* the `well_formed` predicate is now available for manual triggering of type
invariants :x:
Tools
* counterexamples given by `why3prove` are no longer printed using JSON
......
......@@ -167,6 +167,14 @@ a program function that expects an argument of a mutable type
will accept an argument of the corresponding snapshot type
as long as it is not modified by the function.
% TODO to be rewritten by someone who knows the rules in details
Invariants can be added on types. They are preserved by the tool so specific
goals are produced to check those. For usability, \why allows to temporary
breaks the invariants. The user can trigger a type invariant check by calling a
function or predicate on the whole value (not on independant fields) or by
using the \texttt{well\_formed} predicate.
\index{well-formed@\verb+well_formed+}
\section{Logical expressions: terms and formulas}
\label{sec:terms}
......
......@@ -926,6 +926,11 @@ let clone_meta tdt th sm = match tdt.td_node with
with Not_found -> None end
| _ -> invalid_arg "Theory.clone_meta"
let well_formed =
let preid =
{ pre_name = "well_formed"; pre_attrs = Sattr.empty; pre_loc = None } in
Term.create_lsymbol ~constr:0 preid [Ty.ty_var (Ty.tv_of_string "a")] None
(** Base theories *)
let builtin_theory =
......@@ -942,6 +947,13 @@ let create_theory ?(path=[]) n =
let bool_theory =
let uc = empty_theory (id_fresh "Bool") ["why3";"Bool"] in
let uc = add_data_decl uc [ts_bool, [fs_bool_true,[]; fs_bool_false,[]]] in
let uc =
let vs = Term.create_vsymbol
{pre_name = "a"; pre_attrs = Sattr.empty; pre_loc = None}
(Ty.ty_var (Ty.tv_of_string "a")) in
let d = Decl.make_ls_defn well_formed [vs] Term.t_true in
add_logic_decl uc [d]
in
close_theory uc
let highord_theory =
......
......@@ -234,6 +234,9 @@ val tuple_theory_name : string -> int option
val add_decl_with_tuples : theory_uc -> decl -> theory_uc
val well_formed: lsymbol
(* Symbol for the well_formed predicate *)
(* {2 Exceptions} *)
type badinstance_error =
......
......@@ -173,6 +173,8 @@ let rec eval_match kn stop env t =
t_attr_copy t (match t.t_node with
| Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
cs_equ env (eval env t1) (eval env t2)
| Tapp (ls, [_]) when ls_equal ls Theory.well_formed ->
Term.t_true
| Tnot { t_node = Tapp (ls, [t1;t2]) } when ls_equal ls ps_equ ->
t_not_simp (cs_equ env (eval env t1) (eval env t2))
| Tapp (ls, [t1]) when is_projection ls ->
......
......@@ -878,6 +878,14 @@ let e_func_app fn e =
let e_func_app_l fn el = List.fold_left e_func_app fn el
let wf_app = rs_of_ls Theory.well_formed
let wf_app =
let v_args = wf_app.rs_cty.cty_args in
let ity = wf_app.rs_cty.cty_result in
let c = create_cty v_args [] [] Mxs.empty Mpv.empty eff_empty ity in
LDsym (wf_app, c_any c)
(* boolean constructors *)
let e_if e0 e1 e2 =
......
......@@ -290,6 +290,8 @@ val ld_func_app : let_defn
val e_func_app : expr -> expr -> expr
val e_func_app_l : expr -> expr list -> expr
val wf_app: let_defn
(** {2 Pretty-printing} *)
val forget_rs : rsymbol -> unit (* flush id_unique for a program symbol *)
......
......@@ -604,9 +604,10 @@ let pd_func, pd_func_app = match highord_theory.th_decls with
mk_decl (PDlet ld_func_app) [da]
| _ -> assert false
let pd_bool = match bool_theory.th_decls with
| [{td_node = Decl db}] ->
mk_decl (PDtype [mk_itd its_bool [] [rs_true; rs_false] [] []]) [db]
let pd_bool, pd_wf = match bool_theory.th_decls with
| [{td_node = Decl db}; { td_node = Decl dw}] ->
mk_decl (PDtype [mk_itd its_bool [] [rs_true; rs_false] [] []]) [db],
mk_decl (PDlet Expr.wf_app) [dw]
| _ -> assert false
let pd_tuple = Wstdlib.Hint.memo 17 (fun n ->
......
......@@ -117,6 +117,7 @@ val pd_str : pdecl
val pd_tuple : int -> pdecl
val pd_func : pdecl
val pd_func_app : pdecl
val pd_wf : pdecl
(** {2 Known identifiers} *)
......
......@@ -391,6 +391,7 @@ let builtin_module =
let bool_module =
let uc = empty_module dummy_env (id_fresh "Bool") ["why3";"Bool"] in
let uc = add_pdecl_no_logic uc pd_bool in
let uc = add_pdecl_no_logic uc pd_wf in
let m = close_module uc in
{ m with mod_theory = bool_theory }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment