Add preliminary support for notations with large class (non-recursive) binders.

We introduce a class of open binders which includes "x", "x:t", "'pat"
and a class of closed binders which includes "x", "(x:t)", "'pat".

8 files changed, 48 insertions, 29 deletions

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 977cbbccf2..a5ff5df7cf 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -83,6 +83,8 @@ type cases_pattern_expr_r =
   | CPatCast   of cases_pattern_expr * constr_expr
 and cases_pattern_expr = cases_pattern_expr_r CAst.t
 
+and kinded_cases_pattern_expr = cases_pattern_expr * Glob_term.binding_kind
+
 and cases_pattern_notation_substitution =
     cases_pattern_expr list *     (* for constr subterms *)
     cases_pattern_expr list list  (* for recursive notations *)
@@ -150,7 +152,7 @@ and local_binder_expr =
 and constr_notation_substitution =
     constr_expr list *      (* for constr subterms *)
     constr_expr list list * (* for recursive notations *)
-    cases_pattern_expr list *   (* for binders *)
+    kinded_cases_pattern_expr list *   (* for binders *)
     local_binder_expr list list (* for binder lists (recursive notations) *)
 
 type constr_pattern_expr = constr_expr
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index efc2a35b65..fe107c3580 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -94,6 +94,9 @@ and cases_pattern_notation_substitution_eq (s1, n1) (s2, n2) =
   List.equal cases_pattern_expr_eq s1 s2 &&
   List.equal (List.equal cases_pattern_expr_eq) n1 n2
 
+let kinded_cases_pattern_expr_eq (p1,bk1) (p2,bk2) =
+  cases_pattern_expr_eq p1 p2 && Glob_ops.binding_kind_eq bk1 bk2
+
 let eq_universes u1 u2 =
   match u1, u2 with
   | None, None -> true
@@ -231,7 +234,7 @@ and local_binder_eq l1 l2 = match l1, l2 with
 and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) =
   List.equal constr_expr_eq e1 e2 &&
   List.equal (List.equal constr_expr_eq) el1 el2 &&
-  List.equal cases_pattern_expr_eq b1 b2 &&
+  List.equal kinded_cases_pattern_expr_eq b1 b2 &&
   List.equal (List.equal local_binder_eq) bl1 bl2
 
 and instance_eq (x1,c1) (x2,c2) =
