[isabelle] Lazy Code Generation

Dear all,

I've been experimenting with SML code generation for lazy evaluated codatatypes using the theory Code_Lazy. It's a very nice development, and it works pretty well on some examples. However, I've hit an issue with generated code that seems to be related to polymorphism.

Consider the following example. First, I create the following codatatype and set up the lazy code generator:

codatatype ('e, 'r) itree = Ret 'r | Tau "('e, 'r) itree" | Vis "'e ⇀ ('e, 'r) itree"
code_lazy_type itree

then I create a simple definition

definition deadlock :: "('e, 'r) itree" where "deadlock = Vis Map.empty"

Finally, I try to evaluate this, which invokes the code generator:

value "deadlock :: (int, int) itree"

This raises an error in the generated code:

Error: Type ('a, 'b) itree includes a free type variable
val deadlock : ('a, 'b) itree = Lazy_itree (Lazy.lazy (fn ... => ...))
At (line 155 of "generated code")
Error: Type error in function application.
   Function: term_of_itree typerep_int term_of_int :
      ('a, inta) itree -> term
   Argument: deadlock : ('a, 'b) itree
   Reason: Can't unify inta to 'a (Cannot unify with explicit type variable)

There seems to be an issue with the polymorphic type of deadlock, which cannot be specialised when used in another definition. I attach a minimal example that exhibits this behaviour. I can code generate Haskell for this example (excluding Code_Lazy) without issue. Moreover, if I turn itree into a datatype (i.e. inductive) and don't use code_lazy_type, the code also works correctly.

Is there a workaround for this issue? 



Dr. Simon Foster - Research Fellow in Computer Science
High Integrity Systems Engineering Group, University of York

My normal working hours are 8:30am to 4:30pm Monday to Friday.

Attachment: Lazy.thy
Description: Binary data

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