Commit 12125891 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: store variants in the specification

parent 22f5d8b2
......@@ -44,7 +44,7 @@ and pdecl_node =
| PDdata of data_decl list
| PDval of val_decl
| PDlet of let_defn
| PDrec of rec_defn list
| PDrec of rec_defn
| PDexn of xsymbol
let pd_equal : pdecl -> pdecl -> bool = (==)
......@@ -187,9 +187,9 @@ let create_let_decl ld =
*)
mk_decl (PDlet ld) (*syms*) news
let create_rec_decl rdl =
let create_rec_decl ({ rec_defn = rdl } as d) =
if rdl = [] then raise Decl.EmptyDecl;
let add_rd s { rec_ps = p } = check_vars p.ps_vars; news_id s p.ps_name in
let add_rd s { fun_ps = p } = check_vars p.ps_vars; news_id s p.ps_name in
let news = List.fold_left add_rd Sid.empty rdl in
(*
let add_rd syms { rec_ps = ps; rec_lambda = l; rec_vars = vm } =
......@@ -204,7 +204,7 @@ let create_rec_decl rdl =
syms_expr syms l.l_expr in
let syms = List.fold_left add_rd Sid.empty rdl in
*)
mk_decl (PDrec rdl) (*syms*) news
mk_decl (PDrec d) (*syms*) news
let create_val_decl vd =
let news = letvar_news vd.val_sym in
......
......@@ -45,7 +45,7 @@ and pdecl_node = private
| PDdata of data_decl list
| PDval of val_decl
| PDlet of let_defn
| PDrec of rec_defn list
| PDrec of rec_defn
| PDexn of xsymbol
(** {2 Declaration constructors} *)
......@@ -62,7 +62,7 @@ val create_val_decl : val_decl -> pdecl
val create_let_decl : let_defn -> pdecl
val create_rec_decl : rec_defn list -> pdecl
val create_rec_decl : rec_defn -> pdecl
val create_exn_decl : xsymbol -> pdecl
......
......@@ -101,11 +101,6 @@ type val_decl = {
val_vty : vty;
}
type variant = {
v_term : term; (* : tau *)
v_rel : lsymbol option; (* tau tau : prop *)
}
let add_pv_vars pv m = Mid.add pv.pv_vs.vs_name pv.pv_vtv.vtv_vars m
let add_vs_vars vs m = add_pv_vars (restore_pv vs) m
......@@ -114,25 +109,19 @@ let post_vars f vsset = Mvs.set_union vsset f.t_vars
let xpost_vars = Mexn.fold (fun _ -> post_vars)
let variant_vars varl vsset =
let add_variant s { v_term = t; v_rel = ps } =
begin match ps with
| Some ps -> ignore (ps_app ps [t;t])
| None -> t_ty_check t (Some ty_int)
(* TODO: allow algebraic types in variants *)
end;
Mvs.set_union s t.t_vars in
let add_variant s (t,_) = Mvs.set_union s t.t_vars in
List.fold_left add_variant vsset varl
let spec_varmap varm variant spec =
let spec_varmap varm spec =
let vsset = pre_vars spec.c_pre Mvs.empty in
let vsset = post_vars spec.c_post vsset in
let vsset = xpost_vars spec.c_xpost vsset in
let vsset = variant_vars variant vsset in
let vsset = variant_vars spec.c_variant vsset in
Mvs.fold (fun vs _ m -> add_vs_vars vs m) vsset varm
let rec vta_varmap vta =
let varm = vty_varmap vta.vta_result in
let varm = spec_varmap varm [] vta.vta_spec in
let varm = spec_varmap varm vta.vta_spec in
let del_pv m pv = Mid.remove pv.pv_vs.vs_name m in
List.fold_left del_pv varm vta.vta_args
......@@ -160,6 +149,8 @@ let eff_check vars result e =
let rec vta_check vars vta =
let add_arg vars pv = vars_union vars pv.pv_vtv.vtv_vars in
let vars = List.fold_left add_arg vars vta.vta_args in
if vta.vta_spec.c_variant <> [] || vta.vta_spec.c_letrec <> 0 then
Loc.errorm "variants are not allowed in a parameter declaration";
eff_check vars vta.vta_result vta.vta_spec.c_effect;
vty_check vars vta.vta_result
......@@ -373,7 +364,7 @@ and expr_node =
| Earrow of psymbol
| Eapp of expr * pvsymbol * spec
| Elet of let_defn * expr
| Erec of rec_defn list * expr
| Erec of rec_defn * expr
| Eif of expr * expr * expr
| Ecase of expr * (ppattern * expr) list
| Eassign of expr * region * pvsymbol
......@@ -393,8 +384,13 @@ and let_defn = {
}
and rec_defn = {
rec_ps : psymbol;
rec_lambda : lambda;
rec_defn : fun_defn list;
rec_letrec : int;
}
and fun_defn = {
fun_ps : psymbol;
fun_lambda : lambda;
}
and lambda = {
......@@ -511,27 +507,26 @@ let e_app_real e pv =
let eff = eff_union e.e_effect spec.c_effect in
mk_expr (Eapp (e,pv,spec)) vty eff (add_pv_vars pv e.e_varm)
let create_fun_defn id lam recsyms =
let create_fun_defn id lam letrec recsyms =
let e = lam.l_expr in
let spec = {
c_pre = lam.l_pre;
c_post = lam.l_post;
c_xpost = lam.l_xpost;
c_effect = e.e_effect; } in
let varm = Mid.set_diff e.e_varm recsyms in
let varm = spec_varmap varm lam.l_variant spec in
c_pre = lam.l_pre;
c_post = lam.l_post;
c_xpost = lam.l_xpost;
c_effect = e.e_effect;
c_variant = lam.l_variant;
c_letrec = letrec; } in
let varm = spec_varmap e.e_varm spec in
let varm = Mid.set_diff varm recsyms in
let del_pv m pv = Mid.remove pv.pv_vs.vs_name m in
let varm = List.fold_left del_pv varm lam.l_args in
let vta = vty_arrow lam.l_args ~spec e.e_vty in
{ rec_ps = create_psymbol_poly id vta varm;
rec_lambda = lam; }
{ fun_ps = create_psymbol_poly id vta varm;
fun_lambda = lam; }
(* FIXME: if the given rdl is not the result of create_rec_defn,
the varmap calculation below might be off. We should probably
make [rec_defn list] a private type. *)
let e_rec rdl e =
let add_varm m rd = varmap_union m rd.rec_ps.ps_varm in
let varm = List.fold_left add_varm e.e_varm rdl in
let add_varm m rd = varmap_union m rd.fun_ps.ps_varm in
let varm = List.fold_left add_varm e.e_varm rdl.rec_defn in
mk_expr (Erec (rdl,e)) e.e_vty e.e_effect varm
let on_value fn e = match e.e_node with
......@@ -689,9 +684,11 @@ let e_ghost e =
mk_expr (Eghost e) (vty_ghostify e.e_vty) e.e_effect e.e_varm
let e_any spec vty =
let varm = spec_varmap (vty_varmap vty) [] spec in
let varm = spec_varmap (vty_varmap vty) spec in
let vars = vars_merge varm vars_empty in
spec_check spec vty;
if spec.c_variant <> [] || spec.c_letrec <> 0 then
Loc.errorm "variants are not allowed in a parameter declaration";
eff_check vars vty spec.c_effect;
vty_check vars vty;
mk_expr (Eany spec) vty spec.c_effect varm
......@@ -829,12 +826,14 @@ let e_try e0 bl =
let e_abstract e q xq =
let spec = {
c_pre = t_true;
c_post = q;
c_xpost = xq;
c_effect = e.e_effect; } in
c_pre = t_true;
c_post = q;
c_xpost = xq;
c_effect = e.e_effect;
c_variant = [];
c_letrec = 0 } in
spec_check spec e.e_vty;
let varm = spec_varmap e.e_varm [] spec in
let varm = spec_varmap e.e_varm spec in
mk_expr (Eabstr (e,q,xq)) e.e_vty e.e_effect varm
let e_assert ak f =
......@@ -890,12 +889,12 @@ let rec expr_subst psm e = match e.e_node with
let ld = create_let_defn (id_clone ps.ps_name) (expr_subst psm d) in
let ns = match ld.let_sym with LetA a -> a | LetV _ -> assert false in
e_let ld (expr_subst (Mid.add ps.ps_name ns psm) e)
| Erec (rdl,e) ->
| Erec ({ rec_defn = rdl; rec_letrec = letrec }, e) ->
let conv lam = { lam with l_expr = expr_subst psm lam.l_expr } in
let defl = List.map (fun rd -> rd.rec_ps, conv rd.rec_lambda) rdl in
let rdl = create_rec_defn defl in
let add psm (ps,_) rd = Mid.add ps.ps_name rd.rec_ps psm in
e_rec rdl (expr_subst (List.fold_left2 add psm defl rdl) e)
let defl = List.map (fun rd -> rd.fun_ps, conv rd.fun_lambda) rdl in
let rdl = create_rec_defn letrec defl in
let add psm (ps,_) rd = Mid.add ps.ps_name rd.fun_ps psm in
e_rec rdl (expr_subst (List.fold_left2 add psm defl rdl.rec_defn) e)
| Eif (e,e1,e2) ->
e_if (expr_subst psm e) (expr_subst psm e1) (expr_subst psm e2)
| Ecase (e,bl) ->
......@@ -918,21 +917,22 @@ let rec expr_subst psm e = match e.e_node with
e_for_real pv bounds inv (expr_subst psm e)
| Elogic _ | Evalue _ | Earrow _ | Eany _ | Eabsurd | Eassert _ -> e
and create_rec_defn defl =
and create_rec_defn letrec defl =
let add_sym acc (ps,_) = Sid.add ps.ps_name acc in
let recsyms = List.fold_left add_sym Sid.empty defl in
let conv m (ps,lam) =
let rd = create_fun_defn (id_clone ps.ps_name) lam recsyms in
if ps_compat ps rd.rec_ps then m, { rd with rec_ps = ps }
else Mid.add ps.ps_name rd.rec_ps m, rd in
let rd = create_fun_defn (id_clone ps.ps_name) lam letrec recsyms in
if ps_compat ps rd.fun_ps then m, { rd with fun_ps = ps }
else Mid.add ps.ps_name rd.fun_ps m, rd in
let m, rdl = Util.map_fold_left conv Mid.empty defl in
if Mid.is_empty m then rdl else subst_rd m rdl
if Mid.is_empty m then { rec_defn = rdl; rec_letrec = letrec }
else subst_rd letrec m rdl
and subst_rd psm rdl =
let subst { rec_ps = ps; rec_lambda = lam } =
and subst_rd letrec psm rdl =
let subst { fun_ps = ps; fun_lambda = lam } =
Mid.find_def ps ps.ps_name psm,
{ lam with l_expr = expr_subst psm lam.l_expr } in
create_rec_defn (List.map subst rdl)
create_rec_defn letrec (List.map subst rdl)
(* Before we start computing the fixpoint for effects, we must
get the pre/post/xpost right. Therefore we require every ps
......@@ -943,30 +943,32 @@ and subst_rd psm rdl =
and with the same final spec (except the effect). The result
is passed to create_rec_defn above which repeats substitution
until the effects are stabilized. TODO: prove correctness *)
let create_rec_defn defl =
let create_rec_defn = let letrec = ref 0 in fun defl ->
incr letrec;
let add_sym acc (ps,_) = Sid.add ps.ps_name acc in
let recsyms = List.fold_left add_sym Sid.empty defl in
let conv m (ps,lam) = match lam.l_expr.e_vty with
| VTarrow _ -> Loc.errorm ?loc:lam.l_expr.e_loc
"The body of a recursive function must be a first-order value"
| VTvalue _ ->
let rd = create_fun_defn (id_clone ps.ps_name) lam recsyms in
Mid.add ps.ps_name rd.rec_ps m, rd in
let rd = create_fun_defn (id_clone ps.ps_name) lam !letrec recsyms in
Mid.add ps.ps_name rd.fun_ps m, rd in
let m, rdl = Util.map_fold_left conv Mid.empty defl in
subst_rd m rdl
subst_rd !letrec m rdl
let create_fun_defn id lam =
if lam.l_variant <> [] then
Loc.errorm "Variants are not allowed in a non-recursive definition";
create_fun_defn id lam Sid.empty
Loc.errorm "variants are not allowed in a non-recursive definition";
let fd = create_fun_defn id lam 0 Sid.empty in
{ rec_defn = [fd]; rec_letrec = 0 }
(* fold *)
let e_fold fn acc e = match e.e_node with
| Elet (ld,e) -> fn (fn acc ld.let_expr) e
| Erec (rdl,e) ->
let fnrd acc rd = fn acc rd.rec_lambda.l_expr in
fn (List.fold_left fnrd acc rdl) e
let fnrd acc rd = fn acc rd.fun_lambda.l_expr in
fn (List.fold_left fnrd acc rdl.rec_defn) e
| Ecase (e,bl) ->
let fnbr acc (_,e) = fn acc e in
List.fold_left fnbr (fn acc e) bl
......
......@@ -139,7 +139,7 @@ and expr_node = private
| Earrow of psymbol
| Eapp of expr * pvsymbol * spec
| Elet of let_defn * expr
| Erec of rec_defn list * expr
| Erec of rec_defn * expr
| Eif of expr * expr * expr
| Ecase of expr * (ppattern * expr) list
| Eassign of expr * region * pvsymbol
......@@ -159,8 +159,13 @@ and let_defn = private {
}
and rec_defn = private {
rec_ps : psymbol;
rec_lambda : lambda;
rec_defn : fun_defn list;
rec_letrec : int;
}
and fun_defn = private {
fun_ps : psymbol;
fun_lambda : lambda;
}
and lambda = {
......@@ -172,11 +177,6 @@ and lambda = {
l_xpost : xpost;
}
and variant = {
v_term : term; (* : tau *)
v_rel : lsymbol option; (* tau tau : prop *)
}
val e_label : ?loc:Loc.position -> Slab.t -> expr -> expr
val e_label_add : label -> expr -> expr
val e_label_copy : expr -> expr -> expr
......@@ -200,13 +200,13 @@ val e_plapp : plsymbol -> expr list -> ity -> expr
val create_let_defn : preid -> expr -> let_defn
val create_fun_defn : preid -> lambda -> rec_defn
val create_rec_defn : (psymbol * lambda) list -> rec_defn list
val create_rec_defn : (psymbol * lambda) list -> rec_defn
exception StaleRegion of expr * region * ident
(* freshness violation: a previously reset region is associated to an ident *)
val e_let : let_defn -> expr -> expr
val e_rec : rec_defn list -> expr -> expr
val e_rec : rec_defn -> expr -> expr
val e_if : expr -> expr -> expr -> expr
val e_case : expr -> (ppattern * expr) list -> expr
......
......@@ -277,7 +277,7 @@ let add_let uc = function
| LetV pv -> add_symbol add_ps pv.pv_vs.vs_name (PV pv) uc
| LetA ps -> add_symbol add_ps ps.ps_name (PS ps) uc
let add_rec uc { rec_ps = ps } =
let add_rec uc { fun_ps = ps } =
add_symbol add_ps ps.ps_name (PS ps) uc
let add_exn uc xs =
......@@ -314,7 +314,7 @@ let add_pdecl uc d =
| PDval { val_sym = lv } | PDlet { let_sym = lv } ->
add_let uc lv
| PDrec rdl ->
List.fold_left add_rec uc rdl
List.fold_left add_rec uc rdl.rec_defn
| PDexn xs ->
add_exn uc xs
......
......@@ -192,7 +192,7 @@ let print_variant fmt varl =
let print_rel fmt = function
| Some ps -> fprintf fmt "@ [%a]" Pretty.print_ls ps
| None -> () in
let print_var fmt { v_term = t; v_rel = ps } =
let print_var fmt (t, ps) =
fprintf fmt " %a%a" Pretty.print_term t print_rel ps in
fprintf fmt "variant@ {%a }@ " (print_list comma print_var) varl
......@@ -276,10 +276,10 @@ and print_enode pri fmt e = match e.e_node with
fprintf fmt (protect_on (pri > 0) "@[<hov 2>let %a =@ %a@ in@]@\n%a")
print_lv lv (print_lexpr 4) e1 print_expr e2;
forget_lv lv
| Erec (rdl,e) ->
| Erec ({ rec_defn = rdl }, e) ->
fprintf fmt (protect_on (pri > 0) "%a@ in@\n%a")
(print_list_next newline print_rec) rdl print_expr e;
let forget_rd rd = forget_ps rd.rec_ps in
let forget_rd rd = forget_ps rd.fun_ps in
List.iter forget_rd rdl
| Eif (e0,e1,e2) ->
fprintf fmt (protect_on (pri > 0) "if %a then %a@ else %a")
......@@ -323,7 +323,7 @@ and print_xbranch fmt (xs, pv, e) =
fprintf fmt "@[<hov 4>| %a %a ->@ %a@]" print_xs xs print_pv pv print_expr e;
forget_pv pv
and print_rec fst fmt { rec_ps = ps ; rec_lambda = lam } =
and print_rec fst fmt { fun_ps = ps ; fun_lambda = lam } =
let print_arg fmt pv = fprintf fmt "@[(%a)@]" print_pvty pv in
fprintf fmt "@[<hov 2>%s (%a)@ %a =@\n{ %a }@\n%a%a@\n{ %a }@]"
(if fst then "let rec" else "with")
......@@ -416,7 +416,7 @@ let print_pdecl fmt d = match d.pd_node with
| PDdata tl -> print_list_next newline print_data_decl fmt tl
| PDval vd -> print_val_decl fmt vd
| PDlet ld -> print_let_decl fmt ld
| PDrec rdl -> print_list_next newline print_rec_decl fmt rdl
| PDrec rdl -> print_list_next newline print_rec_decl fmt rdl.rec_defn
| PDexn xs -> print_exn_decl fmt xs
let print_next_data_decl = print_data_decl false
......
......@@ -633,6 +633,8 @@ type pre = term (* precondition: pre_fmla *)
type post = term (* postcondition: eps result . post_fmla *)
type xpost = post Mexn.t (* exceptional postconditions *)
type variant = term * lsymbol option (* tau * (tau -> tau -> prop) *)
let create_post vs f = t_eps_close vs f
let open_post f = match f.t_node with
......@@ -644,39 +646,48 @@ let check_post ty f = match f.t_node with
| _ -> Loc.errorm "invalid post-condition"
type spec = {
c_pre : pre;
c_post : post;
c_xpost : xpost;
c_effect : effect;
c_pre : pre;
c_post : post;
c_xpost : xpost;
c_effect : effect;
c_variant : variant list;
c_letrec : int;
}
let spec_empty ty = {
c_pre = t_true;
c_post = create_post (create_vsymbol (id_fresh "dummy") ty) t_true;
c_xpost = Mexn.empty;
c_effect = eff_empty;
c_pre = t_true;
c_post = create_post (create_vsymbol (id_fresh "dummy") ty) t_true;
c_xpost = Mexn.empty;
c_effect = eff_empty;
c_variant = [];
c_letrec = 0;
}
let spec_full_inst sbs tvm vsm c =
let subst = t_ty_subst tvm vsm in {
c_pre = subst c.c_pre;
c_post = subst c.c_post;
c_xpost = Mexn.map subst c.c_xpost;
c_effect = eff_full_inst sbs c.c_effect;
c_pre = subst c.c_pre;
c_post = subst c.c_post;
c_xpost = Mexn.map subst c.c_xpost;
c_effect = eff_full_inst sbs c.c_effect;
c_variant = List.map (fun (t,rel) -> subst t, rel) c.c_variant;
c_letrec = c.c_letrec;
}
let spec_subst sbs c =
let subst = t_subst sbs in {
c_pre = subst c.c_pre;
c_post = subst c.c_post;
c_xpost = Mexn.map subst c.c_xpost;
c_effect = c.c_effect;
c_pre = subst c.c_pre;
c_post = subst c.c_post;
c_xpost = Mexn.map subst c.c_xpost;
c_effect = c.c_effect;
c_variant = List.map (fun (t,rel) -> subst t, rel) c.c_variant;
c_letrec = c.c_letrec;
}
let spec_filter varm vars c =
let add _ f s = Mvs.set_union f.t_vars s in
let vss = add () c.c_pre c.c_post.t_vars in
let vss = Mexn.fold add c.c_xpost vss in
let add f s = Mvs.set_union f.t_vars s in
let vss = add c.c_pre c.c_post.t_vars in
let vss = Mexn.fold (fun _ -> add) c.c_xpost vss in
let vss = List.fold_right (fun (t,_) -> add t) c.c_variant vss in
let check { vs_name = id } _ = if not (Mid.mem id varm) then
Loc.errorm "Local variable %s escapes from its scope" id.id_string in
Mvs.iter check vss;
......@@ -689,6 +700,10 @@ let spec_check c ty =
Loc.error ?loc:c.c_pre.t_loc (Term.FmlaExpected c.c_pre);
check_post ty c.c_post;
Mexn.iter (fun xs q -> check_post (ty_of_ity xs.xs_ity) q) c.c_xpost;
let check_variant (t,rel) = match rel with
| Some ps -> ignore (ps_app ps [t;t])
| None -> t_ty_check t (Some ty_int) in
List.iter check_variant c.c_variant;
let sexn = Sexn.union c.c_effect.eff_raises c.c_effect.eff_ghostx in
let sexn = Mexn.set_diff sexn c.c_xpost in
if not (Sexn.is_empty sexn) then
......
......@@ -235,14 +235,18 @@ type pre = term (* precondition: pre_fmla *)
type post = term (* postcondition: eps result . post_fmla *)
type xpost = post Mexn.t (* exceptional postconditions *)
type variant = term * lsymbol option (* tau * (tau -> tau -> prop) *)
val create_post : vsymbol -> term -> post
val open_post : post -> vsymbol * term
type spec = {
c_pre : pre;
c_post : post;
c_xpost : xpost;
c_effect : effect;
c_pre : pre;
c_post : post;
c_xpost : xpost;
c_effect : effect;
c_variant : variant list;
c_letrec : int;
}
(** program variables *)
......
......@@ -675,7 +675,7 @@ let create_pre lenv f =
let create_variant lenv (t,r) =
let t = Typing.type_term lenv.th_at lenv.log_denv lenv.log_vars t in
count_term_tuples t;
{ v_term = t; v_rel = r }
t, r
let add_local x lv lenv = match lv with
| LetA _ ->
......@@ -791,10 +791,12 @@ let rec type_c lenv gh vars dtyc =
and add_ity ity eff = Sreg.fold add_reg ity.ity_vars.vars_reg eff in
add_ity v.vtv_ity eff
| VTarrow _ -> eff in
{ c_pre = create_pre lenv dtyc.dc_pre;
c_effect = eff;
c_post = create_post lenv "result" vty dtyc.dc_post;
c_xpost = xpost lenv dtyc.dc_xpost }, vty
{ c_pre = create_pre lenv dtyc.dc_pre;
c_effect = eff;
c_post = create_post lenv "result" vty dtyc.dc_post;
c_xpost = xpost lenv dtyc.dc_xpost;
c_variant = [];
c_letrec = 0 }, vty
and type_v lenv gh vars = function
| DSpecV (ghost,v) ->
......@@ -832,21 +834,21 @@ and expr_desc lenv loc de = match de.de_desc with
end
end
| DElet (x, gh, { de_desc = DEfun lam }, de2) ->
let def = expr_fun lenv x gh lam in
let lenv = add_local x.id (LetA def.rec_ps) lenv in
let def, ps = expr_fun lenv x gh lam in
let lenv = add_local x.id (LetA ps) lenv in
let e2 = expr lenv de2 in
e_rec [def] e2
e_rec def e2
| DEfun lam ->
let x = mk_id "fn" loc in
let def = expr_fun lenv x false lam in
let e2 = e_arrow def.rec_ps def.rec_ps.ps_vta in
e_rec [def] e2
let def, ps = expr_fun lenv x false lam in
let e2 = e_arrow ps ps.ps_vta in
e_rec def e2
(* FIXME? (ghost "lab" fun x -> ...) loses the label "lab" *)
| DEghost { de_desc = DEfun lam } ->
let x = mk_id "fn" loc in
let def = expr_fun lenv x true lam in
let e2 = e_arrow def.rec_ps def.rec_ps.ps_vta in
e_rec [def] e2
let def, ps = expr_fun lenv x true lam in
let e2 = e_arrow ps ps.ps_vta in
e_rec def e2
| DElet (x, gh, de1, de2) ->
let e1 = e_ghostify gh (expr lenv de1) in
begin match e1.e_vty with
......@@ -860,8 +862,8 @@ and expr_desc lenv loc de = match de.de_desc with
e_let def1 e2
| DEletrec (rdl, de1) ->
let rdl = expr_rec lenv rdl in
let add_rd { rec_ps = ps } = add_local ps.ps_name.id_string (LetA ps) in
let e1 = expr (List.fold_right add_rd rdl lenv) de1 in
let add_rd { fun_ps = ps } = add_local ps.ps_name.id_string (LetA ps) in
let e1 = expr (List.fold_right add_rd rdl.rec_defn lenv) de1 in
e_rec rdl e1
| DEapply (de1, del) ->
let el = List.map (expr lenv) del in
......@@ -970,7 +972,8 @@ and expr_rec lenv rdl =
and expr_fun lenv x gh lam =
let lam = expr_lam lenv gh lam in
create_fun_defn (Denv.create_user_id x) lam
let def = create_fun_defn (Denv.create_user_id x) lam in
def, (List.hd def.rec_defn).fun_ps
and expr_lam lenv gh (bl, var, p, de, q, xq) =
let lenv, pvl = binders lenv bl in
......@@ -1460,8 +1463,8 @@ let add_module lib path mm mt m =
let e = dexpr (create_denv uc) e in
let pd = match e.de_desc with
| DEfun lam ->
let def = expr_fun (create_lenv uc) id gh lam in
create_rec_decl [def]
let def, _ = expr_fun (create_lenv uc) id gh lam in
create_rec_decl def
| _ ->
let e = e_ghostify gh (expr (create_lenv uc) e) in
if not gh && vty_ghost e.e_vty then
......
......@@ -228,7 +228,7 @@ type wp_env = {
let decrease ?loc env mk_old varl =
let rec decr pr = function
| [] -> t_false
| { v_term = t; v_rel = rel }::varl ->
| (t, rel)::varl ->
let old_t = mk_old t in
let d = match rel with
| Some ls -> ps_app ls [t; old_t]
......@@ -558,7 +558,7 @@ and wp_lambda env l =
wp_forall (List.map (fun pv -> pv.pv_vs) l.l_args) f
and wp_rec_defn env rdl =
List.map (fun rd -> wp_lambda env rd.rec_lambda) rdl
List.map (fun rd -> wp_lambda env rd.fun_lambda) rdl.rec_defn
(***
let bool_to_prop env f =
......@@ -660,10 +660,10 @@ let wp_rec env km th rdl =
let fl = wp_rec_defn env rdl in
let add_one th d f =
Debug.dprintf debug "wp %s = %a@\n----------------@."
d.rec_ps.ps_name.id_string Pretty.print_term f;
d.fun_ps.ps_name.id_string Pretty.print_term f;
let f = wp_forall (Mvs.keys f.t_vars) f in
add_wp_decl d.rec_ps.ps_name f th
add_wp_decl d.fun_ps.ps_name f th
in
List.fold_left2 add_one th rdl fl
List.fold_left2 add_one th rdl.rec_defn fl
let wp_val _env _km th _vd = th
......@@ -44,4 +44,4 @@ val remove_old : Term.term -> Term.term
val wp_val: Env.env -> known_map -> theory_uc -> val_decl -> theory_uc
val wp_let: Env.env -> known_map -> theory_uc -> let_defn -> theory_uc
val wp_rec: Env.env -> known_map -> theory_uc -> rec_defn list -> theory_uc
val wp_rec: Env.env -> known_map -> theory_uc -> rec_defn -> theory_uc
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