@@ -472,7 +475,7 @@ let locs_of_notation ?loc locs ntn =
 let ntn_loc ?loc (args,argslist,binders,binderslist) =
   locs_of_notation ?loc
     (List.map constr_loc (args@List.flatten argslist)@
-     List.map cases_pattern_expr_loc binders@
+     List.map (fun (x,_) -> cases_pattern_expr_loc x) binders@
      List.map local_binders_loc binderslist)
 
 let patntn_loc ?loc (args,argslist) =
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8d3cf7274a..aa3a458989 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1303,7 +1303,8 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
                       termlists in
                   let bl =
                     List.map (fun ((vars,bl),(subentry,(scopt,scl))) ->
-                      mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl))
+                      (mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl)),
+                      Explicit)
                       binders in
                   let bll =
                     List.map (fun ((vars,bl),(subentry,(scopt,scl))) ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b13225d91f..cb2c5b5f4c 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -715,7 +715,7 @@ let out_patvar = CAst.map_with_loc (fun ?loc -> function
   | _ -> assert false)
 
 let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function
- | Anonymous -> (renaming,env), None, Anonymous
+ | Anonymous -> (renaming,env), None, Anonymous, Explicit
  | Name id ->
   let store,get = set_temporary_memory () in
   let test_kind = test_kind_tolerant in
@@ -726,17 +726,17 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
     let pat, na = match disjpat with
     | [pat] when is_patvar_store store pat -> let na = get () in None, na
     | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in
-    (renaming,env), pat, na
+    (renaming,env), pat, na, Explicit
   with Not_found ->
   try
     (* Trying to associate a pattern *)
-    let pat,(onlyident,scopes) = Id.Map.find id binders in
+    let (pat,bk),(onlyident,scopes) = Id.Map.find id binders in
     let env = set_env_scopes env scopes in
     if onlyident then
       (* Do not try to interpret a variable as a constructor *)
       let na = out_patvar pat in
       let env = push_name_env ntnvars [] env na in
-      (renaming,env), None, na.v
+      (renaming,env), None, na.v, bk
     else
       (* Interpret as a pattern *)
       let env,((disjpat,ids),id),na = intern_pat test_kind ntnvars env pat in
@@ -744,7 +744,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
         match disjpat with
         | [pat] when is_patvar_store store pat -> let na = get () in None, na
         | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in
-      (renaming,env), pat, na
+      (renaming,env), pat, na, bk
   with Not_found ->
     (* Binders not bound in the notation do not capture variables *)
     (* outside the notation (i.e. in the substitution) *)
@@ -752,7 +752,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
     let renaming' =
       if Id.equal id id' then renaming else Id.Map.add id id' renaming
     in
-    (renaming',env), None, Name id'
+    (renaming',env), None, Name id', Explicit
 
 type binder_action =
 | AddLetIn of lname * constr_expr * constr_expr option
@@ -877,7 +877,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
             Id.Map.add id (gc, None) map
           with Nametab.GlobalizationError _ -> map
         in
-        let mk_env' (c, (onlyident,scopes)) =
+        let mk_env' ((c,_bk), (onlyident,scopes)) =
           let nenv = set_env_scopes env scopes in
           let test_kind =
             if onlyident then test_kind_ident_in_notation
@@ -916,17 +916,17 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
     (* Two special cases to keep binder name synchronous with BinderType *)
     | NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
         when Name.equal na na' ->
-        let subinfos,disjpat,na = traverse_binder intern_pat ntnvars subst avoid subinfos na in
+        let subinfos,disjpat,na,bk = traverse_binder intern_pat ntnvars subst avoid subinfos na in
         let ty = DAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
-        DAst.make ?loc @@ GProd (na,Explicit,ty,Option.fold_right apply_cases_pattern disjpat (aux subst' subinfos c'))
+        DAst.make ?loc @@ GProd (na,bk,ty,Option.fold_right apply_cases_pattern disjpat (aux subst' subinfos c'))
     | NLambda (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
         when Name.equal na na' ->
-        let subinfos,disjpat,na = traverse_binder intern_pat ntnvars subst  avoid subinfos na in
+        let subinfos,disjpat,na,bk = traverse_binder intern_pat ntnvars subst  avoid subinfos na in
         let ty = DAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
-        DAst.make ?loc @@ GLambda (na,Explicit,ty,Option.fold_right apply_cases_pattern disjpat (aux subst' subinfos c'))
+        DAst.make ?loc @@ GLambda (na,bk,ty,Option.fold_right apply_cases_pattern disjpat (aux subst' subinfos c'))
     | t ->
       glob_constr_of_notation_constr_with_binders ?loc
-        (traverse_binder intern_pat ntnvars subst  avoid) (aux subst') ~h:binder_status_fun subinfos t
+        (traverse_binder intern_pat ntnvars subst avoid) (aux subst') ~h:binder_status_fun subinfos t
   and subst_var (terms, binderopt, _terminopt) (renaming, env) id =
     (* subst remembers the delimiters stack in the interpretation *)
     (* of the notations *)
@@ -935,7 +935,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
       intern (set_env_scopes env scopes) a
     with Not_found ->
     try
-      let pat,(onlyident,scopes) = Id.Map.find id binders in
+      let (pat,_bk),(onlyident,scopes) = Id.Map.find id binders in
       let nenv = set_env_scopes env scopes in
       let test_kind =
         if onlyident then test_kind_ident_in_notation
@@ -982,13 +982,13 @@ let split_by_type ids subst =
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
     | NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) ->
        let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
-       let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,(false,scl)) binders' in
+       let binders' = Id.Map.add id ((coerce_to_cases_pattern_expr a,Explicit),(false,scl)) binders' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
     | NtnTypeBinder NtnBinderParsedAsConstr AsIdent ->
        let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
-       let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in
+       let binders' = Id.Map.add id ((cases_pattern_of_name (coerce_to_name a),Explicit),(true,scl)) binders' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
-    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ as x) ->
+    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder as x) ->
        let onlyident = (x = NtnParsedAsIdent) in
        let binders,binders' = bind id (onlyident,scl) binders binders' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
diff --git a/interp/notation.ml b/interp/notation.ml
index 286ece6cb6..b5951a9c59 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -64,7 +64,8 @@ let notation_binder_source_eq s1 s2 = match s1, s2 with
 | NtnParsedAsIdent,  NtnParsedAsIdent -> true
 | NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2
 | NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2
-| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false
+| NtnParsedAsBinder,  NtnParsedAsBinder -> true
+| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _ | NtnParsedAsBinder), _ -> false
 
 let ntpe_eq t1 t2 = match t1, t2 with
 | NtnTypeConstr, NtnTypeConstr -> true
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index c4d2a2a496..61f93aa969 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -272,9 +272,14 @@ let default_binder_status_fun = {
   slide = (fun x -> x);
 }
 
+let test_implicit_argument_mark bk =
+  if not (Glob_ops.binding_kind_eq bk Explicit) then
+    user_err (Pp.str "Unexpected implicit argument mark.")
+
 let protect g e na =
-  let e',disjpat,na = g e na in
+  let e',disjpat,na,bk = g e na in
   if disjpat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern.");
+  test_implicit_argument_mark bk;
   e',na
 
 let apply_cases_pattern_term ?loc (ids,disjpat) tm c =
@@ -302,12 +307,13 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
       DAst.get (subst_glob_vars outerl it)
   | NLambda (na,ty,c) ->
       let e = h.switch_lambda e in
-      let e',disjpat,na = g e na in GLambda (na,Explicit,f (h.restart_prod e) ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
+      let e',disjpat,na,bk = g e na in GLambda (na,bk,f (h.restart_prod e) ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
   | NProd (na,ty,c) ->
       let e = h.switch_prod e in
-      let e',disjpat,na = g e na in GProd (na,Explicit,f (h.restart_prod e) ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
+      let e',disjpat,na,bk = g e na in GProd (na,bk,f (h.restart_prod e) ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
   | NLetIn (na,b,t,c) ->
-      let e',disjpat,na = g e na in
+      let e',disjpat,na,bk = g e na in
+      test_implicit_argument_mark bk;
       (match disjpat with
        | None -> GLetIn (na,f (h.restart_lambda e) b,Option.map (f (h.restart_prod e)) t,f e' c)
        | Some (disjpat,_id) -> DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c)))
