Support quotations (genargs) in patterns

For coq#11641

`constr_pattern` is split in 2 types, one is allowed to contain
genargs and the other not.
To share code this uses a GADT `'i constr_pattern_r`, with genargs
allowed instantiated to `` [`uninstantiated] constr_pattern_r ``,
without genargs instantiated to `` constr_pattern = [`any] constr_pattern_r ``.

Ltac2 instantiates the genargs in the `ml_interp` for the TacExt ie
a pattern expression is interned to `` [`uninstantiated] constr_pattern_r ``
then interped to `constr_pattern`.

Most code (basically everything except ltac2) uses only the no-genarg
version (TODO change this? but currently we have no non-ltac2 genargs
handled).

For now I just have it handling `$pattern:` quotations.

For instance something like `ltac2pat:(tactic : pattern)` should be
easy to implement (main issue is how to handle the tactic monad
switch, but maybe `interp_pat` should live in the monad?).

Exposing a `preterm -> pattern` should also be possible.

Also maybe internalization should pass around `pattern_mode`? This
would let us intern `ltac2:(tac)` with different expected types
depending on if we're interning as constr or pattern.

PS the genarg mod_subst operators should probably be in their own
gensubst module, for now out of lazyness I put them in genarg.ml

dev/ci/user-overlays/17667-SkySkimmer-pattern-quotations.sh

@@ -0,0 +1,3 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi pattern-quotations 17667
+
+overlay equations https://github.com/SkySkimmer/Coq-Equations pattern-quotations 17667

interp/constrextern.ml

@@ -1377,7 +1377,22 @@ let compute_displayed_name_in_pattern sigma avoid na c =
   let open Namegen in
   compute_displayed_name_in_gen (fun _ -> Patternops.noccurn_pattern) sigma avoid na c
 
-let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
+let glob_of_pat_under_context glob_of_pat avoid env sigma (nas, pat) =
+  let fold (avoid, env, nas, epat) na =
+    let na, avoid = compute_displayed_name_in_pattern (Global.env ()) sigma avoid na epat in
+    let env = Termops.add_name na env in
+    let epat = match epat with PLambda (_, _, p) -> p | _ -> assert false in
+    (avoid, env, na :: nas, epat)
+  in
+  let epat = Array.fold_right (fun na p -> PLambda (na, PMeta None, p)) nas pat in
+  let (avoid', env', nas, _) = Array.fold_left fold (avoid, env, [], epat) nas in
+  let pat = glob_of_pat avoid' env' sigma pat in
+  (Array.rev_of_list nas, pat)
+
+let rec glob_of_pat
+  : 'a. _ -> _ -> _ -> 'a constr_pattern_r -> _
+  = fun (type a) avoid env sigma (pat: a constr_pattern_r) ->
+    DAst.make @@ match pat with
   | PRef ref -> GRef (ref,None)
   | PVar id  -> GVar id
   | PEvar (evk,l) ->
@@ -1400,6 +1415,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
       GVar id
   | PMeta None -> GHole (Evar_kinds.InternalHole, IntroAnonymous)
   | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n)
+  | PGenarg g -> GGenarg g
   | PProj (p,c) -> GApp (DAst.make @@ GRef (GlobRef.ConstRef (Projection.constant p),None),
                          [glob_of_pat avoid env sigma c])
   | PApp (f,args) ->
@@ -1424,15 +1440,15 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
       GIf (glob_of_pat avoid env sigma c, (Anonymous,None),
            glob_of_pat avoid env sigma b1, glob_of_pat avoid env sigma b2)
   | PCase ({cip_style=Constr.LetStyle},None,tm,[(0,n,b)]) ->
-      let n, b = glob_of_pat_under_context avoid env sigma (n, b) in
+      let n, b = glob_of_pat_under_context glob_of_pat avoid env sigma (n, b) in
       let nal = Array.to_list n in
       GLetTuple (nal,(Anonymous,None),glob_of_pat avoid env sigma tm,b)
   | PCase (info,p,tm,bl) ->
       let mat = match bl, info.cip_ind with
         | [], _ -> []
         | _, Some ind ->
           let map (i, n, c) =
-            let n, c = glob_of_pat_under_context avoid env sigma (n, c) in
+            let n, c = glob_of_pat_under_context glob_of_pat avoid env sigma (n, c) in
             let nal = Array.to_list n in
             let mkPatVar na = DAst.make @@ PatVar na in
             let p = DAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in
@@ -1447,7 +1463,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
       let indnames,rtn = match p, info.cip_ind with
         | None, _ -> (Anonymous,None),None
         | Some p, Some ind ->
-          let nas, p = glob_of_pat_under_context avoid env sigma p in
+          let nas, p = glob_of_pat_under_context glob_of_pat avoid env sigma p in
           let nas = Array.rev_to_list nas in
           ((List.hd nas, Some (CAst.make (ind, List.tl nas))), Some p)
         | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
@@ -1493,18 +1509,6 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
     let glob_of = glob_of_pat avoid env sigma in
     GArray (None, Array.map glob_of t, glob_of def, glob_of ty)
 
-and glob_of_pat_under_context avoid env sigma (nas, pat) =
-  let fold (avoid, env, nas, epat) na =
-    let na, avoid = compute_displayed_name_in_pattern (Global.env ()) sigma avoid na epat in
-    let env = Termops.add_name na env in
-    let epat = match epat with PLambda (_, _, p) -> p | _ -> assert false in
-    (avoid, env, na :: nas, epat)
-  in
-  let epat = Array.fold_right (fun na p -> PLambda (na, PMeta None, p)) nas pat in
-  let (avoid', env', nas, _) = Array.fold_left fold (avoid, env, [], epat) nas in
-  let pat = glob_of_pat avoid' env' sigma pat in
-  (Array.rev_of_list nas, pat)
-
 let extern_constr_pattern env sigma pat =
   extern true ((constr_some_level,None),([],[]))
     (* XXX no vars? *)

interp/constrextern.mli

@@ -29,7 +29,7 @@ val extern_cases_pattern : Id.Set.t -> 'a cases_pattern_g -> cases_pattern_expr
 val extern_glob_constr : extern_env -> 'a glob_constr_g -> constr_expr
 val extern_glob_type : ?impargs:Glob_term.binding_kind list -> extern_env -> 'a glob_constr_g -> constr_expr
 val extern_constr_pattern : names_context -> Evd.evar_map ->
-  constr_pattern -> constr_expr
+  _ constr_pattern_r -> constr_expr
 val extern_closed_glob : ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name ->
   env -> Evd.evar_map -> closed_glob_constr -> constr_expr
 

interp/constrintern.ml

@@ -2368,7 +2368,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
           intern_sign;
           strict_check = match env.strict_check with None -> false | Some b -> b;
         } in
-        let (_, glb) = Genintern.generic_intern ist gen in
+        let intern = if pattern_mode
+          then Genintern.generic_intern_pat ?loc
+          else Genintern.generic_intern
+        in
+        let (_, glb) = intern ist gen in
         DAst.make ?loc @@
         GGenarg glb
     (* Parsing pattern variables *)
@@ -2702,6 +2706,11 @@ let intern_constr_pattern env sigma ?(as_type=false) ?strict_check ?(ltacvars=em
             ?strict_check ~pattern_mode:true ~ltacvars env sigma c in
   pattern_of_glob_constr c
 
+let intern_uninstantiated_constr_pattern env sigma ?(as_type=false) ?strict_check ?(ltacvars=empty_ltac_sign) c =
+  let c = intern_gen (if as_type then IsType else WithoutTypeConstraint)
+            ?strict_check ~pattern_mode:true ~ltacvars env sigma c in
+  uninstantiated_pattern_of_glob_constr c
+
 let intern_core kind env sigma ?strict_check ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
       { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c =
   let tmp_scope = scope_of_type_kind env sigma kind in

interp/constrintern.mli

@@ -144,6 +144,10 @@ val intern_constr_pattern :
   env -> evar_map -> ?as_type:bool -> ?strict_check:bool -> ?ltacvars:ltac_sign ->
     constr_pattern_expr -> Id.Set.t * constr_pattern
 
+val intern_uninstantiated_constr_pattern :
+  env -> evar_map -> ?as_type:bool -> ?strict_check:bool -> ?ltacvars:ltac_sign ->
+    constr_pattern_expr -> Id.Set.t * [`uninstantiated] constr_pattern_r
+
 (** Returns None if it's an abbreviation not bound to a name, raises an error
     if not existing *)
 val intern_reference : qualid -> GlobRef.t option

