From 056068abd228fefab4951a61700aa6d54fb88287 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Jan 2013 09:10:29 +0000 Subject: Ported to Coq 8.4pl1. Merge of branches/coq-8.4. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Camlcoq.ml | 251 +++++++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 191 insertions(+), 60 deletions(-) (limited to 'lib/Camlcoq.ml') diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index 00c21030..442766d8 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -16,75 +16,206 @@ (* Library of useful Caml <-> Coq conversions *) open Datatypes -open BinPos +open BinNums open BinInt +open BinPos open Floats -(* Integers *) +(* Coq's [nat] type and some of its operations *) -let rec camlint_of_positive = function - | Coq_xI p -> Int32.add (Int32.shift_left (camlint_of_positive p) 1) 1l - | Coq_xO p -> Int32.shift_left (camlint_of_positive p) 1 - | Coq_xH -> 1l +module Nat = struct -let camlint_of_z = function - | Z0 -> 0l - | Zpos p -> camlint_of_positive p - | Zneg p -> Int32.neg (camlint_of_positive p) + type t = nat = O | S of t + + let rec to_int = function + | O -> 0 + | S n -> succ (to_int n) + + let rec to_int32 = function + | O -> 0l + | S n -> Int32.succ(to_int32 n) + + let rec of_int n = + assert (n >= 0); + if n = 0 then O else S (of_int (pred n)) + + let rec of_int32 n = + assert (n >= 0l); + if n = 0l then O else S (of_int32 (Int32.pred n)) + +end + + +(* Coq's [positive] type and some of its operations *) -let camlint_of_coqint : Integers.Int.int -> int32 = camlint_of_z +module P = struct -let rec camlint64_of_positive = function - | Coq_xI p -> Int64.add (Int64.shift_left (camlint64_of_positive p) 1) 1L - | Coq_xO p -> Int64.shift_left (camlint64_of_positive p) 1 + type t = positive = Coq_xI of t | Coq_xO of t | Coq_xH + + let one = Coq_xH + let succ = Pos.succ + let pred = Pos.pred + let add = Pos.add + let sub = Pos.sub + let eq x y = (Pos.compare x y = Eq) + let lt x y = (Pos.compare x y = Lt) + let gt x y = (Pos.compare x y = Gt) + let le x y = (Pos.compare x y <> Gt) + let ge x y = (Pos.compare x y <> Lt) + + let rec to_int = function + | Coq_xI p -> (to_int p lsl 1) + 1 + | Coq_xO p -> to_int p lsl 1 + | Coq_xH -> 1 + + let rec of_int n = + if n = 0 then assert false else + if n = 1 then Coq_xH else + if n land 1 = 0 + then Coq_xO (of_int (n lsr 1)) + else Coq_xI (of_int (n lsr 1)) + + let rec to_int32 = function + | Coq_xI p -> Int32.add (Int32.shift_left (to_int32 p) 1) 1l + | Coq_xO p -> Int32.shift_left (to_int32 p) 1 + | Coq_xH -> 1l + + let rec of_int32 n = + if n = 0l then assert false else + if n = 1l then Coq_xH else + if Int32.logand n 1l = 0l + then Coq_xO (of_int32 (Int32.shift_right_logical n 1)) + else Coq_xI (of_int32 (Int32.shift_right_logical n 1)) + + let rec to_int64 = function + | Coq_xI p -> Int64.add (Int64.shift_left (to_int64 p) 1) 1L + | Coq_xO p -> Int64.shift_left (to_int64 p) 1 | Coq_xH -> 1L -let camlint64_of_z = function - | Z0 -> 0L - | Zpos p -> camlint64_of_positive p - | Zneg p -> Int64.neg (camlint64_of_positive p) + let rec of_int64 n = + if n = 0L then assert false else + if n = 1L then Coq_xH else + if Int64.logand n 1L = 0L + then Coq_xO (of_int64 (Int64.shift_right_logical n 1)) + else Coq_xI (of_int64 (Int64.shift_right_logical n 1)) + + let (+) = add + let (-) = sub + let (=) = eq + let (<) = lt + let (<=) = le + let (>) = gt + let (>=) = ge + +end + +(* Coq's [Z] type and some of its operations *) + +module Z = struct + + type t = coq_Z = Z0 | Zpos of positive | Zneg of positive + + let zero = Z0 + let one = Zpos Coq_xH + let mone = Zneg Coq_xH + let succ = Z.succ + let pred = Z.pred + let neg = Z.opp + let add = Z.add + let sub = Z.sub + let mul = Z.mul + let eq x y = (Z.compare x y = Eq) + let lt x y = (Z.compare x y = Lt) + let gt x y = (Z.compare x y = Gt) + let le x y = (Z.compare x y <> Gt) + let ge x y = (Z.compare x y <> Lt) + + let to_int = function + | Z0 -> 0 + | Zpos p -> P.to_int p + | Zneg p -> - (P.to_int p) + + let of_sint n = + if n = 0 then Z0 else + if n > 0 then Zpos (P.of_int n) + else Zneg (P.of_int (-n)) + + let of_uint n = + if n = 0 then Z0 else Zpos (P.of_int n) + + let to_int32 = function + | Z0 -> 0l + | Zpos p -> P.to_int32 p + | Zneg p -> Int32.neg (P.to_int32 p) -let camlint64_of_coqint : Integers.Int64.int -> int64 = camlint64_of_z + let of_sint32 n = + if n = 0l then Z0 else + if n > 0l then Zpos (P.of_int32 n) + else Zneg (P.of_int32 (Int32.neg n)) -let rec camlint_of_nat = function - | O -> 0 - | S n -> camlint_of_nat n + 1 - -let rec nat_of_camlint n = - assert (n >= 0l); - if n = 0l then O else S (nat_of_camlint (Int32.sub n 1l)) - -let rec positive_of_camlint n = - if n = 0l then assert false else - if n = 1l then Coq_xH else - if Int32.logand n 1l = 0l - then Coq_xO (positive_of_camlint (Int32.shift_right_logical n 1)) - else Coq_xI (positive_of_camlint (Int32.shift_right_logical n 1)) - -let z_of_camlint n = - if n = 0l then Z0 else - if n > 0l then Zpos (positive_of_camlint n) - else Zneg (positive_of_camlint (Int32.neg n)) - -let coqint_of_camlint (n: int32) : Integers.Int.int = - (* Interpret n as unsigned so that resulting Z is in range *) - if n = 0l then Z0 else Zpos (positive_of_camlint n) - -let rec positive_of_camlint64 n = - if n = 0L then assert false else - if n = 1L then Coq_xH else - if Int64.logand n 1L = 0L - then Coq_xO (positive_of_camlint64 (Int64.shift_right_logical n 1)) - else Coq_xI (positive_of_camlint64 (Int64.shift_right_logical n 1)) - -let z_of_camlint64 n = - if n = 0L then Z0 else - if n > 0L then Zpos (positive_of_camlint64 n) - else Zneg (positive_of_camlint64 (Int64.neg n)) - -let coqint_of_camlint64 (n: int64) : Integers.Int64.int = - (* Interpret n as unsigned so that resulting Z is in range *) - if n = 0L then Z0 else Zpos (positive_of_camlint64 n) + let of_uint32 n = + if n = 0l then Z0 else Zpos (P.of_int32 n) + + let to_int64 = function + | Z0 -> 0L + | Zpos p -> P.to_int64 p + | Zneg p -> Int64.neg (P.to_int64 p) + + let of_sint64 n = + if n = 0L then Z0 else + if n > 0L then Zpos (P.of_int64 n) + else Zneg (P.of_int64 (Int64.neg n)) + + let of_uint64 n = + if n = 0L then Z0 else Zpos (P.of_int64 n) + + let rec to_string_rec base buff x = + if x = Z0 then () else begin + let (q, r) = Z.div_eucl x base in + to_string_rec base buff q; + let q' = to_int q in + Buffer.add_char buff (Char.chr + (if q' < 10 then Char.code '0' + q' + else Char.code 'A' + q' - 10)) + end + + let to_string_aux base x = + match x with + | Z0 -> "0" + | Zpos _ -> + let buff = Buffer.create 10 in + to_string_rec base buff x; + Buffer.contents buff + | Zneg p -> + let buff = Buffer.create 10 in + Buffer.add_char buff '-'; + to_string_rec base buff (Zpos p); + Buffer.contents buff + + let dec = to_string_aux (of_uint 10) + + let hex = to_string_aux (of_uint 16) + + let to_string = dec + + let (+) = add + let (-) = sub + let ( * ) = mul + let (=) = eq + let (<) = lt + let (<=) = le + let (>) = gt + let (>=) = ge +end + +(* Alternate names *) + +let camlint_of_coqint : Integers.Int.int -> int32 = Z.to_int32 +let coqint_of_camlint : int32 -> Integers.Int.int = Z.of_uint32 + (* interpret the int32 as unsigned so that result Z is in range for int *) +let camlint64_of_coqint : Integers.Int64.int -> int64 = Z.to_int64 +let coqint_of_camlint64 : int64 -> Integers.Int64.int = Z.of_uint64 + (* interpret the int64 as unsigned so that result Z is in range for int *) (* Atoms (positive integers representing strings) *) @@ -97,7 +228,7 @@ let intern_string s = Hashtbl.find atom_of_string s with Not_found -> let a = !next_atom in - next_atom := coq_Psucc !next_atom; + next_atom := Pos.succ !next_atom; Hashtbl.add atom_of_string s a; Hashtbl.add string_of_atom a s; a @@ -106,7 +237,7 @@ let extern_atom a = try Hashtbl.find string_of_atom a with Not_found -> - Printf.sprintf "$%ld" (camlint_of_positive a) + Printf.sprintf "$%d" (P.to_int a) let first_unused_ident () = !next_atom -- cgit