Code extraction (wip)

Minor changes in compile.ml and ocaml_printer.ml

src/mlw/compile.ml

@@ -102,8 +102,7 @@ module ML = struct
   type binop = Band | Bor | Beq
 
   type exn =
-    | Xident  of ident
-    | Xexit             (* Pervasives.Exit *)
+    | Xident of ident
 
   type ity = I of Ity.ity | C of Ity.cty (* TODO: keep it like this? *)
 
@@ -123,7 +122,7 @@ module ML = struct
     | Eletrec of is_rec * (rsymbol * var list * expr) list * expr
     | Eif     of expr * expr * expr
     | Ecast   of expr * ty
-    | Eassign of (rsymbol * pvsymbol) list
+    | Eassign of (pvsymbol * rsymbol * pvsymbol) list
     | Etuple  of expr list (* at least 2 expressions *)
     | Ematch  of expr * (pat * expr) list
     | Ebinop  of expr * binop * expr
@@ -340,7 +339,7 @@ module Translate = struct
 
   (* expressions *)
   let rec expr info ({e_effect = eff} as e) =
-    (* assert (not eff.eff_ghost); *)
+    assert (not eff.eff_ghost);
     match e.e_node with
     | Econst c ->
        let c = match c with Number.ConstInt c -> c | _ -> assert false in
@@ -410,16 +409,24 @@ module Translate = struct
       let e2 = expr info e2 in
       ML.mk_expr (ML.Ewhile (e1, e2)) (ML.I e.e_ity) eff
     | Efor (pv1, (pv2, direction, pv3), _, efor) ->
-      let e = expr info e in
+      let efor = expr info efor in
       let direction = for_direction direction in
-      ML.mk_expr (ML.Efor (pv1, pv2, direction, pv3, e)) (ML.I efor.e_ity) eff
-    | Eghost eg ->
-      expr info eg (* it keeps its ghost status *)
-    | Eassign [(_, rs, pv)] ->
-      ML.mk_expr (ML.Eassign [(rs, pv)]) (ML.I e.e_ity) eff
+      ML.mk_expr (ML.Efor (pv1, pv2, direction, pv3, efor)) (ML.I e.e_ity) eff
+    | Eghost _ ->
+      ML.mk_unit
+    | Eassign [(rho, rs, pv)] ->
+      ML.mk_expr (ML.Eassign [(rho, rs, pv)]) (ML.I e.e_ity) eff
     | Epure _ -> assert false
     | Etry _ -> assert false
-    | Eraise _ -> assert false
+    | Eraise (xs, ex) ->
+      let ex =
+        let open ML in
+        match expr info ex with
+        | {e_node = Eblock []} -> None
+        | e -> Some e
+      in
+      let exn = ML.Xident xs.xs_name in
+      ML.mk_expr (ML.Eraise (exn, ex)) (ML.I e.e_ity) eff
     | _ -> (* TODO *) assert false
 
   and ebranch info ({pp_pat = p}, e) =

src/mlw/ocaml_printer.ml

@@ -55,9 +55,18 @@ module Print = struct
     forget_all aprinter
 
   let forget_id vs = forget_id iprinter vs
+  let _forget_ids = List.iter forget_id
   let forget_var (id, _, _) = forget_id id
   let forget_vars = List.iter forget_var
 
+  let rec forget_pat = function
+    | Pwild -> ()
+    | Pident id -> forget_id id
+    | Papp (_, pl) | Ptuple pl -> List.iter forget_pat pl
+    | Precord pl -> List.iter (fun (_,p) -> forget_pat p) pl
+    | Por (p1, p2) -> forget_pat p1; forget_pat p2
+    | Pas (p, _) -> forget_pat p
+
   let print_ident fmt id =
     let s = id_unique iprinter id in
     fprintf fmt "%s" s
@@ -104,6 +113,9 @@ module Print = struct
     | Ttuple tl ->
       fprintf fmt (protect_on paren "@[%a@]")
         (print_list star (print_ty ~paren:false info)) tl
+    | Tapp (ts, [t1; t2]) when id_equal ts ts_func.ts_name ->
+      fprintf fmt (protect_on paren "@[%a ->@ %a@]")
+        (print_ty ~paren:true info) t1 (print_ty info) t2
     | Tapp (ts, tl) ->
       begin match query_syntax info.info_syn ts with
         | Some s -> syntax_arguments s (print_ty info) fmt tl
