whyml: back to spec.c_letrec (better this time)

src/whyml/mlw_decl.ml

@@ -34,7 +34,7 @@ type data_decl = itysymbol * constructor list * post
 
 type pdecl = {
   pd_node : pdecl_node;
-(*   pd_syms : Sid.t;         (* idents used in declaration *) *)
+  pd_syms : Sid.t;         (* idents used in declaration *)
   pd_news : Sid.t;         (* idents introduced in declaration *)
   pd_tag  : int;           (* unique tag *)
 }
@@ -51,9 +51,9 @@ let pd_equal : pdecl -> pdecl -> bool = (==)
 
 let mk_decl =
   let r = ref 0 in
-  fun node (*syms*) news ->
+  fun node syms news ->
     incr r;
-    { pd_node = node; (*pd_syms = syms;*) pd_news = news; pd_tag = !r; }
+    { pd_node = node; pd_syms = syms; pd_news = news; pd_tag = !r; }
 
 let news_id s id = Sid.add_new (Decl.ClashIdent id) id s
 
@@ -116,7 +116,7 @@ let syms_expr s _e = s (* TODO *)
 let create_ty_decl its =
 (*   let syms = Util.option_fold syms_ity Sid.empty its.its_def in *)
   let news = Sid.singleton its.its_pure.ts_name in
-  mk_decl (PDtype its) (*syms*) news
+  mk_decl (PDtype its) Sid.empty news
 
 type pre_constructor = preid * (pvsymbol * bool) list
 
@@ -173,7 +173,7 @@ let create_data_decl tdl =
     its, List.map (build_constructor its) cl, null_invariant its
   in
   let tdl = List.map build_type tdl in
-  mk_decl (PDdata tdl) (*!syms*) !news
+  mk_decl (PDdata tdl) Sid.empty !news
 
 let add_invariant pd its p =
   if not its.its_inv then invalid_arg "Mlw_decl.add_invariant";
@@ -191,7 +191,7 @@ let add_invariant pd its p =
     | [] -> raise Not_found
   in
   match pd.pd_node with
-    | PDdata tdl -> mk_decl (PDdata (add tdl)) (*pd.pd_syms*) pd.pd_news
+    | PDdata tdl -> mk_decl (PDdata (add tdl)) pd.pd_syms pd.pd_news
     | _ -> invalid_arg "Mlw_decl.add_invariant"
 
 let check_vars vars =
@@ -215,18 +215,20 @@ let create_let_decl ld =
   let news = match ld.let_sym with
     | LetA ps -> new_regs vars news ps.ps_vars
     | LetV pv -> new_regs vars news pv.pv_vars in
+  let syms = Mid.map (fun _ -> ()) ld.let_expr.e_varm in
 (*
   let syms = syms_varmap Sid.empty ld.let_expr.e_vars in
   let syms = syms_effect syms ld.let_expr.e_effect in
   let syms = syms_vty syms ld.let_expr.e_vty in
   let syms = syms_expr syms ld.let_expr in
 *)
-  mk_decl (PDlet ld) (*syms*) news
+  mk_decl (PDlet ld) syms news
 
 let create_rec_decl fdl =
   let add_fd s { fun_ps = p } =
     check_vars p.ps_vars; news_id s p.ps_name in
   let news = List.fold_left add_fd Sid.empty fdl in
+  let syms = Mid.map (fun _ -> ()) (rec_varmap Mid.empty fdl) in
 (*
   let add_fd syms { rec_ps = ps; rec_lambda = l; rec_vars = vm } =
     let syms = syms_varmap syms vm in
@@ -240,27 +242,27 @@ let create_rec_decl fdl =
     syms_expr syms l.l_expr in
   let syms = List.fold_left add_fd Sid.empty fdl in
 *)
-  mk_decl (PDrec fdl) (*syms*) news
+  mk_decl (PDrec fdl) syms news
 
 let create_val_decl lv =
   let news = letvar_news lv in
