whyml: let rec typing

src/whyml/mlw_dtree.ml

@@ -51,22 +51,22 @@ type dpost_fmla = Ptree.lexpr
 type dexn_post_fmla = Ptree.lexpr
 type dpost = dpost_fmla * (Term.lsymbol * dexn_post_fmla) list
 
-type dueffect = {
-  du_reads  : Ptree.lexpr list;
-  du_writes : Ptree.lexpr list;
-  du_raises : xsymbol list;
+type deffect = {
+  deff_reads  : Ptree.lexpr list;
+  deff_writes : Ptree.lexpr list;
+  deff_raises : xsymbol list;
 }
 
-type dubinder = ident * ghost * dity
+type dbinder = ident * ghost * dity
 
 (**
 type dutype_v =
   | DUTpure  of Denv.dty
-  | DUTarrow of dubinder list * dutype_c
+  | DUTarrow of dbinder list * dutype_c
 
 and dutype_c =
   { duc_result_type : dutype_v;
-    duc_effect      : dueffect;
+    duc_effect      : deffect;
     duc_pre         : Ptree.lexpr;
     duc_post        : Ptree.lexpr * (Term.lsymbol * Ptree.lexpr) list; }
 **)
@@ -75,7 +75,7 @@ type dvariant = Ptree.lexpr * Term.lsymbol option
 
 type dloop_annotation = {
   dloop_invariant : Ptree.lexpr option;
-  dloop_variant   : dvariant option;
+  dloop_variant   : dvariant list;
 }
 
 type dexpr = {
@@ -93,7 +93,7 @@ and dexpr_desc =
   | DEglobal_pl of plsymbol
   | DEglobal_ls of Term.lsymbol
   | DEapply of dexpr * dexpr list
-  | DEfun of dubinder list * dtriple
+  | DEfun of dbinder list * dtriple
   | DElet of ident * dexpr * dexpr
   | DEletrec of drecfun list * dexpr
   | DEassign of dexpr * dexpr
@@ -111,6 +111,6 @@ and dexpr_desc =
   | DEmark of string * dexpr
   (* | DEany of dutype_c *)
 
-and drecfun = (ident * Denv.dty) * dubinder list * dvariant option * dtriple
+and drecfun = ident * dity * dbinder list * dvariant list * dtriple
 
 and dtriple = dpre * dexpr * dpost

src/whyml/mlw_dty.ml

@@ -208,6 +208,8 @@ let ts_arrow =
   Ty.create_tysymbol (Ident.id_fresh "arrow") v None
 
 let rec vty_of_dity = function
+  | Dvar { contents = Dval d } ->
+      vty_of_dity d
   | Dts (ts, [d1; d2]) when ts_equal ts ts_arrow ->
       VTarrow (vty_arrow (vty_value (ity_of_dity d1)) (vty_of_dity d2))
   | dity ->

src/whyml/mlw_typing.ml

@@ -327,16 +327,12 @@ and dexpr_desc ~userloc denv loc = function
       let denv = { denv with locals = locals; tvars = tvars } in
       let e2 = dexpr ~userloc denv e2 in
       DElet (id, e1, e2), e2.dexpr_type
+  | Ptree.Eletrec (rdl, e1) ->
+      let denv, dl = dletrec ~userloc denv rdl in
+      let e1 = dexpr ~userloc denv e1 in
+      DEletrec (dl, e1), e1.dexpr_type
   | Ptree.Efun (bl, tr) ->
-      let dbinder denv (id, pty) =
-        let dity = match pty with
-          | Some pty -> dity_of_pty ~user:false denv pty
-          | None -> create_type_variable () in
-        add_var id dity denv, (id, false, dity) in
-      let denv, bl = Util.map_fold_left dbinder denv bl in
-      let _,e,_ as tr = dtriple ~userloc denv tr in
-      let dity =
-        make_arrow_type (List.map (fun (_,_,d) -> d) bl) e.dexpr_type in
+      let bl, _, tr, dity = dlambda ~userloc denv bl None tr in
       DEfun (bl, tr), dity
   | Ptree.Ecast (e1, pty) ->
       let e1 = dexpr ~userloc denv e1 in
@@ -431,8 +427,6 @@ and dexpr_desc ~userloc denv loc = function
         expected_type e res;
         ppat, e in
       DEmatch (e1, List.map branch bl), res
-  | Ptree.Eletrec (_rdl, _e1) ->
-      assert false (*TODO*)
   | Ptree.Eloop (_ann, _e1) ->
       assert false (*TODO*)
   | Ptree.Eabsurd ->
@@ -452,10 +446,31 @@ and dexpr_desc ~userloc denv loc = function
   | Ptree.Eabstract (_e1, _post) ->
       assert false (*TODO*)
 
-and dtriple ~userloc denv (p, e, q) =
+and dletrec ~userloc denv rdl =
+  (* add all functions into environment *)
+  let add_one denv (id, bl, var, tr) =
+    let res = create_type_variable () in
+    let locals = Mstr.add id.id (denv.tvars, res) denv.locals in
+    { denv with locals = locals }, (id, res, bl, var, tr) in
+  let denv, rdl = Util.map_fold_left add_one denv rdl in
+  (* then type-check all of them and unify *)
+  let type_one (id, res, bl, var, tr) =
+    let bl, var, tr, dity = dlambda ~userloc denv bl var tr in
+    Loc.try2 id.id_loc unify dity res;
+    id, dity, bl, var, tr in
+  denv, List.map type_one rdl
+
+and dlambda ~userloc denv bl _var (p, e, q) =
+  let dbinder denv (id, pty) =
+    let dity = match pty with
+      | Some pty -> dity_of_pty ~user:false denv pty
+      | None -> create_type_variable () in
+    add_var id dity denv, (id, false, dity) in
+  let denv, bl = Util.map_fold_left dbinder denv bl in
+  let tyl = List.map (fun (_,_,d) -> d) bl in
   let e = dexpr ~userloc denv e in
   let q = dpost denv q in
-  p, e, q
+  bl, [], (p, e, q), make_arrow_type tyl e.dexpr_type
 
 and dpost _denv (q, _ql) =
   q, [] (* TODO *)
@@ -483,6 +498,11 @@ let rec expr locals de = match de.dexpr_desc with
       let locals = Mstr.add x.id def1.let_var locals in
       let e2 = expr locals de2 in
       e_let def1 e2
+  | DEletrec (rdl, de1) ->
+      let rdl = expr_rec locals rdl in
+      let add_rd { rec_ps = ps } = Mstr.add ps.ps_name.id_string (LetA ps) in
+      let e1 = expr (List.fold_right add_rd rdl locals) de1 in
+      e_rec rdl e1
   | DEapply (de1, del) ->
       let el = List.map (expr locals) del in
       begin match de1.dexpr_desc with
@@ -523,27 +543,41 @@ let rec expr locals de = match de.dexpr_desc with
   | _ ->
       assert false (*TODO*)
 
-and expr_fun locals x bl (_, e1, _) =
+and expr_rec locals rdl =
+  let step1 locals (id, dity, bl, var, tr) =
+    let vta = match vty_of_dity dity with
+      | VTarrow vta -> vta
+      | VTvalue _ -> assert false in
+    let ps = create_psymbol (id_user id) vta vars_empty in
+    Mstr.add id.id (LetA ps) locals, (ps, bl, var, tr)
+  in
+  let locals, rdl = Util.map_fold_left step1 locals rdl in
+  let step2 (ps, bl, var, tr) = ps, expr_lam locals bl var tr in
+  create_rec_defn (List.map step2 rdl)
+
+and expr_fun locals x bl tr =
+  let lam = expr_lam locals bl [] tr in
+  create_fun_defn (id_user x) lam
+
+and expr_lam locals bl _var (_, e, _) =
   let binder (id, ghost, dity) =
     let vtv = vty_value ~ghost (ity_of_dity dity) in
     create_pvsymbol (id_user id) vtv in
   let pvl = List.map binder bl in
   let add_binder pv = Mstr.add pv.pv_vs.vs_name.id_string (LetV pv) in
-  let locals' = List.fold_right add_binder pvl locals in
-  let e1 = expr locals' e1 in
-  let ty1 = match e1.e_vty with
+  let locals = List.fold_right add_binder pvl locals in
+  let e = expr locals e in
+  let ty = match e.e_vty with
     | VTarrow _ -> ty_tuple []
     | VTvalue vtv -> ty_of_ity vtv.vtv_ity in
-  let res1 = create_vsymbol (id_fresh "result") ty1 in
-  let lam = {
-    l_args = pvl;
-    l_variant = [];
+  let res = create_vsymbol (id_fresh "result") ty in
+  { l_args = pvl;
+    l_variant = [];                   (* TODO *)
     l_pre = t_true;                   (* TODO *)
-    l_expr = e1;
-    l_post = create_post res1 t_true; (* TODO *)
+    l_expr = e;
+    l_post = create_post res t_true;  (* TODO *)
     l_xpost = Mexn.empty;             (* TODO *)
-  } in
-  create_fun_defn (id_user x) lam
+  }
 
 (** Type declaration *)
 
@@ -1017,7 +1051,12 @@ let add_module lib path mm mt m =
               create_let_decl def
         in
         Loc.try2 loc add_pdecl_with_tuples uc pd
-    | Dletrec _ | Dparam _ | Dexn _ ->
+    | Dletrec rdl ->
+        let _, rdl = dletrec ~userloc:None (create_denv uc) rdl in
+        let rdl = expr_rec Mstr.empty rdl in
+        let pd = create_rec_decl rdl in
+        Loc.try2 loc add_pdecl_with_tuples uc pd
+    | Dparam _ | Dexn _ ->
         assert false (* TODO *)
     | Duse _ ->
         assert false (*TO BE REMOVED EVENTUALLY *)

tests/test-pgm-jcf.mlx

@@ -21,13 +21,20 @@ module N
   type tree 'a = Node 'a (forest 'a) | Leaf
   with forest 'a = Cons (tree 'a) (forest 'a) | Nil
 
-  type ref 'b = {| ghost mutable contents : 'b |}
+  type ref 'b = {| (* ghost *) mutable contents : 'b |}
 
   type myrec 'a = {| f1 : int ; ghost f2 : tree 'a |}
 
-  let bang y = y.contents
-
-  let h () = bang
+  let myfun r =
+    let rec on_tree t = match t with
+      | Node {| contents = v |} f -> v + on_forest f
+      | Leaf -> 0
+    end with on_forest f = match f with
+      | Cons t f -> on_tree t + on_forest f
+      | Nil -> 1
+    end
+    in
+    on_tree r
 end
 
 (*