Re: [isabelle] Performing global rewrites on the code setup



Hi Lars,


On 10/10/17 07:52, Lars Hupel wrote:
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?

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. Yes, I got that. That's why I suggested a simproc. The simproc should be called on all
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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.