Merge PR coq#17667: Support quotations (genargs) in patterns

Reviewed-by: ppedrot
Co-authored-by: ppedrot <[email protected]>

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

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

doc/changelog/06-Ltac2-language/17667-pattern-quotations.rst

@@ -0,0 +1,5 @@
+- **Added:**
+  Ltac2 supports pattern quotations when building `pattern` values.
+  This allows building dynamic patterns, eg `Ltac2 eq_pattern a b := pattern:($pattern:a = $pattern:b)`
+  (`#17667 <https://github.com/coq/coq/pull/17667>`_,
+  by Gaëtan Gilbert).

doc/sphinx/proof-engine/ltac2.rst

@@ -777,6 +777,15 @@ Similarly variables of type `preterm` have an antiquotation
 
 It is equivalent to pretyping the preterm with the appropriate typing constraint.
 
+Variables of type `pattern` have an antiquotation
+
+.. prodn:: term += $pattern:@lident
+
+Its use is only allowed when producing a pattern, i.e.
+`pattern:($pattern:x -> True)` is allowed but
+`constr:($pattern:x -> True)` is not allowed. Conversely `constr` and `preterm`
+antiquotations are not allowed when producing a pattern.
+
 Match over terms
 ~~~~~~~~~~~~~~~~
 

interp/constrextern.ml

@@ -1399,7 +1399,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) ->
@@ -1422,6 +1437,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
       GVar id
   | PMeta None -> GHole (GInternalHole)
   | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n)
+  | PUninstantiated (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) ->
@@ -1446,15 +1462,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
@@ -1469,7 +1485,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.")
@@ -1515,18 +1531,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

@@ -2399,7 +2399,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 *)
@@ -2739,6 +2743,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

@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Mod_subst
 open Genarg
 
 module Store = Store.Make ()
@@ -50,7 +49,6 @@ type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr optio
 type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern
 
 type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
-type 'glb subst_fun = substitution -> 'glb -> 'glb
 type 'glb ntn_subst_fun = Id.Set.t -> Glob_term.glob_constr Id.Map.t -> 'glb -> 'glb
 
 module InternObj =
@@ -60,13 +58,6 @@ struct
   let default _ = None
 end
 
-module SubstObj =
-struct
-  type ('raw, 'glb, 'top) obj = 'glb subst_fun
-  let name = "subst"
-  let default _ = None
-end
-
 module NtnSubstObj =
 struct
   type ('raw, 'glb, 'top) obj = 'glb ntn_subst_fun
@@ -75,7 +66,6 @@ struct
 end
 
 module Intern = Register (InternObj)
-module Subst = Register (SubstObj)
 module NtnSubst = Register (NtnSubstObj)
 
 let intern = Intern.obj
@@ -85,15 +75,26 @@ let generic_intern ist (GenArg (Rawwit wit, v)) =
   let (ist, v) = intern wit ist v in
   (ist, in_gen (glbwit wit) v)
 
-(** Substitution functions *)
+type ('raw,'glb) intern_pat_fun = ?loc:Loc.t -> ('raw,'glb) intern_fun
 
-let substitute = Subst.obj
-let register_subst0 = Subst.register0
+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 generic_substitute subs (GenArg (Glbwit wit, v)) =
-  in_gen (glbwit wit) (substitute wit subs v)
+let intern_pat = InternPat.obj
 
-let () = Hook.set Detyping.subst_genarg_hook generic_substitute
+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 *)
 

interp/genintern.mli

@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Mod_subst
 open Genarg
 
 module Store : Store.S
@@ -47,14 +46,13 @@ val intern : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb) intern_fun
 
 val generic_intern : (raw_generic_argument, glob_generic_argument) intern_fun
 
-(** {5 Substitution functions} *)
+(** {5 Internalization in tactic patterns} *)
 
-type 'glb subst_fun = substitution -> 'glb -> 'glb
-(** The type of functions used for substituting generic arguments. *)
+type ('raw,'glb) intern_pat_fun = ?loc:Loc.t -> ('raw,'glb) intern_fun
 
