[isabelle] Code equations get eta-contracted



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




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