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}.

3 files changed, 83 insertions, 33 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 379d09e89..158ac24b2 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -549,6 +549,18 @@ let is_var store pat =
   | PatVar na -> store na; true
   | _ -> false
 
+let out_var pat =
+  match pat.CAst.v with
+  | CPatAtom (Some (Ident (_,id))) -> Name id
+  | CPatAtom None -> Anonymous
+  | _ -> assert false
+
+let term_of_name = function
+  | Name id -> DAst.make (GVar id)
+  | Anonymous ->
+       let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
+       DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), Misctypes.IntroAnonymous, None))
+
 let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function
  | Anonymous -> (renaming,env), None, Anonymous
  | Name id ->
@@ -564,13 +576,21 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
   with Not_found ->
   try
     (* Trying to associate a pattern *)
-    let pat,scopes = Id.Map.find id binders in
+    let pat,(onlyident,scopes) = Id.Map.find id binders in
     let env = set_env_scopes env scopes in
-    let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
-    let pat, na = match disjpat with
-    | [pat] when is_var store pat -> let na = get () in None, na
-    | _ -> Some ((List.map snd ids,disjpat),id), snd na in
-    (renaming,env), pat, na
+    if onlyident then
+      (* Do not try to interpret a variable as a constructor *)
+      let na = out_var pat in
+      let env = push_name_env ntnvars (Variable,[],[],[]) env (pat.CAst.loc, na) in
+      (renaming,env), None, na
+    else
+      (* Interpret as a pattern *)
+      let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
+      let pat, na =
+        match disjpat with
+        | [pat] when is_var store pat -> let na = get () in None, na
+        | _ -> Some ((List.map snd ids,disjpat),id), snd na in
+      (renaming,env), pat, na
   with Not_found ->
     (* Binders not bound in the notation do not capture variables *)
     (* outside the notation (i.e. in the substitution) *)
@@ -688,12 +708,15 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
           let gc = intern nenv c in
           (gc, Some c)
         in
-        let mk_env' (c, (tmp_scope, subscopes)) =
+        let mk_env' (c, (onlyident,(tmp_scope,subscopes))) =
           let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
-          let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in
-          match disjpat with
-          | [pat] -> (glob_constr_of_cases_pattern pat, None)
-          | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.CAst.loc ()
+          if onlyident then
+            let na = out_var c in term_of_name na, None
+          else
+            let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in
+            match disjpat with
+            | [pat] -> (glob_constr_of_cases_pattern pat, None)
+            | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.CAst.loc ()
         in
         let terms = Id.Map.map mk_env terms in
         let binders = Id.Map.map mk_env' binders in
@@ -744,15 +767,18 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
                 scopes = subscopes @ env.scopes} a
     with Not_found ->
     try
-      let pat,scopes = Id.Map.find id binders in
+      let pat,(onlyident,scopes) = Id.Map.find id binders in
       let env = set_env_scopes env scopes in
       (* We deactivate impls to avoid the check on hidden parameters *)
       (* and since we are only interested in the pattern as a term *)
       let env = reset_hidden_inductive_implicit_test env in
-      let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
-      match disjpat with
-      | [pat] -> glob_constr_of_cases_pattern pat
-      | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.")
+      if onlyident then
+        term_of_name (out_var pat)
+      else
+        let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
+        match disjpat with
+        | [pat] -> glob_constr_of_cases_pattern pat
+        | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.")
     with Not_found ->
     try
       match binderopt with
@@ -774,6 +800,10 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
    into a substitution for interpretation and based on binding/constr
    distinction *)
 
+let cases_pattern_of_name (loc,na) =
+  let atom = match na with Name id -> Some (Ident (loc,id)) | Anonymous -> None in
+  CAst.make ?loc (CPatAtom atom)
+
 let split_by_type ids subst =
   let bind id scl l s =
     match l with
@@ -785,12 +815,17 @@ let split_by_type ids subst =
     | NtnTypeConstr ->
        let terms,terms' = bind id scl terms terms' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
-    | NtnTypeBinder NtnParsedAsConstr ->
+    | NtnTypeBinder NtnBinderParsedAsConstr (Extend.AsIdentOrPattern | Extend.AsStrictPattern) ->
+       let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
+       let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,(false,scl)) binders' in
+       (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
+    | NtnTypeBinder NtnBinderParsedAsConstr Extend.AsIdent ->
        let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
-       let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,scl) binders' in
+       let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
-    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern) ->
-       let binders,binders' = bind id scl binders binders' in
+    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ as x) ->
+       let onlyident = (x = NtnParsedAsIdent) in
+       let binders,binders' = bind id (onlyident,scl) binders binders' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
     | NtnTypeConstrList ->
        let termlists,termlists' = bind id scl termlists termlists' in
diff --git a/interp/notation.ml b/interp/notation.ml
index 13ff960f6..ea7ef21b1 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -97,9 +97,10 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with
 | ETBigint, ETBigint -> true
 | ETBinder b1, ETBinder b2 -> b1 == b2
 | ETConstr lev1, ETConstr lev2 -> eq lev1 lev2
