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