CspCASLProver.hs revision 33bdce26495121cdbce30331ef90a1969126a840
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederDescription : Interface to the CspCASLProver (Isabelle based) theorem prover
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) Liam O'Reilly and Markus Roggenbach, Swansea University 2009
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : csliam@swansea.ac.uk
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederPortability : portable
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaederInterface for CspCASLProver theorem prover.
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder Interface between CspCASLProver and Hets:
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder Hets writes CspCASLProver's Isabelle .thy files and
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder starts Isabelle with CspProver
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder User extends .thy file with proofs
a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maeder User finishes Isabelle
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder Hets reads in created *.deps files
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich ( cspCASLProver
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maederimport CASL.AS_Basic_CASL (CASLFORMULA)
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maederimport CASL.Sign (CASLSign, Sign(..))
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maederimport Common.AS_Annotation (Named, mapNamedM)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport qualified Comorphisms.CASL2PCFOL as CASL2PCFOL
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport qualified Comorphisms.CASL2SubCFOL as CASL2SubCFOL
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport qualified Comorphisms.CFOL2IsabelleHOL as CFOL2IsabelleHOL
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport CspCASL.SignCSP (ccSig2CASLSign, ccSig2CspSign, CspCASLSign, CspSign(..)
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder , CspCASLSen(..))
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport CspCASL.Morphism (CspMorphism)
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport qualified Data.Maybe as Maybe
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian Maederimport qualified Data.Set as Set
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport qualified Isabelle.IsaSign as Isa
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederimport Logic.Comorphism (wrapMapTheory)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- | The string that Hets uses as CspCASLProver
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian MaedercspCASLProverS :: String
308834907a120fd8771e18292ed2ca9cd767c12dChristian MaedercspCASLProverS = "CspCASLProver"
734257b9ea9fcaa18d4e3627f54f5295a99aa1f7Felix Gabriel Mance-- | The wrapper function that is CspCASL Prover
8cacad2a09782249243b80985f28e9387019fe40Christian MaedercspCASLProver :: Prover CspCASLSign CspCASLSen CspMorphism () ()
6a2dad705deefd1b7a7e09b84fd2d75f2213be47Christian MaedercspCASLProver = mkProverTemplate cspCASLProverS () cspCASLProverProve
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder-- | The main cspCASLProver function
014dc30f64ec25e4790cca987d4d1e6635430510Christian MaedercspCASLProverProve :: String -> Theory CspCASLSign CspCASLSen () -> a ->
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich IO([Proof_status ()])
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian MaedercspCASLProverProve thName (Theory ccSign ccSensThSens) _freedefs =
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder let -- get the CASL signature of the data part of the CspcASL theory
feca1d35123d8c31aee238c9ce79947b0bf65494Christian Maeder caslSign = ccSig2CASLSign ccSign
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder -- Get a list of CspCASL named sentences
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder ccNamedSens = toNamedList ccSensThSens
f5c0884429b01e74c6e658ded921fb2e16dfb478Christian Maeder -- A filter to change a CspCASLSen to a CASLSen (if possible)
db675e8302ddb0d6528088ce68f5e98a00e890e3Christian Maeder caslSenFilter ccSen = case ccSen of
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder CASLSen sen -> Just sen
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder ProcessEq _ _ _ _ -> Nothing
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder -- All named CASL sentences from the datapart
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder caslNamedSens = Maybe.catMaybes $
23ffcc44ca8612feccbd8fda63fa5be7ab5f9dc3Christian Maeder map (mapNamedM caslSenFilter) ccNamedSens
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder -- Generate data encoding. This may fail.
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder Result diag (dataTh) = produceDataEncoding caslSign caslNamedSens
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder in case dataTh of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Nothing -> do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- Data translation failed
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder putStrLn $ "Sorry, could not encode the data part:" ++ (show diag)
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder Just (dataThSig, dataThSens, pcfolSign, cfolSign) -> do
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder -- Data translation succeeded
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder -- Write out the data encoding
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder writeIsaTheory (mkThyNameDataEnc thName)
dc679edd4ca027663212afdf00926ae2ce19b555Christian Maeder (Theory dataThSig (toThSens dataThSens))
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- Generate and write out the preAlpbate, justification theorems
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder -- and the instances code.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder writeIsaTheory (mkThyNamePreAlphabet thName)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (producePreAlphabet thName caslSign pcfolSign)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder -- Generate and write out the Alpbatet construction, bar types
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder -- and choose functions.
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder writeIsaTheory (mkThyNameAlphabet thName)
b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder (produceAlphabet thName caslSign)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder -- Generate and write out the integration theorems
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich writeIsaTheory (mkThyNameIntThms thName)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (produceIntegrationTheorems thName caslSign)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- Generate and Isabelle to prove the process refinements (also produces
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- the processes)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder isaProve thName (produceProcesses thName ccSign ccNamedSens pcfolSign
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder-- | Produce the Isabelle theory of the data part of a CspCASL
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder-- specification. The data transalation can fail. If it does fail there will
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder-- be an error message. Its arguments are the CASL signature from the data
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder-- part and a list of the named CASL sentences from the data part. Returned
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- are the Isabelle signature, Isabelle named sentences and also the CASL
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- signature of the data part after translation to pcfol (i.e. with out
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- subsorting) and cfol (i.e. with out subsorting and partiality).
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederproduceDataEncoding :: CASLSign -> [Named CASLFORMULA] ->
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Result (Isa.Sign, [Named Isa.Sentence], CASLSign,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederproduceDataEncoding caslSign caslNamedSens =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let -- Comorphisms
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder casl2pcfol = (wrapMapTheory CASL2PCFOL.CASL2PCFOL)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder pcfol2cfol = (wrapMapTheory CASL2SubCFOL.defaultCASL2SubCFOL)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder cfol2isabelleHol = (wrapMapTheory CFOL2IsabelleHOL.CFOL2IsabelleHOL)
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder in do -- Remove Subsorting from the CASL part of the CspCASL
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder -- specification
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder th_pcfol <- casl2pcfol (caslSign, caslNamedSens)
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder -- Next Remove partial functions
e6d5dbbc3308f05197868806e0b860f4f53875f1Christian Maeder th_cfol <- pcfol2cfol th_pcfol
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder -- Next Translate to IsabelleHOL code
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian Maeder (th_isa_Sig, th_isa_Sens) <- cfol2isabelleHol th_cfol
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian Maeder return (th_isa_Sig, th_isa_Sens, fst th_pcfol, fst th_cfol)
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian Maeder-- | Produce the Isabelle theory which contains the PreAlphabet,
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- Justification Theorems and also the instances code. We need the
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- PFOL signature which is the data part CASL signature after
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder-- translation to PCFOL (i.e. without subsorting) to pass on as an
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederproducePreAlphabet :: String -> CASLSign -> CASLSign ->
6cd33d6101fb1b93baa6d86fac158af18a115108Christian MaederproducePreAlphabet thName caslSign pfolSign =
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder let sortList = Set.toList(sortSet caslSign)
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder -- empty Isabelle signature which imports the data encoding
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder -- and quotient.thy (which is needed for the instances code)
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder isaSignEmpty = Isa.emptySign {Isa.imports = [mkThyNameDataEnc thName
59138b404f12352d103eeffbeaeb3957b90e75fdChristian Maeder , quotientThyS] }
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder -- Start with our empty isabelle theory, add the preAlphabet
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder -- datetype, then all the comparewith functions, then add the
7d0ee72ee91ec305408688b969c43f07b9667c80Christian Maeder -- eq function. Finally add the justification theorems and
7d0ee72ee91ec305408688b969c43f07b9667c80Christian Maeder -- instance of code.
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder (isaSign, isaSens) = addInstansanceOfEquiv
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder $ addJustificationTheorems caslSign pfolSign
0e5b095a19790411e5352fa7cf57cb0388e70472Christian Maeder $ addEqFun sortList
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder $ addAllCompareWithFun caslSign
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder $ addPreAlphabet sortList
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder $ (isaSignEmpty,[])
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder in Theory isaSign (toThSens isaSens)
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder-- | Produce the Isabelle theory which contains the Alphabet
14c56dc499da4bbeaeebeb558ceb755150ae341cChristian Maeder-- construction, and also the bar types and choose
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder-- fucntions for CspCASLProver.
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederproduceAlphabet :: String -> CASLSign -> Theory Isa.Sign Isa.Sentence ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederproduceAlphabet thName caslSign =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder let sortList = Set.toList(sortSet caslSign)
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder -- empty Isabelle signature which imports the preAlphabet encoding
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder isaSignEmpty = Isa.emptySign {
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder Isa.imports = [mkThyNamePreAlphabet thName]}
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder -- Start with our empty isabelle theory, add the Alphabet type
328a85c807f2a95c3f147d10b05927eaf862ebebChristian Maeder -- , then the bar types and finally the choose functions.
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder (isaSign, isaSens) = addAllChooseFunctions sortList
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblett $ addAllBarTypes sortList
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder $ addAlphabetType
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder $ (isaSignEmpty,[])
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder in Theory isaSign (toThSens isaSens)
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers-- | Produce the Isabelle theory which contains the Integration
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- Theorems on data
819e29dba060687cf391e444e0f6ff88c1908cc3Christian MaederproduceIntegrationTheorems :: String -> CASLSign ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederproduceIntegrationTheorems thName caslSign =
140287998aa8592c9c403bd9e308e447ba92ae11Christian Maeder let sortList = Set.toList(sortSet caslSign)
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder -- empty Isabelle signature which imports the alphabet encoding
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder isaSignEmpty = Isa.emptySign {Isa.imports = [mkThyNameAlphabet thName] }
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder -- Start with our empty isabelle theory and add the
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder -- integration theorems.
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers (isaSign, isaSens) = addAllIntegrationTheorems sortList caslSign
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder $ (isaSignEmpty,[])
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder in Theory isaSign (toThSens isaSens)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- | Produce the Isabelle theory which contains the Process Translations and
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- process refinement theorems. We -- need the PCFOL and CFOL signatures of
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder-- the data part after translation to PCFOL and CFOL to pass -- along to the
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder-- process translation.
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian MaederproduceProcesses :: String -> CspCASLSign -> [Named CspCASLSen] ->
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder CASLSign -> CASLSign -> Theory Isa.Sign Isa.Sentence ()
3554301a34639efb6c9961a8571775d0061284c9Christian MaederproduceProcesses thName ccSign ccNnamedSens pcfolSign cfolSign =
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder let caslSign = ccSig2CASLSign ccSign
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder cspSign = ccSig2CspSign ccSign
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder sortList = Set.toList(sortSet caslSign)
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder sortRel' = sortRel caslSign
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder chanNameMap = chans cspSign
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder -- Isabelle signature which imports the integration theorems encoding
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder isaSignEmpty = Isa.emptySign {Isa.imports = [mkThyNameIntThms thName
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder , cspFThyS] }
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder -- Start with our empty isabelle theory and add the
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder -- processes the the process refinement theorems.
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder (isaSign, isaSens) = addProcMap ccNnamedSens caslSign pcfolSign cfolSign
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder $ addProcNameDatatype cspSign
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder $ addDataSetTypes sortList
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder $ addFlatTypes sortList
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder $ addProjFlatFun
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder $ addEventDataType sortRel' chanNameMap
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder $ (isaSignEmpty,[])
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder in Theory isaSign (toThSens isaSens)