Re: [isabelle] Code generation for sorts from locales

Hi 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

your experience boils down to the following

> definition foo :: "'a ⇒ 'b ⇒ 'b"
>   where "foo x = id"
> lemma [code]:
>   "foo (x :: 'a) = (id :: 'a ⇒ 'a)"
>   by (simp add: foo_def)
> export_code foo in Haskell

i.e. currently the code generator accepts code equations which violate
the precondition that the type scheme of the constant in the theorem
(here, 'a => 'a => 'a) must match to the type scheme of the constant in
the theory (here, 'a => 'b => 'b).  I will have to investigate this and
to repair the corresponding check.

Note that in order for your example to work, you must generalize your
interpretation to let A.my_code have a suitable type scheme for my_code.

Thanks a lot,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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