Re: [isabelle-dev] [isabelle] Congruence rules for the code preprocessor
On 05/30/2011 06:03 PM, Lukas Bulwahn wrote:
On 05/30/2011 12:33 PM, Andreas Lochbihler wrote:
Hi Lukas,
here is an example that I would have expected to work. However,
congruences seem to work other than I expected. Du you know what I am
missing here?
theory Scratch imports Main begin
definition test where test xs = (last xs = 0)
definition test2 where test2 xs = (xs ~= [] test (rev xs))
(* Optimized implementation for test with context condition *)
lemma test_rev: xs ~= [] == test (rev xs) = (hd xs = 0)
unfolding test_def by(simp add: last_rev)
declare conj_cong[cong] test_rev[simp]
thm test2_def test2_def[simplified]
lemma test2 xs = (xs ~= [] test (rev xs))
apply simp
oops
The [simplified] attribute does apply the test_rev equation, but the
simp method in the proof does. Apparently, the same issue prevents
the code preprocessor from optimizing the code for test:
The simplifier behaves differently when working with free variables or
schematic variables.
Tobias can probably give a more precise answer how it behaves
differently (and why).
I will change the code preprocessor, so that you get the intended
behaviour.
Changeset 027ed67f5d98 enables rewriting with the declared congruence rules.
In the example above, the negation still causes problems (in your
setup), but it works if you define some predicate for xs ~= [] hiding
the negation.
Getting the setup for the code preprocessing simplifier right is of
course an exercise for its users.
It might be worth discussing if the simplified attribute should be
changed to do the same thing.
After an offline discussion with Tobias, I experimented to do the same
with the simplified attribute resulting in the following changeset:
--- a/src/Pure/simplifier.MLTue May 31 18:29:00 2011 +0200
+++ b/src/Pure/simplifier.MLTue May 31 18:32:58 2011 +0200
@@ -321,8 +321,8 @@
val simplified = conv_mode -- Attrib.thms
(fn (f, ths) = Thm.rule_attribute (fn context =
-f ((if null ths then I else Raw_Simplifier.clear_ss)
-(simpset_of (Context.proof_of context)) addsimps ths)));
+singleton (Variable.trade (fn ctxt = map (f ((if null ths then I
else Raw_Simplifier.clear_ss)
+(simpset_of ctxt) addsimps ths))) (Context.proof_of context;
end;
Unfortunately, the provided function Variable.trade renames schematic
variables (even if not necessary), making its behaviour too unexpected
for the users and causing problems with many applications in the
distribution (cf.
http://isabelle.in.tum.de/testboard/Isabelle/rev/330c709f0df9).
A Variable.trade function that at least tries to keep the same schematic
variables (in the obvious cases) would be nice for this setting. But as
long as such a function is not provided, modifying the simplified
attribute leads to problems that are not worth the benefits.
Lukas
Lukas
lemmas [code_inline] = test_rev test_rev[folded List.null_def]
setup {* Code_Preproc.map_pre (fn ss = ss addcongs [@{thm
conj_cong}]) *}
code_thms test2
test2 is still implemented in terms of test (rev xs)
How can I unfold test_rev in test2_def?
Andreas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Congruence rules for the code preprocessor
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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Congruence rules for the code preprocessor
On 05/30/2011 12:33 PM, Andreas Lochbihler wrote:
Hi Lukas,
here is an example that I would have expected to work. However,
congruences seem to work other than I expected. Du you know what I am
missing here?
theory Scratch imports Main begin
definition test where test xs = (last xs = 0)
definition test2 where test2 xs = (xs ~= [] test (rev xs))
(* Optimized implementation for test with context condition *)
lemma test_rev: xs ~= [] == test (rev xs) = (hd xs = 0)
unfolding test_def by(simp add: last_rev)
declare conj_cong[cong] test_rev[simp]
thm test2_def test2_def[simplified]
lemma test2 xs = (xs ~= [] test (rev xs))
apply simp
oops
The [simplified] attribute does apply the test_rev equation, but the
simp method in the proof does. Apparently, the same issue prevents the
code preprocessor from optimizing the code for test:
The simplifier behaves differently when working with free variables or
schematic variables.
Tobias can probably give a more precise answer how it behaves
differently (and why).
I will change the code preprocessor, so that you get the intended behaviour.
It might be worth discussing if the simplified attribute should be
changed to do the same thing.
Lukas
lemmas [code_inline] = test_rev test_rev[folded List.null_def]
setup {* Code_Preproc.map_pre (fn ss = ss addcongs [@{thm
conj_cong}]) *}
code_thms test2
test2 is still implemented in terms of test (rev xs)
How can I unfold test_rev in test2_def?
Andreas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Congruence rules for the code preprocessor
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
