whyml: type pattern matching

src/whyml/mlw_dtree.ml

@@ -102,7 +102,7 @@ and dexpr_desc =
   | DEloop of dloop_annotation * dexpr
   | DElazy of lazy_op * dexpr * dexpr
   | DEnot of dexpr
-  | DEmatch of dexpr * (Denv.dpattern * dexpr) list
+  | DEmatch of dexpr * (pre_ppattern * dexpr) list
   | DEabsurd
   | DEraise of xsymbol * dexpr option
   | DEtry of dexpr * (xsymbol * string option * dexpr) list

src/whyml/mlw_expr.ml

@@ -102,6 +102,10 @@ let ppat_var pv =
     ppat_vtv     = pv.pv_vtv;
     ppat_effect  = eff_empty; }
 
+let ppat_is_wild pp = match pp.ppat_pattern.pat_node with
+  | Pwild -> true
+  | _ -> false
+
 let ppat_plapp pls ppl vtv =
   if vtv.vtv_mut <> None then
     Loc.errorm "Only variable patterns can be mutable";
@@ -117,14 +121,17 @@ let ppat_plapp pls ppl vtv =
     let ghost = pp.ppat_vtv.vtv_ghost in
     if ghost <> (vtv.vtv_ghost || arg.vtv_ghost) then
       Loc.errorm "Ghost pattern in a non-ghost context";
+    let effect = eff_union eff pp.ppat_effect in
     match arg.vtv_mut, pp.ppat_vtv.vtv_mut with
+    | _ when ppat_is_wild pp ->
+        effect
     | Some r1, Some r2 ->
         ignore (reg_match sbs r1 r2);
-        eff_read ~ghost (eff_union eff pp.ppat_effect) (reg_full_inst sbs r1)
+        eff_read ~ghost effect (reg_full_inst sbs r1)
     | Some r1, None ->
-        eff_read ~ghost (eff_union eff pp.ppat_effect) (reg_full_inst sbs r1)
+        eff_read ~ghost effect (reg_full_inst sbs r1)
     | None, None ->
-        eff_union eff pp.ppat_effect
+        effect
     | None, Some _ ->
         Loc.errorm "Mutable pattern in a non-mutable position"
   in
@@ -218,6 +225,7 @@ let make_ppattern pp vtv =
           let ghost = vtv.vtv_ghost || arg.vtv_ghost in
           let mut = Util.option_map (reg_full_inst sbs) arg.vtv_mut in
           let pp = make (vty_value ~ghost ?mut ity) pp in
+          if ppat_is_wild pp then pp.ppat_effect, pp else
           Util.option_fold (eff_read ~ghost) pp.ppat_effect mut, pp
         in
         let ppl = try List.map2 mtch pls.pl_args ppl with Invalid_argument _ ->

src/whyml/mlw_expr.mli

@@ -189,6 +189,8 @@ val e_cast : psymbol -> vty -> expr
 exception ValueExpected of expr
 exception ArrowExpected of expr
 
+val vtv_of_expr : expr -> vty_value
+
 exception GhostWrite of expr * region
 exception GhostRaise of expr * xsymbol
 (* a ghost expression writes in a non-ghost region or raises an exception *)

src/whyml/mlw_pretty.ml

@@ -241,20 +241,17 @@ and print_enode pri fmt e = match e.e_node with
   | Eassign (pv1,r,pv2) ->
       fprintf fmt (protect_on (pri > 0) "%a <%a> <- %a")
         print_pv pv1 print_regty r print_pv pv2
-(*
-  | Tcase (v,bl) ->
+  | Ecase (pv,bl) ->
       fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
-        print_expr v (print_list newline print_branch) bl
-*)
+        print_pv pv (print_list newline print_branch) bl
   | _ ->
       fprintf fmt "<expr TODO>"
 
