diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-08 17:12:59 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-27 19:31:49 +0100 |
commit | e4a09fc480f512f54d5e7ba05d7e408dc5817a46 (patch) | |
tree | 3ce040b7abb1860a3dc60aade92e454c121c355b | |
parent | 97960e114e72bc38814e78a71f06aca4fdfc4512 (diff) |
Selecting which notation to print based on current stack of scope.
See discussion on coq-club starting on 23 August 2016.
An open question: what priority to give to "abbreviations"?
-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 | 2 | ||||
-rw-r--r-- | test-suite/output/Notations2.v | 1 | ||||
-rw-r--r-- | test-suite/output/Notations3.out | 10 | ||||
-rw-r--r-- | test-suite/output/Notations3.v | 58 |
10 files changed, 114 insertions, 24 deletions
@@ -7,6 +7,10 @@ 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. Tactics diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e1df24f71..bc8debd02 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -383,7 +383,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 pat) + (uninterp_cases_pattern_notations scopes pat) with No_match -> lift (fun ?loc -> function | PatVar (Name id) -> CPatAtom (Some (Ident (loc,id))) @@ -514,7 +514,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 ind) + (uninterp_ind_pattern_notations scopes 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 @@ -734,7 +734,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 r'') + extern_notation scopes vars r'' (uninterp_notations scopes 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 f36294f73..94ce2a6c8 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -526,15 +526,38 @@ let interp_notation ?loc ntn local_scopes = user_err ?loc (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".") -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 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 availability_of_notation (ntn_scope,ntn) scopes = let f scope = diff --git a/interp/notation.mli b/interp/notation.mli index 2066d346f..7d055571c 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -124,9 +124,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 : '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 +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 (** 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 7bcd7b041..2f0ee765d 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. -SUM (nat * nat) nat +(nat * nat + nat)%type : 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 +(false && I 3)%bool /\ (I 6)%bool : 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 fe6c05c39..413812ee1 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). +Notation "! A" := (forall _:nat, A) (at level 60) : type_scope. 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). +Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10) : bool_scope. -Check (false && I 3)%bool /\ I 6. +Check (false && I 3)%bool /\ (I 6)%bool. (**********************************************************************) (* Check notations with several recursive patterns *) diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 1ec701ae8..ecb8d2c9f 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -41,7 +41,7 @@ Notation plus2 n := (S(S(n))) match n with | nil => 2 | 0 :: _ => 2 -| list1 => 0 +| 1 :: nil => 0 | 1 :: _ :: _ => 2 | plus2 _ :: _ => 2 end diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index ceb29d1b9..0dcb74652 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -70,6 +70,7 @@ 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 6ef75dd13..1b5725275 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -128,3 +128,13 @@ 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 diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 1f142cf47..a8d6c97fb 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)). +Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)) : type_scope. Check forall n:nat, {# n | 1 > n}. Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop. @@ -197,7 +197,59 @@ Check !!! (x y:nat), True. (* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) -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"). +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. 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. |