Stream: Coq devs & plugin devs

Topic: Meaning of subst and discharge in Libobject


view this post on Zulip Julin Shaji (Jan 12 2024 at 08:56):

I was looking at superglobal_object function from Libobject:
https://coq.inria.fr/doc/master/api/coq-core/Libobject/index.html#val-superglobal_object

But couldn't understand what its arguments mean.

I guess cache is like a state.
Is it that subst is modify the cache?
Does discharge see if a element is in cache?

And what is stage from summary.ml ?

view this post on Zulip Gaëtan Gilbert (Jan 12 2024 at 09:04):

look at the big comment at the start of the file
superglobal_object is just a helper where load = cache

view this post on Zulip Julin Shaji (Feb 10 2024 at 16:26):

What does subsitution mean in this context though?

view this post on Zulip Julin Shaji (Feb 10 2024 at 16:58):

The doc page for libobject looked a bit off formatting-wise. I tried to make it better: https://github.com/ju-sh/coq/blob/docfix/library/libobject.mli

Does that look better?

view this post on Zulip Gaëtan Gilbert (Feb 10 2024 at 17:29):

I prefer reading the raw mli over the generated html so no

substitution is module substitution
for instance if you have

Module Type T. Parameter x : nat. Notation y := x. End T.
Module F(A:T).
End F.
Declare Module M : T.
Module N := M.

module type T has a notation object whose interpretation refers to constant T.x
inside functor F we want a notation which refers to A.x instead
the declare module should produce a notation which refers to M.x
etc

view this post on Zulip Julin Shaji (Feb 10 2024 at 17:40):

I prefer reading the raw mli over the generated html so no

I was thinking of making a PR with this.

But if people usually read the mli file itself, this change will
disfigure the comments and make it more uncomfortable to read.

I'll keep this change to myself.

view this post on Zulip Julin Shaji (Feb 10 2024 at 17:41):

module type T has a notation object whose interpretation refers to constant T.x
inside functor F we want a notation which refers to A.x instead
the declare module should produce a notation which refers to M.x
etc

And how can we control this subsitution via the substitution function?

We can choose to make y refer to some other variable of our choice
if want? Is that it?
As in x of some other module?

view this post on Zulip Julin Shaji (Feb 10 2024 at 17:50):


Specifically, I was trying to understand what's happening here:
https://github.com/coq/coq/blob/master/plugins/extraction/table.ml#L657

let inline_extraction : bool * GlobRef.t list -> obj =
  declare_object @@ superglobal_object "Extraction Inline"
    ~cache:(fun (b,l) -> add_inline_entries b l)
    ~subst:(Some (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l))))
    ~discharge:(fun x -> Some x)

For the caching function, what does fun (b,l) -> add_inline_entries b l function do?

view this post on Zulip Julin Shaji (Feb 10 2024 at 17:52):

Its type should be cache_function : 'b -> unit.

view this post on Zulip Julin Shaji (Feb 10 2024 at 17:53):

where 'bis (b:bool, l: a list) if I got that part right.

view this post on Zulip Julin Shaji (Feb 10 2024 at 17:54):

I was also having trouble figuring what the substitution and discharge functions here are doing.

Discharge is like saying what to when a section is closed, right? Why should it (and subst, in this case) return an option? Sorry if this is already mentioned in the docs...

view this post on Zulip Gaëtan Gilbert (Feb 10 2024 at 20:44):

And how can we control this subsitution via the substitution function?

when doing eg Declare Module M : T, the objects of T have their substitution function called with the mod_subst argument being T |-> M
then the load_function is called on the substituted objects (for superglobal_object, the load function and the cache function are the same)

discharge_function returns None when the object does not survive the section, eg a notation
not sure why superglobal_object takes an optional substitution, it should always be Some (NB it's not that the subst_function returns an option, the whole function is the option ie Some (fun _ -> _) instead of fun _ -> Some _)


Last updated: Oct 13 2024 at 01:02 UTC