Extraction of match..with..exception expressions

src/mlw/compile.ml

@@ -45,7 +45,7 @@ module ML = struct
 
   let rec get_decl_name = function
     | Dtype itdefl ->
-        let add_id = function
+        let add_id = function (* add name of constructors and projections *)
           | Some (Ddata l)   -> List.map (fun (idc,    _) -> idc) l
           | Some (Drecord l) -> List.map (fun (_, idp, _) -> idp) l
           | _ -> [] in
@@ -152,9 +152,9 @@ module ML = struct
     | Eexn (_xs, Some ty, e) -> (* FIXME? How come we never do binding here? *)
         iter_deps_ty f ty;
         iter_deps_expr f e
-    | Etry (e, xbranchl) ->
+    | Etry (e, _, xl) ->
         iter_deps_expr f e;
-        List.iter (iter_deps_xbranch f) xbranchl
+        List.iter (iter_deps_xbranch f) xl
     | Eassign assingl ->
         List.iter (fun (_, rs, _) -> f rs.rs_name) assingl
     | Eignore e -> iter_deps_expr f e
@@ -236,6 +236,11 @@ module ML = struct
   let e_match e bl =
     mk_expr (Mltree.Ematch (e, bl))
 
+  let e_match_exn e bl eff_bl lbl_match xl =
+    let ity = match bl with (_, d) :: _ -> d.e_ity | [] -> assert false in
+    let e = e_match e bl ity eff_bl lbl_match in
+    mk_expr (Mltree.Etry (e, true, xl))
+
   let e_assign al ity eff lbl =
     if al = [] then e_unit else mk_expr (Mltree.Eassign al) ity eff lbl
 
@@ -558,8 +563,8 @@ module Translate = struct
            it must be the case the first branch is irrefutable *)
         (match bl with
          | [] -> assert false | (_, e) :: _ -> expr info svar e.e_mask e)
-    | Ecase (e1, pl) -> let pl = List.map (ebranch info svar mask) pl in
-        ML.e_match (expr info svar e1.e_mask e1) pl (Mltree.I e.e_ity) eff lbl
+    | Ecase (e1, bl) -> let bl = List.map (ebranch info svar mask) bl in
+        ML.e_match (expr info svar e1.e_mask e1) bl (Mltree.I e.e_ity) eff lbl
     | Eassert _ ->
         ML.e_unit
     | Eif (e1, e2, e3) when e_ghost e1 ->
@@ -590,29 +595,32 @@ module Translate = struct
         let dir = for_direction dir in
         let efor = expr info svar efor.e_mask efor in
         ML.e_for pv1 pv2 dir pv3 efor eff lbl
-    | Eghost _ | Epure _ -> assert false
+    | Eghost _ | Epure _ ->
+        assert false
     | Eassign al ->
         let rm_ghost (_, rs, _) = not (rs_ghost rs) in
         let al = List.filter rm_ghost al in
         ML.e_assign al (Mltree.I e.e_ity) eff lbl
-    | Etry (etry, case, pvl_e_map) ->
-        assert (not case); (* TODO *)
+    | Etry ({e_node = Ecase (etry, bl); e_effect; e_label}, true, xl) ->
+        let etry = expr info svar etry.e_mask etry in
+        let bl = List.map (ebranch info svar mask) bl in
+        let mk_xl (xs, (pvl, e)) = xs, pvl, expr info svar mask e in
+        let xl = Mxs.bindings xl in
+        let xl = List.map mk_xl xl in
+        ML.e_match_exn etry bl e_effect e_label xl (Mltree.I e.e_ity) eff lbl
+    | Etry (etry, _, xl) ->
         let etry = expr info svar mask etry in
