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



Hi Andreas,

> Can anyone spot the mistake or provide some background how
> Code_Target.evaluator is supposed to be used?

this is indeed a very uncomfortable corner of the system.  The
evaluation stack has to accomplish a couple of issues at the same time:
* consistent embedding into the pre-/postprocessor infrastructure
* sane separation of static and dynamic context
* dealing with extralogical questions »how to compile strings to values«
and such.

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.

> theory Scratch imports "~~/src/HOL/Main" begin
> 
> datatype foo = Foo
> 
> ML {*
> fun do_something _ = true;
> fun test target =
>   Code_Thingol.dynamic_value @{theory} (fn _ => I)
>     (fn naming => fn program => fn ((_, vs_ty), t) => fn deps =>
>        do_something
>          (Code_Target.evaluator @{theory} target naming program deps
> (vs_ty, t)))
>     @{term "Foo"}
> *}

Formally, this does not look bad.  A slightly refined version:

> datatype foo = Foo
> definition "bar x = x"
> 
> ML {*
> val t = @{term "Foo"}; 
> 
> fun do_something ([(_, s)], _) = (writeln s; true);
> fun test thy target =
>   Code_Thingol.dynamic_value thy (fn _ => I)
>     (fn naming => fn program => fn ((_, vs_ty), t) => fn deps =>
>        do_something
>          (Code_Target.evaluator thy target naming program deps (vs_ty, t)))
>     t
> *}
> 
> ML {* test @{theory} "Scala" *}
> ML {* test @{theory} "SML" *}
> ML {* test @{theory} "Eval" *}
> ML {* test @{theory} "Haskell" *} 

Two observations:
a) Scala will choke always.  As of Isabelle2013-2, Scala just does not
carry on for evaluation.
b) The problems with the other invocations vanish as soon as you replace
term "Foo" by the logically identical "bar Foo".  Don't ask me exactly
why, but it could be a misbehaviour wrt. dependencies which for subtle
reasons does not show up in the existing applications.

Both problems cannot be reproduced on the ongoing development branch.
Since we are converging towards a release, you might consider basing
your work on a particular source code revision until the next release.

The whole evaluation stack has seen considerable reworking and
clarification during the last months and subtle misbehaviours are likely
to have been eliminated.

I'm not giving this advice light-minded but I trust your experience.  In
case, we should continue the discussion on isabelle-dev.

Hope this helps,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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