aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrintern.ml3
-rw-r--r--interp/notation.ml2
-rw-r--r--interp/notation_ops.ml69
-rw-r--r--interp/reserve.ml2
-rw-r--r--intf/notation_term.ml4
-rw-r--r--test-suite/output/Notations3.out2
-rw-r--r--test-suite/output/Notations3.v4
7 files changed, 48 insertions, 38 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3c8643ee36..bedf932b03 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -663,12 +663,13 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
Some (Genintern.generic_substitute_notation bindings arg)
in
DAst.make ?loc @@ GHole (knd, naming, arg)
- | NBinderList (x,y,iter,terminator) ->
+ | NBinderList (x,y,iter,terminator,lassoc) ->
(try
(* All elements of the list are in scopes (scopt,subscopes) *)
let (bl,(scopt,subscopes)) = Id.Map.find x binders in
(* We flatten binders so that we can interpret them at substitution time *)
let bl = flatten_binders bl in
+ let bl = if lassoc then List.rev bl else bl in
(* We isolate let-ins which do not contribute to the repeated pattern *)
let l = List.map (function | CLocalDef (na,c,t) -> AddLetIn (na,c,t)
| binder -> AddPreBinderIter (y,binder)) bl in
diff --git a/interp/notation.ml b/interp/notation.ml
index 94ce2a6c8d..31f16e1a90 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -292,7 +292,7 @@ let cases_pattern_key c = match DAst.get c with
let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
| NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
| NList (_,_,NApp (NRef ref,args),_,_)
- | NBinderList (_,_,NApp (NRef ref,args),_) ->
+ | NBinderList (_,_,NApp (NRef ref,args),_,_) ->
RefKey (canonical_gr ref), Some (List.length args)
| NRef ref -> RefKey(canonical_gr ref), None
| NApp (_,args) -> Oth, Some (List.length args)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index c414ba67a9..73b5100ca6 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -42,9 +42,9 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
| NProd (na1, t1, u1), NProd (na2, t2, u2) ->
Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
-| NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) ->
+| NBinderList (i1, j1, t1, u1, b1), NBinderList (i2, j2, t2, u2, b2) ->
Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 &&
- (eq_notation_constr vars) u1 u2
+ (eq_notation_constr vars) u1 u2 && b1 == b2
| NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) ->
Name.equal na1 na2 && eq_notation_constr vars b1 b2 &&
Option.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
@@ -146,11 +146,11 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
let inner = lt @@ GApp (lt @@ GVar (ldots_var),[subst_glob_vars innerl it]) in
let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in
DAst.get (subst_glob_vars outerl it)
- | NBinderList (x,y,iter,tail) ->
+ | NBinderList (x,y,iter,tail,swap) ->
let t = f e tail in let it = f e iter in
- let innerl = [(ldots_var,t);(x, lt @@ GVar y)] in
+ let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in
let inner = lt @@ GApp (lt @@ GVar ldots_var,[subst_glob_vars innerl it]) in
- let outerl = [(ldots_var,inner)] in
+ let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in
DAst.get (subst_glob_vars outerl it)
| NLambda (na,ty,c) ->
let e',na = g e na in GLambda (na,Explicit,f e ty,f e' c)
@@ -255,7 +255,7 @@ let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b'
type recursive_pattern_kind =
| RecursiveTerms of bool (* associativity *)
-| RecursiveBinders of glob_constr * glob_constr
+| RecursiveBinders of bool (* associativity *) * glob_constr * glob_constr
let compare_recursive_parts found f f' (iterator,subc) =
let diff = ref None in
@@ -289,9 +289,11 @@ let compare_recursive_parts found f f' (iterator,subc) =
| GLambda (Name x,_,t_x,c), GLambda (Name y,_,t_y,term)
| GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) when not (Id.equal x y) ->
(* We found a binding position where it differs *)
+ let lassoc = match !terminator with None -> false | Some _ -> true in
+ let x,t_x,y,t_y = if lassoc then y,t_y,x,t_x else x,t_x,y,t_y in
begin match !diff with
| None ->
- let () = diff := Some (x, y, RecursiveBinders (t_x,t_y)) in
+ let () = diff := Some (x, y, RecursiveBinders (lassoc,t_x,t_y)) in
aux c term
| Some _ -> false
end
@@ -323,15 +325,15 @@ let compare_recursive_parts found f f' (iterator,subc) =
(* found variables have been collected by compare_constr *)
found := { !found with vars = List.remove Id.equal y (!found).vars;
recursive_term_vars = Option.fold_right (fun a l -> a::l) toadd (!found).recursive_term_vars };
- NList (x,y,iterator,f (Option.get !terminator),lassoc)
- | Some (x,y,RecursiveBinders (t_x,t_y)) ->
- let iterator = f' (subst_glob_vars [x, DAst.make @@ GVar y] iterator) in
- (* found have been collected by compare_constr *)
+ NList (x,y,iterator,f (Option.get !terminator),lassoc)
+ | Some (x,y,RecursiveBinders (lassoc,t_x,t_y)) ->
+ let iterator = f' (if lassoc then iterator else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in
+ (* found have been collected by compare_constr *)
found := { !found with vars = List.remove Id.equal y (!found).vars;
recursive_binders_vars = (x,y) :: (!found).recursive_binders_vars };
- check_is_hole x t_x;
- check_is_hole y t_y;
- NBinderList (x,y,iterator,f (Option.get !terminator))
+ check_is_hole x t_x;
+ check_is_hole y t_y;
+ NBinderList (x,y,iterator,f (Option.get !terminator),lassoc)
else
raise Not_found
@@ -512,11 +514,11 @@ let rec subst_notation_constr subst bound raw =
if r1' == r1 && r2' == r2 then raw else
NProd (n,r1',r2')
- | NBinderList (id1,id2,r1,r2) ->
+ | NBinderList (id1,id2,r1,r2,b) ->
let r1' = subst_notation_constr subst bound r1
and r2' = subst_notation_constr subst bound r2 in
if r1' == r1 && r2' == r2 then raw else
- NBinderList (id1,id2,r1',r2')
+ NBinderList (id1,id2,r1',r2',b)
| NLetIn (n,r1,t,r2) ->
let r1' = subst_notation_constr subst bound r1 in
@@ -929,28 +931,28 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 =
let glue_letin_with_decls = true
-let rec match_iterated_binders islambda decls bi = DAst.(with_loc_val (fun ?loc -> function
+let rec match_iterated_binders islambda decls bi lassoc = DAst.(with_loc_val (fun ?loc -> function
| GLambda (na,bk,t,b) as b0 ->
begin match na, DAst.get b with
| Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))])
when islambda && is_gvar p e && not (occur_glob_constr p b) ->
- match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
+ match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b lassoc
| _, _ when islambda ->
- match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b
+ match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b lassoc
| _ -> (decls, DAst.make ?loc b0)
end
| GProd (na,bk,t,b) as b0 ->
begin match na, DAst.get b with
| Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))])
when not islambda && is_gvar p e && not (occur_glob_constr p b) ->
- match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
+ match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b lassoc
| Name _, _ when not islambda ->
- match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b
+ match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b lassoc
| _ -> (decls, DAst.make ?loc b0)
end
| GLetIn (na,c,t,b) when glue_letin_with_decls ->
match_iterated_binders islambda
- ((DAst.make ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b
+ ((DAst.make ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b lassoc
| b -> (decls, DAst.make ?loc b)
)) bi
@@ -964,7 +966,7 @@ let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas
let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas
-let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin =
+let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin lassoc =
let rec aux sigma bl rest =
try
let metas = add_ldots_var (add_meta_bindinglist y metas) in
@@ -978,6 +980,7 @@ let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin =
with No_match when not (List.is_empty bl) ->
bl, rest, sigma in
let bl,rest,sigma = aux sigma [] rest in
+ let bl = if lassoc then List.rev bl else bl in
let alp,sigma = bind_bindinglist_env alp sigma x bl in
match_fun alp metas sigma rest termin
@@ -1041,46 +1044,46 @@ let rec match_ inner u alp metas sigma a1 a2 =
| r1, NList (x,y,iter,termin,lassoc) ->
match_termlist (match_hd u alp) alp metas sigma a1 x y iter termin lassoc
- | GLambda (na1, bk, t1, b1), NBinderList (x,y,iter,termin) ->
+ | GLambda (na1, bk, t1, b1), NBinderList (x,y,iter,termin,lassoc) ->
begin match na1, DAst.get b1, iter with
(* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
| Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), NLambda (Name _, _, _)
when is_gvar p e && not (occur_glob_constr p b1) ->
- let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 in
+ let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 lassoc in
let alp,sigma = bind_bindinglist_env alp sigma x decls in
match_in u alp metas sigma b termin
(* Matching recursive notations for binders: ad hoc cases supporting let-in *)
| _, _, NLambda (Name _,_,_) ->
- let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 in
+ let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 lassoc in
(* TODO: address the possibility that termin is a Lambda itself *)
let alp,sigma = bind_bindinglist_env alp sigma x decls in
match_in u alp metas sigma b termin
(* Matching recursive notations for binders: general case *)
| _, _, _ ->
- match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin
+ match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin lassoc
end
- | GProd (na1, bk, t1, b1), NBinderList (x,y,iter,termin) ->
+ | GProd (na1, bk, t1, b1), NBinderList (x,y,iter,termin,lassoc) ->
(* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
begin match na1, DAst.get b1, iter, termin with
| Name p, GCases (LetPatternStyle,None,[(e, _)],[(_,(ids,[cp],b1))]), NProd (Name _,_,_), NVar _
when is_gvar p e && not (occur_glob_constr p b1) ->
- let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 in
+ let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 lassoc in
let alp,sigma = bind_bindinglist_env alp sigma x decls in
match_in u alp metas sigma b termin
| _, _, NProd (Name _,_,_), _ when na1 != Anonymous ->
- let (decls,b) = match_iterated_binders false [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 in
+ let (decls,b) = match_iterated_binders false [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 lassoc in
(* TODO: address the possibility that termin is a Prod itself *)
let alp,sigma = bind_bindinglist_env alp sigma x decls in
match_in u alp metas sigma b termin
(* Matching recursive notations for binders: general case *)
| _, _, _, _ ->
- match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin
+ match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin lassoc
end
(* Matching recursive notations for binders: general case *)
- | _r, NBinderList (x,y,iter,termin) ->
- match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin
+ | _r, NBinderList (x,y,iter,termin,lassoc) ->
+ match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin lassoc
(* Matching individual binders as part of a recursive pattern *)
| GLambda (na1, bk, t1, b1), NLambda (na2, t2, b2) ->
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 22c5a2f5e5..04710282f5 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -71,7 +71,7 @@ let reserve_revtable = Summary.ref KeyMap.empty ~name:"reserved-type-rev"
let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
| NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
| NList (_,_,NApp (NRef ref,args),_,_)
- | NBinderList (_,_,NApp (NRef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args)
+ | NBinderList (_,_,NApp (NRef ref,args),_,_) -> RefKey (canonical_gr ref), Some (List.length args)
| NRef ref -> RefKey(canonical_gr ref), None
| _ -> Oth, None
diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index 028d14ccfd..52fd0f368f 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -25,11 +25,11 @@ type notation_constr =
| NVar of Id.t
| NApp of notation_constr * notation_constr list
| NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option
- | NList of Id.t * Id.t * notation_constr * notation_constr * bool
+ | 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
- | NBinderList of Id.t * Id.t * notation_constr * 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 *
(notation_constr * (Name.t * (inductive * Name.t list) option)) list *
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index cf69874ca7..e114ea8948 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -161,3 +161,5 @@ exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R),
exists_true (x : nat) (A : Type) (R : A -> A -> Prop)
(_ : Reflexive R) (y : nat), x + y = 0 -> forall z : A, R z z
: Prop
+{{{{True, nat -> True}}, nat -> True}}
+ : Prop * Prop * Prop
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 3e07fbce91..a7fed35611 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -278,3 +278,7 @@ Class Reflexive {A:Type} (R : A->A->Prop) := reflexivity : forall x : A, R x x.
Check exists_true `{Reflexive A R}, forall x, R x x.
Check exists_true x `{Reflexive A R} y, x+y=0 -> forall z, R z z.
End G.
+
+(* Allows recursive patterns for binders to be associative on the left *)
+Notation "!! x .. y # A #" := (.. (A,(forall x, True)) ..,(forall y, True)) (at level 200, x binder).
+Check !! a b : nat # True #.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:18:52 +0000