Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] SML Code generator and records

Email Gateway (Aug 18 2022 at 14:06):

From: Peter Lammich <peter.lammich@uni-muenster.de>
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

Email Gateway (Aug 18 2022 at 14:06):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,

this is the infamous ML value restriction. Perhaps it is possible to
circumvent it by

declare fifo_empty'_def [code unfold]

which inlines this definition in-place.

Hope this helps
Florian
signature.asc

Last updated: Apr 27 2024 at 01:05 UTC