-  let news = match lv with
+  let news, syms = match lv with
     | LetV { pv_vtv = { vtv_mut = Some _ }} ->
         Loc.errorm "abstract parameters cannot be mutable"
-    | LetV pv -> new_regs vars_empty news pv.pv_vars
-    | LetA _ -> news in
+    | LetV pv -> new_regs vars_empty news pv.pv_vars, Sid.empty
+    | LetA ps -> news, Mid.map (fun _ -> ()) ps.ps_varm in
 (*
   let syms = syms_type_v Sid.empty vd.val_spec in
   let syms = syms_varmap syms vd.val_vars in
 *)
-  mk_decl (PDval lv) (*syms*) news
+  mk_decl (PDval lv) syms news
 
 let create_exn_decl xs =
   let news = Sid.singleton xs.xs_name in
 (*
   let syms = syms_ity Sid.empty xs.xs_ity in
 *)
-  mk_decl (PDexn xs) (*syms*) news
+  mk_decl (PDexn xs) Sid.empty news
 
 (** {2 Cloning} *)
 
@@ -281,7 +283,7 @@ let clone_data_decl sm pd = match pd.pd_node with
         news := news_id !news its.its_pure.ts_name;
         its, List.map add_cs csl, inv in
       let tdl = List.map add_td tdl in
-      mk_decl (PDdata tdl) (*!syms*) !news
+      mk_decl (PDdata tdl) Sid.empty !news
   | _ -> invalid_arg "Mlw_decl.clone_data_decl"
 
 (** {2 Known identifiers} *)
@@ -298,18 +300,6 @@ let merge_known kn1 kn2 =
   in
   Mid.union check_known kn1 kn2
 
-let pd_vars pd = match pd.pd_node with
-  | PDval (LetV _) -> Sid.empty
-  | PDval (LetA ps) -> Mid.map (fun _ -> ()) ps.ps_varm
-  | PDlet ld -> Mid.map (fun _ -> ()) ld.let_expr.e_varm
-  | PDrec fdl ->
-      let add_fd s fd = Mid.set_union s fd.fun_varm in
-      let del_fd s fd = Mid.remove fd.fun_ps.ps_name s in
-      let varm = List.fold_left add_fd Mid.empty fdl in
-      let varm = List.fold_left del_fd varm fdl in
-      Mid.map (fun _ -> ()) varm
-  | PDtype _ | PDdata _ | PDexn _ -> Sid.empty
-
 let known_add_decl lkn0 kn0 d =
   let kn = Mid.map (const d) d.pd_news in
   let check id decl0 _ =
@@ -317,7 +307,7 @@ let known_add_decl lkn0 kn0 d =
     then raise (KnownIdent id)
     else raise (RedeclaredIdent id) in
   let kn = Mid.union check kn0 kn in
-  let unk = Mid.set_diff (pd_vars d) kn in
+  let unk = Mid.set_diff d.pd_syms kn in
   let unk = Mid.set_diff unk lkn0 in
   if Sid.is_empty unk then kn
   else raise (UnknownIdent (Sid.choose unk))

src/whyml/mlw_decl.mli

@@ -36,6 +36,7 @@ type data_decl = itysymbol * constructor list * post
 
 type pdecl = private {
   pd_node : pdecl_node;
+  pd_syms : Sid.t;         (* idents used in declaration *)
   pd_news : Sid.t;         (* idents introduced in declaration *)
   pd_tag  : int;           (* unique tag *)
 }

src/whyml/mlw_expr.ml

@@ -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 <> [] then
+  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;
   match vta.vta_result with
@@ -939,16 +939,17 @@ let e_try e0 bl =
 let pv_dummy = create_pvsymbol (id_fresh "dummy") (vty_value ity_unit)
 
 let e_any spec vty =
