[isabelle-dev] [isabelle] Congruence rules for the code preprocessor

[Lukas Bulwahn]

On 05/30/2011 10:31 AM, Andreas Lochbihler wrote:
> Thanks Lukas and Florian.
>
> I guess that it *is* a corner case in my specifications, because I 
> have a conditional code equation that implements one constant x in 
> terms of another y. However, I use x only in the equation of another 
> constant z which tests for the precondition first. At the moment, I 
> explicitly the code equation for z with x replaced by y. With 
> congruence rules, that replacement would be automated.
>
> Since this is rather special, I am also happy with the ML setup. 
> However, I recommend that an ML example be added to the code 
> generation tutorial.
>
I will add this ML example to the documentation. Could you provide a 
minimalistic but understandable example of your use case for the 
documentation?


Lukas


> Andreas
>
> Lukas Bulwahn schrieb:
>> Hi Andreas,
>>
>>
>> the following ML line should do the job of adding the congruence rule 
>> in your case:
>>
>> setup {* Code_Preproc.map_pre (fn ss => ss addcongs [@{thm 
>> conj_cong}]) *}
>>
>> Before we add yet another feature to the code generation setup in 
>> Isar, we would like to understand your scenario.
>> Does it occur naturally when setting up the code generator or is it a 
>> very special corner case in your specifications?
>>
>>
>> Lukas
>>
>>
>> On 05/29/2011 04:44 PM, Tobias Nipkow wrote:
>>> Does the current attribute mechanism support selective attributes 
>>> such as [code_inline cong], maybe along the lines of [simp del]? If 
>>> it does, I assume it would be easy to add that information in the 
>>> place that Florian pointed to?
>>>
>>> Tobias
>>>
>>> Am 28/05/2011 14:45, schrieb Florian Haftmann:
>>>> Hi Andreas,
>>>>
>>>>> the code generator tutorial mentions that "the simpset for the code
>>>>> preprocessor can apply the full generality of the Isabelle 
>>>>> simplifier".
>>>>> But how can I add anything else other than unfold theorems? The
>>>>> attributes code_unfold and code_inline do not accept declarations 
>>>>> like
>>>>>
>>>>> declare conj_cong[code_inline cong]
>>>>>
>>>>> Is there a way in Isar to declare congruence rules to the 
>>>>> preprocessor?
>>>>
>>>> no, this can only be done on the ML level, cf.
>>>> http://isabelle.in.tum.de/reports/Isabelle/file/0f9534b7ea75/src/Tools/Code/code_preproc.ML#l10. 
>>>>
>>>>
>>>> Maybe it would be worth thinking about transfering all simpset
>>>> declaration attributes also to code_inline.
>>>>
>>>> Hope this helps,
>>>>     Florian
>>>>
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>>>
>>
>