Hi, Enrico.

It seems functors aren't yet supported?

I did some very initial experiments (https://github.com/gstew5/coq-elpi) to see how hard it would be to add them, and got far enough to see the following new test case (`test_API.v`

) fail:

```
Elpi Query lp:{{
std.do! [
coq.env.begin-module-type "TF" [],
coq.env.add-axiom "w" {{nat}} _,
coq.env.end-module-type MP_TF,
coq.locate-module-type "TA" MP_TA,
coq.env.begin-module "F" (some MP_TF) [pr "a" MP_TA, pr "b" MP_TA],
coq.env.import-module {coq.locate-module "a"},
coq.env.add-const "w" {{z}} _ _ _, %<-- This fails unexpectedly ("z not found").
coq.env.end-module _
]
}}.
Print F.
Module B := F A A.
Print B.
Print B.w.
```

The module type `TA`

is defined above this point as:

```
coq.env.begin-module-type "TA" [],
coq.env.add-axiom "z" {{nat}} _,
coq.env.add-axiom "i" {{Type}} _,
coq.env.end-module-type MP_TA,
```

I've never hacked on Coq before so it's likely that some part of what I'm doing in `coq_elpi_builtins.ml`

is wrong:

```
(* XXX When Coq's API allows it, call vernacentries directly *)
MLCode(Pred("coq.env.begin-module",
In(id, "Name",
In(option modtypath, "ModTyPath",
In(list (pair id modtypath), "Functor arguments",
Full(unit_ctx, "Starts a module, the modtype can be omitted *E*")))),
(fun name mp binders_ast ~depth _ _ -> on_global_state "coq.env.begin-module" (fun state ->
if Global.sections_are_opened () then
err Pp.(str"This elpi code cannot be run within a section since it opens a module");
let ty =
match mp with
| None -> Declaremods.Check []
| Some mp ->
let fpath = Nametab.path_of_modtype mp in
let tname = Constrexpr.CMident (Libnames.qualid_of_path fpath) in
Declaremods.(Enforce (CAst.make tname, DefaultInline)) in
let id = Id.of_string name in
let binders_ast =
List.map (fun (farg_id,farg_mp) ->
let fpath = Nametab.path_of_modtype farg_mp in
let tname = Constrexpr.CMident (Libnames.qualid_of_path fpath) in
[CAst.make (Id.of_string farg_id)], (CAst.make tname, Declaremods.DefaultInline))
binders_ast in
let _mp = Declaremods.start_module None id binders_ast ty in
state, (), []))),
DocAbove);
```

Alternatively, maybe I'm severely underestimating what has to change to support functors? I don't fully understand the coq-elpi codebase yet but did notice some `nYI "functors"`

in various places.

About `{{z}}`

I think it is just that quotations are expanded at compilation time, not at run time. For that you may use `coq.locate`

.

See https://github.com/LPCIC/coq-elpi/blob/f2d3c3da556629713407b95631fd487adf9e03ca/coq-builtin.elpi#L715 (it seems the same problem).

I'll look at the code tomorrow, no time now. Also, feel free to open a PR.

Thanks, Enrico. Here's a PR for easier review: https://github.com/LPCIC/coq-elpi/pull/332. I get your point about `{{z}}`

and will try to fix it in the PR a bit later today.

The `{{z}}`

thing was indeed a phase mismatch; thanks!

Last updated: Jun 06 2023 at 23:01 UTC