aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/03-notations/13265-master+allow-single-binder-entry.rst6
-rw-r--r--doc/sphinx/user-extensions/syntax-extensions.rst24
-rw-r--r--interp/constrexpr.ml6
-rw-r--r--interp/constrexpr_ops.ml107
-rw-r--r--interp/constrextern.ml12
-rw-r--r--interp/constrintern.ml130
-rw-r--r--interp/notation.ml3
-rw-r--r--interp/notation_ops.ml76
-rw-r--r--interp/notation_ops.mli2
-rw-r--r--interp/notation_term.ml6
-rw-r--r--parsing/extend.ml1
-rw-r--r--parsing/extend.mli1
-rw-r--r--parsing/g_constr.mlg28
-rw-r--r--parsing/pcoq.ml2
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--parsing/ppextend.ml6
-rw-r--r--parsing/ppextend.mli4
-rw-r--r--plugins/ssrsearch/g_search.mlg2
-rw-r--r--printing/ppconstr.ml69
-rw-r--r--printing/proof_diffs.ml3
-rw-r--r--test-suite/output/Notations4.out12
-rw-r--r--test-suite/output/Notations4.v18
-rw-r--r--vernac/egramcoq.ml11
-rw-r--r--vernac/metasyntax.ml24
24 files changed, 362 insertions, 193 deletions
diff --git a/doc/changelog/03-notations/13265-master+allow-single-binder-entry.rst b/doc/changelog/03-notations/13265-master+allow-single-binder-entry.rst
new file mode 100644
index 0000000000..c973e157dd
--- /dev/null
+++ b/doc/changelog/03-notations/13265-master+allow-single-binder-entry.rst
@@ -0,0 +1,6 @@
+- **Added:**
+ The :n:`@binder` entry of :cmd:`Notation` can now be used in
+ notations expecting a single (non-recursive) binder
+ (`#13265 <https://github.com/coq/coq/pull/13265>`_,
+ by Hugo Herbelin, see section :n:`notations-and-binders` of the
+ reference manual).
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 16c8586a9f..5cbd2e400e 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -709,6 +709,30 @@ Note also that in the absence of a ``as ident``, ``as strict pattern`` or
``as pattern`` :n:`@syntax_modifier`\s, the default is to consider sub-expressions occurring
in binding position and parsed as terms to be ``as ident``.
+Binders bound in the notation and parsed as general binders
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+
+It is also possible to rely on Coq's syntax of binders using the
+`binder` modifier as follows:
+
+.. coqtop:: in
+
+ Notation "'myforall' p , [ P , Q ] " := (forall p, P -> Q)
+ (at level 200, p binder).
+
+In this case, all of :n:`@ident`, :n:`{@ident}`, :n:`[@ident]`, :n:`@ident:@type`,
+:n:`{@ident:@type}`, :n:`[@ident:@type]`, :n:`'@pattern` can be used in place of
+the corresponding notation variable. In particular, the binder can
+declare implicit arguments:
+
+.. coqtop:: all
+
+ Check fun (f : myforall {a}, [a=0, Prop]) => f eq_refl.
+ Check myforall '((x,y):nat*nat), [ x = y, True ].
+
+By using instead `closed binder`, the same list of binders is allowed
+except that :n:`@ident:@type` requires parentheses around.
+
.. _NotationsWithBinders:
Binders not bound in the notation
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 977cbbccf2..b3f06faa1c 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -83,6 +83,8 @@ type cases_pattern_expr_r =
| CPatCast of cases_pattern_expr * constr_expr
and cases_pattern_expr = cases_pattern_expr_r CAst.t
+and kinded_cases_pattern_expr = cases_pattern_expr * Glob_term.binding_kind
+
and cases_pattern_notation_substitution =
cases_pattern_expr list * (* for constr subterms *)
cases_pattern_expr list list (* for recursive notations *)
@@ -145,12 +147,12 @@ and recursion_order_expr = recursion_order_expr_r CAst.t
and local_binder_expr =
| CLocalAssum of lname list * binder_kind * constr_expr
| CLocalDef of lname * constr_expr * constr_expr option
- | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t
+ | CLocalPattern of cases_pattern_expr
and constr_notation_substitution =
constr_expr list * (* for constr subterms *)
constr_expr list list * (* for recursive notations *)
- cases_pattern_expr list * (* for binders *)
+ kinded_cases_pattern_expr list * (* for binders *)
local_binder_expr list list (* for binder lists (recursive notations) *)
type constr_pattern_expr = constr_expr
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index efc2a35b65..a60dc11b57 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -94,6 +94,9 @@ and cases_pattern_notation_substitution_eq (s1, n1) (s2, n2) =
List.equal cases_pattern_expr_eq s1 s2 &&
List.equal (List.equal cases_pattern_expr_eq) n1 n2
+let kinded_cases_pattern_expr_eq (p1,bk1) (p2,bk2) =
+ cases_pattern_expr_eq p1 p2 && Glob_ops.binding_kind_eq bk1 bk2
+
let eq_universes u1 u2 =
match u1, u2 with
| None, None -> true
@@ -231,7 +234,7 @@ and local_binder_eq l1 l2 = match l1, l2 with
and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) =
List.equal constr_expr_eq e1 e2 &&
List.equal (List.equal constr_expr_eq) el1 el2 &&
- List.equal cases_pattern_expr_eq b1 b2 &&
+ List.equal kinded_cases_pattern_expr_eq b1 b2 &&
List.equal (List.equal local_binder_eq) bl1 bl2
and instance_eq (x1,c1) (x2,c2) =
@@ -268,39 +271,37 @@ let is_constructor id =
(Nametab.locate_extended (qualid_of_ident id)))
with Not_found -> false
-let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with
+let rec cases_pattern_fold_names f h nacc pt = match CAst.(pt.v) with
| CPatRecord l ->
- List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l
- | CPatAlias (pat,{CAst.v=na}) -> Name.fold_right f na (cases_pattern_fold_names f a pat)
+ List.fold_left (fun nacc (r, cp) -> cases_pattern_fold_names f h nacc cp) nacc l
+ | CPatAlias (pat,{CAst.v=na}) -> Name.fold_right (fun na (n,acc) -> (f na n,acc)) na (cases_pattern_fold_names f h nacc pat)
| CPatOr (patl) ->
- List.fold_left (cases_pattern_fold_names f) a patl
+ List.fold_left (cases_pattern_fold_names f h) nacc patl
| 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
+ List.fold_left (cases_pattern_fold_names f h)
+ (Option.fold_left (List.fold_left (cases_pattern_fold_names f h)) nacc patl1) patl2
| 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
+ List.fold_left (cases_pattern_fold_names f h)
+ (List.fold_left (cases_pattern_fold_names f h) nacc (patl@List.flatten patll)) patl'
+ | CPatDelimiters (_,pat) -> cases_pattern_fold_names f h nacc pat
| CPatAtom (Some qid)
when qualid_is_ident qid && not (is_constructor @@ qualid_basename qid) ->
- f (qualid_basename qid) a
- | CPatPrim _ | CPatAtom _ -> a
- | CPatCast ({CAst.loc},_) ->
- CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names"
- (Pp.strbrk "Casts are not supported here.")
-
-let ids_of_pattern =
- cases_pattern_fold_names Id.Set.add Id.Set.empty
-
-let ids_of_pattern_list =
- List.fold_left
- (List.fold_left (cases_pattern_fold_names Id.Set.add))
- Id.Set.empty
+ let (n, acc) = nacc in
+ (f (qualid_basename qid) n, acc)
+ | CPatPrim _ | CPatAtom _ -> nacc
+ | CPatCast (p,t) ->
+ let (n, acc) = nacc in
+ cases_pattern_fold_names f h (n, h acc t) p
+
+let ids_of_pattern_list p =
+ fst (List.fold_left
+ (List.fold_left (cases_pattern_fold_names Id.Set.add (fun () _ -> ())))
+ (Id.Set.empty,()) p)
let ids_of_cases_tomatch tms =
List.fold_right
(fun (_, ona, indnal) l ->
- Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t)
+ Option.fold_right (fun t ids -> fst (cases_pattern_fold_names Id.Set.add (fun () _ -> ()) (ids,()) t))
indnal
(Option.fold_right (CAst.with_val (Name.fold_right Id.Set.add)) ona l))
tms Id.Set.empty
@@ -312,9 +313,9 @@ let rec fold_local_binders g f n acc b = let open CAst in function
f n (fold_local_binders g f n' acc b l) t
| CLocalDef ( { v = na },c,t)::l ->
Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t
- | CLocalPattern { v = pat,t }::l ->
- let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in
- Option.fold_left (f n) acc t
+ | CLocalPattern pat :: l ->
+ let n, acc = cases_pattern_fold_names g (f n) (n,acc) pat in
+ fold_local_binders g f n acc b l
| [] ->
f n acc b
@@ -378,10 +379,42 @@ let names_of_constr_expr c =
let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c)
+let rec fold_map_cases_pattern f h acc (CAst.{v=pt;loc} as p) = match pt with
+ | CPatRecord l ->
+ let acc, l = List.fold_left_map (fun acc (r, cp) -> let acc, cp = fold_map_cases_pattern f h acc cp in acc, (r, cp)) acc l in
+ acc, CAst.make ?loc (CPatRecord l)
+ | CPatAlias (pat,({CAst.v=na} as lna)) ->
+ let acc, p = fold_map_cases_pattern f h acc pat in
+ let acc = Name.fold_right f na acc in
+ acc, CAst.make ?loc (CPatAlias (pat,lna))
+ | CPatOr patl ->
+ let acc, patl = List.fold_left_map (fold_map_cases_pattern f h) acc patl in
+ acc, CAst.make ?loc (CPatOr patl)
+ | CPatCstr (c,patl1,patl2) ->
+ let acc, patl1 = Option.fold_left_map (List.fold_left_map (fold_map_cases_pattern f h)) acc patl1 in
+ let acc, patl2 = List.fold_left_map (fold_map_cases_pattern f h) acc patl2 in
+ acc, CAst.make ?loc (CPatCstr (c,patl1,patl2))
+ | CPatNotation (sc,ntn,(patl,patll),patl') ->
+ let acc, patl = List.fold_left_map (fold_map_cases_pattern f h) acc patl in
+ let acc, patll = List.fold_left_map (List.fold_left_map (fold_map_cases_pattern f h)) acc patll in
+ let acc, patl' = List.fold_left_map (fold_map_cases_pattern f h) acc patl' in
+ acc, CAst.make ?loc (CPatNotation (sc,ntn,(patl,patll),patl'))
+ | CPatDelimiters (d,pat) ->
+ let acc, p = fold_map_cases_pattern f h acc pat in
+ acc, CAst.make ?loc (CPatDelimiters (d,pat))
+ | CPatAtom (Some qid)
+ when qualid_is_ident qid && not (is_constructor @@ qualid_basename qid) ->
+ f (qualid_basename qid) acc, p
+ | CPatPrim _ | CPatAtom _ -> (acc,p)
+ | CPatCast (pat,t) ->
+ let acc, pat = fold_map_cases_pattern f h acc pat in
+ let t = h acc t in
+ acc, CAst.make ?loc (CPatCast (pat,t))
+
(* Used in correctness and interface *)
let map_binder g e nal = List.fold_right (CAst.with_val (Name.fold_right g)) nal e
-let map_local_binders f g e bl =
+let fold_map_local_binders f g e bl =
(* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
let open CAst in
let h (e,bl) = function
@@ -389,9 +422,9 @@ let map_local_binders f g e bl =
(map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl)
| CLocalDef( { loc ; v = na } as cna ,c,ty) ->
(Name.fold_right g na e, CLocalDef(cna,f e c,Option.map (f e) ty)::bl)
- | CLocalPattern { loc; v = pat,t } ->
- let ids = ids_of_pattern pat in
- (Id.Set.fold g ids e, CLocalPattern (make ?loc (pat,Option.map (f e) t))::bl) in
+ | CLocalPattern pat ->
+ let e, pat = fold_map_cases_pattern g f e pat in
+ (e, CLocalPattern pat::bl) in
let (e,rbl) = List.fold_left h (e,[]) bl in
(e, List.rev rbl)
@@ -400,16 +433,16 @@ let map_constr_expr_with_binders g f e = CAst.map (function
| CApp ((p,a),l) ->
CApp ((p,f e a),List.map (fun (a,i) -> (f e a,i)) l)
| CProdN (bl,b) ->
- let (e,bl) = map_local_binders f g e bl in CProdN (bl,f e b)
+ let (e,bl) = fold_map_local_binders f g e bl in CProdN (bl,f e b)
| CLambdaN (bl,b) ->
- let (e,bl) = map_local_binders f g e bl in CLambdaN (bl,f e b)
+ let (e,bl) = fold_map_local_binders f g e bl in CLambdaN (bl,f e b)
| 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 (inscope,n,(l,ll,bl,bll)) ->
(* This is an approximation because we don't know what binds what *)
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))
+ List.map (fun bl -> snd (fold_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)
| CHole _ | CEvar _ | CPatVar _ | CSort _
@@ -431,7 +464,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function
CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2)
| CFix (id,dl) ->
CFix (id,List.map (fun (id,n,bl,t,d) ->
- let (e',bl') = map_local_binders f g e bl in
+ let (e',bl') = fold_map_local_binders f g e bl in
let t' = f e' t in
(* Note: fix names should be inserted before the arguments... *)
let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_,_) -> g id e) e' dl in
@@ -439,7 +472,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function
(id,n,bl',t',d')) dl)
| CCoFix (id,dl) ->
CCoFix (id,List.map (fun (id,bl,t,d) ->
- let (e',bl') = map_local_binders f g e bl in
+ let (e',bl') = fold_map_local_binders f g e bl in
let t' = f e' t in
let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_) -> g id e) e' dl in
let d' = f e'' d in
@@ -472,7 +505,7 @@ let locs_of_notation ?loc locs ntn =
let ntn_loc ?loc (args,argslist,binders,binderslist) =
locs_of_notation ?loc
(List.map constr_loc (args@List.flatten argslist)@
- List.map cases_pattern_expr_loc binders@
+ List.map (fun (x,_) -> cases_pattern_expr_loc x) binders@
List.map local_binders_loc binderslist)
let patntn_loc ?loc (args,argslist) =
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8d3cf7274a..cf88036f73 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1126,7 +1126,7 @@ and factorize_prod ?impargs scopes vars na bk t c =
let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in
let b = extern_typ scopes vars b in
let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in
- let binder = CLocalPattern (make ?loc:c.loc (p,None)) in
+ let binder = CLocalPattern p in
(match b.v with
| CProdN (bl,b) -> CProdN (binder::bl,b)
| _ -> CProdN ([binder],b))
@@ -1167,7 +1167,7 @@ and factorize_lambda inctx scopes vars na bk t c =
let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in
let b = sub_extern inctx scopes vars b in
let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in
- let binder = CLocalPattern (make ?loc:c.loc (p,None)) in
+ let binder = CLocalPattern p in
(match b.v with
| CLambdaN (bl,b) -> CLambdaN (binder::bl,b)
| _ -> CLambdaN ([binder],b))
@@ -1219,7 +1219,10 @@ and extern_local_binder scopes vars = function
if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
let p = mkCPatOr (List.map (extern_cases_pattern vars) p) in
let (assums,ids,l) = extern_local_binder scopes vars l in
- (assums,ids, CLocalPattern(CAst.make @@ (p,ty)) :: l)
+ let p = match ty with
+ | None -> p
+ | Some ty -> CAst.make @@ (CPatCast (p,ty)) in
+ (assums,ids, CLocalPattern p :: l)
and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} =
let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in
@@ -1303,7 +1306,8 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
termlists in
let bl =
List.map (fun ((vars,bl),(subentry,(scopt,scl))) ->
- mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl))
+ (mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl)),
+ Explicit)
binders in
let bll =
List.map (fun ((vars,bl),(subentry,(scopt,scl))) ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c7ed066f7e..8bd77abc4a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -298,21 +298,20 @@ let error_expect_binder_notation_type ?loc id =
let set_var_scope ?loc id istermvar (tmp_scope,subscopes as scopes) ntnvars =
try
let used_as_binder,idscopes,typ = Id.Map.find id ntnvars in
- if not istermvar then used_as_binder := true;
- let () = if istermvar then
+ if istermvar then begin
(* scopes have no effect on the interpretation of identifiers *)
- begin match !idscopes with
+ (match !idscopes with
| None -> idscopes := Some scopes
| Some (tmp_scope', subscopes') ->
let s' = make_current_scope tmp_scope' subscopes' in
let s = make_current_scope tmp_scope subscopes in
- if not (List.equal String.equal s' s) then error_inconsistent_scope ?loc id s' s
+ if not (List.equal String.equal s' s) then error_inconsistent_scope ?loc id s' s);
+ (match typ with
+ | Notation_term.NtnInternTypeOnlyBinder -> error_expect_binder_notation_type ?loc id
+ | Notation_term.NtnInternTypeAny -> ())
end
- in
- match typ with
- | Notation_term.NtnInternTypeOnlyBinder ->
- if istermvar then error_expect_binder_notation_type ?loc id
- | Notation_term.NtnInternTypeAny -> ()
+ else
+ used_as_binder := true
with Not_found ->
(* Not in a notation *)
()
@@ -587,7 +586,10 @@ let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) =
(push_name_env ntnvars impls env locna,
(na,Explicit,term,ty))
-let intern_cases_pattern_as_binder ?loc test_kind ntnvars env p =
+let intern_cases_pattern_as_binder intern test_kind ntnvars env bk (CAst.{v=p;loc} as pv) =
+ let p,t = match p with
+ | CPatCast (p, t) -> (p, Some t)
+ | _ -> (pv, None) in
let il,disjpat =
let (il, subst_disjpat) = !intern_cases_pattern_fwd test_kind ntnvars (env_for_pattern (reset_tmp_scope env)) p in
let substl,disjpat = List.split subst_disjpat in
@@ -595,12 +597,17 @@ let intern_cases_pattern_as_binder ?loc test_kind ntnvars env p =
user_err ?loc (str "Unsupported nested \"as\" clause.");
il,disjpat
in
- let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars [] env (make ?loc @@ Name id)) il env in
let na = alias_of_pat (List.hd disjpat) in
+ let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars [] env (make ?loc @@ Name id)) il env in
let ienv = Name.fold_right Id.Set.remove na env.ids in
let id = Namegen.next_name_away_with_default "pat" na ienv in
let na = make ?loc @@ Name id in
- env,((disjpat,il),id),na
+ let t = match t with
+ | Some t -> t
+ | None -> CAst.make ?loc @@ CHole(Some (Evar_kinds.BinderType na.v),IntroAnonymous,None) in
+ let _, bl' = intern_assumption intern ntnvars env [na] (Default bk) t in
+ let {v=(_,bk,t)} = List.hd bl' in
+ env,((disjpat,il),id),na,bk,t
let intern_local_binder_aux intern ntnvars (env,bl) = function
| CLocalAssum(nal,bk,ty) ->
@@ -610,17 +617,9 @@ let intern_local_binder_aux intern ntnvars (env,bl) = function
| CLocalDef( {loc; v=na} as locna,def,ty) ->
let env,(na,bk,def,ty) = intern_letin_binder intern ntnvars env (locna,def,ty) in
env, (DAst.make ?loc @@ GLocalDef (na,bk,def,ty)) :: bl
- | CLocalPattern {loc;v=(p,ty)} ->
- let tyc =
- match ty with
- | Some ty -> ty
- | None -> CAst.make ?loc @@ CHole(None,IntroAnonymous,None)
- in
- let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc test_kind_tolerant ntnvars env p in
- let bk = Default Explicit in
- let _, bl' = intern_assumption intern ntnvars env [na] bk tyc in
- let {v=(_,bk,t)} = List.hd bl' in
- (env, (DAst.make ?loc @@ GLocalPattern((disjpat,List.map (fun x -> x.v) il),id,bk,t)) :: bl)
+ | CLocalPattern p ->
+ let env, ((disjpat,il),id),na,bk,t = intern_cases_pattern_as_binder intern test_kind_tolerant ntnvars env Explicit p in
+ (env, (DAst.make ?loc:p.CAst.loc @@ GLocalPattern((disjpat,List.map (fun x -> x.v) il),id,bk,t)) :: bl)
let intern_generalization intern env ntnvars loc bk ak c =
let c = intern {env with unb = true} c in
@@ -706,7 +705,7 @@ let is_patvar c =
let is_patvar_store store pat =
match DAst.get pat with
- | PatVar na -> ignore(store na); true
+ | PatVar na -> ignore(store (CAst.make ?loc:pat.loc na)); true
| _ -> false
let out_patvar = CAst.map_with_loc (fun ?loc -> function
@@ -715,37 +714,57 @@ let out_patvar = CAst.map_with_loc (fun ?loc -> function
| CPatAtom None -> Anonymous
| _ -> assert false)
-let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function
- | Anonymous -> (renaming,env), None, Anonymous
+let canonize_type = function
+ | None -> None
+ | Some t as t' ->
+ match DAst.get t with
+ | GHole (Evar_kinds.BinderType _,IntroAnonymous,None) -> None
+ | _ -> t'
+
+let set_type ty1 ty2 =
+ match canonize_type ty1, canonize_type ty2 with
+ (* Not a meta-binding binder, we use the type given in the notation *)
+ | _, None -> ty1
+ (* A meta-binding binder meta-bound to a possibly-typed pattern *)
+ (* the binder is supposed to come w/o an explicit type in the notation *)
+ | None, Some _ -> ty2
+ | Some ty1, Some t2 ->
+ (* An explicitly typed meta-binding binder, not supposed to be a pattern; checked in interp_notation *)
+ user_err ?loc:t2.CAst.loc Pp.(str "Unexpected type constraint in notation already providing a type constraint.")
+
+let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) na ty =
+ match na with
+ | Anonymous -> (renaming,env), None, Anonymous, Explicit, set_type ty None
| Name id ->
let store,get = set_temporary_memory () in
let test_kind = test_kind_tolerant in
try
(* We instantiate binder name with patterns which may be parsed as terms *)
let pat = coerce_to_cases_pattern_expr (fst (Id.Map.find id terms)) in
- let env,((disjpat,ids),id),na = intern_pat test_kind ntnvars env pat in
+ let env,((disjpat,ids),id),na,bk,t = intern_pat test_kind ntnvars env Explicit pat in
let pat, na = match disjpat with
| [pat] when is_patvar_store store pat -> let na = get () in None, na
- | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in
- (renaming,env), pat, na
+ | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na in
+ (renaming,env), pat, na.v, bk, set_type ty (Some t)
with Not_found ->
try
(* Trying to associate a pattern *)
- let pat,(onlyident,scopes) = Id.Map.find id binders in
+ let (pat,bk),(onlyident,scopes) = Id.Map.find id binders in
let env = set_env_scopes env scopes in
if onlyident then
(* Do not try to interpret a variable as a constructor *)
let na = out_patvar pat in
let env = push_name_env ntnvars [] env na in
- (renaming,env), None, na.v
+ let ty' = DAst.make @@ GHole (Evar_kinds.BinderType na.CAst.v,IntroAnonymous,None) in
+ (renaming,env), None, na.v, bk, set_type ty (Some ty')
else
(* Interpret as a pattern *)
- let env,((disjpat,ids),id),na = intern_pat test_kind ntnvars env pat in
+ let env,((disjpat,ids),id),na,bk,t = intern_pat test_kind ntnvars env bk pat in
let pat, na =
match disjpat with
| [pat] when is_patvar_store store pat -> let na = get () in None, na
- | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in
- (renaming,env), pat, na
+ | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na in
+ (renaming,env), pat, na.v, bk, set_type ty (Some t)
with Not_found ->
(* Binders not bound in the notation do not capture variables *)
(* outside the notation (i.e. in the substitution) *)
@@ -753,7 +772,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
let renaming' =
if Id.equal id id' then renaming else Id.Map.add id id' renaming
in
- (renaming',env), None, Name id'
+ (renaming',env), None, Name id', Explicit, set_type ty None
type binder_action =
| AddLetIn of lname * constr_expr * constr_expr option
@@ -878,12 +897,13 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
Id.Map.add id (gc, None) map
with Nametab.GlobalizationError _ -> map
in
- let mk_env' (c, (onlyident,scopes)) =
- let nenv = set_env_scopes env scopes in
+ let mk_env' ((c,_bk), (onlyident,(tmp_scope,subscopes))) =
+ let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
let test_kind =
if onlyident then test_kind_ident_in_notation
else test_kind_pattern_in_notation in
- let _,((disjpat,_),_),_ = intern_pat test_kind ntnvars nenv c in
+ let _,((disjpat,_),_),_,_,_ty = intern_pat test_kind ntnvars nenv Explicit c in
+ (* TODO: use cast? *)
match disjpat with
| [pat] -> (glob_constr_of_cases_pattern (Global.env()) pat, None)
| _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc ()
@@ -908,26 +928,15 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
aux (terms,None,Some (l,terminator,iter)) subinfos (NVar ldots_var)
with Not_found ->
anomaly (Pp.str "Inconsistent substitution of recursive notation."))
- | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt ->
+ | NProd (Name id, None, c') when option_mem_assoc id binderopt ->
let binder = snd (Option.get binderopt) in
expand_binders ?loc mkGProd [binder] (aux subst' (renaming,env) c')
- | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt ->
+ | NLambda (Name id, None, c') when option_mem_assoc id binderopt ->
let binder = snd (Option.get binderopt) in
expand_binders ?loc mkGLambda [binder] (aux subst' (renaming,env) c')
- (* Two special cases to keep binder name synchronous with BinderType *)
- | NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
- when Name.equal na na' ->
- let subinfos,disjpat,na = traverse_binder intern_pat ntnvars subst avoid subinfos na in
- let ty = DAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
- DAst.make ?loc @@ GProd (na,Explicit,ty,Option.fold_right apply_cases_pattern disjpat (aux subst' subinfos c'))
- | NLambda (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
- when Name.equal na na' ->
- let subinfos,disjpat,na = traverse_binder intern_pat ntnvars subst avoid subinfos na in
- let ty = DAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
- DAst.make ?loc @@ GLambda (na,Explicit,ty,Option.fold_right apply_cases_pattern disjpat (aux subst' subinfos c'))
| t ->
glob_constr_of_notation_constr_with_binders ?loc
- (traverse_binder intern_pat ntnvars subst avoid) (aux subst') ~h:binder_status_fun subinfos t
+ (traverse_binder intern_pat ntnvars subst avoid) (aux subst') ~h:binder_status_fun subinfos t
and subst_var (terms, binderopt, _terminopt) (renaming, env) id =
(* subst remembers the delimiters stack in the interpretation *)
(* of the notations *)
@@ -936,12 +945,13 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
intern (set_env_scopes env scopes) a
with Not_found ->
try
- let pat,(onlyident,scopes) = Id.Map.find id binders in
- let nenv = set_env_scopes env scopes in
+ let (pat,bk),(onlyident,scopes) = Id.Map.find id binders in
+ let env = set_env_scopes env scopes in
let test_kind =
if onlyident then test_kind_ident_in_notation
else test_kind_pattern_in_notation in
- let env,((disjpat,ids),id),na = intern_pat test_kind ntnvars nenv pat in
+ let env,((disjpat,ids),id),na,bk,_ty = intern_pat test_kind ntnvars env bk pat in
+ (* TODO: use cast? *)
match disjpat with
| [pat] -> glob_constr_of_cases_pattern (Global.env()) pat
| _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.")
@@ -983,13 +993,13 @@ let split_by_type ids subst =
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
| NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | 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
+ let binders' = Id.Map.add id ((coerce_to_cases_pattern_expr a,Explicit),(false,scl)) binders' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
| NtnTypeBinder NtnBinderParsedAsConstr AsIdent ->
let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
- let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in
+ let binders' = Id.Map.add id ((cases_pattern_of_name (coerce_to_name a),Explicit),(true,scl)) binders' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
- | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ as x) ->
+ | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder 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')
@@ -1031,7 +1041,7 @@ let intern_notation intern env ntnvars loc ntn fullargs =
(* Dispatch parsing substitution to an interpretation substitution *)
let subst = split_by_type ids fullargs in
(* Instantiate the notation *)
- instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst (Id.Map.empty, env) c
+ instantiate_notation_constr loc intern (intern_cases_pattern_as_binder intern) ntnvars subst (Id.Map.empty, env) c
(**********************************************************************)
(* Discriminating between bound variables and global references *)
@@ -1159,7 +1169,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
check_no_explicitation args1;
let subst = split_by_type ids (List.map fst args1,[],[],[]) in
let infos = (Id.Map.empty, env) in
- let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in
+ let c = instantiate_notation_constr loc intern (intern_cases_pattern_as_binder intern) ntnvars subst infos c in
let loc = c.loc in
let err () =
user_err ?loc (str "Notation " ++ pr_qualid qid
diff --git a/interp/notation.ml b/interp/notation.ml
index 286ece6cb6..b5951a9c59 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -64,7 +64,8 @@ let notation_binder_source_eq s1 s2 = match s1, s2 with
| NtnParsedAsIdent, NtnParsedAsIdent -> true
| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2
| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2
-| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false
+| NtnParsedAsBinder, NtnParsedAsBinder -> true
+| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _ | NtnParsedAsBinder), _ -> 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 c4d2a2a496..f51d3bfdfb 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -131,7 +131,11 @@ let compare_notation_constr lt (vars1,vars2) t1 t2 =
| NApp (t1, a1), NApp (t2, a2) -> aux vars renaming t1 t2; List.iter2 (aux vars renaming) a1 a2
| NLambda (na1, t1, u1), NLambda (na2, t2, u2)
| NProd (na1, t1, u1), NProd (na2, t2, u2) ->
- aux vars renaming t1 t2;
+ (match t1, t2 with
+ | None, None -> ()
+ | Some _, None -> if lt then strictly_lt := true
+ | Some t1, Some t2 -> aux vars renaming t1 t2
+ | None, Some _ -> raise Exit);
let renaming = check_eq_name vars renaming na1 na2 in
aux vars renaming u1 u2
| NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) ->
@@ -272,11 +276,25 @@ let default_binder_status_fun = {
slide = (fun x -> x);
}
+let test_implicit_argument_mark bk =
+ if not (Glob_ops.binding_kind_eq bk Explicit) then
+ user_err (Pp.str "Unexpected implicit argument mark.")
+
+let test_pattern_cast = function
+ | None -> ()
+ | Some t -> user_err ?loc:t.CAst.loc (Pp.str "Unsupported pattern cast.")
+
let protect g e na =
- let e',disjpat,na = g e na in
+ let e',disjpat,na,bk,t = g e na None in
if disjpat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern.");
+ test_implicit_argument_mark bk;
+ test_pattern_cast t;
e',na
+let set_anonymous_type na = function
+ | None -> DAst.make @@ GHole (Evar_kinds.BinderType na, IntroAnonymous, None)
+ | Some t -> t
+
let apply_cases_pattern_term ?loc (ids,disjpat) tm c =
let eqns = List.map (fun pat -> (CAst.make ?loc (ids,[pat],c))) disjpat in
DAst.make ?loc @@ GCases (Constr.LetPatternStyle, None, [tm,(Anonymous,None)], eqns)
@@ -302,15 +320,21 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
DAst.get (subst_glob_vars outerl it)
| NLambda (na,ty,c) ->
let e = h.switch_lambda e in
- let e',disjpat,na = g e na in GLambda (na,Explicit,f (h.restart_prod e) ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
+ let ty = Option.map (f (h.restart_prod e)) ty in
+ let e',disjpat,na',bk,ty = g e na ty in
+ GLambda (na',bk,set_anonymous_type na ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
| NProd (na,ty,c) ->
let e = h.switch_prod e in
- let e',disjpat,na = g e na in GProd (na,Explicit,f (h.restart_prod e) ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
+ let ty = Option.map (f (h.restart_prod e)) ty in
+ let e',disjpat,na',bk,ty = g e na ty in
+ GProd (na',bk,set_anonymous_type na ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
| NLetIn (na,b,t,c) ->
- let e',disjpat,na = g e na in
+ let t = Option.map (f (h.restart_prod e)) t in
+ let e',disjpat,na,bk,t = g e na t in
+ test_implicit_argument_mark bk;
(match disjpat with
- | None -> GLetIn (na,f (h.restart_lambda e) b,Option.map (f (h.restart_prod e)) t,f e' c)
- | Some (disjpat,_id) -> DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c)))
+ | None -> GLetIn (na,f (h.restart_lambda e) b,t,f e' c)
+ | Some (disjpat,_id) -> test_pattern_cast t; DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c)))
| NCases (sty,rtntypopt,tml,eqnl) ->
let e = h.no e in
let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
@@ -323,7 +347,11 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
e',Some (CAst.make ?loc (ind,nal')) in
let e',na' = protect g e' na in
(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
- let fold (idl,e) na = let (e,disjpat,na) = g e na in ((Name.cons na idl,e),disjpat,na) in
+ let fold (idl,e) na =
+ let (e,disjpat,na,bk,t) = g e na None in
+ test_implicit_argument_mark bk;
+ test_pattern_cast t;
+ ((Name.cons na idl,e),disjpat,na) in
let eqnl' = List.map (fun (patl,rhs) ->
let ((idl,e),patl) =
List.fold_left_map (cases_pattern_fold_map ?loc fold) ([],e) patl in
@@ -356,7 +384,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
let glob_constr_of_notation_constr ?loc x =
let rec aux () x =
- glob_constr_of_notation_constr_with_binders ?loc (fun () id -> ((),None,id)) aux () x
+ glob_constr_of_notation_constr_with_binders ?loc (fun () id t -> ((),None,id,Explicit,t)) aux () x
in aux () x
(******************************************************************************)
@@ -551,8 +579,8 @@ let notation_constr_and_vars_of_glob_constr recvars a =
| GApp (g,args) ->
(* Treat applicative notes as binary nodes *)
let a,args = List.sep_last args in mkNApp1 (aux (DAst.make (GApp (g, args))), aux a)
- | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c)
- | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c)
+ | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux_type ty,aux c)
+ | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux_type ty,aux c)
| GLetIn (na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t, aux c)
| GCases (sty,rtntypopt,tml,eqnl) ->
let f {CAst.v=(idl,pat,rhs)} = List.iter (add_id found) idl; (pat,aux rhs) in
@@ -589,6 +617,9 @@ let notation_constr_and_vars_of_glob_constr recvars a =
| GEvar _ | GPatVar _ ->
user_err Pp.(str "Existential variables not allowed in notations.")
) x
+ and aux_type t = DAst.with_val (function
+ | GHole (Evar_kinds.BinderType _,IntroAnonymous,None) -> None
+ | _ -> Some (aux t)) t
in
let t = aux a in
(* Side effect *)
@@ -697,13 +728,13 @@ let rec subst_notation_constr subst bound raw =
NList (id1,id2,r1',r2',b)
| NLambda (n,r1,r2) ->
- let r1' = subst_notation_constr subst bound r1
+ let r1' = Option.Smart.map (subst_notation_constr subst bound) r1
and r2' = subst_notation_constr subst bound r2 in
if r1' == r1 && r2' == r2 then raw else
NLambda (n,r1',r2')
| NProd (n,r1,r2) ->
- let r1' = subst_notation_constr subst bound r1
+ let r1' = Option.Smart.map (subst_notation_constr subst bound) r1
and r2' = subst_notation_constr subst bound r2 in
if r1' == r1 && r2' == r2 then raw else
NProd (n,r1',r2')
@@ -819,7 +850,7 @@ let abstract_return_type_context_glob_constr tml rtn =
let abstract_return_type_context_notation_constr tml rtn =
abstract_return_type_context snd
- (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, IntroAnonymous, None),c)) tml rtn
+ (fun na c -> NLambda(na,None,c)) tml rtn
let rec push_pattern_binders vars pat =
match DAst.get pat with
@@ -852,6 +883,7 @@ let is_onlybinding_pattern_like_meta isvar id metas =
| _,NtnTypeBinder (NtnBinderParsedAsConstr
(AsIdentOrPattern | AsStrictPattern)) -> true
| _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar)
+ | _,NtnTypeBinder NtnParsedAsBinder -> not isvar
| _ -> false
with Not_found -> false
@@ -1325,9 +1357,9 @@ let rec match_ inner u alp metas sigma a1 a2 =
List.fold_left2 (match_ may_use_eta u alp metas)
(match_hd u alp metas sigma f1 f2) l1 l2
| GLambda (na1,bk1,t1,b1), NLambda (na2,t2,b2) ->
- match_extended_binders false u alp metas na1 na2 bk1 t1 (match_in u alp metas sigma t1 t2) b1 b2
+ match_extended_binders false u alp metas na1 na2 bk1 t1 (match_in_type u alp metas sigma t1 t2) b1 b2
| GProd (na1,bk1,t1,b1), NProd (na2,t2,b2) ->
- match_extended_binders true u alp metas na1 na2 bk1 t1 (match_in u alp metas sigma t1 t2) b1 b2
+ match_extended_binders true u alp metas na1 na2 bk1 t1 (match_in_type u alp metas sigma t1 t2) b1 b2
| GLetIn (na1,b1,_,c1), NLetIn (na2,b2,None,c2)
| GLetIn (na1,b1,None,c1), NLetIn (na2,b2,_,c2) ->
match_binders u alp metas na1 na2 (match_in u alp metas sigma b1 b2) c1 c2
@@ -1396,14 +1428,14 @@ let rec match_ inner u alp metas sigma a1 a2 =
otherwise how to ensure it corresponds to a well-typed eta-expansion;
we make an exception for types which are metavariables: this is useful e.g.
to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *)
- | _b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner ->
+ | _b1, NLambda (Name id as na,(None | Some (NVar _) as t2),b2) when inner ->
let avoid =
Id.Set.union (free_glob_vars a1) (* as in Namegen: *) (glob_visible_short_qualid a1) in
let id' = Namegen.next_ident_away id avoid in
let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),IntroAnonymous,None) in
let sigma = match t2 with
- | NHole _ -> sigma
- | NVar id2 -> bind_term_env alp sigma id2 t1
+ | None -> sigma
+ | Some (NVar id2) -> bind_term_env alp sigma id2 t1
| _ -> assert false in
let (alp,sigma) =
if is_bindinglist_meta id metas then
@@ -1423,6 +1455,10 @@ let rec match_ inner u alp metas sigma a1 a2 =
| GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
| GCast _ | GInt _ | GFloat _ | GArray _), _ -> raise No_match
+and match_in_type u alp metas sigma t = function
+ | None -> sigma
+ | Some t' -> match_in u alp metas sigma t t'
+
and match_in u = match_ true u
and match_hd u = match_ false u
@@ -1497,7 +1533,7 @@ let match_notation_constr ~print_univ c ~vars (metas,pat) =
let v = glob_constr_of_cases_pattern (Global.env()) pat in
(((vars,v),scl)::terms',termlists',binders',binderlists')
| _ -> raise No_match)
- | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) ->
+ | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder) ->
(terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists')
| NtnTypeConstrList ->
(terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists')
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 9d451a5bb9..e7a0429b35 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -53,7 +53,7 @@ val apply_cases_pattern : ?loc:Loc.t ->
(Id.t list * cases_pattern_disjunction) * Id.t -> glob_constr -> glob_constr
val glob_constr_of_notation_constr_with_binders : ?loc:Loc.t ->
- ('a -> Name.t -> 'a * ((Id.t list * cases_pattern_disjunction) * Id.t) option * Name.t) ->
+ ('a -> Name.t -> glob_constr option -> 'a * ((Id.t list * cases_pattern_disjunction) * Id.t) option * Name.t * Glob_term.binding_kind * glob_constr option) ->
('a -> notation_constr -> glob_constr) -> ?h:'a binder_status_fun ->
'a -> notation_constr -> glob_constr
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 82238b71b7..29db23cc54 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -27,8 +27,8 @@ type notation_constr =
| NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
| NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
(* Part only in [glob_constr] *)
- | NLambda of Name.t * notation_constr * notation_constr
- | NProd of Name.t * notation_constr * notation_constr
+ | NLambda of Name.t * notation_constr option * notation_constr
+ | NProd of Name.t * notation_constr option * notation_constr
| NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
| NLetIn of Name.t * notation_constr * notation_constr option * notation_constr
| NCases of Constr.case_style * notation_constr option *
@@ -78,6 +78,8 @@ type notation_binder_source =
| NtnParsedAsIdent
(* This accepts ident, or pattern, or both *)
| NtnBinderParsedAsConstr of constr_as_binder_kind
+ (* This accepts ident, _, and quoted pattern *)
+ | NtnParsedAsBinder
type notation_var_instance_type =
| NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList
diff --git a/parsing/extend.ml b/parsing/extend.ml
index a6fa6edad5..94c3768116 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -58,6 +58,7 @@ type constr_prod_entry_key =
| ETProdName (* Parsed as a name (ident or _) *)
| ETProdReference (* Parsed as a global reference *)
| ETProdBigint (* Parsed as an (unbounded) integer *)
+ | ETProdOneBinder of bool (* Parsed as name, or name:type or 'pattern, possibly in closed form *)
| ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *)
| ETProdPattern of int (* Parsed as pattern as a binder (as subpart of a constr) *)
| ETProdConstrList of Constrexpr.notation_entry * (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr, or subentries of those *)
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 057fdb3841..b698415fd6 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -53,6 +53,7 @@ type constr_prod_entry_key =
| ETProdName (* Parsed as a name (ident or _) *)
| ETProdReference (* Parsed as a global reference *)
| ETProdBigint (* Parsed as an (unbounded) integer *)
+ | ETProdOneBinder of bool (* Parsed as name, or name:type or 'pattern, possibly in closed form *)
| ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *)
| ETProdPattern of int (* Parsed as pattern as a binder (as subpart of a constr) *)
| ETProdConstrList of Constrexpr.notation_entry * (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr, or subentries of those *)
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 67a061175a..68530178f8 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -39,6 +39,10 @@ let binder_of_name expl { CAst.loc = loc; v = na } =
let binders_of_names l =
List.map (binder_of_name Explicit) l
+let pat_of_name CAst.{loc;v} = match v with
+| Anonymous -> CAst.make ?loc @@ CPatAtom None
+| Name id -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident id))
+
let err () = raise Stream.Failure
(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
@@ -84,7 +88,8 @@ GRAMMAR EXTEND Gram
universe_level universe_name sort sort_family
global constr_pattern cpattern Constr.ident
closed_binder open_binders binder binders binders_fixannot
- record_declaration typeclass_constraint pattern arg type_cstr;
+ record_declaration typeclass_constraint pattern arg type_cstr
+ one_closed_binder one_open_binder;
Constr.ident:
[ [ id = Prim.ident -> { id } ] ]
;
@@ -438,13 +443,20 @@ GRAMMAR EXTEND Gram
{ List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (MaxImplicit, b), t)) tc }
| "`["; tc = LIST1 typeclass_constraint SEP "," ; "]" ->
{ List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (NonMaxImplicit, b), t)) tc }
- | "'"; p = pattern LEVEL "0" ->
- { let (p, ty) =
- match p.CAst.v with
- | CPatCast (p, ty) -> (p, Some ty)
- | _ -> (p, None)
- in
- [CLocalPattern (CAst.make ~loc (p, ty))] } ] ]
+ | "'"; p = pattern LEVEL "0" -> { [CLocalPattern p] } ] ]
+ ;
+ one_open_binder:
+ [ [ na = name -> { (pat_of_name na, Explicit) }
+ | na = name; ":"; t = lconstr -> { (CAst.make ~loc @@ CPatCast (pat_of_name na, t), Explicit) }
+ | b = one_closed_binder -> { b } ] ]
+ ;
+ one_closed_binder:
+ [ [ "("; na = name; ":"; t = lconstr; ")" -> { (CAst.make ~loc @@ CPatCast (pat_of_name na, t), Explicit) }
+ | "{"; na = name; "}" -> { (pat_of_name na, MaxImplicit) }
+ | "{"; na = name; ":"; t = lconstr; "}" -> { (CAst.make ~loc @@ CPatCast (pat_of_name na, t), MaxImplicit) }
+ | "["; na = name; "]" -> { (pat_of_name na, NonMaxImplicit) }
+ | "["; na = name; ":"; t = lconstr; "]" -> { (CAst.make ~loc @@ CPatCast (pat_of_name na, t), NonMaxImplicit) }
+ | "'"; p = pattern LEVEL "0" -> { (p, Explicit) } ] ]
;
typeclass_constraint:
[ [ "!" ; c = term LEVEL "200" -> { (CAst.make ~loc Anonymous), true, c }
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 22b5e70311..d49a49d242 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -327,6 +327,8 @@ module Constr =
let binder = Entry.create "binder"
let binders = Entry.create "binders"
let open_binders = Entry.create "open_binders"
+ let one_open_binder = Entry.create "one_open_binder"
+ let one_closed_binder = Entry.create "one_closed_binder"
let binders_fixannot = Entry.create "binders_fixannot"
let typeclass_constraint = Entry.create "typeclass_constraint"
let record_declaration = Entry.create "record_declaration"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index ce4c91d51f..d0ae594db1 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -203,6 +203,8 @@ module Constr :
val binder : local_binder_expr list Entry.t (* closed_binder or variable *)
val binders : local_binder_expr list Entry.t (* list of binder *)
val open_binders : local_binder_expr list Entry.t
+ val one_open_binder : kinded_cases_pattern_expr Entry.t
+ val one_closed_binder : kinded_cases_pattern_expr Entry.t
val binders_fixannot : (local_binder_expr list * recursion_order_expr option) Entry.t
val typeclass_constraint : (lname * bool * constr_expr) Entry.t
val record_declaration : constr_expr Entry.t
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index aab385a707..b64c2b956a 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -36,9 +36,11 @@ let ppcmd_of_cut = function
| PpFnl -> fnl ()
| PpBrk(n1,n2) -> brk(n1,n2)
+type pattern_quote_style = QuotedPattern | NotQuotedPattern
+
type unparsing =
| UnpMetaVar of entry_relative_level * Extend.side option
- | UnpBinderMetaVar of entry_relative_level
+ | UnpBinderMetaVar of entry_relative_level * pattern_quote_style
| UnpListMetaVar of entry_relative_level * unparsing list * Extend.side option
| UnpBinderListMetaVar of bool * unparsing list
| UnpTerminal of string
@@ -50,7 +52,7 @@ type extra_unparsing_rules = (string * string) list
let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with
| UnpMetaVar (p1,s1), UnpMetaVar (p2,s2) -> entry_relative_level_eq p1 p2 && s1 = s2
- | UnpBinderMetaVar p1, UnpBinderMetaVar p2 -> entry_relative_level_eq p1 p2
+ | UnpBinderMetaVar (p1,s1), UnpBinderMetaVar (p2,s2) -> entry_relative_level_eq p1 p2 && s1 = s2
| UnpListMetaVar (p1,l1,s1), UnpListMetaVar (p2,l2,s2) -> entry_relative_level_eq p1 p2 && List.for_all2eq unparsing_eq l1 l2 && s1 = s2
| UnpBinderListMetaVar (b1,l1), UnpBinderListMetaVar (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq l1 l2
| UnpTerminal s1, UnpTerminal s2 -> String.equal s1 s2
diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli
index 56a3fc8e3c..ca22aacacf 100644
--- a/parsing/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -28,10 +28,12 @@ val ppcmd_of_cut : ppcut -> Pp.t
(** {6 Printing rules for notations} *)
+type pattern_quote_style = QuotedPattern | NotQuotedPattern
+
(** Declare and look for the printing rule for symbolic notations *)
type unparsing =
| UnpMetaVar of entry_relative_level * Extend.side option
- | UnpBinderMetaVar of entry_relative_level
+ | UnpBinderMetaVar of entry_relative_level * pattern_quote_style
| UnpListMetaVar of entry_relative_level * unparsing list * Extend.side option
| UnpBinderListMetaVar of bool * unparsing list
| UnpTerminal of string
diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg
index 54fdea0860..74535a10d3 100644
--- a/plugins/ssrsearch/g_search.mlg
+++ b/plugins/ssrsearch/g_search.mlg
@@ -141,7 +141,7 @@ let interp_search_notation ?loc tag okey =
let rec sub () = function
| NVar x when List.mem_assoc x nvars -> DAst.make ?loc @@ GPatVar (FirstOrderPatVar x)
| c ->
- glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), None, x) sub () c in
+ glob_constr_of_notation_constr_with_binders ?loc (fun _ x t -> (), None, x, Explicit, t) sub () c in
let _, npat = Patternops.pattern_of_glob_constr (sub () body) in
Search.GlobSearchSubPattern (Vernacexpr.Anywhere,false,npat)
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index e312c68b7d..8942bc7805 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -98,10 +98,10 @@ let tag_var = tag Tag.variable
let pp2 = aux l in
let pp1 = pr (if parens && side <> None then LevelLe 0 else prec) c in
return unp pp1 pp2
- | UnpBinderMetaVar prec as unp :: l ->
- let c = pop bl in
+ | UnpBinderMetaVar (prec,style) as unp :: l ->
+ let c,bk = pop bl in
let pp2 = aux l in
- let pp1 = pr_patt prec c in
+ let pp1 = pr_patt prec style bk c in
return unp pp1 pp2
| UnpListMetaVar (prec, sl, side) as unp :: l ->
let cl = pop envlist in
@@ -273,28 +273,29 @@ let tag_var = tag Tag.variable
let las = lapp
let lpator = 0
let lpatrec = 0
+ let lpatcast = LevelLe 100
let lpattop = LevelLe 200
- let rec pr_patt sep inh p =
+ let rec pr_patt sep pr inh p =
let (strm,prec) = match CAst.(p.v) with
| CPatRecord l ->
- pr_record_body "{|" "|}" (pr_patt spc lpattop) l, lpatrec
+ pr_record_body "{|" "|}" (pr_patt spc pr lpattop) l, lpatrec
| CPatAlias (p, na) ->
- pr_patt mt (LevelLe las) p ++ str " as " ++ pr_lname na, las
+ pr_patt mt pr (LevelLe las) p ++ str " as " ++ pr_lname na, las
| CPatCstr (c, None, []) ->
pr_reference c, latom
| CPatCstr (c, None, args) ->
- pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) args, lapp
+ pr_reference c ++ prlist (pr_patt spc pr (LevelLt lapp)) args, lapp
| CPatCstr (c, Some args, []) ->
- str "@" ++ pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) args, lapp
+ str "@" ++ pr_reference c ++ prlist (pr_patt spc pr (LevelLt lapp)) args, lapp
| CPatCstr (c, Some expl_args, extra_args) ->
- surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) expl_args)
- ++ prlist (pr_patt spc (LevelLt lapp)) extra_args, lapp
+ surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc pr (LevelLt lapp)) expl_args)
+ ++ prlist (pr_patt spc pr (LevelLt lapp)) extra_args, lapp
| CPatAtom (None) ->
str "_", latom
@@ -303,25 +304,25 @@ let tag_var = tag Tag.variable
pr_reference r, latom
| CPatOr pl ->
- let pp p = hov 0 (pr_patt mt lpattop p) in
+ let pp p = hov 0 (pr_patt mt pr lpattop p) in
surround (hov 0 (prlist_with_sep pr_spcbar pp pl)), lpator
| CPatNotation (_,(_,"( _ )"),([p],[]),[]) ->
- pr_patt (fun()->str"(") lpattop p ++ str")", latom
+ pr_patt (fun()->str"(") pr lpattop p ++ str")", latom
| 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
+ let strm_not, l_not = pr_notation (pr_patt mt pr) (fun _ _ _ _ -> mt ()) (fun _ _ _ -> mt()) which s (l,ll,[],[]) in
(if List.is_empty args||prec_less l_not (LevelLt lapp) then strm_not else surround strm_not)
- ++ prlist (pr_patt spc (LevelLt lapp)) args, if not (List.is_empty args) then lapp else l_not
+ ++ prlist (pr_patt spc pr (LevelLt lapp)) args, if not (List.is_empty args) then lapp else l_not
| CPatPrim p ->
pr_prim_token p, latom
| CPatDelimiters (k,p) ->
- pr_delimiters k (pr_patt mt lsimplepatt p), 1
+ pr_delimiters k (pr_patt mt pr lsimplepatt p), 1
- | CPatCast _ ->
- assert false
+ | CPatCast (p,t) ->
+ (pr_patt mt pr lpatcast p ++ spc () ++ str ":" ++ ws 1 ++ pr t), 1
in
let loc = p.CAst.loc in
pr_with_comments ?loc
@@ -329,12 +330,21 @@ let tag_var = tag Tag.variable
let pr_patt = pr_patt mt
+ let pr_patt_binder pr prec style bk c =
+ match bk with
+ | MaxImplicit -> str "{" ++ pr_patt pr lpattop c ++ str "}"
+ | NonMaxImplicit -> str "[" ++ pr_patt pr lpattop c ++ str "]"
+ | Explicit ->
+ match style, c with
+ | NotQuotedPattern, _ | _, {v=CPatAtom _} -> pr_patt pr prec c
+ | QuotedPattern, _ -> str "'" ++ pr_patt pr prec c
+
let pr_eqn pr {loc;v=(pl,rhs)} =
spc() ++ hov 4
(pr_with_comments ?loc
(str "| " ++
hov 0 (prlist_with_sep pr_spcbar
- (fun p -> hov 0 (prlist_with_sep sep_v (pr_patt ltop) p)) pl
+ (fun p -> hov 0 (prlist_with_sep sep_v (pr_patt (pr ltop) ltop) p)) pl
++ str " =>") ++
pr_sep_com spc (pr ltop) rhs))
@@ -391,13 +401,8 @@ let tag_var = tag Tag.variable
surround (pr_lname na ++
pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++
str" :=" ++ spc() ++ pr_c c)
- | CLocalPattern {CAst.loc; v = p,tyo} ->
- let p = pr_patt lsimplepatt p in
- match tyo with
- | None ->
- str "'" ++ p
- | Some ty ->
- str "'" ++ surround (p ++ spc () ++ str ":" ++ ws 1 ++ pr_c ty)
+ | CLocalPattern p ->
+ str "'" ++ pr_patt pr_c lsimplepatt p
let pr_undelimited_binders sep pr_c =
prlist_with_sep sep (pr_binder_among_many pr_c)
@@ -459,16 +464,16 @@ let tag_var = tag Tag.variable
(pr_decl "with" true) dl ++
fnl() ++ keyword "for" ++ spc () ++ pr_id id
- let pr_asin pr na indnalopt =
+ let pr_as_in pr na indnalopt =
(match na with (* Decision of printing "_" or not moved to constrextern.ml *)
| Some na -> spc () ++ keyword "as" ++ spc () ++ pr_lname na
| None -> mt ()) ++
(match indnalopt with
| None -> mt ()
- | Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt lsimplepatt t)
+ | Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt pr lsimplepatt t)
let pr_case_item pr (tm,as_clause, in_clause) =
- hov 0 (pr (LevelLe lcast) tm ++ pr_asin pr as_clause in_clause)
+ hov 0 (pr (LevelLe lcast) tm ++ pr_as_in (pr ltop) as_clause in_clause)
let pr_case_type pr po =
match po with
@@ -601,8 +606,8 @@ let tag_var = tag Tag.variable
return (
hv 0 (
keyword "let" ++ spc () ++ str"'" ++
- hov 0 (pr_patt ltop p ++
- pr_asin (pr_dangling_with_for mt pr) as_clause in_clause ++
+ hov 0 (pr_patt (pr mt ltop) ltop p ++
+ pr_as_in (pr mt ltop) as_clause in_clause ++
str " :=" ++ pr spc ltop c ++
pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++
spc () ++ keyword "in" ++ pr spc ltop b)),
@@ -673,7 +678,7 @@ let tag_var = tag Tag.variable
| CNotation (_,(_,"( _ )"),([t],[],[],[])) ->
return (pr (fun()->str"(") ltop t ++ str")", latom)
| CNotation (which,s,env) ->
- pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) which s env
+ pr_notation (pr mt) (pr_patt_binder (pr mt ltop)) (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 ->
@@ -737,7 +742,7 @@ let tag_var = tag Tag.variable
let pr_constr_pattern_expr c = !term_pr.pr_constr_pattern_expr c
let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c
- let pr_cases_pattern_expr = pr_patt ltop
+ let pr_cases_pattern_expr = pr_patt (pr ltop) ltop
let pr_binders env sigma = pr_undelimited_binders spc (pr_expr env sigma ltop)
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index b2ebc61b4e..9bf765717f 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -433,7 +433,8 @@ let match_goals ot nt =
constr_expr ogname c c2;
constr_expr_opt ogname t t2
| CLocalPattern p, CLocalPattern p2 ->
- let (p,ty), (p2,ty2) = p.v,p2.v in
+ let ty = match p.v with CPatCast (_,ty) -> Some ty | _ -> None in
+ let ty2 = match p2.v with CPatCast (_,ty) -> Some ty | _ -> None in
constr_expr_opt ogname ty ty2
| _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (2)")
in
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 86c4b3cccc..df64ae2af3 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -197,3 +197,15 @@ Found an inductive type while a pattern was expected.
: nat * nat
%%%
: Type
+## (x, _) (x = 0)
+ : Prop
+The command has indeed failed with message:
+Unexpected type constraint in notation already providing a type constraint.
+## '(x, y) (x + y = 0)
+ : Prop
+## x (x = 0)
+ : Prop
+## '(x, y) (x = 0)
+ : Prop
+fun f : ## a (a = 0) => f 1 eq_refl
+ : ## a (a = 0) -> 1 = 0
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 6af192ea82..ebc1426fc8 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -487,3 +487,21 @@ Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
Check %%%.
End MorePrecise3.
+
+Module TypedPattern.
+
+Notation "## x P" := (forall x:nat*nat, P) (x pattern, at level 0).
+Check ## (x,y) (x=0).
+Fail Check ## ((x,y):bool*bool) (x=y).
+
+End TypedPattern.
+
+Module SingleBinder.
+
+Notation "## x P" := (forall x, x = x -> P) (x binder, at level 0).
+Check ## '(x,y) (x+y=0).
+Check ## (x:nat) (x=0).
+Check ## '((x,y):nat*nat) (x=0).
+Check fun (f : ## {a} (a=0)) => f (a:=1) eq_refl.
+
+End SingleBinder.
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index efe4e17d0b..ad6ac8d3f3 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -249,6 +249,7 @@ type (_, _) entry =
| TTName : ('self, lname) entry
| TTReference : ('self, qualid) entry
| TTBigint : ('self, string) entry
+| TTBinder : bool -> ('self, kinded_cases_pattern_expr) entry
| TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
| TTConstrList : notation_entry * prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry
| TTPattern : int -> ('self, cases_pattern_expr) entry
@@ -364,6 +365,8 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol =
| TTClosedBinderList [] -> MayRecNo (Pcoq.Symbol.list1 (Pcoq.Symbol.nterm Constr.binder))
| TTClosedBinderList tkl -> MayRecNo (Pcoq.Symbol.list1sep (Pcoq.Symbol.nterm Constr.binder) (make_sep_rules tkl) false)
| TTName -> MayRecNo (Pcoq.Symbol.nterm Prim.name)
+| TTBinder true -> MayRecNo (Pcoq.Symbol.nterm Constr.one_open_binder)
+| TTBinder false -> MayRecNo (Pcoq.Symbol.nterm Constr.one_closed_binder)
| TTOpenBinderList -> MayRecNo (Pcoq.Symbol.nterm Constr.open_binders)
| TTBigint -> MayRecNo (Pcoq.Symbol.nterm Prim.bignat)
| TTReference -> MayRecNo (Pcoq.Symbol.nterm Constr.global)
@@ -372,6 +375,7 @@ let interp_entry forpat e = match e with
| ETProdName -> TTAny TTName
| ETProdReference -> TTAny TTReference
| ETProdBigint -> TTAny TTBigint
+| ETProdOneBinder o -> TTAny (TTBinder o)
| ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat))
| ETProdPattern p -> TTAny (TTPattern p)
| ETProdConstrList (s, p, tkl) -> TTAny (TTConstrList (s, p, tkl, forpat))
@@ -385,7 +389,7 @@ let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na
type 'r env = {
constrs : 'r list;
constrlists : 'r list list;
- binders : cases_pattern_expr list;
+ binders : kinded_cases_pattern_expr list;
binderlists : local_binder_expr list list;
}
@@ -396,14 +400,15 @@ match e with
| TTConstr _ -> push_constr subst v
| TTName ->
begin match forpat with
- | ForConstr -> { subst with binders = cases_pattern_expr_of_name v :: subst.binders }
+ | ForConstr -> { subst with binders = (cases_pattern_expr_of_name v, Glob_term.Explicit) :: subst.binders }
| ForPattern -> push_constr subst (cases_pattern_expr_of_name v)
end
| TTPattern _ ->
begin match forpat with
- | ForConstr -> { subst with binders = v :: subst.binders }
+ | ForConstr -> { subst with binders = (v, Glob_term.Explicit) :: subst.binders }
| ForPattern -> push_constr subst v
end
+| TTBinder o -> { subst with binders = v :: subst.binders }
| TTOpenBinderList -> { subst with binderlists = v :: subst.binderlists }
| TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists }
| TTBigint ->
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index dc2b2e889e..8759798331 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -342,12 +342,10 @@ let unparsing_metavar i from typs =
match x with
| ETConstr _ | ETGlobal | ETBigint ->
UnpMetaVar (prec,side)
- | ETPattern _ ->
- UnpBinderMetaVar prec
- | ETIdent ->
- UnpBinderMetaVar prec
- | ETBinder isopen ->
- assert false
+ | ETPattern _ | ETIdent ->
+ UnpBinderMetaVar (prec,NotQuotedPattern)
+ | ETBinder _ ->
+ UnpBinderMetaVar (prec,QuotedPattern)
(* Heuristics for building default printing rules *)
@@ -636,7 +634,7 @@ let prod_entry_type = function
| ETIdent -> ETProdName
| ETGlobal -> ETProdReference
| ETBigint -> ETProdBigint
- | ETBinder _ -> assert false (* See check_binder_type *)
+ | ETBinder o -> ETProdOneBinder o
| ETConstr (s,_,p) -> ETProdConstr (s,p)
| ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n)
@@ -970,15 +968,6 @@ let check_useless_entry_types recvars mainvars etyps =
(Id.print x ++ str " is unbound in the notation.")
| _ -> ()
-let check_binder_type recvars etyps =
- let l1,l2 = List.split recvars in
- let l = l1@l2 in
- List.iter (function
- | (x,ETBinder b) when not (List.mem x l) ->
- CErrors.user_err (str (if b then "binder" else "closed binder") ++
- strbrk " is only for use in recursive notations for binders.")
- | _ -> ()) etyps
-
let interp_non_syntax_modifiers mods =
let set modif (only_parsing,only_printing,entry) = match modif with
| SetOnlyParsing -> Some (true,only_printing,entry)
@@ -1058,7 +1047,7 @@ let make_interpretation_type isrec isonlybinding default_if_binding = function
| ETBigint | ETGlobal -> NtnTypeConstr
| ETBinder _ ->
if isrec then NtnTypeBinderList
- else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.")
+ else NtnTypeBinder NtnParsedAsBinder
let subentry_of_constr_prod_entry from_level = function
(* Specific 8.2 approximation *)
@@ -1297,7 +1286,6 @@ let compute_syntax_data ~local deprecation df modifiers =
let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in
let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in
let _ = check_useless_entry_types recvars mainvars mods.etyps in
- let _ = check_binder_type recvars mods.etyps in
(* Notations for interp and grammar *)
let msgs,n = find_precedence mods.custom mods.level mods.etyps symbols onlyprint in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:16:59 +0000