Email Gateway (Aug 22 2022 at 16:13): Email Gateway (Aug 22 2022 at 16:13):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I am trying to apply a function "thm list -> thm list" to the global set
of code equations. I thought "functrans" allow me to do that, but
apparently they only work locally (i.e. on a single function). My use
case is to unfold all constants of arity zero.
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:14):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Lars,
Function transformers are indeed only called on a single function at a time. Moreover,
they are not called at all on functions with abstract code equations (of the form Rep (f
x) = ...). They are mainly used to change the pattern-matching structure of functions.
As unfolding should only be done on the right-hand sides of the equations, I wonder why
you don't just write a simproc that you add to the preprocessor simpset?
Andreas
Email Gateway (Aug 22 2022 at 16:14):From: Lars Hupel <hupel@in.tum.de>
Hi Andreas,
I don't know all the constants and their code equations in advance. I
literally want to unfold all constants with arity zero that are in the
set of "code_thms" for a specific function. Otherwise I could just
declare them as "[code_unfold]" when I define them.
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:14):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Lars,
atoms of a term. If the atom is a constant, then it can get the code equations for the
constant and look whether it does not take any argument. If so, use the code equation to
generate the unfolding theorem.
You can get the code equations for a specific constant from the context by
Code.get_cert @{context} [] @{const_name map} |> Code.equations_of_cert @{theory}
Andreas
Email Gateway (Aug 22 2022 at 16:14):From: Lars Hupel <hupel@in.tum.de>
Could this could be problematic because of potential loops where
something in the preprocessor of the code will invoke the preprocessor
again to obtain code equations? In any case, I'll try it out and let you
know.
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:14):From: Lars Hupel <hupel@in.tum.de>
It looks like it works. As a precautionary measure, I have wrapped the
simproc into a declaration flag so that I can disable it further down
the recursive invocation.
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:18):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lars,
Code.get_cert @{context} [] does not involve any preprocessing.
What you are definitely loosing is the case that functions transformers
would reduce the number of arguments to 0.
Hope this helps,
Florian
signature.asc
Last updated: Apr 25 2024 at 20:15 UTC