Skip to content

GenConstr can intern directly to constr #22106

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
coqbot-app merged 2 commits into from
Aug 26, 2026
+69 −37
Merged

GenConstr can intern directly to constr #22106

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
92ccb7b
GenConstr can intern directly to constr
SkySkimmer Jun 8, 2026
9623c35
Remove the overlay.
ppedrot Aug 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions dev/ci/user-overlays/22106-SkySkimmer-intern-gen.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
overlay elpi https://github.com/SkySkimmer/coq-elpi intern-gen 22106
69 changes: 40 additions & 29 deletions interp/constrintern.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2585,6 +2585,35 @@ let appexpl self genv env lvar ?loc ((ref,us), args) =
if args = [] then DAst.make ?loc @@ GApp (f,[])
else apply_args self genv env lvar loc f (List.map fst args)

let genarg_gen self genv env lvar ?loc gen =
let (ltacvars, ntnvars) = lvar in
(* Preventively declare notation variables in ltac as non-bindings *)
Id.Map.iter (fun x status -> status.Genintern.ntnvar_used_as_binder <- false) ntnvars;
let extra = ltacvars.ltac_extra in
(* We inform ltac that the interning vars and the notation vars are bound *)
(* but we could instead rely on the "intern_sign" *)
let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in
let lvars = Id.Set.union lvars (Id.Map.domain ntnvars) in
let ltacvars = Id.Set.union lvars env.ids in
(* Propagating enough information for mutual interning with tac-in-term *)
let intern_sign = {
Genintern.intern_ids = env.ids;
Genintern.intern_univs = env.local_univs.bound;
Genintern.notation_variable_status = ntnvars
} in
let ist = {
Genintern.genv;
ltacvars;
extra;
intern_sign;
strict_check = match env.strict_check with None -> false | Some b -> b;
} in
let intern = if env.pattern_mode
then Genintern.generic_intern_pat
else Genintern.generic_intern_constr
in
intern ?loc ist gen

let app self genv env lvar ?loc (f, args) =
let intern env = intern self genv env lvar in
let apply_impargs env = apply_impargs self genv env lvar in
Expand All @@ -2600,6 +2629,13 @@ let app self genv env lvar ?loc (f, args) =
| CNotation (_,ntn,ntnargs) ->
let c = intern_notation intern env (snd lvar) loc ntn ntnargs in
apply_impargs env loc c args
| CGenarg gen ->
let f, info = genarg_gen self genv env lvar ?loc:f.loc gen in
if info.passthrough_impls then
apply_impargs env loc f args
else
let args = extract_regular_arguments args in
apply_args env loc f args
| _ ->
let f = intern_no_implicit self genv env lvar f in
let args = extract_regular_arguments args in
Expand Down Expand Up @@ -2746,35 +2782,10 @@ let hole self genv env lvar ?loc k =
GHole k

let genarg self genv env lvar ?loc gen =
let (ltacvars, ntnvars) = lvar in
(* Preventively declare notation variables in ltac as non-bindings *)
Id.Map.iter (fun x status -> status.Genintern.ntnvar_used_as_binder <- false) ntnvars;
let extra = ltacvars.ltac_extra in
(* We inform ltac that the interning vars and the notation vars are bound *)
(* but we could instead rely on the "intern_sign" *)
let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in
let lvars = Id.Set.union lvars (Id.Map.domain ntnvars) in
let ltacvars = Id.Set.union lvars env.ids in
(* Propagating enough information for mutual interning with tac-in-term *)
let intern_sign = {
Genintern.intern_ids = env.ids;
Genintern.intern_univs = env.local_univs.bound;
Genintern.notation_variable_status = ntnvars
} in
let ist = {
Genintern.genv;
ltacvars;
extra;
intern_sign;
strict_check = match env.strict_check with None -> false | Some b -> b;
} in
let intern = if env.pattern_mode
then Genintern.generic_intern_pat
else Genintern.generic_intern_constr
in
let glb = intern ?loc ist gen in
DAst.make ?loc @@
GGenarg glb
let c, info = genarg_gen self genv env lvar ?loc gen in
if info.passthrough_impls then
apply_impargs self genv env lvar loc c []
else c

let genargglob self genv env lvar ?loc gen =
DAst.make ?loc @@ GGenarg gen
Expand Down
25 changes: 19 additions & 6 deletions interp/genintern.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,8 +67,18 @@ end

type ('raw, 'glb) constr_intern_fun = ?loc:Loc.t -> glob_sign -> 'raw -> 'glb

type constr_intern_info = { passthrough_impls : bool }

