[isabelle] Code generation for sorts from locales
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] Code generation for sorts from locales
- From: Dmitriy Traytel <traytel at in.tum.de>
- Date: Sat, 15 Sep 2012 22:16:36 +0200
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:15.0) Gecko/20120827 Thunderbird/15.0
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
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?
locale A =
fixes b :: 'b
and ba :: "'b \<Rightarrow> 'a :: linorder"
and baa :: "'b \<Rightarrow> 'a \<Rightarrow> 'a :: linorder"
assumes "baa b a = a"
definition code :: "'a \<Rightarrow> 'a" where
"code a = baa b a"
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and