Email Gateway (Aug 18 2022 at 14:16): 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
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: Nov 21 2024 at 12:39 UTC