-| ETPattern n1, ETPattern n2 -> Option.equal Int.equal n1 n2
+| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2
+| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
 | ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2'
-| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _), _ -> false
+| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false
 
 let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) =
   let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
@@ -626,10 +627,10 @@ let availability_of_prim_token n printer_scope local_scopes =
 let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
 
 let notation_binder_source_eq s1 s2 = match s1, s2 with
-   | NtnParsedAsConstr, NtnParsedAsConstr -> true
-   | NtnParsedAsIdent,  NtnParsedAsIdent -> true
-   | NtnParsedAsPattern, NtnParsedAsPattern -> true
-   | (NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern), _ -> false
+| NtnParsedAsIdent,  NtnParsedAsIdent -> true
+| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2
+| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2
+| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false
 
 let ntpe_eq t1 t2 = match t1, t2 with
 | NtnTypeConstr, NtnTypeConstr -> true
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 44073c3b5..c65f4785e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -671,12 +671,20 @@ let is_term_meta id metas =
   try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false
   with Not_found -> false
 
+let is_onlybinding_strict_meta id metas =
+  try match Id.List.assoc id metas with _,NtnTypeBinder (NtnParsedAsPattern true) -> true | _ -> false
+  with Not_found -> false
+
 let is_onlybinding_meta id metas =
   try match Id.List.assoc id metas with _,NtnTypeBinder _ -> true | _ -> false
   with Not_found -> false
 
-let is_onlybinding_pattern_like_meta id metas =
-  try match Id.List.assoc id metas with _,NtnTypeBinder (NtnParsedAsConstr | NtnParsedAsPattern) -> true | _ -> false
+let is_onlybinding_pattern_like_meta isvar id metas =
+  try match Id.List.assoc id metas with
+      | _,NtnTypeBinder (NtnBinderParsedAsConstr
+                           (Extend.AsIdentOrPattern | Extend.AsStrictPattern)) -> true
+      | _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar)
+      | _ -> false
   with Not_found -> false
 
 let is_bindinglist_meta id metas =
@@ -962,6 +970,8 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
   | _ -> raise No_match
 
 let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
+  | (na1,Name id2) when is_onlybinding_strict_meta id2 metas ->
+      raise No_match
   | (na1,Name id2) when is_onlybinding_meta id2 metas ->
       bind_binding_env alp sigma id2 [DAst.make (PatVar na1)]
   | (Name id1,Name id2) when is_term_meta id2 metas ->
@@ -977,7 +987,9 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
 
 let rec match_cases_pattern_binders allow_catchall metas (alp,sigma as acc) pat1 pat2 =
   match DAst.get pat1, DAst.get pat2 with
-  | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta id2 metas ->
+  | PatVar _, PatVar (Name id2) when is_onlybinding_pattern_like_meta true id2 metas ->
+      bind_binding_env alp sigma id2 [pat1]
+  | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta false id2 metas ->
       bind_binding_env alp sigma id2 [pat1]
   | PatVar na1, PatVar na2 -> match_names metas acc na1 na2
   | _, PatVar Anonymous when allow_catchall -> acc
@@ -1093,7 +1105,9 @@ let rec match_ inner u alp metas sigma a1 a2 =
   match DAst.get a1, a2 with
   (* Matching notation variable *)
   | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 a1
-  | r1, NVar id2 when is_onlybinding_pattern_like_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1
+  | GVar _, NVar id2 when is_onlybinding_pattern_like_meta true id2 metas -> bind_binding_as_term_env alp sigma id2 a1
+  | r1, NVar id2 when is_onlybinding_pattern_like_meta false id2 metas -> bind_binding_as_term_env alp sigma id2 a1
+  | GVar _, NVar id2 when is_onlybinding_strict_meta id2 metas -> raise No_match
   | GVar _, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1
   | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 a1
 
@@ -1232,7 +1246,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
      match_in u alp metas sigma b1 b2
      | _ -> assert false)
   | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id
-       when is_gvar p e && is_onlybinding_pattern_like_meta id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 ->
+       when is_gvar p e && is_onlybinding_pattern_like_meta false id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 ->
     (match get () with
      | [(_,(ids,disj_of_patl,b1))] ->
      let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in
@@ -1276,13 +1290,13 @@ let match_notation_constr u c (metas,pat) =
     | NtnTypeConstr ->
       let term = try Id.List.assoc x terms with Not_found -> raise No_match in
        ((term, scl)::terms',termlists',binders',binderlists')
-    | NtnTypeBinder NtnParsedAsConstr ->
+    | NtnTypeBinder (NtnBinderParsedAsConstr _) ->
        (match Id.List.assoc x binders with
         | [pat] ->
           let v = glob_constr_of_cases_pattern pat in
           ((v,scl)::terms',termlists',binders',binderlists')
         | _ -> raise No_match)
-    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern) ->
+    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) ->
        (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists')
     | NtnTypeConstrList ->
        (terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists')