OCaml extraction no more uses realizations

everything is contained in the driver (ocaml.drv)
with possible references to OCaml modules contained in why3extract.cma
(currently why3__Prelude, why3__BigInt, why3__Map)

Makefile.in

@@ -63,7 +63,7 @@ HACHA = @HACHA@
 #PSVIEWER  = @PSVIEWER@
 #PDFVIEWER = @PDFVIEWER@
 
-INCLUDES = 
+INCLUDES =
 OFLAGS = -w Aer-41-44-45 -dtypes -g -I lib/why3 $(INCLUDES)
 BFLAGS = -w Aer-41-44-45 -dtypes -g -I lib/why3 $(INCLUDES)
 
@@ -1199,16 +1199,7 @@ clean::
 # Ocaml realizations
 #######################
 
-OCAMLLIBS_INT_THEORIES = Int Abs ComputerDivision Lex2 MinMax
-OCAMLLIBS_MAP_THEORIES = Map
-OCAMLLIBS_REF_MODULES = Ref Refint
-OCAMLLIBS_ARRAY_MODULES = Array
-
-OCAMLLIBS_FILES = why3__BigInt why3__BuiltIn why3__Prelude \
-	$(addprefix int__, $(OCAMLLIBS_INT_THEORIES)) \
-	$(addprefix map__, $(OCAMLLIBS_MAP_THEORIES)) \
-	$(addprefix ref__, $(OCAMLLIBS_REF_MODULES)) \
-	$(addprefix array__, $(OCAMLLIBS_ARRAY_MODULES)) 
+OCAMLLIBS_FILES = why3__BigInt why3__Prelude why3__Map
 
 OCAMLLIBS_MODULES := $(addprefix lib/ocaml/, $(OCAMLLIBS_FILES))
 
@@ -1264,13 +1255,6 @@ install_no_local_lib::
 		$(OCAMLINSTALLLIB)/why3
 
 
-update-ocaml: update-ocaml-int 
-
-update-ocaml-int: bin/why3 theories/int.why
-	# does not work: would erase existing realization :-(
-	#	for f in $(OCAMLLIBS_INT_THEORIES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ -E ocaml -L modules -L theories -T int.$$f -o lib/ocaml; done
-
-
 
 ################
 # Jessie3 plugin

drivers/ocaml.drv

@@ -2,6 +2,7 @@
 printer "ocaml"
 
 theory BuiltIn
+  syntax type int "Why3__BigInt.t"
   syntax predicate  (=)   "(%1 = %2)"
 end
 
@@ -31,6 +32,45 @@ theory bool.Bool
   (* syntax function implb "(implb %1)" *)
 end
 
+theory int.Int
+  syntax constant zero "Why3__BigInt.zero"
+  syntax constant one  "Why3__BigInt.one"
+
+  syntax predicate (<)  "(Why3__BigInt.lt %1 %2)"
+  syntax predicate (<=) "(Why3__BigInt.le %1 %2)"
+  syntax predicate (>)  "(Why3__BigInt.gt %1 %2)"
+  syntax predicate (>=) "(Why3__BigInt.ge %1 %2)"
+
+  syntax function (+)   "(Why3__BigInt.add %1 %2)"
+  syntax function (-)   "(Why3__BigInt.sub %1 %2)"
+  syntax function ( * ) "(Why3__BigInt.mul %1 %2)"
+  syntax function (-_)  "(Why3__BigInt.minus %1)"
+end
+
+theory int.Abs
+  syntax function abs "(Why3__BigInt.abs %1)"
+end
+
+theory int.MinMax
+  syntax function min "(Why3__BigInt.min %1 %2)"
+  syntax function max "(Why3__BigInt.max %1 %2)"
+end
+
+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
+
+theory int.ComputerDivision
+  syntax function div "(Why3__BigInt.computer_div %1 %2)"
+  syntax function mod "(Why3__BigInt.computer_mod %1 %2)"
+end
+
 theory list.List
   syntax type     list "%1 list"
   syntax function Nil  "[]"