-(*
-and print_tbranch fmt br =
-  let p,t = t_open_branch br in
-  fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_term t;
+and print_branch fmt ({ ppat_pattern = p }, e) =
+  fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_expr e;
   Svs.iter forget_var p.pat_vars
 
+(*
 and print_tl fmt tl =
   if tl = [] then () else fprintf fmt "@ [%a]"
     (print_list alt (print_list comma print_term)) tl

src/whyml/mlw_typing.ml

@@ -214,6 +214,80 @@ let mk_let ~loc ~userloc e (desc,dity) =
     dexpr_desc = desc; dexpr_type = dity; dexpr_loc = loc; dexpr_lab = [] } in
   DElet ({ id = "q"; id_lab = []; id_loc = loc }, e, e1), dity
 
+(* patterns *)
+let id_user x = id_user x.id x.id_loc
+
+let add_var id dity denv =
+  let tvars = add_tvars denv.tvars dity in
+  let locals = Mstr.add id.id (tvars,dity) denv.locals in
+  { denv with locals = locals; tvars = tvars }
+
+let specialize_qualid ~loc uc p =
+  let x = Typing.string_list_of_qualid [] p in
+  try match ns_find_ps (get_namespace uc) x with
+    | PV pv -> DEglobal_pv pv, specialize_pvsymbol pv
+    | PS ps -> DEglobal_ps ps, specialize_psymbol  ps
+    | PL pl -> DEglobal_pl pl, specialize_plsymbol pl
+  with Not_found -> try
+    let ls = ns_find_ls (Theory.get_namespace (get_theory uc)) x in
+    DEglobal_ls ls, specialize_lsymbol ls
+  with Not_found ->
+    errorm ~loc "unbound symbol %a" Typing.print_qualid p
+
+let mk_dexpr desc dity loc labs =
+  { dexpr_desc = desc; dexpr_type = dity; dexpr_loc = loc; dexpr_lab = labs }
+
+let rec dpattern denv ({ pat_loc = loc } as pp) = match pp.pat_desc with
+  | Ptree.PPpwild ->
+      PPwild, create_type_variable (), denv
+  | Ptree.PPpvar id ->
+      let dity = create_type_variable () in
+      PPvar (id_user id), dity, add_var id dity denv
+  | Ptree.PPpapp (q,ppl) ->
+      let sym, dity = specialize_qualid ~loc denv.uc q in
+      dpat_app denv (mk_dexpr sym dity loc []) ppl
+  | Ptree.PPprec fl when pure_record ~loc denv.uc fl ->
+      let kn = Theory.get_known (get_theory denv.uc) in
+      let fl = List.map (find_pure_field ~loc denv.uc) fl in
+      let cs,pjl,flm = Loc.try2 loc Decl.parse_record kn fl in
+      let wild = { pat_desc = Ptree.PPpwild; pat_loc = loc } in
+      let get_val pj = Mls.find_def wild pj flm in
+      dpat_app denv (hidden_ls ~loc cs) (List.map get_val pjl)
+  | Ptree.PPprec fl ->
+      let fl = List.map (find_field ~loc denv.uc) fl in
+      let cs,pjl,flm = Loc.try2 loc parse_record denv.uc fl in
+      let wild = { pat_desc = Ptree.PPpwild; pat_loc = loc } in
+      let get_val pj = Mls.find_def wild pj.pl_ls flm in
+      dpat_app denv (hidden_pl ~loc cs) (List.map get_val pjl)
+  | Ptree.PPptuple ppl ->
+      let cs = fs_tuple (List.length ppl) in
+      dpat_app denv (hidden_ls ~loc cs) ppl
+  | Ptree.PPpor (pp1, pp2) ->
+      let pp1, dity1, denv = dpattern denv pp1 in
+      let pp2, dity2, denv = dpattern denv pp2 in
+      Loc.try2 loc unify dity1 dity2;
+      PPor (pp1, pp2), dity1, denv
+  | Ptree.PPpas (pp, id) ->
+      let pp, dity, denv = dpattern denv pp in
+      PPas (pp, id_user id), dity, add_var id dity denv
+
+and dpat_app denv ({ dexpr_loc = loc } as de) ppl =
+  let add_pp pp (ppl, tyl, denv) =
+    let pp,ty,denv = dpattern denv pp in pp::ppl,ty::tyl,denv in
+  let ppl, tyl, denv = List.fold_right add_pp ppl ([],[],denv) in
+  let pp = match de.dexpr_desc with
+    | DEglobal_pl pl -> Mlw_expr.PPpapp (pl, ppl)
+    | DEglobal_ls ls -> PPlapp (ls, ppl)
+    | DEglobal_pv pv ->
+        errorm ~loc "%a is not a constructor" Mlw_pretty.print_pv pv
+    | DEglobal_ps ps ->
+        errorm ~loc "%a is not a constructor" Mlw_pretty.print_ps ps
+    | _ -> assert false
+  in
+  let res = create_type_variable () in
+  Loc.try2 loc unify de.dexpr_type (make_arrow_type tyl res);
+  pp, res, denv
+
 (* value restriction *)
 let rec is_fun e = match e.dexpr_desc with
   | DEfun _ -> true
@@ -231,7 +305,7 @@ let rec dexpr ~userloc denv e =
   let labs, userloc, d = extract_labels [] userloc e in
   let d, ty = dexpr_desc ~userloc denv loc d in
   let loc = def_option loc userloc in
-  { dexpr_desc = d; dexpr_loc = loc; dexpr_lab = labs; dexpr_type = ty }
+  mk_dexpr d ty loc labs
 
 and dexpr_desc ~userloc denv loc = function
   | Ptree.Eident (Qident {id=x}) when Mstr.mem x denv.locals ->
@@ -240,43 +314,25 @@ and dexpr_desc ~userloc denv loc = function
       let dity = specialize_scheme tvs dity in
       DElocal x, dity
   | Ptree.Eident p ->
-      let x = Typing.string_list_of_qualid [] p in
-      begin try match ns_find_ps (get_namespace denv.uc) x with
-        | PV pv -> DEglobal_pv pv, specialize_pvsymbol pv
-        | PS ps -> DEglobal_ps ps, specialize_psymbol  ps
-        | PL pl -> DEglobal_pl pl, specialize_plsymbol pl
-      with Not_found -> try
-        let ls = ns_find_ls (Theory.get_namespace (get_theory denv.uc)) x in
-        DEglobal_ls ls, specialize_lsymbol ls
-      with Not_found ->
-        errorm ~loc "unbound symbol %a" Typing.print_qualid p
-      end
+      specialize_qualid ~loc denv.uc p
   | Ptree.Eapply (e1, e2) ->
       let e, el = decompose_app [e2] e1 in
       let el = List.map (dexpr ~userloc denv) el in
       dexpr_app (dexpr ~userloc denv e) el
   | Ptree.Elet (id, e1, e2) ->
       let e1 = dexpr ~userloc denv e1 in
-      let tvars =
-        if is_fun e1 then denv.tvars else add_tvars denv.tvars e1.dexpr_type in
-      let s = tvars, e1.dexpr_type in
-      let denv =
-        { denv with locals = Mstr.add id.id s denv.locals; tvars = tvars } in
+      let dity = e1.dexpr_type in
+      let tvars = if is_fun e1 then denv.tvars else add_tvars denv.tvars dity in
+      let locals = Mstr.add id.id (tvars, dity) denv.locals in
+      let denv = { denv with locals = locals; tvars = tvars } in
       let e2 = dexpr ~userloc denv e2 in
       DElet (id, e1, e2), e2.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
-        let tvars = add_tvars denv.tvars dity in
-        let denv = { denv with
-          locals = Mstr.add id.id (tvars, dity) denv.locals;
-          tvars  = tvars }
-        in
-        denv, (id, false, dity)
-      in
+          | 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 =
@@ -328,9 +384,8 @@ and dexpr_desc ~userloc denv loc = function
       let get_val pj = match Mls.find_opt pj flm with
         | Some e -> dexpr ~userloc denv e
         | None ->
-            let d,dt = dexpr_app (hidden_ls ~loc pj) [e0] in
-            { dexpr_desc = d; dexpr_type = dt; dexpr_loc = loc; dexpr_lab = [] }
-      in
+            let d, dity = dexpr_app (hidden_ls ~loc pj) [e0] in
+            mk_dexpr d dity loc [] in
       let res = dexpr_app (hidden_ls ~loc cs) (List.map get_val pjl) in
       mk_let ~loc ~userloc e1 res
   | Ptree.Eupdate (e1, fl) ->
@@ -341,9 +396,8 @@ and dexpr_desc ~userloc denv loc = function
       let get_val pj = match Mls.find_opt pj.pl_ls flm with
         | Some e -> dexpr ~userloc denv e
         | None ->
-            let d,dt = dexpr_app (hidden_pl ~loc pj) [e0] in
-            { dexpr_desc = d; dexpr_type = dt; dexpr_loc = loc; dexpr_lab = [] }
-      in
+            let d, dity = dexpr_app (hidden_pl ~loc pj) [e0] in
+            mk_dexpr d dity loc [] in
       let res = dexpr_app (hidden_pl ~loc cs) (List.map get_val pjl) in
       mk_let ~loc ~userloc e1 res
   | Ptree.Eassign (e1, q, e2) ->
@@ -367,12 +421,20 @@ and dexpr_desc ~userloc denv loc = function
       expected_type e1 dity_bool;
       expected_type e2 dity_bool;
       DElazy (op, e1, e2), dity_bool
+  | Ptree.Ematch (e1, bl) ->
+      let e1 = dexpr ~userloc denv e1 in
+      let res = create_type_variable () in
+      let branch (pp,e) =
+        let ppat, dity, denv = dpattern denv pp in
+        let e = dexpr ~userloc denv e in
+        Loc.try2 pp.pat_loc unify dity e1.dexpr_type;
+        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.Ematch (_e1, _bl) ->
-      assert false (*TODO*)
   | Ptree.Eabsurd ->
       assert false (*TODO*)
   | Ptree.Eraise (_q, _e1) ->
@@ -398,8 +460,6 @@ and dtriple ~userloc denv (p, e, q) =
 and dpost _denv (q, _ql) =
   q, [] (* TODO *)
 
-let id_user x = id_user x.id x.id_loc
-
 let rec expr locals de = match de.dexpr_desc with
   | DElocal x ->
       assert (Mstr.mem x locals);
@@ -452,6 +512,14 @@ let rec expr locals de = match de.dexpr_desc with
       e_lazy_or (expr locals de1) (expr locals de2)
   | DEnot de1 ->
       e_not (expr locals de1)
+  | DEmatch (de1, bl) ->
+      let e1 = expr locals de1 in
+      let vtv = vtv_of_expr e1 in
+      let branch (pp,de) =
+        let vm, pp = make_ppattern pp vtv in
+        let locals = Mstr.fold (fun s pv -> Mstr.add s (LetV pv)) vm locals in
+        pp, expr locals de in
+      e_case e1 (List.map branch bl)
   | _ ->
       assert false (*TODO*)
 

tests/test-pgm-jcf.mlx

@@ -23,15 +23,14 @@ module N
 
   type ref 'b = {| ghost mutable contents : 'b |}
 
-  type myrec 'a = {| f1 : int ; f2 : tree 'a |}
+  type myrec 'a = {| f1 : int ; ghost f2 : tree 'a |}
 
   let h x =
     let bang y = y.contents in
-    let z = bang x + zero in
-    let u = {| f1 = z; f2 = Node x Nil |} in
-    let r = {| contents = {| u with f2 = Node one Nil |} |} in
-    x.contents <- one;
-    zero
+    match x with
+    | {| f2 = Node x _ |} -> Node x Nil
+    | _ -> Leaf
+    end
 end
 
 (*