OCaml extraction: preludes

parent e16c5897
......@@ -5,7 +5,7 @@
printer "ocaml"
theory BuiltIn
syntax type int "Why3__BigInt.t"
syntax type int "Why3extract.Why3__BigInt.t"
syntax predicate (=) "(%1 = %2)"
end
......@@ -14,6 +14,7 @@ import "ocaml-no-arith.drv"
(* int *)
theory int.Int
prelude "open Why3extract"
syntax constant zero "Why3__BigInt.zero"
syntax constant one "Why3__BigInt.one"
......@@ -29,38 +30,46 @@ theory int.Int
end
theory int.Abs
prelude "open Why3extract"
syntax function abs "(Why3__BigInt.abs %1)"
end
theory int.MinMax
prelude "open Why3extract"
syntax function min "(Why3__BigInt.min %1 %2)"
syntax function max "(Why3__BigInt.max %1 %2)"
end
theory int.Lex2
prelude "open Why3extract"
syntax predicate lt_nat "(Why3__BigInt.lt_nat %1 %2)"
syntax predicate lex "(Why3__BigInt.lex %1 %2)"
end
theory int.EuclideanDivision
prelude "open Why3extract"
syntax function div "(Why3__BigInt.euclidean_div %1 %2)"
syntax function mod "(Why3__BigInt.euclidean_mod %1 %2)"
end
theory int.ComputerDivision
prelude "open Why3extract"
syntax function div "(Why3__BigInt.computer_div %1 %2)"
syntax function mod "(Why3__BigInt.computer_mod %1 %2)"
end
theory int.Power
prelude "open Why3extract"
syntax function power "(Why3__BigInt.power %1 %2)"
end
theory int.Fact
prelude "open Why3extract"
syntax function fact "(Why3__IntAux.fact %1)"
end
theory int.Fibonacci
prelude "open Why3extract"
syntax function fib "(Why3__IntAux.fib %1)"
end
......@@ -69,6 +78,7 @@ end
(* WhyML *)
module stack.Stack
prelude "open Why3extract"
syntax type t "(%1 Stack.t)"
syntax val create "Stack.create"
syntax val push "Stack.push"
......@@ -84,6 +94,7 @@ module stack.Stack
end
module queue.Queue
prelude "open Why3extract"
syntax type t "(%1 Queue.t)"
syntax val create "Queue.create"
syntax val push "Queue.push"
......@@ -100,6 +111,7 @@ module queue.Queue
end
module array.Array
prelude "open Why3extract"
syntax type array "(%1 Why3__Array.t)"
syntax function ([]) "(Why3__Array.get %1 %2)"
......@@ -120,6 +132,7 @@ module array.Array
end
module matrix.Matrix
prelude "open Why3extract"
syntax type matrix "(%1 Why3__Matrix.t)"
syntax function get "(Why3__Matrix.get %1 %2)"
......@@ -137,16 +150,17 @@ module matrix.Matrix
end
module mach.int.Int
prelude "open Why3extract"
syntax val ( / ) "Why3__BigInt.computer_div"
syntax val ( % ) "Why3__BigInt.computer_mod"
end
module mach.int.Int31
(* even on a 64-bit machine, it is safe to use type int for 31-bit integers *)
syntax val of_int "Why3__BigInt.to_int"
syntax val of_int "Why3extract.Why3__BigInt.to_int"
syntax converter of_int "%1"
syntax function to_int "(Why3__BigInt.of_int %1)"
syntax function to_int "(Why3extract.Why3__BigInt.of_int %1)"
syntax type int31 "int"
syntax val ( + ) "( + )"
......@@ -165,6 +179,7 @@ end
module mach.int.UInt64
(* no OCaml library for unsigned 64-bit integers => we use BigInt *)
prelude "open Why3extract"
syntax val of_int "(fun x -> x)"
syntax converter of_int "(Why3__BigInt.of_string \"%1\")"
......@@ -202,6 +217,7 @@ end
module string.Char
prelude "open Why3extract"
syntax type char "Pervasives.char"
syntax val chr "Why3__BigInt.chr"
syntax val code "Why3__BigInt.code"
......@@ -211,13 +227,13 @@ end
module io.StdIO
prelude "open Why3extract"
syntax val print_char "Pervasives.print_char"
syntax val print_int "Why3__BigInt.print"
syntax val print_newline "Pervasives.print_newline"
end
module random.Random
prelude "open Why3extract"
syntax val random_int "Why3__BigInt.random_int"
end
......@@ -47,32 +47,26 @@ theory int.MinMax
syntax function max "(Pervasives.max %1 %2)"
end
(* FIXME
theory int.Lex2
syntax predicate lt_nat "(Why3__BigInt.lt_nat %1 %2)"
syntax predicate lex "(Why3__BigInt.lex %1 %2)"
end
theory int.EuclideanDivision
syntax function div "(Why3__BigInt.euclidean_div %1 %2)"
syntax function mod "(Why3__BigInt.euclidean_mod %1 %2)"
end
(* TODO
- int.EuclideanDivision
- number.Gcd
*)
theory int.Power
syntax function power "(Why3__BigInt.power %1 %2)"
prelude "let rec power x n = if n = 0 then 1 else x * power x (n-1)"
syntax function power "(power %1 %2)"
end
theory int.Fact
syntax function fact "(Why3__IntAux.fact %1)"
prelude "let rec fact n = if n <= 1 then 1 else n * fact (n-1)"
syntax function fact "(fact %1)"
end
theory int.Fibonacci
syntax function fib "(Why3__IntAux.fib %1)"
prelude "let rec fib n = if n <= 1 then n else fib (n-2) + fib (n-1)"
syntax function fib "(fib %1)"
end
TODO number.Gcd
*)
(* WhyML *)
module stack.Stack
......@@ -243,24 +237,3 @@ module mach.matrix.Matrix63
syntax val copy "(Array.map Array.copy)"
end
(* TODO
module string.Char
syntax type char "Pervasives.char"
syntax val chr "Why3__BigInt.chr"
syntax val code "Why3__BigInt.code"
syntax function uppercase "Char.uppercase"
syntax function lowercase "Char.lowercase"
end
module io.StdIO
syntax val print_char "Pervasives.print_char"
syntax val print_int "Why3__BigInt.print"
syntax val print_newline "Pervasives.print_newline"
end
module random.Random
syntax val random_int "Why3__BigInt.random_int"
end
*)
......@@ -15,10 +15,10 @@ import "ocaml-gen.drv"
end*)
module mach.int.Int32
syntax val of_int "Why3__BigInt.to_int32"
syntax val of_int "Why3extract.Why3__BigInt.to_int32"
syntax converter of_int "%1l"
syntax function to_int "(Why3__BigInt.of_int32 %1)"
syntax function to_int "(Why3extract.Why3__BigInt.of_int32 %1)"
syntax type int32 "Int32.t"
syntax val (+) "Int32.add"
......@@ -39,10 +39,10 @@ module mach.int.Int32
end
module mach.int.UInt32
syntax val of_int "Why3__BigInt.to_int64"
syntax val of_int "Why3extract.Why3__BigInt.to_int64"
syntax converter of_int "%1L"
syntax function to_int "(Why3__BigInt.of_int64 %1)"
syntax function to_int "(Why3extract.Why3__BigInt.of_int64 %1)"
syntax constant zero_unsigned "0L"
syntax type uint32 "Int64.t"
......@@ -78,10 +78,10 @@ module mach.int.UInt32
end
module mach.int.Int63
syntax val of_int "Why3__BigInt.to_int64"
syntax val of_int "Why3extract.Why3__BigInt.to_int64"
syntax converter of_int "%1L"
syntax function to_int "(Why3__BigInt.of_int64 %1)"
syntax function to_int "(Why3extract.Why3__BigInt.of_int64 %1)"
syntax type int63 "Int64.t"
syntax val (+) "Int64.add"
......@@ -99,10 +99,10 @@ module mach.int.Int63
end
module mach.int.Int64
syntax val of_int "Why3__BigInt.to_int64"
syntax val of_int "Why3extract.Why3__BigInt.to_int64"
syntax converter of_int "%1L"
syntax function to_int "(Why3__BigInt.of_int64 %1)"
syntax function to_int "(Why3extract.Why3__BigInt.of_int64 %1)"
syntax type int64 "Int64.t"
syntax val (+) "Int64.add"
......
......@@ -6,10 +6,10 @@ import "ocaml-gen.drv"
(** Machine arithmetic *)
module mach.int.Int32
syntax val of_int "Why3__BigInt.to_int"
syntax val of_int "Why3extract.Why3__BigInt.to_int"
syntax converter of_int "%1"
syntax function to_int "(Why3__BigInt.of_int %1)"
syntax function to_int "(Why3extract.Why3__BigInt.of_int %1)"
syntax type int32 "int"
syntax val ( + ) "( + )"
......@@ -27,10 +27,10 @@ module mach.int.Int32
end
module mach.int.UInt32
syntax val of_int "Why3__BigInt.to_int"
syntax val of_int "Why3extract.Why3__BigInt.to_int"
syntax converter of_int "%1"
syntax function to_int "(Why3__BigInt.of_int %1)"
syntax function to_int "(Why3extract.Why3__BigInt.of_int %1)"
syntax constant zero_unsigned "0"
syntax type uint32 "int"
......@@ -63,10 +63,10 @@ module mach.int.UInt32
end
module mach.int.Int63
syntax val of_int "Why3__BigInt.to_int"
syntax val of_int "Why3extract.Why3__BigInt.to_int"
syntax converter of_int "%1"
syntax function to_int "(Why3__BigInt.of_int %1)"
syntax function to_int "(Why3extract.Why3__BigInt.of_int %1)"
syntax type int63 "int"
syntax val ( + ) "( + )"
......@@ -98,10 +98,10 @@ module mach.int.MinMax63
end
module mach.int.Int64
syntax val of_int "Why3__BigInt.to_int64"
syntax val of_int "Why3extract.Why3__BigInt.to_int64"
syntax converter of_int "%1L"
syntax function to_int "(Why3__BigInt.of_int64 %1)"
syntax function to_int "(Why3extract.Why3__BigInt.of_int64 %1)"
syntax type int64 "Int64.t"
syntax val (+) "Int64.add"
......@@ -120,7 +120,7 @@ end
module mach.peano.Peano
syntax type t "int"
syntax val to_int "Why3__BigInt.of_int"
syntax val to_int "Why3extract.Why3__BigInt.of_int"
syntax val zero "(fun _ -> 0)"
syntax val succ "succ"
syntax val pred "pred"
......@@ -135,7 +135,7 @@ module mach.peano.Peano
syntax val add "(fun x y _ _ -> x+y)"
syntax val sub "(fun x y _ _ -> x-y)"
syntax val mul "(fun x y _ _ -> x*y)"
syntax val of_int "(fun n _ _ -> Why3__BigInt.to_int n)"
syntax val of_int "(fun n _ _ -> Why3extract.Why3__BigInt.to_int n)"
syntax val div "(/)"
syntax val mod "(mod)"
syntax val max "max"
......@@ -144,7 +144,7 @@ end
module mach.onetime.OneTime
syntax type t "int"
syntax val to_int "Why3__BigInt.of_int"
syntax val to_int "Why3extract.Why3__BigInt.of_int"
syntax val zero "(fun _ -> 0)"
syntax val succ "succ"
syntax val pred "pred"
......
......@@ -29,8 +29,6 @@
- ghost code
remove it as much as possible (in types and function arguments)
- preludes
*)
open Format
......@@ -351,7 +349,8 @@ module Translate = struct
ML.etuple (List.map (term info) tl)
| Tapp (fs, [t1; t2]) when not info.unsafe_int
&& ls_equal fs ps_equ && oty_equal t1.t_ty oty_int ->
ML.Esyntax ("(Why3__BigInt.eq %1 %2)", [term info t1; term info t2])
ML.Esyntax ("(Why3extract.Why3__BigInt.eq %1 %2)",
[term info t1; term info t2])
| Tapp (fs, tl) ->
begin match query_syntax info.info_syn fs.ls_name with
| Some s -> ML.Esyntax (s, List.map (term info) tl)
......@@ -852,15 +851,16 @@ module Print = struct
let print_const ~paren fmt c =
let n = Number.compute_int c in
if BigInt.eq n BigInt.zero then
fprintf fmt "Why3__BigInt.zero"
fprintf fmt "Why3extract.Why3__BigInt.zero"
else if BigInt.eq n BigInt.one then
fprintf fmt "Why3__BigInt.one"
fprintf fmt "Why3extract.Why3__BigInt.one"
else if BigInt.le min_int31 n && BigInt.le n max_int31 then
let m = BigInt.to_int n in
fprintf fmt (protect_on paren "Why3__BigInt.of_int %d") m
fprintf fmt (protect_on paren "Why3extract.Why3__BigInt.of_int %d") m
else
let s = BigInt.to_string n in
fprintf fmt (protect_on paren "Why3__BigInt.of_string \"%s\"") s
fprintf fmt
(protect_on paren "Why3extract.Why3__BigInt.of_string \"%s\"") s
let print_binop fmt = function
| Band -> fprintf fmt "&&"
......@@ -952,7 +952,7 @@ module Print = struct
(print_expr info) e1
| Efor (x, vfrom, dir, vto, e1) ->
fprintf fmt
"@[<hov 2>(Why3__IntAux.for_loop_%s %a %a@ (fun %a ->@ %a))@]"
"@[<hov 2>(Why3extract.Why3__IntAux.for_loop_%s %a %a@ (fun %a ->@ %a))@]"
(if dir = To then "to" else "downto")
(print_lident info) vfrom (print_lident info) vto
(print_lident info) x (print_expr info) e1
......@@ -1045,6 +1045,14 @@ let extract_filename ?fname th =
let unsafe_int drv =
drv.Mlw_driver.drv_printer = Some "ocaml-unsafe-int"
let print_preludes used fmt pm =
(* we do not print the same prelude twice *)
let ht = Hstr.create 5 in
let add l s = if Hstr.mem ht s then l else (Hstr.add ht s (); s :: l) in
let l = Sid.fold
(fun id l -> List.fold_left add l (Mid.find_def [] id pm)) used [] in
print_prelude fmt l
let extract_theory drv ?old ?fname fmt th =
ignore (old); ignore (fname);
let info = {
......@@ -1061,7 +1069,9 @@ let extract_theory drv ?old ?fname fmt th =
fprintf fmt
"(* This file has been generated from Why3 theory %a *)@\n@\n"
Print.print_theory_name th;
if not info.unsafe_int then fprintf fmt "open Why3extract@\n@\n";
print_prelude fmt drv.Mlw_driver.drv_prelude;
print_preludes th.th_used fmt drv.Mlw_driver.drv_thprelude;
fprintf fmt "@\n";
print_list nothing (Print.print_decl info) fmt decls;
fprintf fmt "@."
......@@ -1085,7 +1095,10 @@ let extract_module drv ?old ?fname fmt m =
fprintf fmt
"(* This file has been generated from Why3 module %a *)@\n@\n"
Print.print_module_name m;
if not info.unsafe_int then fprintf fmt "open Why3extract@\n@\n";
print_prelude fmt drv.Mlw_driver.drv_prelude;
let used = Sid.union m.mod_used m.mod_theory.th_used in
print_preludes used fmt drv.Mlw_driver.drv_thprelude;
fprintf fmt "@\n";
print_list nothing (Print.print_decl info) fmt decls;
print_list nothing (Print.print_decl info) fmt mdecls;
fprintf fmt "@."
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment