Code extraction: work in progress

Added support for translation and printing of lambdas
in an expression. This can be done via partial application
or by defining a [fun -> ...] expression explicitly

src/mlw/compile.ml

@@ -331,8 +331,28 @@ module Translate = struct
       let ml_let = ML.ml_let pvs ML.mk_unit (expr info e2) in
        ML.mk_expr ml_let (ML.I e.e_ity) eff
     | Elet (LDvar (pvs, e1), e2) ->
-       let ml_let = ML.ml_let pvs (expr info e1) (expr info e2) in
-       ML.mk_expr ml_let (ML.I e.e_ity) eff
+      let ml_let = ML.ml_let pvs (expr info e1) (expr info e2) in
+      ML.mk_expr ml_let (ML.I e.e_ity) eff
+    | Elet (LDsym (rs, {c_node = Cfun ef; c_cty = cty}), ein) ->
+      let p pv = not pv.pv_ghost in
+      let def pv = pv_name pv, ity pv.pv_ity, pv.pv_ghost in
+      let al pv = pv_name pv, ML.tunit, false in
+      let args = filter2_ghost_params p def al cty.cty_args in
+      let ef = expr info ef in
+      let ein = expr info ein in
+      let ml_letrec = ML.Eletrec (false, [rs, args, ef], ein) in
+      ML.mk_expr ml_letrec (ML.I e.e_ity) eff
+    | Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); _}), ein) ->
+      let p pv = not pv.pv_ghost in
+      let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) eff_empty in
+      let al _ = ML.mk_unit in
+      let args = filter2_ghost_params p def al pvl in
+      let eapp =
+        ML.mk_expr (ML.Eapp (rs_app, args)) (ML.I ein.e_ity) ein.e_effect in
+      let ein = expr info ein in
+
+      let ml_letrec = ML.Eletrec (false, [rsf, [], eapp], ein) in
+      ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
     | Eexec ({c_node = Capp (rs, [])}, _) when is_rs_tuple rs ->
       ML.mk_unit
     | Eexec ({c_node = Capp (rs, _)}, _) when rs_ghost rs ->
@@ -340,6 +360,14 @@ module Translate = struct
     | Eexec ({c_node = Capp (rs, pvl)}, _) ->
       let pvl = app info rs pvl in
       ML.mk_expr (ML.Eapp (rs, pvl)) (ML.I e.e_ity) eff
+    | Eexec ({c_node = Cfun e; c_cty = cty}, _) ->
+      Format.printf "Length of args:%d@\n" (List.length cty.cty_args);
+      let p pv = not pv.pv_ghost in
+      let def pv = pv_name pv, ity pv.pv_ity, pv.pv_ghost in
+      let al pv = pv_name pv, ML.tunit, false in
+      let args = filter2_ghost_params p def al cty.cty_args in
+      ML.mk_expr (ML.Efun (args, expr info e)) (ML.I e.e_ity) eff
+    | Eexec _ -> assert false
     | Eabsurd ->
       ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
     | Ecase (e1, _) when e_ghost e1 ->
@@ -359,6 +387,11 @@ module Translate = struct
       expr info eg (* it keeps its ghost status *)
     | Eassign [(_, rs, pv)] ->
       ML.mk_expr (ML.Eassign [(rs, pv)]) (ML.I e.e_ity) eff
+    | Epure _ -> assert false
+    | Efor _ -> assert false
+    | Ewhile _ -> assert false
+    | Etry _ -> assert false
+    | Eraise _ -> assert false
     | _ -> (* TODO *) assert false
 
   and ebranch info ({pp_pat = p}, e) =

src/mlw/ocaml_printer.ml

@@ -234,7 +234,7 @@ module Print = struct
     | Evar pvs ->
        (print_lident info) fmt (pv_name pvs)
     | Elet (pv, e1, e2) ->
-       fprintf fmt "@[<hov 2>let @[%a@] =@ @[%a@]@] in@ %a"
+       fprintf fmt "@[<hov 2>let %a =@ @[%a@]@] in@ %a"
          (print_lident info) (pv_name pv) (print_expr info) e1 (print_expr info) e2
     | Eabsurd ->
        fprintf fmt "assert false (* absurd *)"
