Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Question about Code Generator


view this post on Zulip Email Gateway (Aug 18 2022 at 14:16):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi,

I have defined some datatype using typedef, it encapsulates some
data-structure together with its invariant, for example distinct lists
(used to implement sets here):

typedef 'a lset = "{ l::'a list . distinct l }"

by auto

On this, I can define operations, e.g.:

definition "ls_empty == Abs_lset []"

definition "ls_\<alpha> l == set (Rep_lset l)"

definition "ls_memb x l == x mem (Rep_lset l)"

definition "ls_ins x l == if ls_memb x l then l else Abs_lset (x #
Rep_lset l)"

...

My question is, how to setup the code generator such that it implements "'a
lset" by "'a list", or, in general, in the same way as it would
implement the underlying datatype ?

With no further ado, the code generator complains about missing code
equations:

export_code ls_empty ls_memb ls_ins in SML file -

*** No code equations for Rep_lset, Abs_lset

*** At command "export_code".

Regards and thanks in advance for any help/pointers to examples
Peter

view this post on Zulip Email Gateway (Aug 18 2022 at 14:16):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi,

I have defined some datatype using typedef, it encapsulates some
data-structure together with its invariant, for example distinct lists
(used to implement sets here):

typedef 'a lset = "{ l::'a list . distinct l }"

by auto

On this, I can define operations, e.g.:

definition "ls_empty == Abs_lset []"

definition "ls_\<alpha> l == set (Rep_lset l)"

definition "ls_memb x l == x mem (Rep_lset l)"

definition "ls_ins x l == if ls_memb x l then l else Abs_lset (x #
Rep_lset l)"

...

My question is, how to setup the code generator such that it implements "'a
lset" by "'a list", or, in general, in the same way as it would
implement the underlying datatype ?

With no further ado, the code generator complains about missing code
equations:

export_code ls_empty ls_memb ls_ins in SML file -

*** No code equations for Rep_lset, Abs_lset

*** At command "export_code".

Regards and thanks in advance for any help/pointers to examples
Peter


Last updated: Mar 29 2024 at 12:28 UTC