[isabelle-dev] Towards the Isabelle2017 release

[Thiemann, Rene]

Dear Florian,

>> - There have been some changes w.r.t. code-generation which now lead
>>  to runtime exception in the generated code. For instance, now
>>  I get code like
>>  “f x = Code.abort …”
>>  whereas in 2016-1 there was a proper code like
>>  “f x = some ordinary right-hand side”
>>  We did not yet isolate the problem and will report later.
> 
> OK, I will dig into this after you have isolated it.  Might be well that
> this only occurs on certain theory merges.

The problem seems to be a change wrt. locale interpretations.

Consider the following code:

=====
locale foo = fixes f :: "nat => nat"
  assumes f_mono[termination_simp]: "f x <= x"
begin

fun bar :: "nat => nat" where
  "bar 0 = 0"
| "bar (Suc x) = Suc (bar (f x))"

end

definition com where
  [code del]: "com = foo.bar id"

interpretation foo id
  rewrites "foo.bar id = com"
  unfolding com_def by (unfold_locales, auto)

lemma "com 5 = 5" by eval
export_code com in Haskell
=====


This works perfectly fine in Isabelle 2016-1, and especially
the [code del] is required to make the final export_code and eval succeed.

In contrast, in a recent development version, the [code del] still is accepted,
but the export_code will deliver “com _ = error …” and the “eval” will fail.

The solution is easy: remove the previously required [code del].

Cheers,
René
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 842 bytes
Desc: Message signed with OpenPGP
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170828/b1fb13a2/attachment.sig>