{- |
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 :: String
cspCASLProverS = "CspCASLProver"

-- | The wrapper function that is CspCASL Prover
cspCASLProver :: Prover CspCASLSign CspCASLSen CspCASLMorphism () ()
cspCASLProver :: Prover CspCASLSign CspCASLSen CspCASLMorphism () ()
cspCASLProver = (String
-> ()
-> (String
    -> Theory CspCASLSign CspCASLSen ()
    -> [FreeDefMorphism CspCASLSen CspCASLMorphism]
    -> IO [ProofStatus ()])
-> Prover CspCASLSign CspCASLSen CspCASLMorphism () ()
forall sublogics theory sentence morphism proof_tree.
String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO [ProofStatus proof_tree])
-> ProverTemplate theory sentence morphism sublogics proof_tree
mkProverTemplate String
cspCASLProverS () String
-> Theory CspCASLSign CspCASLSen ()
-> [FreeDefMorphism CspCASLSen CspCASLMorphism]
-> IO [ProofStatus ()]
forall a.
String
-> Theory CspCASLSign CspCASLSen () -> a -> IO [ProofStatus ()]
cspCASLProverProve)
  { proverUsable :: IO (Maybe String)
proverUsable = String -> IO (Maybe String)
checkBinary "isabelle" }

-- | The main cspCASLProver function
cspCASLProverProve :: String -> Theory CspCASLSign CspCASLSen () -> a ->
                      IO [ProofStatus ()]
cspCASLProverProve :: String
-> Theory CspCASLSign CspCASLSen () -> a -> IO [ProofStatus ()]
cspCASLProverProve thName :: String
thName (Theory ccSign :: CspCASLSign
ccSign ccSensThSens :: ThSens CspCASLSen (ProofStatus ())
ccSensThSens) _freedefs :: a
_freedefs =
  let -- get the CASL signature of the data part of the CspcASL theory
      caslSign :: CASLSign
caslSign = CspCASLSign -> CASLSign
ccSig2CASLSign CspCASLSign
ccSign
      -- Get a list of CspCASL named sentences
      ccNamedSens :: [Named CspCASLSen]
ccNamedSens = ThSens CspCASLSen (ProofStatus ()) -> [Named CspCASLSen]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens CspCASLSen (ProofStatus ())
ccSensThSens
      -- A filter to change a CspCASLSen to a CASLSen (if possible)
      caslSenFilter :: CspCASLSen -> Maybe (FORMULA ())
caslSenFilter ccSen :: CspCASLSen
ccSen = case CspCASLSen
ccSen of
        ExtFORMULA (ProcessEq {}) -> Maybe (FORMULA ())
forall a. Maybe a
Nothing
        sen :: CspCASLSen
sen -> FORMULA () -> Maybe (FORMULA ())
forall a. a -> Maybe a
Just (FORMULA () -> Maybe (FORMULA ()))
-> FORMULA () -> Maybe (FORMULA ())
forall a b. (a -> b) -> a -> b
$ Record CspSen (FORMULA ()) (TERM ()) -> CspCASLSen -> FORMULA ()
forall f a b. Record f a b -> FORMULA f -> a
foldFormula ((CspSen -> ()) -> Record CspSen (FORMULA ()) (TERM ())
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord ((CspSen -> ()) -> Record CspSen (FORMULA ()) (TERM ()))
-> (CspSen -> ()) -> Record CspSen (FORMULA ()) (TERM ())
forall a b. (a -> b) -> a -> b
$ () -> CspSen -> ()
forall a b. a -> b -> a
const ()) CspCASLSen
sen
      -- All named CASL sentences from the datapart
      caslNamedSens :: [Named (FORMULA ())]
