From 93119295d0dd81669b46f52032c1bfe8f36afca0 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 6 Apr 2018 16:37:47 +0200 Subject: Prelude : update the comment about ML plugins loaded by Init --- theories/Init/Prelude.v | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'theories') diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 802f18c0f2..390ff5e240 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -19,8 +19,11 @@ Require Export Peano. Require Export Coq.Init.Wf. Require Export Coq.Init.Tactics. Require Export Coq.Init.Tauto. -(* Initially available plugins - (+ nat_syntax_plugin loaded in Datatypes) *) +(* Some initially available plugins. See also: + - ltac_plugin (in Notations) + - nat_syntax_plugin (in Datatypes) + - tauto_plugin (in Tauto). +*) Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". (* Default substrings not considered by queries like SearchAbout *) -- cgit v1.2.3 From 006d2cd8c25dbcd787168c49e0ebfdf5dfc89c12 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 28 Feb 2017 10:54:33 +0100 Subject: Numeral Notation: allow parsing from/to Decimal.int or Decimal.uint This way, we could fully bypass bigint.ml. The previous mechanism of parsing/printing Z is kept for now. Currently, the conversion functions accepted by Numeral Notation foo may have the following types. for parsing: int -> foo int -> option foo uint -> foo uint -> option foo Z -> foo Z -> option foo for printing: foo -> int foo -> option int foo -> uint foo -> option uint foo -> Z foo -> option Z Notes: - The Declare ML Module is directly done in Prelude - When doing a Numeral Notation, having the Z datatype around isn't mandatory anymore (but the error messages suggest that it can still be used). - An option (abstract after ...) allows to keep large numbers in an abstract form such as (Nat.of_uint 123456) instead of reducing to (S (S (S ...))) and ending immediately with Stack Overflow. - After checking with Matthieu, there is now a explicit check and an error message in case of polymorphic inductive types --- theories/Init/Decimal.v | 6 ++++++ theories/Init/Prelude.v | 10 ++++++++++ 2 files changed, 16 insertions(+) (limited to 'theories') diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 57163b1b07..34b4e75814 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -161,3 +161,9 @@ with succ_double d := end. End Little. + +(** 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 390ff5e240..f99a6a7c60 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -26,5 +26,15 @@ Require Export Coq.Init.Tauto. *) Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". +Declare ML Module "numeral_notation_plugin". + +(* Parsing / printing of decimal numbers *) +Arguments Nat.of_uint d%uint_scope. +Arguments Nat.of_int d%int_scope. +Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint + : uint_scope. +Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int + : int_scope. + (* Default substrings not considered by queries like SearchAbout *) Add Search Blacklist "_subproof" "_subterm" "Private_". -- cgit v1.2.3 From 24ccc118ccfb4c1223cd37bd43c9d26a77851176 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 15 Mar 2017 03:11:23 +0100 Subject: Numeral Notation for nat This parsing/printing method for nat should be just as fast as the previous dedicated code. Moreover, we could now parse large literals as nat numbers, by leaving them in a half-abstract form such as (Nat.of_uint 123456). This form is convertible to the closed (S (S (S ...))) form, so it shouldn't be a big deal for compatibility, except for if some Ltac stuff relies on (S ...) to be present after parsing. Of course, forcing the computation of a (Nat.of_uint ....) may take a while or raise a Stack Overflow. --- theories/Init/Datatypes.v | 1 - theories/Init/Nat.v | 4 +++ theories/Init/Peano.v | 1 + theories/Init/Prelude.v | 4 ++- theories/NArith/BinNatDef.v | 6 ++++ theories/Numbers/AltBinNotations.v | 68 ++++++++++++++++++++++++++++++++++++++ theories/Numbers/BinNums.v | 16 ++++----- theories/PArith/BinPosDef.v | 10 ++++-- theories/ZArith/BinIntDef.v | 12 +++++-- 9 files changed, 104 insertions(+), 18 deletions(-) create mode 100644 theories/Numbers/AltBinNotations.v (limited to 'theories') diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 05b741f0ac..1e6843d511 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -12,7 +12,6 @@ Set Implicit Arguments. Require Import Notations. Require Import Logic. -Declare ML Module "nat_syntax_plugin". (********************************************************************) (** * Datatypes with zero and one element *) diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v index ad1bc717c4..eb4ba0e5e6 100644 --- a/theories/Init/Nat.v +++ b/theories/Init/Nat.v @@ -24,6 +24,10 @@ Definition t := nat. (** ** Constants *) +Local Notation "0" := O. +Local Notation "1" := (S O). +Local Notation "2" := (S (S O)). + Definition zero := 0. Definition one := 1. Definition two := 2. diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index d5322d0945..65e5e76a22 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -31,6 +31,7 @@ Require Import Logic. Require Coq.Init.Nat. Open Scope nat_scope. +Local Notation "0" := O. Definition eq_S := f_equal S. Definition f_equal_nat := f_equal (A:=nat). diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index f99a6a7c60..e8997d30b8 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -21,7 +21,6 @@ Require Export Coq.Init.Tactics. Require Export Coq.Init.Tauto. (* Some initially available plugins. See also: - ltac_plugin (in Notations) - - nat_syntax_plugin (in Datatypes) - tauto_plugin (in Tauto). *) Declare ML Module "cc_plugin". @@ -36,5 +35,8 @@ Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int : int_scope. +(* Parsing / printing of [nat] numbers *) +Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5000). + (* Default substrings not considered by queries like SearchAbout *) Add Search Blacklist "_subproof" "_subterm" "Private_". diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 5de75537cb..8bbecf9acb 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -13,6 +13,10 @@ Require Import BinPos. Local Open Scope N_scope. +Local Notation "0" := N0. +Local Notation "1" := (Npos 1). +Local Notation "2" := (Npos 2). + (**********************************************************************) (** * Binary natural numbers, definitions of operations *) (**********************************************************************) @@ -399,3 +403,5 @@ Definition to_uint n := Definition to_int n := Decimal.Pos (to_uint n). End N. + +Numeral Notation N N.of_uint N.to_uint : N_scope. diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v new file mode 100644 index 0000000000..595934ad89 --- /dev/null +++ b/theories/Numbers/AltBinNotations.v @@ -0,0 +1,68 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Some p + | _ => None + end. + +Definition pos_to_z p := Zpos p. + +Numeral Notation positive pos_of_z pos_to_z : positive_scope. + +(** [N] *) + +Definition n_of_z z := + match z with + | Z0 => Some N0 + | Zpos p => Some (Npos p) + | Zneg _ => None + end. + +Definition n_to_z n := + match n with + | N0 => Z0 + | Npos p => Zpos p + end. + +Numeral Notation N n_of_z n_to_z : N_scope. + +(** [Z] *) + +Definition z_of_z (z:Z) := z. + +Numeral Notation Z z_of_z z_of_z : Z_scope. diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v index d5eb4f2681..3ba9d1f5ed 100644 --- a/theories/Numbers/BinNums.v +++ b/theories/Numbers/BinNums.v @@ -12,15 +12,11 @@ Set Implicit Arguments. -Declare ML Module "positive_syntax_plugin". -Declare ML Module "n_syntax_plugin". -Declare ML Module "z_syntax_plugin". - (** [positive] is a datatype representing the strictly positive integers in a binary way. Starting from 1 (represented by [xH]), one can add a new least significant digit via [xO] (digit 0) or [xI] (digit 1). - Numbers in [positive] can also be denoted using a decimal notation; - e.g. [6%positive] abbreviates [xO (xI xH)] *) + Numbers in [positive] will also be denoted using a decimal notation; + e.g. [6%positive] will abbreviate [xO (xI xH)] *) Inductive positive : Set := | xI : positive -> positive @@ -34,8 +30,8 @@ Arguments xI _%positive. (** [N] is a datatype representing natural numbers in a binary way, by extending the [positive] datatype with a zero. - Numbers in [N] can also be denoted using a decimal notation; - e.g. [6%N] abbreviates [Npos (xO (xI xH))] *) + Numbers in [N] will also be denoted using a decimal notation; + e.g. [6%N] will abbreviate [Npos (xO (xI xH))] *) Inductive N : Set := | N0 : N @@ -49,8 +45,8 @@ Arguments Npos _%positive. An integer is either zero or a strictly positive number (coded as a [positive]) or a strictly negative number (whose opposite is stored as a [positive] value). - Numbers in [Z] can also be denoted using a decimal notation; - e.g. [(-6)%Z] abbreviates [Zneg (xO (xI xH))] *) + Numbers in [Z] will also be denoted using a decimal notation; + e.g. [(-6)%Z] will abbreviate [Zneg (xO (xI xH))] *) Inductive Z : Set := | Z0 : Z diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 070314746a..39b609e9dd 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -26,6 +26,8 @@ Require Export BinNums. for the number 6 (which is 110 in binary notation). *) +Local Notation "1" := xH. + Notation "p ~ 1" := (xI p) (at level 7, left associativity, format "p '~' '1'") : positive_scope. Notation "p ~ 0" := (xO p) @@ -325,14 +327,14 @@ Definition sqrtrem_step (f g:positive->positive) p := let r' := g (f r) in if s' <=? r' then (s~1, sub_mask r' s') else (s~0, IsPos r') - | (s,_) => (s~0, sub_mask (g (f 1)) 4) + | (s,_) => (s~0, sub_mask (g (f 1)) 1~0~0) end. Fixpoint sqrtrem p : positive * mask := match p with | 1 => (1,IsNul) - | 2 => (1,IsPos 1) - | 3 => (1,IsPos 2) + | 1~0 => (1,IsPos 1) + | 1~1 => (1,IsPos 1~0) | p~0~0 => sqrtrem_step xO xO (sqrtrem p) | p~0~1 => sqrtrem_step xO xI (sqrtrem p) | p~1~0 => sqrtrem_step xI xO (sqrtrem p) @@ -615,3 +617,5 @@ Definition to_uint p := Decimal.rev (to_little_uint p). Definition to_int n := Decimal.Pos (to_uint n). End Pos. + +Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope. diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index db4de0b90c..8abcd15700 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -14,6 +14,10 @@ Require Import BinPos BinNat. Local Open Scope Z_scope. +Local Notation "0" := Z0. +Local Notation "1" := (Zpos 1). +Local Notation "2" := (Zpos 2). + (***********************************************************) (** * Binary Integers, Definitions of Operations *) (***********************************************************) @@ -53,7 +57,7 @@ Definition succ_double x := Definition pred_double x := match x with - | 0 => -1 + | 0 => neg 1 | neg p => neg p~1 | pos p => pos (Pos.pred_double p) end. @@ -104,7 +108,7 @@ Definition succ x := x + 1. (** ** Predecessor *) -Definition pred x := x + -1. +Definition pred x := x + neg 1. (** ** Subtraction *) @@ -171,7 +175,7 @@ Definition sgn z := match z with | 0 => 0 | pos p => 1 - | neg p => -1 + | neg p => neg 1 end. (** Boolean equality and comparisons *) @@ -636,3 +640,5 @@ Definition lxor a b := end. End Z. + +Numeral Notation Z Z.of_int Z.to_int : Z_scope. -- cgit v1.2.3 From 44638cda2f8f7461506a6e5a9a2edf860971f96c Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 12 Mar 2018 17:21:04 +0100 Subject: Decimal: scope name changed dec_(u)int_scope This avoid a clash with int_scope in ssreflect's ssrint.v --- theories/Init/Decimal.v | 8 ++++---- theories/Init/Prelude.v | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) (limited to 'theories') diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 34b4e75814..1ff00ec11c 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -42,10 +42,10 @@ Notation zero := (D0 Nil). Inductive int := Pos (d:uint) | Neg (d:uint). -Delimit Scope uint_scope with uint. -Bind Scope uint_scope with uint. -Delimit Scope int_scope with int. -Bind Scope int_scope with int. +Delimit Scope dec_uint_scope with uint. +Bind Scope dec_uint_scope with uint. +Delimit Scope dec_int_scope with int. +Bind Scope dec_int_scope with int. (** This representation favors simplicity over canonicity. For normalizing numbers, we need to remove head zero digits, diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index e8997d30b8..6d98bcb34a 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -28,12 +28,12 @@ Declare ML Module "ground_plugin". Declare ML Module "numeral_notation_plugin". (* Parsing / printing of decimal numbers *) -Arguments Nat.of_uint d%uint_scope. -Arguments Nat.of_int d%int_scope. +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 - : uint_scope. + : dec_uint_scope. Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int - : int_scope. + : dec_int_scope. (* Parsing / printing of [nat] numbers *) Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5000). -- cgit v1.2.3 From fa0f378c91286d9127777a06b1dc557f695c22ae Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 14 Jul 2018 06:25:22 -0400 Subject: Fix numeral notation for a rebase on top of master Some of this code is cargo-culted or kludged to work. As I understand it, the situation is as follows: There are two sorts of use-cases that need to be supported: 1. A plugin registers an OCaml function as a numeral interpreter. In this case, the function registration must be synchronized with the document state, but the functions should not be marshelled / stored in the .vo. 2. A vernacular registers a Gallina function as a numeral interpreter. In this case, the registration must be synchronized, and the function should be marshelled / stored in the .vo. In case (1), we can compare functions by pointer equality, and we should be able to rely on globally unique keys, even across backtracking. In case (2), we cannot compare functions by pointer equality (because they must be regenerated on unmarshelling when `Require`ing a .vo file), and we also cannot rely on any sort of unique key being both unique and persistent across files. The solution we use here is that we ask clients to provide "unique" keys, and that clients tell us whether or not to overwrite existing registered functions, i.e., to tell us whether or not we should expect interpreter functions to be globally unique under pointer equality. For plugins, a simple string suffices, as long as the string does not clash between different plugins. In the case of vernacular-registered functions, use marshell a description of all of the data used to generate the function, and use that string as a unique key which is expected to persist across files. Because we cannot rely on function-pointer uniqueness here, we tell the interpretation-registration to allow overwriting. ---- Some of this code is response to comments on the PR ---- Some code is to fix an issue that bignums revealed: Both Int31 and bignums registered numeral notations in int31_scope. We now prepend a globally unique identifier when registering numeral notations from OCaml plugins. This is permissible because we don't store the uid information for such notations in .vo files (assuming I'm understanding the code correctly). --- theories/Numbers/AltBinNotations.v | 45 +++++++++++++++++++------------------- 1 file changed, 23 insertions(+), 22 deletions(-) (limited to 'theories') 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 *) -(* of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b)) end. +Numeral Notation Z of_int to_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. -- cgit v1.2.3