Re: [isabelle] Code_Target.evaluator raises various exception during serialisation

Hi again,

>> When building similar thing, it is best to follow structure
>> Code_Runtime.  The Quickcheck Narrowing engine is an experimental
>> (though apparently operative) ad-hoc approach toward code generation and
>> definitely nothing I recommend to glimpse from in that respect.
> In Code_Runtime, we have not found anything related to actually writing
> out the files, compiling and executing them and reading back the input.
> This is essentially what we take from Quickcheck_Narrowing. We am aware
> that the whole setup with narrowing_engine.hs is ad hoc and we avoid that.

the actual compiler invocation is in these lines in Code_Runtime:

> fun exec verbose code =
>   (if ! trace then tracing code else ();
>   ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code));

> There is also something in both Code_Runtime and Quickcheck_Narrowing
> that we have not yet understood. What is the purpose of the cookies that
> appear everywhere? So far, our solution seems to work without them, but
> maybe our testcases are too simple.

The cookies are a device to connect to ML more or less raw compiler to
the runtime system.

In an ideal world, the ML compiler could provide a function

    evaluate : ml_program -> ml_expr -> tau

where ml_program is an abstract representation of an ML program, ml_expr
is an abstract representation of an ML expression, and tau is the
expected result type.  The compiler would then compile the program,
evaluate the expression against it and return the internalized value
(raising and exception on type mismatch).

But we do not have this in ML as used by Isabelle (I do not know whether
particular compilers provided such extensions).  What we have else is
something like

    compile : string -> unit

where string is ML source code which is compiled resulting in a side
effect on the underlying ML environment.

Here the cookie comes in.  It has three fields get, put, put_ml.  The
plain string put_ml is a reference by name to a slot which can be filled
with an evaluation result.  After compilation, the internalized
evaluation result can be obtained using get.  The put is just a security
device to make sure that the connection between put and put_ml has not
been broken by name space shadowing etc.  Thus:

    val _ put error_evaluation
    val _ = compile (»compiled program, containing a value which is
stored using put_ml (by name)«)
    val result = get ctxt;

I have spent a lot of thought for alternative patterns here, but have
not been able to find any.

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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