@@ -323,7 +329,10 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
           e',Some (CAst.make ?loc (ind,nal')) in
         let e',na' = protect g e' na in
         (e',(f e tm,(na',t'))::tml')) tml (e,[]) in
-      let fold (idl,e) na = let (e,disjpat,na) = g e na in ((Name.cons na idl,e),disjpat,na) in
+      let fold (idl,e) na =
+        let (e,disjpat,na,bk) = g e na in
+        test_implicit_argument_mark bk;
+        ((Name.cons na idl,e),disjpat,na) in
       let eqnl' = List.map (fun (patl,rhs) ->
         let ((idl,e),patl) =
           List.fold_left_map (cases_pattern_fold_map ?loc fold) ([],e) patl in
@@ -356,7 +365,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
 
 let glob_constr_of_notation_constr ?loc x =
   let rec aux () x =
-    glob_constr_of_notation_constr_with_binders ?loc (fun () id -> ((),None,id)) aux () x
+    glob_constr_of_notation_constr_with_binders ?loc (fun () id -> ((),None,id,Explicit)) aux () x
   in aux () x
 
 (******************************************************************************)
@@ -852,6 +861,7 @@ let is_onlybinding_pattern_like_meta isvar id metas =
       | _,NtnTypeBinder (NtnBinderParsedAsConstr
                            (AsIdentOrPattern | AsStrictPattern)) -> true
       | _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar)
+      | _,NtnTypeBinder NtnParsedAsBinder -> not isvar
       | _ -> false
   with Not_found -> false
 
@@ -1497,7 +1507,7 @@ let match_notation_constr ~print_univ c ~vars (metas,pat) =
           let v = glob_constr_of_cases_pattern (Global.env()) pat in
           (((vars,v),scl)::terms',termlists',binders',binderlists')
         | _ -> raise No_match)
-    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) ->
+    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder) ->
        (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists')
     | NtnTypeConstrList ->
        (terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists')
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 9d451a5bb9..3e8fdd8254 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -53,7 +53,7 @@ val apply_cases_pattern : ?loc:Loc.t ->
   (Id.t list * cases_pattern_disjunction) * Id.t -> glob_constr -> glob_constr
 
 val glob_constr_of_notation_constr_with_binders : ?loc:Loc.t ->
-  ('a -> Name.t -> 'a * ((Id.t list * cases_pattern_disjunction) * Id.t) option * Name.t) ->
+  ('a -> Name.t -> 'a * ((Id.t list * cases_pattern_disjunction) * Id.t) option * Name.t * Glob_term.binding_kind) ->
   ('a -> notation_constr -> glob_constr) -> ?h:'a binder_status_fun ->
   'a -> notation_constr -> glob_constr
 
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 82238b71b7..47b9deccce 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -78,6 +78,8 @@ type notation_binder_source =
   | NtnParsedAsIdent
   (* This accepts ident, or pattern, or both *)
   | NtnBinderParsedAsConstr of constr_as_binder_kind
+  (* This accepts ident, _, and quoted pattern *)
+  | NtnParsedAsBinder
 
 type notation_var_instance_type =
   | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList