Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 6e120719 authored by Andrei Paskevich's avatar Andrei Paskevich

Mlw: logical declarations for let-definitions

parent 5f632c77
......@@ -759,6 +759,8 @@ let effect_of_dspec dsp =
let eff = if dsp.ds_diverge then eff_diverge eff else eff in
wl, eff
(* TODO: add warnings for empty postconditions (anywhere)
and empty exceptional postconditions (toplevel). *)
let check_spec dsp ecty e =
let bad_write weff eff = not (Mreg.submap (fun _ s1 s2 -> Spv.subset s1 s2)
weff.eff_writes eff.eff_writes) in
......@@ -790,8 +792,6 @@ let check_spec dsp ecty e =
if check_rwd && bad_write eeff ueff then
Loc.errorm ?loc:(e_locate_effect (fun eff -> bad_write eff ueff) e)
"this@ expression@ produces@ an@ unlisted@ write@ effect";
(* TODO FIXME : revise the requirements for explicit "raises".
Should we only require them at the top level? *)
if ecty.cty_args <> [] && bad_raise eeff ueff then Sexn.iter (fun xs ->
Loc.errorm ?loc:(e_locate_effect (fun eff -> Sexn.mem xs eff.eff_raises) e)
"this@ expression@ raises@ unlisted@ exception@ %a"
......@@ -936,11 +936,6 @@ let cty_of_spec env bl dsp dity =
(** Expressions *)
(*
let implicit_post = Debug.register_flag "implicit_post"
~desc:"Generate@ a@ postcondition@ for@ pure@ functions@ without@ one."
*)
let warn_unused s loc =
if s = "" || s.[0] <> '_' then
Warning.emit ?loc "unused variable %s" s
......
......@@ -482,7 +482,7 @@ let rec raw_of_expr e = copy_labels e (match e.e_node with
| Tbinop (Tiff, {t_node =
Tapp (ps,[{t_node = Tvar u}; {t_node = Tapp (fs,[])}])},f)
when ls_equal ps ps_equ && vs_equal v u &&
ls_equal fs fs_bool_true && t_v_occurs v f = 0 -> f
ls_equal fs fs_bool_true && t_v_occurs v f = 0 -> f
| _ -> raise Exit in
begin match t.t_node, al with
| Tapp (s, tl), _::_ ->
......@@ -520,8 +520,7 @@ let rec raw_of_expr e = copy_labels e (match e.e_node with
t_or (pure_of_expr true e0) (pure_of_expr true e2)
| Eif (e0,e1,e2) ->
let prop = ity_equal e.e_ity ity_bool in
t_if (pure_of_expr true e0)
(pure_of_expr prop e1) (pure_of_expr prop e2)
t_if (pure_of_expr true e0) (pure_of_expr prop e1) (pure_of_expr prop e2)
| Ecase (d,bl) ->
let prop = ity_equal e.e_ity ity_bool in
let conv (p,e) = t_close_branch p.pp_pat (pure_of_expr prop e) in
......@@ -529,25 +528,70 @@ let rec raw_of_expr e = copy_labels e (match e.e_node with
| Etry _ | Eraise _ | Eabsurd -> raise Exit)
and pure_of_expr prop e =
let loca f = t_label ?loc:e.e_loc Slab.empty f in
let t = raw_of_expr e in
match t.t_ty with
| Some _ when prop ->
t_label ?loc:t.t_loc Slab.empty (t_equ_simp t t_bool_true)
| None when not prop ->
t_label ?loc:t.t_loc Slab.empty (t_if_simp t t_bool_true t_bool_false)
| None when not prop -> loca (t_if_simp t t_bool_true t_bool_false)
| Some _ when prop -> loca (t_equ_simp t t_bool_true)
| _ -> t
let fmla_of_expr e =
let term_of_expr ~prop e =
if not (eff_pure e.e_effect) then None else
try Some (pure_of_expr true e) with Exit -> None
let term_of_expr e =
if not (eff_pure e.e_effect) then None else
try Some (pure_of_expr false e) with Exit -> None
let post_of_expr e =
if not (eff_pure e.e_effect) then None else
try Some (raw_of_expr e) with Exit -> None
try Some (pure_of_expr prop e) with Exit -> None
let post_of_term res t =
let loca f = t_label ?loc:t.t_loc Slab.empty f in
let f_of_t t = loca (t_equ_simp t t_bool_true) in
match res.t_ty, t.t_ty with
| Some _, Some _ -> loca (t_equ_simp res t)
| None, None -> loca (t_iff_simp res t)
| Some _, None -> loca (t_iff_simp (f_of_t res) t)
| None, Some _ -> loca (t_iff_simp res (f_of_t t))
let rec post_of_expr res e = match e.e_node with
| _ when ity_equal e.e_ity ity_unit -> t_true
| Eassign _ | Ewhile _ | Efor _ | Eassert _ -> assert false
| Eabsurd -> copy_labels e t_false
| Elet (LDvar (v,_d),e) when ity_equal v.pv_ity ity_unit ->
copy_labels e (t_subst_single v.pv_vs t_void (post_of_expr res e))
| Elet (LDvar (v,d),e) ->
copy_labels e (t_let_close_simp v.pv_vs
(pure_of_expr false d) (post_of_expr res e))
| Elet (LDsym (s,_),e) ->
if is_rlpv s then raise Exit;
copy_labels e (post_of_expr res e)
| Elet (LDrec rdl,e) ->
if List.exists (fun rd -> is_rlpv rd.rec_sym) rdl then raise Exit;
copy_labels e (post_of_expr res e)
| Eif (_,e1,e2) when is_e_true e1 || is_e_false e2 ||
(is_e_false e1 && is_e_true e2) ->
post_of_term res (raw_of_expr e)
| Eif (e0,e1,e2) ->
t_if (pure_of_expr true e0) (post_of_expr res e1) (post_of_expr res e2)
| Ecase (d,bl) ->
let conv (p,e) = t_close_branch p.pp_pat (post_of_expr res e) in
t_case (pure_of_expr false d) (List.map conv bl)
| Etry _ | Eraise _ -> raise Exit
| _ -> post_of_term res (raw_of_expr e)
let local_post_of_expr e =
if ity_equal e.e_ity ity_unit || not (eff_pure e.e_effect) then [] else
let res = create_vsymbol (id_fresh "result") (ty_of_ity e.e_ity) in
try [create_post res (post_of_expr (t_var res) e)] with Exit -> []
let post_of_expr res e =
ty_equal_check (ty_of_ity e.e_ity)
(match res.t_ty with Some ty -> ty | None -> ty_bool);
if ity_equal e.e_ity ity_unit || not (eff_pure e.e_effect) then None
else try
(* we avoid capturing the free variables of res *)
let clone v _ = create_vsymbol (id_clone v.vs_name) v.vs_ty in
let sbs = Mvs.mapi clone (t_vars res) in
let res = t_subst (Mvs.map t_var sbs) res in
let q = post_of_expr res e in
let inverse o n m = Mvs.add n (t_var o) m in
Some (t_subst (Mvs.fold inverse sbs Mvs.empty) q)
with Exit -> None
(* let-definitions *)
......@@ -565,10 +609,9 @@ let let_sym id ?(ghost=false) ?(kind=RKnone) c =
the antecedents of WP, but provers must perform beta-reduction
to apply it: auto-inlining might be really helpful here. *)
let cty = match c with
| {c_node = Cfun e; c_cty = {cty_post = []} as c}
| {c_node = Cfun e; c_cty = {cty_post = []}}
when (kind = RKnone (*|| kind = RKlocal*)) ->
begin match post_of_expr e with
| Some t -> add_post c t | None -> c end
cty_add_post c.c_cty (local_post_of_expr e)
| _ -> c.c_cty in
let s = create_rsymbol id ~ghost:(c_ghost c) ~kind cty in
LDsym (s,c), s
......@@ -868,7 +911,7 @@ and rec_fixp dl =
if c_ghost d <> rs_ghost s then Loc.errorm
"Expr.let_rec: ghost status mismatch";
let c = if List.length c.cty_pre < List.length s.rs_cty.cty_pre
then c else cty_add_pre [List.hd s.rs_cty.cty_pre] c in
then cty_add_pre [List.hd s.rs_cty.cty_pre] c else c in
if eff_equal c.cty_effect s.rs_cty.cty_effect then sm, (s,d)
else let n = rs_dup s c in Mrs.add s n sm, (n,d) in
let sm, dl = Lists.map_fold_left update Mrs.empty dl in
......
......@@ -247,8 +247,8 @@ val proxy_label : label
val e_rs_subst : rsymbol Mrs.t -> expr -> expr
val c_rs_subst : rsymbol Mrs.t -> cexp -> cexp
val term_of_expr : expr -> term option
val fmla_of_expr : expr -> term option
val term_of_expr : prop:bool -> expr -> term option
val post_of_expr : term -> expr -> term option
(** {2 Built-in symbols} *)
......
......@@ -339,22 +339,99 @@ let create_type_decl dl =
let defn = if defn = [] then [] else [create_data_decl defn] in
mk_decl (PDtype dl) (abst @ defn @ rest)
(* TODO: share with Eliminate_definition *)
let rec t_insert hd t = match t.t_node with
| Tif (f1,t2,t3) ->
t_if f1 (t_insert hd t2) (t_insert hd t3)
| Tlet (t1,bt) ->
let v,t2 = t_open_bound bt in
t_let_close v t1 (t_insert hd t2)
| Tcase (tl,bl) ->
t_case tl (List.map (fun b ->
let pl,t1 = t_open_branch b in
t_close_branch pl (t_insert hd t1)) bl)
| _ when hd.t_ty = None -> t_iff_simp hd t
| _ -> t_equ_simp hd t
let create_let_decl ld =
let ls_of_rs s dl = match s.rs_logic with
| RLnone | RLlemma -> dl
let conv_post t q =
let v,f = open_post q in t_subst_single v t f in
let conv_post t ql = List.map (conv_post t) ql in
let cty_axiom id cty f =
(* FIXME: this is unsound in presence of aliases *)
let add_old o v m = Mvs.add o.pv_vs (t_var v.pv_vs) m in
let sbs = Mpv.fold add_old cty.cty_oldies Mvs.empty in
let f = List.fold_right t_implies cty.cty_pre (t_subst sbs f) in
let args = List.map (fun v -> v.pv_vs) cty.cty_args in
let f = t_forall_close args [] f in
let f = t_forall_close (Mvs.keys (t_vars f)) [] f in
create_prop_decl Paxiom (create_prsymbol id) f in
let cty_axiom id cty f axms =
if t_equal f t_true then axms
else cty_axiom id cty f :: axms in
let add_ls sm s ({c_cty = cty} as c) (abst,defn,axms) =
match s.rs_logic with
| RLpv _ -> invalid_arg "Pdecl.create_let_decl"
| RLls s -> create_param_decl s :: dl in
let ldl = match ld with
| RLnone -> abst, defn, axms
| RLlemma ->
let f = if ity_equal cty.cty_result ity_unit then
t_and_simp_l (conv_post t_void cty.cty_post)
else match cty.cty_post with
| q::ql ->
let v, f = open_post q in
let fl = f :: conv_post (t_var v) ql in
t_exists_close [v] [] (t_and_simp_l fl)
| [] -> t_true in
abst, defn, cty_axiom (id_clone s.rs_name) cty f axms
| RLls ls ->
let vl = List.map (fun v -> v.pv_vs) cty.cty_args in
let t = t_app ls (List.map t_var vl) ls.ls_value in
let f = t_and_simp_l (conv_post t cty.cty_post) in
let axms = cty_axiom (id_clone ls.ls_name) cty f axms in
let c = if Mrs.is_empty sm then c else c_rs_subst sm c in
begin match c.c_node with
| Cany | Capp _ ->
create_param_decl ls :: abst, defn, axms
| Cfun e ->
let res = if c.c_cty.cty_pre <> [] then None else
term_of_expr ~prop:(ls.ls_value = None) e in
begin match res with
| Some f -> abst, (ls, vl, f) :: defn, axms
| None ->
let axms = match post_of_expr t e with
| Some f ->
let nm = ls.ls_name.id_string ^ "_def" in
cty_axiom (id_derive nm ls.ls_name) cty f axms
| None -> axms in
create_param_decl ls :: abst, defn, axms
end
end in
let abst, defn, axms = match ld with
| LDvar ({pv_vs = {vs_name = {id_loc = loc}}},e) ->
if not (ity_closed e.e_ity) then
Loc.errorm ?loc "Top-level variables must have monomorphic type";
if match e.e_node with Eexec _ -> false | _ -> true then
Loc.errorm ?loc "Top-level computations must carry a specification";
[]
| LDrec rdl -> List.fold_right (fun d dl -> ls_of_rs d.rec_sym dl) rdl []
| LDsym (s,_) -> ls_of_rs s [] in
(* TODO: real function definitions and lemmas *)
mk_decl (PDlet ld) ldl
[], [], []
| LDrec rdl ->
let add_rd sm d = Mrs.add d.rec_rsym d.rec_sym sm in
let sm = List.fold_left add_rd Mrs.empty rdl in
let add_rd d dl = add_ls sm d.rec_sym d.rec_fun dl in
List.fold_right add_rd rdl ([],[],[])
| LDsym (s,c) ->
add_ls Mrs.empty s c ([],[],[]) in
let defn = if defn = [] then [] else
let dl = List.map (fun (s,vl,t) -> make_ls_defn s vl t) defn in
try [create_logic_decl dl] with Decl.NoTerminationProof _ ->
let abst = List.map (fun (s,_) -> create_param_decl s) dl in
let mk_ax ({ls_name = id} as s, vl, t) =
let nm = id.id_string ^ "_def" in
let pr = create_prsymbol (id_derive nm id) in
let hd = t_app s (List.map t_var vl) t.t_ty in
let ax = t_forall_close vl [] (t_insert hd t) in
create_prop_decl Paxiom pr ax in
abst @ List.map mk_ax defn in
mk_decl (PDlet ld) (abst @ defn @ axms)
let create_exn_decl xs =
if not (ity_closed xs.xs_ity) then Loc.errorm ?loc:xs.xs_name.id_loc
......
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