aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES4
-rw-r--r--interp/constrintern.ml75
-rw-r--r--interp/notation.ml13
-rw-r--r--interp/notation_ops.ml28
-rw-r--r--intf/extend.ml8
-rw-r--r--intf/notation_term.ml9
-rw-r--r--intf/vernacexpr.ml1
-rw-r--r--parsing/g_vernac.ml416
-rw-r--r--printing/ppvernac.ml15
-rw-r--r--test-suite/output/Notations3.out2
-rw-r--r--test-suite/output/Notations3.v2
-rw-r--r--test-suite/success/Notations2.v19
-rw-r--r--vernac/metasyntax.ml88
13 files changed, 203 insertions, 77 deletions
diff --git a/CHANGES b/CHANGES
index 74e120a31..32a533d14 100644
--- a/CHANGES
+++ b/CHANGES
@@ -12,7 +12,9 @@ Notations
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").
+ "fun 'pat =>" or "match p with pat => ... end"). Two variants are
+ available, depending on whether a single variable is considered as a
+ pattern or not.
- Recursive notations now support ".." patterns with several
occurrences of the recursive term or binder, possibly mixing terms
and binders, possibly in reverse left-to-right order.
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 379d09e89..158ac24b2 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -549,6 +549,18 @@ let is_var store pat =
| PatVar na -> store na; true
| _ -> false
+let out_var pat =
+ match pat.CAst.v with
+ | CPatAtom (Some (Ident (_,id))) -> Name id
+ | CPatAtom None -> Anonymous
+ | _ -> assert false
+
+let term_of_name = function
+ | Name id -> DAst.make (GVar id)
+ | Anonymous ->
+ let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
+ DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), Misctypes.IntroAnonymous, None))
+
let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function
| Anonymous -> (renaming,env), None, Anonymous
| Name id ->
@@ -564,13 +576,21 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
with Not_found ->
try
(* Trying to associate a pattern *)
- let pat,scopes = Id.Map.find id binders in
+ let pat,(onlyident,scopes) = Id.Map.find id binders in
let env = set_env_scopes env scopes in
- let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
- let pat, na = match disjpat with
- | [pat] when is_var store pat -> let na = get () in None, na
- | _ -> Some ((List.map snd ids,disjpat),id), snd na in
- (renaming,env), pat, na
+ if onlyident then
+ (* Do not try to interpret a variable as a constructor *)
+ let na = out_var pat in
+ let env = push_name_env ntnvars (Variable,[],[],[]) env (pat.CAst.loc, na) in
+ (renaming,env), None, na
+ else
+ (* Interpret as a pattern *)
+ let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
+ let pat, na =
+ match disjpat with
+ | [pat] when is_var store pat -> let na = get () in None, na
+ | _ -> Some ((List.map snd ids,disjpat),id), snd na in
+ (renaming,env), pat, na
with Not_found ->
(* Binders not bound in the notation do not capture variables *)
(* outside the notation (i.e. in the substitution) *)
@@ -688,12 +708,15 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
let gc = intern nenv c in
(gc, Some c)
in
- let mk_env' (c, (tmp_scope, subscopes)) =
+ let mk_env' (c, (onlyident,(tmp_scope,subscopes))) =
let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
- let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in
- match disjpat with
- | [pat] -> (glob_constr_of_cases_pattern pat, None)
- | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.CAst.loc ()
+ if onlyident then
+ let na = out_var c in term_of_name na, None
+ else
+ let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in
+ match disjpat with
+ | [pat] -> (glob_constr_of_cases_pattern pat, None)
+ | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.CAst.loc ()
in
let terms = Id.Map.map mk_env terms in
let binders = Id.Map.map mk_env' binders in
@@ -744,15 +767,18 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
scopes = subscopes @ env.scopes} a
with Not_found ->
try
- let pat,scopes = Id.Map.find id binders in
+ let pat,(onlyident,scopes) = Id.Map.find id binders in
let env = set_env_scopes env scopes in
(* We deactivate impls to avoid the check on hidden parameters *)
(* and since we are only interested in the pattern as a term *)
let env = reset_hidden_inductive_implicit_test env in
- let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
- match disjpat with
- | [pat] -> glob_constr_of_cases_pattern pat
- | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.")
+ if onlyident then
+ term_of_name (out_var pat)
+ else
+ let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
+ match disjpat with
+ | [pat] -> glob_constr_of_cases_pattern pat
+ | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.")
with Not_found ->
try
match binderopt with
@@ -774,6 +800,10 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
into a substitution for interpretation and based on binding/constr
distinction *)
+let cases_pattern_of_name (loc,na) =
+ let atom = match na with Name id -> Some (Ident (loc,id)) | Anonymous -> None in
+ CAst.make ?loc (CPatAtom atom)
+
let split_by_type ids subst =
let bind id scl l s =
match l with
@@ -785,12 +815,17 @@ let split_by_type ids subst =
| NtnTypeConstr ->
let terms,terms' = bind id scl terms terms' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
- | NtnTypeBinder NtnParsedAsConstr ->
+ | NtnTypeBinder NtnBinderParsedAsConstr (Extend.AsIdentOrPattern | Extend.AsStrictPattern) ->
+ let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
+ let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,(false,scl)) binders' in
+ (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
+ | NtnTypeBinder NtnBinderParsedAsConstr Extend.AsIdent ->
let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
- let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,scl) binders' in
+ let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
- | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern) ->
- let binders,binders' = bind id scl binders binders' in
+ | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ as x) ->
+ let onlyident = (x = NtnParsedAsIdent) in
+ let binders,binders' = bind id (onlyident,scl) binders binders' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
| NtnTypeConstrList ->
let termlists,termlists' = bind id scl termlists termlists' in
diff --git a/interp/notation.ml b/interp/notation.ml
index 13ff960f6..ea7ef21b1 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -97,9 +97,10 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with
| ETBigint, ETBigint -> true
| ETBinder b1, ETBinder b2 -> b1 == b2
| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2
-| ETPattern n1, ETPattern n2 -> Option.equal Int.equal n1 n2
+| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2
+| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
| ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2'
-| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _), _ -> false
+| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false
let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) =
let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
@@ -626,10 +627,10 @@ let availability_of_prim_token n printer_scope local_scopes =
let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
let notation_binder_source_eq s1 s2 = match s1, s2 with
- | NtnParsedAsConstr, NtnParsedAsConstr -> true
- | NtnParsedAsIdent, NtnParsedAsIdent -> true
- | NtnParsedAsPattern, NtnParsedAsPattern -> true
- | (NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern), _ -> false
+| NtnParsedAsIdent, NtnParsedAsIdent -> true
+| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2
+| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2
+| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false
let ntpe_eq t1 t2 = match t1, t2 with
| NtnTypeConstr, NtnTypeConstr -> true
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 44073c3b5..c65f4785e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -671,12 +671,20 @@ let is_term_meta id metas =
try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false
with Not_found -> false
+let is_onlybinding_strict_meta id metas =
+ try match Id.List.assoc id metas with _,NtnTypeBinder (NtnParsedAsPattern true) -> true | _ -> false
+ with Not_found -> false
+
let is_onlybinding_meta id metas =
try match Id.List.assoc id metas with _,NtnTypeBinder _ -> true | _ -> false
with Not_found -> false
-let is_onlybinding_pattern_like_meta id metas =
- try match Id.List.assoc id metas with _,NtnTypeBinder (NtnParsedAsConstr | NtnParsedAsPattern) -> true | _ -> false
+let is_onlybinding_pattern_like_meta isvar id metas =
+ try match Id.List.assoc id metas with
+ | _,NtnTypeBinder (NtnBinderParsedAsConstr
+ (Extend.AsIdentOrPattern | Extend.AsStrictPattern)) -> true
+ | _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar)
+ | _ -> false
with Not_found -> false
let is_bindinglist_meta id metas =
@@ -962,6 +970,8 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
| _ -> raise No_match
let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
+ | (na1,Name id2) when is_onlybinding_strict_meta id2 metas ->
+ raise No_match
| (na1,Name id2) when is_onlybinding_meta id2 metas ->
bind_binding_env alp sigma id2 [DAst.make (PatVar na1)]
| (Name id1,Name id2) when is_term_meta id2 metas ->
@@ -977,7 +987,9 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
let rec match_cases_pattern_binders allow_catchall metas (alp,sigma as acc) pat1 pat2 =
match DAst.get pat1, DAst.get pat2 with
- | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta id2 metas ->
+ | PatVar _, PatVar (Name id2) when is_onlybinding_pattern_like_meta true id2 metas ->
+ bind_binding_env alp sigma id2 [pat1]
+ | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta false id2 metas ->
bind_binding_env alp sigma id2 [pat1]
| PatVar na1, PatVar na2 -> match_names metas acc na1 na2
| _, PatVar Anonymous when allow_catchall -> acc
@@ -1093,7 +1105,9 @@ let rec match_ inner u alp metas sigma a1 a2 =
match DAst.get a1, a2 with
(* Matching notation variable *)
| r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 a1
- | r1, NVar id2 when is_onlybinding_pattern_like_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1
+ | GVar _, NVar id2 when is_onlybinding_pattern_like_meta true id2 metas -> bind_binding_as_term_env alp sigma id2 a1
+ | r1, NVar id2 when is_onlybinding_pattern_like_meta false id2 metas -> bind_binding_as_term_env alp sigma id2 a1
+ | GVar _, NVar id2 when is_onlybinding_strict_meta id2 metas -> raise No_match
| GVar _, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1
| r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 a1
@@ -1232,7 +1246,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
match_in u alp metas sigma b1 b2
| _ -> assert false)
| Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id
- when is_gvar p e && is_onlybinding_pattern_like_meta id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 ->
+ when is_gvar p e && is_onlybinding_pattern_like_meta false id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 ->
(match get () with
| [(_,(ids,disj_of_patl,b1))] ->
let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in
@@ -1276,13 +1290,13 @@ let match_notation_constr u c (metas,pat) =
| NtnTypeConstr ->
let term = try Id.List.assoc x terms with Not_found -> raise No_match in
((term, scl)::terms',termlists',binders',binderlists')
- | NtnTypeBinder NtnParsedAsConstr ->
+ | NtnTypeBinder (NtnBinderParsedAsConstr _) ->
(match Id.List.assoc x binders with
| [pat] ->
let v = glob_constr_of_cases_pattern pat in
((v,scl)::terms',termlists',binders',binderlists')
| _ -> raise No_match)
- | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern) ->
+ | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) ->
(terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists')
| NtnTypeConstrList ->
(terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists')
diff --git a/intf/extend.ml b/intf/extend.ml
index 813ed6dc6..78f0aa117 100644
--- a/intf/extend.ml
+++ b/intf/extend.ml
@@ -29,6 +29,11 @@ type production_level =
| NextLevel
| NumLevel of int
+type constr_as_binder_kind =
+ | AsIdent
+ | AsIdentOrPattern
+ | AsStrictPattern
+
(** User-level types used to tell how to parse or interpret of the non-terminal *)
type 'a constr_entry_key_gen =
@@ -37,7 +42,8 @@ type 'a constr_entry_key_gen =
| ETBigint
| ETBinder of bool (* open list of binders if true, closed list of binders otherwise *)
| ETConstr of 'a
- | ETPattern of int option
+ | ETConstrAsBinder of constr_as_binder_kind * 'a
+ | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *)
| ETOther of string * string
(** Entries level (left-hand side of grammar rules) *)
diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index 0f4bfef60..86f5adbd7 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -61,7 +61,14 @@ type subscopes = tmp_scope_name option * scope_name list
(** Type of the meta-variables of an notation_constr: in a recursive pattern x..y,
x carries the sequence of objects bound to the list x..y *)
-type notation_binder_source = NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern
+type notation_binder_source =
+ (* This accepts only pattern *)
+ (* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *)
+ | NtnParsedAsPattern of bool
+ (* This accepts only ident *)
+ | NtnParsedAsIdent
+ (* This accepts ident, or pattern, or both *)
+ | NtnBinderParsedAsConstr of Extend.constr_as_binder_kind
type notation_var_instance_type =
| NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 8e0fe54c5..0b5009e26 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -214,6 +214,7 @@ type proof_expr =
type syntax_modifier =
| SetItemLevel of string list * Extend.production_level
+ | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level
| SetLevel of int
| SetAssoc of Extend.gram_assoc
| SetEntryType of string * Extend.simple_constr_prod_entry_key
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 009c1c19a..cca1b2989 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1174,6 +1174,7 @@ GEXTEND Gram
| x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at";
lev = level -> SetItemLevel (x::l,lev)
| x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev)
+ | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,lev)
| x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ)
] ]
;
@@ -1181,9 +1182,20 @@ GEXTEND Gram
[ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference
| IDENT "bigint" -> ETBigint
| IDENT "binder" -> ETBinder true
- | IDENT "pattern" -> ETPattern None
- | IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (Some n)
+ | IDENT "constr"; n = OPT at_level; b = constr_as_binder_kind -> ETConstrAsBinder (b,n)
+ | IDENT "pattern" -> ETPattern (false,None)
+ | IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (false,Some n)
+ | IDENT "strict"; IDENT "pattern" -> ETPattern (true,None)
+ | IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (true,Some n)
| IDENT "closed"; IDENT "binder" -> ETBinder false
] ]
;
+ at_level:
+ [ [ "at"; n = level -> n ] ]
+ ;
+ constr_as_binder_kind:
+ [ [ "as"; IDENT "ident" -> AsIdent
+ | "as"; IDENT "pattern" -> AsIdentOrPattern
+ | "as"; IDENT "strict"; IDENT "pattern" -> AsStrictPattern ] ]
+ ;
END
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 42329d03a..2fc7843ed 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -97,13 +97,21 @@ open Decl_kinds
| NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
| NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
+ let pr_constr_as_binder_kind = function
+ | AsIdent -> keyword "as ident"
+ | AsIdentOrPattern -> keyword "as pattern"
+ | AsStrictPattern -> keyword "as strict pattern"
+
+ let pr_strict b = if b then str "strict " else mt ()
+
let pr_set_entry_type pr = function
| ETName -> str"ident"
| ETReference -> str"global"
- | ETPattern None -> str"pattern"
- | ETPattern (Some n) -> str"pattern" ++ spc () ++ pr_at_level (NumLevel n)
+ | ETPattern (b,None) -> pr_strict b ++ str"pattern"
+ | ETPattern (b,Some n) -> pr_strict b ++ str"pattern" ++ spc () ++ pr_at_level (NumLevel n)
| ETConstr lev -> str"constr" ++ pr lev
| ETOther (_,e) -> str e
+ | ETConstrAsBinder (bk,lev) -> pr lev ++ spc () ++ pr_constr_as_binder_kind bk
| ETBigint -> str "bigint"
| ETBinder true -> str "binder"
| ETBinder false -> str "closed binder"
@@ -373,6 +381,9 @@ open Decl_kinds
let pr_syntax_modifier = function
| SetItemLevel (l,n) ->
prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n
+ | SetItemLevelAsBinder (l,bk,n) ->
+ prlist_with_sep sep_v2 str l ++
+ spc() ++ pr_at_level n ++ spc() ++ pr_constr_as_binder_kind bk
| SetLevel n -> pr_at_level (NumLevel n)
| SetAssoc LeftA -> keyword "left associativity"
| SetAssoc RightA -> keyword "right associativity"
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 6d195b512..3fd4c1c31 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -194,8 +194,6 @@ 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}
- : Set
exists2' {{x, y}}, x = 0 & y = 0
: Prop
exists2 x : nat * nat,
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index b4ad4a7b3..9ea218481 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -341,8 +341,6 @@ Check fun x => if x is n.+1 then n else 1.
(* Examples with binding patterns *)
-Check {(x,y)|x+y=0}.
-
Module D.
Notation "'exists2'' x , p & q" := (ex2 (fun x => p) (fun x => q))
(at level 200, x pattern, p at level 200, right associativity,
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 08d904cea..7c2cf3ee5 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -98,12 +98,12 @@ Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200).
(* 11. Notations with needed factorization of a recursive pattern *)
(* See https://github.com/coq/coq/issues/6078#issuecomment-342287412 *)
-Module A.
+Module M11.
Notation "[:: x1 ; .. ; xn & s ]" := (cons x1 .. (cons xn s) ..).
Notation "[:: x1 ; .. ; xn ]" := (cons x1 .. (cons xn nil) ..).
Check [:: 1 ; 2 ; 3 ].
Check [:: 1 ; 2 ; 3 & nil ]. (* was failing *)
-End A.
+End M11.
(* 12. Preventively check that a variable which does not occur can be instantiated *)
(* by any term. In particular, it should not be restricted to a binder *)
@@ -111,3 +111,18 @@ Module M12.
Notation "N ++ x" := (S x) (only parsing).
Check 2 ++ 0.
End M12.
+
+(* 13. Check that internal data about associativity are not used in comparing levels *)
+Module M13.
+Notation "x ;; z" := (x + z)
+ (at level 100, z at level 200, only parsing, right associativity).
+Notation "x ;; z" := (x * z)
+ (at level 100, z at level 200, only parsing) : foo_scope.
+End M13.
+
+(* 14. Check that a notation with a "ident" binder does not include a pattern *)
+Module M14.
+Notation "'myexists' x , p" := (ex (fun x => p))
+ (at level 200, x ident, p at level 200, right associativity) : type_scope.
+Check myexists I, I = 0. (* Should not be seen as a constructor *)
+End M14.
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 44a7462de..524c9b32b 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -285,14 +285,17 @@ let prec_assoc = function
| LeftA -> (E,L)
| NonA -> (L,L)
-let precedence_of_entry_type from = function
- | ETConstr (NumLevel n,BorderProd (_,None)) -> n, Prec n
- | ETConstr (NumLevel n,BorderProd (b,Some a)) ->
+let precedence_of_position_and_level from = function
+ | NumLevel n, BorderProd (_,None) -> n, Prec n
+ | NumLevel n, BorderProd (b,Some a) ->
n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp
- | ETConstr (NumLevel n,InternalProd) -> n, Prec n
- | ETConstr (NextLevel,_) -> from, L
- | ETPattern n -> let n = match n with None -> 0 | Some n -> n in n, Prec n
- | _ -> 0, E (* ?? *)
+ | NumLevel n, InternalProd -> n, Prec n
+ | NextLevel, _ -> from, L
+
+let precedence_of_entry_type from = function
+ | ETConstr x | ETConstrAsBinder (_,x) -> precedence_of_position_and_level from x
+ | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in n, Prec n
+ | _ -> 0, E (* should not matter *)
(* Some breaking examples *)
(* "x = y" : "x /1 = y" (breaks before any symbol) *)
@@ -361,7 +364,7 @@ let unparsing_metavar i from typs =
let x = List.nth typs (i-1) in
let prec = snd (precedence_of_entry_type from x) in
match x with
- | ETConstr _ | ETReference | ETBigint ->
+ | ETConstr _ | ETConstrAsBinder _ | ETReference | ETBigint ->
UnpMetaVar (i,prec)
| ETPattern _ ->
UnpBinderMetaVar (i,prec)
@@ -596,7 +599,7 @@ let expand_list_rule typ tkl x n p ll =
let is_constr_typ typ x etyps =
match List.assoc x etyps with
- | ETConstr typ' -> typ = typ'
+ | ETConstr typ' | ETConstrAsBinder (_,typ') -> typ = typ'
| _ -> false
let include_possible_similar_trailing_pattern typ etyps sl l =
@@ -614,8 +617,8 @@ let prod_entry_type = function
| ETReference -> ETProdReference
| ETBigint -> ETProdBigint
| ETBinder _ -> assert false (* See check_binder_type *)
- | ETConstr p -> ETProdConstr p
- | ETPattern n -> ETProdPattern (match n with None -> 0 | Some n -> n)
+ | ETConstr p | ETConstrAsBinder (_,p) -> ETProdConstr p
+ | ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n)
| ETOther (s,t) -> ETProdOther (s,t)
let make_production etyps symbols =
@@ -659,6 +662,7 @@ let rec find_symbols c_current c_next c_last = function
let border = function
| (_,ETConstr(_,BorderProd (_,a))) :: _ -> a
+ | (_,(ETConstrAsBinder(_,(_,BorderProd (_,a))))) :: _ -> a
| _ -> None
let recompute_assoc typs =
@@ -679,7 +683,9 @@ let pr_arg_level from (lev,typ) =
| (n,Prec m) when Int.equal m n -> str "at level " ++ int n
| (n,_) -> str "Unknown level" in
Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++
- (match typ with ETConstr _ | ETPattern _ -> spc () ++ pplev lev | _ -> mt ())
+ (match typ with
+ | ETConstr _ | ETConstrAsBinder _ | ETPattern _ -> spc () ++ pplev lev
+ | _ -> mt ())
let pr_level ntn (from,args,typs) =
str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++
@@ -811,6 +817,8 @@ let interp_modifiers modl = let open NotationMods in
interp { acc with etyps = (id,typ) :: acc.etyps; } l
| SetItemLevel ([],n) :: l ->
interp acc l
+ | SetItemLevelAsBinder ([],_,_) :: l ->
+ interp acc l
| SetItemLevel (s::idl,n) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id acc.etyps then
@@ -818,8 +826,14 @@ let interp_modifiers modl = let open NotationMods in
(str s ++ str " is already assigned to an entry or constr level.");
let typ = ETConstr (Some n) in
interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevel (idl,n)::l)
+ | SetItemLevelAsBinder (s::idl,bk,n) :: l ->
+ let id = Id.of_string s in
+ if Id.List.mem_assoc id acc.etyps then
+ user_err ~hdr:"Metasyntax.interp_modifiers"
+ (str s ++ str " is already assigned to an entry or constr level.");
+ let typ = ETConstrAsBinder (bk,Some n) in
+ interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevelAsBinder (idl,bk,n)::l)
| SetLevel n :: l ->
-
interp { acc with level = Some n; } l
| SetAssoc a :: l ->
if not (Option.is_empty acc.assoc) then user_err Pp.(str "An associativity is given more than once.");
@@ -886,9 +900,14 @@ let set_entry_type etyps (x,typ) =
| ETConstr (Some n), (_,BorderProd (left,_)) ->
ETConstr (n,BorderProd (left,None))
| ETConstr (Some n), (_,InternalProd) -> ETConstr (n,InternalProd)
- | (ETPattern _ | ETName | ETBigint | ETOther _ |
- ETReference | ETBinder _ as t), _ -> t
+ | ETConstrAsBinder (bk, Some n), (_,BorderProd (left,_)) ->
+ ETConstrAsBinder (bk, (n,BorderProd (left,None)))
+ | ETConstrAsBinder (bk, Some n), (_,InternalProd) ->
+ ETConstrAsBinder (bk, (n,InternalProd))
+ | ETPattern (b,n), _ -> ETPattern (b,n)
+ | (ETName | ETBigint | ETReference | ETBinder _ | ETOther _ as x), _ -> x
| ETConstr None, _ -> ETConstr typ
+ | ETConstrAsBinder (bk,None), _ -> ETConstrAsBinder (bk,typ)
with Not_found -> ETConstr typ
in (x,typ)
@@ -909,7 +928,7 @@ let join_auxiliary_recursive_types recvars etyps =
let internalization_type_of_entry_type = function
| ETBinder _ -> NtnInternTypeOnlyBinder
- | ETConstr _ | ETBigint | ETReference
+ | ETConstr _ | ETConstrAsBinder _ | ETBigint | ETReference
| ETName | ETPattern _ | ETOther _ -> NtnInternTypeAny
let set_internalization_type typs =
@@ -923,10 +942,13 @@ let make_internalization_vars recvars mainvars typs =
let make_interpretation_type isrec isonlybinding = function
| ETConstr _ ->
if isrec then NtnTypeConstrList else
- if isonlybinding then NtnTypeBinder NtnParsedAsConstr (* Parsed as constr, but interpreted as binder *)
+ if isonlybinding then
+ (* Parsed as constr, but interpreted as a binder: default is to parse it as an ident only *)
+ NtnTypeBinder (NtnBinderParsedAsConstr AsIdent)
else NtnTypeConstr
+ | ETConstrAsBinder (bk,_) -> NtnTypeBinder (NtnBinderParsedAsConstr bk)
| ETName -> NtnTypeBinder NtnParsedAsIdent
- | ETPattern _ -> NtnTypeBinder NtnParsedAsPattern (* Parsed as ident/pattern, primarily interpreted as binder *)
+ | ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *)
| ETBigint | ETReference | ETOther _ -> NtnTypeConstr
| ETBinder _ ->
if isrec then NtnTypeBinderList
@@ -982,6 +1004,7 @@ let is_not_printable onlyparse reversibility = function
(warn_non_reversible_notation reversibility; true)
else onlyparse
+
let find_precedence lev etyps symbols onlyprint =
let first_symbol =
let rec aux = function
@@ -999,27 +1022,30 @@ let find_precedence lev etyps symbols onlyprint =
match first_symbol with
| None -> [],0
| Some (NonTerminal x) ->
+ let test () =
+ if onlyprint then
+ if Option.is_empty lev then
+ user_err Pp.(str "Explicit level needed in only-printing mode when the level of the leftmost non-terminal is given.")
+ else [],Option.get lev
+ else
+ user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in
(try match List.assoc x etyps with
- | ETConstr _ ->
- if onlyprint then
- if Option.is_empty lev then
- user_err Pp.(str "Explicit level needed in only-printing mode when the level of the leftmost non-terminal is given.")
- else [],Option.get lev
- else
- user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.")
- | ETName | ETBigint | ETReference ->
+ | ETConstr _ -> test ()
+ | ETConstrAsBinder (_,Some _) -> test ()
+ | (ETName | ETBigint | ETReference) ->
begin match lev with
| None ->
([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0)
| Some 0 ->
([],0)
| _ ->
- user_err Pp.(str "A notation starting with an atomic expression must be at level 0.")
+ user_err Pp.(str "A notation starting with an atomic expression must be at level 0.")
end
- | ETPattern _ | ETBinder _ | ETOther _ -> (* Give a default ? *)
- if Option.is_empty lev then
- user_err Pp.(str "Need an explicit level.")
- else [],Option.get lev
+ | (ETPattern _ | ETBinder _ | ETOther _ | ETConstrAsBinder _) ->
+ (* Give a default ? *)
+ if Option.is_empty lev then
+ user_err Pp.(str "Need an explicit level.")
+ else [],Option.get lev
with Not_found ->
if Option.is_empty lev then
user_err Pp.(str "A left-recursive notation must have an explicit level.")
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 07:44:39 +0000