From 65505b835d6a77b8702d11d09e8cf6b84c529c65 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 12 Aug 2017 13:42:01 +0200
Subject: Adding support for re-folding notation referring to isolated "forall
 '(x,y), t".

Was apparently forgotten in a67bd7f9.
---
 interp/notation_ops.ml | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 326d05cba6..2e3f19a37d 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1084,11 +1084,18 @@ let rec match_ inner u alp metas sigma a1 a2 =
     | _ ->
       match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
     end
-
-  | GProd (na,bk,t,b1), NProd (Name id,_,b2)
-      when is_bindinglist_meta id metas && na != Anonymous ->
-      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na,bk,t)] in
+  | GProd (na1, bk, t1, b1), NProd (na2, t2, b2) ->
+    begin match na1, DAst.get b1, na2 with
+    | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id
+      when is_gvar p e && is_bindinglist_meta id metas && not (occur_glob_constr p b1) ->
+      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] in
       match_in u alp metas sigma b1 b2
+    | _, _, Name id when is_bindinglist_meta id metas && na1 != Anonymous ->
+      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] in
+      match_in u alp metas sigma b1 b2
+    | _ ->
+      match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
+    end
 
   (* Matching compositionally *)
   | GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
@@ -1104,8 +1111,6 @@ let rec match_ inner u alp metas sigma a1 a2 =
       let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in
       List.fold_left2 (match_ may_use_eta u alp metas)
         (match_in u alp metas sigma f1 f2) l1 l2
-  | GProd (na1,_,t1,b1), NProd (na2,t2,b2) ->
-     match_binders u alp metas na1 na2 (match_in 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
-- 
cgit v1.2.3


From 6e1f26a075a48fb32bce32e07d6b58e2f38b97a5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 12 Aug 2017 14:23:11 +0200
Subject: More precise explanation when a notation is not reversible for
 printing.

---
 interp/notation_ops.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 2e3f19a37d..472b9de599 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -396,7 +396,7 @@ let notation_constr_and_vars_of_glob_constr a =
   t, !found, !has_ltac
 
 let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) =
-  let injective = ref true in
+  let injective = ref [] in
   let recvars = nenv.ninterp_rec_vars in
   let fold _ y accu = Id.Set.add y accu in
   let useless_vars = Id.Map.fold fold recvars Id.Set.empty in
@@ -419,7 +419,7 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) =
 	user_err Pp.(str
           (Id.to_string x ^
           " should not be bound in a recursive pattern of the right-hand side."))
-      else injective := false
+      else injective := x :: !injective
   in
   let check_pair s x y where =
     if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then
@@ -440,12 +440,15 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) =
 	end
     | NtnInternTypeIdent -> check_bound x in
   Id.Map.iter check_type vars;
-  !injective
+  List.rev !injective
 
 let notation_constr_of_glob_constr nenv a =
   let a, found, has_ltac = notation_constr_and_vars_of_glob_constr a in
   let injective = check_variables_and_reversibility nenv found in
-  a, not has_ltac && injective
+  let status = if has_ltac then HasLtac else match injective with
+  | [] -> APrioriReversible
+  | l -> NonInjective l in
+  a, status
 
 (**********************************************************************)
 (* Substitution of kernel names, avoiding a list of bound identifiers *)
-- 
cgit v1.2.3


From 6901f720c6115c8eec1343846641a5c8453c3268 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 12 Aug 2017 17:18:36 +0200
Subject: Notations: documenting structure collecting variables occurring in
 notation.

---
 interp/notation_ops.ml | 29 ++++++++++++++++++-----------
 1 file changed, 18 insertions(+), 11 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 472b9de599..301ec69847 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -201,7 +201,13 @@ let glob_constr_of_notation_constr ?loc x =
 (******************************************************************************)
 (* Translating a glob_constr into a notation, interpreting recursive patterns *)
 
-let add_id r id = r := (id :: pi1 !r, pi2 !r, pi3 !r)
+type found_variables = {
+    vars : Id.t list;
+    recursive_term_vars : (Id.t * Id.t) list;
+    recursive_binders_vars : (Id.t * Id.t) list;
+  }
+
+let add_id r id = r := { !r with vars = id :: (!r).vars }
 let add_name r = function Anonymous -> () | Name id -> add_id r id
 
 let is_gvar id c = match DAst.get c with
@@ -301,12 +307,12 @@ let compare_recursive_parts found f f' (iterator,subc) =
           (str "Both ends of the recursive pattern are the same.")
     | Some (x,y,RecursiveTerms lassoc) ->
         let toadd,x,y,lassoc =
-          if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) ||
-             List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi3 !found)
+          if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_term_vars ||
+             List.mem_f (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_binders_vars
           then
             None,x,y,lassoc
-          else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi2 !found) ||
-                  List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi3 !found)
+          else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (!found).recursive_term_vars ||
+                  List.mem_f (pair_equal Id.equal Id.equal) (y,x) (!found).recursive_binders_vars
           then
             None,y,x,not lassoc
           else
@@ -315,14 +321,14 @@ let compare_recursive_parts found f f' (iterator,subc) =
 	  f' (if lassoc then iterator
 	      else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in
 	(* found variables have been collected by compare_constr *)
-	found := (List.remove Id.equal y (pi1 !found),
-                  Option.fold_right (fun a l -> a::l) toadd (pi2 !found),
-                  pi3 !found);
+        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 *)
-	found := (List.remove Id.equal y (pi1 !found), pi2 !found, (x,y) :: pi3 !found);
+        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))
@@ -330,7 +336,7 @@ let compare_recursive_parts found f f' (iterator,subc) =
     raise Not_found
 
 let notation_constr_and_vars_of_glob_constr a =
-  let found = ref ([],[],[]) in
+  let found = ref { vars = []; recursive_term_vars = []; recursive_binders_vars = [] } in
   let has_ltac = ref false in
   let rec aux c =
     let keepfound = !found in
@@ -395,7 +401,8 @@ let notation_constr_and_vars_of_glob_constr a =
   (* Side effect *)
   t, !found, !has_ltac
 
-let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) =
+let check_variables_and_reversibility nenv
+  { vars = found; recursive_term_vars = foundrec; recursive_binders_vars = foundrecbinding } =
   let injective = ref [] in
   let recvars = nenv.ninterp_rec_vars in
   let fold _ y accu = Id.Set.add y accu in
-- 
cgit v1.2.3


From 51976c9f2157953f794ed1efcd68403a8545d346 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 9 Aug 2017 13:58:59 +0200
Subject: A bit of miscellaneous code documentation around notations.

---
 interp/notation_ops.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 301ec69847..c414ba67a9 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -338,6 +338,7 @@ let compare_recursive_parts found f f' (iterator,subc) =
 let notation_constr_and_vars_of_glob_constr a =
   let found = ref { vars = []; recursive_term_vars = []; recursive_binders_vars = [] } in
   let has_ltac = ref false in
+  (* Turn a glob_constr into a notation_constr by first trying to find a recursive pattern *)
   let rec aux c =
     let keepfound = !found in
     (* n^2 complexity but small and done only once per notation *)
-- 
cgit v1.2.3


From d4c2ed95fcfd64cdcc10e51e40be739d9f1c4a74 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 13 Aug 2017 20:05:03 +0200
Subject: Allows recursive patterns for binders to be associative on the left.

This makes treatment of recursive binders closer to the one of
recursive terms. It is unclear whether there are interesting notations
liable to use this, but this shall make easier mixing recursive
binders and recursive terms as in next commits.

Example of (artificial) notation that this commit supports:

  Notation "! x .. y # A #" :=
    (.. (A,(forall x, True)) ..,(forall y, True))
    (at level 200, x binder).
---
 interp/notation_ops.ml | 69 ++++++++++++++++++++++++++------------------------
 1 file changed, 36 insertions(+), 33 deletions(-)

(limited to 'interp/notation_ops.ml')

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) ->
-- 
cgit v1.2.3


From a18e87f6a929ce296f8c277b310e286151e06293 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 14 Aug 2017 01:27:04 +0200
Subject: Allowing variables used in recursive notation to occur several times
 in pattern.

This allows for instance to support recursive notations of the form:

