Stream: Elpi users & devs

Topic: Functors


view this post on Zulip Gordon Stewart (Jan 25 2022 at 15:04):

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.

view this post on Zulip Enrico Tassi (Jan 25 2022 at 18:10):

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.

view this post on Zulip Enrico Tassi (Jan 25 2022 at 18:11):

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

view this post on Zulip Enrico Tassi (Jan 25 2022 at 18:11):

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

view this post on Zulip Gordon Stewart (Jan 25 2022 at 18:19):

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.

view this post on Zulip Gordon Stewart (Jan 25 2022 at 21:21):

The {{z}} thing was indeed a phase mismatch; thanks!


Last updated: Feb 04 2023 at 02:03 UTC