mp: extraction to ocaml

.gitignore

@@ -226,6 +226,8 @@ pvsbin/
 /examples/vstte12_combinators/*__*.ml
 /examples/in_progress/bigInt/jsmain.js
 /examples/in_progress/bigInt/*__*.ml
+/examples/in_progress/mp/jsmain.js
+/examples/in_progress/mp/*__*.ml
 
 
 # modules

drivers/ocaml32.drv

@@ -45,6 +45,14 @@ module mach.int.UInt32
   syntax val      (<)       "(<)"
   syntax val      (>=)      "(>=)"
   syntax val      (>)       "(>)"
+
+  (* direct realization of add_with_carry.
+     Remind that parameters x y and c are assumed to denote unsigned integers
+     less than 2^{32} *)
+  syntax val      add_with_carry "(fun x y c ->
+    let r = Int64.add x (Int64.add y c) in
+    (Int64.logand r 0xFFFFFFFFL,Int64.shift_right_logical r 32))"
+
 end
 
 module mach.int.Int63

examples/in_progress/mp.mlw

@@ -20,6 +20,7 @@ module N
   these are represented by an array of "limbs". A limb is expected to
   be a machine word, abstractly it can be any unsigned integer type
   *)
+(* does not allow extraction...
   type limb
 
   clone mach.int.Unsigned as Limb
@@ -29,6 +30,21 @@ module N
 
   constant radix : int = Limb.max + 1
 
+*)
+
+(* temporary: stick to uint32 *)
+
+  use mach.int.UInt32 as Limb
+
+  type limb = Limb.uint32
+
+  axiom limb_max_bound: 1 <= Limb.max_uint32
+
+  constant radix : int = Limb.max_uint32 + 1
+
+(**)
+
+
   function l2i (x:limb) : int = Limb.to_int x
 
   function p2i (i:int31) : int = Int31.to_int i
@@ -312,7 +328,7 @@ module N
     let one = Int31.of_int 1 in
     let limb_zero = Limb.of_int 0 in
     let lx = x.length in
-    if Int31.eq lx (Int31.of_int Int31.max_int31) then raise TooManyDigits;
+    if Int31.eq lx (of_int 0x3FFFFFFF) then raise TooManyDigits;
     let r = Array31.make (Int31.(+) lx one) limb_zero in
     Array31.blit x zero r zero lx;
     assert { MapEq.map_eq_sub x.elts r.elts 0 (p2i lx) };
@@ -338,3 +354,15 @@ module N
       { digits = add_array y.digits x.digits }
 
 end
+
+
+
+(* does not work as expected
+module N64
+
+  use import mach.int.Int64
+
+  clone N with type limb = int64
+
+end
+*)
\ No newline at end of file

examples/in_progress/mp/Makefile

+
+BENCH ?= no
+
+ifeq ($(BENCH),yes)
+  WHY3=../../bin/why3
+  WHY3SHARE=../../share
+else
+  ifeq ($(BINDIR),)
+    WHY3=why3
+  else
+    WHY3=$(BINDIR)/why3
+  endif
+  WHY3SHARE=$(shell $(WHY3) --print-datadir)
+endif
+
+include $(WHY3SHARE)/Makefile.config
+
+ifeq ($(BENCH),yes)
+  INCLUDE += -I ../../lib/why3
+endif
+
+MAIN=main
+GEN=map__Map mach__int__UInt32 mp__N
+OBJ=$(GEN) parse
+
+GENML = $(addsuffix .ml, $(GEN))
+ML = $(addsuffix .ml, $(OBJ))
+CMO = $(addsuffix .cmo, $(OBJ))
+CMX = $(addsuffix .cmx, $(OBJ))
+
+OCAMLOPT=ocamlopt -noassert -inline 1000
+
+all: $(MAIN).$(OCAMLBEST)
+
+extract: $(ML)
+
+$(MAIN).byte: $(CMO)  $(MAIN).cmo
+	ocamlc $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -g -o $@ $^
+
+$(MAIN).opt: $(CMX)  $(MAIN).cmx
+	$(OCAMLOPT) $(INCLUDE) $(BIGINTLIB).cmxa why3extract.cmxa -o $@ $^
+
+$(MAIN).cmx: $(CMX)
+
+$(ML): ../mp.mlw
+	$(WHY3) -E ocaml32 $< -o .
+
+%.cmx: %.ml
+	$(OCAMLOPT) $(INCLUDE) -annot -c $<
+
+%.cmo: %.ml
+	ocamlc -g $(INCLUDE) -annot -c $<
+
+%.cmi: %.mli
+	ocamlc -g $(INCLUDE) -annot -c $<
+
+clean::
+	rm -f $(GENML) *.cm[xio] *.o *.annot $(MAIN).opt $(MAIN).byte
+	rm -f why3__*.ml* mp__*.ml* int__*.ml*
+
+
+# javascript
+
+
+JSMAIN=jsmain
+
+JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
+          -syntax camlp4o
+
+$(JSMAIN).js: $(JSMAIN).byte 
+	js_of_ocaml -pretty -noinline $(JSMAIN).byte
+
+
+$(JSMAIN).byte: $(ML) jsmain.ml
+	$(JSOCAMLC) $(INCLUDE) -o $@ -linkpkg $^
+
+
+%.cmo: %.ml
+	$(JSOCAMLC) $(INCLUDE) -g -annot -c $<
+
+%.cmi: %.mli
+	$(JSOCAMLC) $(INCLUDE) -g -annot -c $<
+

examples/in_progress/mp/main.ml

+
+open Why3extract
+open Format
+
+let usage () =
+  eprintf "Usage: %s <decimal number>@." Sys.argv.(0);
+  exit 2
+
+let input =
+  if Array.length Sys.argv <> 2 then usage ();
+  Sys.argv.(1)
+
+open Mp__N
+
+let input_num =
+  try let a,i = Parse.parse_dec input 0 in a
+  with Parse.SyntaxError -> usage ()
+
+let () =
+  Format.printf "zero   : %a@." Parse.pr (zero ());
+  Format.printf "one    : %a@." Parse.pr (from_limb 1L);
+  Format.printf "2^{32} : %a@." Parse.pr (from_limb 0x100000000L);
+  Format.printf "input  : %a@." Parse.pr input_num;
+  let a = add input_num input_num in
+  Format.printf "times 2: %a@." Parse.pr a;
+  let a = add a input_num in
+  Format.printf "times 3: %a@." Parse.pr a

examples/in_progress/mp/parse.ml

+
+open Mp__N
+
+let n__add = Mp__N.add
+let n__zero = Mp__N.zero
+let n__from_limb = Mp__N.from_limb
+
+exception SyntaxError
+
+let times10 a =
+  let a2 = n__add a a in
+  let a4 = n__add a2 a2 in
+  let a5 = n__add a4 a in
+  n__add a5 a5
+
+let parse_dec s idx =
+  let a = ref (n__zero ()) in
+  let i = ref idx in
+  try
+  while !i < String.length s do
+    match String.get s !i with
+      | '0'..'9' as c ->
+        let d = Int64.of_int (Char.code c - Char.code '0') in
+        a := n__add (times10 !a) (n__from_limb d);
+        i := succ !i
+      | _ ->
+        raise Exit
+  done;
+  raise Exit
+  with Exit ->
+    if !i = idx then raise SyntaxError else !a,!i
+
+let parse_sep_star s idx =
+  let i = ref idx in
+  try
+  while !i < String.length s do
+    match String.get s !i with
+      | ' ' | '\t' | '\n' | '\r' -> i := succ !i
+      | _ -> raise Exit
+  done;
+  raise Exit
+  with Exit -> !i
+
+open Format
+
+let pr fmt a =
+  let a = a.digits in
+  let l = Array.length a in
+  for i=l-1 downto 0 do
+    fprintf fmt "|%016LX" a.(i);
+  done;
+  fprintf fmt "|"
+