caslNamedSens = (Named CspCASLSen -> Maybe (Named (FORMULA ())))
-> [Named CspCASLSen] -> [Named (FORMULA ())]
forall a b. (a -> Maybe b) -> [a] -> [b]
Maybe.mapMaybe ((CspCASLSen -> Maybe (FORMULA ()))
-> Named CspCASLSen -> Maybe (Named (FORMULA ()))
forall (m :: * -> *) s t.
Monad m =>
(s -> m t) -> Named s -> m (Named t)
mapNamedM CspCASLSen -> Maybe (FORMULA ())
caslSenFilter) [Named CspCASLSen]
ccNamedSens
      -- Generate data encoding. This may fail.
      Result diag :: [Diagnosis]
diag dataTh :: Maybe (Sign, [Named Sentence], CASLSign, CASLSign)
dataTh = CASLSign
-> [Named (FORMULA ())]
-> Result (Sign, [Named Sentence], CASLSign, CASLSign)
produceDataEncoding CASLSign
caslSign [Named (FORMULA ())]
caslNamedSens
  in case Maybe (Sign, [Named Sentence], CASLSign, CASLSign)
dataTh of
    Nothing -> do
      -- Data translation failed
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Sorry, could not encode the data part:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Diagnosis] -> String
forall a. Show a => a -> String
show [Diagnosis]
diag
      [ProofStatus ()] -> IO [ProofStatus ()]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Just (dataThSig :: Sign
dataThSig, dataThSens :: [Named Sentence]
dataThSens, pcfolSign :: CASLSign
pcfolSign, cfolSign :: CASLSign
cfolSign) -> do
      {- Data translation succeeded
      Write out the data encoding -}
      String -> Theory Sign Sentence () -> IO ()
writeIsaTheory (String -> String
mkThyNameDataEnc String
thName)
                         (Sign -> ThSens Sentence (ProofStatus ()) -> Theory Sign Sentence ()
forall sign sen proof_tree.
sign
-> ThSens sen (ProofStatus proof_tree)
-> Theory sign sen proof_tree
Theory Sign
dataThSig ([Named Sentence] -> ThSens Sentence (ProofStatus ())
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named Sentence]
dataThSens))
      {- Generate and write out the preAlpbate, justification theorems
      and the instances code. -}
      String -> Theory Sign Sentence () -> IO ()
writeIsaTheory (String -> String
mkThyNamePreAlphabet String
thName)
                         (String -> CASLSign -> CASLSign -> Theory Sign Sentence ()
producePreAlphabet String
thName CASLSign
caslSign CASLSign
pcfolSign)
      {- Generate and write out the Alpbatet construction, bar types
      and choose functions. -}
      String -> Theory Sign Sentence () -> IO ()
writeIsaTheory (String -> String
mkThyNameAlphabet String
thName)
                         (String -> CASLSign -> Theory Sign Sentence ()
produceAlphabet String
thName CASLSign
caslSign)
      -- Generate and write out the integration theorems
      String -> Theory Sign Sentence () -> IO ()
writeIsaTheory (String -> String
mkThyNameIntThms String
thName)
                         (String -> CASLSign -> Theory Sign Sentence ()
produceIntegrationTheorems String
thName CASLSign
caslSign)
      {- Generate and Isabelle to prove the process refinements (also produces
      the processes) -}
      IsaEditor
