Commit 335c4f8e authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: get rid of spec.c_letrec

parent 3f6de048
......@@ -303,8 +303,10 @@ let pd_vars pd = match pd.pd_node with
| PDval (LetA ps) -> Mid.map (fun _ -> ()) ps.ps_varm
| PDlet ld -> Mid.map (fun _ -> ()) ld.let_expr.e_varm
| PDrec rd ->
let add_rd s fd = Mid.set_union s fd.fun_ps.ps_varm in
let add_rd s fd = Mid.set_union s fd.fun_varm in
let del_rd s fd = Mid.remove fd.fun_ps.ps_name s in
let varm = List.fold_left add_rd Mid.empty rd.rec_defn in
let varm = List.fold_left del_rd varm rd.rec_defn in
Mid.map (fun _ -> ()) varm
| PDtype _ | PDdata _ | PDexn _ -> Sid.empty
......
......@@ -409,7 +409,7 @@ let vtv_check vars eff vtv =
let rec vta_check vars vta =
let add_arg vars pv = vars_union vars pv.pv_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
if vta.vta_spec.c_variant <> [] then
Loc.errorm "variants are not allowed in a parameter declaration";
eff_check vars vta.vta_result vta.vta_spec.c_effect;
match vta.vta_result with
......@@ -479,12 +479,12 @@ and let_defn = {
and rec_defn = {
rec_defn : fun_defn list;
rec_letrec : int;
}
and fun_defn = {
fun_ps : psymbol;
fun_lambda : lambda;
fun_varm : varmap;
}
and lambda = {
......@@ -534,17 +534,16 @@ let ps_pvset pvs ps = varmap_pvset pvs ps.ps_varm
let e_pvset pvs e = varmap_pvset pvs e.e_varm
let spec_of_lambda lam letrec = {
let spec_of_lambda lam = {
c_pre = lam.l_pre;
c_effect = lam.l_expr.e_effect;
c_post = lam.l_post;
c_xpost = lam.l_xpost;
c_variant = lam.l_variant;
c_letrec = letrec; }
c_variant = lam.l_variant; }
let l_pvset pvs lam =
let pvs = e_pvset pvs lam.l_expr in
let pvs = spec_pvset pvs (spec_of_lambda lam 0) in
let pvs = spec_pvset pvs (spec_of_lambda lam) in
List.fold_right Spv.remove lam.l_args pvs
let spec_of_abstract e q xq = {
......@@ -552,8 +551,7 @@ let spec_of_abstract e q xq = {
c_post = q;
c_xpost = xq;
c_effect = e.e_effect;
c_variant = [];
c_letrec = 0; }
c_variant = []; }
let abstr_pvset pvs e q xq =
let pvs = e_pvset pvs e in
......@@ -988,24 +986,25 @@ let e_absurd ity =
(* simple functional definitions *)
let create_fun_defn id lam letrec recsyms =
let spec = spec_of_lambda lam letrec in
let create_fun_defn id lam recsyms =
let spec = spec_of_lambda lam in
let varm = spec_varmap lam.l_expr.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 varm_ps = Mid.set_diff varm recsyms in
let vty = match lam.l_expr.e_vty with
| VTvalue ({ vtv_mut = Some _ } as vtv) -> VTvalue (vtv_unmut vtv)
| vty -> vty in
let vta = vty_arrow lam.l_args ~spec vty in
{ fun_ps = create_psymbol_poly id vta varm;
fun_lambda = lam; }
{ fun_ps = create_psymbol_poly id vta varm_ps;
fun_lambda = lam;
fun_varm = varm; }
let e_rec rdl e =
let add_rd m { fun_ps = ps } =
(* psymbols defined in rdl can't occur in ps.ps_varm *)
varmap_union (Mid.remove ps.ps_name m) ps.ps_varm in
let add_rd m rd = varmap_union rd.fun_varm m in
let del_rd m rd = Mid.remove rd.fun_ps.ps_name m in
let varm = List.fold_left add_rd e.e_varm rdl.rec_defn in
let varm = List.fold_left del_rd varm rdl.rec_defn in
mk_expr (Erec (rdl,e)) e.e_vty e.e_effect varm
(* compute the fixpoint on recursive definitions *)
......@@ -1038,10 +1037,7 @@ let ps_compat ps1 ps2 =
vta_compat ps1.ps_vta ps2.ps_vta &&
Mid.equal (fun _ _ -> true) ps1.ps_varm ps2.ps_varm
let rec expr_subst psm e =
let e' = expr_subst_node psm e in
{ e' with e_loc = e.e_loc; e_label = e.e_label }
and expr_subst_node psm e = match e.e_node with
let rec expr_subst psm e = e_label_copy e (match e.e_node with
| Earrow ps when Mid.mem ps.ps_name psm ->
e_arrow (Mid.find ps.ps_name psm) (vta_of_expr e)
| Eapp (e,pv,_) ->
......@@ -1055,10 +1051,10 @@ and expr_subst_node 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 ({ rec_defn = rdl; rec_letrec = letrec }, e) ->
| Erec ({ rec_defn = rdl }, e) ->
let conv lam = { lam with l_expr = expr_subst psm lam.l_expr } in
let defl = List.map (fun rd -> rd.fun_ps, conv rd.fun_lambda) rdl in
let rdl = create_rec_defn letrec defl in
let rdl = create_rec_defn 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) ->
......@@ -1081,24 +1077,23 @@ and expr_subst_node psm e = match e.e_node with
e_loop inv var (expr_subst psm e)
| Efor (pv,bounds,inv,e) ->
e_for_real pv bounds inv (expr_subst psm e)
| Elogic _ | Evalue _ | Earrow _ | Eany _ | Eabsurd | Eassert _ -> e
| Elogic _ | Evalue _ | Earrow _ | Eany _ | Eabsurd | Eassert _ -> e)
and create_rec_defn letrec defl =
and create_rec_defn 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 letrec recsyms in
let rd = create_fun_defn (id_clone ps.ps_name) lam 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 { rec_defn = rdl; rec_letrec = letrec }
else subst_rd letrec m rdl
if Mid.is_empty m then { rec_defn = rdl } else subst_rd m rdl
and subst_rd letrec psm rdl =
and subst_rd 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 letrec (List.map subst rdl)
create_rec_defn (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
......@@ -1109,8 +1104,7 @@ and subst_rd letrec 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 = let letrec = ref 0 in fun defl ->
incr letrec;
let create_rec_defn defl =
if defl = [] then invalid_arg "Mlw_expr.create_rec_defn";
(* check that the all variants use the same order *)
let variant1 = (snd (List.hd defl)).l_variant in
......@@ -1130,16 +1124,15 @@ let create_rec_defn = let letrec = ref 0 in fun defl ->
| 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 !letrec recsyms in
let rd = create_fun_defn (id_clone ps.ps_name) lam 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 !letrec m rdl
subst_rd m rdl
let create_fun_defn id lam =
if lam.l_variant <> [] then
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 }
{ rec_defn = [create_fun_defn id lam Sid.empty] }
(* fold *)
......
......@@ -171,14 +171,14 @@ and let_defn = private {
let_expr : expr;
}
and rec_defn = private {
and rec_defn = {
rec_defn : fun_defn list;
rec_letrec : int;
}
and fun_defn = private {
fun_ps : psymbol;
fun_lambda : lambda;
fun_varm : varmap;
}
and lambda = {
......
......@@ -318,7 +318,7 @@ let pdecl_vc env km th d = match d.pd_node with
| PDtype _ | PDdata _ | PDexn _ -> th
| PDval lv -> wp_val env km th lv
| PDlet ld -> wp_let env km th ld
| PDrec rdl ->wp_rec env km th rdl
| PDrec rd -> wp_rec env km th rd
let add_pdecl ~wp uc d =
let uc = { uc with
......@@ -456,8 +456,7 @@ let clone_export uc m inst =
c_post = conv_term mv c.c_post;
c_xpost = Mexn.fold (addx mv) c.c_xpost Mexn.empty;
c_effect = conv_eff c.c_effect;
c_variant = [];
c_letrec = 0; } in
c_variant = []; } in
let rec conv_vta mv a =
let args = List.map conv_pv a.vta_args in
let add mv pv npv = Mvs.add pv.pv_vs npv.pv_vs mv in
......
......@@ -687,6 +687,10 @@ and print_vty info fmt = function
| VTvalue vtv -> print_vtv info fmt vtv
| VTarrow vta -> print_vta info fmt vta
let is_letrec = function
| [fd] -> Mid.mem fd.fun_ps.ps_name fd.fun_varm
| _ -> true
let ity_mark = ity_pur Mlw_wp.ts_mark []
let rec print_expr info fmt e = print_lexpr 0 info fmt e
......@@ -759,24 +763,24 @@ and print_lexpr pri info fmt e =
| Ecase (e1, bl) ->
fprintf fmt "@[(match @[%a@] with@\n@[<hov>%a@])@]"
(print_expr info) e1 (print_list newline (print_ebranch info)) bl
| Erec ({ rec_defn = rdl; rec_letrec = lr }, e) ->
| Erec ({ rec_defn = rdl }, e) ->
(* print non-ghost first *)
let cmp {fun_ps=ps1} {fun_ps=ps2} =
Pervasives.compare ps1.ps_vta.vta_ghost ps2.ps_vta.vta_ghost in
let rdl = List.sort cmp rdl in
fprintf fmt "@[<v>%a@\nin@\n%a@]"
(print_list_next newline (print_rec_decl lr info)) rdl
(print_list_next newline (print_rec_decl (is_letrec rdl) info)) rdl
(print_expr info) e
and print_rec lr info fst fmt { fun_ps = ps ; fun_lambda = lam } =
if ps.ps_vta.vta_ghost then
fprintf fmt "(* %s %a *)"
(if fst then if lr > 0 then "let rec" else "let" else "with")
(if fst then if lr then "let rec" else "let" else "with")
(print_ps info) ps
else
let print_arg fmt pv = fprintf fmt "@[%a@]" (print_pvty info) pv in
fprintf fmt "@[<hov 2>%s %a %a =@ %a@]"
(if fst then if lr > 0 then "let rec" else "let" else "and")
(if fst then if lr then "let rec" else "let" else "and")
(print_ps info) ps (print_list space print_arg) lam.l_args
(print_expr info) lam.l_expr
......@@ -968,14 +972,14 @@ let pdecl info fmt pd = match pd.pd_node with
fprintf fmt "@\n@\n"
| PDlet ld ->
print_let_decl info fmt ld
| PDrec { rec_defn = rdl; rec_letrec = lr } ->
| PDrec { rec_defn = rdl } ->
(* print defined, non-ghost first *)
let cmp {fun_ps=ps1} {fun_ps=ps2} =
Pervasives.compare
(ps1.ps_vta.vta_ghost || has_syntax info ps1.ps_name)
(ps2.ps_vta.vta_ghost || has_syntax info ps2.ps_name) in
let rdl = List.sort cmp rdl in
print_list_next newline (print_rec_decl lr info) fmt rdl;
print_list_next newline (print_rec_decl (is_letrec rdl) info) fmt rdl;
fprintf fmt "@\n@\n"
| PDexn xs ->
print_exn_decl info fmt xs
......
......@@ -220,6 +220,10 @@ let print_list_next sep print fmt = function
| x :: r -> print true fmt x; sep fmt ();
print_list sep (print false) fmt r
let is_letrec = function
| [fd] -> Mid.mem fd.fun_ps.ps_name fd.fun_varm
| _ -> true
let rec print_expr fmt e = print_lexpr 0 fmt e
and print_lexpr pri fmt e =
......@@ -277,11 +281,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 ({ rec_defn = rdl; rec_letrec = lr }, e) ->
| Erec ({ rec_defn = fdl }, e) ->
fprintf fmt (protect_on (pri > 0) "%a@ in@\n%a")
(print_list_next newline (print_rec lr)) rdl print_expr e;
let forget_rd rd = forget_ps rd.fun_ps in
List.iter forget_rd rdl
(print_list_next newline (print_rec (is_letrec fdl))) fdl print_expr e;
List.iter (fun fd -> forget_ps fd.fun_ps) fdl
| Eif (e0,e1,e2) ->
fprintf fmt (protect_on (pri > 0) "if %a then %a@ else %a")
print_expr e0 print_expr e1 print_expr e2
......@@ -327,7 +330,7 @@ and print_xbranch fmt (xs, pv, e) =
and print_rec lr 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 if lr > 0 then "let rec" else "let" else "with")
(if fst then if lr then "let rec" else "let" else "with")
print_psty ps
(print_list space print_arg) lam.l_args
print_term lam.l_pre
......@@ -422,8 +425,8 @@ 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 { rec_defn = rdl; rec_letrec = lr } ->
print_list_next newline (print_rec_decl lr) fmt rdl
| PDrec { rec_defn = fdl } ->
print_list_next newline (print_rec_decl (is_letrec fdl)) fmt fdl
| PDexn xs -> print_exn_decl fmt xs
(* Print exceptions *)
......
......@@ -734,7 +734,6 @@ type spec = {
c_xpost : xpost;
c_effect : effect;
c_variant : variant list;
c_letrec : int;
}
let spec_empty ty = {
......@@ -743,7 +742,6 @@ let spec_empty ty = {
c_xpost = Mexn.empty;
c_effect = eff_empty;
c_variant = [];
c_letrec = 0;
}
let spec_full_inst sbs tvm vsm c =
......@@ -753,7 +751,6 @@ let spec_full_inst sbs tvm vsm c =
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 =
......@@ -763,7 +760,6 @@ let spec_subst sbs c =
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 =
......@@ -858,6 +854,7 @@ and vty_arrow = {
vta_result : vty;
vta_spec : spec;
vta_ghost : bool;
vta_family : int;
}
let rec vta_vars vta =
......@@ -882,14 +879,15 @@ let ty_of_vty = function
let spec_check spec vty = spec_check spec (ty_of_vty vty)
let vty_arrow_unsafe argl ~spec ~ghost vty = {
let vty_arrow_unsafe argl spec ghost family vty = {
vta_args = argl;
vta_result = vty;
vta_spec = spec;
vta_ghost = ghost || vty_ghost vty;
vta_family = family;
}
let vty_arrow argl ?spec ?(ghost=false) vty =
let vty_arrow = let c = ref 0 in fun argl ?spec ?(ghost=false) vty ->
let exn = Invalid_argument "Mlw.vty_arrow" in
(* the arguments must be all distinct *)
if argl = [] then raise exn;
......@@ -906,7 +904,10 @@ let vty_arrow argl ?spec ?(ghost=false) vty =
let spec = match spec with
| Some spec -> spec_check spec vty; spec
| None -> spec_empty (ty_of_vty vty) in
vty_arrow_unsafe argl ~spec ~ghost vty
(* we admit non-empty variant list even for null letrec,
so that we can store there external variables from
user-written effects to save them from spec_filter *)
vty_arrow_unsafe argl spec ghost (incr c; !c) vty
(* this only compares the types of arguments and results, and ignores
the spec. In other words, only the type variables and regions
......@@ -944,7 +945,7 @@ let vta_full_inst sbs vta =
let vty = match vta.vta_result with
| VTarrow vta -> VTarrow (vta_inst vsm vta)
| VTvalue vtv -> VTvalue (vtv_inst vtv) in
vty_arrow_unsafe args ~ghost:vta.vta_ghost ~spec vty
vty_arrow_unsafe args spec vta.vta_ghost vta.vta_family vty
in
vta_inst Mvs.empty vta
......@@ -975,7 +976,7 @@ let rec vta_filter varm vars vta =
let eff = reg_fold on_reg v.vtv_ity.ity_vars spec.c_effect in
{ spec with c_effect = eff }
| VTarrow _ -> spec in
vty_arrow_unsafe vta.vta_args ~ghost:vta.vta_ghost ~spec vty
vty_arrow_unsafe vta.vta_args spec vta.vta_ghost vta.vta_family vty
let vta_filter varm vta =
vta_filter varm (vars_merge varm vars_empty) vta
......@@ -997,12 +998,17 @@ let vta_app vta pv =
| VTarrow a when not (List.exists (pv_equal arg) a.vta_args) ->
let result = vty_subst a.vta_result in
let spec = spec_subst sbs a.vta_spec in
VTarrow (vty_arrow_unsafe a.vta_args ~ghost:a.vta_ghost ~spec result)
VTarrow (vty_arrow_unsafe a.vta_args spec
a.vta_ghost a.vta_family result)
| vty -> vty in
let result = vty_subst vta.vta_result in
let spec = spec_subst sbs vta.vta_spec in
if not vtv.vtv_ghost && arg.pv_vtv.vtv_ghost then
Loc.errorm "non-ghost value passed as a ghost argument";
let ghost = vta.vta_ghost || (vtv.vtv_ghost && not arg.pv_vtv.vtv_ghost) in
if rest = [] then spec, (if ghost then vty_ghostify result else result)
else spec_empty ty_unit, VTarrow (vty_arrow_unsafe rest ~ghost ~spec result)
let ghost =
vta.vta_ghost || (vtv.vtv_ghost && not arg.pv_vtv.vtv_ghost) in
if rest = [] then
spec, (if ghost then vty_ghostify result else result)
else
spec_empty ty_unit,
VTarrow (vty_arrow_unsafe rest spec ghost vta.vta_family result)
......@@ -256,7 +256,6 @@ type spec = {
c_xpost : xpost;
c_effect : effect;
c_variant : variant list;
c_letrec : int;
}
(** program variables *)
......@@ -303,6 +302,7 @@ and vty_arrow = private {
vta_result : vty;
vta_spec : spec;
vta_ghost : bool;
vta_family : int;
}
exception UnboundException of xsymbol
......
......@@ -907,8 +907,7 @@ let rec type_c lenv gh pvs vars dtyc =
c_effect = eff;
c_post = create_post lenv "result" vty dtyc.dc_post;
c_xpost = complete_xpost lenv eff dtyc.dc_xpost;
c_variant = [];
c_letrec = 0 } in
c_variant = []; } in
(* we add an exception postcondition for %Exit that mentions
every external variable in effect expressions which also
does not occur in pre/post/xpost. In this way, we keep
......
......@@ -712,8 +712,11 @@ and wp_desc env e q xq = match e.e_node with
| Eapp (e1,_,spec) ->
let p = wp_label e (wp_expl expl_pre spec.c_pre) in
let p = t_label ?loc:e.e_loc p.t_label p in
let d = if spec.c_letrec = 0 then t_true else
let olds = Mint.find_def [] spec.c_letrec env.letrec_var in
let d =
if spec.c_variant = [] then t_true else
let olds = match e1.e_vty with
| VTarrow a -> Mint.find_def [] a.vta_family env.letrec_var
| _ -> assert false in
if olds = [] then t_true (* we are out of letrec *) else
let d = decrease ?loc:e.e_loc env olds spec.c_variant in
wp_expl expl_variant (t_label ?loc:e.e_loc d.t_label d) in
......@@ -815,17 +818,19 @@ and wp_abstract env c_eff c_q c_xq q xq =
in
backstep proceed c_q c_xq
and wp_fun_defn env lr { fun_ps = ps ; fun_lambda = l } =
and wp_fun_defn env faml { fun_ps = ps ; fun_lambda = l } =
let lab = fresh_mark () in
let add_arg sbs pv = ity_match sbs pv.pv_vtv.vtv_ity pv.pv_vtv.vtv_ity in
let subst = List.fold_left add_arg ps.ps_subst l.l_args in
let regs = Mreg.map (fun _ -> ()) subst.ity_subst_reg in
let args = List.map (fun pv -> pv.pv_vs) l.l_args in
let env = if lr = 0 || l.l_variant = [] then env else
let env = if l.l_variant = [] then env else
let lab = t_var lab in
let t_at_lab (t,_) = t_app fs_at [t; lab] t.t_ty in
let tl = List.map t_at_lab l.l_variant in
{ env with letrec_var = Mint.add lr tl env.letrec_var }
let add_family lrv fam = Mint.add fam tl lrv in
let lrv = List.fold_left add_family env.letrec_var faml in
{ env with letrec_var = lrv }
in
let q = old_mark lab (wp_expl expl_post l.l_post) in
let conv p = old_mark lab (wp_expl expl_xpost p) in
......@@ -833,8 +838,9 @@ and wp_fun_defn env lr { fun_ps = ps ; fun_lambda = l } =
let f = wp_implies l.l_pre (erase_mark lab f) in
wp_forall args (quantify env regs f)
and wp_rec_defn env { rec_defn = rdl; rec_letrec = lr } =
List.map (wp_fun_defn env lr) rdl
and wp_rec_defn env { rec_defn = fdl } =
let faml = List.map (fun fd -> fd.fun_ps.ps_vta.vta_family) fdl in
List.map (wp_fun_defn env faml) fdl
(***
let bool_to_prop env f =
......@@ -1075,7 +1081,7 @@ and fast_wp_desc env s r e =
| Evalue _ -> assert false (*TODO*)
| Eabsurd -> assert false (*TODO*)
and fast_wp_fun_defn env lr { fun_ps = ps ; fun_lambda = l } =
and fast_wp_fun_defn env faml { fun_ps = ps ; fun_lambda = l } =
(* OK: forall bl. pl => ok(e)
NE: true *)
let lab = fresh_mark () in
......@@ -1083,11 +1089,13 @@ and fast_wp_fun_defn env lr { fun_ps = ps ; fun_lambda = l } =
let subst = List.fold_left add_arg ps.ps_subst l.l_args in
let regs = Mreg.map (fun _ -> ()) subst.ity_subst_reg in
let args = List.map (fun pv -> pv.pv_vs) l.l_args in
let env = if lr = 0 || l.l_variant = [] then env else
let env = if l.l_variant = [] then env else
let lab = t_var lab in
let t_at_lab (t,_) = t_app fs_at [t; lab] t.t_ty in
let tl = List.map t_at_lab l.l_variant in
{ env with letrec_var = Mint.add lr tl env.letrec_var }
let add_family lrv fam = Mint.add fam tl lrv in
let lrv = List.fold_left add_family env.letrec_var faml in
{ env with letrec_var = lrv }
in
let q = old_mark lab (wp_expl expl_post l.l_post) in
let result, _ as q = open_post q in
......@@ -1100,8 +1108,9 @@ and fast_wp_fun_defn env lr { fun_ps = ps ; fun_lambda = l } =
let f = wp_implies l.l_pre (erase_mark lab f) in
wp_forall args (quantify env regs f)
and fast_wp_rec_defn env { rec_defn = rdl; rec_letrec = lr } =
List.map (fast_wp_fun_defn env lr) rdl
and fast_wp_rec_defn env { rec_defn = fdl } =
let faml = List.map (fun fd -> fd.fun_ps.ps_vta.vta_family) fdl in
List.map (fast_wp_fun_defn env faml) fdl
let fast_wp_let env km th { let_sym = lv; let_expr = e } =
let env = mk_env env km th in
......
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