@@ -169,11 +181,6 @@ module Print = struct
        in
        fprintf fmt "{ %a }" (print_list semi print_field) fl
 
-  let print_const fmt c =
-    let n = Number.compute_int c in
-    let m = BigInt.to_int n in
-    fprintf fmt "%d" m
-
   (** Expressions *)
 
   let extract_op {id_string = s} =
@@ -194,11 +201,8 @@ module Print = struct
   let rec args_syntax info fmt s tl =
     try
       ignore (Str.search_forward (Str.regexp "[%]\\([tv]?\\)[0-9]+") s 0);
-      printf "template: %s@\n" s;
       syntax_arguments s (print_expr info) fmt tl
-    with Not_found ->
-      ()
-      (* tl *)
+    with Not_found -> ()
 
   and print_apply info fmt rs pvl =
     let isfield =
@@ -214,15 +218,16 @@ module Print = struct
         List.exists is_constructor its
       | _ -> false
     in
-    match extract_op rs.rs_name, pvl with
-    | Some o, [e1; e2] ->
-      fprintf fmt "@[<hov 1>%a %s %a@]"
-        (print_expr info) e1 o (print_expr info) e2
-    | _, [] ->
-       print_ident fmt rs.rs_name
-    | _, [t1] when isfield ->
+    match query_syntax info.info_convert rs.rs_name,
+          query_syntax info.info_syn rs.rs_name, pvl with
+    | Some s, _, _
+    | _, Some s, _ ->
+      syntax_arguments s (print_expr info) fmt pvl
+    | _, _, [] ->
+      print_ident fmt rs.rs_name
+    | _,  _, [t1] when isfield ->
       fprintf fmt "%a.%a" (print_expr info) t1 print_ident rs.rs_name
-    | _, tl when isconstructor () ->
+    | _, _, tl when isconstructor () ->
       let pjl = get_record info rs in
       if pjl = [] then
         fprintf fmt "@[<hov 2>%a (%a)@]"
@@ -240,45 +245,43 @@ module Print = struct
         in
         fprintf fmt "@[<hov 2>{ %a}@]"
           (print_list2 semi equal (print_rs info) (print_expr info)) (pjl, tl)
-    | _, tl ->
-      match query_syntax info.info_convert rs.rs_name,
-            query_syntax info.info_syn rs.rs_name with
-      | Some s, _
-      | _, Some s ->
-        syntax_arguments s (print_expr info) fmt tl;
-        args_syntax info fmt s tl;
-        fprintf fmt "@[<hov 2>%s %a@]"
-          s (print_list space (print_expr info)) tl
-      | _ ->
+    | _, _, tl ->
         fprintf fmt "@[<hov 2>%a %a@]"
           print_ident rs.rs_name (print_list space (print_expr info)) tl
 
   and print_enode info fmt = function
     | Econst c ->
-       fprintf fmt "%a" print_const c
+      let n = Number.compute_int c in
+      fprintf fmt "(Z.of_string \"%s\")" (BigInt.to_string n)
     | Evar pvs ->
-       (print_lident info) fmt (pv_name pvs)
+      (print_lident info) fmt (pv_name pvs)
     | Elet (pv, e1, e2) ->
-       fprintf fmt "@[<hov 2>let %a =@ %a@] in@\n%a"
-         (print_lident info) (pv_name pv)
-         (print_expr info) e1 (print_expr info) e2
+      fprintf fmt "@[<hov 2>let %a =@ %a@] in@\n%a"
+        (print_lident info) (pv_name pv)
+        (print_expr info) e1 (print_expr info) e2;
+      forget_id (pv_name pv)
     | Eabsurd ->
-       fprintf fmt "assert false (* absurd *)"
+      fprintf fmt "assert false (* absurd *)"
     | Eapp (s, []) when rs_equal s rs_true ->
-       fprintf fmt "true"
+      fprintf fmt "true"
     | Eapp (s, []) when rs_equal s rs_false ->
       fprintf fmt "false"
     | Eapp (s, [e1; e2]) when rs_equal s rs_func_app ->
       fprintf fmt "@[<hov 1>%a %a@]"
         (print_expr info) e1 (print_expr info) e2
     | Eapp (s, pvl) ->
-       print_apply info fmt s pvl
+      print_apply info fmt s pvl
     | Ematch (e, pl) ->