@@ -49,7 +89,14 @@ theory list.Reverse
   syntax function reverse "(List.rev %1)"
 end
 
-
+theory map.Map
+  syntax type map "((%1, %2) Why3__Map.map)"
+  syntax function const "(Why3__Map.const %1)"
+  syntax function ([]) "(Why3__Map.get %1 %2)"
+  syntax function get "(Why3__Map.get %1 %2)"
+  syntax function ([<-]) "(Why3__Map.set %1 %2 %3)"
+  syntax function set "(Why3__Map.set %1 %2 %3)"
+end
 
 (* WhyML *)
 
@@ -61,6 +108,31 @@ module ref.Ref
   syntax val      (:=)     "Pervasives.(:=)"
 end
 
+module ref.Refint
+  syntax val incr "Why3__BigInt.incr"
+  syntax val decr "Why3__BigInt.decr"
+  syntax val ( += ) "Why3__BigInt.(+=)"
+  syntax val ( -= ) "Why3__BigInt.(-=)"
+  syntax val ( *= ) "Why3__BigInt.(*=)"
+end
+
+module array.Array
+  syntax type array "(%1 Why3__BigInt.Array.t)"
+  syntax function ([]) "(Why3__BigInt.Array.get %1 %2)"
+  syntax val ([]) "Why3__BigInt.Array.get"
+  syntax val ([]<-) "Why3__BigInt.Array.set"
+  syntax val length "Why3__BigInt.Array.length"
+  syntax exception OutOfBounds "Why3__BigInt.Array.OutOfBounds"
+  syntax val defensive_get "Why3__BigInt.Array.defensive_get"
+  syntax val defensive_set "Why3__BigInt.Array.defensive_set"
+  syntax val make "Why3__BigInt.Array.make"
+  syntax val append "Why3__BigInt.Array.append"
+  syntax val sub "Why3__BigInt.Array.sub"
+  syntax val copy "Why3__BigInt.Array.copy"
+  syntax val fill "Why3__BigInt.Array.fill"
+  syntax val blit "Why3__BigInt.Array.blit"
+end
+
 module mach.int.Int31
   (* even on a 64-bit machine, it is safe to use type int for 31-bit integers *)
   syntax type     int31     "int"

examples/euler001/main.ml

@@ -13,7 +13,7 @@ let input =
 
 let input_num =
   try
-    Why3__BuiltIn.int_constant input
+    Why3__BigInt.of_string input
   with _ -> usage ()
 
 let () =

lib/ocaml/array__Array.ml