+  if spec.c_variant <> [] || spec.c_letrec <> 0 then
+    Loc.errorm "variants are not allowed in `any'";
   let vta = vty_arrow [pv_dummy] ~spec vty in
   let varm = vta_varmap vta in
   vta_check (vars_merge varm vars_empty) vta;
   mk_expr (Eany spec) vty spec.c_effect varm
 
 let e_abstract e spec =
-  if spec.c_variant <> [] then
+  if spec.c_variant <> [] || spec.c_letrec <> 0 then
     Loc.errorm "variants are not allowed in `abstract'";
-  let spec = { spec with c_effect = e.e_effect } in
-  spec_check spec e.e_vty;
+  spec_check { spec with c_effect = e.e_effect } e.e_vty;
   let varm = spec_varmap e.e_varm spec in
   mk_expr (Eabstr (e,spec)) e.e_vty e.e_effect varm
 
@@ -974,14 +975,24 @@ let create_fun_defn id lam recsyms =
     | vty -> vty in
   let vta = vty_arrow lam.l_args ~spec vty in
   { fun_ps     = create_psymbol_poly id vta varm_ps;
-    fun_lambda = { lam with l_spec = spec };
+    fun_lambda = lam;
     fun_varm   = varm; }
 
-let e_rec fdl e =
+let rec_varmap varm fdl =
+  let fd, rest = match fdl with
+    | [] -> invalid_arg "Mlw_expr.rec_varm"
+    | fd :: fdl -> fd, fdl in
+  let lr = fd.fun_ps.ps_vta.vta_spec.c_letrec in
+  let bad fd = fd.fun_ps.ps_vta.vta_spec.c_letrec <> lr in
+  if List.exists bad rest then invalid_arg "Mlw_expr.rec_varm";
   let add_fd m fd = varmap_union fd.fun_varm m in
   let del_fd m fd = Mid.remove fd.fun_ps.ps_name m in
-  let varm = List.fold_left add_fd e.e_varm fdl in
+  let varm = List.fold_left add_fd varm fdl in
   let varm = List.fold_left del_fd varm fdl in
+  varm
+
+let e_rec fdl e =
+  let varm = rec_varmap e.e_varm fdl in
   mk_expr (Erec (fdl,e)) e.e_vty e.e_effect varm
 
 (* compute the fixpoint on recursive definitions *)
@@ -1081,7 +1092,7 @@ and subst_fd psm fdl =
    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 1 in fun 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_spec.c_variant in
@@ -1101,13 +1112,16 @@ let create_rec_defn defl =
     | VTarrow _ -> Loc.errorm ?loc:lam.l_expr.e_loc
         "The body of a recursive function must be a first-order value"
     | VTvalue _ ->
+        let spec = { lam.l_spec with c_letrec = !letrec } in
+        let lam = { lam with l_spec = spec } in
         let fd = create_fun_defn (id_clone ps.ps_name) lam recsyms in
         Mid.add ps.ps_name fd.fun_ps m, fd in
   let m, fdl = Util.map_fold_left conv Mid.empty defl in
+  incr letrec;
   subst_fd m fdl
 
 let create_fun_defn id lam =
-  if lam.l_spec.c_variant <> [] then
+  if lam.l_spec.c_variant <> [] || lam.l_spec.c_letrec <> 0 then
     Loc.errorm "variants are not allowed in a non-recursive definition";
   create_fun_defn id lam Sid.empty
 

src/whyml/mlw_expr.mli

@@ -211,6 +211,8 @@ val create_let_defn : preid -> expr -> let_defn
 val create_fun_defn : preid -> lambda -> fun_defn
 val create_rec_defn : (psymbol * lambda) list -> fun_defn list
 
+val rec_varmap : varmap -> fun_defn list -> varmap
+
 exception StaleRegion of expr * ident
 (* freshness violation: a previously reset region is associated to an ident *)
 

src/whyml/mlw_module.ml

@@ -456,7 +456,8 @@ 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 = []; } in
+    c_variant = [];
+    c_letrec  = 0; } 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

src/whyml/mlw_ty.ml

@@ -734,6 +734,7 @@ type spec = {
   c_xpost   : xpost;
   c_effect  : effect;
   c_variant : variant list;
+  c_letrec  : int;
 }
 
 let spec_empty ty = {
@@ -742,6 +743,7 @@ 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 =
@@ -751,6 +753,7 @@ 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 =
@@ -760,6 +763,7 @@ 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 =
@@ -854,7 +858,6 @@ and vty_arrow = {
   vta_result : vty;
   vta_spec   : spec;
   vta_ghost  : bool;
-  vta_family : int;
 }
 
 let rec vta_vars vta =
@@ -879,15 +882,14 @@ let ty_of_vty = function
 
 let spec_check spec vty = spec_check spec (ty_of_vty vty)
 
-let vty_arrow_unsafe argl spec ghost family vty = {
+let vty_arrow_unsafe argl spec ghost vty = {
   vta_args   = argl;
   vta_result = vty;
   vta_spec   = spec;
   vta_ghost  = ghost || vty_ghost vty;
-  vta_family = family;
 }
 
-let vty_arrow = let c = ref 0 in fun argl ?spec ?(ghost=false) vty ->
+let vty_arrow argl ?spec ?(ghost=false) vty =
   let exn = Invalid_argument "Mlw.vty_arrow" in
   (* the arguments must be all distinct *)
   if argl = [] then raise exn;
@@ -907,7 +909,7 @@ let vty_arrow = let c = ref 0 in fun argl ?spec ?(ghost=false) 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
+  vty_arrow_unsafe argl spec ghost vty
 
 (* this only compares the types of arguments and results, and ignores
    the spec. In other words, only the type variables and regions
@@ -945,7 +947,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 spec vta.vta_ghost vta.vta_family vty
+    vty_arrow_unsafe args spec vta.vta_ghost vty
   in
   vta_inst Mvs.empty vta
 
@@ -976,7 +978,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 spec vta.vta_ghost vta.vta_family vty
+  vty_arrow_unsafe vta.vta_args spec vta.vta_ghost vty
 
 let vta_filter varm vta =
   vta_filter varm (vars_merge varm vars_empty) vta
@@ -998,8 +1000,7 @@ 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 spec
-          a.vta_ghost a.vta_family result)
+        VTarrow (vty_arrow_unsafe a.vta_args spec a.vta_ghost result)
     | vty -> vty in
   let result = vty_subst vta.vta_result in
   let spec = spec_subst sbs vta.vta_spec in
@@ -1007,8 +1008,5 @@ let vta_app vta pv =
     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 spec ghost vta.vta_family result)
+  if rest = [] then spec, (if ghost then vty_ghostify result else result)
+  else spec_empty ty_unit, VTarrow (vty_arrow_unsafe rest spec ghost result)

src/whyml/mlw_ty.mli

@@ -256,6 +256,7 @@ type spec = {
   c_xpost   : xpost;
   c_effect  : effect;
   c_variant : variant list;
+  c_letrec  : int;
 }
 
 (** program variables *)
@@ -302,7 +303,6 @@ and vty_arrow = private {
   vta_result : vty;
   vta_spec   : spec;
   vta_ghost  : bool;
-  vta_family : int;
 }
 
 exception UnboundException of xsymbol

src/whyml/mlw_typing.ml

@@ -891,7 +891,9 @@ let spec_of_dspec lenv eff vty dsp = {
   c_post    = create_post lenv "result" vty dsp.ds_post;
   c_xpost   = create_xpost lenv "result" dsp.ds_xpost;
   c_effect  = eff;
-  c_variant = List.map (create_variant lenv) dsp.ds_variant; }
+  c_variant = List.map (create_variant lenv) dsp.ds_variant;
+  c_letrec  = 0;
+}
 
 let rec type_c lenv gh pvs vars (dtyv, dsp) =
   let vty = type_v lenv gh pvs vars dtyv in

src/whyml/mlw_wp.ml