-      fprintf fmt "@[begin match @[%a@] with@\n@[<hov>%a@] end@]"
+      fprintf fmt "begin match @[%a@] with@\n@[<hov>%a@] end"
         (print_expr info) e (print_list newline (print_branch info)) pl
-    | Eassign [(rs, pv)] ->
-      fprintf fmt "%a <-@ %a"
-        print_ident rs.rs_name print_ident (pv_name pv)
+    | Eassign [(rho, rs, pv)] ->
+      fprintf fmt "%a.%a <-@ %a"
+        print_ident (pv_name rho) print_ident rs.rs_name
+        print_ident (pv_name pv)
+    | Eif (e1, e2, {e_node = Eblock []}) ->
+      fprintf fmt
+        "@[<hv>@[<hov 2>if@ %a@]@ then begin@;<1 2>@[%a@] end@]"
+        (print_expr info) e1 (print_expr info) e2
     | Eif (e1, e2, e3) ->
       fprintf fmt
         "@[<hv>@[<hov 2>if@ %a@]@ then@;<1 2>@[%a@]@;<1 0>else@;<1 2>@[%a@]@]"
@@ -306,7 +309,32 @@ module Print = struct
         (print_list space (print_vs_arg info)) args
         (print_expr info) ef
         (print_expr info) ein
-    | _ -> (* TODO *) assert false
+    | Ewhile (e1, e2) ->
+      fprintf fmt "@[<hov 2>while %a do@ %a@ done@]"
+        (print_expr info) e1 (print_expr info) e2
+    | Eraise (Xident id, None) -> (* FIXME : check exceptions in driver *)
+      fprintf fmt "raise %a" (print_uident info) id
+    | Eraise (Xident id, Some e) ->
+      fprintf fmt "(raise %a %a)"
+        (print_uident info) id (print_expr info) e
+    | Etuple _ -> (* TODO *) assert false
+    | Efor (pv1, pv2, direction, pv3, e) ->
+      let print_for_direction fmt = function
+        | To -> fprintf fmt "to"
+        | DownTo -> fprintf fmt "downto"
+      in
+      fprintf fmt "@[<hov 2>for %a = %a %a %a do@ @[%a@]@ done@]"
+        (print_lident info) (pv_name pv1)
+        (print_lident info) (pv_name pv2)
+        print_for_direction direction
+        (print_lident info) (pv_name pv3)
+        (print_expr info) e
+    | Etry _ -> (* TODO *) assert false
+    | Enot _ -> (* TODO *) assert false
+    | Ebinop _ -> (* TODO *) assert false
+    | Eletrec _ -> (* TODO *) assert false
+    | Ecast _ -> (* TODO *) assert false
+    | Eassign _ -> (* TODO *) assert false
 
   and print_branch info fmt (p, e) =
     fprintf fmt "@[<hov 4>| %a ->@ @[%a@]@]" print_pat p (print_expr info) e
@@ -350,6 +378,13 @@ module Print = struct
       print_def its.its_def
 
   let print_decl info fmt = function
+    | Dlet (isrec, [rs, [], e]) ->
+       fprintf fmt "@[<hov 2>%s %a =@ %a@]"
+               (if isrec then "let rec" else "let")
+               print_ident rs.rs_name
+               (print_expr info) e;
+       forget_tvs ();
+       fprintf fmt "@\n@\n"
     | Dlet (isrec, [rs, pvl, e]) ->
        fprintf fmt "@[<hov 2>%s %a@ %a =@ %a@]"
                (if isrec then "let rec" else "let")
@@ -384,7 +419,6 @@ let extract_module pargs ?old fmt ({mod_theory = th} as m) =
     info_mo_known_map = m.mod_known;
     info_fname        = None; (* TODO *)
   } in
-  fprintf fmt "(*@\n%a@\n*)@\n@\n" print_module m;
   fprintf fmt
     "(* This file has been generated from Why3 module %a *)@\n@\n"
     Print.print_module_name m;

tests/test_extraction_mario.mlw

 module M
 
-  use import int.Int
-  use import seq.Seq
+  use import mach.int.Int31
 
-  let function f (y: int) (x: int) : int
-    requires { x >= 0 }
-    ensures  { result >= 0 }
-  = x
+  let f (x: int31) : int
+  = min_int31
 
-  let g (ghost z: int) (x: int) : int
-    requires { x > 0 }
-    ensures  { result > 0 }
-  = let y = x in
-    y
+(*   use import seq.Seq *)
 