-        let bl   =
-          let bl_map = Mxs.bindings pvl_e_map in
-          let mk_bl_map (xs, (pvl, e)) = xs, pvl, expr info svar mask e in
-          List.map mk_bl_map bl_map in
-        ML.mk_expr (Mltree.Etry (etry, bl)) (Mltree.I e.e_ity) eff lbl
-    | Eraise (xs, ex) ->
-        (* let ex = exp_of_mask ex xs.xs_mask in *)
-        let ex = expr info svar xs.xs_mask ex in
-        let ex = match ex with
-          | {Mltree.e_node = Mltree.Eblock []} -> None
-          | e -> Some e in
+        let mk_xl (xs, (pvl, e)) = xs, pvl, expr info svar mask e in
+        let xl = Mxs.bindings xl in
+        let xl = List.map mk_xl xl in
+        ML.mk_expr (Mltree.Etry (etry, false, xl)) (Mltree.I e.e_ity) eff lbl
+    | Eraise (xs, ex) -> let ex = match expr info svar xs.xs_mask ex with
+        | {Mltree.e_node = Mltree.Eblock []} -> None
+        | e -> Some e in
         ML.mk_expr (Mltree.Eraise (xs, ex)) (Mltree.I e.e_ity) eff lbl
     | Eexn (xs, e1) ->
         if mask_ghost e1.e_mask then ML.mk_expr
-            (Mltree.Eexn (xs, None, ML.e_unit)) (Mltree.I e.e_ity) eff lbl
+          (Mltree.Eexn (xs, None, ML.e_unit)) (Mltree.I e.e_ity) eff lbl
         else let e1 = expr info svar xs.xs_mask e1 in
           let ty = if ity_equal xs.xs_ity ity_unit then None
             else Some (mlty_of_ity xs.xs_mask xs.xs_ity) in
@@ -838,10 +846,10 @@ module Transform = struct
     | Eraise (exn, Some e) ->
         let e, spv = expr info subst e in
         mk (Eraise (exn, Some e)), spv
-    | Etry (e, bl) ->
+    | Etry (e, case, bl) ->
         let e, spv = expr info subst e in
         let e_bl, spv_bl = mk_list_eb bl (xbranch info subst) in
-        mk (Etry (e, e_bl)), Spv.union spv spv_bl
+        mk (Etry (e, case, e_bl)), Spv.union spv spv_bl
     | Eassign _al -> (* FIXME : produced superfolous let *)
         (* let assign e (_, _, pv) = mk_let subst pv e in *)
         e, (* List.fold_left assign e al, *) Spv.empty

src/mlw/cprinter.ml

@@ -836,7 +836,8 @@ module MLToC = struct
                                    C.Sblock b))))
         end
       end
-    | Etry (b,xl) ->
+    | Etry (b, case, xl) ->
+        assert (not case); (* TODO *)
       if debug then Format.printf "TRY@.";
       let is_while = match b.e_node with Ewhile _ -> true | _-> false in
       let breaks, returns = List.fold_left

src/mlw/mltree.ml

@@ -28,11 +28,11 @@ type for_direction = To | DownTo
 
 type pat =
   | Pwild
-  | Pvar    of vsymbol
-  | Papp    of lsymbol * pat list
-  | Ptuple  of pat list
-  | Por     of pat * pat
-  | Pas     of pat * vsymbol
+  | Pvar   of vsymbol
+  | Papp   of lsymbol * pat list
+  | Ptuple of pat list
+  | Por    of pat * pat
+  | Pas    of pat * vsymbol
 
 type is_rec = bool
 
@@ -62,7 +62,7 @@ and expr_node =
   | Efor    of pvsymbol * pvsymbol * for_direction * pvsymbol * expr
   | Eraise  of xsymbol * expr option
   | Eexn    of xsymbol * ty option * expr
-  | Etry    of expr * (xsymbol * pvsymbol list * expr) list
+  | Etry    of expr * bool * (xsymbol * pvsymbol list * expr) list
   | Eignore of expr
   | Eabsurd
   | Ehole

src/mlw/ocaml_printer.ml

@@ -250,8 +250,8 @@ module Print = struct
             match pjl with
             | []  -> print_papp info ls fmt pl
             | pjl -> fprintf fmt "@[<hov 2>{ %a }@]"
-                       (print_list2 semi equal (print_rs info) (print_pat info))
-                       (pjl, pl)
+                (print_list2 semi equal (print_rs info) (print_pat info))
+                (pjl, pl)
 
   and print_papp info ls fmt = function
     | []  -> fprintf fmt "%a"      (print_uident info) ls.ls_name
