Theory Export

section ‹Export›

theory Export
  imports Prover
begin

text ‹In this theory, we make the prover executable using the code interpretation of the abstract
completeness framework and the Isabelle to Haskell code generator.›

text ‹To actually execute the prover, we need to lazily evaluate the stream of rules to apply.
Otherwise, we will never actually get to a result.›
code_lazy_type stream

text ‹We would also like to make the evaluation of streams a bit more efficient.›
declare Stream.smember_code [code del]
lemma [code]: "Stream.smember x (y ## s) = (x = y ∨ Stream.smember x s)"
  unfolding Stream.smember_def by auto

text ‹To export code to Haskell, we need to specify that functions on the option type should be
  exported into the equivalent functions on the Maybe monad.›
code_printing
  constant the ⇀ (Haskell) "MaybeExt.fromJust"
| constant Option.is_none ⇀ (Haskell) "MaybeExt.isNothing"

text ‹To use the Maybe monad, we need to import it, so we add a shim to do so in every module.›
code_printing code_module MaybeExt ⇀ (Haskell)
  ‹module MaybeExt(fromJust, isNothing) where
     import Data.Maybe(fromJust, isNothing);›

text ‹The default export setup will create a cycle of module imports, so we roll most of the
  theories into one module when exporting to Haskell to prevent this.›
code_identifier
  code_module Stream ⇀ (Haskell) Prover
| code_module Prover ⇀ (Haskell) Prover
| code_module Export ⇀ (Haskell) Prover
| code_module Option ⇀ (Haskell) Prover
| code_module MaybeExt ⇀ (Haskell) Prover
| code_module Abstract_Completeness ⇀ (Haskell) Prover

text ‹Finally, we define an executable version of the prover using the code interpretation from the
  framework, and a version where the list of terms is initially empty.›
definition ‹secavTreeCode ≡ i.mkTree (λr s. Some (effect r s)) rules›
definition ‹secavProverCode ≡ λz . secavTreeCode ([], z)›

text ‹We then export this version of the prover into Haskell.›
export_code open secavProverCode in Haskell

end