Fixed extraction

kernel/uint63.mli

@@ -50,3 +50,8 @@ val compare : t -> t -> int
 val head0   : t -> t
 val tail0   : t -> t
 
+val foldi_cont :
+  (t -> ('a -> 'b) -> 'a -> 'b) -> t -> t -> ('a -> 'b) -> 'a -> 'b
+val foldi_down_cont :
+  (t -> ('a -> 'b) -> 'a -> 'b) -> t -> t -> ('a -> 'b) -> 'a -> 'b
+val print_uint : t -> t

kernel/uint63_amd64.ml

@@ -181,3 +181,19 @@ let tail0 x =
   if !x land 0x3 = 0    then (x := !x lsr 2;  r := !r + 2);
   if !x land 0x1 = 0    then (                r := !r + 1);
   !r
+
+let rec foldi_cont f min max cont a =
+  if lt min max then f min (foldi_cont f (add min 1) max cont) a
+  else if min = max then f min cont a 
+  else cont a 
+
+let rec foldi_down_cont f max min cont a =
+  if lt min max then
+    f max (foldi_down_cont f (sub max 1) min cont) a
+  else if min = max then f min cont a
+  else cont a
+
+let print_uint x =
+  Printf.fprintf stderr "%s" (to_string x);
+  flush stderr;
+  x

kernel/uint63_x86.ml

@@ -115,3 +115,19 @@ let tail0 x =
   if Int64.logand !x 0x3L = 0L    then (x := Int64.shift_right !x 2;  r := !r + 2);
   if Int64.logand !x 0x1L = 0L    then (                r := !r + 1);
   Int64.of_int !r
+
+let rec foldi_cont f min max cont a =
+  if lt min max then f min (foldi_cont f (add min 1) max cont) a
+  else if min = max then f min cont a 
+  else cont a 
+
+let rec foldi_down_cont f max min cont a =
+  if lt min max then
+    f max (foldi_down_cont f (sub max 1) min cont) a
+  else if min = max then f min cont a
+  else cont a
+
+let print_uint x =
+  Printf.fprintf stderr "%s" (to_string x);
+  flush stderr;
+  x

plugins/extraction/ExtractNative.v

@@ -0,0 +1,53 @@
+Require Import Int63.
+Require Import PArray.
+
+Extract Inductive bool => "bool" ["true" "false"].
+Extract Inductive comparison => "int" ["0" "(-1)" "1"].
+Extract Inductive prod => "(*)"  [ "(,)" ].
+Extract Inductive carry => "Uint63.carry" ["Uint63.C0" "Uint63.C1"].
+
+Extract Constant int => "Uint63.t".
+Extract Constant lsl => "Uint63.l_sl".
+Extract Constant lsr => "Uint63.l_sr".
+Extract Constant Int63Native.land => "Uint63.l_and".
+Extract Constant Int63Native.lor => "Uint63.l_or".
+Extract Constant Int63Native.lxor => "Uint63.l_xor".
+Extract Constant add => "Uint63.add".
+Extract Constant sub => "Uint63.sub". 
+Extract Constant mul => "Uint63.mul".
+Extract Constant mulc => "Uint63.mulc".
+Extract Constant div => "Uint63.div".
+Extract Constant Int63Native.mod => "Uint63.rem".
+Extract Constant eqb => "Uint63.eq".
+Extract Constant ltb => "Uint63.lt".
+Extract Constant leb => "Uint63.le".
+Extract Constant compare => "Uint63.compare".
+Extract Constant head0 => "Uint63.head0".
+Extract Constant tail0 => "Uint63.tail0".
+
+Extract Constant addc => "Uint63.addc".
+Extract Constant addcarryc => "Uint63.addcarryc".
+Extract Constant subc => "Uint63.subc".
+Extract Constant subcarryc => "Uint63.subcarryc".
+Extract Constant diveucl => "Uint63.diveucl".
+
+Extract Constant diveucl_21 => "Uint63.diveucl_21".
+Extract Constant addmuldiv => "Uint63.addmuldiv".
+
+(* Pierre que faut-il faire pour celui la *)
+(* Extract Constant eqb_correct => "Uint63.eqb_correct". *)
+Extract Constant foldi_cont => "Uint63.foldi_cont".
+Extract Constant foldi_down_cont => "Uint63.foldi_down_cont".
+Extract Constant print_int => "Uint63.print_uint".
+
+(** Extraction of Array *)
+Extract Constant array "'a" => "'a Parray.t".
+Extract Constant make => "Parray.make".
+Extract Constant get => "Parray.get".
+Extract Constant default => "Parray.default".
+Extract Constant set => "Parray.set".
+Extract Constant length => "Parray.length".
+Extract Constant copy => "Parray.copy".
+Extract Constant reroot => "Parray.reroot".
+Extract Constant init => "Parray.init".
+Extract Constant map => "Parray.map".

plugins/extraction/ocaml.ml

@@ -57,7 +57,7 @@ let keywords =
     "module"; "mutable"; "new"; "object"; "of"; "open"; "or";
     "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true";
     "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod";
-    "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ]
+    "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "int" ; "_" ; "__" ]
   Idset.empty
 
 let pp_open mp = str ("open "^ string_of_modfile mp ^"\n")

plugins/extraction/vo.itarget

@@ -1,3 +1,4 @@
+ExtractNative.vo
 ExtrOcamlBasic.vo
 ExtrOcamlIntConv.vo
 ExtrOcamlBigIntConv.vo