Email Gateway (Aug 22 2022 at 15:44): Email Gateway (Aug 22 2022 at 15:44):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Isabelle experts,
I noticed that the code generator sometimes eta-contracts the right-hand sides of code
equations when they are declared as [code]. Here is a small artificial example:
declare [[eta_contract = false]]
consts foo :: "'a ⇒ 'a ⇒ 'a"
lemma [code equation]: "foo x y = foldr (λx y. foo (id x) y) [y] x" sorry
code_thms foo
Here, code_thms displays foo's code equation as
foo ?x ?y ≡ foldr (λx. foo (id x)) [?y] ?x
instead of
foo ?x ?y = foldr (λx y. foo (id x) y) [?y] ?x
Why is this contraction happening and can I disable it? My problem with the
eta-contraction is that it prevents subsequent [code_unfold] equations from rewriting the
expressions because the equations expect a certain number of arguments. My idea was that
users can control the rewriting by the number of arguments they state in the code
equation, but eta contracting the right-hand sides breaks this.
Andreas
Email Gateway (Aug 22 2022 at 15:45):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
Why is this contraction happening and can I disable it? My problem with> the eta-contraction is that it prevents subsequent [code_unfold]>
equations from rewriting the expressions because the equations expect a>
certain number of arguments. My idea was that users can control the>
rewriting by the number of arguments they state in the code equation,>
but eta contracting the right-hand sides breaks this.
I guess this is due to the internal rewriting of code equations, which
uses common Isabelle infrastructure where spontaneous eta-expansion or
-contraction can happen.
I don't see a way to lift this in the short run.
Cheers,
Florian
signature.asc
Last updated: Apr 24 2024 at 04:17 UTC