aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/sphinx/user-extensions/syntax-extensions.rst4
-rw-r--r--interp/constrexpr.ml10
-rw-r--r--interp/constrexpr_ops.ml20
-rw-r--r--interp/constrextern.ml68
-rw-r--r--interp/constrintern.ml18
-rw-r--r--interp/implicit_quantifiers.ml2
-rw-r--r--interp/notation.ml36
-rw-r--r--interp/notation.mli12
-rw-r--r--parsing/g_constr.mlg6
-rw-r--r--parsing/notgram_ops.ml20
-rw-r--r--parsing/notgram_ops.mli8
-rw-r--r--parsing/ppextend.ml61
-rw-r--r--parsing/ppextend.mli17
-rw-r--r--plugins/ssrmatching/ssrmatching.ml8
-rw-r--r--printing/ppconstr.ml16
-rw-r--r--printing/proof_diffs.ml2
-rw-r--r--test-suite/output/Notations4.out32
-rw-r--r--test-suite/output/Notations4.v81
-rw-r--r--vernac/egramcoq.ml4
-rw-r--r--vernac/metasyntax.ml209
20 files changed, 450 insertions, 184 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index a8d5ac610f..04419f08f7 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -163,6 +163,10 @@ Grammar constr` is at level 100. To avoid ``x : A`` being parsed as a type cast,
it is necessary to put ``x`` at a level below 100, typically 99. Hence, a correct
definition is the following:
+.. coqtop:: none
+
+ Reset Initial.
+
.. coqtop:: all
Notation "{ x : A | P }" := (sig A (fun x => P)) (x at level 99).
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index b96ef7c4e5..1d51109b7f 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -19,11 +19,17 @@ type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.g
type ident_decl = lident * universe_decl_expr option
type name_decl = lname * universe_decl_expr option
+type notation_with_optional_scope = LastLonelyNotation | NotationInScope of string
type notation_entry = InConstrEntry | InCustomEntry of string
type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * int
type notation_key = string
+
+(* A notation associated to a given parsing rule *)
type notation = notation_entry_level * notation_key
+(* A notation associated to a given interpretation *)
+type specific_notation = notation_with_optional_scope * notation
+
type 'a or_by_notation_r =
| AN of 'a
| ByNotation of (string * string option)
@@ -78,7 +84,7 @@ type cases_pattern_expr_r =
(** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *)
| CPatAtom of qualid option
| CPatOr of cases_pattern_expr list
- | CPatNotation of notation * cases_pattern_notation_substitution
+ | CPatNotation of notation_with_optional_scope option * notation * cases_pattern_notation_substitution
* cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents
(notation n applied with substitution l1)
applied to arguments l2 *)
@@ -119,7 +125,7 @@ and constr_expr_r =
| CEvar of Glob_term.existential_name * (Id.t * constr_expr) list
| CSort of Glob_term.glob_sort
| CCast of constr_expr * constr_expr Glob_term.cast_type
- | CNotation of notation * constr_notation_substitution
+ | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
| CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr
| CPrim of prim_token
| CDelimiters of string * constr_expr
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index b4798127f9..401853b625 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -75,7 +75,8 @@ let rec cases_pattern_expr_eq p1 p2 =
Option.equal qualid_eq r1 r2
| CPatOr a1, CPatOr a2 ->
List.equal cases_pattern_expr_eq a1 a2
- | CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) ->
+ | CPatNotation (inscope1, n1, s1, l1), CPatNotation (inscope2, n2, s2, l2) ->
+ Option.equal notation_with_optional_scope_eq inscope1 inscope2 &&
notation_eq n1 n2 &&
cases_pattern_notation_substitution_eq s1 s2 &&
List.equal cases_pattern_expr_eq l1 l2
@@ -160,7 +161,8 @@ let rec constr_expr_eq e1 e2 =
Glob_ops.glob_sort_eq s1 s2
| CCast(t1,c1), CCast(t2,c2) ->
constr_expr_eq t1 t2 && cast_expr_eq c1 c2
- | CNotation(n1, s1), CNotation(n2, s2) ->
+ | CNotation(inscope1, n1, s1), CNotation(inscope2, n2, s2) ->
+ Option.equal notation_with_optional_scope_eq inscope1 inscope2 &&
notation_eq n1 n2 &&
constr_notation_substitution_eq s1 s2
| CPrim i1, CPrim i2 ->
@@ -271,7 +273,7 @@ let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with
| CPatCstr (_,patl1,patl2) ->
List.fold_left (cases_pattern_fold_names f)
(Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2
- | CPatNotation (_,(patl,patll),patl') ->
+ | CPatNotation (_,_,(patl,patll),patl') ->
List.fold_left (cases_pattern_fold_names f)
(List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl'
| CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat
@@ -320,7 +322,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b
| CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
| CCast (a,CastCoerce) -> f n acc a
- | CNotation (_,(l,ll,bl,bll)) ->
+ | CNotation (_,_,(l,ll,bl,bll)) ->
(* The following is an approximation: we don't know exactly if
an ident is binding nor to which subterms bindings apply *)
let acc = List.fold_left (f n) acc (l@List.flatten ll) in
@@ -399,9 +401,9 @@ let map_constr_expr_with_binders g f e = CAst.map (function
| CLetIn (na,a,t,b) ->
CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b)
| CCast (a,c) -> CCast (f e a, Glob_ops.map_cast_type (f e) c)
- | CNotation (n,(l,ll,bl,bll)) ->
+ | CNotation (inscope,n,(l,ll,bl,bll)) ->
(* This is an approximation because we don't know what binds what *)
- CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, bl,
+ CNotation (inscope,n,(List.map (f e) l,List.map (List.map (f e)) ll, bl,
List.map (fun bl -> snd (map_local_binders f g e bl)) bll))
| CGeneralization (b,a,c) -> CGeneralization (b,a,f e c)
| CDelimiters (s,a) -> CDelimiters (s,f e a)
@@ -574,7 +576,7 @@ let mkAppPattern ?loc p lp =
CErrors.user_err ?loc:p.loc ~hdr:"compound_pattern"
(Pp.str "Nested applications not supported.")
| CPatCstr (r, l1, l2) -> CPatCstr (r, l1 , l2@lp)
- | CPatNotation (n, s, l) -> CPatNotation (n , s, l@lp)
+ | CPatNotation (inscope, n, s, l) -> CPatNotation (inscope, n , s, l@lp)
| _ -> CErrors.user_err
?loc:p.loc ~hdr:"compound_pattern"
(Pp.str "Such pattern cannot have arguments."))
@@ -591,8 +593,8 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
(mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v
| CAppExpl ((None,r,i),args) ->
CPatCstr (r,Some (List.map coerce_to_cases_pattern_expr args),[])
- | CNotation (ntn,(c,cl,[],[])) ->
- CPatNotation (ntn,(List.map coerce_to_cases_pattern_expr c,
+ | CNotation (inscope,ntn,(c,cl,[],[])) ->
+ CPatNotation (inscope,ntn,(List.map coerce_to_cases_pattern_expr c,
List.map (List.map coerce_to_cases_pattern_expr) cl),[])
| CPrim p ->
CPatPrim p
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 06232b8e1a..a0f4bdcca1 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -75,10 +75,10 @@ let inactive_notations_table =
let inactive_scopes_table =
Summary.ref ~name:"inactive_scopes_table" CString.Set.empty
-let show_scope scopt =
- match scopt with
- | None -> str ""
- | Some sc -> spc () ++ str "in scope" ++ spc () ++ str sc
+let show_scope inscope =
+ match inscope with
+ | LastLonelyNotation -> str ""
+ | NotationInScope sc -> spc () ++ str "in scope" ++ spc () ++ str sc
let _show_inactive_notations () =
begin
@@ -97,8 +97,8 @@ let _show_inactive_notations () =
let _ = Feedback.msg_notice (str "Inactive notations:") in
IRuleSet.iter
(function
- | NotationRule (scopt, ntn) ->
- Feedback.msg_notice (pr_notation ntn ++ show_scope scopt)
+ | NotationRule (inscope, ntn) ->
+ Feedback.msg_notice (pr_notation ntn ++ show_scope inscope)
| SynDefRule kn -> Feedback.msg_notice (str (string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn))))
!inactive_notations_table
@@ -107,18 +107,19 @@ let deactivate_notation nr =
| SynDefRule kn ->
(* shouldn't we check whether it is well defined? *)
inactive_notations_table := IRuleSet.add nr !inactive_notations_table
- | NotationRule (scopt, ntn) ->
- match availability_of_notation (scopt, ntn) (scopt, []) with
+ | NotationRule (inscope, ntn) ->
+ let scopt = match inscope with NotationInScope sc -> Some sc | LastLonelyNotation -> None in
+ match availability_of_notation (inscope, ntn) (scopt, []) with
| None -> user_err ~hdr:"Notation"
(pr_notation ntn ++ spc () ++ str "does not exist"
- ++ (match scopt with
- | None -> spc () ++ str "in the empty scope."
- | Some _ -> show_scope scopt ++ str "."))
+ ++ (match inscope with
+ | LastLonelyNotation -> spc () ++ str "in the empty scope."
+ | NotationInScope _ -> show_scope inscope ++ str "."))
| Some _ ->
if IRuleSet.mem nr !inactive_notations_table then
Feedback.msg_warning
(str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
- ++ str "is already inactive" ++ show_scope scopt ++ str ".")
+ ++ str "is already inactive" ++ show_scope inscope ++ str ".")
else inactive_notations_table := IRuleSet.add nr !inactive_notations_table
let reactivate_notation nr =
@@ -127,9 +128,9 @@ let reactivate_notation nr =
IRuleSet.remove nr !inactive_notations_table
with Not_found ->
match nr with
- | NotationRule (scopt, ntn) ->
+ | NotationRule (inscope, ntn) ->
Feedback.msg_warning (str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
- ++ str "is already active" ++ show_scope scopt ++
+ ++ str "is already active" ++ show_scope inscope ++
str ".")
| SynDefRule kn ->
let s = string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) in
@@ -157,8 +158,8 @@ let reactivate_scope sc =
let is_inactive_rule nr =
IRuleSet.mem nr !inactive_notations_table ||
match nr with
- | NotationRule (Some sc, ntn) -> CString.Set.mem sc !inactive_scopes_table
- | NotationRule (None, ntn) -> false
+ | NotationRule (NotationInScope sc, ntn) -> CString.Set.mem sc !inactive_scopes_table
+ | NotationRule (LastLonelyNotation, ntn) -> false
| SynDefRule _ -> false
(* args: notation, scope, activate/deactivate *)
@@ -169,10 +170,13 @@ let toggle_scope_printing ~scope ~activate =
deactivate_scope scope
let toggle_notation_printing ?scope ~notation ~activate =
+ let inscope = match scope with
+ | None -> LastLonelyNotation
+ | Some sc -> NotationInScope sc in
if activate then
- reactivate_notation (NotationRule (scope, notation))
+ reactivate_notation (NotationRule (inscope, notation))
else
- deactivate_notation (NotationRule (scope, notation))
+ deactivate_notation (NotationRule (inscope, notation))
(* This governs printing of projections using the dot notation symbols *)
let print_projections = ref false
@@ -254,11 +258,11 @@ let insert_pat_alias ?loc p = function
let rec insert_coercion ?loc l c = match l with
| [] -> c
- | ntn::l -> CAst.make ?loc @@ CNotation (ntn,([insert_coercion ?loc l c],[],[],[]))
+ | (inscope,ntn)::l -> CAst.make ?loc @@ CNotation (Some inscope,ntn,([insert_coercion ?loc l c],[],[],[]))
let rec insert_pat_coercion ?loc l c = match l with
| [] -> c
- | ntn::l -> CAst.make ?loc @@ CPatNotation (ntn,([insert_pat_coercion ?loc l c],[]),[])
+ | (inscope,ntn)::l -> CAst.make ?loc @@ CPatNotation (Some inscope,ntn,([insert_pat_coercion ?loc l c],[]),[])
(**********************************************************************)
(* conversion of references *)
@@ -348,19 +352,19 @@ let make_notation_gen loc ntn mknot mkprim destprim l bl =
| None -> mknot (loc,ntn,l,bl) end
| _ -> mknot (loc,ntn,l,bl)
-let make_notation loc ntn (terms,termlists,binders,binderlists as subst) =
+let make_notation loc (inscope,ntn) (terms,termlists,binders,binderlists as subst) =
if not (List.is_empty termlists) || not (List.is_empty binderlists) then
- CAst.make ?loc @@ CNotation (ntn,subst)
+ CAst.make ?loc @@ CNotation (Some inscope,ntn,subst)
else
make_notation_gen loc ntn
- (fun (loc,ntn,l,bl) -> CAst.make ?loc @@ CNotation (ntn,(l,[],bl,[])))
+ (fun (loc,ntn,l,bl) -> CAst.make ?loc @@ CNotation (Some inscope,ntn,(l,[],bl,[])))
(fun (loc,p) -> CAst.make ?loc @@ CPrim p)
destPrim terms binders
-let make_pat_notation ?loc ntn (terms,termlists as subst) args =
- if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (ntn,subst,args)) else
+let make_pat_notation ?loc (inscope,ntn) (terms,termlists as subst) args =
+ if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (Some inscope,ntn,subst,args)) else
make_notation_gen loc ntn
- (fun (loc,ntn,l,_) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args))
+ (fun (loc,ntn,l,_) -> CAst.make ?loc @@ CPatNotation (Some inscope,ntn,(l,[]),args))
(fun (loc,p) -> CAst.make ?loc @@ CPatPrim p)
destPatPrim terms []
@@ -450,12 +454,12 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
(custom, (tmp_scope, scopes) as allscopes) vars =
function
- | NotationRule (sc,ntn) ->
+ | NotationRule (_,ntn as specific_ntn) ->
begin
match availability_of_entry_coercion custom (fst ntn) with
| None -> raise No_match
| Some coercion ->
- match availability_of_notation (sc,ntn) (tmp_scope,scopes) with
+ match availability_of_notation specific_ntn (tmp_scope,scopes) with
(* Uninterpretation is not allowed in current context *)
| None -> raise No_match
(* Uninterpretation is allowed in current context *)
@@ -479,7 +483,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
in
insert_pat_coercion coercion
(insert_pat_delimiters ?loc
- (make_pat_notation ?loc ntn (l,ll) l2') key)
+ (make_pat_notation ?loc specific_ntn (l,ll) l2') key)
end
| SynDefRule kn ->
match availability_of_entry_coercion custom InConstrEntrySomeLevel with
@@ -1185,11 +1189,11 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
match_notation_constr !print_universes t pat in
(* Try availability of interpretation ... *)
match keyrule with
- | NotationRule (sc,ntn) ->
+ | NotationRule (_,ntn as specific_ntn) ->
(match availability_of_entry_coercion custom (fst ntn) with
| None -> raise No_match
| Some coercion ->
- match availability_of_notation (sc,ntn) scopes with
+ match availability_of_notation specific_ntn scopes with
(* Uninterpretation is not allowed in current context *)
| None -> raise No_match
(* Uninterpretation is allowed in current context *)
@@ -1212,7 +1216,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
List.map (fun (bl,(subentry,(scopt,scl))) ->
pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl))
binderlists in
- let c = make_notation loc ntn (l,ll,bl,bll) in
+ let c = make_notation loc specific_ntn (l,ll,bl,bll) in
let c = insert_coercion coercion (insert_delimiters c key) in
let args = fill_arg_scopes args argsscopes allscopes in
let args = extern_args (extern true) vars args in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b2c572d290..1cfd50e26e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -226,7 +226,7 @@ let contract_curly_brackets ntn (l,ll,bl,bll) =
let ntn' = ref ntn in
let rec contract_squash n = function
| [] -> []
- | { CAst.v = CNotation ((InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l ->
+ | { CAst.v = CNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
@@ -242,7 +242,7 @@ let contract_curly_brackets_pat ntn (l,ll) =
let ntn' = ref ntn in
let rec contract_squash n = function
| [] -> []
- | { CAst.v = CPatNotation ((InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l ->
+ | { CAst.v = CPatNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
@@ -1719,13 +1719,13 @@ let drop_notations_pattern looked_for genv =
(* but not scopes in expl_pl *)
let (argscs1,_) = find_remaining_scopes expl_pl pl g in
DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
- | CPatNotation ((InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a ->
+ | CPatNotation (_,(InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a ->
let p = match a.CAst.v with CPatPrim (Numeral (_, p)) -> p | _ -> assert false in
let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (SMinus,p)) scopes in
rcp_of_glob scopes pat
- | CPatNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) ->
+ | CPatNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) ->
in_pat top scopes a
- | CPatNotation (ntn,fullargs,extrargs) ->
+ | CPatNotation (_,ntn,fullargs,extrargs) ->
let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in
let ((ids',c),df) = Notation.interp_notation ?loc ntn scopes in
let (terms,termlists) = split_by_type_pat ?loc ids' (terms,termlists) in
@@ -2035,11 +2035,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
DAst.make ?loc @@
GLetIn (na.CAst.v, inc1, int,
intern_restart_binders (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2)
- | CNotation ((InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a ->
+ | CNotation (_,(InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a ->
let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in
intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p)))
- | CNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a
- | CNotation (ntn,args) ->
+ | CNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a
+ | CNotation (_,ntn,args) ->
intern_notation intern env ntnvars loc ntn args
| CGeneralization (b,a,c) ->
intern_generalization intern env ntnvars loc b a c
@@ -2070,7 +2070,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| CRef (ref,us) ->
intern_applied_reference ~isproj intern env
(Environ.named_context_val globalenv) lvar us args ref
- | CNotation (ntn,([],[],[],[])) ->
+ | CNotation (_,ntn,([],[],[],[])) ->
assert (Option.is_empty isproj);
let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in
let x, impl, scopes, l = find_appl_head_data c in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index ffbb982ab7..e6f12f7eb2 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -92,7 +92,7 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
let rec aux bdvars l c = match CAst.(c.v) with
| CRef (qid,_) when qualid_is_ident qid ->
found c.CAst.loc (qualid_basename qid) bdvars l
- | CNotation ((InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
+ | CNotation (_,(InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) ->
Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c
| _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
diff --git a/interp/notation.ml b/interp/notation.ml
index 789d59eda9..744528ca0b 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -49,6 +49,11 @@ let notation_entry_level_eq s1 s2 = match (s1,s2) with
| InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2
| (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false
+let notation_with_optional_scope_eq inscope1 inscope2 = match (inscope1,inscope2) with
+ | LastLonelyNotation, LastLonelyNotation -> true
+ | NotationInScope s1, NotationInScope s2 -> String.equal s1 s2
+ | (LastLonelyNotation | NotationInScope _), _ -> false
+
let notation_eq (from1,ntn1) (from2,ntn2) =
notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2
@@ -63,6 +68,15 @@ module NotationOrd =
module NotationSet = Set.Make(NotationOrd)
module NotationMap = CMap.Make(NotationOrd)
+module SpecificNotationOrd =
+ struct
+ type t = specific_notation
+ let compare = pervasives_compare
+ end
+
+module SpecificNotationSet = Set.Make(SpecificNotationOrd)
+module SpecificNotationMap = CMap.Make(SpecificNotationOrd)
+
(**********************************************************************)
(* Scope of symbols *)
@@ -254,7 +268,7 @@ let find_delimiters_scope ?loc key =
(* Uninterpretation tables *)
type interp_rule =
- | NotationRule of scope_name option * notation
+ | NotationRule of specific_notation
| SynDefRule of KerName.t
(* We define keys for glob_constr and aconstr to split the syntax entries
@@ -1064,8 +1078,8 @@ let check_required_module ?loc sc (sp,d) =
the scope stack [scopes], and if yes, using delimiters or not *)
let find_with_delimiters = function
- | None -> None
- | Some scope ->
+ | LastLonelyNotation -> None
+ | NotationInScope scope ->
match (String.Map.find scope !scope_map).delimiters with
| Some key -> Some (Some scope, Some key)
| None -> None
@@ -1074,7 +1088,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
| OpenScopeItem scope :: scopes ->
(* Is the expected ntn/numpr attached to the most recently open scope? *)
begin match ntn_scope with
- | Some scope' when String.equal scope scope' ->
+ | NotationInScope scope' when String.equal scope scope' ->
Some (None,None)
| _ ->
(* If the most recently open scope has a notation/numeral printer
@@ -1086,7 +1100,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
end
| LonelyNotationItem ntn' :: scopes ->
begin match ntn_scope, ntn with
- | None, Some ntn when notation_eq ntn ntn' ->
+ | LastLonelyNotation, Some ntn when notation_eq ntn ntn' ->
Some (None, None)
| _ ->
find_without_delimiters find (ntn_scope,ntn) scopes
@@ -1244,7 +1258,7 @@ let availability_of_notation (ntn_scope,ntn) scopes =
commonly from the lowest level of the source entry to the highest
level of the target entry. *)
-type entry_coercion = notation list
+type entry_coercion = (notation_with_optional_scope * notation) list
module EntryCoercionOrd =
struct
@@ -1295,7 +1309,7 @@ let rec insert_coercion_path path = function
else if shorter_path path path' then path::allpaths
else path'::insert_coercion_path path paths
-let declare_entry_coercion (entry,_ as ntn) entry' =
+let declare_entry_coercion (scope,(entry,_) as specific_ntn) entry' =
let entry, lev = decompose_custom_entry entry in
let entry', lev' = decompose_custom_entry entry' in
(* Transitive closure *)
@@ -1304,19 +1318,19 @@ let declare_entry_coercion (entry,_ as ntn) entry' =
List.fold_right (fun ((lev'',lev'''),path) l ->
if notation_entry_eq entry entry''' && level_ord lev lev''' &&
not (notation_entry_eq entry' entry'')
- then ((entry'',entry'),((lev'',lev'),path@[ntn]))::l else l) paths l)
+ then ((entry'',entry'),((lev'',lev'),path@[specific_ntn]))::l else l) paths l)
!entry_coercion_map [] in
let toaddright =
EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
List.fold_right (fun ((lev'',lev'''),path) l ->
if entry' = entry'' && level_ord lev' lev'' && entry <> entry'''
- then ((entry,entry'''),((lev,lev'''),path@[ntn]))::l else l) paths l)
+ then ((entry,entry'''),((lev,lev'''),path@[specific_ntn]))::l else l) paths l)
!entry_coercion_map [] in
entry_coercion_map :=
List.fold_right (fun (pair,path) ->
let olds = try EntryCoercionMap.find pair !entry_coercion_map with Not_found -> [] in
EntryCoercionMap.add pair (insert_coercion_path path olds))
- (((entry,entry'),((lev,lev'),[ntn]))::toaddright@toaddleft)
+ (((entry,entry'),((lev,lev'),[specific_ntn]))::toaddright@toaddleft)
!entry_coercion_map
let entry_has_global_map = ref String.Map.empty
@@ -1417,7 +1431,7 @@ let availability_of_prim_token n printer_scope local_scopes =
with Not_found -> false
in
let scopes = make_current_scopes local_scopes in
- Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes)
+ Option.map snd (find_without_delimiters f (NotationInScope printer_scope,None) scopes)
(* Miscellaneous *)
diff --git a/interp/notation.mli b/interp/notation.mli
index 707be6cb87..87f0ba63c8 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -25,11 +25,15 @@ val notation_entry_eq : notation_entry -> notation_entry -> bool
val notation_entry_level_eq : notation_entry_level -> notation_entry_level -> bool
(** Equality on [notation_entry_level]. *)
+val notation_with_optional_scope_eq : notation_with_optional_scope -> notation_with_optional_scope -> bool
+
val notation_eq : notation -> notation -> bool
(** Equality on [notation]. *)
module NotationSet : Set.S with type elt = notation
module NotationMap : CMap.ExtS with type key = notation and module Set := NotationSet
+module SpecificNotationSet : Set.S with type elt = specific_notation
+module SpecificNotationMap : CMap.ExtS with type key = specific_notation and module Set := SpecificNotationSet
(** {6 Scopes } *)
(** A scope is a set of interpreters for symbols + optional
@@ -213,7 +217,7 @@ val availability_of_prim_token :
(** Binds a notation in a given scope to an interpretation *)
type interp_rule =
- | NotationRule of scope_name option * notation
+ | NotationRule of specific_notation
| SynDefRule of KerName.t
val declare_notation_interpretation : notation -> scope_name option ->
@@ -236,7 +240,7 @@ 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
argument is itself not None if a delimiters is needed *)
-val availability_of_notation : scope_name option * notation -> subscopes ->
+val availability_of_notation : specific_notation -> subscopes ->
(scope_name option * delimiters option) option
(** {6 Miscellaneous} *)
@@ -299,8 +303,8 @@ val locate_notation : (glob_constr -> Pp.t) -> notation_key ->
val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t
-type entry_coercion = notation list
-val declare_entry_coercion : notation -> notation_entry_level -> unit
+type entry_coercion = (notation_with_optional_scope * notation) list
+val declare_entry_coercion : specific_notation -> notation_entry_level -> unit
val availability_of_entry_coercion : notation_entry_level -> notation_entry_level -> entry_coercion option
val declare_custom_entry_has_global : string -> int -> unit
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index dcc3a87b11..d6c6c365cb 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -199,11 +199,11 @@ GRAMMAR EXTEND Gram
collapse -(3) into the numeral -3. *)
(match c.CAst.v with
| CPrim (Numeral (SPlus,n)) ->
- CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"( _ )"),([c],[],[],[]))
+ CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"( _ )"),([c],[],[],[]))
| _ -> c) }
| "{|"; c = record_declaration; bar_cbrace -> { c }
| "{"; c = binder_constr ; "}" ->
- { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) }
+ { CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) }
| "`{"; c = operconstr LEVEL "200"; "}" ->
{ CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) }
| "`("; c = operconstr LEVEL "200"; ")" ->
@@ -380,7 +380,7 @@ GRAMMAR EXTEND Gram
collapse -(3) into the numeral -3. *)
match p.CAst.v with
| CPatPrim (Numeral (SPlus,n)) ->
- CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
+ CAst.make ~loc @@ CPatNotation(None,(InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
| _ -> p }
| "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" ->
{ CAst.make ~loc @@ CPatOr (p::pl) }
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 5c220abeda..915799e997 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -14,21 +14,23 @@ open Util
open Notation
open Notation_gram
-(* Uninterpreted notation levels *)
+(* Register the level of notation for parsing and printing
+ (we also register a precomputed parsing rule) *)
let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
-let declare_notation_level ?(onlyprint=false) ntn level =
+let declare_notation_level ntn ~onlyprint parsing_rule level =
try
- let (level,onlyprint) = NotationMap.find ntn !notation_level_map in
- if not onlyprint then anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
+ let _ = NotationMap.find ntn !notation_level_map in
+ anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
with Not_found ->
- notation_level_map := NotationMap.add ntn (level,onlyprint) !notation_level_map
+ notation_level_map := NotationMap.add ntn (onlyprint,parsing_rule,level) !notation_level_map
-let level_of_notation ?(onlyprint=false) ntn =
- let (level,onlyprint') = NotationMap.find ntn !notation_level_map in
- if onlyprint' && not onlyprint then raise Not_found;
- level
+let level_of_notation ntn =
+ NotationMap.find ntn !notation_level_map
+
+let get_defined_notations () =
+ NotationSet.elements @@ NotationMap.domain !notation_level_map
(**********************************************************************)
(* Equality *)
diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli
index c31f4505e7..d5711569f0 100644
--- a/parsing/notgram_ops.mli
+++ b/parsing/notgram_ops.mli
@@ -16,5 +16,9 @@ val level_eq : level -> level -> bool
(** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
-val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit
-val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *)
+val declare_notation_level : notation -> onlyprint:bool -> notation_grammar -> level -> unit
+val level_of_notation : notation -> bool (* = onlyprint *) * notation_grammar * level
+ (** raise [Not_found] if not declared *)
+
+(** Returns notations with defined parsing/printing rules *)
+val get_defined_notations : unit -> notation list
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index 7368f4109e..92f44faec8 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -47,31 +47,56 @@ type unparsing =
type unparsing_rule = unparsing list * precedence
type extra_unparsing_rules = (string * string) list
+
+let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with
+ | UnpMetaVar (n1,p1), UnpMetaVar (n2,p2) -> n1 = n2 && p1 = p2
+ | UnpBinderMetaVar (n1,p1), UnpBinderMetaVar (n2,p2) -> n1 = n2 && p1 = p2
+ | UnpListMetaVar (n1,p1,l1), UnpListMetaVar (n2,p2,l2) -> n1 = n2 && p1 = p2 && List.for_all2eq unparsing_eq l1 l2
+ | UnpBinderListMetaVar (n1,b1,l1), UnpBinderListMetaVar (n2,b2,l2) -> n1 = n2 && b1 = b2 && List.for_all2eq unparsing_eq l1 l2
+ | UnpTerminal s1, UnpTerminal s2 -> String.equal s1 s2
+ | UnpBox (b1,l1), UnpBox (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq (List.map snd l1) (List.map snd l2)
+ | UnpCut p1, UnpCut p2 -> p1 = p2
+ | (UnpMetaVar _ | UnpBinderMetaVar _ | UnpListMetaVar _ |
+ UnpBinderListMetaVar _ | UnpTerminal _ | UnpBox _ | UnpCut _), _ -> false
+
(* Concrete syntax for symbolic-extension table *)
-let notation_rules =
- Summary.ref ~name:"notation-rules" (NotationMap.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) NotationMap.t)
+let generic_notation_printing_rules =
+ Summary.ref ~name:"generic-notation-printing-rules" (NotationMap.empty : (unparsing_rule * bool * extra_unparsing_rules) NotationMap.t)
+
+let specific_notation_printing_rules =
+ Summary.ref ~name:"specific-notation-printing-rules" (SpecificNotationMap.empty : (unparsing_rule * extra_unparsing_rules) SpecificNotationMap.t)
+
+let declare_generic_notation_printing_rules ntn ~reserved ~extra unpl =
+ generic_notation_printing_rules := NotationMap.add ntn (unpl,reserved,extra) !generic_notation_printing_rules
+let declare_specific_notation_printing_rules specific_ntn ~extra unpl =
+ specific_notation_printing_rules := SpecificNotationMap.add specific_ntn (unpl,extra) !specific_notation_printing_rules
+
+let has_generic_notation_printing_rule ntn =
+ NotationMap.mem ntn !generic_notation_printing_rules
+
+let find_generic_notation_printing_rule ntn =
+ NotationMap.find ntn !generic_notation_printing_rules
-let declare_notation_rule ntn ~extra unpl gram =
- notation_rules := NotationMap.add ntn (unpl,extra,gram) !notation_rules
+let find_specific_notation_printing_rule specific_ntn =
+ SpecificNotationMap.find specific_ntn !specific_notation_printing_rules
-let find_notation_printing_rule ntn =
- try pi1 (NotationMap.find ntn !notation_rules)
- with Not_found -> anomaly (str "No printing rule found for " ++ pr_notation ntn ++ str ".")
-let find_notation_extra_printing_rules ntn =
- try pi2 (NotationMap.find ntn !notation_rules)
- with Not_found -> []
-let find_notation_parsing_rules ntn =
- try pi3 (NotationMap.find ntn !notation_rules)
- with Not_found -> anomaly (str "No parsing rule found for " ++ pr_notation ntn ++ str ".")
+let find_notation_printing_rule which ntn =
+ try match which with
+ | None -> raise Not_found (* Normally not the case *)
+ | Some which -> fst (find_specific_notation_printing_rule (which,ntn))
+ with Not_found -> pi1 (find_generic_notation_printing_rule ntn)
-let get_defined_notations () =
- NotationSet.elements @@ NotationMap.domain !notation_rules
+let find_notation_extra_printing_rules which ntn =
+ try match which with
+ | None -> raise Not_found
+ | Some which -> snd (find_specific_notation_printing_rule (which,ntn))
+ with Not_found -> pi3 (find_generic_notation_printing_rule ntn)
let add_notation_extra_printing_rule ntn k v =
try
- notation_rules :=
- let p, pp, gr = NotationMap.find ntn !notation_rules in
- NotationMap.add ntn (p, (k,v) :: pp, gr) !notation_rules
+ generic_notation_printing_rules :=
+ let p, b, pp = NotationMap.find ntn !generic_notation_printing_rules in
+ NotationMap.add ntn (p, b, (k,v) :: pp) !generic_notation_printing_rules
with Not_found ->
user_err ~hdr:"add_notation_extra_printing_rule"
(str "No such Notation.")
diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli
index be5af75e72..7996e7696d 100644
--- a/parsing/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -41,11 +41,14 @@ type unparsing =
type unparsing_rule = unparsing list * precedence
type extra_unparsing_rules = (string * string) list
-val declare_notation_rule : notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit
-val find_notation_printing_rule : notation -> unparsing_rule
-val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
-val find_notation_parsing_rules : notation -> notation_grammar
-val add_notation_extra_printing_rule : notation -> string -> string -> unit
-(** Returns notations with defined parsing/printing rules *)
-val get_defined_notations : unit -> notation list
+val unparsing_eq : unparsing -> unparsing -> bool
+
+val declare_generic_notation_printing_rules : notation -> reserved:bool -> extra:extra_unparsing_rules -> unparsing_rule -> unit
+val declare_specific_notation_printing_rules : specific_notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit
+val has_generic_notation_printing_rule : notation -> bool
+val find_generic_notation_printing_rule : notation -> unparsing_rule * bool * extra_unparsing_rules
+val find_specific_notation_printing_rule : specific_notation -> unparsing_rule * extra_unparsing_rules
+val find_notation_printing_rule : notation_with_optional_scope option -> notation -> unparsing_rule
+val find_notation_extra_printing_rules : notation_with_optional_scope option -> notation -> extra_unparsing_rules
+val add_notation_extra_printing_rule : notation -> string -> string -> unit
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index e45bae19ca..96f8cb12ba 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -857,7 +857,7 @@ let glob_cpattern gs p =
| k, (v, Some t), _ as orig ->
if k = 'x' then glob_ssrterm gs ('(', (v, Some t), None) else
match t.CAst.v with
- | CNotation((InConstrEntrySomeLevel,"( _ in _ )"), ([t1; t2], [], [], [])) ->
+ | CNotation(_,(InConstrEntrySomeLevel,"( _ in _ )"), ([t1; t2], [], [], [])) ->
(try match glob t1, glob t2 with
| (r1, None), (r2, None) -> encode k "In" [r1;r2]
| (r1, Some _), (r2, Some _) when isCVar t1 ->
@@ -865,11 +865,11 @@ let glob_cpattern gs p =
| (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2]
| _ -> CErrors.anomaly (str"where are we?.")
with _ when isCVar t1 -> encode k "In" [bind_in t1 t2])
- | CNotation((InConstrEntrySomeLevel,"( _ in _ in _ )"), ([t1; t2; t3], [], [], [])) ->
+ | CNotation(_,(InConstrEntrySomeLevel,"( _ in _ in _ )"), ([t1; t2; t3], [], [], [])) ->
check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3]
- | CNotation((InConstrEntrySomeLevel,"( _ as _ )"), ([t1; t2], [], [], [])) ->
+ | CNotation(_,(InConstrEntrySomeLevel,"( _ as _ )"), ([t1; t2], [], [], [])) ->
encode k "As" [fst (glob t1); fst (glob t2)]
- | CNotation((InConstrEntrySomeLevel,"( _ as _ in _ )"), ([t1; t2; t3], [], [], [])) ->
+ | CNotation(_,(InConstrEntrySomeLevel,"( _ as _ in _ )"), ([t1; t2; t3], [], [], [])) ->
check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3]
| _ -> glob_ssrterm gs orig
;;
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index f9f46e1ceb..2f60663c82 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -133,8 +133,8 @@ let tag_var = tag Tag.variable
in
aux unps
- let pr_notation pr pr_patt pr_binders s env =
- let unpl, level = find_notation_printing_rule s in
+ let pr_notation pr pr_patt pr_binders which s env =
+ let unpl, level = find_notation_printing_rule which s in
print_hunks level pr pr_patt pr_binders env unpl, level
let pr_delimiters key strm =
@@ -279,11 +279,11 @@ let tag_var = tag Tag.variable
let pp p = hov 0 (pr_patt mt (lpator,Any) p) in
surround (hov 0 (prlist_with_sep pr_spcbar pp pl)), lpator
- | CPatNotation ((_,"( _ )"),([p],[]),[]) ->
+ | CPatNotation (_,(_,"( _ )"),([p],[]),[]) ->
pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
- | CPatNotation (s,(l,ll),args) ->
- let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ -> mt ()) (fun _ _ _ -> mt()) s (l,ll,[],[]) in
+ | CPatNotation (which,s,(l,ll),args) ->
+ let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ -> mt ()) (fun _ _ _ -> mt()) which s (l,ll,[],[]) in
(if List.is_empty args||prec_less l_not (lapp,L) then strm_not else surround strm_not)
++ prlist (pr_patt spc (lapp,L)) args, if not (List.is_empty args) then lapp else l_not
@@ -650,10 +650,10 @@ let tag_var = tag Tag.variable
| CastCoerce -> str ":>"),
lcast
)
- | CNotation ((_,"( _ )"),([t],[],[],[])) ->
+ | CNotation (_,(_,"( _ )"),([t],[],[],[])) ->
return (pr (fun()->str"(") (max_int,L) t ++ str")", latom)
- | CNotation (s,env) ->
- pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) s env
+ | CNotation (which,s,env) ->
+ pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) which s env
| CGeneralization (bk,ak,c) ->
return (pr_generalization bk ak (pr mt ltop c), latom)
| CPrim p ->
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index d93dd15f91..c3ee5968dc 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -529,7 +529,7 @@ let match_goals ot nt =
constr_expr ogname a a2
| CastCoerce, CastCoerce -> ()
| _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (4)"))
- | CNotation (ntn,args), CNotation (ntn2,args2) ->
+ | CNotation (_,ntn,args), CNotation (_,ntn2,args2) ->
constr_notation_substitution ogname args args2
| CGeneralization (b,a,c), CGeneralization (b2,a2,c2) ->
constr_expr ogname c c2
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 1c8f237bb8..66b54b629f 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -77,3 +77,35 @@ Entry constr:expr is
[ "201" RIGHTA
[ "{"; constr:operconstr LEVEL "200"; "}" ] ]
+fun x : nat => [ x ]
+ : nat -> nat
+fun x : nat => [x]
+ : nat -> nat
+∀ x : nat, x = x
+ : Prop
+File "stdin", line 222, characters 0-160:
+Warning: Notation "∀ _ .. _ , _" was already defined with a different format
+in scope type_scope. [notation-incompatible-format,parsing]
+∀x : nat,x = x
+ : Prop
+File "stdin", line 235, characters 0-60:
+Warning: Notation "_ %%% _" was already defined with a different format.
+[notation-incompatible-format,parsing]
+File "stdin", line 239, characters 0-64:
+Warning: Notation "_ %%% _" was already defined with a different format.
+[notation-incompatible-format,parsing]
+File "stdin", line 244, characters 0-62:
+Warning: Lonely notation "_ %%%% _" was already defined with a different
+format. [notation-incompatible-format,parsing]
+3 %% 4
+ : nat
+3 %% 4
+ : nat
+3 %% 4
+ : nat
+File "stdin", line 272, characters 0-61:
+Warning: The format modifier is irrelevant for only parsing rules.
+[irrelevant-format-only-parsing,parsing]
+File "stdin", line 276, characters 0-63:
+Warning: The only parsing modifier has no effect in Reserved Notation.
+[irrelevant-reserved-notation-only-parsing,parsing]
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 4ab800c9ba..a6503a8bf3 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -195,3 +195,84 @@ Notation "{ p }" := (p) (in custom expr at level 201, p constr).
Print Custom Grammar expr.
End Bug11331.
+
+Module Bug_6082.
+
+Declare Scope foo.
+Notation "[ x ]" := (S x) (format "[ x ]") : foo.
+Open Scope foo.
+Check fun x => S x.
+
+Declare Scope bar.
+Notation "[ x ]" := (S x) (format "[ x ]") : bar.
+Open Scope bar.
+
+Check fun x => S x.
+
+End Bug_6082.
+
+Module Bug_7766.
+
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+ (at level 200, x binder, y binder, right associativity,
+ format "'[ ' ∀ x .. y ']' , P") : type_scope.
+
+Check forall (x : nat), x = x.
+
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+ (at level 200, x binder, y binder, right associativity,
+ format "∀ x .. y , P") : type_scope.
+
+Check forall (x : nat), x = x.
+
+End Bug_7766.
+
+Module N.
+
+(* Other tests about generic and specific formats *)
+
+Reserved Notation "x %%% y" (format "x %%% y", at level 35).
+Reserved Notation "x %%% y" (format "x %%% y", at level 35).
+
+(* Not using the reserved format, we warn *)
+
+Notation "x %%% y" := (x+y) (format "x %%% y", at level 35).
+
+(* Same scope (here lonely): we warn *)
+
+Notation "x %%%% y" := (x+y) (format "x %%%% y", at level 35).
+Notation "x %%%% y" := (x+y) (format "x %%%% y", at level 35).
+
+(* Test if the format for a specific notation becomes the default
+ generic format or if the generic format, in the absence of a
+ Reserved Notation, is the one canonically obtained from the
+ notation *)
+
+Declare Scope foo_scope.
+Declare Scope bar_scope.
+Declare Scope bar'_scope.
+Notation "x %% y" := (x+y) (at level 47, format "x %% y") : foo_scope.
+Open Scope foo_scope.
+Check 3 %% 4.
+
+(* No scope, we inherit the initial format *)
+
+Notation "x %% y" := (x*y) : bar_scope. (* Inherit the format *)
+Open Scope bar_scope.
+Check 3 %% 4.
+
+(* Different scope and no reserved notation, we don't warn *)
+
+Notation "x %% y" := (x*y) (at level 47, format "x %% y") : bar'_scope.
+Open Scope bar'_scope.
+Check 3 %% 4.
+
+(* Warn for combination of "only parsing" and "format" *)
+
+Notation "###" := 0 (at level 0, only parsing, format "###").
+
+(* In reserved notation, warn only for the "only parsing" *)
+
+Reserved Notation "##" (at level 0, only parsing, format "##").
+
+End N.
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 5e98f5ddc0..e8d0aee331 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -537,10 +537,10 @@ let rec pure_sublevels' assoc from forpat level = function
let make_act : type r. r target -> _ -> r gen_eval = function
| ForConstr -> fun notation loc env ->
let env = (env.constrs, env.constrlists, env.binders, env.binderlists) in
- CAst.make ~loc @@ CNotation (notation, env)
+ CAst.make ~loc @@ CNotation (None, notation, env)
| ForPattern -> fun notation loc env ->
let env = (env.constrs, env.constrlists) in
- CAst.make ~loc @@ CPatNotation (notation, env, [])
+ CAst.make ~loc @@ CPatNotation (None, notation, env, [])
let extend_constr state forpat ng =
let custom,n,_,_ = ng.notgram_level in
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index f2e1002f71..623baf7db7 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -776,43 +776,96 @@ let error_parsing_incompatible_level ntn ntn' oldprec prec =
spc() ++ str "while it is now required to be" ++ spc() ++
pr_level ntn prec ++ str ".")
-type syntax_extension = {
+let warn_incompatible_format =
+ CWarnings.create ~name:"notation-incompatible-format" ~category:"parsing"
+ (fun (specific,ntn) ->
+ let head,scope = match specific with
+ | None -> str "Notation", mt ()
+ | Some LastLonelyNotation -> str "Lonely notation", mt ()
+ | Some (NotationInScope sc) -> str "Notation", strbrk (" in scope " ^ sc) in
+ head ++ spc () ++ pr_notation ntn ++
+ strbrk " was already defined with a different format" ++ scope ++ str ".")
+
+type syntax_parsing_extension = {
synext_level : Notation_gram.level;
synext_notation : notation;
synext_notgram : notation_grammar;
- synext_unparsing : unparsing list;
+}
+
+type syntax_printing_extension = {
+ synext_reserved : bool;
+ synext_unparsing : unparsing_rule;
synext_extra : (string * string) list;
}
-type syntax_extension_obj = locality_flag * syntax_extension
+let generic_format_to_declare ntn {synext_unparsing = (rules,_); synext_extra = extra_rules } =
+ try
+ let (generic_rules,_),reserved,generic_extra_rules =
+ Ppextend.find_generic_notation_printing_rule ntn in
+ if reserved &&
+ (not (List.for_all2eq unparsing_eq rules generic_rules)
+ || extra_rules <> generic_extra_rules)
+ then
+ (warn_incompatible_format (None,ntn); true)
+ else
+ false
+ with Not_found -> true
+
+let check_reserved_format ntn = function
+ | None -> ()
+ | Some sy_pp_rules -> let _ = generic_format_to_declare ntn sy_pp_rules in ()
+
+let specific_format_to_declare (specific,ntn as specific_ntn)
+ {synext_unparsing = (rules,_); synext_extra = extra_rules } =
+ try
+ let (specific_rules,_),specific_extra_rules =
+ Ppextend.find_specific_notation_printing_rule specific_ntn in
+ if not (List.for_all2eq unparsing_eq rules specific_rules)
+ || extra_rules <> specific_extra_rules then
+ (warn_incompatible_format (Some specific,ntn); true)
+ else false
+ with Not_found -> true
+
+type syntax_extension_obj =
+ locality_flag * (syntax_parsing_extension * syntax_printing_extension option)
let check_and_extend_constr_grammar ntn rule =
try
let ntn_for_grammar = rule.notgram_notation in
if notation_eq ntn ntn_for_grammar then raise Not_found;
let prec = rule.notgram_level in
- let oldprec = Notgram_ops.level_of_notation ntn_for_grammar in
- if not (Notgram_ops.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
+ let oldonlyprint,_,oldprec = Notgram_ops.level_of_notation ntn_for_grammar in
+ if not (Notgram_ops.level_eq prec oldprec) && not oldonlyprint then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
+ if oldonlyprint then raise Not_found
with Not_found ->
Egramcoq.extend_constr_grammar rule
-let cache_one_syntax_extension se =
- let ntn = se.synext_notation in
- let prec = se.synext_level in
- let onlyprint = se.synext_notgram.notgram_onlyprinting in
- try
- let oldprec = Notgram_ops.level_of_notation ~onlyprint ntn in
- if not (Notgram_ops.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec;
- with Not_found ->
- begin
- (* Reserve the notation level *)
- Notgram_ops.declare_notation_level ntn prec ~onlyprint;
- (* Declare the parsing rule *)
- if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules;
- (* Declare the notation rule *)
- declare_notation_rule ntn
- ~extra:se.synext_extra (se.synext_unparsing, let (_,lev,_,_) = prec in lev) se.synext_notgram
- end
+let cache_one_syntax_extension (pa_se,pp_se) =
+ let ntn = pa_se.synext_notation in
+ let prec = pa_se.synext_level in
+ let onlyprint = pa_se.synext_notgram.notgram_onlyprinting in
+ (* Check and ensure that the level and the precomputed parsing rule is declared *)
+ let parsing_to_activate =
+ try
+ let oldonlyprint,_,oldprec = Notgram_ops.level_of_notation ntn in
+ if not (Notgram_ops.level_eq prec oldprec) && (not oldonlyprint || onlyprint) then error_incompatible_level ntn oldprec prec;
+ oldonlyprint && not onlyprint
+ with Not_found ->
+ (* Declare the level and the precomputed parsing rule *)
+ let _ = Notgram_ops.declare_notation_level ntn ~onlyprint pa_se.synext_notgram prec in
+ not onlyprint in
+ (* Declare the parsing rule *)
+ if parsing_to_activate then
+ List.iter (check_and_extend_constr_grammar ntn) pa_se.synext_notgram.notgram_rules;
+ (* Printing *)
+ match pp_se with
+ | None -> ()
+ | Some pp_se ->
+ (* Check compatibility of format in case of two Reserved Notation *)
+ (* and declare or redeclare printing rule *)
+ if generic_format_to_declare ntn pp_se then
+ declare_generic_notation_printing_rules ntn
+ ~extra:pp_se.synext_extra ~reserved:pp_se.synext_reserved pp_se.synext_unparsing
let cache_syntax_extension (_, (_, sy)) =
cache_one_syntax_extension sy
@@ -821,11 +874,11 @@ let subst_parsing_rule subst x = x
let subst_printing_rule subst x = x
-let subst_syntax_extension (subst, (local, sy)) =
- (local, { sy with
- synext_notgram = { sy.synext_notgram with notgram_rules = List.map (subst_parsing_rule subst) sy.synext_notgram.notgram_rules };
- synext_unparsing = subst_printing_rule subst sy.synext_unparsing;
- })
+let subst_syntax_extension (subst, (local, (pa_sy,pp_sy))) =
+ (local, ({ pa_sy with
+ synext_notgram = { pa_sy.synext_notgram with notgram_rules = List.map (subst_parsing_rule subst) pa_sy.synext_notgram.notgram_rules }},
+ Option.map (fun pp_sy -> {pp_sy with synext_unparsing = subst_printing_rule subst pp_sy.synext_unparsing}) pp_sy)
+ )
let classify_syntax_definition (local, _ as o) =
if local then Dispose else Substitute o
@@ -1351,6 +1404,7 @@ type notation_obj = {
notobj_onlyprint : bool;
notobj_deprecation : Deprecation.t option;
notobj_notation : notation * notation_location;
+ notobj_specific_pp_rules : syntax_printing_extension option;
}
let load_notation_common silently_define_scope_if_undefined _ (_, nobj) =
@@ -1372,22 +1426,31 @@ let open_notation i (_, nobj) =
let pat = nobj.notobj_interp in
let onlyprint = nobj.notobj_onlyprint in
let deprecation = nobj.notobj_deprecation in
+ let specific = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in
+ let specific_ntn = (specific,ntn) in
let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in
if Int.equal i 1 && fresh then begin
(* Declare the interpretation *)
let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in
(* Declare the uninterpretation *)
if not nobj.notobj_onlyparse then
- Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat;
+ Notation.declare_uninterpretation (NotationRule specific_ntn) pat;
(* Declare a possible coercion *)
(match nobj.notobj_coercion with
- | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion ntn entry
+ | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion specific_ntn entry
| Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n
| Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n
| Some (IsEntryNumeral (entry,n)) -> Notation.declare_custom_entry_has_numeral entry n
| Some (IsEntryString (entry,n)) -> Notation.declare_custom_entry_has_string entry n
| None -> ())
- end
+ end;
+ (* Declare specific format if any *)
+ match nobj.notobj_specific_pp_rules with
+ | Some pp_sy ->
+ if specific_format_to_declare specific_ntn pp_sy then
+ Ppextend.declare_specific_notation_printing_rules
+ specific_ntn ~extra:pp_sy.synext_extra pp_sy.synext_unparsing
+ | None -> ()
let cache_notation o =
load_notation_common false 1 o;
@@ -1428,22 +1491,27 @@ let with_syntax_protection f x =
exception NoSyntaxRule
let recover_notation_syntax ntn =
- try
- let prec = Notgram_ops.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in
- let pp_rule,_ = find_notation_printing_rule ntn in
- let pp_extra_rules = find_notation_extra_printing_rules ntn in
- let pa_rule = find_notation_parsing_rules ntn in
- { synext_level = prec;
- synext_notation = ntn;
- synext_notgram = pa_rule;
- synext_unparsing = pp_rule;
- synext_extra = pp_extra_rules;
- }
- with Not_found ->
- raise NoSyntaxRule
+ let pa =
+ try
+ let _,pa_rule,prec = Notgram_ops.level_of_notation ntn in
+ { synext_level = prec;
+ synext_notation = ntn;
+ synext_notgram = pa_rule }
+ with Not_found ->
+ raise NoSyntaxRule in
+ let pp =
+ try
+ let pp_rule,reserved,pp_extra_rules = find_generic_notation_printing_rule ntn in
+ Some {
+ synext_reserved = reserved;
+ synext_unparsing = pp_rule;
+ synext_extra = pp_extra_rules;
+ }
+ with Not_found -> None in
+ pa,pp
let recover_squash_syntax sy =
- let sq = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in
+ let sq,_ = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in
sy :: sq.synext_notgram.notgram_rules
(**********************************************************************)
@@ -1475,16 +1543,25 @@ let make_pp_rule level (typs,symbols) fmt =
| Some fmt ->
hunks_of_format (level, List.split typs) (symbols, parse_format fmt)
-(* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *)
-let make_syntax_rules (sd : SynData.syn_data) = let open SynData in
+let make_parsing_rules (sd : SynData.syn_data) = let open SynData in
let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in
- let custom,level,_,_ = sd.level in
- let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in
- let pp_rule = make_pp_rule level sd.pp_syntax_data sd.format in {
+ let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in {
synext_level = sd.level;
synext_notation = fst sd.info;
synext_notgram = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule };
- synext_unparsing = pp_rule;
+ }
+
+let warn_irrelevant_format =
+ CWarnings.create ~name:"irrelevant-format-only-parsing" ~category:"parsing"
+ (fun () -> str "The format modifier is irrelevant for only parsing rules.")
+
+let make_printing_rules reserved (sd : SynData.syn_data) = let open SynData in
+ let custom,level,_,_ = sd.level in
+ let pp_rule = make_pp_rule level sd.pp_syntax_data sd.format in
+ if sd.only_parsing then (if sd.format <> None then warn_irrelevant_format (); None)
+ else Some {
+ synext_reserved = reserved;
+ synext_unparsing = (pp_rule,level);
synext_extra = sd.extra;
}
@@ -1498,9 +1575,10 @@ let to_map l =
let add_notation_in_scope ~local deprecation df env c mods scope =
let open SynData in
let sd = compute_syntax_data ~local deprecation df mods in
- (* Prepare the interpretation *)
(* Prepare the parsing and printing rules *)
- let sy_rules = make_syntax_rules sd in
+ let sy_pa_rules = make_parsing_rules sd in
+ let sy_pp_rules = make_printing_rules false sd in
+ (* Prepare the interpretation *)
let i_vars = make_internalization_vars sd.recvars sd.mainvars sd.intern_typs in
let nenv = {
ninterp_var_type = to_map i_vars;
@@ -1520,24 +1598,29 @@ let add_notation_in_scope ~local deprecation df env c mods scope =
notobj_onlyprint = sd.only_printing;
notobj_deprecation = sd.deprecation;
notobj_notation = sd.info;
+ notobj_specific_pp_rules = sy_pp_rules;
} in
+ let gen_sy_pp_rules =
+ if Ppextend.has_generic_notation_printing_rule (fst sd.info) then None
+ else sy_pp_rules (* We use the format of this notation as the default *) in
+ let _ = check_reserved_format (fst sd.info) sy_pp_rules in
(* Ready to change the global state *)
List.iter (fun f -> f ()) sd.msgs;
- Lib.add_anonymous_leaf (inSyntaxExtension (local, sy_rules));
+ Lib.add_anonymous_leaf (inSyntaxExtension (local, (sy_pa_rules,gen_sy_pp_rules)));
Lib.add_anonymous_leaf (inNotation notation);
sd.info
let add_notation_interpretation_core ~local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint deprecation =
let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in
(* Recover types of variables and pa/pp rules; redeclare them if needed *)
- let level, i_typs, onlyprint = if not (is_numeral symbs) then begin
- let sy = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in
+ let level, i_typs, onlyprint, pp_sy = if not (is_numeral symbs) then begin
+ let (pa_sy,pp_sy as sy) = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in
let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in
(* If the only printing flag has been explicitly requested, put it back *)
- let onlyprint = onlyprint || sy.synext_notgram.notgram_onlyprinting in
- let _,_,_,typs = sy.synext_level in
- Some sy.synext_level, typs, onlyprint
- end else None, [], false in
+ let onlyprint = onlyprint || pa_sy.synext_notgram.notgram_onlyprinting in
+ let _,_,_,typs = pa_sy.synext_level in
+ Some pa_sy.synext_level, typs, onlyprint, pp_sy
+ end else None, [], false, None in
(* Declare interpretation *)
let path = (Lib.library_dp(), Lib.current_dirpath true) in
let df' = (make_notation_key InConstrEntrySomeLevel symbs, (path,df)) in
@@ -1560,6 +1643,7 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization
notobj_onlyprint = onlyprint;
notobj_deprecation = deprecation;
notobj_notation = df';
+ notobj_specific_pp_rules = pp_sy;
} in
Lib.add_anonymous_leaf (inNotation notation);
df'
@@ -1567,10 +1651,11 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization
(* Notations without interpretation (Reserved Notation) *)
let add_syntax_extension ~local ({CAst.loc;v=df},mods) = let open SynData in
- let psd = compute_pure_syntax_data ~local df mods in
- let sy_rules = make_syntax_rules {psd with deprecation = None} in
+ let psd = {(compute_pure_syntax_data ~local df mods) with deprecation = None} in
+ let pa_rules = make_parsing_rules psd in
+ let pp_rules = make_printing_rules true psd in
List.iter (fun f -> f ()) psd.msgs;
- Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
+ Lib.add_anonymous_leaf (inSyntaxExtension(local,(pa_rules,pp_rules)))
(* Notations with only interpretation *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:10:53 +0000