@@ -525,10 +525,14 @@ module Print = struct
           (* then    *) (print_expr info) e (print_lident info) for_id
                         op (print_pv info) pv1
           (* in      *) (print_lident info) for_id (print_pv info) pv2
-    | Etry (e, bl) ->
+    | Etry ({e_node = Ematch (e, bl)}, true, xl) ->
         fprintf fmt
-          "@[<hv>@[<hov 2>begin@ try@ %a@] with@]@\n@[<hov>%a@]@\nend"
-          (print_expr info) e (print_list newline (print_xbranch info)) bl
+          (protect_on paren "begin match @[%a@] with@\n@[<hov>%a@\n%a@]@\nend")
+          (print_expr info) e (print_list newline (print_branch info)) bl
+          (print_list newline (print_xbranch info true)) xl
+    | Etry (e, _, xl) ->
+        fprintf fmt "@[<hv>@[<hov 2>begin@ try@ %a@] with@]@\n@[<hov>%a@]@\nend"
+          (print_expr info) e (print_list newline (print_xbranch info false)) xl
     | Eexn (xs, None, e) ->
         fprintf fmt "@[<hv>let exception %a in@\n%a@]"
           (print_uident info) xs.xs_name (print_expr info) e
@@ -557,22 +561,22 @@ module Print = struct
         fprintf fmt (protect_on paren "raise (%a %a)")
           (print_uident info) xs.xs_name (print_expr ~paren:true info) e
 
-  and print_xbranch info fmt (xs, pvl, e) =
-    let print_var fmt pv =
-      print_lident info fmt (pv_name pv) in
+  and print_xbranch info case fmt (xs, pvl, e) =
+    let print_exn fmt () =
+      if case then fprintf fmt "exception " else fprintf fmt "" in
+    let print_var fmt pv = print_lident info fmt (pv_name pv) in
     match query_syntax info.info_syn xs.xs_name, pvl with
-    | Some s, _ ->
-        fprintf fmt "@[<hov 4>| %a ->@ %a@]"
-          (syntax_arguments s print_var) pvl (print_expr info ~paren:true) e
-    | None, []->
-        fprintf fmt "@[<hov 4>| %a ->@ %a@]" (print_uident info) xs.xs_name
-          (print_expr info) e
-    | None, [pv] ->
-        fprintf fmt "@[<hov 4>| %a %a ->@ %a@]" (print_uident info) xs.xs_name
-          print_var pv (print_expr info) e
-    | None, pvl ->
-        fprintf fmt "@[<hov 4>| %a %a ->@ %a@]" (print_uident info) xs.xs_name
-          (print_list comma print_var) pvl (print_expr info) e
+    | Some s, _ -> fprintf fmt "@[<hov 4>| %a%a ->@ %a@]"
+        print_exn () (syntax_arguments s print_var) pvl
+        (print_expr info ~paren:true) e
+    | None, [] -> fprintf fmt "@[<hov 4>| %a%a ->@ %a@]"
+        print_exn () (print_uident info) xs.xs_name (print_expr info) e
+    | None, [pv] -> fprintf fmt "@[<hov 4>| %a%a %a ->@ %a@]"
+        print_exn () (print_uident info) xs.xs_name print_var pv
+        (print_expr info) e
+    | None, pvl -> fprintf fmt "@[<hov 4>| %a%a (%a) ->@ %a@]"
+        print_exn () (print_uident info) xs.xs_name
+        (print_list comma print_var) pvl (print_expr info) e
 
   let print_type_decl info fst fmt its =
     let print_constr fmt (id, cs_args) =

src/transform/reification.ml

@@ -1151,7 +1151,8 @@ let rec interp_expr info (e:Mltree.expr) : value =
                raise CannotReduce
   | Ehole -> Debug.dprintf debug_interp "Ehole@.";
              raise CannotReduce
-  | Etry (e,bl) ->
+  | Etry (e, case, bl) ->
+     assert (not case); (* TODO *)
      try interp_expr info e
      with (Raised (xs, ov, _)  as e) ->
           let rec aux = function