From 77ef9a400cd570e0857a45c015bca0308e2a0eff Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 24 Aug 2017 15:34:12 +0200 Subject: User-level support for Gonthier-Ssreflect's "if t then pat then u else v". --- theories/Init/Notations.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'theories') diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 5e8d2faa58..0c212b025a 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -78,6 +78,18 @@ Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99). Reserved Notation "{ x : A & P }" (at level 0, x at level 99). Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99). +(** Support for Gonthier-Ssreflect's "if c is pat then u else v" *) + +Module IfNotations. + +Notation "'if' c 'is' p 'then' u 'else' v" := + (match c with p => u | _ => v end) + (at level 200, p pattern at level 100). + +End IfNotations. + +(** Scopes *) + Delimit Scope type_scope with type. Delimit Scope function_scope with function. Delimit Scope core_scope with core. -- cgit v1.2.3 From 5b2f29e461d7dfb1336117050cc8c5d510025bf1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 22 Aug 2017 01:22:21 +0200 Subject: More structured printing in unicode notations for binders. --- theories/Unicode/Utf8_core.v | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'theories') diff --git a/theories/Unicode/Utf8_core.v b/theories/Unicode/Utf8_core.v index a0545c0a46..95c8336d2a 100644 --- a/theories/Unicode/Utf8_core.v +++ b/theories/Unicode/Utf8_core.v @@ -10,10 +10,12 @@ (* Logic *) -Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) - (at level 200, x binder, y binder, right associativity) : type_scope. -Notation "∃ x .. y , P" := (exists x, .. (exists y, P) ..) - (at level 200, x binder, y binder, right associativity) : type_scope. +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' ∀ x .. y ']' , P") : type_scope. +Notation "∃ x .. y , P" := (exists x, .. (exists y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' ∃ x .. y ']' , P") : type_scope. Notation "x ∨ y" := (x \/ y) (at level 85, right associativity) : type_scope. Notation "x ∧ y" := (x /\ y) (at level 80, right associativity) : type_scope. @@ -25,5 +27,6 @@ Notation "¬ x" := (~x) (at level 75, right associativity) : type_scope. Notation "x ≠ y" := (x <> y) (at level 70) : type_scope. (* Abstraction *) -Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) - (at level 200, x binder, y binder, right associativity). +Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' 'λ' x .. y ']' , t"). -- cgit v1.2.3 From 9fe03a830ae7b10e1c5fb2b9d41213257bd617f0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 3 Nov 2017 11:48:36 +0100 Subject: Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc. --- theories/Init/Logic.v | 7 +++++++ theories/Init/Specif.v | 26 ++++++++++++++++++++++++++ 2 files changed, 33 insertions(+) (limited to 'theories') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 037d37daff..053ed601f0 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -267,6 +267,13 @@ Notation "'exists2' x : A , p & q" := (ex2 (A:=A) (fun x => p) (fun x => q)) format "'[' 'exists2' '/ ' x : A , '/ ' '[' p & '/' q ']' ']'") : type_scope. +Notation "'exists2' ' x , p & q" := (ex2 (fun x => p) (fun x => q)) + (at level 200, x strict pattern, p at level 200, right associativity) : type_scope. +Notation "'exists2' ' x : A , p & q" := (ex2 (A:=A) (fun x => p) (fun x => q)) + (at level 200, x strict pattern, A at level 200, p at level 200, right associativity, + format "'[' 'exists2' '/ ' ' x : A , '/ ' '[' p & '/' q ']' ']'") + : type_scope. + (** Derived rules for universal quantification *) Section universal_quantification. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 3b4f833a31..ef95aef500 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -53,6 +53,32 @@ Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope. Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) : type_scope. +Module SpecifPatternNotations. + +Reserved Notation "{ ' pat | P }" + (at level 0, pat strict pattern, format "{ ' pat | P }"). +Reserved Notation "{ ' pat | P & Q }" + (at level 0, pat strict pattern, format "{ ' pat | P & Q }"). +Reserved Notation "{ ' pat : A | P }" + (at level 0, pat strict pattern, format "{ ' pat : A | P }"). +Reserved Notation "{ ' pat : A | P & Q }" + (at level 0, pat strict pattern, format "{ ' pat : A | P & Q }"). +Reserved Notation "{ ' pat : A & P }" + (at level 0, pat strict pattern, format "{ ' pat : A & P }"). +Reserved Notation "{ ' pat : A & P & Q }" + (at level 0, pat strict pattern, format "{ ' pat : A & P & Q }"). + +Notation "{ ' pat | P }" := (sig (fun pat => P)) : type_scope. +Notation "{ ' pat | P & Q }" := (sig2 (fun pat => P) (fun pat => Q)) : type_scope. +Notation "{ ' pat : A | P }" := (sig (A:=A) (fun pat => P)) : type_scope. +Notation "{ ' pat : A | P & Q }" := (sig2 (A:=A) (fun pat => P) (fun pat => Q)) : + type_scope. +Notation "{ ' pat : A & P }" := (sigT (A:=A) (fun pat => P)) : type_scope. +Notation "{ ' pat : A & P & Q }" := (sigT2 (A:=A) (fun pat => P) (fun pat => Q)) : + type_scope. + +End SpecifPatternNotations. + Add Printing Let sig. Add Printing Let sig2. Add Printing Let sigT. -- cgit v1.2.3 From 0af54860172efe1aa5da419b81e4cb34348320ee Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 23 Nov 2017 13:42:41 +0100 Subject: Trying a hack to support {'pat|P} without breaking compatibility. Concretely, we bypass the following limitation: The notation "{ ' pat | P }" broke the parsing of expressions of the form "{ forall x, P } + { Q }". Indeed the latter works thanks to a tolerance of Camlp5 in parsing "forall x, P" at level 200 while the rule asks to actually parse the interior of "{ ... }" at level 99 (the reason for 99 is to be below the rule for "M : T" which is at level 100, so that "{ x : A | P }" does not see "x : A" as a cast). Adding an extra "'"; pat = pattern in parallel to c = constr LEVEL "99" broke the tolerance for constr at level 200. We fix this by adding an ad hoc rule for "{ binder_constr }" in the native grammar (g_constr.ml4). Actually, this is inconsistent with having a rule for "{ constr at level 99 }" in Notations.v. We should have both rules in Notations.v or both rules hard-wired in the native grammar. But I still don't know what is the best decision to take, so leaving as it at the current time. Advantages of hard-wiring both rules in g_constr.ml4: a bit simpler in metasyntax.ml (no need to ensure that the rule exist). Disadvantages: if one wants a different initial state without the business needing the "{ }" for sumbool, sumor, sig, sigT, one still have the rules there. Advantages of having them in Notations.v: more modular, we can change the initial state. Disadvantages: one would need a new kind of modifier, something like "x at level 99 || binder_constr", with all the difficulty to find a nice, intuitive, name for "binder_constr", and the difficulty of understanding if there is a generality to this "||" disjunction operator, and whether it should be documented or not. --- theories/Init/Notations.v | 15 +++++++++++++++ theories/Init/Specif.v | 17 ----------------- 2 files changed, 15 insertions(+), 17 deletions(-) (limited to 'theories') diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 0c212b025a..a9051e761b 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -78,6 +78,21 @@ Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99). Reserved Notation "{ x : A & P }" (at level 0, x at level 99). Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99). +Reserved Notation "{ ' pat | P }" + (at level 0, pat strict pattern, format "{ ' pat | P }"). +Reserved Notation "{ ' pat | P & Q }" + (at level 0, pat strict pattern, format "{ ' pat | P & Q }"). + +Reserved Notation "{ ' pat : A | P }" + (at level 0, pat strict pattern, format "{ ' pat : A | P }"). +Reserved Notation "{ ' pat : A | P & Q }" + (at level 0, pat strict pattern, format "{ ' pat : A | P & Q }"). + +Reserved Notation "{ ' pat : A & P }" + (at level 0, pat strict pattern, format "{ ' pat : A & P }"). +Reserved Notation "{ ' pat : A & P & Q }" + (at level 0, pat strict pattern, format "{ ' pat : A & P & Q }"). + (** Support for Gonthier-Ssreflect's "if c is pat then u else v" *) Module IfNotations. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index ef95aef500..47e8a7558e 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -53,21 +53,6 @@ Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope. Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) : type_scope. -Module SpecifPatternNotations. - -Reserved Notation "{ ' pat | P }" - (at level 0, pat strict pattern, format "{ ' pat | P }"). -Reserved Notation "{ ' pat | P & Q }" - (at level 0, pat strict pattern, format "{ ' pat | P & Q }"). -Reserved Notation "{ ' pat : A | P }" - (at level 0, pat strict pattern, format "{ ' pat : A | P }"). -Reserved Notation "{ ' pat : A | P & Q }" - (at level 0, pat strict pattern, format "{ ' pat : A | P & Q }"). -Reserved Notation "{ ' pat : A & P }" - (at level 0, pat strict pattern, format "{ ' pat : A & P }"). -Reserved Notation "{ ' pat : A & P & Q }" - (at level 0, pat strict pattern, format "{ ' pat : A & P & Q }"). - Notation "{ ' pat | P }" := (sig (fun pat => P)) : type_scope. Notation "{ ' pat | P & Q }" := (sig2 (fun pat => P) (fun pat => Q)) : type_scope. Notation "{ ' pat : A | P }" := (sig (A:=A) (fun pat => P)) : type_scope. @@ -77,8 +62,6 @@ Notation "{ ' pat : A & P }" := (sigT (A:=A) (fun pat => P)) : type_scope. Notation "{ ' pat : A & P & Q }" := (sigT2 (A:=A) (fun pat => P) (fun pat => Q)) : type_scope. -End SpecifPatternNotations. - Add Printing Let sig. Add Printing Let sig2. Add Printing Let sigT. -- cgit v1.2.3