@@ -258,11 +258,29 @@ module Print = struct
     | Eblock [e] ->
       print_expr info fmt e
     | Eblock el ->
-      fprintf fmt "@[<hv>begin@;<1 2>@[%a@]@ end@]" (print_list semi (print_expr info)) el
+      fprintf fmt "@[<hv>begin@;<1 2>@[%a@]@ end@]"
+        (print_list semi (print_expr info)) el
+    | Efun (varl, e) ->
+      printf "list length:%d@\n" (List.length varl);
+      fprintf fmt "@[<hov 2>(fun %a ->@ %a)@]"
+        (print_list space print_vs_arg) varl (print_expr info) e
+    | Eletrec (is_rec, [rs, [], ef], ein) ->
+      fprintf fmt "@[<hov 2>let %s%a =@ @[%a@]@] in@ %a"
+        (if is_rec then "rec " else "")
+        (print_lident info) rs.rs_name
+        (print_expr info) ef
+        (print_expr info) ein
+    | Eletrec (is_rec, [rs, args, ef], ein) ->
+      fprintf fmt "@[<hov 2>let %s%a %a@ =@ @[%a@]@] in@ %a"
+        (if is_rec then "rec " else "")
+        (print_lident info) rs.rs_name
+        (print_list space print_vs_arg) args
+        (print_expr info) ef
+        (print_expr info) ein
     | _ -> (* TODO *) assert false
 
   and print_branch info fmt (p, e) =
-    fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p (print_expr info) e
+    fprintf fmt "@[<hov 4>| %a ->@ @[%a@]@]" print_pat p (print_expr info) e
 
   and print_expr info fmt e =
     print_enode info fmt e.e_node
@@ -304,7 +322,7 @@ module Print = struct
 
   let print_decl info fmt = function
     | Dlet (isrec, [rs, pvl, e]) ->
-       fprintf fmt "@[<hov 2>%s %a@ %a@ =@ %a@]"
+       fprintf fmt "@[<hov 2>%s %a@ %a =@ @[%a@]@]"
                (if isrec then "let rec" else "let")
                print_ident rs.rs_name
                (print_list space print_vs_arg) pvl

tests/test_extraction_mario.mlw

@@ -31,8 +31,16 @@ module M
     ghost mutable v : seq 'a;
   }
 
-  let create_cursor (l: list int) (i i2: int) : cursor int =
-    { collection = l; index = i; index2 = i2; v = empty }
+  type r 'a = {
+    aa: 'a;
+    ghost i: int;
+  }
+
+  (* let create_cursor (l: list int) (i i2: int) : cursor int = *)
+  (*   { collection = l; index = i; index2 = i2; v = empty } *)
+
+  let create_r (x: int) (y: int) : r int =
+    { aa = x; i = y }
 
   use import ref.Ref
 
@@ -80,8 +88,6 @@ module M
     x 42
 *)
 
-  use import int.Int
-
   let test (x: int) : int =
     let y =
       let z = x in
@@ -111,8 +117,6 @@ module M
     42
 
   let test_call (x: int) : int =
-    (* FIXME let partial = test_filter_ghost_args x in
-    partial 42; *)
     test_filter_ghost_args x 0
 
   let many_args (a b c d e f g h i j k l m: int) : int = 42
@@ -121,6 +125,19 @@ module M
     let _ = 42 in (* FIXME? print _ in OCaml *)
     x
 
+  let test_fun (x: int) : int -> int =
+    fun (y: int) -> x + y
+
+  let test_partial (x: int) : int =
+    let partial = test_filter_ghost_args x in
+    partial 42
+
+  let test_local (x: int) : int =
+    let fact (x: int) (y: int): int = x + y
+    in
+    fact x 42
+
+
   (* let filter_record (c: cursor 'a) : int = *)
   (*   match c with *)
   (*   | { collection = l; index = i; index2 = i2; v = v} -> i *)