extraction: removed ghost arguments in functions and applications

Makefile.in

@@ -1676,7 +1676,10 @@ test-extraction: bin/why3.opt bin/why3extract.opt lib/why3/why3extract.cmxa
 	@mkdir -p tests/test-extraction-mario
 	@bin/why3extract.opt -D drivers/ocaml64.drv \
 	  tests/test_extraction_mario.mlw -o tests/test-extraction-mario/
-	@$(OCAMLOPT) -c -I lib/ocaml -I lib/why3 tests/test-extraction-mario/test_extraction_mario__M.ml
+	@cd tests/test-extraction-mario/ ; \
+	  ocamlfind ocamlopt -package zarith -linkpkg \
+	  test_extraction_mario__M.ml main.ml -o a.out
+	@tests/test-extraction-mario/a.out
 
 ################
 # documentation

drivers/ocaml64.drv

@@ -65,12 +65,14 @@ end
 *)
 
 module mach.int.Int63
-  syntax val of_int "Why3extract.Why3__BigInt.to_int"
+  syntax val of_int "Z.to_int %1"
   syntax converter of_int "%1"
 
-  syntax function to_int "(Why3extract.Why3__BigInt.of_int %1)"
+  syntax function to_int "Z.of_int %1"
 
   syntax type     int63     "int"
+  syntax constant min_int63 "min_int"
+  syntax constant max_int63 "max_int"
   syntax val      ( + )     "( + ) %1 %2"
   syntax val      ( - )     "( - ) %1 %2"
   syntax val      (-_)      "( ~- ) %1 %2"
@@ -241,4 +243,5 @@ end
 
 module ocaml.Pervasives
   syntax exception Exit "Pervasives.Exit"
+  syntax val ocaml_assert "assert (%1)"
 end
\ No newline at end of file

modules/ocaml.mlw

-module OCaml
-
-use export int.Int
-use export int.MinMax
-use export option.Option
-use export list.List
-use export seq.Seq
-
-scope Sys
-  constant max_array_length : int
-end
-
-use array.Array
-type array 'a = Array.array 'a
-
-end
 
 module Sys
 
@@ -40,4 +24,24 @@ module Pervasives
     requires { "expl:integer overflow" in_bounds (to_int x - 1) }
     ensures  { to_int result = to_int x - 1 }
 
-end
\ No newline at end of file
+  exception AssertFailure
+
+  val ocaml_assert (b: bool) : unit
+    raises { AssertFailure }
+
+end
+
+module OCaml
+
+  use export int.Int
+  use export int.MinMax
+  use export option.Option
+  use export list.List
+  use export seq.Seq
+
+  use Sys
+
+  use array.Array
+  type array 'a = Array.array 'a
+
+end

src/mlw/compile.ml

@@ -183,6 +183,8 @@ module ML = struct
 
   let mk_var id ty ghost = (id, ty, ghost)
 
+  let mk_var_unit () = id_register (id_fresh "_"), tunit, true
+
   let mk_its_defn id args private_ def =
     { its_name = id; its_args = args; its_private = private_; its_def = def; }
 
@@ -314,10 +316,6 @@ module Translate = struct
     | To -> ML.To
     | DownTo -> ML.DownTo
 
-  (* function arguments *)
-  let args = (* point-free *)
-    List.map pvty
-
   let isconstructor info rs =
     match Mid.find_opt rs.rs_name info.info_mo_known_map with
     | Some {pd_node = PDtype its} ->
@@ -346,6 +344,16 @@ module Translate = struct
     let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) eff_empty in
     filter_ghost_params pv_not_ghost def pvl
 
+  (* function arguments *)
+  let filter_params args =
+    let args = List.map pvty args in
+    let p (_, _, is_ghost) = not is_ghost in
+    List.filter p args
+
+  let params args =
+    let args = filter_params args in
+    if args = [] then [ML.mk_var_unit ()] else args
+
   (* expressions *)
   let rec expr info ({e_effect = eff} as e) =
     assert (not eff.eff_ghost);
@@ -366,38 +374,35 @@ module Translate = struct
       let ml_let = ML.ml_let_var 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 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 pv_not_ghost def al cty.cty_args in
+      let args = params cty.cty_args in
       let ef = expr info ef in
       let ein = expr info ein in
       let ml_letrec = ML.Elet (ML.Lsym (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); c_cty = cty}), ein)
       when isconstructor info rs_app ->
-
       let eta_app = make_eta_expansion rs_app pvl cty in
       let ein = expr info ein in
       let ml_letrec = ML.Elet (ML.Lsym (rsf, [], eta_app), ein) in
       ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
     | Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein) ->
+      (* partial application *)
       let pvl = app pvl in
       let eapp =
         ML.mk_expr (ML.Eapp (rs_app, pvl)) (ML.C cty) cty.cty_effect in
       let ein = expr info ein in
-      let ml_letrec = ML.Elet (ML.Lsym (rsf, [], eapp), ein) in
+      let args =
+        if filter_params cty.cty_args = [] then [ML.mk_var_unit ()] else [] in
+      let ml_letrec = ML.Elet (ML.Lsym (rsf, args, eapp), ein) in
       ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
     | Elet (LDrec rdefl, ein) ->
