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



Hi Lars,

Am 10.10.2017 um 08:19 schrieb Lars Hupel:
>> 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}
> 
> 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.

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


-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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