let default_info = { passthrough_impls = false }

let wrap_constr_intern (type raw glb) (tag:(raw,glb) GenConstr.tag) (f:(raw, glb) constr_intern_fun)
: (raw, Glob_term.glob_constr * constr_intern_info) constr_intern_fun =
fun ?loc ist v ->
let v = f ?loc ist v in
DAst.make ?loc @@ Glob_term.GGenarg (Glb (tag, v)), default_info

module CInternObj = struct
type ('r, 'g) t = ('r, 'g) constr_intern_fun
type ('r, _) t = ('r, Glob_term.glob_constr * constr_intern_info) constr_intern_fun
end

module NtnSubstObj =
Expand All @@ -82,23 +92,26 @@ module NtnSubst = GenConstr.Register (NtnSubstObj)

let intern = Intern.obj
let register_intern0 = Intern.register0
let register_intern_constr = CIntern.register
let register_intern_constr_gen = CIntern.register
let register_intern_constr tag f =
register_intern_constr_gen tag (wrap_constr_intern tag f)

let generic_intern ist (GenArg (Rawwit wit, v)) =
let (ist, v) = intern wit ist v in
(ist, in_gen (glbwit wit) v)

let generic_intern_constr ?loc ist (GenConstr.Raw (tag, v)) =
let internf = CIntern.get tag in
GenConstr.Glb (tag, internf ?loc ist v)
internf ?loc ist v

module InternPatObj = struct
type ('raw, 'glb) t = ('raw, 'glb) constr_intern_fun
type ('raw, _) t = ('raw, Glob_term.glob_constr * constr_intern_info) constr_intern_fun
end

module InternPat = GenConstr.Register (InternPatObj)

let register_intern_pat = InternPat.register
let register_intern_pat_gen = InternPat.register
let register_intern_pat tag f = register_intern_pat_gen tag (wrap_constr_intern tag f)

let generic_intern_pat ?loc ist (GenConstr.Raw (tag, v)) =
match InternPat.find_opt tag with
Expand All @@ -107,7 +120,7 @@ let generic_intern_pat ?loc ist (GenConstr.Raw (tag, v)) =
CErrors.user_err ?loc Pp.(str "This quotation is not supported in tactic patterns (" ++ str name ++ str ").")
| Some internf ->
let v = internf ?loc ist v in
GenConstr.Glb (tag, v)
v

(** Notation substitution *)

Expand Down
12 changes: 10 additions & 2 deletions interp/genintern.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,15 +51,17 @@ type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb

type ('raw, 'glb) constr_intern_fun = ?loc:Loc.t -> glob_sign -> 'raw -> 'glb

type constr_intern_info = { passthrough_impls : bool }

@SkySkimmer SkySkimmer Aug 20, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

instead of telling the interner to look at the produced term we could return the data produced by find appl_head_data (as used in

rocq/interp/constrintern.ml

Line 2317 in 9fa45ea

let head, impls, subscopes = find_appl_head_data genv env lvar c in
) directly
That would allow genargs to have implicits even when interning to GGenarg
not sure if worth doing


val intern : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb) intern_fun

val generic_intern : (raw_generic_argument, glob_generic_argument) intern_fun

val generic_intern_constr : (GenConstr.raw, GenConstr.glb) constr_intern_fun
val generic_intern_constr : (GenConstr.raw, Glob_term.glob_constr * constr_intern_info) constr_intern_fun

(** {5 Internalization in tactic patterns} *)

val generic_intern_pat : (GenConstr.raw, GenConstr.glb) constr_intern_fun
val generic_intern_pat : (GenConstr.raw, Glob_term.glob_constr * constr_intern_info) constr_intern_fun

(** {5 Notation functions} *)

Expand All @@ -83,6 +85,12 @@ val register_intern_constr : ('raw, 'glb) GenConstr.tag ->
val register_intern_pat : ('raw, 'glb) GenConstr.tag ->
('raw, 'glb) constr_intern_fun -> unit

val register_intern_constr_gen : ('raw, Util.Empty.t) GenConstr.tag ->
('raw, Glob_term.glob_constr * constr_intern_info) constr_intern_fun -> unit

val register_intern_pat_gen : ('raw, Util.Empty.t) GenConstr.tag ->
('raw, Glob_term.glob_constr * constr_intern_info) constr_intern_fun -> unit

val register_ntn_subst0 : (_, 'glb) GenConstr.tag -> 'glb ntn_subst_fun -> unit

(** Used to compute the set of used notation variables during internalization.*)
Expand Down
Loading