{- |
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)