-val substitute : ('raw, 'glb, 'top) genarg_type -> 'glb subst_fun
+val intern_pat : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb) intern_pat_fun
 
-val generic_substitute : glob_generic_argument subst_fun
+val generic_intern_pat : (raw_generic_argument, glob_generic_argument) intern_pat_fun
 
 (** {5 Notation functions} *)
 
@@ -69,8 +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_subst0 : ('raw, 'glb, 'top) genarg_type ->
-  'glb subst_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

interp/notation_ops.ml

@@ -919,7 +919,7 @@ let rec subst_notation_constr subst bound raw =
     else NHole nknd
 
   | NGenarg arg ->
-    let arg' = Genintern.generic_substitute subst arg in
+    let arg' = Gensubst.generic_substitute subst arg in
     if arg' == arg then raw
     else NGenarg arg'
 

plugins/ltac/tacentries.ml

@@ -830,7 +830,7 @@ let in_tacval =
   let intern_fun _ e = Empty.abort e in
   let subst_fun s v = v in
   let () = Genintern.register_intern0 wit intern_fun in
-  let () = Genintern.register_subst0 wit subst_fun in
+  let () = Gensubst.register_subst0 wit subst_fun in
   (* No need to register a value tag for it via register_val0 since we will
      never access this genarg directly. *)
   let interp_fun ist tac =
@@ -871,7 +871,7 @@ type ('a, 'b) argument_intern =
 | ArgInternWit : ('a, 'b, 'c) Genarg.genarg_type -> ('a, 'b) argument_intern
 
 type 'b argument_subst =
-| ArgSubstFun : 'b Genintern.subst_fun -> 'b argument_subst
+| ArgSubstFun : 'b Gensubst.subst_fun -> 'b argument_subst
 | ArgSubstWit : ('a, 'b, 'c) Genarg.genarg_type -> 'b argument_subst
 
 type ('b, 'c) argument_interp =
@@ -898,7 +898,7 @@ match arg.arg_intern with
     let ans = Genarg.out_gen (glbwit wit) (Tacintern.intern_genarg ist (Genarg.in_gen (rawwit wit) v)) in
     (ist, ans)
 
-let subst_fun (type a b c) (arg : (a, b, c) tactic_argument) : b Genintern.subst_fun =
+let subst_fun (type a b c) (arg : (a, b, c) tactic_argument) : b Gensubst.subst_fun =
 match arg.arg_subst with
 | ArgSubstFun f -> f
 | ArgSubstWit wit ->
@@ -923,7 +923,7 @@ match arg.arg_interp with
 let argument_extend (type a b c) ~plugin ~name (arg : (a, b, c) tactic_argument) =
   let wit = Genarg.create_arg name in
   let () = Genintern.register_intern0 wit (intern_fun name arg) in
-  let () = Genintern.register_subst0 wit (subst_fun arg) in
+  let () = Gensubst.register_subst0 wit (subst_fun arg) in
   let tag = match arg.arg_tag with
   | None ->
     let () = register_val0 wit None in

plugins/ltac/tacentries.mli

@@ -156,7 +156,7 @@ type ('a, 'b) argument_intern =
 | ArgInternWit : ('a, 'b, 'c) Genarg.genarg_type -> ('a, 'b) argument_intern
 
 type 'b argument_subst =
-| ArgSubstFun : 'b Genintern.subst_fun -> 'b argument_subst
+| ArgSubstFun : 'b Gensubst.subst_fun -> 'b argument_subst
 | ArgSubstWit : ('a, 'b, 'c) Genarg.genarg_type -> 'b argument_subst
 
 type ('b, 'c) argument_interp =

plugins/ltac/tacinterp.ml

@@ -2061,7 +2061,7 @@ let def_interp ist x = Ftactic.return x
 
 let declare_uniform t =
   Genintern.register_intern0 t def_intern;
-  Genintern.register_subst0 t def_subst;
+  Gensubst.register_subst0 t def_subst;
   register_interp0 t def_interp
 
 let () =

plugins/ltac/tacsubst.ml

@@ -272,29 +272,29 @@ and subst_genarg subst (GenArg (Glbwit wit, x)) =
     let q = out_gen (glbwit wit2) (subst_genarg subst (in_gen (glbwit wit2) q)) in
     in_gen (glbwit (wit_pair wit1 wit2)) (p, q)
   | ExtraArg s ->
-      Genintern.generic_substitute subst (in_gen (glbwit wit) x)
+      Gensubst.generic_substitute subst (in_gen (glbwit wit) x)
 
 (** Registering *)
 
 let () =
-  Genintern.register_subst0 wit_int_or_var (fun _ v -> v);
-  Genintern.register_subst0 wit_nat_or_var (fun _ v -> v);
-  Genintern.register_subst0 wit_ref subst_global_reference;
-  Genintern.register_subst0 wit_smart_global subst_global_reference;
-  Genintern.register_subst0 wit_pre_ident (fun _ v -> v);
-  Genintern.register_subst0 wit_ident (fun _ v -> v);
-  Genintern.register_subst0 wit_hyp (fun _ v -> v);
-  Genintern.register_subst0 wit_intropattern subst_intro_pattern [@warning "-3"];
-  Genintern.register_subst0 wit_simple_intropattern subst_intro_pattern;
-  Genintern.register_subst0 wit_tactic subst_tactic;
-  Genintern.register_subst0 wit_ltac subst_tactic;
-  Genintern.register_subst0 wit_constr subst_glob_constr;
-  Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v);
-  Genintern.register_subst0 wit_uconstr (fun subst c -> subst_glob_constr subst c);
-  Genintern.register_subst0 wit_open_constr (fun subst c -> subst_glob_constr subst c);
-  Genintern.register_subst0 Redexpr.wit_red_expr subst_redexp;
-  Genintern.register_subst0 wit_quant_hyp subst_declared_or_quantified_hypothesis;
-  Genintern.register_subst0 wit_bindings subst_bindings;
-  Genintern.register_subst0 wit_constr_with_bindings subst_glob_with_bindings;
-  Genintern.register_subst0 wit_destruction_arg subst_destruction_arg;
+  Gensubst.register_subst0 wit_int_or_var (fun _ v -> v);
+  Gensubst.register_subst0 wit_nat_or_var (fun _ v -> v);
+  Gensubst.register_subst0 wit_ref subst_global_reference;
+  Gensubst.register_subst0 wit_smart_global subst_global_reference;
+  Gensubst.register_subst0 wit_pre_ident (fun _ v -> v);
+  Gensubst.register_subst0 wit_ident (fun _ v -> v);
+  Gensubst.register_subst0 wit_hyp (fun _ v -> v);
+  Gensubst.register_subst0 wit_intropattern subst_intro_pattern [@warning "-3"];
+  Gensubst.register_subst0 wit_simple_intropattern subst_intro_pattern;
+  Gensubst.register_subst0 wit_tactic subst_tactic;
+  Gensubst.register_subst0 wit_ltac subst_tactic;
+  Gensubst.register_subst0 wit_constr subst_glob_constr;
+  Gensubst.register_subst0 wit_clause_dft_concl (fun _ v -> v);
+  Gensubst.register_subst0 wit_uconstr (fun subst c -> subst_glob_constr subst c);
+  Gensubst.register_subst0 wit_open_constr (fun subst c -> subst_glob_constr subst c);
+  Gensubst.register_subst0 Redexpr.wit_red_expr subst_redexp;
+  Gensubst.register_subst0 wit_quant_hyp subst_declared_or_quantified_hypothesis;
+  Gensubst.register_subst0 wit_bindings subst_bindings;
+  Gensubst.register_subst0 wit_constr_with_bindings subst_glob_with_bindings;
+  Gensubst.register_subst0 wit_destruction_arg subst_destruction_arg;
   ()