{- |
Module      :  $Header$
Description :  Utilities for CspCASLProver related to Isabelle
Copyright   :  (c) Liam O'Reilly and Markus Roggenbach,
               Swansea University 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  csliam@swansea.ac.uk
Stability   :  provisional
Portability :  portable

Utilities for CspCASLProver related to Isabelle. The functions here
typically manipulate Isabelle signatures.
-}

module CspCASLProver.IsabelleUtils
    ( addConst
    , addDef
    , addInstanceOf
    , addLemmasCollection
    , addPrimRec
    , addTheoremWithProof
    , updateDomainTab
    , writeIsaTheory
    ) where

import Common.AS_Annotation (makeNamed, Named, SenAttr (..))
import Common.ProofUtils (prepareSenNames)

import Comorphisms.CFOL2IsabelleHOL (IsaTheory)

-- import CspCASLProver.Consts

import qualified Data.Map as Map

import Isabelle.IsaParse (parseTheory)
import Isabelle.IsaPrint (getAxioms, printIsaTheory)
import Isabelle.IsaSign (DomainEntry, IsaProof (..), mkCond, mkSen
                         , Sentence (..), Sign (..), Sort
                         , Term (..), Typ (..))
import Isabelle.IsaConsts (mkVName)
import Isabelle.Translate (transString)

import Logic.Prover (Theory (..), toNamedList)

import Text.ParserCombinators.Parsec (parse)

-- | Add a single constant to the signature of an Isabelle theory
addConst :: String -> Typ -> IsaTheory -> IsaTheory
addConst cName cType isaTh =
    let isaTh_sign = fst isaTh
        isaTh_sen = snd isaTh
        isaTh_sign_ConstTab = constTab isaTh_sign
        isaTh_sign_ConstTabUpdated =
            Map.insert (mkVName cName) cType isaTh_sign_ConstTab
        isaTh_sign_updated = isaTh_sign {
                               constTab = isaTh_sign_ConstTabUpdated
                             }
    in (isaTh_sign_updated, isaTh_sen)

-- | Function to add a def command to an Isabelle theory
addDef :: String -> Term -> Term -> IsaTheory -> IsaTheory
addDef name lhs rhs isaTh =
    let isaTh_sign = fst isaTh
        isaTh_sen = snd isaTh
        sen = ConstDef (IsaEq lhs rhs)
        namedSen = makeNamed name sen
    in (isaTh_sign, isaTh_sen ++ [namedSen])

{- | Function to add an instance of command to an Isabelle theory. The
sort parameters here are basically strings. -}
addInstanceOf :: String -> [Sort] -> Sort -> [(String, Term)] -> IsaProof ->
                 IsaTheory -> IsaTheory
addInstanceOf name args res defs prf isaTh =
    let isaTh_sign = fst isaTh
        isaTh_sen = snd isaTh
        sen = Instance name args res defs prf
        namedSen = makeNamed name sen
    in (isaTh_sign, isaTh_sen ++ [namedSen])

{- | Add a lemmas sentence (definition) that allow us to group large collections
of lemmas in to a single lemma. This cuts down on the repreated addition of
lemmas in the proofs. -}
addLemmasCollection :: String -> [String] -> IsaTheory -> IsaTheory
addLemmasCollection lemmaname lemmas isaTh =
    if null lemmas
    then isaTh
    else let isaTh_sign = fst isaTh
             isaTh_sen = snd isaTh
             -- Make a named lemmas sentence
             namedSen = (makeNamed lemmaname (Lemmas lemmaname lemmas))
                        {isAxiom = False}
         in (isaTh_sign, isaTh_sen ++ [namedSen])