-(* This file has been generated from Why3 module array.Array *)
-
-module BigInt = Why3__BigInt
-
-type 'a pervasives_array = 'a array
-type 'a array = 'a pervasives_array
-
-let mixfix_lbrb (a: 'a array) (i: Why3__BuiltIn.int) : 'a =
-  a.(BigInt.to_int i)
-
-let mixfix_lbrblsmn (a: 'a array) (i: Why3__BuiltIn.int) (v: 'a) : unit =
-  a.(BigInt.to_int i) <- v
-
-let length (a: 'a array) : Why3__BuiltIn.int =
-  BigInt.of_int (Array.length a)
-
-exception OutOfBounds
-
-let defensive_get (a: 'a array) (i: Why3__BuiltIn.int) =
-  begin if let o = (let o1 = (length a) in
-             (Int__Int.infix_gteq i o1)) in
-        (Int__Int.infix_ls i (Why3__BuiltIn.int_constant "0") || (o = true))
-        then raise OutOfBounds
-        else (());
-  ((mixfix_lbrb a) i) end
-
-let defensive_set (a1: 'a array) (i1: Why3__BuiltIn.int) (v: 'a) =
-  begin if let o = (let o1 = (length a1) in
-             (Int__Int.infix_gteq i1 o1)) in
-        (Int__Int.infix_ls i1 (Why3__BuiltIn.int_constant "0") || (o = true))
-        then raise OutOfBounds
-        else (());
-  (((mixfix_lbrblsmn a1) i1) v) end
-
-let make (n: Why3__BuiltIn.int) (v1: 'a) : 'a array =
-  Array.make (BigInt.to_int n) v1
-
-
-
-let append (a11: 'a array) (a2: 'a array) : 'a array =
-  Array.append a11 a2
-
-
-
-let sub (a2: 'a array) (ofs: Why3__BuiltIn.int) (len: Why3__BuiltIn.int)
-    : 'a array =
-  Array.sub a2 (BigInt.to_int ofs) (BigInt.to_int len)
-
-
-
-let copy (a2: 'a array) : 'a array =
-  Array.copy a2
-
-
-let fill (a2: 'a array) (ofs: Why3__BuiltIn.int) (len: Why3__BuiltIn.int)
-  (v1: 'a) =
-  let o = (Int__Int.infix_mn len (Why3__BuiltIn.int_constant "1")) in
-  let o1 = ((Why3__BuiltIn.int_constant "0")) in
-  (Int__Int.for_loop_to o1 o
-    (fun k -> let o2 = (Int__Int.infix_pl ofs k) in
-    (((mixfix_lbrblsmn a2) o2) v1)))
-
-let blit (a11: 'a array) (ofs1: Why3__BuiltIn.int) (a21: 'a array) (ofs2:
-  Why3__BuiltIn.int) (len1: Why3__BuiltIn.int) : unit =
-  Array.blit a11 (BigInt.to_int ofs1)
-             a21 (BigInt.to_int ofs2) (BigInt.to_int len1)
-
-
-
-

lib/ocaml/bigInt_zarith.ml

@@ -27,6 +27,8 @@ let gt = gt_big_int
 let le = le_big_int
 let ge = ge_big_int
 
+let lt_nat x y = le zero y && lt x y
+let lex (x1,x2) (y1,y2) = lt x1 y1 || eq x1 y1 && lt x2 y2
 
 let euclidean_div_mod = quomod_big_int
 
@@ -38,7 +40,7 @@ let computer_div_mod x y =
   let q,r = quomod_big_int x y in
   (* we have x = q*y + r with 0 <= r < |y| *)
   if sign x < 0 then
-    if sign y < 0 
+    if sign y < 0
     then (pred q, add r y)
     else (succ q, sub r y)
   else (q,r)
@@ -56,3 +58,41 @@ let pow_int_pos = power_int_positive_int
 let to_string = string_of_big_int
 let of_string = big_int_of_string
 let to_int = int_of_big_int
+
+(* the code below is to be used in OCaml extracted code (see ocaml.drv) *)
+
+let rec for_loop_to x1 x2 body =
+  if le x1 x2 then begin
+    body x1;
+    for_loop_to (succ x1) x2 body
+  end
+
+let rec for_loop_downto x1 x2 body =
+  if ge x1 x2 then begin
+    body x1;
+    for_loop_downto (pred x1) x2 body
+  end
+
+let incr r = r := succ !r
+let decr r = r := pred !r
+let ( += ) r v = r := add !r v
+let ( -= ) r v = r := sub !r v
+let ( *= ) r v = r := mul !r v
+
+module Array = struct
+  type 'a t = 'a array
+  let get a i = a.(to_int i)
+  let set a i v = a.(to_int i) <- v
+  let length a = of_int (Array.length a)
+  exception OutOfBounds
+  let check_bounds a i = if i < 0 || i >= Array.length a then raise OutOfBounds
+  let defensive_get a i = let i = to_int i in check_bounds a i; a.(i)
+  let defensive_set a i v = let i = to_int i in check_bounds a i; a.(i) <- v
+  let make n v = Array.make (to_int n) v
+  let append = Array.append
+  let sub a ofs len = Array.sub a (to_int ofs) (to_int len)
+  let copy = Array.copy
+  let fill a ofs len v = Array.fill a (to_int ofs) (to_int len) v
+  let blit a1 ofs1 a2 ofs2 len =
+    Array.blit a1 (to_int ofs1) a2 (to_int ofs2) (to_int len)
+end

lib/ocaml/int__Abs.ml

-(* This file has been generated from Why3 theory int.Abs *)
-
-let abs = Why3__BigInt.abs
-
-
-

lib/ocaml/int__ComputerDivision.ml

-(* This file has been generated from Why3 theory int.ComputerDivision *)
-
-module BigInt = Why3__BigInt
-
-let div = BigInt.computer_div
-
-let mod_renamed = BigInt.computer_mod

lib/ocaml/int__Int.ml

-(* This file has been generated from Why3 theory int.Int *)
-
-module BigInt = Why3__BigInt
-
-let zero  : Why3__BuiltIn.int = BigInt.zero
-
-let one  : Why3__BuiltIn.int = BigInt.one
-
-let infix_ls (x: Why3__BuiltIn.int) (x1: Why3__BuiltIn.int) : bool =
-  BigInt.lt x x1
-
-let infix_gt (x: Why3__BuiltIn.int) (y: Why3__BuiltIn.int) : bool =
-  infix_ls y x
-
-let infix_lseq (x: Why3__BuiltIn.int) (y: Why3__BuiltIn.int) : bool =
-  infix_ls x y || (x = y)
-
-let infix_pl (x: Why3__BuiltIn.int) (x1:
-  Why3__BuiltIn.int) : Why3__BuiltIn.int =
-  BigInt.add x x1
-
-let prefix_mn (x: Why3__BuiltIn.int) : Why3__BuiltIn.int =
-  BigInt.minus x
-
-let infix_as (x: Why3__BuiltIn.int) (x1:
-  Why3__BuiltIn.int) : Why3__BuiltIn.int =
-  BigInt.mul x x1
-
-let infix_mn (x: Why3__BuiltIn.int) (y:
-  Why3__BuiltIn.int) : Why3__BuiltIn.int = infix_pl x (prefix_mn y)
-
-let infix_gteq (x: Why3__BuiltIn.int) (y: Why3__BuiltIn.int) : bool =
-  infix_lseq y x
-
-let rec for_loop_to x1 x2 body =
-  if BigInt.le x1 x2 then begin
-    body x1;
-    for_loop_to (BigInt.succ x1) x2 body
-  end
-
-let rec for_loop_downto x1 x2 body =
-  if BigInt.ge x1 x2 then begin
-    body x1;
-    for_loop_downto (BigInt.pred x1) x2 body
-  end
-

lib/ocaml/int__Lex2.ml

-(* This file has been generated from Why3 theory int.Lex2 *)
-
-let lt_nat (x: Why3__BuiltIn.int) (y: Why3__BuiltIn.int) : bool =
-  Int__Int.infix_lseq (Why3__BuiltIn.int_constant "0") y &&
-  Int__Int.infix_ls x y
-
-let lex (x: (Why3__BuiltIn.int * Why3__BuiltIn.int)) (x1:
-  (Why3__BuiltIn.int * Why3__BuiltIn.int)) : bool =
-  let (fst1, snd1) = x in
-  let (fst2, snd2) = x1 in
-  Int__Int.infix_ls fst1 fst2 || fst1 = fst2 && Int__Int.infix_ls snd1 snd2
-
-
-

lib/ocaml/int__MinMax.ml

-(* This file has been generated from Why3 theory int.MinMax *)
-
-let min = Why3__BigInt.min
-let max = Why3__BigInt.max
-

lib/ocaml/ref__Ref.ml

-(* This file has been generated from Why3 module ref.Ref *)
-
-(* type ref is overridden by driver *)
-
-(* symbol ref is overridden by driver *)
-
-(* symbol prefix_ex is overridden by driver *)
-
-(* symbol infix_cleq is overridden by driver *)
-
-

lib/ocaml/ref__Refint.ml

-(* This file has been generated from Why3 module ref.Refint *)
-
-let incr (r: (Why3__BuiltIn.int Pervasives.ref)) =
-  let o =
-    (let o1 = (Pervasives.(!) r) in
-    (Int__Int.infix_pl o1 (Why3__BuiltIn.int_constant "1"))) in
-  ((Pervasives.(:=) r) o)
-
-let decr (r1: (Why3__BuiltIn.int Pervasives.ref)) =
-  let o =
-    (let o1 = (Pervasives.(!) r1) in
-    (Int__Int.infix_mn o1 (Why3__BuiltIn.int_constant "1"))) in
-  ((Pervasives.(:=) r1) o)
-
-let infix_pleq (r2: (Why3__BuiltIn.int Pervasives.ref))
-  (v: Why3__BuiltIn.int) =
-  let o = (let o1 = (Pervasives.(!) r2) in
-    (Int__Int.infix_pl o1 v)) in
-  ((Pervasives.(:=) r2) o)
-
-let infix_mneq (r3: (Why3__BuiltIn.int Pervasives.ref))
-  (v1: Why3__BuiltIn.int) =
-  let o = (let o1 = (Pervasives.(!) r3) in
-    (Int__Int.infix_mn o1 v1)) in
-  ((Pervasives.(:=) r3) o)
-
-let infix_aseq (r4: (Why3__BuiltIn.int Pervasives.ref))
-  (v2: Why3__BuiltIn.int) =
-  let o = (let o1 = (Pervasives.(!) r4) in
-    (Int__Int.infix_as o1 v2)) in
-  ((Pervasives.(:=) r4) o)
-
-

lib/ocaml/why3__BuiltIn.ml

-
-
-type int = Why3__BigInt.t
-
-let infix_eq = Pervasives.(=)
-
-let int_zero = Why3__BigInt.zero
-let int_one = Why3__BigInt.one
-let int_constant = Why3__BigInt.of_string
-

lib/ocaml/map__Map.ml → lib/ocaml/why3__Map.ml

-(* This file has been generated from Why3 theory Map *)
 
-type ('a, 'b) map = (* inefficient implementation *)
+(* inefficient implementation of theory map.Map
+   to be used in OCaml extracted code (see driver ocaml.drv) *)
+
+type ('a, 'b) map =
   { default : 'b;
     table : ('a * 'b) list;
   }
 
-let get (x: ('a, 'b) map) (x1: 'a) : 'b = 
+let get (x: ('a, 'b) map) (x1: 'a) : 'b =
   try
-    List.assoc x1 x.table 
+    List.assoc x1 x.table
   with Not_found -> x.default
 
 let rec update l x y =
@@ -24,7 +26,7 @@ let mixfix_lbrb (a: ('a, 'b) map) (i: 'a) : 'b = get a i
 let mixfix_lblsmnrb (a: ('a, 'b) map) (i: 'a) (v: 'b) : ('a, 'b) map =
   set a i v
 
-let const (x: 'b) : ('a, 'b) map = 
+let const (x: 'b) : ('a, 'b) map =
   { default = x ; table = [] }
 
 

src/util/bigInt.ml

@@ -37,6 +37,8 @@ let gt = gt_big_int
 let le = le_big_int
 let ge = ge_big_int
 
+let lt_nat x y = le zero y && lt x y
+let lex (x1,x2) (y1,y2) = lt x1 y1 || eq x1 y1 && lt x2 y2
 
 let euclidean_div_mod = quomod_big_int
 
@@ -67,3 +69,40 @@ let to_string = string_of_big_int
 let of_string = big_int_of_string
 let to_int = int_of_big_int
 
+(* the code below is to be used in OCaml extracted code (see ocaml.drv) *)
+
+let rec for_loop_to x1 x2 body =
+  if le x1 x2 then begin
+    body x1;
+    for_loop_to (succ x1) x2 body
+  end
+
+let rec for_loop_downto x1 x2 body =
+  if ge x1 x2 then begin
+    body x1;
+    for_loop_downto (pred x1) x2 body
+  end
+
+let incr r = r := succ !r
+let decr r = r := pred !r
+let ( += ) r v = r := add !r v
+let ( -= ) r v = r := sub !r v
+let ( *= ) r v = r := mul !r v
+
+module Array = struct
+  type 'a t = 'a array
+  let get a i = a.(to_int i)
+  let set a i v = a.(to_int i) <- v
+  let length a = of_int (Array.length a)
+  exception OutOfBounds
+  let check_bounds a i = if i < 0 || i >= Array.length a then raise OutOfBounds
+  let defensive_get a i = let i = to_int i in check_bounds a i; a.(i)
+  let defensive_set a i v = let i = to_int i in check_bounds a i; a.(i) <- v
+  let make n v = Array.make (to_int n) v
+  let append = Array.append
+  let sub a ofs len = Array.sub a (to_int ofs) (to_int len)
+  let copy = Array.copy
+  let fill a ofs len v = Array.fill a (to_int ofs) (to_int len) v
+  let blit a1 ofs1 a2 ofs2 len =
+    Array.blit a1 (to_int ofs1) a2 (to_int ofs2) (to_int len)
+end

src/util/bigInt.mli

@@ -36,6 +36,9 @@ val gt : t -> t -> bool
 val le : t -> t -> bool
 val ge : t -> t -> bool
 
+val lt_nat: t -> t -> bool
+val lex: t * t -> t * t -> bool
+
 (** Division and modulo operators with the convention
 that modulo is always non-negative.
 
@@ -65,3 +68,8 @@ val pow_int_pos : int -> int -> t
 val of_string : string -> t
 val to_string : t -> string
 val to_int : t -> int
+
+(** for loops *)
+
+val for_loop_to: t -> t -> (t -> unit) -> unit
+val for_loop_downto: t -> t -> (t -> unit) -> unit

src/whyml/mlw_ocaml.ml

@@ -335,13 +335,13 @@ let print_const ~paren fmt = function
   | ConstInt c ->
       let n = Number.compute_int c in
       if BigInt.eq n BigInt.zero then
-        fprintf fmt "Why3__BuiltIn.int_zero"
+        fprintf fmt "Why3__BigInt.zero"
       else
       if BigInt.eq n BigInt.one then
-        fprintf fmt "Why3__BuiltIn.int_one"
+        fprintf fmt "Why3__BigInt.one"
       else
       let s = BigInt.to_string n in
-      fprintf fmt (protect_on paren "Why3__BuiltIn.int_constant \"%s\"") s
+      fprintf fmt (protect_on paren "Why3__BigInt.of_string \"%s\"") s
   | ConstReal (RConstDec (i,f,None)) ->
       fprintf fmt (non_executable_fmt "%s.%s") i f
   | ConstReal (RConstDec (i,f,Some e)) ->
@@ -749,7 +749,7 @@ let rec print_expr ?(paren=false) info fmt e =
       fprintf fmt "@[<hv>while true do@;<1 2>@[%a@]@ done@]" (print_expr info) e
   | Efor (pv,(pvfrom,dir,pvto),_,e) ->
       fprintf fmt
-        "@[<hov 2>(Int__Int.for_loop_%s %a %a@ (fun %a -> %a))@]"
+        "@[<hov 2>(Why3__BigInt.for_loop_%s %a %a@ (fun %a -> %a))@]"
         (if dir = To then "to" else "downto")
         (print_pv info) pvfrom (print_pv info) pvto
         (print_pv info) pv (print_expr info) e