Integration of Jacques-Henri Jourdan's verified parser.

(Merge of branch newparser.)


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 50 insertions, 0 deletions

diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index c580e21..8d6fd24 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -324,3 +324,53 @@ let coqfloat_of_camlfloat f =
 let camlfloat_of_coqfloat f =
   Int64.float_of_bits(camlint64_of_coqint(Float.bits_of_double f))
 
+(* Int31 *)
+
+module Int31 = struct
+
+(*
+let constr (b30,b29,b28,b27,b26,b25,b24,
+            b23,b22,b21,b20,b19,b18,b17,b16,
+            b15,b14,b13,b12,b11,b10,b9,b8,
+            b7,b6,b5,b4,b3,b2,b1,b0) =
+  let f i b accu = if b then accu + (1 lsl i) else accu in
+  f 30 b30 (f 29 b29 (f 28 b28 (f 27 b27 (f 26 b26 (f 25 b25 (f 24 b24
+  (f 23 b23 (f 22 b22 (f 21 b21 (f 20 b20 (f 19 b19 (f 18 b18 (f 17 b17 (f 16 b16
+  (f 15 b15 (f 14 b14 (f 13 b13 (f 12 b12 (f 11 b11 (f 10 b10 (f 9 b9 (f 8 b8
+  (f 7 b7 (f 6 b6 (f 5 b5 (f 4 b4 (f 3 b3 (f 2 b2 (f 1 b1 (f 0 b0 0))))))))))))))))))))))))))))))
+*)
+
+let constr (b30,b29,b28,b27,b26,b25,b24,
+            b23,b22,b21,b20,b19,b18,b17,b16,
+            b15,b14,b13,b12,b11,b10,b9,b8,
+            b7,b6,b5,b4,b3,b2,b1,b0) =
+  let f i b = if b then 1 lsl i else 0 in
+  f 30 b30 + f 29 b29 + f 28 b28 + f 27 b27 + f 26 b26 + f 25 b25 + f 24 b24 +
+  f 23 b23 + f 22 b22 + f 21 b21 + f 20 b20 + f 19 b19 + f 18 b18 + f 17 b17 + f 16 b16 +
+  f 15 b15 + f 14 b14 + f 13 b13 + f 12 b12 + f 11 b11 + f 10 b10 + f 9 b9 + f 8 b8 +
+  f 7 b7 + f 6 b6 + f 5 b5 + f 4 b4 + f 3 b3 + f 2 b2 + f 1 b1 + f 0 b0
+
+let destr f n =
+  let b i = n land (1 lsl i) <> 0 in
+  f (b 30) (b 29) (b 28) (b 27) (b 26) (b 25) (b 24)
+    (b 23) (b 22) (b 21) (b 20) (b 19) (b 18) (b 17) (b 16)
+    (b 15) (b 14) (b 13) (b 12) (b 11) (b 10) (b 9) (b 8)
+    (b 7) (b 6) (b 5) (b 4) (b 3) (b 2) (b 1) (b 0)
+
+let twice n =
+  (n lsl 1) land 0x7FFFFFFF
+
+let twice_plus_one n =
+  ((n lsl 1) land 0x7FFFFFFF) lor 1
+
+let compare (x:int) (y:int) =
+  if x = y then Datatypes.Eq
+  else begin
+    let sx = x < 0 and sy = y < 0 in
+    if sx = sy then
+      (if x < y then Datatypes.Lt else Datatypes.Gt)
+    else
+      (if sx then Datatypes.Gt else Datatypes.Lt)
+  end
+
+end