Notation "! x .. y # A #" :=
  (((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..)
  (at level 200, x binder).
---
 interp/notation_ops.ml | 25 ++++++++++++++++++++++---
 1 file changed, 22 insertions(+), 3 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 73b5100ca6..ac65f6875f 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -284,7 +284,9 @@ let compare_recursive_parts found f f' (iterator,subc) =
       | None ->
         let () = diff := Some (x, y, RecursiveTerms lassoc) in
         true
-      | Some _ -> false
+      | Some (x', y', RecursiveTerms lassoc')
+      | Some (x', y', RecursiveBinders (lassoc',_,_)) ->
+        Id.equal x x' && Id.equal y y' && lassoc = lassoc'
       end
   | 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) ->
@@ -295,7 +297,11 @@ let compare_recursive_parts found f f' (iterator,subc) =
       | None ->
         let () = diff := Some (x, y, RecursiveBinders (lassoc,t_x,t_y)) in
         aux c term
-      | Some _ -> false
+      | Some (x', y', RecursiveBinders (lassoc',_,_)) ->
+        Id.equal x x' && Id.equal y y' && lassoc = lassoc'
+      | Some (x', y', RecursiveTerms lassoc') ->
+        let () = diff := Some (x, y, RecursiveBinders (lassoc,t_x,t_y)) in
+        Id.equal x x' && Id.equal y y' && lassoc = lassoc'
       end
   | _ ->
       mk_glob_constr_eq aux c1 c2 in
@@ -327,10 +333,21 @@ let compare_recursive_parts found f f' (iterator,subc) =
                                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 (lassoc,t_x,t_y)) ->
+        let toadd,x,y,lassoc =
+          if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_term_vars ||
+             List.mem_f (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_binders_vars
+          then
+            None,x,y,lassoc
+          else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (!found).recursive_term_vars ||
+                  List.mem_f (pair_equal Id.equal Id.equal) (y,x) (!found).recursive_binders_vars
+          then
+            None,y,x,not lassoc
+          else
+            Some (x,y),x,y,lassoc in
         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 };
+                               recursive_binders_vars = Option.fold_right (fun a l -> a::l) toadd (!found).recursive_binders_vars };
         check_is_hole x t_x;
         check_is_hole y t_y;
         NBinderList (x,y,iterator,f (Option.get !terminator),lassoc)
@@ -976,6 +993,8 @@ let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin las
         match Id.List.assoc y binderlists with [b] -> b | _ ->assert false
       in
       let sigma = remove_bindinglist_sigma y (remove_sigma ldots_var sigma) in
+      (* In case y is bound not only to a binder but also to a term *)
+      let sigma = remove_sigma y sigma in
       aux sigma (b::bl) rest
     with No_match when not (List.is_empty bl) ->
       bl, rest, sigma in
-- 
cgit v1.2.3


From 96d6ef7036e19bf1def1512abae5ef8c6ace06b0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 14 Aug 2017 13:29:39 +0200
Subject: Supporting recursive notations reversing the left-to-right order.

Seizing this opportunity to generalize the possibility for different
associativity into simply reversing the order or not. Also dropping
some dead code.

Example of recursive notation now working:

  Notation "[ a , .. , b |- A ]" := (cons b .. (cons a nil) .., A).
---
 interp/notation_ops.ml | 172 ++++++++++++++++++++++++-------------------------
 1 file changed, 86 insertions(+), 86 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index ac65f6875f..602271bf62 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -251,13 +251,25 @@ let check_is_hole id t = match DAst.get t with GHole _ -> () | _ ->
    (strbrk "In recursive notation with binders, " ++ Id.print id ++
     strbrk " is expected to come without type.")
 
+let check_pair_matching ?loc x y x' y' revert revert' =
+  if not (Id.equal x x' && Id.equal y y' && revert = revert') then
+    let x,y = if revert then y,x else x,y in
+    let x',y' = if revert' then y',x' else x',y' in
+    (* This is a case where one would like to highlight two locations! *)
+    user_err ?loc
+      (strbrk "Found " ++ Id.print x ++ strbrk " matching " ++ Id.print y ++
+       strbrk " while " ++ Id.print x' ++ strbrk " matching " ++ Id.print y' ++
+       strbrk " was first found.")
+
 let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b'
 
+let mem_recursive_pair (x,y) l = List.mem_f (pair_equal Id.equal Id.equal) (x,y) l
+
 type recursive_pattern_kind =
-| RecursiveTerms of bool (* associativity *)
-| RecursiveBinders of bool (* associativity *) * glob_constr * glob_constr
+| RecursiveTerms of bool (* in reverse order *)
+| RecursiveBinders of bool (* in reverse order *)
 
-let compare_recursive_parts found f f' (iterator,subc) =
+let compare_recursive_parts recvars found f f' (iterator,subc) =
   let diff = ref None in
   let terminator = ref None in
   let rec aux c1 c2 = match DAst.get c1, DAst.get c2 with
@@ -276,32 +288,41 @@ let compare_recursive_parts found f f' (iterator,subc) =
       List.for_all2eq aux l1 l2
     | _ -> mk_glob_constr_eq aux c1 c2
     end
-  | GVar x, GVar y when not (Id.equal x y) ->
+  | GVar x, GVar y
+        when mem_recursive_pair (x,y) recvars || mem_recursive_pair (y,x) recvars ->
       (* We found the position where it differs *)
-      let lassoc = match !terminator with None -> false | Some _ -> true in
-      let x,y = if lassoc then y,x else x,y in
+      let revert = mem_recursive_pair (y,x) recvars in
+      let x,y = if revert then y,x else x,y in
       begin match !diff with
       | None ->
-        let () = diff := Some (x, y, RecursiveTerms lassoc) in
+        let () = diff := Some (x, y, RecursiveTerms revert) in
+        true
+      | Some (x', y', RecursiveTerms revert')
+      | Some (x', y', RecursiveBinders revert') ->
+        check_pair_matching ?loc:c1.CAst.loc x y x' y' revert revert';
         true
-      | Some (x', y', RecursiveTerms lassoc')
-      | Some (x', y', RecursiveBinders (lassoc',_,_)) ->
-        Id.equal x x' && Id.equal y y' && lassoc = lassoc'
       end
   | 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) ->
+  | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term)
+        when mem_recursive_pair (x,y) recvars || mem_recursive_pair (y,x) recvars ->
       (* 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
+      check_is_hole x t_x;
+      check_is_hole y t_y;
+      let revert = mem_recursive_pair (y,x) recvars in
+      let x,y = if revert then y,x else x,y in
       begin match !diff with
       | None ->
-        let () = diff := Some (x, y, RecursiveBinders (lassoc,t_x,t_y)) in
+        let () = diff := Some (x, y, RecursiveBinders revert) in
         aux c term
-      | Some (x', y', RecursiveBinders (lassoc',_,_)) ->
-        Id.equal x x' && Id.equal y y' && lassoc = lassoc'
-      | Some (x', y', RecursiveTerms lassoc') ->
-        let () = diff := Some (x, y, RecursiveBinders (lassoc,t_x,t_y)) in
-        Id.equal x x' && Id.equal y y' && lassoc = lassoc'
+      | Some (x', y', RecursiveBinders revert') ->
+        check_pair_matching ?loc:c1.CAst.loc x y x' y' revert revert';
+        true
+      | Some (x', y', RecursiveTerms revert') ->
+        (* Recursive binders have precedence: they can be coerced to
+           terms but not reciprocally *)
+        check_pair_matching ?loc:c1.CAst.loc x y x' y' revert revert';
+        let () = diff := Some (x, y, RecursiveBinders revert) in
+        true
       end
   | _ ->
       mk_glob_constr_eq aux c1 c2 in
@@ -310,58 +331,36 @@ let compare_recursive_parts found f f' (iterator,subc) =
     | None ->
 	let loc1 = loc_of_glob_constr iterator in
 	let loc2 = loc_of_glob_constr (Option.get !terminator) in
-	(* Here, we would need a loc made of several parts ... *)
-	user_err ?loc:(subtract_loc loc1 loc2)
+        (* Here, we would need a loc made of several parts ... *)
+        user_err ?loc:(subtract_loc loc1 loc2)
           (str "Both ends of the recursive pattern are the same.")
-    | Some (x,y,RecursiveTerms lassoc) ->
-        let toadd,x,y,lassoc =
-          if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_term_vars ||
-             List.mem_f (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_binders_vars
-          then
-            None,x,y,lassoc
-          else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (!found).recursive_term_vars ||
-                  List.mem_f (pair_equal Id.equal Id.equal) (y,x) (!found).recursive_binders_vars
-          then
-            None,y,x,not lassoc
-          else
-            Some (x,y),x,y,lassoc in
-	let iterator =
-	  f' (if lassoc then iterator
-	      else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in
-	(* found variables have been collected by compare_constr *)
+    | Some (x,y,RecursiveTerms revert) ->
+        (* By arbitrary convention, we use the second variable of the pair
+           as the place-holder for the iterator *)
+        let iterator =
+          f' (if revert then iterator else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in
+        (* 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 (lassoc,t_x,t_y)) ->
-        let toadd,x,y,lassoc =
-          if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_term_vars ||
-             List.mem_f (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_binders_vars
-          then
-            None,x,y,lassoc
-          else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (!found).recursive_term_vars ||
-                  List.mem_f (pair_equal Id.equal Id.equal) (y,x) (!found).recursive_binders_vars
-          then
-            None,y,x,not lassoc
-          else
-            Some (x,y),x,y,lassoc in
-        let iterator = f' (if lassoc then iterator else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in
+                               recursive_term_vars = List.add_set (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_term_vars };
+        NList (x,y,iterator,f (Option.get !terminator),revert)
+    | Some (x,y,RecursiveBinders revert) ->
+        let iterator =
+          f' (if revert 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 = Option.fold_right (fun a l -> a::l) toadd (!found).recursive_binders_vars };
-        check_is_hole x t_x;
-        check_is_hole y t_y;
-        NBinderList (x,y,iterator,f (Option.get !terminator),lassoc)
+                               recursive_binders_vars = List.add_set (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_binders_vars };
+        NBinderList (x,y,iterator,f (Option.get !terminator),revert)
   else
     raise Not_found
 
-let notation_constr_and_vars_of_glob_constr a =
+let notation_constr_and_vars_of_glob_constr recvars a =
   let found = ref { vars = []; recursive_term_vars = []; recursive_binders_vars = [] } in
   let has_ltac = ref false in
   (* Turn a glob_constr into a notation_constr by first trying to find a recursive pattern *)
   let rec aux c =
     let keepfound = !found in
     (* n^2 complexity but small and done only once per notation *)
-    try compare_recursive_parts found aux aux' (split_at_recursive_part c)
+    try compare_recursive_parts recvars found aux aux' (split_at_recursive_part c)
     with Not_found ->
     found := keepfound;
     match DAst.get c with
@@ -449,7 +448,7 @@ let check_variables_and_reversibility nenv
       else injective := x :: !injective
   in
   let check_pair s x y where =
-    if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then
+    if not (mem_recursive_pair (x,y) where) then
       user_err  (strbrk "in the right-hand side, " ++ Id.print x ++
 	str " and " ++ Id.print y ++ strbrk " should appear in " ++ str s ++
 	str " position as part of a recursive pattern.") in
@@ -470,7 +469,8 @@ let check_variables_and_reversibility nenv
   List.rev !injective
 
 let notation_constr_of_glob_constr nenv a =
-  let a, found, has_ltac = notation_constr_and_vars_of_glob_constr a in
+  let recvars = Id.Map.bindings nenv.ninterp_rec_vars in
+  let a, found, has_ltac = notation_constr_and_vars_of_glob_constr recvars a in
   let injective = check_variables_and_reversibility nenv found in
   let status = if has_ltac then HasLtac else match injective with
   | [] -> APrioriReversible
@@ -948,28 +948,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 lassoc = DAst.(with_loc_val (fun ?loc -> function
+let rec match_iterated_binders islambda decls bi revert = 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 lassoc
+      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b revert
     | _, _ when islambda ->
-      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b lassoc
+      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b revert
     | _ -> (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 lassoc
+      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b revert
     | Name _, _ when not islambda ->
-      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b lassoc
+      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b revert
     | _ -> (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 lassoc
+        ((DAst.make ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b revert
   | b -> (decls, DAst.make ?loc b)
   )) bi
 
@@ -983,7 +983,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 lassoc =
+let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin revert =
   let rec aux sigma bl rest =
     try
       let metas = add_ldots_var (add_meta_bindinglist y metas) in
@@ -999,13 +999,13 @@ let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin las
     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 bl = if revert 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
 
 let add_meta_term x metas = (x,((None,[]),NtnTypeConstr))::metas
 
-let match_termlist match_fun alp metas sigma rest x y iter termin lassoc =
+let match_termlist match_fun alp metas sigma rest x y iter termin revert =
   let rec aux sigma acc rest =
     try
       let metas = add_ldots_var (add_meta_term y metas) in
@@ -1017,7 +1017,7 @@ let match_termlist match_fun alp metas sigma rest x y iter termin lassoc =
     with No_match when not (List.is_empty acc) ->
       acc, match_fun metas sigma rest termin in
   let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in
-  let l = if lassoc then l else List.rev l in
+  let l = if revert then l else List.rev l in
   if is_bindinglist_meta x metas then
     (* This is a recursive pattern for both bindings and terms; it is *)
     (* registered for binders *)
@@ -1060,49 +1060,49 @@ let rec match_ inner u alp metas sigma a1 a2 =
   | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 a1
 
   (* Matching recursive notations for terms *)
-  | r1, NList (x,y,iter,termin,lassoc) ->
-      match_termlist (match_hd u alp) alp metas sigma a1 x y iter termin lassoc
+  | r1, NList (x,y,iter,termin,revert) ->
+      match_termlist (match_hd u alp) alp metas sigma a1 x y iter termin revert
 
-  | GLambda (na1, bk, t1, b1), NBinderList (x,y,iter,termin,lassoc) ->
+  | GLambda (na1, bk, t1, b1), NBinderList (x,y,iter,termin,revert) ->
     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 lassoc in
+      let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 revert 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 lassoc in
+      let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 revert 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 lassoc
+      match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin revert
     end
 
-  | GProd (na1, bk, t1, b1), NBinderList (x,y,iter,termin,lassoc) ->
+  | GProd (na1, bk, t1, b1), NBinderList (x,y,iter,termin,revert) ->
     (* "∀ 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 lassoc in
+      let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 revert 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 lassoc in
+      let (decls,b) = match_iterated_binders false [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 revert 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 lassoc
+      match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin revert
     end
 
   (* Matching recursive notations for binders: general case *)
-  | _r, NBinderList (x,y,iter,termin,lassoc) ->
-       match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin lassoc
+  | _r, NBinderList (x,y,iter,termin,revert) ->
+       match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin revert
 
   (* Matching individual binders as part of a recursive pattern *)
   | GLambda (na1, bk, t1, b1), NLambda (na2, t2, b2) ->
@@ -1278,7 +1278,7 @@ let bind_env_cases_pattern (terms,x,termlists,y as sigma) var v =
     (* TODO: handle the case of multiple occs in different scopes *)
     (var,v)::terms,x,termlists,y
 
-let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc =
+let match_cases_pattern_list match_fun metas sigma rest x y iter termin revert =
   let rec aux sigma acc rest =
     try
       let metas = add_ldots_var (add_meta_term y metas) in
@@ -1290,7 +1290,7 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc =
     with No_match when not (List.is_empty acc) ->
       acc, match_fun metas sigma rest termin in
   let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in
-  (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists)
+  (terms,onlybinders,(x,if revert then l else List.rev l)::termlists, binderlists)
 
 let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 =
  match DAst.get a1, a2 with
@@ -1309,9 +1309,9 @@ let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 =
       else
 	let l1',more_args = Util.List.chop le2 l1 in
 	(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
-  | r1, NList (x,y,iter,termin,lassoc) ->
+  | r1, NList (x,y,iter,termin,revert) ->
       (match_cases_pattern_list (match_cases_pattern_no_more_args)
-	metas (terms,(),termlists,()) a1 x y iter termin lassoc),(0,[])
+        metas (terms,(),termlists,()) a1 x y iter termin revert),(0,[])
   | _ -> raise No_match
 
 and match_cases_pattern_no_more_args metas sigma a1 a2 =
-- 
cgit v1.2.3


From 34cf92821e03a2c6ce64c78c66a00624d0fe9c99 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 15 Aug 2017 14:55:44 +0200
Subject: In printing notations with "match", reasoning up to the order of
 clauses.

---
 interp/notation_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 602271bf62..e68e8dd97f 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1163,7 +1163,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
       let sigma = List.fold_left2
       (fun s (tm1,_) (tm2,_) ->
         match_in u alp metas s tm1 tm2) sigma tml1 tml2 in
-      List.fold_left2 (match_equations u alp metas) sigma eqnl1 eqnl2
+      List.fold_left2_set No_match (match_equations u alp metas) sigma eqnl1 eqnl2
   | GLetTuple (nal1,(na1,to1),b1,c1), NLetTuple (nal2,(na2,to2),b2,c2)
       when Int.equal (List.length nal1) (List.length nal2) ->
       let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in
-- 
cgit v1.2.3


From 84e3da72fc14b996b0a917c5b6f011df4b79ab86 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 15 Aug 2017 15:14:46 +0200
Subject: Preliminary steps before adding general support for patterns in
 notations.

Moving earlier functions which will be needed earlier.
---
 interp/notation_ops.ml | 60 +++++++++++++++++++++++++-------------------------
 1 file changed, 30 insertions(+), 30 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index e68e8dd97f..2a2b6fc911 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -708,6 +708,36 @@ let add_binding_env alp (terms,onlybinders,termlists,binderlists) var v =
 let add_bindinglist_env (terms,onlybinders,termlists,binderlists) x bl =
   (terms,onlybinders,termlists,(x,bl)::binderlists)
 
+let rec map_cases_pattern_name_left f = DAst.map (function
+  | PatVar na -> PatVar (f na)
+  | PatCstr (c,l,na) -> PatCstr (c,List.map_left (map_cases_pattern_name_left f) l,f na)
+  )
+
+let rec fold_cases_pattern_eq f x p p' =
+  let loc = p.CAst.loc in
+  match DAst.get p, DAst.get p' with
+  | PatVar na, PatVar na' -> let x,na = f x na na' in x, DAst.make ?loc @@ PatVar na
+  | PatCstr (c,l,na), PatCstr (c',l',na') when eq_constructor c c' ->
+     let x,l = fold_cases_pattern_list_eq f x l l' in
+     let x,na = f x na na' in
+     x, DAst.make ?loc @@ PatCstr (c,l,na)
+  | _ -> failwith "Not equal"
+
+and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with
+  | [], [] -> x, []
+  | p::pl, p'::pl' ->
+     let x, p = fold_cases_pattern_eq f x p p' in
+     let x, pl = fold_cases_pattern_list_eq f x pl pl' in
+     x, p :: pl
+  | _ -> assert false
+
+let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with
+| PatVar na1, PatVar na2 -> Name.equal na1 na2
+| PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) ->
+  eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
+  Name.equal na1 na2
+| _ -> false
+
 let rec pat_binder_of_term t = DAst.map (function
   | GVar id -> PatVar (Name id)
   | GApp (t, l) ->
@@ -790,36 +820,6 @@ let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var
         else (fst alp,(id1,id2)::snd alp),sigma
   with Not_found -> alp, add_binding_env alp sigma var v
 
-let rec map_cases_pattern_name_left f = DAst.map (function
-  | PatVar na -> PatVar (f na)
-  | PatCstr (c,l,na) -> PatCstr (c,List.map_left (map_cases_pattern_name_left f) l,f na)
-  )
-
-let rec fold_cases_pattern_eq f x p p' =
-  let loc = p.CAst.loc in
-  match DAst.get p, DAst.get p' with
-  | PatVar na, PatVar na' -> let x,na = f x na na' in x, DAst.make ?loc @@ PatVar na
-  | PatCstr (c,l,na), PatCstr (c',l',na') when eq_constructor c c' ->
-     let x,l = fold_cases_pattern_list_eq f x l l' in
-     let x,na = f x na na' in
-     x, DAst.make ?loc @@ PatCstr (c,l,na)
-  | _ -> failwith "Not equal"
-
-and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with
-  | [], [] -> x, []
-  | p::pl, p'::pl' ->
-     let x, p = fold_cases_pattern_eq f x p p' in
-     let x, pl = fold_cases_pattern_list_eq f x pl pl' in
-     x, p :: pl
-  | _ -> assert false
-
-let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with
-| PatVar na1, PatVar na2 -> Name.equal na1 na2
-| PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) ->
-  eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
-  Name.equal na1 na2
-| _ -> false
-
 let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) var bl =
   let bl = List.rev bl in
   try
-- 
cgit v1.2.3


From bfed8dcbe7f91ec65ae5e6d1c0a2f06ca7fa01f6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 15 Aug 2017 17:28:32 +0200
Subject: Preliminary work before extending support for binders in notations
 (binders shall be substitutable by arbitrary cases patterns).

Giving a proper status to the functions unifying different instance of
the same notation variable (up to alpha-renaming).

Note: The a priori change of semantics in "bind_binding_as_term_env"
which now apply renaming from "unify_id" (as it did in
"bind_bindinglist_as_term_env") should not have an effect since, as
the former comment said, this corresponds to a "Anonymous" case which
should not occur, since the term would have to be bound upwards.
---
 interp/notation_ops.ml | 215 +++++++++++++++++++++++++------------------------
 1 file changed, 111 insertions(+), 104 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 2a2b6fc911..4c4c73fab5 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -751,39 +751,111 @@ let rec pat_binder_of_term t = DAst.map (function
   | _ -> raise No_match
   ) t
 
+let unify_name_upto alp na na' =
+  match na, na' with
+  | Anonymous, na' -> alp, na'
+  | na, Anonymous -> alp, na
+  | Name id, Name id' ->
+     if Id.equal id id' then alp, na'
+     else (fst alp,(id,id')::snd alp), na'
+
+let unify_pat_upto alp p p' =
+  try fold_cases_pattern_eq unify_name_upto alp p p' with Failure _ -> raise No_match
+
+let unify_term alp v v' =
+  match DAst.get v, DAst.get v' with
+  | GHole _, _ -> v'
+  | _, GHole _ -> v
+  | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match
+
+let unify_opt_term alp v v' =
+  match v, v' with
+  | Some t, Some t' -> Some (unify_term alp t t')
+  | (Some _ as x), None | None, (Some _ as x) -> x
+  | None, None -> None
+
+let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match
+
+let unify_binder_upto alp b b' =
+  let loc, loc' = CAst.(b.loc, b'.loc) in
+  match DAst.get b, DAst.get b' with
+  | GLocalAssum (na,bk,t), GLocalAssum (na',bk',t') ->
+     let alp, na = unify_name_upto alp na na' in
+     alp, DAst.make ?loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t')
+  | GLocalDef (na,bk,c,t), GLocalDef (na',bk',c',t') ->
+     let alp, na = unify_name_upto alp na na' in
+     alp, DAst.make ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t')
+  | GLocalPattern ((p,ids),id,bk,t), GLocalPattern ((p',_),_,bk',t') ->
+     let alp, p = unify_pat_upto alp p p' in
+     alp, DAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t')
+  | _ -> raise No_match
+
+let rec unify_terms alp vl vl' =
+  match vl, vl' with
+  | [], [] -> []
+  | v :: vl, v' :: vl' -> unify_term alp v v' :: unify_terms alp vl vl'
+  | _ -> raise No_match
+
+let rec unify_binders_upto alp bl bl' =
+  match bl, bl' with
+  | [], [] -> alp, []
+  | b :: bl, b' :: bl' ->
+     let alp,b = unify_binder_upto alp b b' in
+     let alp,bl = unify_binders_upto alp bl bl' in
+     alp, b :: bl
+  | _ -> raise No_match
+
+let unify_id alp id na' =
+  match na' with
+  | Anonymous -> Name (rename_var (snd alp) id)
+  | Name id' ->
+     if Id.equal (rename_var (snd alp) id) id' then na' else raise No_match
+
+let unify_pat alp p p' =
+  if cases_pattern_eq (map_cases_pattern_name_left (Name.map (rename_var (snd alp))) p) p' then p'
+  else raise No_match
+
+let unify_term_binder alp c = DAst.(map (fun b' ->
+  match DAst.get c, b' with
+  | GVar id, GLocalAssum (na', bk', t') ->
+     GLocalAssum (unify_id alp id na', bk', t')
+  | _, GLocalPattern ((p',ids), id, bk', t') ->
+     let p = pat_binder_of_term c in
+     GLocalPattern ((unify_pat alp p p',ids), id, bk', t')
+  | _ -> raise No_match))
+
+let rec unify_terms_binders alp cl bl' =
+  match cl, bl' with
+  | [], [] -> []
+  | c :: cl, b' :: bl' ->
+     begin match DAst.get b' with
+     | GLocalDef ( _, _, _, t) -> unify_terms_binders alp cl bl'
+     | _ -> unify_term_binder alp c b' :: unify_terms_binders alp cl bl'
+     end
+  | _ -> raise No_match
+
 let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
   try
+    (* If already bound to a term, unify with the new term *)
     let v' = Id.List.assoc var terms in
-    match DAst.get v, DAst.get v' with
-    | GHole _, _ -> sigma
-    | _, GHole _ ->
-        let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in
-        add_env alp sigma var v
-    | _, _ ->
-        if glob_constr_eq (alpha_rename (snd alp) v) v' then sigma
-        else raise No_match
+    let v'' = unify_term alp v v' in
+    if v'' == v' then sigma else
+      let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in
+      add_env alp sigma var v
   with Not_found -> add_env alp sigma var v
 
 let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var vl =
   try
+    (* If already bound to a list of term, unify with the new terms *)
     let vl' = Id.List.assoc var termlists in
-    let unify_term v v' =
-      match DAst.get v, DAst.get v' with
-      | GHole _, _ -> v'
-      | _, GHole _ -> v
-      | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v' else raise No_match in
-    let rec unify vl vl' =
-      match vl, vl' with
-      | [], [] -> []
-      | v :: vl, v' :: vl' -> unify_term v v' :: unify vl vl'
-      | _ -> raise No_match in
-    let vl = unify vl vl' in
+    let vl = unify_terms alp vl vl' in
     let sigma = (terms,onlybinders,Id.List.remove_assoc var termlists,binderlists) in
     add_termlist_env alp sigma var vl
   with Not_found -> add_termlist_env alp sigma var vl
 
 let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
   try
+    (* If already bound to a term, unify the binder and the term *)
     match DAst.get (Id.List.assoc var terms) with
     | GVar id' ->
        (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
@@ -797,109 +869,44 @@ let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sig
 
 let bind_binding_as_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
   try
+    (* If already bound to a binder, unify the term and the binder *)
     let v' = Id.List.assoc var onlybinders in
-    match v' with
-    | Anonymous ->
-        (* Should not occur, since the term has to be bound upwards *)
-        let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
-        add_binding_env alp sigma var (Name id)
-    | Name id' ->
-        if Id.equal (rename_var (snd alp) id) id' then sigma else raise No_match
+    let v'' = unify_id alp id v' in
+    if v' == v'' then sigma
+    else
+      let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
+      add_binding_env alp sigma var v''
   with Not_found -> add_binding_env alp sigma var (Name id)
 
 let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
   try
+    (* If already bound to a binder possibly *)
+    (* generating an alpha-renaming from unifying the new binder *)
     let v' = Id.List.assoc var onlybinders in
-    match v, v' with
-    | Anonymous, _ -> alp, sigma
-    | _, Anonymous ->
-        let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
-        alp, add_binding_env alp sigma var v
-    | Name id1, Name id2 ->
-        if Id.equal id1 id2 then alp,sigma
-        else (fst alp,(id1,id2)::snd alp),sigma
+    let alp, v'' = unify_name_upto alp v v' in
+    if v' == v'' then alp, sigma
+    else
+      let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
+      alp, add_binding_env alp sigma var v
   with Not_found -> alp, add_binding_env alp sigma var v
 
 let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) var bl =
   let bl = List.rev bl in
   try
+    (* If already bound to a list of binders possibly *)
+    (* generating an alpha-renaming from unifying the new binders *)
     let bl' = Id.List.assoc var binderlists in
-    let unify_name alp na na' =
-      match na, na' with
-      | Anonymous, na' -> alp, na'
-      | na, Anonymous -> alp, na
-      | Name id, Name id' ->
-         if Id.equal id id' then alp, na'
-         else (fst alp,(id,id')::snd alp), na' in
-    let unify_pat alp p p' =
-      try fold_cases_pattern_eq unify_name alp p p' with Failure _ -> raise No_match in
-    let unify_term alp v v' =
-      match DAst.get v, DAst.get v' with
-      | GHole _, _ -> v'
-      | _, GHole _ -> v
-      | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in
-    let unify_opt_term alp v v' =
-      match v, v' with
-      | Some t, Some t' -> Some (unify_term alp t t')
-      | (Some _ as x), None | None, (Some _ as x) -> x
-      | None, None -> None in
-    let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in
-    let unify_binder alp b b' =
-      let loc, loc' = CAst.(b.loc, b'.loc) in
-      match DAst.get b, DAst.get b' with
-      | GLocalAssum (na,bk,t), GLocalAssum (na',bk',t') ->
-         let alp, na = unify_name alp na na' in
-         alp, DAst.make ?loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t')
-      | GLocalDef (na,bk,c,t), GLocalDef (na',bk',c',t') ->
-         let alp, na = unify_name alp na na' in
-         alp, DAst.make ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t')
-      | GLocalPattern ((p,ids),id,bk,t), GLocalPattern ((p',_),_,bk',t') ->
-         let alp, p = unify_pat alp p p' in
-         alp, DAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t')
-      | _ -> raise No_match in
-    let rec unify alp bl bl' =
-    match bl, bl' with
-    | [], [] -> alp, []
-    | b :: bl, b' :: bl' ->
-       let alp,b = unify_binder alp b b' in
-       let alp,bl = unify alp bl bl' in
-       alp, b :: bl
-    | _ -> raise No_match in
-    let alp, bl = unify alp bl bl' in
+    let alp, bl = unify_binders_upto alp bl bl' in
     let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in
     alp, add_bindinglist_env sigma var bl
   with Not_found ->
     alp, add_bindinglist_env sigma var bl
 
-let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) var cl =
+let bind_bindinglist_as_termlist_env alp (terms,onlybinders,termlists,binderlists) var cl =
   try
+    (* If already bound to a list of binders, unify the terms and binders *)
     let bl' = Id.List.assoc var binderlists in
-    let unify_id id na' =
-      match na' with
-      | Anonymous -> Name (rename_var (snd alp) id)
-      | Name id' ->
-         if Id.equal (rename_var (snd alp) id) id' then na' else raise No_match in
-    let unify_pat p p' =
-      if cases_pattern_eq (map_cases_pattern_name_left (Name.map (rename_var (snd alp))) p) p' then p'
-      else raise No_match in
-    let unify_term_binder c = DAst.(map (fun b' ->
-      match DAst.get c, b' with
-      | GVar id, GLocalAssum (na', bk', t') ->
-         GLocalAssum (unify_id id na', bk', t')
-      | _, GLocalPattern ((p',ids), id, bk', t') ->
-         let p = pat_binder_of_term c in
-         GLocalPattern ((unify_pat p p',ids), id, bk', t')
-      | _ -> raise No_match )) in
-    let rec unify cl bl' =
-    match cl, bl' with
-    | [], [] -> []
-    | c :: cl, b' :: bl' ->
-      begin match DAst.get b' with
-      | GLocalDef ( _, _, _, t) -> unify cl bl'
-      | _ -> unify_term_binder c b' :: unify cl bl'
-      end
-    | _ -> raise No_match in
-    let bl = unify cl bl' in
+    let bl = unify_terms_binders alp cl bl' in
     let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in
     add_bindinglist_env sigma var bl
   with Not_found ->
@@ -1021,7 +1028,7 @@ let match_termlist match_fun alp metas sigma rest x y iter termin revert =
   if is_bindinglist_meta x metas then
     (* This is a recursive pattern for both bindings and terms; it is *)
     (* registered for binders *)
-    bind_bindinglist_as_term_env alp sigma x l
+    bind_bindinglist_as_termlist_env alp sigma x l
   else
     bind_termlist_env alp sigma x l
 
-- 
cgit v1.2.3


From ecc5658d7efd3a79a6309be6440d1005d30e6285 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 15 Aug 2017 18:19:50 +0200
Subject: Preliminary work before adding general support for patterns in
 notations I.

Factorizing the place where the different form of extended binders
(i.e. possibly including the 'pat form) are matched.
---
 interp/notation_ops.ml | 46 ++++++++++++++++++++--------------------------
 1 file changed, 20 insertions(+), 26 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 4c4c73fab5..9d338b27f8 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1111,32 +1111,6 @@ let rec match_ inner u alp metas sigma a1 a2 =
   | _r, NBinderList (x,y,iter,termin,revert) ->
        match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin revert
 
-  (* Matching individual binders as part of a recursive pattern *)
-  | GLambda (na1, bk, t1, b1), NLambda (na2, t2, b2) ->
-    begin match na1, DAst.get b1, na2 with
-    | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id
-      when is_gvar p e && is_bindinglist_meta id metas && not (occur_glob_constr p b1) ->
-      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] in
-      match_in u alp metas sigma b1 b2
-    | _, _, Name id when is_bindinglist_meta id metas ->
-      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] in
-      match_in u alp metas sigma b1 b2
-    | _ ->
-      match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
-    end
-  | GProd (na1, bk, t1, b1), NProd (na2, t2, b2) ->
-    begin match na1, DAst.get b1, na2 with
-    | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id
-      when is_gvar p e && is_bindinglist_meta id metas && not (occur_glob_constr p b1) ->
-      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] in
-      match_in u alp metas sigma b1 b2
-    | _, _, Name id when is_bindinglist_meta id metas && na1 != Anonymous ->
-      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] in
-      match_in u alp metas sigma b1 b2
-    | _ ->
-      match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
-    end
-
   (* Matching compositionally *)
   | GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
   | GRef (r1,_), NRef r2 when (eq_gr r1 r2) -> sigma
@@ -1151,6 +1125,10 @@ let rec match_ inner u alp metas sigma a1 a2 =
       let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in
       List.fold_left2 (match_ may_use_eta u alp metas)
         (match_in 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
+  | 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
   | 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
@@ -1236,9 +1214,25 @@ and match_in u = match_ true u
 and match_hd u = match_ false u
 
 and match_binders u alp metas na1 na2 sigma b1 b2 =
+  (* Match binders which cannot be substituted by a pattern *)
   let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
   match_in u alp metas sigma b1 b2
 
+and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
+  (* Match binders which can be substituted by a pattern *)
+  match na1, DAst.get b1, na2 with
+  (* Matching individual binders as part of a recursive pattern *)
+  | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id
+       when is_gvar p e && is_bindinglist_meta id metas && not (occur_glob_constr p b1) ->
+     let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in
+     match_in u alp metas sigma b1 b2
+  | _, _, Name id when is_bindinglist_meta id metas && (not isprod || na1 != Anonymous)->
+      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t)] in
+      match_in u alp metas sigma b1 b2
+  | _, _, _ ->
+     let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
+     match_in u alp metas sigma b1 b2
+
 and match_equations u alp metas sigma (_,(_,patl1,rhs1)) (patl2,rhs2) =
   (* patl1 and patl2 have the same length because they respectively
      correspond to some tml1 and tml2 that have the same length *)
-- 
cgit v1.2.3


From e21f70cc2b284a3cf489b16e0251492fb864cf1e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 18 Aug 2017 09:50:17 +0200
Subject: Preliminary work before adding general support for patterns in
 notations II.

Reordering the maps for binders and terms while uninterpreting a
notation the same way it will be at the time of interpreting a
notation.
---
 interp/notation_ops.ml | 72 +++++++++++++++++++++++++-------------------------
 1 file changed, 36 insertions(+), 36 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 9d338b27f8..9ea52821c1 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -666,7 +666,7 @@ let alpha_rename alpmetas v =
   if alpmetas == [] then v
   else try rename_glob_vars alpmetas v with UnsoundRenaming -> raise No_match
 
-let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v =
+let add_env (alp,alpmetas) (terms,termlists,binders,binderlists) var v =
   (* Check that no capture of binding variables occur *)
   (* [alp] is used when matching a pattern "fun x => ... x ... ?var ... x ..."
      with an actual term "fun z => ... z ..." when "x" is not bound in the
@@ -694,19 +694,19 @@ let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v =
      refinement *)
   let v = alpha_rename alpmetas v in
   (* TODO: handle the case of multiple occs in different scopes *)
-  ((var,v)::terms,onlybinders,termlists,binderlists)
+  ((var,v)::terms,termlists,binders,binderlists)
 
-let add_termlist_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var vl =
+let add_termlist_env (alp,alpmetas) (terms,termlists,binders,binderlists) var vl =
   if List.exists (fun (id,_) -> List.exists (occur_glob_constr id) vl) alp then raise No_match;
   let vl = List.map (alpha_rename alpmetas) vl in
-  (terms,onlybinders,(var,vl)::termlists,binderlists)
+  (terms,(var,vl)::termlists,binders,binderlists)
 
-let add_binding_env alp (terms,onlybinders,termlists,binderlists) var v =
+let add_binding_env alp (terms,termlists,binders,binderlists) var v =
   (* TODO: handle the case of multiple occs in different scopes *)
-  (terms,(var,v)::onlybinders,termlists,binderlists)
+  (terms,termlists,(var,v)::binders,binderlists)
 
-let add_bindinglist_env (terms,onlybinders,termlists,binderlists) x bl =
-  (terms,onlybinders,termlists,(x,bl)::binderlists)
+let add_bindinglist_env (terms,termlists,binders,binderlists) x bl =
+  (terms,termlists,binders,(x,bl)::binderlists)
 
 let rec map_cases_pattern_name_left f = DAst.map (function
   | PatVar na -> PatVar (f na)
@@ -834,26 +834,26 @@ let rec unify_terms_binders alp cl bl' =
      end
   | _ -> raise No_match
 
-let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
+let bind_term_env alp (terms,termlists,binders,binderlists as sigma) var v =
   try
     (* If already bound to a term, unify with the new term *)
     let v' = Id.List.assoc var terms in
     let v'' = unify_term alp v v' in
     if v'' == v' then sigma else
-      let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in
+      let sigma = (Id.List.remove_assoc var terms,termlists,binders,binderlists) in
       add_env alp sigma var v
   with Not_found -> add_env alp sigma var v
 
-let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var vl =
+let bind_termlist_env alp (terms,termlists,binders,binderlists as sigma) var vl =
   try
     (* If already bound to a list of term, unify with the new terms *)
     let vl' = Id.List.assoc var termlists in
     let vl = unify_terms alp vl vl' in
-    let sigma = (terms,onlybinders,Id.List.remove_assoc var termlists,binderlists) in
+    let sigma = (terms,Id.List.remove_assoc var termlists,binders,binderlists) in
     add_termlist_env alp sigma var vl
   with Not_found -> add_termlist_env alp sigma var vl
 
-let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
+let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) var id =
   try
     (* If already bound to a term, unify the binder and the term *)
     match DAst.get (Id.List.assoc var terms) with
@@ -867,47 +867,47 @@ let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sig
     (* TODO: look at the consequences for alp *)
     alp, add_env alp sigma var (DAst.make @@ GVar id)
 
-let bind_binding_as_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
+let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var id =
   try
     (* If already bound to a binder, unify the term and the binder *)
-    let v' = Id.List.assoc var onlybinders in
+    let v' = Id.List.assoc var binders in
     let v'' = unify_id alp id v' in
     if v' == v'' then sigma
     else
-      let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
+      let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in
       add_binding_env alp sigma var v''
   with Not_found -> add_binding_env alp sigma var (Name id)
 
-let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
+let bind_binding_env alp (terms,termlists,binders,binderlists as sigma) var v =
   try
     (* If already bound to a binder possibly *)
     (* generating an alpha-renaming from unifying the new binder *)
-    let v' = Id.List.assoc var onlybinders in
+    let v' = Id.List.assoc var binders in
     let alp, v'' = unify_name_upto alp v v' in
     if v' == v'' then alp, sigma
     else
-      let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
+      let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in
       alp, add_binding_env alp sigma var v
   with Not_found -> alp, add_binding_env alp sigma var v
 
-let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) var bl =
+let bind_bindinglist_env alp (terms,termlists,binders,binderlists as sigma) var bl =
   let bl = List.rev bl in
   try
     (* If already bound to a list of binders possibly *)
     (* generating an alpha-renaming from unifying the new binders *)
     let bl' = Id.List.assoc var binderlists in
     let alp, bl = unify_binders_upto alp bl bl' in
-    let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in
+    let sigma = (terms,termlists,binders,Id.List.remove_assoc var binderlists) in
     alp, add_bindinglist_env sigma var bl
   with Not_found ->
     alp, add_bindinglist_env sigma var bl
 
-let bind_bindinglist_as_termlist_env alp (terms,onlybinders,termlists,binderlists) var cl =
+let bind_bindinglist_as_termlist_env alp (terms,termlists,binders,binderlists) var cl =
   try
     (* If already bound to a list of binders, unify the terms and binders *)
     let bl' = Id.List.assoc var binderlists in
     let bl = unify_terms_binders alp cl bl' in
-    let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in
+    let sigma = (terms,termlists,binders,Id.List.remove_assoc var binderlists) in
     add_bindinglist_env sigma var bl
   with Not_found ->
     anomaly (str "There should be a binder list bindings this list of terms.")
@@ -980,11 +980,11 @@ let rec match_iterated_binders islambda decls bi revert = DAst.(with_loc_val (fu
   | b -> (decls, DAst.make ?loc b)
   )) bi
 
-let remove_sigma x (terms,onlybinders,termlists,binderlists) =
-  (Id.List.remove_assoc x terms,onlybinders,termlists,binderlists)
+let remove_sigma x (terms,termlists,binders,binderlists) =
+  (Id.List.remove_assoc x terms,termlists,binders,binderlists)
 
-let remove_bindinglist_sigma x (terms,onlybinders,termlists,binderlists) =
-  (terms,onlybinders,termlists,Id.List.remove_assoc x binderlists)
+let remove_bindinglist_sigma x (terms,termlists,binders,binderlists) =
+  (terms,termlists,binders,Id.List.remove_assoc x binderlists)
 
 let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas
 
@@ -1023,7 +1023,7 @@ let match_termlist match_fun alp metas sigma rest x y iter termin revert =
       aux sigma (t::acc) rest
     with No_match when not (List.is_empty acc) ->
       acc, match_fun metas sigma rest termin in
-  let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in
+  let l,(terms,termlists,binders,binderlists as sigma) = aux sigma [] rest in
   let l = if revert then l else List.rev l in
   if is_bindinglist_meta x metas then
     (* This is a recursive pattern for both bindings and terms; it is *)
@@ -1246,7 +1246,7 @@ let term_of_binder bi = DAst.make @@ match bi with
   | Anonymous -> GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
 
 let match_notation_constr u c (metas,pat) =
-  let terms,binders,termlists,binderlists =
+  let terms,termlists,binders,binderlists =
     match_ false u ([],[]) metas ([],[],[],[]) c pat in
   (* Reorder canonically the substitution *)
   let find_binder x =
@@ -1290,10 +1290,10 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin revert =
       aux sigma (t::acc) rest
     with No_match when not (List.is_empty acc) ->
       acc, match_fun metas sigma rest termin in
-  let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in
-  (terms,onlybinders,(x,if revert then l else List.rev l)::termlists, binderlists)
+  let l,(terms,termlists,binders,binderlists as sigma) = aux sigma [] rest in
+  (terms,(x,if revert then l else List.rev l)::termlists,binders,binderlists)
 
-let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 =
+let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
  match DAst.get a1, a2 with
   | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[])
   | PatVar Anonymous, NHole _ -> sigma,(0,[])
@@ -1309,10 +1309,10 @@ let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 =
 	raise No_match
       else
 	let l1',more_args = Util.List.chop le2 l1 in
-	(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
+        (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
   | r1, NList (x,y,iter,termin,revert) ->
       (match_cases_pattern_list (match_cases_pattern_no_more_args)
-        metas (terms,(),termlists,()) a1 x y iter termin revert),(0,[])
+        metas (terms,termlists,(),()) a1 x y iter termin revert),(0,[])
   | _ -> raise No_match
 
 and match_cases_pattern_no_more_args metas sigma a1 a2 =
@@ -1345,9 +1345,9 @@ let reorder_canonically_substitution terms termlists metas =
     metas ([],[])
 
 let match_notation_constr_cases_pattern c (metas,pat) =
-  let (terms,(),termlists,()),more_args = match_cases_pattern metas ([],(),[],()) c pat in
+  let (terms,termlists,(),()),more_args = match_cases_pattern metas ([],[],(),()) c pat in
   reorder_canonically_substitution terms termlists metas, more_args
 
 let match_notation_constr_ind_pattern ind args (metas,pat) =
-  let (terms,(),termlists,()),more_args = match_ind_pattern metas ([],(),[],()) ind args pat in
+  let (terms,termlists,(),()),more_args = match_ind_pattern metas ([],[],(),()) ind args pat in
   reorder_canonically_substitution terms termlists metas, more_args
-- 
cgit v1.2.3


From 398358618bb3eabfe822b79c669703c1c33b67e6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 15 Aug 2017 18:32:02 +0200
Subject: Adding patterns in the category of binders for notations.

For instance, the following is now possible:

  Check {(x,y)|x+y=0}.

Some questions remains. Maybe, by consistency, the notation should be
"{'(x,y)|x+y=0}"...
---
 interp/notation_ops.ml | 89 ++++++++++++++++++++++++++++++--------------------
 1 file changed, 53 insertions(+), 36 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 9ea52821c1..3a3d4ffa8b 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -103,9 +103,13 @@ let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na
 
 let rec cases_pattern_fold_map ?loc g e = DAst.with_val (function
   | PatVar na ->
-      let e',na' = g e na in e', DAst.make ?loc @@ PatVar na'
+      let e',pat,na' = g e na in
+      e', (match pat with
+      | None -> DAst.make ?loc @@ PatVar na'
+      | Some ((_,pat),_) -> pat)
   | PatCstr (cstr,patl,na) ->
-      let e',na' = g e na in
+      let e',pat,na' = g e na in
+      if pat <> None then user_err (Pp.str "Unable to instantiate an \"as\" clause with a pattern.");
       let e',patl' = List.fold_left_map (cases_pattern_fold_map ?loc g) e patl in
       e', DAst.make ?loc @@ PatCstr (cstr,patl',na')
   )
@@ -136,6 +140,16 @@ let rec subst_glob_vars l gc = DAst.map (function
 
 let ldots_var = Id.of_string ".."
 
+let protect g e na =
+  let e',pat,na = g e na in
+  if pat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern.");
+  e',na
+
+let apply_cases_pattern ?loc ((ids,pat),id) c =
+  let tm = DAst.make ?loc (GVar id) in
+  DAst.make ?loc @@
+    GCases (LetPatternStyle, None, [tm,(Anonymous,None)], [loc,(ids,[pat], c)])
+
 let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
   let lt x = DAst.make ?loc x in lt @@ match nc with
   | NVar id -> GVar id
@@ -153,39 +167,43 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
       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)
+      let e',pat,na = g e na in GLambda (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) pat (f e' c))
   | NProd (na,ty,c) ->
-      let e',na = g e na in GProd (na,Explicit,f e ty,f e' c)
+      let e',pat,na = g e na in GProd (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) pat (f e' c))
   | NLetIn (na,b,t,c) ->
-      let e',na = g e na in GLetIn (na,f e b,Option.map (f e) t,f e' c)
+      let e',pat,na = g e na in
+      (match pat with
+       | None -> GLetIn (na,f e b,Option.map (f e) t,f e' c)
+       | Some pat -> DAst.get (apply_cases_pattern ?loc pat (f e' c)))
   | NCases (sty,rtntypopt,tml,eqnl) ->
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
 	let e',t' = match t with
 	| None -> e',None
 	| Some (ind,nal) ->
 	  let e',nal' = List.fold_right (fun na (e',nal) ->
-	      let e',na' = g e' na in e',na'::nal) nal (e',[]) in
+              let e',na' = protect g e' na in
+              e',na'::nal) nal (e',[]) in
 	  e',Some (Loc.tag ?loc (ind,nal')) in
-	let e',na' = g e' na 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,na) = g e na in ((Name.cons na idl,e),na) in
+      let fold (idl,e) na = let (e,pat,na) = g e na in ((Name.cons na idl,e),pat,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
 	Loc.tag (idl,patl,f e rhs)) eqnl in
       GCases (sty,Option.map (f e') rtntypopt,tml',eqnl')
   | NLetTuple (nal,(na,po),b,c) ->
-      let e',nal = List.fold_left_map g e nal in
-      let e'',na = g e na in
+      let e',nal = List.fold_left_map (protect g) e nal in
+      let e'',na = protect g e na in
       GLetTuple (nal,(na,Option.map (f e'') po),f e b,f e' c)
   | NIf (c,(na,po),b1,b2) ->
-      let e',na = g e na in
+      let e',na = protect g e na in
       GIf (f e c,(na,Option.map (f e') po),f e b1,f e b2)
   | NRec (fk,idl,dll,tl,bl) ->
-      let e,dll = Array.fold_left_map (List.fold_left_map (fun e (na,oc,b) ->
-	  let e,na = g e na in
+      let e,dll = Array.fold_left_map (List.fold_map (fun e (na,oc,b) ->
+          let e,na = protect g e na in
 	  (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
-      let e',idl = Array.fold_left_map (to_id g) e idl in
+      let e',idl = Array.fold_left_map (to_id (protect g)) e idl in
       GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
   | NCast (c,k) -> GCast (f e c,Miscops.map_cast_type (f e) k)
   | NSort x -> GSort x
@@ -195,7 +213,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
 
 let glob_constr_of_notation_constr ?loc x =
   let rec aux () x =
-    glob_constr_of_notation_constr_with_binders ?loc (fun () id -> ((),id)) aux () x
+    glob_constr_of_notation_constr_with_binders ?loc (fun () id -> ((),None,id)) aux () x
   in aux () x
 
 (******************************************************************************)
@@ -867,28 +885,27 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
     (* TODO: look at the consequences for alp *)
     alp, add_env alp sigma var (DAst.make @@ GVar id)
 
-let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var id =
+let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c =
+  let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in
   try
     (* If already bound to a binder, unify the term and the binder *)
-    let v' = Id.List.assoc var binders in
-    let v'' = unify_id alp id v' in
-    if v' == v'' then sigma
+    let pat' = Id.List.assoc var binders in
+    let pat'' = unify_pat alp pat pat' in
+    if pat' == pat'' then sigma
     else
       let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in
-      add_binding_env alp sigma var v''
-  with Not_found -> add_binding_env alp sigma var (Name id)
+      add_binding_env alp sigma var pat''
+  with Not_found -> add_binding_env alp sigma var pat
 
-let bind_binding_env alp (terms,termlists,binders,binderlists as sigma) var v =
+let bind_binding_env alp (terms,termlists,binders,binderlists as sigma) var pat =
   try
     (* If already bound to a binder possibly *)
     (* generating an alpha-renaming from unifying the new binder *)
-    let v' = Id.List.assoc var binders in
-    let alp, v'' = unify_name_upto alp v v' in
-    if v' == v'' then alp, sigma
-    else
-      let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in
-      alp, add_binding_env alp sigma var v
-  with Not_found -> alp, add_binding_env alp sigma var v
+    let pat' = Id.List.assoc var binders in
+    let alp, pat = unify_pat_upto alp pat pat' in
+    let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in
+    alp, add_binding_env alp sigma var pat
+  with Not_found -> alp, add_binding_env alp sigma var pat
 
 let bind_bindinglist_env alp (terms,termlists,binders,binderlists as sigma) var bl =
   let bl = List.rev bl in
@@ -932,7 +949,7 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
 
 let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
   | (na1,Name id2) when is_onlybinding_meta id2 metas ->
-      bind_binding_env alp sigma id2 na1
+      bind_binding_env alp sigma id2 (DAst.make (PatVar na1))
   | (Name id1,Name id2) when is_term_meta id2 metas ->
       (* We let the non-binding occurrence define the rhs and hence reason up to *)
       (* alpha-conversion for the given occurrence of the name (see #4592)) *)
@@ -1063,7 +1080,7 @@ 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
-  | GVar id1, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 id1
+  | r1, 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
 
   (* Matching recursive notations for terms *)
@@ -1226,6 +1243,10 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
        when is_gvar p e && is_bindinglist_meta id metas && not (occur_glob_constr p b1) ->
      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in
      match_in u alp metas sigma b1 b2
+  | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(_,[cp],b1))]), Name id
+       when is_gvar p e && is_onlybinding_meta id metas && not (occur_glob_constr p b1) ->
+     let alp,sigma = bind_binding_env alp sigma id cp in
+     match_in u alp metas sigma b1 b2
   | _, _, Name id when is_bindinglist_meta id metas && (not isprod || na1 != Anonymous)->
       let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t)] in
       match_in u alp metas sigma b1 b2
@@ -1241,16 +1262,12 @@ and match_equations u alp metas sigma (_,(_,patl1,rhs1)) (patl2,rhs2) =
       (alp,sigma) patl1 patl2 in
   match_in u alp metas sigma rhs1 rhs2
 
-let term_of_binder bi = DAst.make @@ match bi with
-  | Name id -> GVar id
-  | Anonymous -> GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
-
 let match_notation_constr u c (metas,pat) =
   let terms,termlists,binders,binderlists =
     match_ false u ([],[]) metas ([],[],[],[]) c pat in
   (* Reorder canonically the substitution *)
   let find_binder x =
-    try term_of_binder (Id.List.assoc x binders)
+    try glob_constr_of_cases_pattern (Id.List.assoc x binders)
     with Not_found ->
       (* Happens for binders bound to Anonymous *)
       (* Find a better way to propagate Anonymous... *)
-- 
cgit v1.2.3


From edd0d22429354a5f2c703a8c7bd1f775e2f97d9e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 12 Aug 2017 09:15:40 +0200
Subject: Adding support for parsing subterms of a notation as "pattern".

This allows in particular to define notations with 'pat style binders.

E.g.:

A non-trivial change in this commit is storing binders and patterns
separately from terms.

This is not strictly necessary but has some advantages.

However, it is relatively common to have binders also used as terms,
or binders parsed as terms. Thus, it is already relatively common to
embed binders into terms (see e.g. notation for ETA in output test
Notations3.v) or to coerce terms to idents (see e.g. the notation for
{x|P} where x is parsed as a constr).

So, it is as simple to always store idents (and eventually patterns)
as terms.
---
 interp/notation_ops.ml | 46 ++++++++++++++++++++++++----------------------
 1 file changed, 24 insertions(+), 22 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 3a3d4ffa8b..ec568823e3 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -472,17 +472,16 @@ let check_variables_and_reversibility nenv
 	str " position as part of a recursive pattern.") in
   let check_type x typ =
     match typ with
-    | NtnInternTypeConstr ->
+    | NtnInternTypeAny ->
 	begin
 	  try check_pair "term" x (Id.Map.find x recvars) foundrec
 	  with Not_found -> check_bound x
 	end
-    | NtnInternTypeBinder ->
+    | NtnInternTypeOnlyBinder ->
 	begin
 	  try check_pair "binding" x (Id.Map.find x recvars) foundrecbinding
 	  with Not_found -> check_bound x
-	end
-    | NtnInternTypeIdent -> check_bound x in
+        end in
   Id.Map.iter check_type vars;
   List.rev !injective
 
@@ -665,7 +664,7 @@ let is_term_meta id metas =
   with Not_found -> false
 
 let is_onlybinding_meta id metas =
-  try match Id.List.assoc id metas with _,NtnTypeOnlyBinder -> true | _ -> false
+  try match Id.List.assoc id metas with _,NtnTypeBinder _ -> true | _ -> false
   with Not_found -> false
 
 let is_bindinglist_meta id metas =
@@ -885,8 +884,11 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
     (* TODO: look at the consequences for alp *)
     alp, add_env alp sigma var (DAst.make @@ GVar id)
 
+let force_cases_pattern c =
+  DAst.make ?loc:c.CAst.loc (DAst.get c)
+
 let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c =
-  let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in
+  let pat = try force_cases_pattern (cases_pattern_of_glob_constr Anonymous c) with Not_found -> raise No_match in
   try
     (* If already bound to a binder, unify the term and the binder *)
     let pat' = Id.List.assoc var binders in
@@ -961,8 +963,10 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
   | (Anonymous,Anonymous) -> alp,sigma
   | _ -> raise No_match
 
-let rec match_cases_pattern_binders metas acc pat1 pat2 =
+let rec match_cases_pattern_binders metas (alp,sigma as acc) pat1 pat2 =
   match DAst.get pat1, DAst.get pat2 with
+  | _, PatVar (Name id2) when is_onlybinding_meta id2 metas ->
+      bind_binding_env alp sigma id2 pat1
   | PatVar na1, PatVar na2 -> match_names metas acc na1 na2
   | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2)
       when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) ->
@@ -1265,26 +1269,24 @@ and match_equations u alp metas sigma (_,(_,patl1,rhs1)) (patl2,rhs2) =
 let match_notation_constr u c (metas,pat) =
   let terms,termlists,binders,binderlists =
     match_ false u ([],[]) metas ([],[],[],[]) c pat in
-  (* Reorder canonically the substitution *)
-  let find_binder x =
-    try glob_constr_of_cases_pattern (Id.List.assoc x binders)
-    with Not_found ->
-      (* Happens for binders bound to Anonymous *)
-      (* Find a better way to propagate Anonymous... *)
-      DAst.make @@GVar x in
-  List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') ->
+  (* Turning substitution based on binding/constr distinction into a
+     substitution based on entry productions *)
+  List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders',binderlists') ->
     match typ with
     | NtnTypeConstr ->
       let term = try Id.List.assoc x terms with Not_found -> raise No_match in
-       ((term, scl)::terms',termlists',binders')
-    | NtnTypeOnlyBinder ->
-       ((find_binder x, scl)::terms',termlists',binders')
+       ((term, scl)::terms',termlists',binders',binderlists')
+    | NtnTypeBinder true ->
+       let v = glob_constr_of_cases_pattern (Id.List.assoc x binders) in
+       ((v,scl)::terms',termlists',binders',binderlists')
+    | NtnTypeBinder false ->
+       (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists')
     | NtnTypeConstrList ->
-       (terms',(Id.List.assoc x termlists,scl)::termlists',binders')
+       (terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists')
     | NtnTypeBinderList ->
       let bl = try Id.List.assoc x binderlists with Not_found -> raise No_match in
-       (terms',termlists',(bl, scl)::binders'))
-    metas ([],[],[])
+       (terms',termlists',binders',(bl, scl)::binderlists'))
+    metas ([],[],[],[])
 
 (* Matching cases pattern *)
 
@@ -1356,7 +1358,7 @@ let reorder_canonically_substitution terms termlists metas =
   List.fold_right (fun (x,(scl,typ)) (terms',termlists') ->
     match typ with
       | NtnTypeConstr -> ((Id.List.assoc x terms, scl)::terms',termlists')
-      | NtnTypeOnlyBinder -> assert false
+      | NtnTypeBinder _ -> assert false
       | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists')
       | NtnTypeBinderList -> assert false)
     metas ([],[])
-- 
cgit v1.2.3


From 3a6b1d2c04ceeb568accbc9ddfc3fc0f14faf25b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 17 Aug 2017 12:35:56 +0200
Subject: Respecting the ident/pattern distinction in notation modifiers.

---
 interp/notation_ops.ml | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index ec568823e3..b7c1d84f13 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -667,6 +667,10 @@ 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
+  with Not_found -> false
+
 let is_bindinglist_meta id metas =
   try match Id.List.assoc id metas with _,NtnTypeBinderList -> true | _ -> false
   with Not_found -> false
@@ -965,7 +969,7 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
 
 let rec match_cases_pattern_binders metas (alp,sigma as acc) pat1 pat2 =
   match DAst.get pat1, DAst.get pat2 with
-  | _, PatVar (Name id2) when is_onlybinding_meta id2 metas ->
+  | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta id2 metas ->
       bind_binding_env alp sigma id2 pat1
   | PatVar na1, PatVar na2 -> match_names metas acc na1 na2
   | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2)
@@ -1084,7 +1088,8 @@ 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_meta id2 metas -> bind_binding_as_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_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
 
   (* Matching recursive notations for terms *)
@@ -1248,7 +1253,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in
      match_in u alp metas sigma b1 b2
   | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(_,[cp],b1))]), Name id
-       when is_gvar p e && is_onlybinding_meta id metas && not (occur_glob_constr p b1) ->
+       when is_gvar p e && is_onlybinding_pattern_like_meta id metas && not (occur_glob_constr p b1) ->
      let alp,sigma = bind_binding_env alp sigma id cp in
      match_in u alp metas sigma b1 b2
   | _, _, Name id when is_bindinglist_meta id metas && (not isprod || na1 != Anonymous)->
@@ -1276,10 +1281,10 @@ 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 true ->
+    | NtnTypeBinder NtnParsedAsConstr ->
        let v = glob_constr_of_cases_pattern (Id.List.assoc x binders) in
        ((v,scl)::terms',termlists',binders',binderlists')
-    | NtnTypeBinder false ->
+    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern) ->
        (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists')
     | NtnTypeConstrList ->
        (terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists')
-- 
cgit v1.2.3


From bc73f267ad2da0f1e24e66cb481725be018a8ce6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 21 Aug 2017 23:25:21 +0200
Subject: A (significant) simplification in printing notations with recursive
 binders.

For historical reasons (this was one of the first examples of
notations with binders), there was a special treatment for notations
whose right-hand side had the form "forall x, P" or "fun x => P". Not
only this is not necessary, but this prevents notations binding to
expressions such as "forall x, x>0 -> P" to be used in printing.

We let the general case absorb this particular case.

We add the integration of "let x:=c in ..." in the middle of a
notation with recursive binders as part of the binder list, reprinting
it "(x:=c)" (this was formerly the case only for the above particular
case).

Note that integrating "let" in sequence of binders is stil not the
case for the regular "forall"/"fun". Should we?
---
 interp/notation_ops.ml | 80 +++++++-------------------------------------------
 1 file changed, 11 insertions(+), 69 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index b7c1d84f13..0480a93e27 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -975,36 +975,9 @@ let rec match_cases_pattern_binders metas (alp,sigma as acc) pat1 pat2 =
   | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2)
       when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) ->
       List.fold_left2 (match_cases_pattern_binders metas)
-	(match_names metas acc na1 na2) patl1 patl2
+        (match_names metas acc na1 na2) patl1 patl2
   | _ -> raise No_match
 
-let glue_letin_with_decls = true
-
-let rec match_iterated_binders islambda decls bi revert = 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 revert
-    | _, _ when islambda ->
-      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b revert
-    | _ -> (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 revert
-    | Name _, _ when not islambda ->
-      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b revert
-    | _ -> (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 revert
-  | b -> (decls, DAst.make ?loc b)
-  )) bi
-
 let remove_sigma x (terms,termlists,binders,binderlists) =
   (Id.List.remove_assoc x terms,termlists,binders,binderlists)
 
@@ -1015,7 +988,9 @@ 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 revert =
+let glue_letin_with_decls = true
+
+let match_binderlist match_fun alp metas sigma rest x y iter termin revert =
   let rec aux sigma bl rest =
     try
       let metas = add_ldots_var (add_meta_bindinglist y metas) in
@@ -1028,8 +1003,12 @@ let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin rev
       (* In case y is bound not only to a binder but also to a term *)
       let sigma = remove_sigma y sigma in
       aux sigma (b::bl) rest
-    with No_match when not (List.is_empty bl) ->
-      bl, rest, sigma in
+    with No_match ->
+    match DAst.get rest with
+    | GLetIn (na,c,t,rest) when glue_letin_with_decls ->
+       let b = DAst.make ?loc:rest.CAst.loc @@ GLocalDef (na,Explicit (*?*), c,t) in
+       aux sigma (b::bl) rest
+    | _ -> if not (List.is_empty bl) then bl, rest, sigma else raise No_match in
   let bl,rest,sigma = aux sigma [] rest in
   let bl = if revert then List.rev bl else bl in
   let alp,sigma = bind_bindinglist_env alp sigma x bl in
@@ -1096,46 +1075,9 @@ let rec match_ inner u alp metas sigma a1 a2 =
   | r1, NList (x,y,iter,termin,revert) ->
       match_termlist (match_hd u alp) alp metas sigma a1 x y iter termin revert
 
-  | GLambda (na1, bk, t1, b1), NBinderList (x,y,iter,termin,revert) ->
-    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 revert 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 revert 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 revert
-    end
-
-  | GProd (na1, bk, t1, b1), NBinderList (x,y,iter,termin,revert) ->
-    (* "∀ 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 revert 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 revert 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 revert
-    end
-
   (* Matching recursive notations for binders: general case *)
   | _r, NBinderList (x,y,iter,termin,revert) ->
-       match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin revert
+      match_binderlist (match_hd u) alp metas sigma a1 x y iter termin revert
 
   (* Matching compositionally *)
   | GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
-- 
cgit v1.2.3


From 15abe33f55b317410223bd48576fa35c81943ff9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 14 Feb 2018 19:55:21 +0100
Subject: Refining the strategy for glueing let-ins to a sequence of binders.

To deal with existing notations starting with a "let" (see notation
"for" in output/Notation2.v) we adopt the pragmatic approach of
glueing only inner let by default.

Ideally, it might be nicer to detect if there is an overlap of
notation, and not to glue only in case of overlap. We could also
decide that a notation starting with a "let" should always be
protected by some constant, say "id", so as to avoid possible
collisions, but this would require changes user side.
---
 interp/notation_ops.ml | 31 ++++++++++++++++++++++++-------
 1 file changed, 24 insertions(+), 7 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 0480a93e27..5fe12e5705 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -988,10 +988,18 @@ let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas
 
 let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas
 
-let glue_letin_with_decls = true
+(* This tells if letins in the middle of binders should be included in
+   the sequence of binders *)
+let glue_inner_letin_with_decls = true
+
+(* This tells if trailing letins (with no further proper binders)
+   should be included in sequence of binders *)
+let glue_trailing_letin_with_decls = false
+
+exception OnlyTrailingLetIns
 
 let match_binderlist match_fun alp metas sigma rest x y iter termin revert =
-  let rec aux sigma bl rest =
+  let rec aux trailing_letins sigma bl rest =
     try
       let metas = add_ldots_var (add_meta_bindinglist y metas) in
       let (terms,_,_,binderlists as sigma) = match_fun alp metas sigma rest iter in
@@ -1002,14 +1010,23 @@ let match_binderlist match_fun alp metas sigma rest x y iter termin revert =
       let sigma = remove_bindinglist_sigma y (remove_sigma ldots_var sigma) in
       (* In case y is bound not only to a binder but also to a term *)
       let sigma = remove_sigma y sigma in
-      aux sigma (b::bl) rest
+      aux false sigma (b::bl) rest
     with No_match ->
     match DAst.get rest with
-    | GLetIn (na,c,t,rest) when glue_letin_with_decls ->
+    | GLetIn (na,c,t,rest') when glue_inner_letin_with_decls ->
        let b = DAst.make ?loc:rest.CAst.loc @@ GLocalDef (na,Explicit (*?*), c,t) in
-       aux sigma (b::bl) rest
-    | _ -> if not (List.is_empty bl) then bl, rest, sigma else raise No_match in
-  let bl,rest,sigma = aux sigma [] rest in
+       (* collect let-in *)
+       (try aux true sigma (b::bl) rest'
+        with OnlyTrailingLetIns
+             when not (trailing_letins && not glue_trailing_letin_with_decls) ->
+         (* renounce to take into account trailing let-ins *)
+         if not (List.is_empty bl) then bl, rest, sigma else raise No_match)
+    | _ ->
+       if trailing_letins && not glue_trailing_letin_with_decls then
+         (* Backtrack to when we tried to glue letins *)
+         raise OnlyTrailingLetIns;
+       if not (List.is_empty bl) then bl, rest, sigma else raise No_match in
+  let bl,rest,sigma = aux false sigma [] rest in
   let bl = if revert 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
-- 
cgit v1.2.3


From 50970e4043d73d9a4fbd17ffe765745f6d726317 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 21 Aug 2017 23:01:04 +0200
Subject: Using an "as" clause when needed for printing irrefutable patterns.

Example which is now reprinted as parsed:

  fun '((x,y) as z) => (y,x)=z
---
 interp/notation_ops.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 5fe12e5705..c44863791e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1208,11 +1208,13 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
   match na1, DAst.get b1, na2 with
   (* Matching individual binders as part of a recursive pattern *)
   | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id
-       when is_gvar p e && is_bindinglist_meta id metas && not (occur_glob_constr p b1) ->
+       when is_gvar p e && is_bindinglist_meta id metas ->
+     let cp = if occur_glob_constr p b1 then set_pat_alias p cp else cp in
      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in
      match_in u alp metas sigma b1 b2
   | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(_,[cp],b1))]), Name id
-       when is_gvar p e && is_onlybinding_pattern_like_meta id metas && not (occur_glob_constr p b1) ->
+       when is_gvar p e && is_onlybinding_pattern_like_meta id metas ->
+     let cp = if occur_glob_constr p b1 then set_pat_alias p cp else cp in
      let alp,sigma = bind_binding_env alp sigma id cp in
      match_in u alp metas sigma b1 b2
   | _, _, Name id when is_bindinglist_meta id metas && (not isprod || na1 != Anonymous)->
-- 
cgit v1.2.3


From e4d93d1cef27d3a8c1e36139fc1e118730406f67 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 17 Aug 2017 20:12:55 +0200
Subject: Adding general support for irrefutable disjunctive patterns.

This now works not only for parsing of fun/forall (as in 8.6), but
also for arbitraty notations with binders and for printing.
---
 interp/notation_ops.ml | 120 ++++++++++++++++++++++++++++---------------------
 1 file changed, 70 insertions(+), 50 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index c44863791e..81cdecf03d 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -101,17 +101,24 @@ let name_to_ident = function
 
 let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na
 
+let product_of_cases_patterns patl =
+  List.fold_right (fun patl restl ->
+     List.flatten (List.map (fun p -> List.map (fun rest -> p::rest) restl) patl))
+    patl [[]]
+
 let rec cases_pattern_fold_map ?loc g e = DAst.with_val (function
   | PatVar na ->
-      let e',pat,na' = g e na in
-      e', (match pat with
-      | None -> DAst.make ?loc @@ PatVar na'
-      | Some ((_,pat),_) -> pat)
+      let e',disjpat,na' = g e na in
+      e', (match disjpat with
+      | None -> [DAst.make ?loc @@ PatVar na']
+      | Some ((_,disjpat),_) -> disjpat)
   | PatCstr (cstr,patl,na) ->
-      let e',pat,na' = g e na in
-      if pat <> None then user_err (Pp.str "Unable to instantiate an \"as\" clause with a pattern.");
+      let e',disjpat,na' = g e na in
+      if disjpat <> None then user_err (Pp.str "Unable to instantiate an \"as\" clause with a pattern.");
       let e',patl' = List.fold_left_map (cases_pattern_fold_map ?loc g) e patl in
-      e', DAst.make ?loc @@ PatCstr (cstr,patl',na')
+      (* Distribute outwards the inner disjunctive patterns *)
+      let disjpatl' = product_of_cases_patterns patl' in
+      e', List.map (fun patl' -> DAst.make ?loc @@ PatCstr (cstr,patl',na')) disjpatl'
   )
 
 let subst_binder_type_vars l = function
@@ -141,14 +148,14 @@ let rec subst_glob_vars l gc = DAst.map (function
 let ldots_var = Id.of_string ".."
 
 let protect g e na =
-  let e',pat,na = g e na in
-  if pat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern.");
+  let e',disjpat,na = g e na in
+  if disjpat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern.");
   e',na
 
-let apply_cases_pattern ?loc ((ids,pat),id) c =
+let apply_cases_pattern ?loc ((ids,disjpat),id) c =
   let tm = DAst.make ?loc (GVar id) in
-  DAst.make ?loc @@
-    GCases (LetPatternStyle, None, [tm,(Anonymous,None)], [loc,(ids,[pat], c)])
+  let eqns = List.map (fun pat -> (loc,(ids,[pat],c))) disjpat in
+  DAst.make ?loc @@ GCases (LetPatternStyle, None, [tm,(Anonymous,None)], eqns)
 
 let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
   let lt x = DAst.make ?loc x in lt @@ match nc with
@@ -167,14 +174,14 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
       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',pat,na = g e na in GLambda (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) pat (f e' c))
+      let e',disjpat,na = g e na in GLambda (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
   | NProd (na,ty,c) ->
-      let e',pat,na = g e na in GProd (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) pat (f e' c))
+      let e',disjpat,na = g e na in GProd (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
   | NLetIn (na,b,t,c) ->
-      let e',pat,na = g e na in
-      (match pat with
+      let e',disjpat,na = g e na in
+      (match disjpat with
        | None -> GLetIn (na,f e b,Option.map (f e) t,f e' c)
-       | Some pat -> DAst.get (apply_cases_pattern ?loc pat (f e' c)))
+       | Some disjpat -> DAst.get (apply_cases_pattern ?loc disjpat (f e' c)))
   | NCases (sty,rtntypopt,tml,eqnl) ->
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
 	let e',t' = match t with
@@ -183,15 +190,16 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
 	  let e',nal' = List.fold_right (fun na (e',nal) ->
               let e',na' = protect g e' na in
               e',na'::nal) nal (e',[]) in
-	  e',Some (Loc.tag ?loc (ind,nal')) in
+          e',Some (Loc.tag ?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,pat,na) = g e na in ((Name.cons na idl,e),pat,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 eqnl' = List.map (fun (patl,rhs) ->
-	let ((idl,e),patl) =
-	  List.fold_left_map (cases_pattern_fold_map ?loc fold) ([],e) patl in
-	Loc.tag (idl,patl,f e rhs)) eqnl in
-      GCases (sty,Option.map (f e') rtntypopt,tml',eqnl')
+        let ((idl,e),patl) =
+          List.fold_left_map (cases_pattern_fold_map ?loc fold) ([],e) patl in
+        let disjpatl = product_of_cases_patterns patl in
+        List.map (fun patl -> Loc.tag (idl,patl,f e rhs)) disjpatl) eqnl in
+      GCases (sty,Option.map (f e') rtntypopt,tml',List.flatten eqnl')
   | NLetTuple (nal,(na,po),b,c) ->
       let e',nal = List.fold_left_map (protect g) e nal in
       let e'',na = protect g e na in
@@ -806,8 +814,8 @@ let unify_binder_upto alp b b' =
   | GLocalDef (na,bk,c,t), GLocalDef (na',bk',c',t') ->
      let alp, na = unify_name_upto alp na na' in
      alp, DAst.make ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t')
-  | GLocalPattern ((p,ids),id,bk,t), GLocalPattern ((p',_),_,bk',t') ->
-     let alp, p = unify_pat_upto alp p p' in
+  | GLocalPattern ((disjpat,ids),id,bk,t), GLocalPattern ((disjpat',_),_,bk',t') when List.length disjpat = List.length disjpat' ->
+     let alp, p = List.fold_left2_map unify_pat_upto alp disjpat disjpat' in
      alp, DAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t')
   | _ -> raise No_match
 
@@ -840,9 +848,9 @@ let unify_term_binder alp c = DAst.(map (fun b' ->
   match DAst.get c, b' with
   | GVar id, GLocalAssum (na', bk', t') ->
      GLocalAssum (unify_id alp id na', bk', t')
-  | _, GLocalPattern ((p',ids), id, bk', t') ->
+  | _, GLocalPattern (([p'],ids), id, bk', t') ->
      let p = pat_binder_of_term c in
-     GLocalPattern ((unify_pat alp p p',ids), id, bk', t')
+     GLocalPattern (([unify_pat alp p p'],ids), id, bk', t')
   | _ -> raise No_match))
 
 let rec unify_terms_binders alp cl bl' =
@@ -895,23 +903,23 @@ let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma)
   let pat = try force_cases_pattern (cases_pattern_of_glob_constr Anonymous c) with Not_found -> raise No_match in
   try
     (* If already bound to a binder, unify the term and the binder *)
-    let pat' = Id.List.assoc var binders in
-    let pat'' = unify_pat alp pat pat' in
-    if pat' == pat'' then sigma
+    let patl' = Id.List.assoc var binders in
+    let patl'' = List.map2 (unify_pat alp) [pat] patl' in
+    if patl' == patl'' then sigma
     else
       let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in
-      add_binding_env alp sigma var pat''
-  with Not_found -> add_binding_env alp sigma var pat
+      add_binding_env alp sigma var patl''
+  with Not_found -> add_binding_env alp sigma var [pat]
 
-let bind_binding_env alp (terms,termlists,binders,binderlists as sigma) var pat =
+let bind_binding_env alp (terms,termlists,binders,binderlists as sigma) var disjpat =
   try
     (* If already bound to a binder possibly *)
     (* generating an alpha-renaming from unifying the new binder *)
-    let pat' = Id.List.assoc var binders in
-    let alp, pat = unify_pat_upto alp pat pat' in
+    let disjpat' = Id.List.assoc var binders in
+    let alp, disjpat = List.fold_left2_map unify_pat_upto alp disjpat disjpat' in
     let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in
-    alp, add_binding_env alp sigma var pat
-  with Not_found -> alp, add_binding_env alp sigma var pat
+    alp, add_binding_env alp sigma var disjpat
+  with Not_found -> alp, add_binding_env alp sigma var disjpat
 
 let bind_bindinglist_env alp (terms,termlists,binders,binderlists as sigma) var bl =
   let bl = List.rev bl in
@@ -955,7 +963,7 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
 
 let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
   | (na1,Name id2) when is_onlybinding_meta id2 metas ->
-      bind_binding_env alp sigma id2 (DAst.make (PatVar na1))
+      bind_binding_env alp sigma id2 [DAst.make (PatVar na1)]
   | (Name id1,Name id2) when is_term_meta id2 metas ->
       (* We let the non-binding occurrence define the rhs and hence reason up to *)
       (* alpha-conversion for the given occurrence of the name (see #4592)) *)
@@ -970,7 +978,7 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
 let rec match_cases_pattern_binders 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 ->
-      bind_binding_env alp sigma id2 pat1
+      bind_binding_env alp sigma id2 [pat1]
   | PatVar na1, PatVar na2 -> match_names metas acc na1 na2
   | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2)
       when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) ->
@@ -1205,18 +1213,27 @@ and match_binders u alp metas na1 na2 sigma b1 b2 =
 
 and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
   (* Match binders which can be substituted by a pattern *)
+  let store, get = set_temporary_memory () in
   match na1, DAst.get b1, na2 with
   (* Matching individual binders as part of a recursive pattern *)
-  | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id
-       when is_gvar p e && is_bindinglist_meta id metas ->
-     let cp = if occur_glob_constr p b1 then set_pat_alias p cp else cp in
-     let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in
+  | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id
+       when is_gvar p e && is_bindinglist_meta 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
+     let disjpat = if occur_glob_constr p b1 then List.map (set_pat_alias p) disjpat else disjpat in
+     let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((disjpat,ids),p,bk,t)] in
      match_in u alp metas sigma b1 b2
-  | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(_,[cp],b1))]), Name id
-       when is_gvar p e && is_onlybinding_pattern_like_meta id metas ->
-     let cp = if occur_glob_constr p b1 then set_pat_alias p cp else cp in
-     let alp,sigma = bind_binding_env alp sigma id cp in
+     | _ -> 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 ->
+    (match get () with
+     | [(_,(ids,disj_of_patl,b1))] ->
+     let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in
+     let disjpat = if occur_glob_constr p b1 then List.map (set_pat_alias p) disjpat else disjpat in
+     let alp,sigma = bind_binding_env alp sigma id disjpat in
      match_in u alp metas sigma b1 b2
+     | _ -> assert false)
   | _, _, Name id when is_bindinglist_meta id metas && (not isprod || na1 != Anonymous)->
       let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t)] in
       match_in u alp metas sigma b1 b2
@@ -1243,8 +1260,11 @@ let match_notation_constr u c (metas,pat) =
       let term = try Id.List.assoc x terms with Not_found -> raise No_match in
        ((term, scl)::terms',termlists',binders',binderlists')
     | NtnTypeBinder NtnParsedAsConstr ->
-       let v = glob_constr_of_cases_pattern (Id.List.assoc x binders) in
-       ((v,scl)::terms',termlists',binders',binderlists')
+       (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) ->
        (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists')
     | NtnTypeConstrList ->
-- 
cgit v1.2.3


From 5806b0476a1ac9b903503641cc3e2997d3e8d960 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 24 Aug 2017 15:18:23 +0200
Subject: When printing a notation with "match", more flexibility in matching
 equations.

We reason up to order, and accept to match a final catch-all clauses
with any other clause.

This allows for instance to parse and print a notation of the form
"if t is S n then p else q".
---
 interp/notation_ops.ml | 33 +++++++++++++++++++++++++--------
 1 file changed, 25 insertions(+), 8 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 81cdecf03d..44073c3b5e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -975,14 +975,15 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
   | (Anonymous,Anonymous) -> alp,sigma
   | _ -> raise No_match
 
-let rec match_cases_pattern_binders metas (alp,sigma as acc) pat1 pat2 =
+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 ->
       bind_binding_env alp sigma id2 [pat1]
   | PatVar na1, PatVar na2 -> match_names metas acc na1 na2
+  | _, PatVar Anonymous when allow_catchall -> acc
   | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2)
       when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) ->
-      List.fold_left2 (match_cases_pattern_binders metas)
+      List.fold_left2 (match_cases_pattern_binders false metas)
         (match_names metas acc na1 na2) patl1 patl2
   | _ -> raise No_match
 
@@ -1129,9 +1130,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
      match_binders u alp metas na1 na2
        (match_in u alp metas (match_in u alp metas sigma b1 b2) t1 t2) c1 c2
   | GCases (sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2)
-      when sty1 == sty2
-	 && Int.equal (List.length tml1) (List.length tml2)
-	 && Int.equal (List.length eqnl1) (List.length eqnl2) ->
+      when sty1 == sty2 && Int.equal (List.length tml1) (List.length tml2) ->
       let rtno1' = abstract_return_type_context_glob_constr tml1 rtno1 in
       let rtno2' = abstract_return_type_context_notation_constr tml2 rtno2 in
       let sigma =
@@ -1141,7 +1140,14 @@ let rec match_ inner u alp metas sigma a1 a2 =
       let sigma = List.fold_left2
       (fun s (tm1,_) (tm2,_) ->
         match_in u alp metas s tm1 tm2) sigma tml1 tml2 in
-      List.fold_left2_set No_match (match_equations u alp metas) sigma eqnl1 eqnl2
+      (* Try two different strategies for matching clauses *)
+      (try
+        List.fold_left2_set No_match (match_equations u alp metas) sigma eqnl1 eqnl2
+      with
+        No_match ->
+        List.fold_left2_set No_match (match_disjunctive_equations u alp metas) sigma
+           (Detyping.factorize_eqns eqnl1)
+           (List.map (fun (patl,rhs) -> ([patl],rhs)) eqnl2))
   | GLetTuple (nal1,(na1,to1),b1,c1), NLetTuple (nal2,(na2,to2),b2,c2)
       when Int.equal (List.length nal1) (List.length nal2) ->
       let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in
@@ -1241,14 +1247,25 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
      let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
      match_in u alp metas sigma b1 b2
 
-and match_equations u alp metas sigma (_,(_,patl1,rhs1)) (patl2,rhs2) =
+and match_equations u alp metas sigma (_,(ids,patl1,rhs1)) (patl2,rhs2) rest1 rest2 =
   (* patl1 and patl2 have the same length because they respectively
      correspond to some tml1 and tml2 that have the same length *)
+  let allow_catchall = (rest2 = [] && ids = []) in
   let (alp,sigma) =
-    List.fold_left2 (match_cases_pattern_binders metas)
+    List.fold_left2 (match_cases_pattern_binders allow_catchall metas)
       (alp,sigma) patl1 patl2 in
   match_in u alp metas sigma rhs1 rhs2
 
+and match_disjunctive_equations u alp metas sigma (_,(ids,disjpatl1,rhs1)) (disjpatl2,rhs2) _ _ =
+  (* patl1 and patl2 have the same length because they respectively
+     correspond to some tml1 and tml2 that have the same length *)
+  let (alp,sigma) =
+    List.fold_left2_set No_match
+      (fun alp_sigma patl1 patl2 _ _ ->
+        List.fold_left2 (match_cases_pattern_binders false metas) alp_sigma patl1 patl2)
+      (alp,sigma) disjpatl1 disjpatl2 in
+  match_in u alp metas sigma rhs1 rhs2
+
 let match_notation_constr u c (metas,pat) =
   let terms,termlists,binders,binderlists =
     match_ false u ([],[]) metas ([],[],[],[]) c pat in
-- 
cgit v1.2.3


From dcfd5c2c2cefcd8ae6a5b2e90fcbd98da4f1b120 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 25 Nov 2017 20:50:03 +0100
Subject: Notations: Adding modifiers to tell which kind of binder a constr can
 parse.

Concretely, we provide "constr as ident", "constr as strict pattern"
and "constr as pattern".

This tells to parse a binder as a constr, restricting to only ident or
to only a strict pattern, or to a pattern which can also be an ident.

The "strict pattern" modifier allows to restrict the use of patterns
in printing rules. This allows e.g. to select the appropriate rule for
printing between {x|P} and {'pat|P}.
---
 interp/notation_ops.ml | 28 +++++++++++++++++++++-------
 1 file changed, 21 insertions(+), 7 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 44073c3b5e..c65f4785ef 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')
-- 
cgit v1.2.3