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 ?

look at the big comment at the start of the file

superglobal_object is just a helper where load = cache

What does subsitution mean in this context though?

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?

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

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.

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?

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?

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

.

where `'b`

is `(b:bool, l: a list)`

if I got that part right.

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...

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