-      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 ein = expr info ein in
       let rdefl =
         List.map (fun rdef ->
           match rdef with
           | {rec_sym = rs1; rec_rsym = rs2;
              rec_fun = {c_node = Cfun ef; c_cty = cty}} ->
-            let args =
-              filter2_ghost_params pv_not_ghost def al cty.cty_args in
+            let args = params cty.cty_args in
             let ef = expr info ef in
             { ML.rec_sym = rs1; ML.rec_rsym = rs2;
               ML.rec_args = args; ML.rec_exp = ef }
@@ -413,9 +418,7 @@ module Translate = struct
       let pvl = app pvl in
       ML.mk_expr (ML.Eapp (rs, pvl)) (ML.I e.e_ity) eff
     | Eexec ({c_node = Cfun e; c_cty = cty}, _) ->
-      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 pv_not_ghost def al cty.cty_args in
+      let args = params cty.cty_args in
       ML.mk_expr (ML.Efun (args, expr info e)) (ML.I e.e_ity) eff
     | Eexec ({c_node = Cany}, _) ->
       (* Error message here *) assert false
@@ -507,25 +510,20 @@ module Translate = struct
     | PDlet (LDsym (rs, _)) when rs_ghost rs ->
        []
     | PDlet (LDsym (_, {c_node = Cfun e})) when is_val e ->
+      (* FIXME: check that this symbol is defined in driver *)
       []
+    | PDlet (LDsym ({rs_cty = {cty_args = []}} as rs, {c_node = Cfun e})) ->
+      [ML.Dlet (ML.Lsym (rs, [], expr info e))]
     | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
-      let args_filter =
-        let p (_, _, is_ghost) = not is_ghost in
-        let def = fun x -> x in
-        let al = fun x -> x in
-        filter2_ghost_params p def al (args cty.cty_args) in
-      [ML.Dlet (ML.Lsym (rs, args_filter, expr info e))]
+      let args = params cty.cty_args in
+      [ML.Dlet (ML.Lsym (rs, args, expr info e))]
     | PDlet (LDrec rl) ->
       let rec_def =
         List.map (fun {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} ->
           let e = match e.c_node with Cfun e -> e | _ -> assert false in
-          let args_filter =
-            let p (_, _, is_ghost) = not is_ghost in
-            let def = fun x -> x in
-            let al = fun x -> x in
-            filter2_ghost_params p def al (args rs1.rs_cty.cty_args) in
+          let args = params rs1.rs_cty.cty_args in
           { ML.rec_sym = rs1; ML.rec_rsym = rs2;
-            ML.rec_args = args_filter; ML.rec_exp = expr info e }) rl
+            ML.rec_args = args; ML.rec_exp = expr info e }) rl
       in
       [ML.Dlet (ML.Lrec rec_def)]
     | PDlet (LDsym _)

src/mlw/ocaml_printer.ml

@@ -231,12 +231,12 @@ module Print = struct
       | _ -> false in
     match query_syntax info.info_convert rs.rs_name,
           query_syntax info.info_syn rs.rs_name, pvl with
-    | Some s, _, _ ->
+    | Some s, _, [{e_node = Econst _}] ->
       let print_constant fmt e = match e.e_node with
         | Econst c ->
-          let c = BigInt.to_int (Number.compute_int c) in
-          fprintf fmt "%d" c
-        | _ -> print_expr info fmt e in
+          let s = BigInt.to_string (Number.compute_int c) in
+          fprintf fmt "%s" s
+        | _ -> assert false in
       syntax_arguments s print_constant fmt pvl
     | _, Some s, _ ->
       syntax_arguments s (print_expr info) fmt pvl

tests/test-extraction-mario/main.ml

+
+let () = Test_extraction_mario__M.main ()

tests/test_extraction_mario.mlw

 module M
 
-  use import mach.int.Int63
-
-  let f (x: int63) : int
-  = min_int63
-
   use import seq.Seq
   use import int.Int
+  use import mach.int.Int
 
   let function f_function (y: int) (x: int) : int
     requires { x >= 0 }
@@ -118,17 +114,23 @@ module M
   let call (x:int) : int =
     ggg () + 42
 
-  let test_filter_ghost_args (x: int) (ghost y: int) : int =
-    x + 42
+  (* functions with ghost arguments *)
+
+  let test_filter_ghost_args (x: int) (ghost y: int) =
+    1 / 0
+
+  let test_call (x: int) : int =
+    test_filter_ghost_args x 0 + 1
+
+  let constant test_partial : int =
+    let partial = test_filter_ghost_args 3 in
+    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
+    1 / 0
 
   let many_args (a b c d e f g h i j k l m: int) : int = 42
 
@@ -139,10 +141,6 @@ module M
   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
@@ -169,6 +167,27 @@ module M
     | { collection = l; index = i; index2 = i2; v = v} -> i
     end
 
+  (** test the execution of the extracted code *)
+
+  use import ocaml.Pervasives
+
+  let test1 () raises { AssertFailure } =
+    ocaml_assert (1 + 1 = 2)
+
+  (** machine arithmetic *)
+
+  use import mach.int.Int63
+
+  let f (x: int63) : int
+  = min_int63
+
+  let test2 () raises { AssertFailure }
+  = ocaml_assert (of_int 1 + of_int 1 = of_int 2)
+
+  let main () raises { AssertFailure } =
+    test1 ();
+    test2 ()
+
 end
 
 (*