diff options
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 160 | ||||
| -rw-r--r-- | interp/notation.ml | 37 | ||||
| -rw-r--r-- | interp/notation.mli | 8 | ||||
| -rw-r--r-- | plugins/syntax/g_numeral.ml4 | 80 | ||||
| -rw-r--r-- | test-suite/success/NumeralNotations.v | 55 | ||||
| -rw-r--r-- | theories/Numbers/AltBinNotations.v | 45 |
6 files changed, 272 insertions, 113 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index e947fd891b..ca588acf29 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1379,42 +1379,130 @@ Numeral notations Starting with version 8.9, the following command allows the user to customize the way numeral literals are parsed and printed: -.. cmd:: Numeral Notation @ty @pa @pr : @scope. - -In the previous line, `ty` should be the name of an inductive type, -while `pa` and `pr` should be the names of two parsing and printing -functions. -The parsing function `pa` should have one of the following types: - - * :g:`Decimal.int -> ty` - * :g:`Decimal.int -> option ty` - * :g:`Decimal.uint -> ty` - * :g:`Decimal.uint -> option ty` - * :g:`Z -> ty` - * :g:`Z -> option ty` - -And the printing function `pr` should have one of the following types: - - * :g:`ty -> Decimal.int` - * :g:`ty -> option Decimal.int` - * :g:`ty -> Decimal.uint` - * :g:`ty -> option Decimal.uint` - * :g:`ty -> Z` - * :g:`ty -> option Z` - -.. cmdv:: Numeral Notation @ty @pa @pr : @scope (warning after @n). - -When a literal larger than `n` is parsed, a warning message about -possible stack overflow will be displayed. - -.. cmdv:: Numeral Notation @ty @pa @pr : @scope (abstract after @n). - -When a literal `m` larger than `n` is parsed, the result will be -:g:`(pa m)`, without reduction of this application to a normal form. -Here `m` will be a ``Decimal.int`` or ``Decimal.uint`` or ``Z``, -depending on the type of the parsing function `pa`. This allows a more -compact representation of literals in types such as ``nat``, and -limits parse failures due to stack overflow. +.. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope. + + In the previous line, :n:`@ident__1` should be the name of an + inductive type, while :n:`@ident__2` and :n:`@ident__3` should be + the names of the parsing and printing functions, respectively. The + parsing function :n:`@ident__2` should have one of the following + types: + + * :n:`Decimal.int -> @ident__1` + * :n:`Decimal.int -> option @ident__1` + * :n:`Decimal.uint -> @ident__1` + * :n:`Decimal.uint -> option @ident__1` + * :n:`Z -> @ident__1` + * :n:`Z -> option @ident__1` + + And the printing function :n:`@ident__3` should have one of the + following types: + + * :n:`@ident__1 -> Decimal.int` + * :n:`@ident__1 -> option Decimal.int` + * :n:`@ident__1 -> Decimal.uint` + * :n:`@ident__1 -> option Decimal.uint` + * :n:`@ident__1 -> Z` + * :n:`@ident__1 -> option Z` + + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). + + When a literal larger than :token:`num` is parsed, a warning + message about possible stack overflow, resulting from evaluating + :n:`@ident__2`, will be displayed. + + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (abstract after @num). + + When a literal :g:`m` larger than :token:`num` is parsed, the + result will be :n:`(@ident__2 m)`, without reduction of this + application to a normal form. Here :g:`m` will be a + :g:`Decimal.int` or :g:`Decimal.uint` or :g:`Z`, depending on the + type of the parsing function :n:`@ident__2`. This allows for a + more compact representation of literals in types such as :g:`nat`, + and limits parse failures due to stack overflow. Note that a + warning will be emitted when an integer larger than :token:`num` + is parsed. + + .. exn:: Cannot interpret this number as a value of type @type + + The numeral notation registered for :g:`ty` does not support the + given numeral. This error is given when the interpretation + function returns :g:`None`, or if the interpretation is registered + for only non-negative integers, and the given numeral is negative. + + .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + + The parsing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. + + .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the the types Decimal.uint or Z could be used{? (require BinNums first)}. + + The printing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. + + .. exn:: @type is not an inductive type + + Numeral notations can only be declared for inductive types with no + arguments. + + .. exn:: The inductive type @type cannot be used in numeral notations because support for polymorphic inductive types is not yet implemented. + + Numeral notations do not currently support polymorphic inductive + types. Ensure that all types involved in numeral notations are + declared with :g:`Unset Universe Polymorphism`, or with the + :g:`Monomorphic` attribute. + + .. exn:: The function @ident cannot be used in numeral notations because support for polymorphic printing and parsing functions is not yet implemented. + + Numeral notations do not currently support polymorphic functions + for printing and parsing. Ensure that both functions passed to + :cmd:`Numeral Notation` are defined with :g:`Unset Universe + Polymorphism`, or with the :g:`Monomorphic` attribute. + + .. exn:: Unexpected term while parsing a numeral notation + + Parsing functions must always return ground terms, made up of + applications of constructors and inductive types. Parsing + functions may not return terms containing axioms, bare + (co)fixpoints, lambdas, etc. + + .. exn:: Unexpected non-option term while parsing a numeral notation + + Parsing functions expected to return an :g:`option` must always + return a concrete :g:`Some` or :g:`None` when applied to a + concrete numeral expressed as a decimal. They may not return + opaque constants. + + .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). + + The type passed to :cmd:`Numeral Notation` must be a single + identifier. + + .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). + + Both functions passed to :cmd:`Numeral Notation` must be single + identifiers. + + .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). + + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(warning after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. + + .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @ident__2. + + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(abstract after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. + Typically, this indicates that the fully computed representation + of numerals can be so large that non-tail-recursive OCaml + functions run out of stack space when trying to walk them. + + For example + + .. coqtop:: all + + Check 90000. + .. _TacticNotation: diff --git a/interp/notation.ml b/interp/notation.ml index f60ddcf909..56d6acbdae 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -378,38 +378,39 @@ let prim_token_interp_infos = let prim_token_uninterp_infos = ref (Refmap.empty : (scope_name * prim_token_uid * bool) Refmap.t) -let hashtbl_check_and_set uid f h eq = +let hashtbl_check_and_set allow_overwrite uid f h eq = match Hashtbl.find h uid with | exception Not_found -> Hashtbl.add h uid f + | _ when allow_overwrite -> Hashtbl.add h uid f | g when eq f g -> () | _ -> user_err ~hdr:"prim_token_interpreter" (str "Unique identifier " ++ str uid ++ str " already used to register a numeral or string (un)interpreter.") -let register_gen_interpretation uid (interp, uninterp) = +let register_gen_interpretation allow_overwrite uid (interp, uninterp) = hashtbl_check_and_set - uid interp prim_token_interpreters InnerPrimToken.interp_eq; + allow_overwrite uid interp prim_token_interpreters InnerPrimToken.interp_eq; hashtbl_check_and_set - uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq + allow_overwrite uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq -let register_rawnumeral_interpretation uid (interp, uninterp) = - register_gen_interpretation uid +let register_rawnumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid (InnerPrimToken.RawNumInterp interp, InnerPrimToken.RawNumUninterp uninterp) -let register_bignumeral_interpretation uid (interp, uninterp) = - register_gen_interpretation uid +let register_bignumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid (InnerPrimToken.BigNumInterp interp, InnerPrimToken.BigNumUninterp uninterp) -let register_string_interpretation uid (interp, uninterp) = - register_gen_interpretation uid +let register_string_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp) type prim_token_infos = { pt_scope : scope_name; (** Concerned scope *) pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) pt_required : required_module; (** Module that should be loaded first *) - pt_refs : global_reference list; (** Entry points during uninterpretation *) + pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) pt_in_match : bool (** Is this prim token legal in match patterns ? *) } @@ -445,19 +446,25 @@ let enable_prim_token_interpretation infos = (the latter inside a [Mltop.declare_cache_obj]). *) +let fresh_string_of = + let count = ref 0 in + fun root -> count := !count+1; (string_of_int !count)^"_"^root + let declare_numeral_interpreter sc dir interp (patl,uninterp,b) = - register_bignumeral_interpretation sc (interp,uninterp); + let uid = fresh_string_of sc in + register_bignumeral_interpretation uid (interp,uninterp); enable_prim_token_interpretation { pt_scope = sc; - pt_uid = sc; + pt_uid = uid; pt_required = dir; pt_refs = List.map_filter glob_prim_constr_key patl; pt_in_match = b } let declare_string_interpreter sc dir interp (patl,uninterp,b) = - register_string_interpretation sc (interp,uninterp); + let uid = fresh_string_of sc in + register_string_interpretation uid (interp,uninterp); enable_prim_token_interpretation { pt_scope = sc; - pt_uid = sc; + pt_uid = uid; pt_required = dir; pt_refs = List.map_filter glob_prim_constr_key patl; pt_in_match = b } diff --git a/interp/notation.mli b/interp/notation.mli index 2545e494ef..1d01d75c82 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -91,19 +91,19 @@ type 'a prim_token_interpretation = 'a prim_token_interpreter * 'a prim_token_uninterpreter val register_rawnumeral_interpretation : - prim_token_uid -> rawnum prim_token_interpretation -> unit + ?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit val register_bignumeral_interpretation : - prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit + ?allow_overwrite:bool -> prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit val register_string_interpretation : - prim_token_uid -> string prim_token_interpretation -> unit + ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit type prim_token_infos = { pt_scope : scope_name; (** Concerned scope *) pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) pt_required : required_module; (** Module that should be loaded first *) - pt_refs : global_reference list; (** Entry points during uninterpretation *) + pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) pt_in_match : bool (** Is this prim token legal in match patterns ? *) } diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index caba4db4fc..19a15fd1df 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) DECLARE PLUGIN "numeral_notation_plugin" @@ -16,7 +18,6 @@ open Globnames open Constrexpr open Constrexpr_ops open Constr -open Misctypes (** * Numeral notation *) @@ -24,7 +25,7 @@ open Misctypes The constr [c] below isn't necessarily well-typed, since we built it via an [mkApp] of a conversion function on a term - that starts with the right constructor, but might be partially + that starts with the right constructor but might be partially applied. At least [c] is known to be evar-free, since it comes from @@ -55,7 +56,7 @@ let warn_large_num = CWarnings.create ~name:"large-number" ~category:"numbers" (fun ty -> strbrk "Stack overflow or segmentation fault happens when " ++ - strbrk "working with large numbers in " ++ pr_reference ty ++ + strbrk "working with large numbers in " ++ pr_qualid ty ++ strbrk " (threshold may vary depending" ++ strbrk " on your system limits and on the command executed).") @@ -64,11 +65,11 @@ let warn_abstract_large_num = (fun (ty,f) -> let (sigma, env) = Pfedit.get_current_context () in strbrk "To avoid stack overflow, large numbers in " ++ - pr_reference ty ++ strbrk " are interpreted as applications of " ++ + pr_qualid ty ++ strbrk " are interpreted as applications of " ++ Printer.pr_constr_env env sigma f ++ strbrk ".") (** Comparing two raw numbers (base 10, big-endian, non-negative). - A bit nasty, but not critical : only used to decide when a + A bit nasty, but not critical: only used to decide when a number is considered as large (see warnings above). *) exception Comp of int @@ -233,18 +234,24 @@ let rec glob_of_constr ?loc c = match Constr.kind c with | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None)) | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None)) | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None)) - | _ -> CErrors.anomaly (str "Numeral.interp: unexpected constr") + | _ -> let (sigma, env) = Pfedit.get_current_context () in + CErrors.user_err ?loc + (str "Unexpected term while parsing a numeral notation:" ++ fnl () ++ + Printer.pr_constr_env env sigma c) let no_such_number ?loc ty = CErrors.user_err ?loc (str "Cannot interpret this number as a value of type " ++ - pr_reference ty) + pr_qualid ty) let interp_option ty ?loc c = match Constr.kind c with | App (_Some, [| _; c |]) -> glob_of_constr ?loc c | App (_None, [| _ |]) -> no_such_number ?loc ty - | x -> CErrors.anomaly (str "Numeral.interp: option expected") + | x -> let (sigma, env) = Pfedit.get_current_context () in + CErrors.user_err ?loc + (str "Unexpected non-option term while parsing a numeral notation:" ++ fnl () ++ + Printer.pr_constr_env env sigma c) let uninterp_option c = match Constr.kind c with @@ -276,7 +283,7 @@ type numeral_notation_obj = to_ty : constr; of_kind : conversion_kind; of_ty : constr; - num_ty : Libnames.reference; (* for warnings / error messages *) + num_ty : Libnames.qualid; (* for warnings / error messages *) warning : numnot_option } let interp o ?loc n = @@ -322,7 +329,7 @@ let uninterp o (Glob_term.AnyGlobConstr n) = let load_numeral_notation _ (_, (uid,opts)) = Notation.register_rawnumeral_interpretation - uid (interp opts, uninterp opts) + ~allow_overwrite:true uid (interp opts, uninterp opts) let cache_numeral_notation x = load_numeral_notation 1 x @@ -355,7 +362,7 @@ let unsafe_locate_ind q = let locate_ind q = try unsafe_locate_ind q - with Not_found -> Nametab.error_global_not_found (CAst.make q) + with Not_found -> Nametab.error_global_not_found q let locate_z () = try @@ -367,35 +374,33 @@ let locate_int () = { uint = locate_ind q_uint; int = locate_ind q_int } -let locate_globref r = - let q = qualid_of_reference r in - try Nametab.locate CAst.(q.v) +let locate_globref q = + try Nametab.locate q with Not_found -> Nametab.error_global_not_found q -let locate_constant r = - let q = qualid_of_reference r in - try Nametab.locate_constant CAst.(q.v) +let locate_constant q = + try Nametab.locate_constant q with Not_found -> Nametab.error_global_not_found q let has_type f ty = let (sigma, env) = Pfedit.get_current_context () in - let c = mkCastC (mkRefC f, CastConv ty) in + let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in try let _ = Constrintern.interp_constr env sigma c in true with Pretype_errors.PretypeError _ -> false let type_error_to f ty loadZ = CErrors.user_err - (pr_reference f ++ str " should go from Decimal.int to " ++ - pr_reference ty ++ str " or (option " ++ pr_reference ty ++ str ")." ++ - fnl () ++ str "Instead of int, the types uint or Z could be used" ++ - (if loadZ then str " (load Z first)." else str ".")) + (pr_qualid f ++ str " should go from Decimal.int to " ++ + pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ + fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ + (if loadZ then str " (require BinNums first)." else str ".")) let type_error_of g ty loadZ = CErrors.user_err - (pr_reference g ++ str " should go from " ++ pr_reference ty ++ - str " to Decimal.int or (option int)." ++ fnl () ++ - str "Instead of int, the types uint or Z could be used" ++ - (if loadZ then str " (load Z first)." else str ".")) + (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 could be used" ++ + (if loadZ then str " (require BinNums first)." else str ".")) let vernac_numeral_notation ty f g scope opts = let int_ty = locate_int () in @@ -405,7 +410,7 @@ let vernac_numeral_notation ty f g scope opts = let of_ty = mkConst (locate_constant g) in let cty = mkRefC ty in let app x y = mkAppC (x,[y]) in - let cref q = mkRefC (CAst.make (Qualid q)) in + let cref q = mkRefC q in let arrow x y = mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) in @@ -420,17 +425,20 @@ let vernac_numeral_notation ty f g scope opts = get_constructors ind | IndRef _ -> CErrors.user_err - (str "The inductive type " ++ pr_reference ty ++ - str " cannot be polymorphic here for the moment") + (str "The inductive type " ++ pr_qualid ty ++ + str " cannot be used in numeral notations because" ++ + str " support for polymorphic inductive types is not yet implemented") | ConstRef _ | ConstructRef _ | VarRef _ -> CErrors.user_err - (pr_reference ty ++ str " is not an inductive type") + (pr_qualid ty ++ str " is not an inductive type") in (* Check the type of f *) let to_kind = if Global.is_polymorphic (Nametab.global f) then CErrors.user_err - (pr_reference f ++ str " cannot be polymorphic for the moment") + (str "The function " ++ pr_qualid f ++ str " cannot be used" ++ + str " in numeral notations because support for polymorphic" ++ + str " printing and parsing functions is not yet implemented.") else if has_type f (arrow cint cty) then Int int_ty, Direct else if has_type f (arrow cint (opt cty)) then Int int_ty, Option else if has_type f (arrow cuint cty) then UInt int_ty.uint, Direct @@ -447,7 +455,7 @@ let vernac_numeral_notation ty f g scope opts = let of_kind = if Global.is_polymorphic (Nametab.global g) then CErrors.user_err - (pr_reference g ++ str " cannot be polymorphic for the moment") + (pr_qualid g ++ str " cannot be polymorphic for the moment") else if has_type g (arrow cty cint) then Int int_ty, Direct else if has_type g (arrow cty (opt cint)) then Int int_ty, Option else if has_type g (arrow cty cuint) then UInt int_ty.uint, Direct diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v new file mode 100644 index 0000000000..a06327c5e6 --- /dev/null +++ b/test-suite/success/NumeralNotations.v @@ -0,0 +1,55 @@ + +(* Test that we fail, rather than raising anomalies, on opaque terms during interpretation *) + +(* 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. + 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. + Delimit Scope opaque_scope with opaque. + Open Scope opaque_scope. + Fail Check 1%opaque. +End Test2. + +Module Test3. + Inductive silly := SILLY (v : Decimal.uint) (f : forall A, A -> A). + Definition to_silly (v : Decimal.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. + Fail Check 1%silly. +End Test3. + + +Module Test4. + Polymorphic 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 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. + Fail Numeral Notation punit to_punit of_punit : pto. + Fail Numeral Notation punit pto_punit of_punit : ppo. + Fail Numeral Notation punit to_punit pof_punit : ptp. + Fail Numeral Notation punit pto_punit pof_punit : ppp. + Numeral Notation unit to_unit of_unit : uto. + Delimit Scope uto with uto. + Check let v := 0%uto in v : unit. + Fail Check 1%uto. + Fail Check (-1)%uto. + Fail Numeral Notation unit pto_unit of_unit : upo. + Fail Numeral Notation unit to_unit pof_unit : utp. + Fail Numeral Notation unit pto_unit pof_unit : upp. +End Test4. diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v index 595934ad89..c7e3999691 100644 --- a/theories/Numbers/AltBinNotations.v +++ b/theories/Numbers/AltBinNotations.v @@ -1,34 +1,35 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** * Alternative Binary Numeral Notations *) (** Faster but less safe parsers and printers of [positive], [N], [Z]. *) -(** Nowadays, literals in types [positive], [N], [Z] are parsed and +(** By default, literals in types [positive], [N], [Z] are parsed and printed via the [Numeral Notation] command, by conversion from/to - the [Decimal.int] representation. This way, we do not need any - ML library of arbitrary precision integers (bigint.ml), hence - reducing the amount of ML code to trust during parsing and printing. - But this new method is slower than the older code, by a margin that - may become significant for literals of thousands of digits and more. - If that becomes a problem for your development, this file provides - some alternative [Numeral Notation] commmands that use [Z] as - bridge type : it hence relies on the bigint.ml library, the efficiency - should be almost the one of the legacy code, at the expense of a - larger ML trust base. To enable these commands, just be sure to - [Require] this file after the other files of - - Please note anyway that literals above 10000 digits in [positive], - [N], [Z] will end up triggering Stack Overlow in various parts of - the Coq engine (type-checker, reduction, etc). So consider using - [BigN] or [BigZ] instead... -*) + the [Decimal.int] representation. When working with numbers with + thousands of digits and more, conversion from/to [Decimal.int] can + become significantly slow. If that becomes a problem for your + development, this file provides some alternative [Numeral + Notation] commmands that use [Z] as bridge type. To enable these + commands, just be sure to [Require] this file after other files + defining numeral notations. + + Note: up to Coq 8.8, literals in types [positive], [N], [Z] were + parsed and printed using a native ML library of arbitrary + precision integers named bigint.ml. From 8.9, the default is to + parse and print using a Coq library converting sequences of + digits, hence reducing the amount of ML code to trust. But this + method is slower. This file then gives access to the legacy + method, trading efficiency against a larger ML trust base relying + on bigint.ml. *) Require Import BinNums. |