content: {- |
  Module      :  ./CspCASLProver/IsabelleUtils.hs
  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 ()
  