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.
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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe
Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbih...@kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