-> String -> Theory Sign Sentence () -> () -> IO [ProofStatus ()]
forall a.
IsaEditor
-> String -> Theory Sign Sentence () -> a -> IO [ProofStatus ()]
isaProve IsaEditor
JEdit String
thName
        (String
-> CspCASLSign
-> [Named CspCASLSen]
-> CASLSign
-> CASLSign
-> Theory Sign Sentence ()
produceProcesses String
thName CspCASLSign
ccSign [Named CspCASLSen]
ccNamedSens CASLSign
pcfolSign CASLSign
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
-> [Named (FORMULA ())]
-> Result (Sign, [Named Sentence], CASLSign, CASLSign)
produceDataEncoding caslSign :: CASLSign
caslSign caslNamedSens :: [Named (FORMULA ())]
caslNamedSens =
    let -- Comorphisms
        casl2pcfol :: (CASLSign, [Named (FORMULA ())])
-> Result (CASLSign, [Named (FORMULA ())])
casl2pcfol = CASL2PCFOL
-> (CASLSign, [Named (FORMULA ())])
-> Result (CASLSign, [Named (FORMULA ())])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory CASL2PCFOL
CASL2PCFOL.CASL2PCFOL
        pcfol2cfol :: (CASLSign, [Named (FORMULA ())])
-> Result (CASLSign, [Named (FORMULA ())])
pcfol2cfol = CASL2SubCFOL
-> (CASLSign, [Named (FORMULA ())])
-> Result (CASLSign, [Named (FORMULA ())])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory (CASL2SubCFOL
 -> (CASLSign, [Named (FORMULA ())])
 -> Result (CASLSign, [Named (FORMULA ())]))
-> CASL2SubCFOL
-> (CASLSign, [Named (FORMULA ())])
-> Result (CASLSign, [Named (FORMULA ())])
forall a b. (a -> b) -> a -> b
$ Bool -> FormulaTreatment -> CASL2SubCFOL
CASL2SubCFOL.CASL2SubCFOL Bool
True
                     FormulaTreatment
CASL2SubCFOL.AllSortBottoms
        cfol2isabelleHol :: (CASLSign, [Named (FORMULA ())]) -> Result (Sign, [Named Sentence])
cfol2isabelleHol = CFOL2IsabelleHOL
-> (CASLSign, [Named (FORMULA ())])
-> Result (Sign, [Named Sentence])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory CFOL2IsabelleHOL
CFOL2IsabelleHOL.CFOL2IsabelleHOL
    in do
      {- Remove Subsorting from the CASL part of the CspCASL
      specification -}
      (CASLSign, [Named (FORMULA ())])
th_pcfol <- (CASLSign, [Named (FORMULA ())])
-> Result (CASLSign, [Named (FORMULA ())])
casl2pcfol (CASLSign
caslSign, [Named (FORMULA ())]
caslNamedSens)
      -- Next Remove partial functions
      (CASLSign, [Named (FORMULA ())])
th_cfol <- (CASLSign, [Named (FORMULA ())])
-> Result (CASLSign, [Named (FORMULA ())])
pcfol2cfol (CASLSign, [Named (FORMULA ())])
th_pcfol
      -- Next Translate to IsabelleHOL code
      (th_isa_Sig :: Sign
th_isa_Sig, th_isa_Sens :: [Named Sentence]
th_isa_Sens) <- (CASLSign, [Named (FORMULA ())]) -> Result (Sign, [Named Sentence])
cfol2isabelleHol (CASLSign, [Named (FORMULA ())])
th_cfol
      (Sign, [Named Sentence], CASLSign, CASLSign)
-> Result (Sign, [Named Sentence], CASLSign, CASLSign)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
th_isa_Sig, [Named Sentence]
th_isa_Sens, (CASLSign, [Named (FORMULA ())]) -> CASLSign
forall a b. (a, b) -> a
fst (CASLSign, [Named (FORMULA ())])
th_pcfol, (CASLSign, [Named (FORMULA ())]) -> CASLSign
forall a b. (a, b) -> a
fst (CASLSign, [Named (FORMULA ())])
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 :: String -> CASLSign -> CASLSign -> Theory Sign Sentence ()
producePreAlphabet thName :: String
thName caslSign :: CASLSign
caslSign pfolSign :: CASLSign
pfolSign =
    let sortList :: [SORT]
sortList = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (CASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet CASLSign
caslSign)
        {- empty Isabelle signature which imports the data encoding
        and quotient.thy (which is needed for the instances code) -}
        isaSignEmpty :: Sign
isaSignEmpty = Sign
Isa.emptySign {imports :: [String]
Isa.imports = [String -> String
mkThyNameDataEnc String
thName
                                                    , String
quotientThyS] }
        -- Start with our empty Isabelle theory, add the constructs
        (isaSign :: Sign
isaSign, isaSens :: [Named Sentence]
isaSens) = (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
addInstanceOfEquiv
                           ((Sign, [Named Sentence]) -> (Sign, [Named Sentence]))
-> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
forall a b. (a -> b) -> a -> b
$ CASLSign
-> CASLSign -> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
addJustificationTheorems CASLSign
caslSign CASLSign
pfolSign
                           ((Sign, [Named Sentence]) -> (Sign, [Named Sentence]))
-> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
forall a b. (a -> b) -> a -> b
$ CASLSign
-> CASLSign -> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
addAllGaAxiomsCollections CASLSign
caslSign CASLSign
pfolSign
                           ((Sign, [Named Sentence]) -> (Sign, [Named Sentence]))
-> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
forall a b. (a -> b) -> a -> b
$ [SORT] -> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
addEqFun [SORT]
sortList
                           ((Sign, [Named Sentence]) -> (Sign, [Named Sentence]))
-> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
forall a b. (a -> b) -> a -> b
$ CASLSign -> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
addAllCompareWithFun CASLSign
caslSign
                           ((Sign, [Named Sentence]) -> (Sign, [Named Sentence]))
-> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
forall a b. (a -> b) -> a -> b
$ [SORT] -> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
addPreAlphabet [SORT]
sortList
                             (Sign
isaSignEmpty, [])
    in Sign -> ThSens Sentence (ProofStatus ()) -> Theory Sign Sentence ()
forall sign sen proof_tree.
sign
-> ThSens sen (ProofStatus proof_tree)
-> Theory sign sen proof_tree
Theory Sign
isaSign ([Named Sentence] -> ThSens Sentence (ProofStatus ())
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named Sentence]
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 :: String -> CASLSign -> Theory Sign Sentence ()
produceAlphabet thName :: String
thName caslSign :: CASLSign
caslSign =
    let sortList :: [SORT]
sortList = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (CASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet CASLSign
caslSign)
        -- empty Isabelle signature which imports the preAlphabet encoding
        isaSignEmpty :: Sign
isaSignEmpty = Sign
Isa.emptySign {
                         imports :: [String]
Isa.imports = [String -> String
mkThyNamePreAlphabet String
thName]}
        {- Start with our empty isabelle theory, add the Alphabet type
        , then the bar types and finally the choose functions. -}
        (isaSign :: Sign
isaSign, isaSens :: [Named Sentence]
isaSens) = [SORT] -> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
addAllChooseFunctions [SORT]
sortList
                           ((Sign, [Named Sentence]) -> (Sign, [Named Sentence]))
-> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
forall a b. (a -> b) -> a -> b
$ [SORT] -> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
addAllBarTypes [SORT]
sortList
                           ((Sign, [Named Sentence]) -> (Sign, [Named Sentence]))
-> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
forall a b. (a -> b) -> a -> b
$ (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
addAlphabetType
                             (Sign
isaSignEmpty, [])
    in Sign -> ThSens Sentence (ProofStatus ()) -> Theory Sign Sentence ()
forall sign sen proof_tree.
sign
-> ThSens sen (ProofStatus proof_tree)
-> Theory sign sen proof_tree
Theory Sign
isaSign ([Named Sentence] -> ThSens Sentence (ProofStatus ())
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named Sentence]
isaSens)

{- |Produce the Isabelle theory which contains the Integration
Theorems on data -}
produceIntegrationTheorems :: String -> CASLSign ->
                              Theory Isa.Sign Isa.Sentence ()
produceIntegrationTheorems :: String -> CASLSign -> Theory Sign Sentence ()
produceIntegrationTheorems thName :: String
thName caslSign :: CASLSign
caslSign =
    let sortList :: [SORT]
sortList = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (CASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet CASLSign
caslSign)
        -- empty Isabelle signature which imports the alphabet encoding
        isaSignEmpty :: Sign
isaSignEmpty = Sign
Isa.emptySign {imports :: [String]
Isa.imports = [String -> String
mkThyNameAlphabet String
thName] }
        {- Start with our empty isabelle theory and add the
        integration theorems. -}
        (isaSign :: Sign
isaSign, isaSens :: [Named Sentence]
isaSens) = [SORT]
-> CASLSign -> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
addAllIntegrationTheorems [SORT]
sortList CASLSign
caslSign
                             (Sign
isaSignEmpty, [])
    in Sign -> ThSens Sentence (ProofStatus ()) -> Theory Sign Sentence ()
forall sign sen proof_tree.
sign
-> ThSens sen (ProofStatus proof_tree)
-> Theory sign sen proof_tree
Theory Sign
isaSign ([Named Sentence] -> ThSens Sentence (ProofStatus ())
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named Sentence]
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 :: String
-> CspCASLSign
-> [Named CspCASLSen]
-> CASLSign
-> CASLSign
-> Theory Sign Sentence ()
produceProcesses thName :: String
thName ccSign :: CspCASLSign
ccSign ccNamedSens :: [Named CspCASLSen]
ccNamedSens pcfolSign :: CASLSign
pcfolSign cfolSign :: CASLSign
cfolSign =
    let caslSign :: CASLSign
caslSign = CspCASLSign -> CASLSign
ccSig2CASLSign CspCASLSign
ccSign
        cspSign :: CspSign
cspSign = CspCASLSign -> CspSign
ccSig2CspSign CspCASLSign
ccSign
        sortList :: [SORT]
sortList = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (CASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet CASLSign
caslSign)
        sortRel' :: Rel SORT
sortRel' = CASLSign -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel CASLSign
caslSign
        chanNameMap :: ChanNameMap
chanNameMap = CspSign -> ChanNameMap
chans CspSign
cspSign
        {- Isabelle signature which imports the integration theorems encoding
        and CSP_F -}
        isaSignEmpty :: Sign
isaSignEmpty = Sign
Isa.emptySign {imports :: [String]
Isa.imports = [String -> String
mkThyNameIntThms String
thName
                                                    , String
cspFThyS] }
        {- Start with our empty isabelle theory and add the
        processes the the process refinement theorems. -}
        (isaSign :: Sign
isaSign, isaSens :: [Named Sentence]
isaSens) =
            [Named CspCASLSen]
-> CspCASLSign
-> CASLSign
-> CASLSign
-> (Sign, [Named Sentence])
-> (Sign, [Named Sentence])
addProcTheorems [Named CspCASLSen]
ccNamedSens CspCASLSign
ccSign CASLSign
pcfolSign CASLSign
cfolSign
          ((Sign, [Named Sentence]) -> (Sign, [Named Sentence]))
-> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
forall a b. (a -> b) -> a -> b
$ [Named CspCASLSen]
-> CspCASLSign
-> CASLSign
-> CASLSign
-> (Sign, [Named Sentence])
-> (Sign, [Named Sentence])
addProcMap [Named CspCASLSen]
ccNamedSens CspCASLSign
ccSign CASLSign
pcfolSign CASLSign
cfolSign
          ((Sign, [Named Sentence]) -> (Sign, [Named Sentence]))
-> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
forall a b. (a -> b) -> a -> b
$ CspSign -> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
addProcNameDatatype CspSign
cspSign
          ((Sign, [Named Sentence]) -> (Sign, [Named Sentence]))
-> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
forall a b. (a -> b) -> a -> b
$ [SORT] -> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
addFlatTypes [SORT]
sortList
          ((Sign, [Named Sentence]) -> (Sign, [Named Sentence]))
-> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
forall a b. (a -> b) -> a -> b
$ (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
addProjFlatFun
          ((Sign, [Named Sentence]) -> (Sign, [Named Sentence]))
-> (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
forall a b. (a -> b) -> a -> b
$ Rel SORT
-> ChanNameMap
-> (Sign, [Named Sentence])
-> (Sign, [Named Sentence])
addEventDataType Rel SORT
sortRel' ChanNameMap
chanNameMap
            (Sign
isaSignEmpty, [])
    in Sign -> ThSens Sentence (ProofStatus ()) -> Theory Sign Sentence ()
forall sign sen proof_tree.
sign
-> ThSens sen (ProofStatus proof_tree)
-> Theory sign sen proof_tree
Theory Sign
isaSign ([Named Sentence] -> ThSens Sentence (ProofStatus ())
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named Sentence]
isaSens)