Re: [isabelle] Lazy Code Generation



Dear Simon,

You're running into SML's value restriction, which is independent of codatatypes and code_lazy. See http://users.cis.fiu.edu/~smithg/cop4555/valrestr.html for an explanation. Deadlock's right-hand side consists of a number of function applications and is therefore not a syntactic ML value. So SML will not treat it as a polymorphic value.

The standard way around is to introduce a unit closure:

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

Then export_code for deadlock results in a `fun` instead of a `val` and `fun` always is a syntactic ML value. If you don't want to clutter your formalization with those unit closures, you can also instruct the code generator's preprocessor to introduce those closures. See the construction of Fail' in CryptHOL.Generative_Probabilistic_Value in the AFP for a very similar example:

https://www.isa-afp.org/browser_info/current/AFP/CryptHOL/Generative_Probabilistic_Value.html

Hope this helps
Andreas

On 15.07.21 14:57, Simon Foster via Cl-isabelle-users wrote:
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?

Regards,

Simon.

--
Dr. Simon Foster - Research Fellow in Computer Science
High Integrity Systems Engineering Group, University of York
http://www.cs.york.ac.uk/~simonf <http://www.cs.york.ac.uk/~simonf>

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




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