diff options
| author | Pierre Roux | 2020-03-26 08:20:09 +0100 |
|---|---|---|
| committer | Pierre Roux | 2020-05-09 17:59:00 +0200 |
| commit | 692c642672f863546b423d72c714c1417164e506 (patch) | |
| tree | 56ac54d810735fefb5fa7d91b2b5392f1f432578 | |
| parent | deb2607027c158d313b82846c67594067194c8b7 (diff) | |
Add hexadecimal numerals
We add hexadecimal numerals according to the following regexp
0[xX][0-9a-fA-F][0-9a-fA-F_]*(\.[0-9a-fA-F_]+)?([pP][+-]?[0-9][0-9_]*)?
This is unfortunately a rather large commit. I suggest reading it in
the following order:
* test-suite/output/ZSyntax.{v,out} new test
* test-suite/output/Int63Syntax.{v,out} ''
* test-suite/output/QArithSyntax.{v,out} ''
* test-suite/output/RealSyntax.{v,out} ''
* test-suite/output/FloatSyntax.{v,out} ''
* interp/numTok.ml{i,} extending numeral tokens
* theories/Init/Hexadecimal.v adaptation of Decimal.v
for the new hexadecimal Numeral Notation
* theories/Init/Numeral.v new interface for Numeral Notation (basically,
a numeral is either a decimal or an hexadecimal)
* theories/Init/Nat.v add hexadecimal numeral notation to nat
* theories/PArith/BinPosDef.v '' positive
* theories/ZArith/BinIntDef.v '' Z
* theories/NArith/BinNatDef.v '' N
* theories/QArith/QArith_base.v '' Q
* interp/notation.ml{i,} adapting implementation of numeral notations
* plugins/syntax/numeral.ml ''
* plugins/syntax/r_syntax.ml adapt parser for real numbers
* plugins/syntax/float_syntax.ml adapt parser for primitive floats
* theories/Init/Prelude.v register parser for nat
* adapting the test-suite (test-suite/output/NumeralNotations.{v,out}
and test-suite/output/SearchPattern.out)
* remaining ml files (interp/constrex{tern,pr_ops}.ml where two open
had to be permuted)
39 files changed, 1403 insertions, 251 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index d6097304ec..a8fb5a3f45 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -15,8 +15,8 @@ open Nameops open Libnames open Namegen open Glob_term -open Constrexpr open Notation +open Constrexpr (***********************) (* For binders parsing *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index d5a5bde616..3f7bb6e330 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -19,13 +19,13 @@ open Libnames open Namegen open Impargs open CAst +open Notation open Constrexpr open Constrexpr_ops open Notation_ops open Glob_term open Glob_ops open Pattern -open Notation open Detyping module NamedDecl = Context.Named.Declaration diff --git a/interp/notation.ml b/interp/notation.ml index 63c539d0eb..9766b12ea1 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -382,7 +382,7 @@ module InnerPrimToken = struct | _ -> false let mkNumeral n = - Numeral (NumTok.Signed.of_bigint n) + Numeral (NumTok.Signed.of_bigint CDec n) let mkString = function | None -> None @@ -423,23 +423,32 @@ type numnot_option = | Abstract of NumTok.UnsignedNat.t type int_ty = - { uint : Names.inductive; + { dec_uint : Names.inductive; + dec_int : Names.inductive; + hex_uint : Names.inductive; + hex_int : Names.inductive; + uint : Names.inductive; int : Names.inductive } type z_pos_ty = { z_ty : Names.inductive; pos_ty : Names.inductive } -type decimal_ty = +type numeral_ty = { int : int_ty; - decimal : Names.inductive } + decimal : Names.inductive; + hexadecimal : Names.inductive; + numeral : Names.inductive } type target_kind = - | Int of int_ty (* Coq.Init.Decimal.int + uint *) - | UInt of Names.inductive (* Coq.Init.Decimal.uint *) + | Int of int_ty (* Coq.Init.Numeral.int + uint *) + | UInt of int_ty (* Coq.Init.Numeral.uint *) | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *) - | Decimal of decimal_ty (* Coq.Init.Decimal.decimal + uint + int *) + | Numeral of numeral_ty (* Coq.Init.Numeral.numeral + uint + int *) + | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *) + | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *) + | Decimal of numeral_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *) type string_target_kind = | ListByte @@ -601,17 +610,23 @@ let warn_abstract_large_num = (** Decimal.Nil has index 1, then Decimal.D0 has index 2 .. Decimal.D9 is 11 *) let digit_of_char c = - assert ('0' <= c && c <= '9'); - Char.code c - Char.code '0' + 2 + assert ('0' <= c && c <= '9' || 'a' <= c && c <= 'f'); + if c <= '9' then Char.code c - Char.code '0' + 2 + else Char.code c - Char.code 'a' + 12 let char_of_digit n = - assert (2<=n && n<=11); - Char.chr (n-2 + Char.code '0') + assert (2<=n && n<=17); + if n <= 11 then Char.chr (n-2 + Char.code '0') + else Char.chr (n-12 + Char.code 'a') -let coquint_of_rawnum uint n = +let coquint_of_rawnum inds c n = + let uint = match c with CDec -> inds.dec_uint | CHex -> inds.hex_uint in let nil = mkConstruct (uint,1) in match n with None -> nil | Some n -> let str = NumTok.UnsignedNat.to_string n in + let str = match c with + | CDec -> str + | CHex -> String.sub str 2 (String.length str - 2) in (* cut "0x" *) let rec do_chars s i acc = if i < 0 then acc else @@ -620,61 +635,126 @@ let coquint_of_rawnum uint n = in do_chars str (String.length str - 1) nil -let coqint_of_rawnum inds (sign,n) = - let uint = coquint_of_rawnum inds.uint (Some n) in +let coqint_of_rawnum inds c (sign,n) = + let ind = match c with CDec -> inds.dec_int | CHex -> inds.hex_int in + let uint = coquint_of_rawnum inds c (Some n) in let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in - mkApp (mkConstruct (inds.int, pos_neg), [|uint|]) + mkApp (mkConstruct (ind, pos_neg), [|uint|]) -let coqdecimal_of_rawnum inds n = +let coqnumeral_of_rawnum inds c n = + let ind = match c with CDec -> inds.decimal | CHex -> inds.hexadecimal in let i, f, e = NumTok.Signed.to_int_frac_and_exponent n in - let i = coqint_of_rawnum inds.int i in - let f = coquint_of_rawnum inds.int.uint f in + let i = coqint_of_rawnum inds.int c i in + let f = coquint_of_rawnum inds.int c f in match e with - | None -> mkApp (mkConstruct (inds.decimal, 1), [|i; f|]) (* Decimal *) + | None -> mkApp (mkConstruct (ind, 1), [|i; f|]) (* (D|Hexad)ecimal *) | Some e -> - let e = coqint_of_rawnum inds.int e in - mkApp (mkConstruct (inds.decimal, 2), [|i; f; e|]) (* DecimalExp *) + let e = coqint_of_rawnum inds.int CDec e in + mkApp (mkConstruct (ind, 2), [|i; f; e|]) (* (D|Hexad)ecimalExp *) -let rawnum_of_coquint c = +let mkDecHex ind c n = match c with + | CDec -> mkApp (mkConstruct (ind, 1), [|n|]) (* (UInt|Int|)Dec *) + | CHex -> mkApp (mkConstruct (ind, 2), [|n|]) (* (UInt|Int|)Hex *) + +exception NonDecimal + +let decimal_coqnumeral_of_rawnum inds n = + if NumTok.Signed.classify n <> CDec then raise NonDecimal; + coqnumeral_of_rawnum inds CDec n + +let coqnumeral_of_rawnum inds n = + let c = NumTok.Signed.classify n in + let n = coqnumeral_of_rawnum inds c n in + mkDecHex inds.numeral c n + +let decimal_coquint_of_rawnum inds n = + if NumTok.UnsignedNat.classify n <> CDec then raise NonDecimal; + coquint_of_rawnum inds CDec (Some n) + +let coquint_of_rawnum inds n = + let c = NumTok.UnsignedNat.classify n in + let n = coquint_of_rawnum inds c (Some n) in + mkDecHex inds.uint c n + +let decimal_coqint_of_rawnum inds n = + if NumTok.SignedNat.classify n <> CDec then raise NonDecimal; + coqint_of_rawnum inds CDec n + +let coqint_of_rawnum inds n = + let c = NumTok.SignedNat.classify n in + let n = coqint_of_rawnum inds c n in + mkDecHex inds.int c n + +let rawnum_of_coquint cl c = let rec of_uint_loop c buf = match Constr.kind c with | Construct ((_,1), _) (* Nil *) -> () | App (c, [|a|]) -> (match Constr.kind c with - | Construct ((_,n), _) (* D0 to D9 *) -> + | Construct ((_,n), _) (* D0 to Df *) -> let () = Buffer.add_char buf (char_of_digit n) in of_uint_loop a buf | _ -> raise NotAValidPrimToken) | _ -> raise NotAValidPrimToken in let buf = Buffer.create 64 in + if cl = CHex then (Buffer.add_char buf '0'; Buffer.add_char buf 'x'); let () = of_uint_loop c buf in - if Int.equal (Buffer.length buf) 0 then + if Int.equal (Buffer.length buf) (match cl with CDec -> 0 | CHex -> 2) then (* To avoid ambiguities between Nil and (D0 Nil), we choose to not display Nil alone as "0" *) raise NotAValidPrimToken else NumTok.UnsignedNat.of_string (Buffer.contents buf) -let rawnum_of_coqint c = +let rawnum_of_coqint cl c = match Constr.kind c with | App (c,[|c'|]) -> (match Constr.kind c with - | Construct ((_,1), _) (* Pos *) -> (SPlus,rawnum_of_coquint c') - | Construct ((_,2), _) (* Neg *) -> (SMinus,rawnum_of_coquint c') + | Construct ((_,1), _) (* Pos *) -> (SPlus,rawnum_of_coquint cl c') + | Construct ((_,2), _) (* Neg *) -> (SMinus,rawnum_of_coquint cl c') | _ -> raise NotAValidPrimToken) | _ -> raise NotAValidPrimToken -let rawnum_of_decimal c = +let rawnum_of_coqnumeral cl c = let of_ife i f e = - let n = rawnum_of_coqint i in - let f = try Some (rawnum_of_coquint f) with NotAValidPrimToken -> None in - let e = match e with None -> None | Some e -> Some (rawnum_of_coqint e) in + let n = rawnum_of_coqint cl i in + let f = try Some (rawnum_of_coquint cl f) with NotAValidPrimToken -> None in + let e = match e with None -> None | Some e -> Some (rawnum_of_coqint CDec e) in NumTok.Signed.of_int_frac_and_exponent n f e in match Constr.kind c with | App (_,[|i; f|]) -> of_ife i f None | App (_,[|i; f; e|]) -> of_ife i f (Some e) | _ -> raise NotAValidPrimToken +let destDecHex c = match Constr.kind c with + | App (c,[|c'|]) -> + (match Constr.kind c with + | Construct ((_,1), _) (* (UInt|Int|)Dec *) -> CDec, c' + | Construct ((_,2), _) (* (UInt|Int|)Hex *) -> CHex, c' + | _ -> raise NotAValidPrimToken) + | _ -> raise NotAValidPrimToken + +let decimal_rawnum_of_coqnumeral c = + rawnum_of_coqnumeral CDec c + +let rawnum_of_coqnumeral c = + let cl, c = destDecHex c in + rawnum_of_coqnumeral cl c + +let decimal_rawnum_of_coquint c = + rawnum_of_coquint CDec c + +let rawnum_of_coquint c = + let cl, c = destDecHex c in + rawnum_of_coquint cl c + +let decimal_rawnum_of_coqint c = + rawnum_of_coqint CDec c + +let rawnum_of_coqint c = + let cl, c = destDecHex c in + rawnum_of_coqint cl c + (***********************************************************************) (** ** Conversion between Coq [Z] and internal bigint *) @@ -768,15 +848,24 @@ let interp o ?loc n = let c = match fst o.to_kind, NumTok.Signed.to_int n with | Int int_ty, Some n -> coqint_of_rawnum int_ty n - | UInt uint_ty, Some (SPlus, n) -> - coquint_of_rawnum uint_ty (Some n) + | UInt int_ty, Some (SPlus, n) -> + coquint_of_rawnum int_ty n + | DecimalInt int_ty, Some n -> + (try decimal_coqint_of_rawnum int_ty n + with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name) + | DecimalUInt int_ty, Some (SPlus, n) -> + (try decimal_coquint_of_rawnum int_ty n + with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name) | Z z_pos_ty, Some n -> z_of_bigint z_pos_ty (NumTok.SignedNat.to_bigint n) | Int63, Some n -> interp_int63 ?loc (NumTok.SignedNat.to_bigint n) - | (Int _ | UInt _ | Z _ | Int63), _ -> + | (Int _ | UInt _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63), _ -> no_such_prim_token "number" ?loc o.ty_name - | Decimal decimal_ty, _ -> coqdecimal_of_rawnum decimal_ty n + | Numeral numeral_ty, _ -> coqnumeral_of_rawnum numeral_ty n + | Decimal numeral_ty, _ -> + (try decimal_coqnumeral_of_rawnum numeral_ty n + with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name) in let env = Global.env () in let sigma = Evd.from_env env in @@ -797,9 +886,12 @@ let uninterp o n = begin function | (Int _, c) -> NumTok.Signed.of_int (rawnum_of_coqint c) | (UInt _, c) -> NumTok.Signed.of_nat (rawnum_of_coquint c) - | (Z _, c) -> NumTok.Signed.of_bigint (bigint_of_z c) - | (Int63, c) -> NumTok.Signed.of_bigint (bigint_of_int63 c) - | (Decimal _, c) -> rawnum_of_decimal c + | (Z _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_z c) + | (Int63, c) -> NumTok.Signed.of_bigint CDec (bigint_of_int63 c) + | (Numeral _, c) -> rawnum_of_coqnumeral c + | (DecimalInt _, c) -> NumTok.Signed.of_int (decimal_rawnum_of_coqint c) + | (DecimalUInt _, c) -> NumTok.Signed.of_nat (decimal_rawnum_of_coquint c) + | (Decimal _, c) -> decimal_rawnum_of_coqnumeral c end o n end @@ -1126,8 +1218,8 @@ let find_notation ntn sc = NotationMap.find ntn (find_scope sc).notations let notation_of_prim_token = function - | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.Unsigned.sprint n - | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.Unsigned.sprint n + | Constrexpr.Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.Unsigned.sprint n + | Constrexpr.Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.Unsigned.sprint n | String _ -> raise Not_found let find_prim_token check_allowed ?loc p sc = @@ -1333,14 +1425,14 @@ let availability_of_prim_token n printer_scope local_scopes = let uid = snd (String.Map.find scope !prim_token_interp_infos) in let open InnerPrimToken in match n, uid with - | Numeral _, NumeralNotation _ -> true + | Constrexpr.Numeral _, NumeralNotation _ -> true | _, NumeralNotation _ -> false | String _, StringNotation _ -> true | _, StringNotation _ -> false | _, Uid uid -> let interp = Hashtbl.find prim_token_interpreters uid in match n, interp with - | Numeral _, (RawNumInterp _ | BigNumInterp _) -> true + | Constrexpr.Numeral _, (RawNumInterp _ | BigNumInterp _) -> true | String _, StringInterp _ -> true | _ -> false with Not_found -> false diff --git a/interp/notation.mli b/interp/notation.mli index 842f2b1458..a6b7e81841 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -74,7 +74,7 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name (** {6 Declare and uses back and forth an interpretation of primitive token } *) -(** A numeral interpreter is the pair of an interpreter for **decimal** +(** A numeral interpreter is the pair of an interpreter for **(hexa)decimal** numbers in terms and an optional interpreter in pattern, if non integer or negative numbers are not supported, the interpreter must fail with an appropriate error message *) @@ -120,23 +120,32 @@ type numnot_option = | Abstract of NumTok.UnsignedNat.t type int_ty = - { uint : Names.inductive; + { dec_uint : Names.inductive; + dec_int : Names.inductive; + hex_uint : Names.inductive; + hex_int : Names.inductive; + uint : Names.inductive; int : Names.inductive } type z_pos_ty = { z_ty : Names.inductive; pos_ty : Names.inductive } -type decimal_ty = +type numeral_ty = { int : int_ty; - decimal : Names.inductive } + decimal : Names.inductive; + hexadecimal : Names.inductive; + numeral : Names.inductive } type target_kind = - | Int of int_ty (* Coq.Init.Decimal.int + uint *) - | UInt of Names.inductive (* Coq.Init.Decimal.uint *) + | Int of int_ty (* Coq.Init.Numeral.int + uint *) + | UInt of int_ty (* Coq.Init.Numeral.uint *) | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *) - | Decimal of decimal_ty (* Coq.Init.Decimal.decimal + uint + int *) + | Numeral of numeral_ty (* Coq.Init.Numeral.numeral + uint + int *) + | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *) + | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *) + | Decimal of numeral_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *) type string_target_kind = | ListByte diff --git a/interp/numTok.ml b/interp/numTok.ml index 300e12f3af..bb14649b91 100644 --- a/interp/numTok.ml +++ b/interp/numTok.ml @@ -12,6 +12,8 @@ e.g. "e"/"E" or the presence of leading 0s, or the presence of a + in the exponent *) +type num_class = CDec | CHex + let string_del_head n s = String.sub s n (String.length s - n) module UnsignedNat = @@ -22,12 +24,15 @@ struct assert (s.[0] >= '0' && s.[0] <= '9'); s let to_string s = - String.(concat "" (split_on_char '_' s)) + String.(map Char.lowercase_ascii (concat "" (split_on_char '_' s))) let sprint s = s let print s = Pp.str (sprint s) - (** Comparing two raw numbers (base 10, big-endian, non-negative). + let classify s = + if String.length s >= 2 && (s.[1] = 'x' || s.[1] = 'X') then CHex else CDec + + (** Comparing two raw numbers (base 10 or 16, big-endian, non-negative). A bit nasty, but not critical: used e.g. to decide when a number is considered as large (see threshold warnings in notation.ml). *) @@ -47,12 +52,20 @@ struct 0 with Comp c -> c + let compare n d = + assert (classify d = CDec); + match classify n with + | CDec -> compare (to_string n) (to_string d) + | CHex -> compare (string_del_head 2 (to_string n)) (to_string d) + let is_zero s = compare s "0" = 0 end type sign = SPlus | SMinus +type 'a exp = EDec of 'a | EBin of 'a + module SignedNat = struct type t = sign * UnsignedNat.t @@ -66,20 +79,83 @@ struct (sign,UnsignedNat.of_string n) let to_string (sign,n) = (match sign with SPlus -> "" | SMinus -> "-") ^ UnsignedNat.to_string n - let to_bigint n = Bigint.of_string (to_string n) - let of_bigint n = + let classify (_,n) = UnsignedNat.classify n + let bigint_of_string (sign,n) = + (* nasty code to remove when switching to zarith + since zarith's of_string handles hexadecimal *) + match UnsignedNat.classify n with + | CDec -> Bigint.of_string (to_string (sign,n)) + | CHex -> + let int_of_char c = match c with + | 'a'..'f' -> 10 + int_of_char c - int_of_char 'a' + | _ -> int_of_char c - int_of_char '0' in + let c16 = Bigint.of_int 16 in + let s = UnsignedNat.to_string n in + let n = ref Bigint.zero in + let len = String.length s in + for d = 2 to len - 1 do + n := Bigint.(add (mult !n c16) (of_int (int_of_char s.[d]))) + done; + match sign with SPlus -> !n | SMinus -> Bigint.neg !n + let to_bigint n = bigint_of_string n + let string_of_nonneg_bigint c n = + (* nasty code to remove when switching to zarith + since zarith's format handles hexadecimal *) + match c with + | CDec -> Bigint.to_string n + | CHex -> + let div16 n = + let n, r0 = Bigint.div2_with_rest n in + let n, r1 = Bigint.div2_with_rest n in + let n, r2 = Bigint.div2_with_rest n in + let n, r3 = Bigint.div2_with_rest n in + let r = match r3, r2, r1, r0 with + | false, false, false, false -> "0" + | false, false, false, true -> "1" + | false, false, true, false -> "2" + | false, false, true, true -> "3" + | false, true, false, false -> "4" + | false, true, false, true -> "5" + | false, true, true, false -> "6" + | false, true, true, true -> "7" + | true, false, false, false -> "8" + | true, false, false, true -> "9" + | true, false, true, false -> "a" + | true, false, true, true -> "b" + | true, true, false, false -> "c" + | true, true, false, true -> "d" + | true, true, true, false -> "e" + | true, true, true, true -> "f" in + n, r in + let n = ref n in + let l = ref [] in + while Bigint.is_strictly_pos !n do + let n', r = div16 !n in + n := n'; + l := r :: !l + done; + "0x" ^ String.concat "" (List.rev !l) + let of_bigint c n = let sign, n = if Bigint.is_strictly_neg n then (SMinus, Bigint.neg n) else (SPlus, n) in - (sign, Bigint.to_string n) + (sign, string_of_nonneg_bigint c n) end module Unsigned = struct type t = { - int : string; (** \[0-9\]\[0-9_\]* *) - frac : string; (** empty or \[0-9_\]+ *) - exp : string (** empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *) + int : string; + frac : string; + exp : string } + (** + - int: \[0-9\]\[0-9_\]* + - frac: empty or \[0-9_\]+ + - exp: empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* + or + - int: 0\[xX\]\[0-9a-fA-F\]\[0-9a-fA-F_\]* + - frac: empty or \[0-9a-fA-F_\]+ + - exp: empty or \[pP\]\[+-\]?\[0-9\]\[0-9_\]* *) let equal n1 n2 = String.(equal n1.int n2.int && equal n1.frac n2.frac && equal n1.exp n2.exp) @@ -98,19 +174,35 @@ struct | Some ('0'..'9' as c) -> Stream.junk s; number (store len c) s | Some ('_' as c) when len > 0 -> Stream.junk s; number (store len c) s | _ -> len in + (* reads [0-9a-fA-F_]* *) + let rec hex_number len s = match Stream.peek s with + | Some (('0'..'9' | 'a'..'f' | 'A'..'F') as c) -> + Stream.junk s; hex_number (store len c) s + | Some ('_' as c) when len > 0 -> + Stream.junk s; hex_number (store len c) s + | _ -> len in fun s -> - let i = get_buff (number 0 s) in + let hex, i = + match Stream.npeek 3 s with + | '0' :: (('x' | 'X') as x) :: (('0'..'9' | 'a'..'f' | 'A'..'F') as c) :: _ -> + Stream.junk s; Stream.junk s; Stream.junk s; + true, get_buff (hex_number (store (store (store 0 '0') x) c) s) + | _ -> false, get_buff (number 0 s) in assert (i <> ""); let f = - match Stream.npeek 2 s with - | '.' :: (('0'..'9' | '_') as c) :: _ -> + match hex, Stream.npeek 2 s with + | true, '.' :: (('0'..'9' | 'a'..'f' | 'A'..'F' | '_') as c) :: _ -> + Stream.junk s; Stream.junk s; get_buff (hex_number (store 0 c) s) + | false, '.' :: (('0'..'9' | '_') as c) :: _ -> Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s) | _ -> "" in let e = - match (Stream.npeek 2 s) with - | (('e'|'E') as e) :: ('0'..'9' as c) :: _ -> + match hex, Stream.npeek 2 s with + | true, (('p'|'P') as e) :: ('0'..'9' as c) :: _ + | false, (('e'|'E') as e) :: ('0'..'9' as c) :: _ -> Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s) - | (('e'|'E') as e) :: (('+'|'-') as sign) :: _ -> + | true, (('p'|'P') as e) :: (('+'|'-') as sign) :: _ + | false, (('e'|'E') as e) :: (('+'|'-') as sign) :: _ -> begin match Stream.npeek 3 s with | _ :: _ :: ('0'..'9' as c) :: _ -> Stream.junk s; Stream.junk s; Stream.junk s; @@ -148,6 +240,7 @@ struct | { int = _; frac = ""; exp = "" } -> true | _ -> false + let classify n = UnsignedNat.classify n.int end open Unsigned @@ -165,8 +258,15 @@ struct | _ -> false let of_int_frac_and_exponent (sign,int) f e = - let exp = match e with Some e -> "e" ^ SignedNat.to_string e | None -> "" in - let frac = match f with Some f -> UnsignedNat.to_string f | None -> "" in + assert (match e with None -> true | Some e -> SignedNat.classify e = CDec); + let c = UnsignedNat.classify int in + let exp = match e with None -> "" | Some e -> + let e = SignedNat.to_string e in + match c with CDec -> "e" ^ e | CHex -> "p" ^ e in + let frac = match f with None -> "" | Some f -> + assert (c = UnsignedNat.classify f); + let f = UnsignedNat.to_string f in + match c with CDec -> f | CHex -> string_del_head 2 f in sign, { int; frac; exp } let to_int_frac_and_exponent (sign, { int; frac; exp }) = @@ -176,7 +276,11 @@ struct | '-' -> SMinus, string_del_head 2 exp | '+' -> SPlus, string_del_head 2 exp | _ -> SPlus, string_del_head 1 exp) in - let f = if frac = "" then None else Some frac in + let f = + if frac = "" then None else + Some (match UnsignedNat.classify int with + | CDec -> frac + | CHex -> "0x" ^ frac) in (sign, int), f, e let of_nat i = @@ -226,27 +330,31 @@ struct Some (SignedNat.to_bigint (sign,UnsignedNat.to_string n)) | _ -> None - let of_bigint n = - let sign, int = SignedNat.of_bigint n in - (sign, { int; frac = ""; exp = "" }) + let of_bigint c n = + of_int (SignedNat.of_bigint c n) let to_bigint_and_exponent (s, { int; frac; exp }) = - let s = match s with SPlus -> "" | SMinus -> "-" in + let c = UnsignedNat.classify int in let int = UnsignedNat.to_string int in let frac = UnsignedNat.to_string frac in - let i = Bigint.of_string (s ^ int ^ frac) in + let i = SignedNat.to_bigint (s, int ^ frac) in let e = let e = if exp = "" then Bigint.zero else match exp.[1] with | '+' -> Bigint.of_string (UnsignedNat.to_string (string_del_head 2 exp)) | '-' -> Bigint.(neg (of_string (UnsignedNat.to_string (string_del_head 2 exp)))) | _ -> Bigint.of_string (UnsignedNat.to_string (string_del_head 1 exp)) in - Bigint.(sub e (of_int (String.length (String.concat "" (String.split_on_char '_' frac))))) in - (i,e) + let l = String.length frac in + let l = match c with CDec -> l | CHex -> 4 * l in + Bigint.(sub e (of_int l)) in + (i, match c with CDec -> EDec e | CHex -> EBin e) let of_bigint_and_exponent i e = - of_int_frac_and_exponent (SignedNat.of_bigint i) None (Some (SignedNat.of_bigint e)) + let c = match e with EDec _ -> CDec | EBin _ -> CHex in + let e = match e with EDec e | EBin e -> Some (SignedNat.of_bigint CDec e) in + of_int_frac_and_exponent (SignedNat.of_bigint c i) None e let is_bigger_int_than (s, { int; frac; exp }) i = frac = "" && exp = "" && UnsignedNat.compare int i >= 0 + let classify (_, n) = Unsigned.classify n end diff --git a/interp/numTok.mli b/interp/numTok.mli index c48fad908d..11d5a0f980 100644 --- a/interp/numTok.mli +++ b/interp/numTok.mli @@ -11,7 +11,7 @@ (** Numerals in different forms: signed or unsigned, possibly with fractional part and exponent. - Numerals are represented using raw strings of decimal + Numerals are represented using raw strings of (hexa)decimal literals and a separate sign flag. Note that this representation is not unique, due to possible @@ -25,21 +25,29 @@ type sign = SPlus | SMinus +type num_class = CDec | CHex + +type 'a exp = EDec of 'a | EBin of 'a + (** {6 String representation of a natural number } *) module UnsignedNat : sig type t val of_string : string -> t - (** Convert from a non-empty sequence of digits (which may contain "_") *) + (** Convert from a non-empty sequence of digits (which may contain "_") + (or hexdigits when starting with "0x" or "0X") *) val to_string : t -> string - (** Convert to a non-empty sequence of digit that does not contain "_" *) + (** Convert to a non-empty sequence of digit that does not contain "_" + (or hexdigits, starting with "0x", all hexdigits are lower case) *) val sprint : t -> string val print : t -> Pp.t (** [sprint] and [print] returns the numeral as it was parsed, for printing *) + val classify : t -> num_class + val compare : t -> t -> int end @@ -49,12 +57,15 @@ module SignedNat : sig type t = sign * UnsignedNat.t val of_string : string -> t - (** Convert from a non-empty sequence of digits which may contain "_" *) + (** Convert from a non-empty sequence of (hex)digits which may contain "_" *) val to_string : t -> string - (** Convert to a non-empty sequence of digit that does not contain "_" *) + (** Convert to a non-empty sequence of (hex)digit that does not contain "_" + (hexadecimals start with "0x" and all hexdigits are lower case) *) - val of_bigint : Bigint.bigint -> t + val classify : t -> num_class + + val of_bigint : num_class -> Bigint.bigint -> t val to_bigint : t -> Bigint.bigint end @@ -78,11 +89,17 @@ sig The recognized syntax is: - integer part: \[0-9\]\[0-9_\]* - - decimal part: empty or .\[0-9_\]+ - - exponent part: empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *) + - fractional part: empty or .\[0-9_\]+ + - exponent part: empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* + or + - integer part: 0\[xX\]\[0-9a-fA-F\]\[0-9a-fA-F_\]* + - fractional part: empty or .\[0-9a-fA-F_\]+ + - exponent part: empty or \[pP\]\[+-\]?\[0-9\]\[0-9_\]* *) val parse_string : string -> t option - (** Parse the string as a positive Coq numeral, if possible *) + (** Parse the string as a non negative Coq numeral, if possible *) + + val classify : t -> num_class end @@ -114,17 +131,20 @@ sig val to_string : t -> string (** Returns a string in the syntax of OCaml's float_of_string *) - val of_bigint : Bigint.bigint -> t + val of_bigint : num_class -> Bigint.bigint -> t val to_bigint : t -> Bigint.bigint option (** Convert from and to bigint when the denotation of a bigint *) val of_int_frac_and_exponent : SignedNat.t -> UnsignedNat.t option -> SignedNat.t option -> t val to_int_frac_and_exponent : t -> SignedNat.t * UnsignedNat.t option * SignedNat.t option - (** n, p and q such that the number is n.p*10^q *) + (** n, p and q such that the number is n.p*10^q or n.p*2^q + pre/postcondition: classify n = classify p, classify q = CDec *) + + val of_bigint_and_exponent : Bigint.bigint -> Bigint.bigint exp -> t + val to_bigint_and_exponent : t -> Bigint.bigint * Bigint.bigint exp + (** n and p such that the number is n*10^p or n*2^p *) - val of_bigint_and_exponent : Bigint.bigint -> Bigint.bigint -> t - val to_bigint_and_exponent : t -> Bigint.bigint * Bigint.bigint - (** n and p such that the number is n*10^p *) + val classify : t -> num_class val is_bigger_int_than : t -> UnsignedNat.t -> bool (** Test if an integer whose absolute value is bounded *) diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml index 0a5825dfc1..9861a060ab 100644 --- a/plugins/syntax/float_syntax.ml +++ b/plugins/syntax/float_syntax.ml @@ -70,7 +70,8 @@ let interp_float ?loc n = else (* e < 0 *) if e' <= e then check m' (-e) m (e - e') else check' m' (-e) (e' - e) m in - if inexact () then warn_inexact_float ?loc (sn, f); + if NumTok.(Signed.classify n = CDec) && inexact () then + warn_inexact_float ?loc (sn, f); DAst.make ?loc (GFloat f) (* Pretty printing is already handled in constrextern.ml *) diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 2250d57809..2db76719b8 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -55,24 +55,45 @@ let locate_z () = }, mkRefC q_z) else None -let locate_decimal () = - let int = "num.int.type" in - let uint = "num.uint.type" in +let locate_numeral () = + let dint = "num.int.type" in + let duint = "num.uint.type" in let dec = "num.decimal.type" in - if Coqlib.has_ref int && Coqlib.has_ref uint && Coqlib.has_ref dec + let hint = "num.hexadecimal_int.type" in + let huint = "num.hexadecimal_uint.type" in + let hex = "num.hexadecimal.type" in + let int = "num.num_int.type" in + let uint = "num.num_uint.type" in + let num = "num.numeral.type" in + if Coqlib.has_ref dint && Coqlib.has_ref duint && Coqlib.has_ref dec + && Coqlib.has_ref hint && Coqlib.has_ref huint && Coqlib.has_ref hex + && Coqlib.has_ref int && Coqlib.has_ref uint && Coqlib.has_ref num then + let q_dint = qualid_of_ref dint in + let q_duint = qualid_of_ref duint in + let q_dec = qualid_of_ref dec in + let q_hint = qualid_of_ref hint in + let q_huint = qualid_of_ref huint in + let q_hex = qualid_of_ref hex in let q_int = qualid_of_ref int in let q_uint = qualid_of_ref uint in - let q_dec = qualid_of_ref dec in + let q_num = qualid_of_ref num in let int_ty = { + dec_int = unsafe_locate_ind q_dint; + dec_uint = unsafe_locate_ind q_duint; + hex_int = unsafe_locate_ind q_hint; + hex_uint = unsafe_locate_ind q_huint; int = unsafe_locate_ind q_int; uint = unsafe_locate_ind q_uint; } in - let dec_ty = { + let num_ty = { int = int_ty; decimal = unsafe_locate_ind q_dec; + hexadecimal = unsafe_locate_ind q_hex; + numeral = unsafe_locate_ind q_num; } in - Some (int_ty, mkRefC q_int, mkRefC q_uint, dec_ty, mkRefC q_dec) + Some (int_ty, mkRefC q_int, mkRefC q_uint, mkRefC q_dint, mkRefC q_duint, + num_ty, mkRefC q_num, mkRefC q_dec) else None let locate_int63 () = @@ -90,20 +111,27 @@ let has_type env sigma f ty = let type_error_to f ty = CErrors.user_err - (pr_qualid f ++ str " should go from Decimal.int to " ++ + (pr_qualid f ++ str " should go from Numeral.int to " ++ pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ - fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).") + fnl () ++ str "Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first).") let type_error_of g ty = CErrors.user_err (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ - str " to Decimal.int or (option Decimal.int)." ++ fnl () ++ - str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).") + str " to Numeral.int or (option Numeral.int)." ++ fnl () ++ + str "Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first).") + +let warn_deprecated_decimal = + CWarnings.create ~name:"decimal-numeral-notation" ~category:"deprecated" + (fun () -> + strbrk "Deprecated Numeral Notation for Decimal.uint, \ + Decimal.int or Decimal.decimal. Use Numeral.uint, \ + Numeral.int or Numeral.numeral respectively.") let vernac_numeral_notation local ty f g scope opts = let env = Global.env () in let sigma = Evd.from_env env in - let dec_ty = locate_decimal () in + let num_ty = locate_numeral () in let z_pos_ty = locate_z () in let int63_ty = locate_int63 () in let tyc = Smartlocate.global_inductive_with_alias ty in @@ -118,13 +146,19 @@ let vernac_numeral_notation local ty f g scope opts = let constructors = get_constructors tyc in (* Check the type of f *) let to_kind = - match dec_ty with - | Some (int_ty, cint, _, _, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct - | Some (int_ty, cint, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option - | Some (int_ty, _, cuint, _, _) when has_type env sigma f (arrow cuint cty) -> UInt int_ty.uint, Direct - | Some (int_ty, _, cuint, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option - | Some (_, _, _, dec_ty, cdec) when has_type env sigma f (arrow cdec cty) -> Decimal dec_ty, Direct - | Some (_, _, _, dec_ty, cdec) when has_type env sigma f (arrow cdec (opt cty)) -> Decimal dec_ty, Option + match num_ty with + | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct + | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option + | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint cty) -> UInt int_ty, Direct + | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty, Option + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum cty) -> Numeral num_ty, Direct + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum (opt cty)) -> Numeral num_ty, Option + | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint cty) -> DecimalInt int_ty, Direct + | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> DecimalInt int_ty, Option + | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint cty) -> DecimalUInt int_ty, Direct + | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> DecimalUInt int_ty, Option + | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec cty) -> Decimal num_ty, Direct + | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec (opt cty)) -> Decimal num_ty, Option | _ -> match z_pos_ty with | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ cty) -> Z z_pos_ty, Direct @@ -137,13 +171,19 @@ let vernac_numeral_notation local ty f g scope opts = in (* Check the type of g *) let of_kind = - match dec_ty with - | Some (int_ty, cint, _, _, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct - | Some (int_ty, cint, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option - | Some (int_ty, _, cuint, _, _) when has_type env sigma g (arrow cty cuint) -> UInt int_ty.uint, Direct - | Some (int_ty, _, cuint, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option - | Some (_, _, _, dec_ty, cdec) when has_type env sigma g (arrow cty cdec) -> Decimal dec_ty, Direct - | Some (_, _, _, dec_ty, cdec) when has_type env sigma g (arrow cty (opt cdec)) -> Decimal dec_ty, Option + match num_ty with + | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct + | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option + | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty cuint) -> UInt int_ty, Direct + | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty, Option + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty cnum) -> Numeral num_ty, Direct + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty (opt cnum)) -> Numeral num_ty, Option + | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty cint) -> DecimalInt int_ty, Direct + | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> DecimalInt int_ty, Option + | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty cuint) -> DecimalUInt int_ty, Direct + | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> DecimalUInt int_ty, Option + | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty cdec) -> Decimal num_ty, Direct + | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty (opt cdec)) -> Decimal num_ty, Option | _ -> match z_pos_ty with | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty cZ) -> Z z_pos_ty, Direct @@ -154,6 +194,11 @@ let vernac_numeral_notation local ty f g scope opts = | Some cint63 when has_type env sigma g (arrow cty (opt cint63)) -> Int63, Option | _ -> type_error_of g ty in + (match to_kind, of_kind with + | ((DecimalInt _ | DecimalUInt _ | Decimal _), _), _ + | _, ((DecimalInt _ | DecimalUInt _ | Decimal _), _) -> + warn_deprecated_decimal () + | _ -> ()); let o = { to_kind; to_ty; of_kind; of_ty; ty_name = ty; warning = opts } diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index b5f11d9025..23a7cc07c5 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -114,20 +114,21 @@ let glob_pow_pos = GlobRef.ConstRef (Constant.make2 z_modpath @@ Label.make "pow let r_of_rawnum ?loc n = let n,e = NumTok.Signed.to_bigint_and_exponent n in + let e,p = NumTok.(match e with EDec e -> e, 10 | EBin e -> e, 2) in let izr z = DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z]) in let rmult r r' = DAst.make @@ GApp (DAst.make @@ GRef(glob_Rmult,None), [r; r']) in let rdiv r r' = DAst.make @@ GApp (DAst.make @@ GRef(glob_Rdiv,None), [r; r']) in - let pow10 e = - let ten = z_of_int ?loc (Bigint.of_int 10) in + let pow p e = + let p = z_of_int ?loc (Bigint.of_int p) in let e = pos_of_bignat e in - DAst.make @@ GApp (DAst.make @@ GRef(glob_pow_pos,None), [ten; e]) in + DAst.make @@ GApp (DAst.make @@ GRef(glob_pow_pos,None), [p; e]) in let n = izr (z_of_int ?loc n) in - if Bigint.is_strictly_pos e then rmult n (izr (pow10 e)) - else if Bigint.is_strictly_neg e then rdiv n (izr (pow10 (neg e))) + if Bigint.is_strictly_pos e then rmult n (izr (pow p e)) + else if Bigint.is_strictly_neg e then rdiv n (izr (pow p (neg e))) else n (* e = 0 *) (**********************************************************************) @@ -149,7 +150,8 @@ let rawnum_of_r c = let le = String.length (Bigint.to_string e) in Bigint.(less_than (add (of_int li) (of_int le)) e) in (* print 123 * 10^-2 as 123e-2 *) - let numTok_exponent () = NumTok.Signed.of_bigint_and_exponent i e in + let numTok_exponent () = + NumTok.Signed.of_bigint_and_exponent i (NumTok.EDec e) in (* print 123 * 10^-2 as 1.23, precondition e < 0 *) let numTok_dot () = let s, i = @@ -168,7 +170,7 @@ let rawnum_of_r c = match DAst.get c with | GApp (r, [a]) when is_gr r glob_IZR -> let n = bigint_of_z a in - NumTok.Signed.of_bigint n + NumTok.(Signed.of_bigint CDec n) | GApp (md, [l; r]) when is_gr md glob_Rmult || is_gr md glob_Rdiv -> begin match DAst.get l, DAst.get r with | GApp (i, [l]), GApp (i', [r]) diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out index 7941d2e647..4a5a700879 100644 --- a/test-suite/output/FloatSyntax.out +++ b/test-suite/output/FloatSyntax.out @@ -42,13 +42,25 @@ closest value will be used and unambiguously printed : float 2.5 + 2.5 : float -File "stdin", line 24, characters 6-11: +-26 + : float +11.171875 + : float +-6882 + : float +44.6875 + : float +2860 + : float +-2.79296875 + : float +File "stdin", line 30, characters 6-11: Warning: The constant 1e309 is not a binary64 floating-point value. A closest value will be used and unambiguously printed infinity. [inexact-float,parsing] infinity : float -File "stdin", line 25, characters 6-12: +File "stdin", line 31, characters 6-12: Warning: The constant -1e309 is not a binary64 floating-point value. A closest value will be used and unambiguously printed neg_infinity. [inexact-float,parsing] diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v index eca712db10..36ffc27239 100644 --- a/test-suite/output/FloatSyntax.v +++ b/test-suite/output/FloatSyntax.v @@ -20,6 +20,12 @@ Check 2.5e123. Check (-2.5e-123). Check (2 + 2). Check (2.5 + 2.5). +Check -0x1a. +Check 0xb.2c. +Check -0x1ae2. +Check 0xb.2cp2. +Check 0xb.2cp8. +Check -0xb.2cp-2. Check 1e309. Check -1e309. diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out index 4d76f1210b..eefa338f0d 100644 --- a/test-suite/output/Int63Syntax.out +++ b/test-suite/output/Int63Syntax.out @@ -6,6 +6,32 @@ : int 9223372036854775807 : int +427 + : int +427 + : int +427 + : int +427 + : int +427 + : int +The command has indeed failed with message: +Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.Int63.int +The command has indeed failed with message: +Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.Int63.int +0 + : int +0 + : int +The command has indeed failed with message: +The reference xg was not found in the current environment. +The command has indeed failed with message: +The reference xG was not found in the current environment. +The command has indeed failed with message: +The reference x1 was not found in the current environment. +The command has indeed failed with message: +The reference x was not found in the current environment. 2 + 2 : int 2 + 2 diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v index 0385e529bf..c49616d918 100644 --- a/test-suite/output/Int63Syntax.v +++ b/test-suite/output/Int63Syntax.v @@ -5,6 +5,19 @@ Check (2 + 2)%int63. Open Scope int63_scope. Check 2. Check 9223372036854775807. +Check 0x1ab. +Check 0X1ab. +Check 0x1Ab. +Check 0x1aB. +Check 0x1AB. +Fail Check 0x1ap5. (* exponents not implemented (yet?) *) +Fail Check 0x1aP5. +Check 0x0. +Check 0x000. +Fail Check 0xg. +Fail Check 0xG. +Fail Check 00x1. +Fail Check 0x. Check (Int63.add 2 2). Check (2+2). Eval vm_compute in 2+2. diff --git a/test-suite/output/NatSyntax.out b/test-suite/output/NatSyntax.out new file mode 100644 index 0000000000..3067896d7a --- /dev/null +++ b/test-suite/output/NatSyntax.out @@ -0,0 +1,34 @@ +42 + : nat +0 + : nat +0 + : nat +427 + : nat +427 + : nat +427 + : nat +427 + : nat +427 + : nat +The command has indeed failed with message: +Cannot interpret this number as a value of type nat +The command has indeed failed with message: +Cannot interpret this number as a value of type nat +0 + : nat +0 + : nat +The command has indeed failed with message: +The reference xg was not found in the current environment. +The command has indeed failed with message: +The reference xG was not found in the current environment. +The command has indeed failed with message: +The reference x1 was not found in the current environment. +The command has indeed failed with message: +The reference x was not found in the current environment. +0x2a + : nat diff --git a/test-suite/output/NatSyntax.v b/test-suite/output/NatSyntax.v new file mode 100644 index 0000000000..66f697d412 --- /dev/null +++ b/test-suite/output/NatSyntax.v @@ -0,0 +1,18 @@ +Check 42. +Check 0. +Check 00. +Check 0x1ab. +Check 0X1ab. +Check 0x1Ab. +Check 0x1aB. +Check 0x1AB. +Fail Check 0x1ap1. (* exponents not implemented (yet?) *) +Fail Check 0x1aP1. +Check 0x0. +Check 0x000. +Fail Check 0xg. +Fail Check 0xG. +Fail Check 00x1. +Fail Check 0x. +Open Scope hex_nat_scope. +Check 42. diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out index 060877707b..34c31ff8a6 100644 --- a/test-suite/output/NumeralNotations.out +++ b/test-suite/output/NumeralNotations.out @@ -32,7 +32,7 @@ Warning: To avoid stack overflow, large numbers in punit are interpreted as applications of pto_punits. [abstract-large-number,numbers] The command has indeed failed with message: In environment -v := pto_punits (Decimal.D1 Decimal.Nil) : punit +v := pto_punits (Numeral.UIntDec (Decimal.D1 Decimal.Nil)) : punit The term "v" has type "punit@{Set}" while it is expected to have type "punit@{u}". S @@ -61,7 +61,7 @@ The command has indeed failed with message: In environment v := 0 : nat The term "v" has type "nat" while it is expected to have type "wuint". - = {| unwrap := Decimal.D0 Decimal.Nil |} + = {| unwrap := Numeral.UIntDec (Decimal.D0 Decimal.Nil) |} : wuint let v := 0%wuint8' in v : wuint : wuint @@ -82,7 +82,7 @@ function (of_uint) targets an option type. The command has indeed failed with message: The 'abstract after' directive has no effect when the parsing function (of_uint) targets an option type. [abstract-large-number-no-op,numbers] -let v := of_uint (Decimal.D1 Decimal.Nil) in v : unit +let v := of_uint (Numeral.UIntDec (Decimal.D1 Decimal.Nil)) in v : unit : unit let v := 0%test13 in v : unit : unit diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v index 47e1b127cb..ca8a14cce1 100644 --- a/test-suite/output/NumeralNotations.v +++ b/test-suite/output/NumeralNotations.v @@ -5,17 +5,17 @@ Declare Scope opaque_scope. (* https://github.com/coq/coq/pull/8064#discussion_r202497516 *) Module Test1. Axiom hold : forall {A B C}, A -> B -> C. - Definition opaque3 (x : Decimal.int) : Decimal.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end). - Numeral Notation Decimal.int opaque3 opaque3 : opaque_scope. + Definition opaque3 (x : Numeral.int) : Numeral.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end). + Numeral Notation Numeral.int opaque3 opaque3 : opaque_scope. Delimit Scope opaque_scope with opaque. Fail Check 1%opaque. End Test1. (* https://github.com/coq/coq/pull/8064#discussion_r202497990 *) Module Test2. - Axiom opaque4 : option Decimal.int. - Definition opaque6 (x : Decimal.int) : option Decimal.int := opaque4. - Numeral Notation Decimal.int opaque6 opaque6 : opaque_scope. + Axiom opaque4 : option Numeral.int. + Definition opaque6 (x : Numeral.int) : option Numeral.int := opaque4. + Numeral Notation Numeral.int opaque6 opaque6 : opaque_scope. Delimit Scope opaque_scope with opaque. Open Scope opaque_scope. Fail Check 1%opaque. @@ -24,8 +24,8 @@ End Test2. Declare Scope silly_scope. Module Test3. - Inductive silly := SILLY (v : Decimal.uint) (f : forall A, A -> A). - Definition to_silly (v : Decimal.uint) := SILLY v (fun _ x => x). + Inductive silly := SILLY (v : Numeral.uint) (f : forall A, A -> A). + Definition to_silly (v : Numeral.uint) := SILLY v (fun _ x => x). Definition of_silly (v : silly) := match v with SILLY v _ => v end. Numeral Notation silly to_silly of_silly : silly_scope. Delimit Scope silly_scope with silly. @@ -45,15 +45,15 @@ Module Test4. Declare Scope upp. Declare Scope ppps. Polymorphic NonCumulative Inductive punit := ptt. - Polymorphic Definition pto_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end. - Polymorphic Definition pto_punit_all (v : Decimal.uint) : punit := ptt. - Polymorphic Definition pof_punit (v : punit) : Decimal.uint := Nat.to_uint 0. - Definition to_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end. - Definition of_punit (v : punit) : Decimal.uint := Nat.to_uint 0. - Polymorphic Definition pto_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end. - Polymorphic Definition pof_unit (v : unit) : Decimal.uint := Nat.to_uint 0. - Definition to_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end. - Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0. + Polymorphic Definition pto_punit (v : Numeral.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end. + Polymorphic Definition pto_punit_all (v : Numeral.uint) : punit := ptt. + Polymorphic Definition pof_punit (v : punit) : Numeral.uint := Nat.to_num_uint 0. + Definition to_punit (v : Numeral.uint) : option punit := match Nat.of_num_uint v with O => Some ptt | _ => None end. + Definition of_punit (v : punit) : Numeral.uint := Nat.to_num_uint 0. + Polymorphic Definition pto_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. + Polymorphic Definition pof_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. + Definition to_unit (v : Numeral.uint) : option unit := match Nat.of_num_uint v with O => Some tt | _ => None end. + Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. Numeral Notation punit to_punit of_punit : pto. Numeral Notation punit pto_punit of_punit : ppo. Numeral Notation punit to_punit pof_punit : ptp. @@ -113,8 +113,8 @@ Module Test6. Local Set Primitive Projections. Record > wnat := wrap { unwrap :> nat }. - Definition to_uint (x : wnat) : Decimal.uint := Nat.to_uint x. - Definition of_uint (x : Decimal.uint) : wnat := Nat.of_uint x. + Definition to_uint (x : wnat) : Numeral.uint := Nat.to_num_uint x. + Definition of_uint (x : Numeral.uint) : wnat := Nat.of_num_uint x. Module Export Scopes. Declare Scope wnat_scope. Delimit Scope wnat_scope with wnat. @@ -138,7 +138,7 @@ End Test6_2. Module Test7. Local Set Primitive Projections. - Record wuint := wrap { unwrap : Decimal.uint }. + Record wuint := wrap { unwrap : Numeral.uint }. Declare Scope wuint_scope. Delimit Scope wuint_scope with wuint. Numeral Notation wuint wrap unwrap : wuint_scope. @@ -148,7 +148,7 @@ End Test7. Module Test8. Local Set Primitive Projections. - Record wuint := wrap { unwrap : Decimal.uint }. + Record wuint := wrap { unwrap : Numeral.uint }. Declare Scope wuint8_scope. Declare Scope wuint8'_scope. Delimit Scope wuint8_scope with wuint8. @@ -162,7 +162,7 @@ Module Test8. End with_var. Check let v := 0%wuint8 in v : nat. Fail Check let v := 0%wuint8 in v : wuint. - Compute wrap (Nat.to_uint 0). + Compute wrap (Nat.to_num_uint 0). Notation wrap'' := wrap. Notation unwrap'' := unwrap. @@ -177,7 +177,7 @@ Module Test9. Delimit Scope wuint9'_scope with wuint9'. Section with_let. Local Set Primitive Projections. - Record wuint := wrap { unwrap : Decimal.uint }. + Record wuint := wrap { unwrap : Numeral.uint }. Let wrap' := wrap. Let unwrap' := unwrap. Local Notation wrap'' := wrap. @@ -193,9 +193,9 @@ End Test9. Module Test10. (* Test that it is only a warning to add abstract after to an optional parsing function *) - Definition to_uint (v : unit) := Nat.to_uint 0. - Definition of_uint (v : Decimal.uint) := match Nat.of_uint v with O => Some tt | _ => None end. - Definition of_any_uint (v : Decimal.uint) := tt. + Definition to_uint (v : unit) := Nat.to_num_uint 0. + Definition of_uint (v : Numeral.uint) := match Nat.of_num_uint v with O => Some tt | _ => None end. + Definition of_any_uint (v : Numeral.uint) := tt. Declare Scope unit_scope. Declare Scope unit2_scope. Delimit Scope unit_scope with unit. @@ -213,7 +213,7 @@ Module Test12. Declare Scope test12_scope. Delimit Scope test12_scope with test12. Section test12. - Context (to_uint : unit -> Decimal.uint) (of_uint : Decimal.uint -> unit). + Context (to_uint : unit -> Numeral.uint) (of_uint : Numeral.uint -> unit). Numeral Notation unit of_uint to_uint : test12_scope. Check let v := 1%test12 in v : unit. @@ -228,8 +228,8 @@ Module Test13. Delimit Scope test13_scope with test13. Delimit Scope test13'_scope with test13'. Delimit Scope test13''_scope with test13''. - Definition to_uint (x y : unit) : Decimal.uint := Nat.to_uint O. - Definition of_uint (x : Decimal.uint) : unit := tt. + Definition to_uint (x y : unit) : Numeral.uint := Nat.to_num_uint O. + Definition of_uint (x : Numeral.uint) : unit := tt. Definition to_uint_good := to_uint tt. Notation to_uint' := (to_uint tt). Notation to_uint'' := (to_uint _). @@ -254,8 +254,8 @@ Module Test14. Delimit Scope test14''_scope with test14''. Delimit Scope test14'''_scope with test14'''. Module Inner. - Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. - Definition of_uint (x : Decimal.uint) : unit := tt. + Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. + Definition of_uint (x : Numeral.uint) : unit := tt. Local Numeral Notation unit of_uint to_uint : test14_scope. Global Numeral Notation unit of_uint to_uint : test14'_scope. Check let v := 0%test14 in v : unit. @@ -267,8 +267,8 @@ Module Test14. Fail Check let v := 0%test14 in v : unit. Check let v := 0%test14' in v : unit. Section InnerSection. - Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. - Definition of_uint (x : Decimal.uint) : unit := tt. + Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. + Definition of_uint (x : Numeral.uint) : unit := tt. Local Numeral Notation unit of_uint to_uint : test14''_scope. Fail Global Numeral Notation unit of_uint to_uint : test14'''_scope. Check let v := 0%test14'' in v : unit. @@ -283,8 +283,8 @@ Module Test15. Declare Scope test15_scope. Delimit Scope test15_scope with test15. Module Inner. - Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. - Definition of_uint (x : Decimal.uint) : unit := tt. + Definition to_uint (x : unit) : Numeral.uint := Nat.to_num_uint O. + Definition of_uint (x : Numeral.uint) : unit := tt. Numeral Notation unit of_uint to_uint : test15_scope. Check let v := 0%test15 in v : unit. End Inner. @@ -306,8 +306,8 @@ Module Test16. End A. Module F (a : A). Inductive Foo := foo (_ : a.T). - Definition to_uint (x : Foo) : Decimal.uint := Nat.to_uint O. - Definition of_uint (x : Decimal.uint) : Foo := foo a.t. + Definition to_uint (x : Foo) : Numeral.uint := Nat.to_num_uint O. + Definition of_uint (x : Numeral.uint) : Foo := foo a.t. Global Numeral Notation Foo of_uint to_uint : test16_scope. Check let v := 0%test16 in v : Foo. End F. @@ -352,9 +352,9 @@ Module Test18. Definition Q_of_nat (x : nat) : Q := {| num := x ; den := 1 ; reduced := transparentify (nat_eq_dec _ _) (gcd_good _) |}. Definition nat_of_Q (x : Q) : option nat := if Nat.eqb x.(den) 1 then Some (x.(num)) else None. - Definition Q_of_uint (x : Decimal.uint) : Q := Q_of_nat (Nat.of_uint x). - Definition uint_of_Q (x : Q) : option Decimal.uint - := option_map Nat.to_uint (nat_of_Q x). + Definition Q_of_uint (x : Numeral.uint) : Q := Q_of_nat (Nat.of_num_uint x). + Definition uint_of_Q (x : Q) : option Numeral.uint + := option_map Nat.to_num_uint (nat_of_Q x). Numeral Notation Q Q_of_uint uint_of_Q : Q_scope. @@ -411,8 +411,8 @@ Module Test20. Record > ty := { t : Type ; kt : known_type t }. - Definition ty_of_uint (x : Decimal.uint) : option ty - := match Nat.of_uint x with + Definition ty_of_uint (x : Numeral.uint) : option ty + := match Nat.of_num_uint x with | 0 => @Some ty zero | 1 => @Some ty one | 2 => @Some ty two @@ -421,8 +421,8 @@ Module Test20. | 5 => @Some ty type | _ => None end. - Definition uint_of_ty (x : ty) : Decimal.uint - := Nat.to_uint match kt x with + Definition uint_of_ty (x : ty) : Numeral.uint + := Nat.to_num_uint match kt x with | prop => 3 | set => 4 | type => 5 diff --git a/test-suite/output/QArithSyntax.out b/test-suite/output/QArithSyntax.out index fe6a1d25c6..9b5c076cb4 100644 --- a/test-suite/output/QArithSyntax.out +++ b/test-suite/output/QArithSyntax.out @@ -12,3 +12,15 @@ eq_refl : -1e-4 = -1e-4 : -1e-4 = -1e-4 eq_refl : -0.50 = -0.50 : -0.50 = -0.50 +eq_refl : -26 = -26 + : -26 = -26 +eq_refl : 2860 # 256 = 2860 # 256 + : 2860 # 256 = 2860 # 256 +eq_refl : -6882 = -6882 + : -6882 = -6882 +eq_refl : 2860 # 64 = 2860 # 64 + : 2860 # 64 = 2860 # 64 +eq_refl : 2860 = 2860 + : 2860 = 2860 +eq_refl : -2860 # 1024 = -2860 # 1024 + : -2860 # 1024 = -2860 # 1024 diff --git a/test-suite/output/QArithSyntax.v b/test-suite/output/QArithSyntax.v index 2f2ee0134a..b5c6222bba 100644 --- a/test-suite/output/QArithSyntax.v +++ b/test-suite/output/QArithSyntax.v @@ -7,3 +7,9 @@ Check (eq_refl : 1.02e+02 = 102 # 1). Check (eq_refl : 10.2e-1 = 1.02). Check (eq_refl : -0.0001 = -1 # 10000). Check (eq_refl : -0.50 = - 50 # 100). +Check (eq_refl : -0x1a = - 26 # 1). +Check (eq_refl : 0xb.2c = 2860 # 256). +Check (eq_refl : -0x1ae2 = -6882). +Check (eq_refl : 0xb.2cp2 = 2860 # 64). +Check (eq_refl : 0xb.2cp8 = 2860). +Check (eq_refl : -0xb.2cp-2 = -2860 # 1024). diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out index 1685964b0f..a9386b2781 100644 --- a/test-suite/output/RealSyntax.out +++ b/test-suite/output/RealSyntax.out @@ -20,3 +20,18 @@ eq_refl : -1e-4 = -1e-4 : -1e-4 = -1e-4 eq_refl : -0.50 = -0.50 : -0.50 = -0.50 +eq_refl : -26 = -26 + : -26 = -26 +eq_refl : 2860 / IZR (BinIntDef.Z.pow_pos 2 8) = 2860 / IZR (Z.pow_pos 2 8) + : 2860 / IZR (BinIntDef.Z.pow_pos 2 8) = 2860 / IZR (Z.pow_pos 2 8) +eq_refl : -6882 = -6882 + : -6882 = -6882 +eq_refl : 2860 / IZR (BinIntDef.Z.pow_pos 2 6) = 2860 / IZR (Z.pow_pos 2 6) + : 2860 / IZR (BinIntDef.Z.pow_pos 2 6) = 2860 / IZR (Z.pow_pos 2 6) +eq_refl : 2860 = 2860 + : 2860 = 2860 +eq_refl +: +-2860 / IZR (BinIntDef.Z.pow_pos 2 10) = - (2860) / IZR (Z.pow_pos 2 10) + : -2860 / IZR (BinIntDef.Z.pow_pos 2 10) = + - (2860) / IZR (Z.pow_pos 2 10) diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v index e5f9d06316..69ce3ef5f9 100644 --- a/test-suite/output/RealSyntax.v +++ b/test-suite/output/RealSyntax.v @@ -14,6 +14,12 @@ Check (eq_refl : 1.02e+02 = IZR 102). Check (eq_refl : 10.2e-1 = 1.02). Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)). Check (eq_refl : -0.50 = IZR (-50) / IZR (Z.pow_pos 10 2)). +Check (eq_refl : -0x1a = - 26). +Check (eq_refl : 0xb.2c = IZR 2860 / IZR (Z.pow_pos 2 8)). +Check (eq_refl : -0x1ae2 = -6882). +Check (eq_refl : 0xb.2cp2 = IZR 2860 / IZR (Z.pow_pos 2 6)). +Check (eq_refl : 0xb.2cp8 = 2860). +Check (eq_refl : -0xb.2cp-2 = - IZR 2860 / IZR (Z.pow_pos 2 10)). Require Import Reals. diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 593d0c7f67..c01f4b2e19 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -21,57 +21,113 @@ le_sind: (use "About" for full details on implicit arguments) false: bool true: bool -eq_true: bool -> Prop is_true: bool -> Prop +eq_true: bool -> Prop negb: bool -> bool +xorb: bool -> bool -> bool andb: bool -> bool -> bool orb: bool -> bool -> bool implb: bool -> bool -> bool -xorb: bool -> bool -> bool -Nat.even: nat -> bool Nat.odd: nat -> bool +Nat.even: nat -> bool BoolSpec: Prop -> Prop -> bool -> Prop -Nat.ltb: nat -> nat -> bool -Nat.testbit: nat -> nat -> bool +Numeral.numeral_beq: Numeral.numeral -> Numeral.numeral -> bool Nat.eqb: nat -> nat -> bool +Nat.testbit: nat -> nat -> bool +Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool +Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool +Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool +Hexadecimal.hexadecimal_beq: + Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool +Numeral.int_beq: Numeral.int -> Numeral.int -> bool +Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool +Nat.ltb: nat -> nat -> bool Nat.leb: nat -> nat -> bool +Hexadecimal.int_beq: Hexadecimal.int -> Hexadecimal.int -> bool +Decimal.int_beq: Decimal.int -> Decimal.int -> bool Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat +eq_true_rec_r: + forall (P : bool -> Set) [b : bool], P b -> eq_true b -> P true +eq_true_ind: + forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b +eq_true_rect_r: + forall (P : bool -> Type) [b : bool], P b -> eq_true b -> P true +bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b eq_true_ind_r: forall (P : bool -> Prop) [b : bool], P b -> eq_true b -> P true +eq_true_rect: + forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b +bool_sind: + forall P : bool -> SProp, P true -> P false -> forall b : bool, P b eq_true_rec: forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b -eq_true_rect: - forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b eq_true_sind: forall P : bool -> SProp, P true -> forall b : bool, eq_true b -> P b -bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b -eq_true_ind: - forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b -eq_true_rec_r: - forall (P : bool -> Set) [b : bool], P b -> eq_true b -> P true -eq_true_rect_r: - forall (P : bool -> Type) [b : bool], P b -> eq_true b -> P true -bool_sind: - forall P : bool -> SProp, P true -> P false -> forall b : bool, P b -Byte.to_bits: - Byte.byte -> - bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) +Numeral.internal_uint_dec_bl1: + forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y +Hexadecimal.internal_hexadecimal_dec_lb: + forall x y : Hexadecimal.hexadecimal, + x = y -> Hexadecimal.hexadecimal_beq x y = true +Hexadecimal.internal_int_dec_lb0: + forall x y : Hexadecimal.int, x = y -> Hexadecimal.int_beq x y = true +Numeral.internal_numeral_dec_lb: + forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true +Decimal.internal_decimal_dec_lb: + forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true +Hexadecimal.internal_int_dec_bl0: + forall x y : Hexadecimal.int, Hexadecimal.int_beq x y = true -> x = y +Numeral.internal_int_dec_lb1: + forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true +Numeral.internal_int_dec_bl1: + forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y +Hexadecimal.internal_hexadecimal_dec_bl: + forall x y : Hexadecimal.hexadecimal, + Hexadecimal.hexadecimal_beq x y = true -> x = y +Numeral.internal_uint_dec_lb1: + forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true +Decimal.internal_int_dec_bl: + forall x y : Decimal.int, Decimal.int_beq x y = true -> x = y +Decimal.internal_int_dec_lb: + forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true +Numeral.internal_numeral_dec_bl: + forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y Byte.of_bits: bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) -> Byte.byte +Byte.to_bits: + Byte.byte -> + bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) +Decimal.internal_decimal_dec_bl: + forall x y : Decimal.decimal, Decimal.decimal_beq x y = true -> x = y +Hexadecimal.internal_uint_dec_bl0: + forall x : Hexadecimal.uint, + (fun x0 : Hexadecimal.uint => + forall y : Hexadecimal.uint, Hexadecimal.uint_beq x0 y = true -> x0 = y) x +Decimal.internal_uint_dec_bl: + forall x : Decimal.uint, + (fun x0 : Decimal.uint => + forall y : Decimal.uint, Decimal.uint_beq x0 y = true -> x0 = y) x +Decimal.internal_uint_dec_lb: + forall x : Decimal.uint, + (fun x0 : Decimal.uint => + forall y : Decimal.uint, x0 = y -> Decimal.uint_beq x0 y = true) x +Hexadecimal.internal_uint_dec_lb0: + forall x : Hexadecimal.uint, + (fun x0 : Hexadecimal.uint => + forall y : Hexadecimal.uint, x0 = y -> Hexadecimal.uint_beq x0 y = true) x andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true andb_true_intro: forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true -BoolSpec_sind: - forall [P Q : Prop] (P0 : bool -> SProp), - (P -> P0 true) -> - (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b BoolSpec_ind: forall [P Q : Prop] (P0 : bool -> Prop), (P -> P0 true) -> (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b +BoolSpec_sind: + forall [P Q : Prop] (P0 : bool -> SProp), + (P -> P0 true) -> + (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b Byte.to_bits_of_bits: forall b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))), @@ -107,14 +163,106 @@ f_equal2_nat: forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2 (use "About" for full details on implicit arguments) +Numeral.internal_numeral_dec_lb: + forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true +Numeral.internal_int_dec_lb1: + forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true +Numeral.internal_numeral_dec_bl: + forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y +Hexadecimal.internal_hexadecimal_dec_lb: + forall x y : Hexadecimal.hexadecimal, + x = y -> Hexadecimal.hexadecimal_beq x y = true +Numeral.internal_int_dec_bl1: + forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y +Numeral.internal_uint_dec_lb1: + forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true +Numeral.internal_uint_dec_bl1: + forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y +Decimal.internal_decimal_dec_lb: + forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true +Hexadecimal.internal_hexadecimal_dec_bl: + forall x y : Hexadecimal.hexadecimal, + Hexadecimal.hexadecimal_beq x y = true -> x = y +Hexadecimal.internal_int_dec_lb0: + forall x y : Hexadecimal.int, x = y -> Hexadecimal.int_beq x y = true +Hexadecimal.internal_int_dec_bl0: + forall x y : Hexadecimal.int, Hexadecimal.int_beq x y = true -> x = y +Decimal.internal_int_dec_lb: + forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true +Decimal.internal_decimal_dec_bl: + forall x y : Decimal.decimal, Decimal.decimal_beq x y = true -> x = y +Decimal.internal_int_dec_bl: + forall x y : Decimal.int, Decimal.int_beq x y = true -> x = y +Decimal.internal_uint_dec_bl: + forall x : Decimal.uint, + (fun x0 : Decimal.uint => + forall y : Decimal.uint, Decimal.uint_beq x0 y = true -> x0 = y) x +Decimal.internal_uint_dec_lb: + forall x : Decimal.uint, + (fun x0 : Decimal.uint => + forall y : Decimal.uint, x0 = y -> Decimal.uint_beq x0 y = true) x +Hexadecimal.internal_uint_dec_lb0: + forall x : Hexadecimal.uint, + (fun x0 : Hexadecimal.uint => + forall y : Hexadecimal.uint, x0 = y -> Hexadecimal.uint_beq x0 y = true) x +Hexadecimal.internal_uint_dec_bl0: + forall x : Hexadecimal.uint, + (fun x0 : Hexadecimal.uint => + forall y : Hexadecimal.uint, Hexadecimal.uint_beq x0 y = true -> x0 = y) x +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true andb_true_intro: forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true -andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true bool_choice: forall [S : Set] [R1 R2 : S -> Prop], (forall x : S, {R1 x} + {R2 x}) -> {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} (use "About" for full details on implicit arguments) +Numeral.internal_numeral_dec_lb: + forall x y : Numeral.numeral, x = y -> Numeral.numeral_beq x y = true +Numeral.internal_numeral_dec_bl: + forall x y : Numeral.numeral, Numeral.numeral_beq x y = true -> x = y +Numeral.internal_int_dec_lb1: + forall x y : Numeral.int, x = y -> Numeral.int_beq x y = true +Numeral.internal_int_dec_bl1: + forall x y : Numeral.int, Numeral.int_beq x y = true -> x = y +Numeral.internal_uint_dec_lb1: + forall x y : Numeral.uint, x = y -> Numeral.uint_beq x y = true +Numeral.internal_uint_dec_bl1: + forall x y : Numeral.uint, Numeral.uint_beq x y = true -> x = y +Hexadecimal.internal_hexadecimal_dec_lb: + forall x y : Hexadecimal.hexadecimal, + x = y -> Hexadecimal.hexadecimal_beq x y = true +Hexadecimal.internal_hexadecimal_dec_bl: + forall x y : Hexadecimal.hexadecimal, + Hexadecimal.hexadecimal_beq x y = true -> x = y +Hexadecimal.internal_int_dec_lb0: + forall x y : Hexadecimal.int, x = y -> Hexadecimal.int_beq x y = true +Hexadecimal.internal_int_dec_bl0: + forall x y : Hexadecimal.int, Hexadecimal.int_beq x y = true -> x = y +Decimal.internal_decimal_dec_lb: + forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true +Decimal.internal_decimal_dec_bl: + forall x y : Decimal.decimal, Decimal.decimal_beq x y = true -> x = y +Decimal.internal_int_dec_lb: + forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true +Decimal.internal_int_dec_bl: + forall x y : Decimal.int, Decimal.int_beq x y = true -> x = y +Hexadecimal.internal_uint_dec_bl0: + forall x : Hexadecimal.uint, + (fun x0 : Hexadecimal.uint => + forall y : Hexadecimal.uint, Hexadecimal.uint_beq x0 y = true -> x0 = y) x +Decimal.internal_uint_dec_bl: + forall x : Decimal.uint, + (fun x0 : Decimal.uint => + forall y : Decimal.uint, Decimal.uint_beq x0 y = true -> x0 = y) x +Decimal.internal_uint_dec_lb: + forall x : Decimal.uint, + (fun x0 : Decimal.uint => + forall y : Decimal.uint, x0 = y -> Decimal.uint_beq x0 y = true) x +Hexadecimal.internal_uint_dec_lb0: + forall x : Hexadecimal.uint, + (fun x0 : Hexadecimal.uint => + forall y : Hexadecimal.uint, x0 = y -> Hexadecimal.uint_beq x0 y = true) x andb_true_intro: forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out index 5627e4bd3c..d42dc575c2 100644 --- a/test-suite/output/SearchHead.out +++ b/test-suite/output/SearchHead.out @@ -8,16 +8,26 @@ le_S_n: forall n m : nat, S n <= S m -> n <= m false: bool true: bool negb: bool -> bool -implb: bool -> bool -> bool -orb: bool -> bool -> bool -andb: bool -> bool -> bool xorb: bool -> bool -> bool -Nat.even: nat -> bool +andb: bool -> bool -> bool +orb: bool -> bool -> bool +implb: bool -> bool -> bool Nat.odd: nat -> bool -Nat.leb: nat -> nat -> bool -Nat.ltb: nat -> nat -> bool +Nat.even: nat -> bool +Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool +Hexadecimal.hexadecimal_beq: + Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool +Nat.ltb: nat -> nat -> bool +Nat.leb: nat -> nat -> bool +Numeral.numeral_beq: Numeral.numeral -> Numeral.numeral -> bool +Numeral.int_beq: Numeral.int -> Numeral.int -> bool +Hexadecimal.int_beq: Hexadecimal.int -> Hexadecimal.int -> bool +Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool +Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool +Decimal.int_beq: Decimal.int -> Decimal.int -> bool +Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool (use "About" for full details on implicit arguments) mult_n_O: forall n : nat, 0 = n * 0 plus_O_n: forall n : nat, 0 + n = n diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index 36fc1a5914..13d0a9e55b 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -1,47 +1,61 @@ false: bool true: bool negb: bool -> bool -implb: bool -> bool -> bool -orb: bool -> bool -> bool -andb: bool -> bool -> bool xorb: bool -> bool -> bool -Nat.even: nat -> bool +andb: bool -> bool -> bool +orb: bool -> bool -> bool +implb: bool -> bool -> bool Nat.odd: nat -> bool -Nat.leb: nat -> nat -> bool -Nat.ltb: nat -> nat -> bool +Nat.even: nat -> bool +Numeral.uint_beq: Numeral.uint -> Numeral.uint -> bool Nat.testbit: nat -> nat -> bool Nat.eqb: nat -> nat -> bool +Hexadecimal.hexadecimal_beq: + Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool +Nat.ltb: nat -> nat -> bool +Nat.leb: nat -> nat -> bool +Numeral.numeral_beq: Numeral.numeral -> Numeral.numeral -> bool +Numeral.int_beq: Numeral.int -> Numeral.int -> bool +Hexadecimal.int_beq: Hexadecimal.int -> Hexadecimal.int -> bool +Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool +Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool +Decimal.int_beq: Decimal.int -> Decimal.int -> bool +Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool (use "About" for full details on implicit arguments) Nat.two: nat -Nat.one: nat Nat.zero: nat +Nat.one: nat O: nat +Nat.double: nat -> nat +Nat.sqrt: nat -> nat Nat.div2: nat -> nat Nat.log2: nat -> nat -Nat.succ: nat -> nat -Nat.sqrt: nat -> nat -S: nat -> nat Nat.pred: nat -> nat -Nat.double: nat -> nat Nat.square: nat -> nat +S: nat -> nat +Nat.succ: nat -> nat +Nat.ldiff: nat -> nat -> nat +Nat.add: nat -> nat -> nat Nat.land: nat -> nat -> nat -Nat.lor: nat -> nat -> nat +Nat.lxor: nat -> nat -> nat +Nat.sub: nat -> nat -> nat Nat.mul: nat -> nat -> nat Nat.tail_mul: nat -> nat -> nat -Nat.div: nat -> nat -> nat -Nat.tail_add: nat -> nat -> nat -Nat.gcd: nat -> nat -> nat -Nat.modulo: nat -> nat -> nat Nat.max: nat -> nat -> nat -Nat.sub: nat -> nat -> nat +Nat.tail_add: nat -> nat -> nat Nat.pow: nat -> nat -> nat -Nat.lxor: nat -> nat -> nat -Nat.ldiff: nat -> nat -> nat Nat.min: nat -> nat -> nat -Nat.add: nat -> nat -> nat +Nat.modulo: nat -> nat -> nat +Nat.div: nat -> nat -> nat +Nat.lor: nat -> nat -> nat +Nat.gcd: nat -> nat -> nat +Hexadecimal.nb_digits: Hexadecimal.uint -> nat +Nat.of_hex_uint: Hexadecimal.uint -> nat +Nat.of_num_uint: Numeral.uint -> nat Nat.of_uint: Decimal.uint -> nat Decimal.nb_digits: Decimal.uint -> nat Nat.tail_addmul: nat -> nat -> nat -> nat +Nat.of_hex_uint_acc: Hexadecimal.uint -> nat -> nat Nat.of_uint_acc: Decimal.uint -> nat -> nat Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat @@ -53,29 +67,30 @@ Nat.div2: nat -> nat Nat.sqrt: nat -> nat Nat.log2: nat -> nat Nat.double: nat -> nat -Nat.pred: nat -> nat +S: nat -> nat Nat.square: nat -> nat Nat.succ: nat -> nat -S: nat -> nat +Nat.pred: nat -> nat +Nat.land: nat -> nat -> nat +Nat.max: nat -> nat -> nat +Nat.gcd: nat -> nat -> nat +Nat.modulo: nat -> nat -> nat Nat.ldiff: nat -> nat -> nat +Nat.tail_add: nat -> nat -> nat Nat.pow: nat -> nat -> nat -Nat.land: nat -> nat -> nat Nat.lxor: nat -> nat -> nat Nat.div: nat -> nat -> nat Nat.lor: nat -> nat -> nat -Nat.tail_mul: nat -> nat -> nat -Nat.modulo: nat -> nat -> nat -Nat.sub: nat -> nat -> nat Nat.mul: nat -> nat -> nat -Nat.gcd: nat -> nat -> nat -Nat.max: nat -> nat -> nat -Nat.tail_add: nat -> nat -> nat -Nat.add: nat -> nat -> nat Nat.min: nat -> nat -> nat +Nat.add: nat -> nat -> nat +Nat.sub: nat -> nat -> nat +Nat.tail_mul: nat -> nat -> nat Nat.tail_addmul: nat -> nat -> nat -> nat Nat.of_uint_acc: Decimal.uint -> nat -> nat -Nat.log2_iter: nat -> nat -> nat -> nat -> nat +Nat.of_hex_uint_acc: Hexadecimal.uint -> nat -> nat Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat +Nat.log2_iter: nat -> nat -> nat -> nat -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat (use "About" for full details on implicit arguments) mult_n_Sm: forall n m : nat, n * m + n = n * S m diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out index dc41b0aa48..c3f2fb5b42 100644 --- a/test-suite/output/ZSyntax.out +++ b/test-suite/output/ZSyntax.out @@ -1,5 +1,7 @@ 32%Z : Z +eq_refl : 42%Z = 42%Z + : 42%Z = 42%Z fun f : nat -> Z => (f 0%nat + 0)%Z : (nat -> Z) -> Z fun x : positive => Z.pos x~0 @@ -24,3 +26,9 @@ Z.of_nat 0 = 0%Z : Prop (0 + Z.of_nat 11)%Z : Z +0x2a%Z + : Z +(-0x2a)%Z + : Z +0x0%Z + : Z diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v index d3640cae44..be9dc543d6 100644 --- a/test-suite/output/ZSyntax.v +++ b/test-suite/output/ZSyntax.v @@ -1,5 +1,6 @@ Require Import ZArith. Check 32%Z. +Check (eq_refl : 0x2a%Z = 42%Z). Check (fun f : nat -> Z => (f 0%nat + 0)%Z). Check (fun x : positive => Zpos (xO x)). Check (fun x : positive => (Zpos x + 1)%Z). @@ -15,3 +16,10 @@ Check (Z.of_nat 0 = 0%Z). (* Submitted by Pierre Casteran *) Require Import Arith. Check (0 + Z.of_nat 11)%Z. + +(* Check hexadecimal printing *) +Definition to_num_int n := Numeral.IntHex (Z.to_hex_int n). +Numeral Notation Z Z.of_num_int to_num_int : Z_scope. +Check 42%Z. +Check (-42)%Z. +Check 0%Z. diff --git a/test-suite/output/bug_12159.v b/test-suite/output/bug_12159.v index 91d66f7f4c..6ea90eab29 100644 --- a/test-suite/output/bug_12159.v +++ b/test-suite/output/bug_12159.v @@ -2,10 +2,10 @@ Declare Scope A. Declare Scope B. Delimit Scope A with A. Delimit Scope B with B. -Definition to_unit (v : Decimal.uint) : option unit - := match Nat.of_uint v with O => Some tt | _ => None end. -Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0. -Definition of_unit' (v : unit) : Decimal.uint := Nat.to_uint 1. +Definition to_unit (v : Numeral.uint) : option unit + := match Nat.of_num_uint v with O => Some tt | _ => None end. +Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0. +Definition of_unit' (v : unit) : Numeral.uint := Nat.to_num_uint 1. Numeral Notation unit to_unit of_unit : A. Numeral Notation unit to_unit of_unit' : B. Definition f x : unit := x. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 9f77221d5a..f789e966f5 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -154,6 +154,9 @@ Inductive nat : Set := | O : nat | S : nat -> nat. +Declare Scope hex_nat_scope. +Delimit Scope hex_nat_scope with xnat. + Declare Scope nat_scope. Delimit Scope nat_scope with nat. Bind Scope nat_scope with nat. diff --git a/theories/Init/Hexadecimal.v b/theories/Init/Hexadecimal.v new file mode 100644 index 0000000000..a4ddad2875 --- /dev/null +++ b/theories/Init/Hexadecimal.v @@ -0,0 +1,245 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * Hexadecimal numbers *) + +(** These numbers coded in base 16 will be used for parsing and printing + other Coq numeral datatypes in an human-readable way. + See the [Numeral Notation] command. + We represent numbers in base 16 as lists of hexadecimal digits, + in big-endian order (most significant digit comes first). *) + +Require Import Datatypes Specif Decimal. + +(** Unsigned integers are just lists of digits. + For instance, sixteen is (D1 (D0 Nil)) *) + +Inductive uint := + | Nil + | D0 (_:uint) + | D1 (_:uint) + | D2 (_:uint) + | D3 (_:uint) + | D4 (_:uint) + | D5 (_:uint) + | D6 (_:uint) + | D7 (_:uint) + | D8 (_:uint) + | D9 (_:uint) + | Da (_:uint) + | Db (_:uint) + | Dc (_:uint) + | Dd (_:uint) + | De (_:uint) + | Df (_:uint). + +(** [Nil] is the number terminator. Taken alone, it behaves as zero, + but rather use [D0 Nil] instead, since this form will be denoted + as [0], while [Nil] will be printed as [Nil]. *) + +Notation zero := (D0 Nil). + +(** For signed integers, we use two constructors [Pos] and [Neg]. *) + +Variant int := Pos (d:uint) | Neg (d:uint). + +(** For decimal numbers, we use two constructors [Hexadecimal] and + [HexadecimalExp], depending on whether or not they are given with an + exponent (e.g., 0x1.a2p+01). [i] is the integral part while [f] is + the fractional part (beware that leading zeroes do matter). *) + +Variant hexadecimal := + | Hexadecimal (i:int) (f:uint) + | HexadecimalExp (i:int) (f:uint) (e:Decimal.int). + +Scheme Equality for uint. +Scheme Equality for int. +Scheme Equality for hexadecimal. + +Declare Scope hex_uint_scope. +Delimit Scope hex_uint_scope with huint. +Bind Scope hex_uint_scope with uint. + +Declare Scope hex_int_scope. +Delimit Scope hex_int_scope with hint. +Bind Scope hex_int_scope with int. + +Register uint as num.hexadecimal_uint.type. +Register int as num.hexadecimal_int.type. +Register hexadecimal as num.hexadecimal.type. + +Fixpoint nb_digits d := + match d with + | Nil => O + | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d + | Da d | Db d | Dc d | Dd d | De d | Df d => + S (nb_digits d) + end. + +(** This representation favors simplicity over canonicity. + For normalizing numbers, we need to remove head zero digits, + and choose our canonical representation of 0 (here [D0 Nil] + for unsigned numbers and [Pos (D0 Nil)] for signed numbers). *) + +(** [nzhead] removes all head zero digits *) + +Fixpoint nzhead d := + match d with + | D0 d => nzhead d + | _ => d + end. + +(** [unorm] : normalization of unsigned integers *) + +Definition unorm d := + match nzhead d with + | Nil => zero + | d => d + end. + +(** [norm] : normalization of signed integers *) + +Definition norm d := + match d with + | Pos d => Pos (unorm d) + | Neg d => + match nzhead d with + | Nil => Pos zero + | d => Neg d + end + end. + +(** A few easy operations. For more advanced computations, use the conversions + with other Coq numeral datatypes (e.g. Z) and the operations on them. *) + +Definition opp (d:int) := + match d with + | Pos d => Neg d + | Neg d => Pos d + end. + +(** For conversions with binary numbers, it is easier to operate + on little-endian numbers. *) + +Fixpoint revapp (d d' : uint) := + match d with + | Nil => d' + | D0 d => revapp d (D0 d') + | D1 d => revapp d (D1 d') + | D2 d => revapp d (D2 d') + | D3 d => revapp d (D3 d') + | D4 d => revapp d (D4 d') + | D5 d => revapp d (D5 d') + | D6 d => revapp d (D6 d') + | D7 d => revapp d (D7 d') + | D8 d => revapp d (D8 d') + | D9 d => revapp d (D9 d') + | Da d => revapp d (Da d') + | Db d => revapp d (Db d') + | Dc d => revapp d (Dc d') + | Dd d => revapp d (Dd d') + | De d => revapp d (De d') + | Df d => revapp d (Df d') + end. + +Definition rev d := revapp d Nil. + +Definition app d d' := revapp (rev d) d'. + +Definition app_int d1 d2 := + match d1 with Pos d1 => Pos (app d1 d2) | Neg d1 => Neg (app d1 d2) end. + +(** [nztail] removes all trailing zero digits and return both the + result and the number of removed digits. *) + +Definition nztail d := + let fix aux d_rev := + match d_rev with + | D0 d_rev => let (r, n) := aux d_rev in pair r (S n) + | _ => pair d_rev O + end in + let (r, n) := aux (rev d) in pair (rev r) n. + +Definition nztail_int d := + match d with + | Pos d => let (r, n) := nztail d in pair (Pos r) n + | Neg d => let (r, n) := nztail d in pair (Neg r) n + end. + +Module Little. + +(** Successor of little-endian numbers *) + +Fixpoint succ d := + match d with + | Nil => D1 Nil + | D0 d => D1 d + | D1 d => D2 d + | D2 d => D3 d + | D3 d => D4 d + | D4 d => D5 d + | D5 d => D6 d + | D6 d => D7 d + | D7 d => D8 d + | D8 d => D9 d + | D9 d => Da d + | Da d => Db d + | Db d => Dc d + | Dc d => Dd d + | Dd d => De d + | De d => Df d + | Df d => D0 (succ d) + end. + +(** Doubling little-endian numbers *) + +Fixpoint double d := + match d with + | Nil => Nil + | D0 d => D0 (double d) + | D1 d => D2 (double d) + | D2 d => D4 (double d) + | D3 d => D6 (double d) + | D4 d => D8 (double d) + | D5 d => Da (double d) + | D6 d => Dc (double d) + | D7 d => De (double d) + | D8 d => D0 (succ_double d) + | D9 d => D2 (succ_double d) + | Da d => D4 (succ_double d) + | Db d => D6 (succ_double d) + | Dc d => D8 (succ_double d) + | Dd d => Da (succ_double d) + | De d => Dc (succ_double d) + | Df d => De (succ_double d) + end + +with succ_double d := + match d with + | Nil => D1 Nil + | D0 d => D1 (double d) + | D1 d => D3 (double d) + | D2 d => D5 (double d) + | D3 d => D7 (double d) + | D4 d => D9 (double d) + | D5 d => Db (double d) + | D6 d => Dd (double d) + | D7 d => Df (double d) + | D8 d => D1 (succ_double d) + | D9 d => D3 (succ_double d) + | Da d => D5 (succ_double d) + | Db d => D7 (succ_double d) + | Dc d => D9 (succ_double d) + | Dd d => Db (succ_double d) + | De d => Dd (succ_double d) + | Df d => Df (succ_double d) + end. + +End Little. diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v index bfd41c5017..7c8cf0b536 100644 --- a/theories/Init/Nat.v +++ b/theories/Init/Nat.v @@ -9,7 +9,7 @@ (************************************************************************) Require Import Notations Logic Datatypes. -Require Decimal. +Require Decimal Hexadecimal Numeral. Local Open Scope nat_scope. (**********************************************************************) @@ -187,6 +187,37 @@ Fixpoint of_uint_acc (d:Decimal.uint)(acc:nat) := Definition of_uint (d:Decimal.uint) := of_uint_acc d O. +Local Notation sixteen := (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))). + +Fixpoint of_hex_uint_acc (d:Hexadecimal.uint)(acc:nat) := + match d with + | Hexadecimal.Nil => acc + | Hexadecimal.D0 d => of_hex_uint_acc d (tail_mul sixteen acc) + | Hexadecimal.D1 d => of_hex_uint_acc d (S (tail_mul sixteen acc)) + | Hexadecimal.D2 d => of_hex_uint_acc d (S (S (tail_mul sixteen acc))) + | Hexadecimal.D3 d => of_hex_uint_acc d (S (S (S (tail_mul sixteen acc)))) + | Hexadecimal.D4 d => of_hex_uint_acc d (S (S (S (S (tail_mul sixteen acc))))) + | Hexadecimal.D5 d => of_hex_uint_acc d (S (S (S (S (S (tail_mul sixteen acc)))))) + | Hexadecimal.D6 d => of_hex_uint_acc d (S (S (S (S (S (S (tail_mul sixteen acc))))))) + | Hexadecimal.D7 d => of_hex_uint_acc d (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))) + | Hexadecimal.D8 d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))) + | Hexadecimal.D9 d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))) + | Hexadecimal.Da d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))) + | Hexadecimal.Db d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))) + | Hexadecimal.Dc d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))) + | Hexadecimal.Dd d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))))) + | Hexadecimal.De d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))))) + | Hexadecimal.Df d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))))))) + end. + +Definition of_hex_uint (d:Hexadecimal.uint) := of_hex_uint_acc d O. + +Definition of_num_uint (d:Numeral.uint) := + match d with + | Numeral.UIntDec d => of_uint d + | Numeral.UIntHex d => of_hex_uint d + end. + Fixpoint to_little_uint n acc := match n with | O => acc @@ -196,14 +227,43 @@ Fixpoint to_little_uint n acc := Definition to_uint n := Decimal.rev (to_little_uint n Decimal.zero). +Fixpoint to_little_hex_uint n acc := + match n with + | O => acc + | S n => to_little_hex_uint n (Hexadecimal.Little.succ acc) + end. + +Definition to_hex_uint n := + Hexadecimal.rev (to_little_hex_uint n Hexadecimal.zero). + +Definition to_num_uint n := Numeral.UIntDec (to_uint n). + +Definition to_num_hex_uint n := Numeral.UIntHex (to_hex_uint n). + Definition of_int (d:Decimal.int) : option nat := match Decimal.norm d with | Decimal.Pos u => Some (of_uint u) | _ => None end. +Definition of_hex_int (d:Hexadecimal.int) : option nat := + match Hexadecimal.norm d with + | Hexadecimal.Pos u => Some (of_hex_uint u) + | _ => None + end. + +Definition of_num_int (d:Numeral.int) : option nat := + match d with + | Numeral.IntDec d => of_int d + | Numeral.IntHex d => of_hex_int d + end. + Definition to_int n := Decimal.Pos (to_uint n). +Definition to_hex_int n := Hexadecimal.Pos (to_hex_uint n). + +Definition to_num_int n := Numeral.IntDec (to_int n). + (** ** Euclidean division *) (** This division is linear and tail-recursive. diff --git a/theories/Init/Numeral.v b/theories/Init/Numeral.v new file mode 100644 index 0000000000..8a0531e004 --- /dev/null +++ b/theories/Init/Numeral.v @@ -0,0 +1,33 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * Decimal or Hexadecimal numbers *) + +Require Import Decimal Hexadecimal. + +Variant uint := UIntDec (u:Decimal.uint) | UIntHex (u:Hexadecimal.uint). + +Variant int := IntDec (i:Decimal.int) | IntHex (i:Hexadecimal.int). + +Variant numeral := Dec (d:Decimal.decimal) | Hex (h:Hexadecimal.hexadecimal). + +Scheme Equality for uint. +Scheme Equality for int. +Scheme Equality for numeral. + +Register uint as num.num_uint.type. +Register int as num.num_int.type. +Register numeral as num.numeral.type. + +(** Pseudo-conversion functions used when declaring + Numeral Notations on [uint] and [int]. *) + +Definition uint_of_uint (i:uint) := i. +Definition int_of_int (i:int) := i. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 6a81517d7e..8f862e8cec 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -15,6 +15,8 @@ Require Export Datatypes. Require Export Specif. Require Coq.Init.Byte. Require Coq.Init.Decimal. +Require Coq.Init.Hexadecimal. +Require Coq.Init.Numeral. Require Coq.Init.Nat. Require Export Peano. Require Export Coq.Init.Wf. @@ -30,16 +32,25 @@ Declare ML Module "ground_plugin". Declare ML Module "numeral_notation_plugin". Declare ML Module "string_notation_plugin". +(* Parsing / printing of hexadecimal numbers *) +Arguments Nat.of_hex_uint d%hex_uint_scope. +Arguments Nat.of_hex_int d%hex_int_scope. +Numeral Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint + : hex_uint_scope. +Numeral Notation Numeral.int Numeral.int_of_int Numeral.int_of_int + : hex_int_scope. + (* Parsing / printing of decimal numbers *) Arguments Nat.of_uint d%dec_uint_scope. Arguments Nat.of_int d%dec_int_scope. -Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint +Numeral Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint : dec_uint_scope. -Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int +Numeral Notation Numeral.int Numeral.int_of_int Numeral.int_of_int : dec_int_scope. (* Parsing / printing of [nat] numbers *) -Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5001). +Numeral Notation nat Nat.of_num_uint Nat.to_num_hex_uint : hex_nat_scope (abstract after 5001). +Numeral Notation nat Nat.of_num_uint Nat.to_num_uint : nat_scope (abstract after 5001). (* Printing/Parsing of bytes *) Export Byte.ByteSyntaxNotations. diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index d68c32b371..1881e387a2 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -1007,7 +1007,7 @@ Bind Scope N_scope with N.t N. (** Exportation of notations *) -Numeral Notation N N.of_uint N.to_uint : N_scope. +Numeral Notation N N.of_num_uint N.to_num_uint : N_scope. Infix "+" := N.add : N_scope. Infix "-" := N.sub : N_scope. diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 04685cc3eb..8a0aee9cf4 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -388,23 +388,55 @@ Definition iter (n:N) {A} (f:A->A) (x:A) : A := Definition of_uint (d:Decimal.uint) := Pos.of_uint d. +Definition of_hex_uint (d:Hexadecimal.uint) := Pos.of_hex_uint d. + +Definition of_num_uint (d:Numeral.uint) := + match d with + | Numeral.UIntDec d => of_uint d + | Numeral.UIntHex d => of_hex_uint d + end. + Definition of_int (d:Decimal.int) := match Decimal.norm d with | Decimal.Pos d => Some (Pos.of_uint d) | Decimal.Neg _ => None end. +Definition of_hex_int (d:Hexadecimal.int) := + match Hexadecimal.norm d with + | Hexadecimal.Pos d => Some (Pos.of_hex_uint d) + | Hexadecimal.Neg _ => None + end. + +Definition of_num_int (d:Numeral.int) := + match d with + | Numeral.IntDec d => of_int d + | Numeral.IntHex d => of_hex_int d + end. + Definition to_uint n := match n with | 0 => Decimal.zero | pos p => Pos.to_uint p end. +Definition to_hex_uint n := + match n with + | 0 => Hexadecimal.zero + | pos p => Pos.to_hex_uint p + end. + +Definition to_num_uint n := Numeral.UIntDec (to_uint n). + Definition to_int n := Decimal.Pos (to_uint n). -Numeral Notation N of_uint to_uint : N_scope. +Definition to_hex_int n := Hexadecimal.Pos (to_hex_uint n). + +Definition to_num_int n := Numeral.IntDec (to_int n). + +Numeral Notation N of_num_uint to_num_uint : N_scope. End N. (** Re-export the notation for those who just [Import NatIntDef] *) -Numeral Notation N N.of_uint N.to_uint : N_scope. +Numeral Notation N N.of_num_uint N.to_num_uint : N_scope. diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 4179765dca..c8414c241d 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1886,7 +1886,7 @@ Bind Scope positive_scope with Pos.t positive. (** Exportation of notations *) -Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope. +Numeral Notation positive Pos.of_num_int Pos.to_num_uint : positive_scope. Infix "+" := Pos.add : positive_scope. Infix "-" := Pos.sub : positive_scope. diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 953068b010..cdb9af542c 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -595,6 +595,56 @@ Fixpoint of_uint (d:Decimal.uint) : N := | Decimal.D9 l => Npos (of_uint_acc l 1~0~0~1) end. +Local Notation sixteen := 1~0~0~0~0. + +Fixpoint of_hex_uint_acc (d:Hexadecimal.uint)(acc:positive) := + match d with + | Hexadecimal.Nil => acc + | Hexadecimal.D0 l => of_hex_uint_acc l (mul sixteen acc) + | Hexadecimal.D1 l => of_hex_uint_acc l (add 1 (mul sixteen acc)) + | Hexadecimal.D2 l => of_hex_uint_acc l (add 1~0 (mul sixteen acc)) + | Hexadecimal.D3 l => of_hex_uint_acc l (add 1~1 (mul sixteen acc)) + | Hexadecimal.D4 l => of_hex_uint_acc l (add 1~0~0 (mul sixteen acc)) + | Hexadecimal.D5 l => of_hex_uint_acc l (add 1~0~1 (mul sixteen acc)) + | Hexadecimal.D6 l => of_hex_uint_acc l (add 1~1~0 (mul sixteen acc)) + | Hexadecimal.D7 l => of_hex_uint_acc l (add 1~1~1 (mul sixteen acc)) + | Hexadecimal.D8 l => of_hex_uint_acc l (add 1~0~0~0 (mul sixteen acc)) + | Hexadecimal.D9 l => of_hex_uint_acc l (add 1~0~0~1 (mul sixteen acc)) + | Hexadecimal.Da l => of_hex_uint_acc l (add 1~0~1~0 (mul sixteen acc)) + | Hexadecimal.Db l => of_hex_uint_acc l (add 1~0~1~1 (mul sixteen acc)) + | Hexadecimal.Dc l => of_hex_uint_acc l (add 1~1~0~0 (mul sixteen acc)) + | Hexadecimal.Dd l => of_hex_uint_acc l (add 1~1~0~1 (mul sixteen acc)) + | Hexadecimal.De l => of_hex_uint_acc l (add 1~1~1~0 (mul sixteen acc)) + | Hexadecimal.Df l => of_hex_uint_acc l (add 1~1~1~1 (mul sixteen acc)) + end. + +Fixpoint of_hex_uint (d:Hexadecimal.uint) : N := + match d with + | Hexadecimal.Nil => N0 + | Hexadecimal.D0 l => of_hex_uint l + | Hexadecimal.D1 l => Npos (of_hex_uint_acc l 1) + | Hexadecimal.D2 l => Npos (of_hex_uint_acc l 1~0) + | Hexadecimal.D3 l => Npos (of_hex_uint_acc l 1~1) + | Hexadecimal.D4 l => Npos (of_hex_uint_acc l 1~0~0) + | Hexadecimal.D5 l => Npos (of_hex_uint_acc l 1~0~1) + | Hexadecimal.D6 l => Npos (of_hex_uint_acc l 1~1~0) + | Hexadecimal.D7 l => Npos (of_hex_uint_acc l 1~1~1) + | Hexadecimal.D8 l => Npos (of_hex_uint_acc l 1~0~0~0) + | Hexadecimal.D9 l => Npos (of_hex_uint_acc l 1~0~0~1) + | Hexadecimal.Da l => Npos (of_hex_uint_acc l 1~0~1~0) + | Hexadecimal.Db l => Npos (of_hex_uint_acc l 1~0~1~1) + | Hexadecimal.Dc l => Npos (of_hex_uint_acc l 1~1~0~0) + | Hexadecimal.Dd l => Npos (of_hex_uint_acc l 1~1~0~1) + | Hexadecimal.De l => Npos (of_hex_uint_acc l 1~1~1~0) + | Hexadecimal.Df l => Npos (of_hex_uint_acc l 1~1~1~1) + end. + +Definition of_num_uint (d:Numeral.uint) : N := + match d with + | Numeral.UIntDec d => of_uint d + | Numeral.UIntHex d => of_hex_uint d + end. + Definition of_int (d:Decimal.int) : option positive := match d with | Decimal.Pos d => @@ -605,6 +655,22 @@ Definition of_int (d:Decimal.int) : option positive := | Decimal.Neg _ => None end. +Definition of_hex_int (d:Hexadecimal.int) : option positive := + match d with + | Hexadecimal.Pos d => + match of_hex_uint d with + | N0 => None + | Npos p => Some p + end + | Hexadecimal.Neg _ => None + end. + +Definition of_num_int (d:Numeral.int) : option positive := + match d with + | Numeral.IntDec d => of_int d + | Numeral.IntHex d => of_hex_int d + end. + Fixpoint to_little_uint p := match p with | 1 => Decimal.D1 Decimal.Nil @@ -614,11 +680,26 @@ Fixpoint to_little_uint p := Definition to_uint p := Decimal.rev (to_little_uint p). +Fixpoint to_little_hex_uint p := + match p with + | 1 => Hexadecimal.D1 Hexadecimal.Nil + | p~1 => Hexadecimal.Little.succ_double (to_little_hex_uint p) + | p~0 => Hexadecimal.Little.double (to_little_hex_uint p) + end. + +Definition to_hex_uint p := Hexadecimal.rev (to_little_hex_uint p). + +Definition to_num_uint p := Numeral.UIntDec (to_uint p). + Definition to_int n := Decimal.Pos (to_uint n). -Numeral Notation positive of_int to_uint : positive_scope. +Definition to_hex_int p := Hexadecimal.Pos (to_hex_uint p). + +Definition to_num_int n := Numeral.IntDec (to_int n). + +Numeral Notation positive of_num_int to_num_uint : positive_scope. End Pos. (** Re-export the notation for those who just [Import BinPosDef] *) -Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope. +Numeral Notation positive Pos.of_num_int Pos.to_num_uint : positive_scope. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 74cdd1797c..84d70e56de 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -85,7 +85,51 @@ Definition to_decimal (q:Q) : option Decimal.decimal := | _ => None end. -Numeral Notation Q of_decimal to_decimal : Q_scope. +Definition of_hexadecimal (d:Hexadecimal.hexadecimal) : Q := + let '(i, f, e) := + match d with + | Hexadecimal.Hexadecimal i f => (i, f, Decimal.Pos Decimal.Nil) + | Hexadecimal.HexadecimalExp i f e => (i, f, e) + end in + let num := Z.of_hex_int (Hexadecimal.app_int i f) in + let e := Z.sub (Z.of_int e) (Z.mul 4 (Z.of_nat (Hexadecimal.nb_digits f))) in + match e with + | Z0 => Qmake num 1 + | Zpos e => Qmake (Pos.iter (Z.mul 2) num e) 1 + | Zneg e => Qmake num (Pos.iter (Pos.mul 2) 1%positive e) + end. + +Definition to_hexadecimal (q:Q) : option Hexadecimal.hexadecimal := + let mk_exp i e := + Hexadecimal.HexadecimalExp i Hexadecimal.Nil (Z.to_int (Z.opp e)) in + let num := Z.to_hex_int (Qnum q) in + let (den, e_den) := Hexadecimal.nztail (Pos.to_hex_uint (Qden q)) in + let e := Z.of_nat e_den in + match den with + | Hexadecimal.D1 Hexadecimal.Nil => + match e_den with + | O => Some (Hexadecimal.Hexadecimal num Hexadecimal.Nil) + | _ => Some (mk_exp num (4 * e)%Z) + end + | Hexadecimal.D2 Hexadecimal.Nil => Some (mk_exp num (1 + 4 * e)%Z) + | Hexadecimal.D4 Hexadecimal.Nil => Some (mk_exp num (2 + 4 * e)%Z) + | Hexadecimal.D8 Hexadecimal.Nil => Some (mk_exp num (3 + 4 * e)%Z) + | _ => None + end. + +Definition of_numeral (d:Numeral.numeral) : option Q := + match d with + | Numeral.Dec d => Some (of_decimal d) + | Numeral.Hex d => Some (of_hexadecimal d) + end. + +Definition to_numeral (q:Q) : option Numeral.numeral := + match to_decimal q with + | None => None + | Some q => Some (Numeral.Dec q) + end. + +Numeral Notation Q of_numeral to_numeral : Q_scope. Definition inject_Z (x : Z) := Qmake x 1. Arguments inject_Z x%Z. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 78b26c83ea..1729b9f85e 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1290,7 +1290,7 @@ Bind Scope Z_scope with Z.t Z. (** Re-export Notations *) -Numeral Notation Z Z.of_int Z.to_int : Z_scope. +Numeral Notation Z Z.of_num_int Z.to_num_int : Z_scope. Infix "+" := Z.add : Z_scope. Notation "- x" := (Z.opp x) : Z_scope. diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index c05ed9ebf4..8464ad1012 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -309,12 +309,32 @@ Definition to_pos (z:Z) : positive := Definition of_uint (d:Decimal.uint) := of_N (Pos.of_uint d). +Definition of_hex_uint (d:Hexadecimal.uint) := of_N (Pos.of_hex_uint d). + +Definition of_num_uint (d:Numeral.uint) := + match d with + | Numeral.UIntDec d => of_uint d + | Numeral.UIntHex d => of_hex_uint d + end. + Definition of_int (d:Decimal.int) := match d with | Decimal.Pos d => of_uint d | Decimal.Neg d => opp (of_uint d) end. +Definition of_hex_int (d:Hexadecimal.int) := + match d with + | Hexadecimal.Pos d => of_hex_uint d + | Hexadecimal.Neg d => opp (of_hex_uint d) + end. + +Definition of_num_int (d:Numeral.int) := + match d with + | Numeral.IntDec d => of_int d + | Numeral.IntHex d => of_hex_int d + end. + Definition to_int n := match n with | 0 => Decimal.Pos Decimal.zero @@ -322,6 +342,15 @@ Definition to_int n := | neg p => Decimal.Neg (Pos.to_uint p) end. +Definition to_hex_int n := + match n with + | 0 => Hexadecimal.Pos Hexadecimal.zero + | pos p => Hexadecimal.Pos (Pos.to_hex_uint p) + | neg p => Hexadecimal.Neg (Pos.to_hex_uint p) + end. + +Definition to_num_int n := Numeral.IntDec (to_int n). + (** ** Iteration of a function By convention, iterating a negative number of times is identity. @@ -639,9 +668,9 @@ Definition lxor a b := | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b)) end. -Numeral Notation Z of_int to_int : Z_scope. +Numeral Notation Z of_num_int to_num_int : Z_scope. End Z. (** Re-export the notation for those who just [Import BinIntDef] *) -Numeral Notation Z Z.of_int Z.to_int : Z_scope. +Numeral Notation Z Z.of_num_int Z.to_num_int : Z_scope. |