@@ -708,21 +708,19 @@ and wp_desc env e q xq = match e.e_node with
       let p = t_label ?loc:e.e_loc p.t_label p in
       (* TODO: propagate call labels into tyc.c_post *)
       let w = wp_abstract env spec.c_effect spec.c_post spec.c_xpost q xq in
-      wp_and ~sym:false p w (* FIXME? do we need pre? *)
+      wp_and ~sym:false p w
   | 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_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 spec.c_letrec = 0 || spec.c_variant = [] then t_true else
+        let olds = Mint.find_def [] spec.c_letrec env.letrec_var 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
       (* TODO: propagate call labels into tyc.c_post *)
       let w = wp_abstract env spec.c_effect spec.c_post spec.c_xpost q xq in
-      let w = wp_and ~sym:false (wp_and ~sym:true d p) w in (* FIXME? ~sym? *)
+      let w = wp_and ~sym:false (wp_and ~sym:true d p) w in
       let q = create_unit_post w in
       wp_expr env e1 q xq (* FIXME? should (wp_label e) rather be here? *)
   | Eabstr (e1, spec) ->
@@ -819,29 +817,26 @@ and wp_abstract env c_eff c_q c_xq q xq =
   in
   backstep proceed c_q c_xq
 
-and wp_fun_defn env faml { fun_ps = ps ; fun_lambda = l } =
+and wp_fun_defn env { fun_ps = ps ; fun_lambda = l } =
   let lab = fresh_mark () and c = l.l_spec 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 c.c_variant = [] then env else
+  let env =
+    if c.c_letrec = 0 || c.c_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 c.c_variant in
-    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 lrv = Mint.add c.c_letrec tl env.letrec_var in
+    { env with letrec_var = lrv } in
   let q = old_mark lab (wp_expl expl_post c.c_post) in
   let conv p = old_mark lab (wp_expl expl_xpost p) in
   let f = wp_expr env l.l_expr q (Mexn.map conv c.c_xpost) in
   let f = wp_implies c.c_pre (erase_mark lab f) in
   wp_forall args (quantify env regs f)
 
-and wp_rec_defn env fdl =
-  let faml = List.map (fun fd -> fd.fun_ps.ps_vta.vta_family) fdl in
-  List.map (wp_fun_defn env faml) fdl
+and wp_rec_defn env fdl = List.map (wp_fun_defn env) fdl
 
 (***
 let bool_to_prop env f =
@@ -1082,7 +1077,7 @@ and fast_wp_desc env s r e =
   | Evalue _ -> assert false (*TODO*)
   | Eabsurd -> assert false (*TODO*)
 
-and fast_wp_fun_defn env faml { fun_ps = ps ; fun_lambda = l } =
+and fast_wp_fun_defn env { fun_ps = ps ; fun_lambda = l } =
   (* OK: forall bl. pl => ok(e)
      NE: true *)
   let lab = fresh_mark () and c = l.l_spec in
@@ -1090,14 +1085,13 @@ and fast_wp_fun_defn env faml { 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 c.c_variant = [] then env else
+  let env =
+    if c.c_letrec = 0 || c.c_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 c.c_variant in
-    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 lrv = Mint.add c.c_letrec tl env.letrec_var in
+    { env with letrec_var = lrv } in
   let q = old_mark lab (wp_expl expl_post c.c_post) in
   let result, _ as q = open_post q in
   let conv p = old_mark lab (wp_expl expl_xpost p) in
@@ -1109,9 +1103,7 @@ and fast_wp_fun_defn env faml { fun_ps = ps ; fun_lambda = l } =
   let f = wp_implies c.c_pre (erase_mark lab f) in
   wp_forall args (quantify env regs f)
 
-and fast_wp_rec_defn env 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
+and fast_wp_rec_defn env fdl = List.map (fast_wp_fun_defn env) fdl
 
 let fast_wp_let env km th { let_sym = lv; let_expr = e } =
   let env = mk_env env km th in