{- | Add a constant with a primrec defintion to the sentences of an Isabelle
theory. Parameters: constant name, type, primrec defintions and isabelle
theory to be added to. -}
addPrimRec :: String -> Typ -> [Term] -> IsaTheory -> IsaTheory
addPrimRec cName cType terms isaTh =
    let isaTh_sign = fst isaTh
        isaTh_sen = snd isaTh
        primRecDef = RecDef {
          keyword = Nothing, constName = mkVName cName,
          constType = Just cType, primRecSenTerms = terms}
        namedPrimRecDef = (makeNamed "BUG_what_does_this_word_do?" primRecDef) {
          isAxiom = False,
          isDef = True}
    in (isaTh_sign, isaTh_sen ++ [namedPrimRecDef])

-- | Add a theorem with proof to an Isabelle theory
addTheoremWithProof :: String -> [Term] -> Term -> IsaProof -> IsaTheory ->
                      IsaTheory
addTheoremWithProof name conds concl proof' isaTh =
    let isaTh_sign = fst isaTh
        isaTh_sen = snd isaTh
        sen = if null conds
              then ((mkSen concl) {thmProof = Just proof'})
              else ((mkCond conds concl) {thmProof = Just proof'})
        namedSen = (makeNamed name sen) {isAxiom = False}
    in (isaTh_sign, isaTh_sen ++ [namedSen])

{- | Prepare a theory for writing it out to a file. This function is based off
the function Isabelle.IsaProve.prepareTheory. The difference being that
this function does not mark axioms nor theorms as to be added to the
simplifier in Isabelle. -}
prepareTheory :: Theory Sign Sentence ()
    -> (Sign, [Named Sentence], [Named Sentence], Map.Map String String)
prepareTheory (Theory sig nSens) = let
    oSens = toNamedList nSens
    nSens' = prepareSenNames transString oSens
    (disAxs, disGoals) = getAxioms nSens'
    in (sig, disAxs, disGoals,
       Map.fromList $ zip (map senAttr nSens') $ map senAttr oSens)

-- | Add a DomainEntry to the domain tab of an Isabelle signature.
updateDomainTab :: DomainEntry -> IsaTheory -> IsaTheory
updateDomainTab domEnt (isaSign, isaSens) =
    let oldDomTab = domainTab isaSign
        isaSignUpdated = isaSign {domainTab = oldDomTab ++ [[domEnt]]}
    in (isaSignUpdated, isaSens)

{- | Write out an Isabelle Theory. The theory should just run through
in Isabelle without any user interactions. This is based heavily
off Isabelle.IsaProve.isaProve -}
writeIsaTheory :: String -> Theory Sign Sentence () -> IO ()
writeIsaTheory thName th = do
  let (sig, axs, ths, _) = prepareTheory th
      -- thms = map senAttr ths
      thBaseName = reverse . takeWhile (/= '/') $ reverse thName
      {- useaxs = filter (\ s ->
      sentence s /= mkSen true && (isDef s ||
      isSuffixOf "def" (senAttr s))) axs
      defaultProof = Just $ IsaProof
      (if null useaxs then [] else [Using $ map senAttr useaxs])
      By Auto -}
      thy = shows (printIsaTheory thBaseName sig $ axs ++ ths) "\n"
      thyFile = thBaseName ++ ".thy"
  -- Check if the Isabelle theory is a valid Isabelle theory
  case parse parseTheory thyFile thy of
    Right _ -> do
      {- prepareThyFiles (ho, bo) thyFile thy
      removeDepFiles thBaseName thms
      isabelle <- getEnvDef "HETS_ISABELLE" "Isabelle"
      callSystem $ isabelle ++ " " ++ thyFile
      ok <- checkFinalThyFile (ho, bo) thyFile
      if ok then getAllProofDeps m thBaseName thms
      else return [] -}
      writeFile thyFile thy
      return ()
    {- The Isabelle theory is not a valid theory (according to Hets)
    as it cannot be parsed. -}
    Left err -> do
      print err
      putStrLn $ "Sorry, a generated theory cannot be parsed, see: "
                   ++ thyFile
      writeFile thyFile thy
      putStrLn "Aborting Isabelle proof attempt"
      return ()
