{- |

Module : $Header$

Description : interface to the CspCASLProver (Isabelle based) theorem prover

Copyright : (c) Liam O'Reilly and Markus Roggenbach, Swansea University 2009

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.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 (CASLFORMULA)

import CASL.Sign (CASLSign, Sign(..))

import Common.AS_Annotation (Named, mapNamedM)

import Common.Result

import qualified Comorphisms.CASL2PCFOL as CASL2PCFOL

import qualified Comorphisms.CASL2SubCFOL as CASL2SubCFOL

import qualified Comorphisms.CFOL2IsabelleHOL as CFOL2IsabelleHOL

import CspCASL.SignCSP (ccSig2CASLSign, ccSig2CspSign, CspCASLSign

, CspCASLSen(..) , CspMorphism)

import CspCASLProver.Consts

import CspCASLProver.IsabelleUtils

import CspCASLProver.Utils

import qualified Data.Maybe as Maybe

import qualified Data.Set as Set

import Isabelle.IsaProve (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 CspMorphism () ()

cspCASLProver = mkProverTemplate cspCASLProverS () cspCASLProverProve

-- | The main cspCASLProver function

cspCASLProverProve :: String -> Theory CspCASLSign CspCASLSen () -> a ->

IO([Proof_status ()])

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

CASLSen sen -> Just sen

ProcessEq _ _ _ _ -> Nothing

-- All named CASL sentences from the datapart

caslNamedSens = Maybe.catMaybes $

map (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 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.defaultCASL2SubCFOL)

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 preAlphabet

-- datetype, then all the comparewith functions, then add the

-- eq function. Finally add the justification theorems and

-- instance of code.

(isaSign, isaSens) = addInstansanceOfEquiv

$ addJustificationTheorems 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 ccNnamedSens pcfolSign cfolSign =

let caslSign = ccSig2CASLSign ccSign

cspSign = ccSig2CspSign ccSign

-- Isabelle sgnature 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) = addProcMap ccNnamedSens caslSign pcfolSign cfolSign

$ addProcNameDatatype cspSign

$ (isaSignEmpty,[])

in Theory isaSign (toThSens isaSens)