[isabelle] SML Code generator and records



Hi all,

I recently encountered the following problem with the SML code generator and record.
I boiled it down to the following example:

record 'a fifo' =
  list1 :: "'a list"
  list2 :: "'a list"

definition fifo_empty':: "'a fifo'" where "fifo_empty' = \<lparr> list1=[], list2=[] \<rparr>"

export_code fifo_empty' in SML
*** Error: Type ('a, unit) Fifo.fifo'_ext_type includes a free type variable Found near val
***    fifo_empty' : ('a, unit) Fifo.fifo'_ext_type = fifo'_ext([ ...])([ ])(()) (line 9 of "generated code")
*** Exception- Fail "Static errors (pass2)" raised
*** At command "export_code".

The generated code is:
structure Fifo =
struct

datatype ('a, 'b) fifo'_ext_type =
  Abs_fifo'_ext_type of ('a list * ('a list * 'b));

fun fifo'_ext list1 list2 more = Abs_fifo'_ext_type (list1, (list2, more));

val fifo_empty' : ('a, unit) fifo'_ext_type = fifo'_ext [] [] ()

end; (*struct Fifo*)

However, when I use a tuple instead of a record, everything is fine.

types 'a fifo = "'a list \<times> 'a list"
definition fifo_empty :: "'a fifo" where "fifo_empty == ([],[])"
export_code fifo_empty in SML -- "No problem"

Is there a workaround if I want to use a record?

Regards and thanks in advance,
  Peter




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