diff options
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 48 | ||||
| -rw-r--r-- | plugins/syntax/g_numeral.ml4 | 11 | ||||
| -rw-r--r-- | test-suite/interactive/PrimNotation.v | 58 | ||||
| -rw-r--r-- | test-suite/success/NumeralNotations.v | 123 |
4 files changed, 195 insertions, 45 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index ca588acf29..50425c8a5d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1376,16 +1376,15 @@ Abbreviations 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 @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: + This command allows the user to customize the way numeral literals + are parsed and printed. + + The token :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` @@ -1404,6 +1403,10 @@ the way numeral literals are parsed and printed: * :n:`@ident__1 -> Z` * :n:`@ident__1 -> option Z` + When parsing, the application of the parsing function + :n:`@ident__2` to the number will be fully reduced, and universes + of the resulting term will be refreshed. + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). When a literal larger than :token:`num` is parsed, a warning @@ -1420,12 +1423,13 @@ the way numeral literals are parsed and printed: 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. + is parsed. Note that :n:`(abstract after @num)` has no effect + when :n:`@ident__2` lands in an :g:`option` type. .. 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 + The numeral notation registered for :token:`type` 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. @@ -1434,7 +1438,7 @@ the way numeral literals are parsed and printed: 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)}. + .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, 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. @@ -1444,20 +1448,6 @@ the way numeral literals are parsed and printed: 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 @@ -1482,6 +1472,12 @@ the way numeral literals are parsed and printed: Both functions passed to :cmd:`Numeral Notation` must be single identifiers. + .. exn:: The reference @ident was not found in the current environment. + + Identifiers passed to :cmd:`Numeral Notation` must be global + definitions, not notations, section variables, section-local + :g:`Let` bound identifiers, etc. + .. 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 diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index 1d2d47fbaa..a097adec24 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -36,13 +36,14 @@ open Constr let eval_constr env sigma (c : Constr.t) = let c = EConstr.of_constr c in let sigma,t = Typing.type_of env sigma c in - let c'= Vnorm.cbv_vm env sigma c t in + let c' = Vnorm.cbv_vm env sigma c t in EConstr.Unsafe.to_constr c' (* For testing with "compute" instead of "vm_compute" : -let eval_constr (c : constr) = - let (sigma, env) = Lemmas.get_current_context () in - Tacred.compute env sigma c +let eval_constr env sigma (c : Constr.t) = + let c = EConstr.of_constr c in + let c' = Tacred.compute env sigma c in + EConstr.Unsafe.to_constr c' *) let eval_constr_app env sigma c1 c2 = @@ -325,7 +326,7 @@ let uninterp o (Glob_term.AnyGlobConstr n) = | UInt _ -> Some (rawnum_of_coquint c, true) | Z _ -> Some (big2raw (bigint_of_z c)) with - | Type_errors.TypeError _ -> None (* cf. eval_constr_app *) + | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *) | NotANumber -> None (* all other functions except big2raw *) (* Here we only register the interp and uninterp functions diff --git a/test-suite/interactive/PrimNotation.v b/test-suite/interactive/PrimNotation.v index 4c81095c68..07986b0df3 100644 --- a/test-suite/interactive/PrimNotation.v +++ b/test-suite/interactive/PrimNotation.v @@ -5,14 +5,60 @@ Delimit Scope Z_scope with Z. Open Scope Z_scope. -Check 0. -(* 0 : nat *) +Check let v := 0 in v : nat. +(* let v := 0 in v : nat : nat *) Require BinInt. -Check 0. -(* 0 : BinNums.Z *) +Check let v := 0 in v : BinNums.Z. +(* let v := 0 in v : BinNums.Z : BinNums.Z *) Back 2. -Check 0. -(* Expected answer: 0 : nat *) +Check let v := 0 in v : nat. +(* Expected answer: let v := 0 in v : nat : nat *) (* Used to fail with: Error: Cannot interpret in Z_scope without requiring first module BinNums. *) + +Local Set Universe Polymorphism. +Delimit Scope punit_scope with punit. +Delimit Scope pcunit_scope with pcunit. +Delimit Scope int_scope with int. +Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int : int_scope. +Module A. + NonCumulative Inductive punit@{u} : Type@{u} := ptt. + Cumulative Inductive pcunit@{u} : Type@{u} := pctt. + Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. + Definition to_pcunit : Decimal.int -> option pcunit + := fun v => match v with 0%int => Some pctt | _ => None end. + Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. + Definition of_pcunit : pcunit -> Decimal.uint := fun _ => Nat.to_uint 0. + Numeral Notation punit to_punit of_punit : punit_scope. + Check let v := 0%punit in v : punit. + Back 2. + Numeral Notation pcunit to_pcunit of_pcunit : punit_scope. + Check let v := 0%punit in v : pcunit. +End A. +Reset A. +Local Unset Universe Polymorphism. +Module A. + Inductive punit : Set := ptt. + Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. + Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. + Numeral Notation punit to_punit of_punit : punit_scope. + Check let v := 0%punit in v : punit. +End A. +Local Set Universe Polymorphism. +Inductive punit@{u} : Type@{u} := ptt. +Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. +Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. +Numeral Notation punit to_punit of_punit : punit_scope. +Check let v := 0%punit in v : punit. +Back 6. (* check backtracking of registering universe polymorphic constants *) +Local Unset Universe Polymorphism. +Inductive punit : Set := ptt. +Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. +Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. +Numeral Notation punit to_punit of_punit : punit_scope. +Check let v := 0%punit in v : punit. diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v index a06327c5e6..907ec32671 100644 --- a/test-suite/success/NumeralNotations.v +++ b/test-suite/success/NumeralNotations.v @@ -31,8 +31,9 @@ End Test3. Module Test4. - Polymorphic Inductive punit := ptt. + 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. @@ -40,16 +41,122 @@ Module Test4. 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 punit to_punit of_punit : pto. + Numeral Notation punit pto_punit of_punit : ppo. + Numeral Notation punit to_punit pof_punit : ptp. + Numeral Notation punit pto_punit pof_punit : ppp. Numeral Notation unit to_unit of_unit : uto. + Delimit Scope pto with pto. + Delimit Scope ppo with ppo. + Delimit Scope ptp with ptp. + Delimit Scope ppp with ppp. Delimit Scope uto with uto. + Check let v := 0%pto in v : punit. + Check let v := 0%ppo in v : punit. + Check let v := 0%ptp in v : punit. + Check let v := 0%ppp in v : punit. 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. + Numeral Notation unit pto_unit of_unit : upo. + Numeral Notation unit to_unit pof_unit : utp. + Numeral Notation unit pto_unit pof_unit : upp. + Delimit Scope upo with upo. + Delimit Scope utp with utp. + Delimit Scope upp with upp. + Check let v := 0%upo in v : unit. + Check let v := 0%utp in v : unit. + Check let v := 0%upp in v : unit. + + Polymorphic Definition pto_punits := pto_punit_all@{Set}. + Polymorphic Definition pof_punits := pof_punit@{Set}. + Numeral Notation punit pto_punits pof_punits : ppps (abstract after 1). + Delimit Scope ppps with ppps. + Universe u. + Constraint Set < u. + Check let v := 0%ppps in v : punit@{u}. (* Check that universes are refreshed *) + Fail Check let v := 1%ppps in v : punit@{u}. (* Note that universes are not refreshed here *) End Test4. + +Module Test5. + Check S. (* At one point gave Error: Anomaly "Uncaught exception Pretype_errors.PretypeError(_, _, _)." Please report at http://coq.inria.fr/bugs/. *) +End Test5. + +Module Test6. + (* Check that numeral notations on enormous terms don't take forever to print/parse *) + (* Ackerman definition from https://stackoverflow.com/a/10303475/377022 *) + Fixpoint ack (n m : nat) : nat := + match n with + | O => S m + | S p => let fix ackn (m : nat) := + match m with + | O => ack p 1 + | S q => ack p (ackn q) + end + in ackn m + end. + + Timeout 1 Check (S (ack 4 4)). (* should be instantaneous *) + + 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. + Module Export Scopes. + Delimit Scope wnat_scope with wnat. + End Scopes. + Module Export Notations. + Export Scopes. + Numeral Notation wnat of_uint to_uint : wnat_scope (abstract after 5000). + End Notations. + Check let v := 0%wnat in v : wnat. + Check wrap O. + Timeout 1 Check wrap (ack 4 4). (* should be instantaneous *) +End Test6. + +Module Test6_2. + Import Test6.Scopes. + Check Test6.wrap 0. + Import Test6.Notations. + Check let v := 0%wnat in v : Test6.wnat. +End Test6_2. + +Module Test7. + Local Set Primitive Projections. + Record > wuint := wrap { unwrap : Decimal.uint }. + Delimit Scope wuint_scope with wuint. + Fail Numeral Notation wuint wrap unwrap : wuint_scope. +End Test7. + +Module Test8. + Local Set Primitive Projections. + Record > wuint := wrap { unwrap : Decimal.uint }. + Delimit Scope wuint_scope with wuint. + Section with_var. + Context (dummy : unit). + Definition wrap' := let __ := dummy in wrap. + Definition unwrap' := let __ := dummy in unwrap. + Global Numeral Notation wuint wrap' unwrap' : wuint_scope. + Check let v := 0%wuint in v : wuint. + End with_var. + Fail Check let v := 0%wuint in v : wuint. + Compute wrap (Nat.to_uint 0). + + Notation wrap'' := wrap. + Notation unwrap'' := unwrap. + Fail Numeral Notation wuint wrap'' unwrap'' : wuint_scope. +End Test8. + +Module Test9. + Section with_let. + Local Set Primitive Projections. + Record > wuint := wrap { unwrap : Decimal.uint }. + Let wrap' := wrap. + Let unwrap' := unwrap. + Local Notation wrap'' := wrap. + Local Notation unwrap'' := unwrap. + Delimit Scope wuint_scope with wuint. + Fail Numeral Notation wuint wrap' unwrap' : wuint_scope. + Fail Numeral Notation wuint wrap'' unwrap'' : wuint_scope. + End with_let. +End Test9. |