Re: [isabelle] Lazy Code Generation
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:
Hope this helps
On 15.07.21 14:57, Simon Foster via Cl-isabelle-users wrote:
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"
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./
This archive was generated by a fusion of
Pipermail (Mailman edition) and