[isabelle] Code_Target.evaluator raises various exception during serialisation



Hi,

We are trying to use the dynamic evaluation facility of the code generator to evaluate Isabelle terms in different target languages. The theory below (also attached) shows our reduced setup, which follows Quickcheck's narrowing engine, and a minimal example. Unfortunately, we keep getting exceptions during the serialisation. Apparently, we are not using the functions correctly, but we have no clue what could be wrong.

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

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"}
*}

ML {* test "Scala" *}    --{* Match  (line 176 of "~~/src/Tools/Code/code_scala.ML") *}
ML {* test "SML" *}      --{* Option (line 81 of "General/basics.ML") *}
ML {* test "Haskell" *}  --{* Match  (line 137 of "~~/src/Tools/Code/code_symbol.ML") *}

end

Thanks in advance for any suggestions,
Andreas

Attachment: Scratch.thy
Description: application/extension-thy



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