interp/genintern.ml

@@ -75,6 +75,27 @@ let generic_intern ist (GenArg (Rawwit wit, v)) =
   let (ist, v) = intern wit ist v in
   (ist, in_gen (glbwit wit) v)
 
+type ('raw,'glb) intern_pat_fun = ?loc:Loc.t -> ('raw,'glb) intern_fun
+
+module InternPatObj = struct
+  type ('raw, 'glb, 'top) obj = ('raw, 'glb) intern_pat_fun
+  let name = "intern_pat"
+  let default tag =
+    Some (fun ?loc ->
+        let name = Genarg.(ArgT.repr (get_arg_tag tag)) in
+        CErrors.user_err ?loc Pp.(str "This quotation is not supported in tactic patterns (" ++ str name ++ str ")"))
+end
+
+module InternPat = Register (InternPatObj)
+
+let intern_pat = InternPat.obj
+
+let register_intern_pat = InternPat.register0
+
+let generic_intern_pat ?loc ist (GenArg (Rawwit wit, v)) =
+  let (ist, v) = intern_pat wit ?loc ist v in
+  (ist, in_gen (glbwit wit) v)
+
 (** Notation substitution *)
 
 let substitute_notation = NtnSubst.obj

interp/genintern.mli

@@ -46,6 +46,14 @@ val intern : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb) intern_fun
 
 val generic_intern : (raw_generic_argument, glob_generic_argument) intern_fun
 
