[isabelle] Code Generation for Executable Sets



I'm trying to generate code from a model that defines numerous sets and
relations.

Currently, I am importing theory Executable_Set (from HOL/Library).
There is a dire warning in this theory: "avoid using this at any cost!"
Is there a better option then?  I'd rather not rephrase the model in
terms of lists everywhere.

With Executable_Set imported, the generated code unfortunately is not
type-correct.  The code generator confuses "'a => bool" with "'a set".
My own functions are generated with the former type, while functions
from Executable_Set expect the latter.  (The problem shows up when one
tries to type-check code generated from the attached theory.)

Fortunately, it seems that I can work around this issue by using
Code.add_signature_cmd.  Is this the suggested solution?

Unfortunately, I haven't yet figured out how to extend this workaround
to records with fields of set type (again, see the attached theory).
Any advice would be appreciated.

Tjark
theory Example imports Executable_Set
begin

definition "foo (x::'a set) \<equiv> x \<subseteq> x"

export_code foo in SML file -  -- {* generated code is not type correct *}

setup {*
  Code.add_signature_cmd ("foo", "'a set \<Rightarrow> bool")
*}

export_code foo in SML file -  -- {* now it works *}


record 'a rec = field :: "'a set"

export_code field in SML file -  -- {* @{const field} gets type @{typ
  "('a, 'b) rec_ext_type \<Rightarrow> 'a \<Rightarrow> bool"} *}

setup {*
  Code.add_signature_cmd ("field", "('a, 'b) rec_ext_type \<Rightarrow> 'a set")
*}

export_code field in SML file -  -- {* now @{const field} has the right
  type, but the code is no longer type-correct (because the underlying
  record implementation is still using @{typ "'a \<Rightarrow> bool"}) *}

end


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