[isabelle] Code generation for sorts from locales



Hi all,

I've stumbled across a problem with the dictionary trick for sorts. I'm generating code from locales following the guidelines in "Code generation from Isabelle/HOL theories" (the Haftmann trick, as Lukas calls it).

Attached is a reduced example where the resulting code contains non-linear patterns (for the sort arguments) in the generated ML-functions (same for Isabelle2012 and e.g. ac2e29fc57a5).

Am I doing something wrong?

Best wishes,
Dmitriy
theory Code
imports Main
begin

locale A =
fixes b :: 'b
and ba :: "'b \<Rightarrow> 'a :: linorder"
and baa :: "'b \<Rightarrow> 'a \<Rightarrow> 'a :: linorder"
assumes "baa b a = a"
begin

definition code :: "'a \<Rightarrow> 'a" where
  "code a = baa b a"

end

definition my_code where [code del]: "my_code \<equiv> \<lambda>a. A.code a (\<lambda>_. id)"

interpretation A as id "\<lambda>_. id" where "A.code as (\<lambda>_. id) = my_code as" sorry

export_code my_code in SML

end


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