diff options
-rw-r--r-- | CHANGES | 4 | ||||
-rw-r--r-- | interp/constrextern.ml | 6 | ||||
-rw-r--r-- | interp/notation.ml | 41 | ||||
-rw-r--r-- | interp/notation.mli | 6 | ||||
-rw-r--r-- | test-suite/output/Notations.out | 4 | ||||
-rw-r--r-- | test-suite/output/Notations.v | 6 | ||||
-rw-r--r-- | test-suite/output/Notations2.out | 6 | ||||
-rw-r--r-- | test-suite/output/Notations2.v | 1 | ||||
-rw-r--r-- | test-suite/output/Notations3.out | 42 | ||||
-rw-r--r-- | test-suite/output/Notations3.v | 62 |
10 files changed, 41 insertions, 137 deletions
@@ -7,10 +7,6 @@ Notations right (e.g. "( x ; .. ; y ; z )") now supported. - Notations with a specific level for the leftmost nonterminal, when printing-only, are supported. -- When several notations are available for the same expression, - priority is given to latest notations defined in the scopes being - opened rather than to the latest notations defined independently of - whether they are in an opened scope or not. - Notations can now refer to the syntactic category of patterns (as in "fun 'pat =>" or "match p with pat => ... end"). Two variants are available, depending on whether a single variable is considered as a diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 949c7cbd8..9efaff3b9 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -386,7 +386,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = try if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation_pattern scopes vars pat - (uninterp_cases_pattern_notations scopes pat) + (uninterp_cases_pattern_notations pat) with No_match -> lift (fun ?loc -> function | PatVar (Name id) -> CPatAtom (Some (Ident (loc,id))) @@ -517,7 +517,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = try if !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation_ind_pattern scopes vars ind args - (uninterp_ind_pattern_notations scopes ind) + (uninterp_ind_pattern_notations ind) with No_match -> let c = extern_reference vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in @@ -741,7 +741,7 @@ let rec extern inctx scopes vars r = try let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation scopes vars r'' (uninterp_notations scopes r'') + extern_notation scopes vars r'' (uninterp_notations r'') with No_match -> lift (fun ?loc -> function | GRef (ref,us) -> extern_global (select_stronger_impargs (implicits_of_global ref)) diff --git a/interp/notation.ml b/interp/notation.ml index da3ed6b8c..47d648135 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -545,38 +545,15 @@ let interp_notation ?loc ntn local_scopes = user_err ?loc (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".") -let sort_notations scopes l = - let extract_scope l = function - | Scope sc -> List.partitioni (fun _i x -> - match x with - | NotationRule (Some sc',_),_,_ -> String.equal sc sc' - | _ -> false) l - | SingleNotation ntn -> List.partitioni (fun _i x -> - match x with - | NotationRule (None,ntn'),_,_ -> String.equal ntn ntn' - | _ -> false) l in - let rec aux l scopes = - if l == [] then [] (* shortcut *) else - match scopes with - | sc :: scopes -> let ntn_in_sc,l = extract_scope l sc in ntn_in_sc @ aux l scopes - | [] -> l in - aux l scopes - -let uninterp_notations scopes c = - let scopes = make_current_scopes scopes in - let keys = glob_constr_keys c in - let maps = List.map_append (fun key -> keymap_find key !notations_key_table) keys in - sort_notations scopes maps - -let uninterp_cases_pattern_notations scopes c = - let scopes = make_current_scopes scopes in - let maps = keymap_find (cases_pattern_key c) !notations_key_table in - sort_notations scopes maps - -let uninterp_ind_pattern_notations scopes ind = - let scopes = make_current_scopes scopes in - let maps = keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table in - sort_notations scopes maps +let uninterp_notations c = + List.map_append (fun key -> keymap_find key !notations_key_table) + (glob_constr_keys c) + +let uninterp_cases_pattern_notations c = + keymap_find (cases_pattern_key c) !notations_key_table + +let uninterp_ind_pattern_notations ind = + keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table let availability_of_notation (ntn_scope,ntn) scopes = let f scope = diff --git a/interp/notation.mli b/interp/notation.mli index aa52b858a..6803a7e51 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -126,9 +126,9 @@ val interp_notation : ?loc:Loc.t -> notation -> local_scopes -> type notation_rule = interp_rule * interpretation * int option (** Return the possible notations for a given term *) -val uninterp_notations : local_scopes -> 'a glob_constr_g -> notation_rule list -val uninterp_cases_pattern_notations : local_scopes -> 'a cases_pattern_g -> notation_rule list -val uninterp_ind_pattern_notations : local_scopes -> inductive -> notation_rule list +val uninterp_notations : 'a glob_constr_g -> notation_rule list +val uninterp_cases_pattern_notations : 'a cases_pattern_g -> notation_rule list +val uninterp_ind_pattern_notations : inductive -> notation_rule list (** Test if a notation is available in the scopes context [scopes]; if available, the result is not None; the first diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 891296b0a..b60b1ee86 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -64,7 +64,7 @@ The command has indeed failed with message: Cannot find where the recursive pattern starts. The command has indeed failed with message: Both ends of the recursive pattern are the same. -(nat * nat + nat)%type +SUM (nat * nat) nat : Set FST (0; 1) : Z @@ -72,7 +72,7 @@ Nil : forall A : Type, list A NIL : list nat : list nat -(false && I 3)%bool /\ (I 6)%bool +(false && I 3)%bool /\ I 6 : Prop [|1, 2, 3; 4, 5, 6|] : Z * Z * Z * (Z * Z * Z) diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 413812ee1..fe6c05c39 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -30,7 +30,7 @@ Check (decomp (true,true) as t, u in (t,u)). Section A. -Notation "! A" := (forall _:nat, A) (at level 60) : type_scope. +Notation "! A" := (forall _:nat, A) (at level 60). Check ! (0=0). Check forall n, n=0. @@ -194,9 +194,9 @@ Open Scope nat_scope. Coercion is_true := fun b => b=true. Coercion of_nat n := match n with 0 => true | _ => false end. -Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10) : bool_scope. +Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10). -Check (false && I 3)%bool /\ (I 6)%bool. +Check (false && I 3)%bool /\ I 6. (**********************************************************************) (* Check notations with several recursive patterns *) diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 6ffe56e11..41d159375 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -37,13 +37,13 @@ let' f (x y : nat) (a := 0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 : (nat -> nat) -> nat -> nat Notation plus2 n := (S(S(n))) λ n : list(nat), match n with - | 1 :: nil => 0 + | list1 => 0 | _ => 2 end : list(nat) -> nat λ n : list(nat), match n with -| 1 :: nil => 0 +| list1 => 0 | nil | 0 :: _ | 1 :: _ :: _ | plus2 _ :: _ => 2 end : list(nat) -> nat @@ -51,7 +51,7 @@ end match n with | nil => 2 | 0 :: _ => 2 -| 1 :: nil => 0 +| list1 => 0 | 1 :: _ :: _ => 2 | plus2 _ :: _ => 2 end diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 923caedac..bcb246879 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -71,7 +71,6 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2. (* Note: does not work for pattern *) Module A. Notation "f ( x )" := (f x) (at level 10, format "f ( x )"). -Open Scope nat_scope. Check fun f x => f x + S x. Open Scope list_scope. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 864b6151a..1987b6a6e 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -128,37 +128,25 @@ return (1, 2, 3, 4) : nat *(1.2) : nat -[{0; 0}] - : list (list nat) -[{1; 2; 3}; - {4; 5; 6}; - {7; 8; 9}] - : list (list nat) -amatch = mmatch 0 (with 0 => 1| 1 => 2 end) - : unit -alist = [0; 1; 2] - : list nat -! '{{x, y}}, x + y = 0 +! '{{x, y}}, x.y = 0 : Prop exists x : nat, nat -> exists y : nat, - nat -> - exists '{{u, t}}, forall z1 : nat, z1 = 0 /\ x + y = 0 /\ u + t = 0 + nat -> exists '{{u, t}}, forall z1 : nat, z1 = 0 /\ x.y = 0 /\ u.t = 0 : Prop exists x : nat, nat -> exists y : nat, - nat -> - exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x + y = 0 /\ z + t = 0 + nat -> exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x.y = 0 /\ z.t = 0 : Prop -exists_true '{{x, y}} (u := 0) '{{z, t}}, x + y = 0 /\ z + t = 0 +exists_true '{{x, y}} (u := 0) '{{z, t}}, x.y = 0 /\ z.t = 0 : Prop exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R), (forall x : A, R x x) : Prop exists_true (x : nat) (A : Type) (R : A -> A -> Prop) -(_ : Reflexive R) (y : nat), x + y = 0 -> forall z : A, R z z +(_ : Reflexive R) (y : nat), x.y = 0 -> forall z : A, R z z : Prop {{{{True, nat -> True}}, nat -> True}} : Prop * Prop * Prop @@ -194,22 +182,22 @@ pair (prod nat (prod nat nat))) (prod (prod nat nat) nat) fun x : nat => if x is n .+ 1 then n else 1 : nat -> nat -{'{{x, y}} : nat * nat | x + y = 0} +{'{{x, y}} : nat * nat | x.y = 0} : Set exists2' {{x, y}}, x = 0 & y = 0 : Prop myexists2 x : nat * nat, let '{{y, z}} := x in y > z & let '{{y, z}} := x in z > y : Prop -fun '({{x, y}} as z) => x + y = 0 /\ z = z +fun '({{x, y}} as z) => x.y = 0 /\ z = z : nat * nat -> Prop -myexists ({{x, y}} as z), x + y = 0 /\ z = z +myexists ({{x, y}} as z), x.y = 0 /\ z = z : Prop -exists '({{x, y}} as z), x + y = 0 /\ z = z +exists '({{x, y}} as z), x.y = 0 /\ z = z : Prop -∀ '({{x, y}} as z), x + y = 0 /\ z = z +∀ '({{x, y}} as z), x.y = 0 /\ z = z : Prop -fun '({{{{x, y}}, true}} | {{{{x, y}}, false}}) => x + y +fun '({{{{x, y}}, true}} | {{{{x, y}}, false}}) => x.y : nat * nat * bool -> nat myexists ({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y : Prop @@ -221,17 +209,17 @@ fun p : nat => if p is S n then n else 0 : nat -> nat fun p : comparison => if p is Lt then 1 else 0 : comparison -> nat -fun S : nat => [S | S + S] +fun S : nat => [S | S.S] : nat -> nat * (nat -> nat) -fun N : nat => [N | N + 0] +fun N : nat => [N | N.0] : nat -> nat * (nat -> nat) -fun S : nat => [[S | S + S]] +fun S : nat => [[S | S.S]] : nat -> nat * (nat -> nat) {I : nat | I = I} : Set {'I : True | I = I} : Prop -{'{{x, y}} : nat * nat | x + y = 0} +{'{{x, y}} : nat * nat | x.y = 0} : Set exists2 '{{y, z}} : nat * nat, y > z & z > y : Prop diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index c98bfff41..c165f9553 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -59,7 +59,7 @@ Check fun f => CURRYINVLEFT (x:nat) (y:bool), f. (* Notations with variables bound both as a term and as a binder *) (* This is #4592 *) -Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)) : type_scope. +Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)). Check forall n:nat, {# n | 1 > n}. Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop. @@ -183,13 +183,9 @@ Check letpair x [1] = {0}; return (1,2,3,4). (* Test spacing in #5569 *) -Section S1. -Variable plus : nat -> nat -> nat. -Infix "+" := plus. Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). Check 1+1+1. -End S1. (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *) Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). @@ -197,62 +193,10 @@ Check !!! (x y:nat), True. (* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) -Section S2. -Notation "* x" := (id x) (only printing, at level 15, format "* x") : nat_scope. -Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y") : nat_scope. +Notation "* x" := (id x) (only printing, at level 15, format "* x"). +Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y"). Check (((id 1) + 2) + 3). Check (id (1 + 2)). -End S2. - -(* Test printing of notations guided by scope *) - -Module A. - -Delimit Scope line_scope with line. -Notation "{ }" := nil (format "{ }") : line_scope. -Notation "{ x }" := (cons x nil) : line_scope. -Notation "{ x ; y ; .. ; z }" := (cons x (cons y .. (cons z nil) ..)) : line_scope. -Notation "[ ]" := nil (format "[ ]") : matx_scope. -Notation "[ l ]" := (cons l%line nil) : matx_scope. -Notation "[ l ; l' ; .. ; l'' ]" := (cons l%line (cons l'%line .. (cons l''%line nil) ..)) - (format "[ '[v' l ; '/' l' ; '/' .. ; '/' l'' ']' ]") : matx_scope. - -Open Scope matx_scope. -Check [[0;0]]. -Check [[1;2;3];[4;5;6];[7;8;9]]. - -End A. - -(* Example by Beta Ziliani *) - -Require Import Lists.List. - -Module B. - -Import ListNotations. - -Delimit Scope pattern_scope with pattern. -Delimit Scope patterns_scope with patterns. - -Notation "a => b" := (a, b) (at level 201) : pattern_scope. -Notation "'with' p1 | .. | pn 'end'" := - ((cons p1%pattern (.. (cons pn%pattern nil) ..))) - (at level 91, p1 at level 210, pn at level 210) : patterns_scope. - -Definition mymatch (n:nat) (l : list (nat * nat)) := tt. -Arguments mymatch _ _%patterns. -Notation "'mmatch' n ls" := (mymatch n ls) (at level 0). - -Close Scope patterns_scope. -Close Scope pattern_scope. - -Definition amatch := mmatch 0 with 0 => 1 | 1 => 2 end. -Print amatch. (* Good: amatch = mmatch 0 (with 0 => 1| 1 => 2 end) *) - -Definition alist := [0;1;2]. -Print alist. - -End B. (* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *) (* for isolated "forall" (was not working already in 8.6) *) |