CspCASLProver.hs revision b87efd3db0d2dc41615ea28669faf80fc1b48d56
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian MaederModule : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : Interface to the CspCASLProver (Isabelle based) theorem prover
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian MaederCopyright : (c) Liam O'Reilly and Markus Roggenbach, Swansea University 2009
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian MaederLicense : GPLv2 or higher
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian MaederMaintainer : csliam@swansea.ac.uk
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian MaederStability : provisional
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian MaederPortability : portable
dd9ab23d84f402532a6b651f6463e0c3bdb60cfdChristian MaederInterface for CspCASLProver theorem prover.
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder Interface between CspCASLProver and Hets:
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder Hets writes CspCASLProver's Isabelle .thy files and
dd9ab23d84f402532a6b651f6463e0c3bdb60cfdChristian Maeder starts Isabelle with CspProver
dd9ab23d84f402532a6b651f6463e0c3bdb60cfdChristian Maeder User extends .thy file with proofs
dd9ab23d84f402532a6b651f6463e0c3bdb60cfdChristian Maeder User finishes Isabelle
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder Hets reads in created *.deps files
dd9ab23d84f402532a6b651f6463e0c3bdb60cfdChristian Maeder ( cspCASLProver
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maederimport CASL.AS_Basic_CASL (CASLFORMULA)
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maederimport CASL.Sign (CASLSign, Sign (..))
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maederimport Common.AS_Annotation (Named, mapNamedM)
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maederimport qualified Comorphisms.CASL2PCFOL as CASL2PCFOL
dc62afbf79603699b39b2387f48298634f642e67cmaederimport qualified Comorphisms.CASL2SubCFOL as CASL2SubCFOL
08444813af2fade39f88fc4bd7c6465452915668Eugen Kuksaimport qualified Comorphisms.CFOL2IsabelleHOL as CFOL2IsabelleHOL
3e214c2b58c1df27f3f491df00e9526ffd6c6973Eugen Kuksaimport CspCASL.SignCSP (ccSig2CASLSign, ccSig2CspSign, CspCASLSign, CspSign (..)
3e214c2b58c1df27f3f491df00e9526ffd6c6973Eugen Kuksa , CspCASLSen (..))
dd9ab23d84f402532a6b651f6463e0c3bdb60cfdChristian Maederimport CspCASL.Morphism (CspMorphism)
5e01ba94cb504e8bee124807390e9c2b49be8c7dEugen Kuksaimport qualified Data.Maybe as Maybe
3c5c7e3fbc88e305dfb8a017757da84b2565d919mscodescuimport qualified Data.Set as Set
3e214c2b58c1df27f3f491df00e9526ffd6c6973Eugen Kuksaimport Isabelle.IsaProve (isaProve)
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskiimport qualified Isabelle.IsaSign as Isa
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskiimport Logic.Comorphism (wrapMapTheory)
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa-- | The string that Hets uses as CspCASLProver
dd9ab23d84f402532a6b651f6463e0c3bdb60cfdChristian MaedercspCASLProverS :: String
dd9ab23d84f402532a6b651f6463e0c3bdb60cfdChristian MaedercspCASLProverS = "CspCASLProver"
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder-- | The wrapper function that is CspCASL Prover
08444813af2fade39f88fc4bd7c6465452915668Eugen KuksacspCASLProver :: Prover CspCASLSign CspCASLSen CspMorphism () ()
dd9ab23d84f402532a6b651f6463e0c3bdb60cfdChristian MaedercspCASLProver = mkProverTemplate cspCASLProverS () cspCASLProverProve
dd9ab23d84f402532a6b651f6463e0c3bdb60cfdChristian Maeder-- | The main cspCASLProver function
dd9ab23d84f402532a6b651f6463e0c3bdb60cfdChristian MaedercspCASLProverProve :: String -> Theory CspCASLSign CspCASLSen () -> a ->
dd9ab23d84f402532a6b651f6463e0c3bdb60cfdChristian Maeder IO [ProofStatus ()]
dd9ab23d84f402532a6b651f6463e0c3bdb60cfdChristian MaedercspCASLProverProve thName (Theory ccSign ccSensThSens) _freedefs =
01ddc4cad68fa84b4e9dd41089ad876329bae5b0Christian Maeder let -- get the CASL signature of the data part of the CspcASL theory
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski caslSign = ccSig2CASLSign ccSign
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski -- Get a list of CspCASL named sentences
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski ccNamedSens = toNamedList ccSensThSens
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski -- A filter to change a CspCASLSen to a CASLSen (if possible)
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski caslSenFilter ccSen = case ccSen of
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski CASLSen sen -> Just sen
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski ProcessEq _ _ _ _ -> Nothing
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski -- All named CASL sentences from the datapart
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski caslNamedSens = Maybe.mapMaybe (mapNamedM caslSenFilter) ccNamedSens
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski -- Generate data encoding. This may fail.
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski Result diag dataTh = produceDataEncoding caslSign caslNamedSens
3e214c2b58c1df27f3f491df00e9526ffd6c6973Eugen Kuksa in case dataTh of
3e214c2b58c1df27f3f491df00e9526ffd6c6973Eugen Kuksa Nothing -> do
3e214c2b58c1df27f3f491df00e9526ffd6c6973Eugen Kuksa -- Data translation failed
3e214c2b58c1df27f3f491df00e9526ffd6c6973Eugen Kuksa putStrLn $ "Sorry, could not encode the data part:" ++ show diag
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder Just (dataThSig, dataThSens, pcfolSign, cfolSign) -> do
5e01ba94cb504e8bee124807390e9c2b49be8c7dEugen Kuksa -- Data translation succeeded
54a08d99d6733842a51b1a6c578af6db86ff7bbfEugen Kuksa -- Write out the data encoding
545949b4e9a60032662bb7f6aeb01194e0934ebaChristian Maeder writeIsaTheory (mkThyNameDataEnc thName)
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski (Theory dataThSig (toThSens dataThSens))
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski -- Generate and write out the preAlpbate, justification theorems
08444813af2fade39f88fc4bd7c6465452915668Eugen Kuksa -- and the instances code.
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski writeIsaTheory (mkThyNamePreAlphabet thName)
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski (producePreAlphabet thName caslSign pcfolSign)
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski -- Generate and write out the Alpbatet construction, bar types
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski -- and choose functions.
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski writeIsaTheory (mkThyNameAlphabet thName)
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski (produceAlphabet thName caslSign)
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa -- Generate and write out the integration theorems
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder writeIsaTheory (mkThyNameIntThms thName)
b1f2971b105e6da3f4722315e0a0e2abef96e66fcmaeder (produceIntegrationTheorems thName caslSign)
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski -- Generate and Isabelle to prove the process refinements (also produces
545949b4e9a60032662bb7f6aeb01194e0934ebaChristian Maeder -- the processes)
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder isaProve thName (produceProcesses thName ccSign ccNamedSens pcfolSign
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder-- |Produce the Isabelle theory of the data part of a CspCASL
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder-- specification. The data transalation can fail. If it does fail there will
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder-- be an error message. Its arguments are the CASL signature from the data
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder-- part and a list of the named CASL sentences from the data part. Returned
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder-- are the Isabelle signature, Isabelle named sentences and also the CASL
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder-- signature of the data part after translation to pcfol (i.e. with out
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder-- subsorting) and cfol (i.e. with out subsorting and partiality).
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian MaederproduceDataEncoding :: CASLSign -> [Named CASLFORMULA] ->
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski Result (Isa.Sign, [Named Isa.Sentence], CASLSign,
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian MaederproduceDataEncoding caslSign caslNamedSens =
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder let -- Comorphisms
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski casl2pcfol = wrapMapTheory CASL2PCFOL.CASL2PCFOL
da5ff3703cc54721f3536212455d6348550057a0Christian Maeder pcfol2cfol = wrapMapTheory $ CASL2SubCFOL.CASL2SubCFOL True
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski cfol2isabelleHol = wrapMapTheory CFOL2IsabelleHOL.CFOL2IsabelleHOL
3e214c2b58c1df27f3f491df00e9526ffd6c6973Eugen Kuksa -- Remove Subsorting from the CASL part of the CspCASL
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder -- specification
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder th_pcfol <- casl2pcfol (caslSign, caslNamedSens)
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski -- Next Remove partial functions
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder th_cfol <- pcfol2cfol th_pcfol
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder -- Next Translate to IsabelleHOL code
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder (th_isa_Sig, th_isa_Sens) <- cfol2isabelleHol th_cfol
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski return (th_isa_Sig, th_isa_Sens, fst th_pcfol, fst th_cfol)
01ddc4cad68fa84b4e9dd41089ad876329bae5b0Christian Maeder-- |Produce the Isabelle theory which contains the PreAlphabet,
5234ff2b6526d88de1d97a03c058e1c9cc48f695Christian Maeder-- Justification Theorems and also the instances code. We need the
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder-- PFOL signature which is the data part CASL signature after
3e214c2b58c1df27f3f491df00e9526ffd6c6973Eugen Kuksa-- translation to PCFOL (i.e. without subsorting) to pass on as an
3e214c2b58c1df27f3f491df00e9526ffd6c6973Eugen KuksaproducePreAlphabet :: String -> CASLSign -> CASLSign ->
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian MaederproducePreAlphabet thName caslSign pfolSign =
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder let sortList = Set.toList (sortSet caslSign)
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder -- empty Isabelle signature which imports the data encoding
3e214c2b58c1df27f3f491df00e9526ffd6c6973Eugen Kuksa -- and quotient.thy (which is needed for the instances code)
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder isaSignEmpty = Isa.emptySign {Isa.imports = [mkThyNameDataEnc thName
3e214c2b58c1df27f3f491df00e9526ffd6c6973Eugen Kuksa , quotientThyS] }
3e214c2b58c1df27f3f491df00e9526ffd6c6973Eugen Kuksa -- Start with our empty isabelle theory, add the preAlphabet
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder -- datetype, then all the comparewith functions, then add the
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder -- eq function. Finally add the justification theorems and
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski -- instance of code.
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder (isaSign, isaSens) = addInstansanceOfEquiv
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder $ addJustificationTheorems caslSign pfolSign
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder $ addAllGaAxiomsCollections caslSign pfolSign
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski $ addEqFun sortList
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski $ addAllCompareWithFun caslSign
01ddc4cad68fa84b4e9dd41089ad876329bae5b0Christian Maeder $ addPreAlphabet sortList
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder (isaSignEmpty, [])
3e214c2b58c1df27f3f491df00e9526ffd6c6973Eugen Kuksa in Theory isaSign (toThSens isaSens)
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski-- |Produce the Isabelle theory which contains the Alphabet
4461c838d986278de476dfb7843c0f3f9b088d17Christian Maeder-- construction, and also the bar types and choose
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski-- fucntions for CspCASLProver.
4461c838d986278de476dfb7843c0f3f9b088d17Christian MaederproduceAlphabet :: String -> CASLSign -> Theory Isa.Sign Isa.Sentence ()
80875f917d741946a39d0ec0b5721e46ba609823Till MossakowskiproduceAlphabet thName caslSign =
4461c838d986278de476dfb7843c0f3f9b088d17Christian Maeder let sortList = Set.toList (sortSet caslSign)
4461c838d986278de476dfb7843c0f3f9b088d17Christian Maeder -- empty Isabelle signature which imports the preAlphabet encoding
4461c838d986278de476dfb7843c0f3f9b088d17Christian Maeder isaSignEmpty = Isa.emptySign {
4461c838d986278de476dfb7843c0f3f9b088d17Christian Maeder Isa.imports = [mkThyNamePreAlphabet thName]}
3a8cd9d6e48924ba4d2ff967eab2dbac17fe7c23Christian Maeder -- Start with our empty isabelle theory, add the Alphabet type
dd9ab23d84f402532a6b651f6463e0c3bdb60cfdChristian Maeder -- , then the bar types and finally the choose functions.
dd9ab23d84f402532a6b651f6463e0c3bdb60cfdChristian Maeder (isaSign, isaSens) = addAllChooseFunctions sortList
dd9ab23d84f402532a6b651f6463e0c3bdb60cfdChristian Maeder $ addAllBarTypes sortList
c1eff8f8127d646590119e59596b023e38de5783Eugen Kuksa $ addAlphabetType
dd9ab23d84f402532a6b651f6463e0c3bdb60cfdChristian Maeder (isaSignEmpty, [])
c1eff8f8127d646590119e59596b023e38de5783Eugen Kuksa in Theory isaSign (toThSens isaSens)
c1eff8f8127d646590119e59596b023e38de5783Eugen Kuksa-- |Produce the Isabelle theory which contains the Integration
beb165291db308df7cae2c4b1a1fdd8ce913205eEugen Kuksa-- Theorems on data
823c8eb15961960517300af6a7bf3e1ff2b36a8cEugen KuksaproduceIntegrationTheorems :: String -> CASLSign ->
823c8eb15961960517300af6a7bf3e1ff2b36a8cEugen KuksaproduceIntegrationTheorems thName caslSign =
5e01ba94cb504e8bee124807390e9c2b49be8c7dEugen Kuksa let sortList = Set.toList (sortSet caslSign)
5e01ba94cb504e8bee124807390e9c2b49be8c7dEugen Kuksa -- empty Isabelle signature which imports the alphabet encoding
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski isaSignEmpty = Isa.emptySign {Isa.imports = [mkThyNameAlphabet thName] }
dc62afbf79603699b39b2387f48298634f642e67cmaeder -- Start with our empty isabelle theory and add the
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski -- integration theorems.
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski (isaSign, isaSens) = addAllIntegrationTheorems sortList caslSign
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski (isaSignEmpty, [])
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa in Theory isaSign (toThSens isaSens)
08444813af2fade39f88fc4bd7c6465452915668Eugen Kuksa-- |Produce the Isabelle theory which contains the Process Translations and
5e01ba94cb504e8bee124807390e9c2b49be8c7dEugen Kuksa-- process refinement theorems. We -- need the PCFOL and CFOL signatures of
08444813af2fade39f88fc4bd7c6465452915668Eugen Kuksa-- the data part after translation to PCFOL and CFOL to pass -- along to the
bcd714f4e2fd0a8d20d33899d24b69b75a3cede5Christian Maeder-- process translation.
bcd714f4e2fd0a8d20d33899d24b69b75a3cede5Christian MaederproduceProcesses :: String -> CspCASLSign -> [Named CspCASLSen] ->
08444813af2fade39f88fc4bd7c6465452915668Eugen Kuksa CASLSign -> CASLSign -> Theory Isa.Sign Isa.Sentence ()
5e01ba94cb504e8bee124807390e9c2b49be8c7dEugen KuksaproduceProcesses thName ccSign ccNamedSens pcfolSign cfolSign =
3e214c2b58c1df27f3f491df00e9526ffd6c6973Eugen Kuksa let caslSign = ccSig2CASLSign ccSign
08444813af2fade39f88fc4bd7c6465452915668Eugen Kuksa cspSign = ccSig2CspSign ccSign
08444813af2fade39f88fc4bd7c6465452915668Eugen Kuksa sortList = Set.toList (sortSet caslSign)
08444813af2fade39f88fc4bd7c6465452915668Eugen Kuksa sortRel' = sortRel caslSign
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder chanNameMap = chans cspSign
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa -- Isabelle signature which imports the integration theorems encoding
4aeea3e8e2e838518e7cc0318cf3bbfccc78063aChristian Maeder isaSignEmpty = Isa.emptySign {Isa.imports = [mkThyNameIntThms thName
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski , cspFThyS] }
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa -- Start with our empty isabelle theory and add the
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa -- processes the the process refinement theorems.
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski (isaSign, isaSens) =
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski addProcTheorems ccNamedSens ccSign pcfolSign cfolSign
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski $ addProcMap ccNamedSens ccSign pcfolSign cfolSign
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski $ addProcNameDatatype cspSign
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski $ addFlatTypes sortList
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski $ addProjFlatFun
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski $ addEventDataType sortRel' chanNameMap
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski (isaSignEmpty, [])
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski in Theory isaSign (toThSens isaSens)