content: {- |
  Module      :  ./CspCASLProver/CspCASLProver.hs
  Description :  Interface to the CspCASLProver (Isabelle based) theorem prover
  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
  
  Interface for CspCASLProver theorem prover.
  -}
  
  {-
    Interface between CspCASLProver and Hets:
     Hets writes CspCASLProver's Isabelle .thy files and
       starts Isabelle with CspProver
     User extends .thy file with proofs
     User finishes Isabelle
     Hets reads in created *.deps files
  -}
  
  module CspCASLProver.CspCASLProver
      ( cspCASLProver
      ) where
  
  import CASL.AS_Basic_CASL
  import CASL.Fold
  import CASL.Sign (CASLSign, Sign (..), sortSet)
  
  import Common.AS_Annotation (Named, mapNamedM)
  import Common.ProverTools
  import Common.Result
  
  import qualified Comorphisms.CASL2PCFOL as CASL2PCFOL
  import qualified Comorphisms.CASL2SubCFOL as CASL2SubCFOL
  import qualified Comorphisms.CFOL2IsabelleHOL as CFOL2IsabelleHOL
  
  import CspCASL.SignCSP
  import CspCASL.Morphism (CspCASLMorphism)
  
  import CspCASLProver.Consts
  import CspCASLProver.IsabelleUtils
  import CspCASLProver.Utils
  
  import qualified Data.Maybe as Maybe
  import qualified Data.Set as Set
  
  import Isabelle.IsaProve
  import qualified Isabelle.IsaSign as Isa
  
  import Logic.Prover
  import Logic.Comorphism (wrapMapTheory)
  
  -- | The string that Hets uses as CspCASLProver
  cspCASLProverS :: String
  cspCASLProverS = "CspCASLProver"
  
  -- | The wrapper function that is CspCASL Prover
  cspCASLProver :: Prover CspCASLSign CspCASLSen CspCASLMorphism () ()
  cspCASLProver = (mkProverTemplate cspCASLProverS () cspCASLProverProve)
    { proverUsable = checkBinary "isabelle" }
  
  -- | The main cspCASLProver function
  cspCASLProverProve :: String -> Theory CspCASLSign CspCASLSen () -> a ->
                        IO [ProofStatus ()]
  cspCASLProverProve thName (Theory ccSign ccSensThSens) _freedefs =
    let -- get the CASL signature of the data part of the CspcASL theory
        caslSign = ccSig2CASLSign ccSign
        -- Get a list of CspCASL named sentences
        ccNamedSens = toNamedList ccSensThSens
        -- A filter to change a CspCASLSen to a CASLSen (if possible)
        caslSenFilter ccSen = case ccSen of
          ExtFORMULA (ProcessEq {}) -> Nothing
          sen -> Just $ foldFormula (mapRecord $ const ()) sen
        -- All named CASL sentences from the datapart
        caslNamedSens = Maybe.mapMaybe (mapNamedM caslSenFilter) ccNamedSens
        -- Generate data encoding. This may fail.
        Result diag dataTh = produceDataEncoding caslSign caslNamedSens
    in case dataTh of
      Nothing -> do
        -- Data translation failed
        putStrLn $ "Sorry, could not encode the data part:" ++ show diag
        return []
      Just (dataThSig, dataThSens, pcfolSign, cfolSign) -> do
        {- Data translation succeeded
        Write out the data encoding -}
        writeIsaTheory (mkThyNameDataEnc thName)
                           (Theory dataThSig (toThSens dataThSens))
        {- Generate and write out the preAlpbate, justification theorems
        and the instances code. -}
        writeIsaTheory (mkThyNamePreAlphabet thName)
                           (producePreAlphabet thName caslSign pcfolSign)
        {- Generate and write out the Alpbatet construction, bar types
        and choose functions. -}
        writeIsaTheory (mkThyNameAlphabet thName)
                           (produceAlphabet thName caslSign)
        -- Generate and write out the integration theorems
        writeIsaTheory (mkThyNameIntThms thName)
                           (produceIntegrationTheorems thName caslSign)
        {- Generate and Isabelle to prove the process refinements (also produces
        the processes) -}
        isaProve JEdit thName
          (produceProcesses thName ccSign ccNamedSens pcfolSign cfolSign) ()
  
  {- |Produce the Isabelle theory of the data part of a CspCASL
  specification. The data transalation can fail. If it does fail there will
  be an error message. Its arguments are the CASL signature from the data
  part and a list of the named CASL sentences from the data part. Returned
  are the Isabelle signature, Isabelle named sentences and also the CASL
  signature of the data part after translation to pcfol (i.e. with out
  subsorting) and cfol (i.e. with out subsorting and partiality). -}
  produceDataEncoding :: CASLSign -> [Named CASLFORMULA] ->
                         Result (Isa.Sign, [Named Isa.Sentence], CASLSign,
                                    CASLSign)
  produceDataEncoding caslSign caslNamedSens =
      let -- Comorphisms
          casl2pcfol = wrapMapTheory CASL2PCFOL.CASL2PCFOL
          pcfol2cfol = wrapMapTheory $ CASL2SubCFOL.CASL2SubCFOL True
                       CASL2SubCFOL.AllSortBottoms
          cfol2isabelleHol = wrapMapTheory CFOL2IsabelleHOL.CFOL2IsabelleHOL
      in do
        {- Remove Subsorting from the CASL part of the CspCASL
        specification -}
        th_pcfol <- casl2pcfol (caslSign, caslNamedSens)
        -- Next Remove partial functions
        th_cfol <- pcfol2cfol th_pcfol
        -- Next Translate to IsabelleHOL code
        (th_isa_Sig, th_isa_Sens) <- cfol2isabelleHol th_cfol
        return (th_isa_Sig, th_isa_Sens, fst th_pcfol, fst th_cfol)
  
  {- | Produce the Isabelle theory which contains the PreAlphabet,
  Justification Theorems and also the instances code. We need the
  PFOL signature which is the data part CASL signature after
  translation to PCFOL (i.e. without subsorting) to pass on as an
  argument. -}
  producePreAlphabet :: String -> CASLSign -> CASLSign ->
                        Theory Isa.Sign Isa.Sentence ()
  producePreAlphabet thName caslSign pfolSign =
      let sortList = Set.toList (sortSet caslSign)
          {- empty Isabelle signature which imports the data encoding
          and quotient.thy (which is needed for the instances code) -}
          isaSignEmpty = Isa.emptySign {Isa.imports = [mkThyNameDataEnc thName
                                                      , quotientThyS] }
          -- Start with our empty Isabelle theory, add the constructs
          (isaSign, isaSens) = addInstanceOfEquiv
                             $ addJustificationTheorems caslSign pfolSign
                             $ addAllGaAxiomsCollections caslSign pfolSign
                             $ addEqFun sortList
                             $ addAllCompareWithFun caslSign
                             $ addPreAlphabet sortList
                               (isaSignEmpty, [])
      in Theory isaSign (toThSens isaSens)
  
  {- |Produce the Isabelle theory which contains the Alphabet
  construction,  and also the bar types and choose
  fucntions for CspCASLProver. -}
  produceAlphabet :: String -> CASLSign -> Theory Isa.Sign Isa.Sentence ()
  produceAlphabet thName caslSign =
      let sortList = Set.toList (sortSet caslSign)
          -- empty Isabelle signature which imports the preAlphabet encoding
          isaSignEmpty = Isa.emptySign {
                           Isa.imports = [mkThyNamePreAlphabet thName]}
          {- Start with our empty isabelle theory, add the Alphabet type
          , then the bar types and finally the choose functions. -}
          (isaSign, isaSens) = addAllChooseFunctions sortList
                             $ addAllBarTypes sortList
                             $ addAlphabetType
                               (isaSignEmpty, [])
      in Theory isaSign (toThSens isaSens)
  
  {- |Produce the Isabelle theory which contains the Integration
  Theorems on data -}
  produceIntegrationTheorems :: String -> CASLSign ->
                                Theory Isa.Sign Isa.Sentence ()
  produceIntegrationTheorems thName caslSign =
      let sortList = Set.toList (sortSet caslSign)
          -- empty Isabelle signature which imports the alphabet encoding
          isaSignEmpty = Isa.emptySign {Isa.imports = [mkThyNameAlphabet thName] }
          {- Start with our empty isabelle theory and add the
          integration theorems. -}
          (isaSign, isaSens) = addAllIntegrationTheorems sortList caslSign
                               (isaSignEmpty, [])
      in Theory isaSign (toThSens isaSens)
  
  {- |Produce the Isabelle theory which contains the Process Translations and
  process refinement theorems. We -- need the PCFOL and CFOL signatures of
  the data part after translation to PCFOL and CFOL to pass -- along to the
  process translation. -}
  produceProcesses :: String -> CspCASLSign -> [Named CspCASLSen] ->
                      CASLSign -> CASLSign -> Theory Isa.Sign Isa.Sentence ()
  produceProcesses thName ccSign ccNamedSens pcfolSign cfolSign =
      let caslSign = ccSig2CASLSign ccSign
          cspSign = ccSig2CspSign ccSign
          sortList = Set.toList (sortSet caslSign)
          sortRel' = sortRel caslSign
          chanNameMap = chans cspSign
          {- Isabelle signature which imports the integration theorems encoding
          and CSP_F -}
          isaSignEmpty = Isa.emptySign {Isa.imports = [mkThyNameIntThms thName
                                                      , cspFThyS] }
          {- Start with our empty isabelle theory and add the
          processes the the process refinement theorems. -}
          (isaSign, isaSens) =
              addProcTheorems ccNamedSens ccSign pcfolSign cfolSign
            $ addProcMap ccNamedSens ccSign pcfolSign cfolSign
            $ addProcNameDatatype cspSign
            $ addFlatTypes sortList
            $ addProjFlatFun
            $ addEventDataType sortRel' chanNameMap
              (isaSignEmpty, [])
      in Theory isaSign (toThSens isaSens)
  