-  type t 'a 'b 'c 'd
+(*   let function f (y: int) (x: int) : int *)
+(*     requires { x >= 0 } *)
+(*     ensures  { result >= 0 } *)
+(*   = x *)
 
-  type list 'a = Nil | Cons 'a (list 'a)
+(*   let g (ghost z: int) (x: int) : int *)
+(*     requires { x > 0 } *)
+(*     ensures  { result > 0 } *)
+(*   = let y = x in *)
+(*     y *)
 
-  type btree 'a = E | N (btree 'a) 'a (btree 'a)
+(*   type t 'a 'b 'c 'd *)
 
-  type ntree 'a = Empty | Node 'a (list 'a)
+(*   type list 'a = Nil | Cons 'a (list 'a) *)
 
-  type list_int = list int
+(*   type btree 'a = E | N (btree 'a) 'a (btree 'a) *)
 
-  type cursor 'a = {
-    collection : list 'a;
-    index      : int;
-    mutable index2     : int;
-    ghost mutable v : seq 'a;
-  }
+(*   type ntree 'a = Empty | Node 'a (list 'a) *)
 
-  type r 'a = {
-    aa: 'a;
-    ghost i: int;
-  }
+(*   type list_int = list int *)
 
-  (* let create_cursor (l: list int) (i i2: int) : cursor int = *)
-  (*   { collection = l; index = i; index2 = i2; v = empty } *)
+(*   type cursor 'a = { *)
+(*     collection : list 'a; *)
+(*     index      : int; *)
+(*     mutable index2     : int; *)
+(*     ghost mutable v : seq 'a; *)
+(*   } *)
 
-  let create_r (x: int) (y: int) : r int =
-    { aa = x; i = y }
+(*   type r 'a = { *)
+(*     aa: 'a; *)
+(*     ghost i: int; *)
+(*   } *)
 
-  use import ref.Ref
+(*   (\* let create_cursor (l: list int) (i i2: int) : cursor int = *\) *)
+(*   (\*   { collection = l; index = i; index2 = i2; v = empty } *\) *)
 
-  let update (c: cursor int) : int
-  = c.index
+(*   let create_r (x: int) (y: int) : r int = *)
+(*     { aa = x; i = y } *)
 
-  exception Empty (list int, int)
-  exception Out_of_bounds int
+(*   use import ref.Ref *)
 
-  (* exception are unary constructors *)
-(*
-  let raise1 () =
-    raises { Empty -> true }
-    raise (Empty (Nil, 0))
-  let raise2 () =
-    raises { Empty -> true }
-    let p = (Nil, 0) in
-    raise (Empty p)
-*)
-
-  let rec length (l: list 'a) : int
-    variant  { l }
-  = match l with
-    | Nil -> 0
-    | Cons _ r -> 1 + length r
-    end
-
-  let t (x:int) : int
-    requires { false }
-  = absurd
-
-  let a () : unit
-  = assert { true }
-
-  let singleton (x: int) (l: list int) : list int =
-    let x = Nil in x
-
-(* FIXME constructors in Why3 can be partially applied
-         => an eta-expansion is needed
-         be careful with side-effects
-         "let c = Cons e in" should be translated to
-         "let c = let o = e in fun x -> Cons (o, x) in ..." in OCaml
-
-   Mário: I think A-normal form takes care of the side-effects problem
-*)
-  let constructor1 () =
-    let x = Cons in
-    x 42
-
-  let foofoo (x: int) : int =
-    let ghost y = x + 1 in
-    x
-
-  let test (x: int) : int =
-    let y =
-      let z = x in
-      (ghost z) + 1
-    in 42
-
-  type list_ghost = Nil2 | Cons2 int list_ghost (ghost int)
-
-  let add_list_ghost (x: int) (l: list_ghost) : list_ghost =
-    match l with
-    | Cons2 _ Nil2 _ | Nil2 -> Cons2 x Nil2 (1+2)
-    | Cons2 _ _ n -> Cons2 x l (n+1)
-    end
-
-  let ggg () : int = 42
-
-  let call (x:int) : int =
-    ggg () + 42
-
-  let test_filter_ghost_args (x: int) (ghost y: int) : int =
-    x + 42
-
-  let test_filter_ghost_args2 (x: int) (ghost y: int) (z: int) : int =
-    x + z
-
-  let test_filter_ghost_args3 (ghost y: int) : int =
-    42
-
-  let test_call (x: int) : int =
-    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
-
-  let foo (x: int) : int =
-    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 test_lets (x: int) : int =
-    let y = x in
-    let z = y + 1 in
-    let yxz = y * x * z in
-    let xzy = x + z + y in
-    let res = yxz - xzy in
-    res
-
-  let test_partial2 (x: int) : int =
-    let sum : int -> int -> int = fun x y -> x + y in
-    let incr_a (a: int) = sum a in
-    incr_a x x
-
-  let constr_partial (x: int) : list int =
-    let x = Cons 42 in
-    x Nil
+(*   let update (c: cursor int) : int *)
+(*   = c.index *)
+
+(*   exception Empty (list int, int) *)
+(*   exception Out_of_bounds int *)
+
+(*   (\* exception are unary constructors *\) *)
+(* (\* *)
+(*   let raise1 () = *)
+(*     raises { Empty -> true } *)
+(*     raise (Empty (Nil, 0)) *)
+(*   let raise2 () = *)
+(*     raises { Empty -> true } *)
+(*     let p = (Nil, 0) in *)
+(*     raise (Empty p) *)
+(* *\) *)
+
+(*   let rec length (l: list 'a) : int *)
+(*     variant  { l } *)
+(*   = match l with *)
+(*     | Nil -> 0 *)
+(*     | Cons _ r -> 1 + length r *)
+(*     end *)
+
+(*   let t (x:int) : int *)
+(*     requires { false } *)
+(*   = absurd *)
+
+(*   let a () : unit *)
+(*   = assert { true } *)
+
+(*   let singleton (x: int) (l: list int) : list int = *)
+(*     let x = Nil in x *)
+
+(* (\* FIXME constructors in Why3 can be partially applied *)
+(*          => an eta-expansion is needed *)
+(*          be careful with side-effects *)
+(*          "let c = Cons e in" should be translated to *)
+(*          "let c = let o = e in fun x -> Cons (o, x) in ..." in OCaml *)
+
+(*    Mário: I think A-normal form takes care of the side-effects problem *)
+(* *\) *)
+(*   let constructor1 () = *)
+(*     let x = Cons in *)
+(*     x 42 *)
+
+(*   let foofoo (x: int) : int = *)
+(*     let ghost y = x + 1 in *)
+(*     x *)
+
+(*   let test (x: int) : int = *)
+(*     let y = *)
+(*       let z = x in *)
+(*       (ghost z) + 1 *)
+(*     in 42 *)
+
+(*   type list_ghost = Nil2 | Cons2 int list_ghost (ghost int) *)
+
+(*   let add_list_ghost (x: int) (l: list_ghost) : list_ghost = *)
+(*     match l with *)
+(*     | Cons2 _ Nil2 _ | Nil2 -> Cons2 x Nil2 (1+2) *)
+(*     | Cons2 _ _ n -> Cons2 x l (n+1) *)
+(*     end *)
+
+(*   let ggg () : int = 42 *)
+
+(*   let call (x:int) : int = *)
+(*     ggg () + 42 *)
+
+(*   let test_filter_ghost_args (x: int) (ghost y: int) : int = *)
+(*     x + 42 *)
+
+(*   let test_filter_ghost_args2 (x: int) (ghost y: int) (z: int) : int = *)
+(*     x + z *)
+
+(*   let test_filter_ghost_args3 (ghost y: int) : int = *)
+(*     42 *)
+
+(*   let test_call (x: int) : int = *)
+(*     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 *)
+
+(*   let foo (x: int) : int = *)
+(*     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 test_lets (x: int) : int = *)
+(*     let y = x in *)
+(*     let z = y + 1 in *)
+(*     let yxz = y * x * z in *)
+(*     let xzy = x + z + y in *)
+(*     let res = yxz - xzy in *)
+(*     res *)
+
+(*   let test_partial2 (x: int) : int = *)
+(*     let sum : int -> int -> int = fun x y -> x + y in *)
+(*     let incr_a (a: int) = sum a in *)
+(*     incr_a x x *)
+
+(*   let constr_partial (x: int) : list int = *)
+(*     let x = Cons 42 in *)
+(*     x Nil *)
 
   (* let filter_record (c: cursor 'a) : int = *)
   (*   match c with *)