Stream: MetaCoq

Topic: Determining when a constant is global?


view this post on Zulip Jason Gross (Oct 28 2022 at 22:00):

How do I tell if a kername refers to a valid global constant that will not be removed from the nametab? (It seems that MPdot is used both for modules and for functors.)

view this post on Zulip Gaëtan Gilbert (Oct 28 2022 at 22:10):

you mean like x in

Module F (A:T).
Parameter x : bla.
End F.

?

view this post on Zulip Jason Gross (Oct 28 2022 at 22:23):

Yes

view this post on Zulip Jason Gross (Oct 28 2022 at 22:24):

The issue is that if I do something like

Module F (A : T).
  Definition x := bla.
  Definition qx := ltac:(run_template_program (prog <% x %>) (fun v => exact v)).
End F.

I want to be able to tell in prog whether or not its argument is going to eventually become invalid after functor substitution. (Where "invalid" here means that it will no longer be unquotable.)

view this post on Zulip Jason Gross (Oct 31 2022 at 16:44):

I guess I can check against tmCurrentModPath, but only if there's a way of telling whether or not some component in the current mod path is a functor or not.

view this post on Zulip Gaëtan Gilbert (Oct 31 2022 at 17:16):

what's the point of this anyway?

view this post on Zulip Jason Gross (Oct 31 2022 at 17:26):

I'm trying to write automation for helping me generate functions of type A -> Ast.term for various A (notably for A := Ast.term and A := Σ ;;; Γ |- t : T) such that postcomposing with tmUnquote is more-or-less-provably equal to the identity.

view this post on Zulip Jason Gross (Oct 31 2022 at 17:27):

Since MetaCoq uses FMapAVL and MSetList, I want to write generic quoting functors for these functors. I want to have automation that helps me do this. This means the automation needs to avoid generating things of the form tConstant "<curfile>.QuoteFMapAVL.stuff".

view this post on Zulip Jason Gross (Oct 31 2022 at 17:29):

But the automation should also be able to handle quoting things in the same file --- notably, there are cases where I have Definition A_dec args : {A args} + {~A args} and then I want to be able to autoquote A_dec.


Last updated: Jan 30 2023 at 18:04 UTC