Jason Gross (Oct 28 2022 at 22:00): 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.)
Gaëtan Gilbert (Oct 28 2022 at 22:10):you mean like x in
Module F (A:T).
Parameter x : bla.
End F.
?
Jason Gross (Oct 28 2022 at 22:23):Yes
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.)
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.
Gaëtan Gilbert (Oct 31 2022 at 17:16):what's the point of this anyway?
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.
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".
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: Jun 10 2023 at 06:31 UTC