-- |This module, and the corresponding 'Zeno.Isabellable' modules,
-- deal with the conversion a 'ProofSet' into Isabelle/HOL code, outputting this
-- code into a file and then checking this file with Isabelle.
module Zeno.Isabelle (
  toIsabelle
) where

import Prelude ()
import Zeno.Prelude
import Zeno.Core
import Zeno.Proof

import Zeno.Isabellable.Class
import Zeno.Isabellable.Proof
import Zeno.Isabellable.Core

import qualified Data.Map as Map
import qualified Data.Text as Text

instance Isabellable ZProofSet where
  toIsabelle (ProofSet pgm named_proofs) =
    "theory Zeno\nimports Main List\nbegin"
    ++ isa_dtypes ++ isa_binds ++ isa_proofs ++ "\n\nend\n"
    where
    flags = programFlags pgm
    (names, proofs) = unzip named_proofs
    names' = map convert names

    all_vars =
      (nubOrd . concatMap (toList . proofGoal)) proofs

    isa_proofs = foldl (++) mempty
               $ zipWith namedIsabelleProof names'  proofs

    binds = sortBindings binds'
    (dtypes, binds')
      | flagIsabelleAll flags =
          ( Map.elems . programDataTypes $ pgm,
            programBindings $ pgm )
      | otherwise =
          dependencies pgm all_vars

    builtInType dt = show dt `elem`
      ["list", "bool", "(,)", "(,,)", "(,,,)"]

    isa_binds = foldl (++) mempty
              . map toIsabelle
              $ binds

    isa_dtypes = foldl (++) mempty
               . map toIsabelle
               . filter (not . builtInType)
               $ dtypes