+(** {5 Internalization in tactic patterns} *)
+
+type ('raw,'glb) intern_pat_fun = ?loc:Loc.t -> ('raw,'glb) intern_fun
+
+val intern_pat : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb) intern_pat_fun
+
+val generic_intern_pat : (raw_generic_argument, glob_generic_argument) intern_pat_fun
+
 (** {5 Notation functions} *)
 
 type 'glb ntn_subst_fun = Id.Set.t -> Glob_term.glob_constr Id.Map.t -> 'glb -> 'glb
@@ -59,5 +67,9 @@ val generic_substitute_notation : glob_generic_argument ntn_subst_fun
 val register_intern0 : ('raw, 'glb, 'top) genarg_type ->
   ('raw, 'glb) intern_fun -> unit
 
+val register_intern_pat : ('raw, 'glb, 'top) genarg_type ->
+  ('raw, 'glb) intern_pat_fun -> unit
+
+
 val register_ntn_subst0 : ('raw, 'glb, 'top) genarg_type ->
   'glb ntn_subst_fun -> unit

plugins/ltac2/tac2core.ml

@@ -1713,11 +1713,15 @@ let () =
   define_ml_object Tac2quote.wit_ident obj
 
 let () =
-  let intern self ist c =
-    let env = ist.Genintern.genv in
+  let intern self {Genintern.ltacvars=lfun; genv=env; extra; intern_sign=_; strict_check} c =
     let sigma = Evd.from_env env in
-    let strict_check = ist.Genintern.strict_check in
-    let _, pat = Constrintern.intern_constr_pattern env sigma ~strict_check ~as_type:false c in
+    let ltacvars = {
+      Constrintern.ltac_vars = lfun;
+      ltac_bound = Id.Set.empty;
+      ltac_extra = extra;
+    }
+    in
+    let _, pat = Constrintern.intern_uninstantiated_constr_pattern env sigma ~strict_check ~as_type:false ~ltacvars c in
     GlbVal pat, gtypref t_pattern
   in
   let subst subst c =
@@ -1726,7 +1730,13 @@ let () =
     Patternops.subst_pattern env sigma subst c
   in
   let print env sigma pat = str "pat:(" ++ Printer.pr_lconstr_pattern_env env sigma pat ++ str ")" in
-  let interp _ c = return (Value.of_pattern c) in
+  let interp env c =
+    let ist = to_lvar env in
+    pf_apply ~catch_exceptions:true begin fun env sigma ->
+      let c = Patternops.interp_pattern env sigma ist c in
+      return (Value.of_pattern c)
+    end
+  in
   let obj = {
     ml_intern = intern;
     ml_interp = interp;
@@ -1963,11 +1973,26 @@ let () =
     let f = match kind with
       | ConstrVar -> interp_constr_var_as_constr
       | PretermVar -> interp_preterm_var_as_constr
+      | PatternVar -> assert false
     in
     f ?loc env sigma tycon id
   in
   GlobEnv.register_constr_interp0 wit_ltac2_var_quotation interp
 
+let () =
+  let interp env sigma ist (kind,id) =
+    let () = match kind with
+      | ConstrVar -> assert false (* checked at intern time *)
+      | PretermVar -> assert false
+      | PatternVar -> ()
+    in
+    let ist = Tac2interp.get_env ist.Ltac_pretype.ltac_genargs in
+    let c = Id.Map.find id ist.env_ist in
+    let c = Value.to_pattern c in
+    c
+  in
+  Patternops.register_interp_pat wit_ltac2_var_quotation interp
+
 let () =
   let pr_raw (kind,id) = Genprint.PrinterBasic (fun _env _sigma ->
       let ppkind =
@@ -1981,6 +2006,7 @@ let () =
       let ppkind = match kind with
         | ConstrVar -> mt()
         | PretermVar -> str "preterm:"
+        | PatternVar -> str "pattern:"
       in
       str "$" ++ ppkind ++ Id.print id) in
   let pr_top x = Util.Empty.abort x in

plugins/ltac2/tac2env.ml

@@ -323,6 +323,7 @@ let ltac1_prefix =
 type var_quotation_kind =
   | ConstrVar
   | PretermVar
+  | PatternVar
 
 let wit_ltac2in1 = Genarg.make0 "ltac2in1"
 let wit_ltac2in1_val = Genarg.make0 "ltac2in1val"

plugins/ltac2/tac2env.mli

@@ -175,6 +175,7 @@ val wit_ltac2_constr : (raw_tacexpr, Id.Set.t * glb_tacexpr, Util.Empty.t) genar
 type var_quotation_kind =
   | ConstrVar
   | PretermVar
+  | PatternVar
 
 val wit_ltac2_var_quotation : (lident option * lident, var_quotation_kind * Id.t, Util.Empty.t) genarg_type
 (** Ltac2 quotations for variables "$x" or "$kind:foo" in Gallina terms.

plugins/ltac2/tac2intern.ml

@@ -31,6 +31,7 @@ let t_constr = coq_type "constr"
 let t_ltac1 = ltac1_kn "t"
 let ltac1_lamdba = ltac1_kn "lambda"
 let t_preterm = coq_type "preterm"
+let t_pattern = coq_type "pattern"
 let t_bool = coq_type "bool"
 
 let ltac2_env : Tac2typing_env.t Genintern.Store.field =
@@ -1957,20 +1958,31 @@ let () = Gensubst.register_subst0 wit_ltac2in1 (fun s (ids, e) -> ids, subst_exp
 let () = Gensubst.register_subst0 wit_ltac2in1_val subst_expr
 let () = Gensubst.register_subst0 wit_ltac2_constr (fun s (ids, e) -> ids, subst_expr s e)
 
-let intern_var_quotation ist (kind, { CAst.v = id; loc }) =
+let intern_var_quotation_gen ~ispat ist (kind, { CAst.v = id; loc }) =
   let open Genintern in
   let kind = match kind with
     | None -> ConstrVar
     | Some kind -> match Id.to_string kind.CAst.v with
       | "constr" -> ConstrVar
       | "preterm" -> PretermVar
+      | "pattern" -> PatternVar
       | _ ->
         CErrors.user_err ?loc:kind.loc
           Pp.(str "Unknown Ltac2 variable quotation kind" ++ spc() ++ Id.print kind.v)
   in
   let typ = match kind with
-    | ConstrVar -> t_constr
-    | PretermVar -> t_preterm
+    | ConstrVar ->
+      if ispat
+      then CErrors.user_err ?loc Pp.(str "constr quotations not supported in tactic patterns.")
+      else t_constr
+    | PretermVar ->
+      if ispat
+      then CErrors.user_err ?loc Pp.(str "preterm quotations not supported in tactic patterns.")
+      else t_preterm
+    | PatternVar ->
+      if not ispat
+      then CErrors.user_err ?loc Pp.(str "pattern quotations not supported outside tactic patterns.")
+      else t_pattern
   in
   let env = match Genintern.Store.get ist.extra ltac2_env with
     | None ->
@@ -1993,6 +2005,14 @@ let intern_var_quotation ist (kind, { CAst.v = id; loc }) =
   let () = unify ?loc env t (GTypRef (Other typ, [])) in
   (ist, (kind, id))
 
+let intern_var_quotation = intern_var_quotation_gen ~ispat:false
+
 let () = Genintern.register_intern0 wit_ltac2_var_quotation intern_var_quotation
 
+let intern_var_quotation_pat ?loc ist v =
+  intern_var_quotation_gen ~ispat:true ist v
+
+let () = Genintern.register_intern_pat wit_ltac2_var_quotation
+    intern_var_quotation_pat
+
 let () = Gensubst.register_subst0 wit_ltac2_var_quotation (fun _ v -> v)

plugins/ltac2/tac2quote.mli

@@ -93,7 +93,7 @@ val of_format : lstring -> raw_tacexpr
 
 (** {5 Generic arguments} *)
 
-val wit_pattern : (Constrexpr.constr_expr, Pattern.constr_pattern) Arg.tag
+val wit_pattern : (Constrexpr.constr_expr, [`uninstantiated] Pattern.constr_pattern_r) Arg.tag
 
 val wit_ident : (Id.t, Id.t) Arg.tag
 

pretyping/constr_matching.ml

@@ -285,7 +285,7 @@ let matches_core env sigma allow_bound_rels
     | ConstructRef c, Construct (c',u) -> Environ.QConstruct.equal env c c'
     | _, _ -> false
   in
-  let rec sorec ctx env subst p t =
+  let rec sorec ctx env subst (p:constr_pattern) t =
     let cT = strip_outer_cast sigma t in
     match p, EConstr.kind sigma cT with
       | PSoApp (n,args),m ->

pretyping/detyping.mli

@@ -55,10 +55,10 @@ val detype_rel_context : 'a delay -> constr option -> Id.Set.t -> (names_context
   evar_map -> rel_context -> 'a glob_decl_g list
 
 val share_pattern_names :
-  (Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern -> 'a) -> int ->
+  (Id.Set.t -> names_context -> 'c -> 'd Pattern.constr_pattern_r -> 'a) -> int ->
   (Name.t * binding_kind * 'b option * 'a) list ->
-  Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern ->
-  Pattern.constr_pattern ->
+  Id.Set.t -> names_context -> 'c -> 'd Pattern.constr_pattern_r ->
+  'd Pattern.constr_pattern_r ->
   (Name.t * binding_kind * 'b option * 'a) list * 'a * 'a
 
 val detype_closed_glob :  ?isgoal:bool -> Id.Set.t -> env -> evar_map -> closed_glob_constr -> glob_constr

pretyping/genarg.ml

@@ -206,8 +206,30 @@ struct
       to an extra argument type, otherwise, it will badly fail. *)
   let obj t = get_obj0 @@ get_arg_tag t
 
+  let mem t =
+    let t = get_arg_tag t in
+    GenMap.mem t !arg0_map
+
   (** NB: we need the [Pack] pattern to get [tag]
       from [_ ArgT.DYN.tag] to [(_ * _ * _) ArgT.DYN.tag] *)
   let fold_keys f acc = GenMap.fold (fun (Any (tag,Pack _)) acc -> f (ArgT.Any tag) acc) !arg0_map acc
 
 end
+
+(** Substitution functions *)
+type 'glb subst_fun = Mod_subst.substitution -> 'glb -> 'glb
+
+module SubstObj =
+struct
+  type ('raw, 'glb, 'top) obj = 'glb subst_fun
+  let name = "subst"
+  let default _ = None
+end
+
+module Subst = Register (SubstObj)
+
+let substitute = Subst.obj
+let register_subst0 = Subst.register0
+
+let generic_substitute subs (GenArg (Glbwit wit, v)) =
+  in_gen (glbwit wit) (substitute wit subs v)