Re: [isabelle] Calling external provers from Isabelle
1) Call Isabelle's code generator to produce a Haskell file of a
as a first entry try
This should suffice for a proof of concept.
Building code from own snippets and generated code is a black art on
own -- if your project evolves into something persistent, get back
and I'll try my best to provide you with the most robust and
ways available to arrange things then.
For the narrowing-based Quickcheck in Isabelle, I already use
Isabelle's code generator to produce a Haskell file,
pass it to the Haskell compiler, and read back its result.
The implementation is in
Function value and dynamic_value_strict provide the compilation and the
Maybe you can reuse part of it, or generalize it to be useful for a
Florian and I discussed extracting this part into a more general
"Haskell evaluator" module.
However as it was of low priority on my todo list and time is generally
rare, we never
This archive was generated by a fusion of
Pipermail (Mailman edition) and