{- |
Module      :  ./CspCASLProver/Consts.hs
Description :  Constants and related fucntions for CspCASLProver
Copyright   :  (c) Liam O'Reilly and Markus Roggenbach,
                   Swansea University 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  csliam@swansea.ac.uk
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

Constants and related fucntions for CspCASLProver.

-}

module CspCASLProver.Consts
    ( alphabetS
    , alphabetType
    , binEq_PreAlphabet
    , classOp
    , classS
    , convertChannelString
    , convertFQProcessName2String
    , convertSort2String
    , cspFThyS
    , eq_PreAlphabetS
    , eq_PreAlphabetV
    , equivTypeClassS
    , eventS
    , eventType
    , flatS
    , flatOp
    , preAlphabetQuotType
    , preAlphabetS
    , preAlphabetSimS
    , preAlphabetType
    , projFlatS
    , projFlatOp
    , lemmasCCProverDecompositionThmsS
    , lemmasCCProverInjectivityThmsS
    , lemmasEmbInjAxS
    , lemmasIdentityAxS
    , lemmasNotDefBotAxS
    , lemmasTotalityAxS
    , lemmasTransAxS
    , mkChooseFunName
    , mkChooseFunOp
    , mkCompareWithFunName
    , mkPreAlphabetConstructor
    , mkPreAlphabetConstructorOp
    , mkProcNameConstructor
    , mkSortBarAbsString
    , mkSortBarAbsOp
    , mkSortBarRepOp
    , mkSortBarString
    , mkSortBarType
    , mkSortFlatString
    , mkThyNameAlphabet
    , mkThyNameDataEnc
    , mkThyNameIntThms
    , mkThyNamePreAlphabet
    , procMapS
    , procMapType
    , procNameType
    , quotEqualityS
    , quotientThyS
    , reflexivityTheoremS
    , symmetryTheoremS
    , transitivityS
    ) where

import CASL.AS_Basic_CASL (SORT)
import CspCASL.AS_CspCASL_Process (CHANNEL_NAME, FQ_PROCESS_NAME (..))
import Isabelle.IsaConsts (binVNameAppl, conDouble, mkFunType, termAppl)
import Isabelle.IsaSign (BaseSig (..), Term, Typ (..), VName (..))
import Isabelle.Translate (showIsaTypeT, transString)

-- | Name for the CspCASLProver's Alphabet
alphabetS :: String
alphabetS :: String
alphabetS = "Alphabet"

-- | Type for the CspCASLProver's Alphabet
alphabetType :: Typ
alphabetType :: Typ
alphabetType = Type :: String -> Sort -> [Typ] -> Typ
Type {typeId :: String
typeId = String
alphabetS,
                     typeSort :: Sort
typeSort = [],
                     typeArgs :: [Typ]
typeArgs = []}

-- | String for the name extension of CspCASLProver's bar types
barExtS :: String
barExtS :: String
barExtS = "_Bar"

{- | Isabelle fucntion to compare eqaulity of two elements of the
PreAlphabet. -}
binEq_PreAlphabet :: Term -> Term -> Term
binEq_PreAlphabet :: Term -> Term -> Term
binEq_PreAlphabet = VName -> Term -> Term -> Term
binVNameAppl VName
eq_PreAlphabetV

-- | Type for (ProcName,Alpahbet) proc
cCProverProcType :: Typ
cCProverProcType :: Typ
cCProverProcType = Type :: String -> Sort -> [Typ] -> Typ
Type {typeId :: String
typeId = String
procS,
                         typeSort :: Sort
typeSort = [],
                         typeArgs :: [Typ]
typeArgs = [Typ
procNameType, Typ
eventType]}

-- | Isabelle operation for the class operation
classOp :: Term -> Term
classOp :: Term -> Term
classOp = Term -> Term -> Term
termAppl (String -> Term
conDouble String
classS)

-- | String for the class operation
classS :: String
classS :: String
classS = "class"

{- | Function that takes a channel name produces the
CspCASLProver's constructor for that channel. -}
convertChannelString :: CHANNEL_NAME -> String
convertChannelString :: CHANNEL_NAME -> String
convertChannelString = CHANNEL_NAME -> String
forall a. Show a => a -> String
show

-- | Convert a SORT to a string
convertSort2String :: SORT -> String
convertSort2String :: CHANNEL_NAME -> String
convertSort2String s :: CHANNEL_NAME
s = String -> String
transString (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ CHANNEL_NAME -> BaseSig -> String
showIsaTypeT CHANNEL_NAME
s BaseSig
Main_thy

-- | Convert a process name to a string
convertFQProcessName2String :: FQ_PROCESS_NAME -> String
convertFQProcessName2String :: FQ_PROCESS_NAME -> String
convertFQProcessName2String fqPn :: FQ_PROCESS_NAME
fqPn =
  case FQ_PROCESS_NAME
fqPn of
    PROCESS_NAME _ ->
      String -> String
forall a. HasCallStack => String -> a
error "CspCASLProver.Consts.convertFQProcessName2String:\
           \ Tried to convert non fully qualified process name to string."
    FQ_PROCESS_NAME pn :: CHANNEL_NAME
pn _ -> CHANNEL_NAME -> String
forall a. Show a => a -> String
show CHANNEL_NAME
pn

-- |  Theory file name for CSP_F of CSP-Prover
cspFThyS :: String
cspFThyS :: String
cspFThyS = "CSP_F"

{- | String of the name of the function to compare eqaulity of two
elements of the PreAlphabet. -}
eq_PreAlphabetS :: String
eq_PreAlphabetS :: String
eq_PreAlphabetS = "eq_PreAlphabet"

{- | VName of the name of the function to compare eqaulity of two
elements of the PreAlphabet. -}
eq_PreAlphabetV :: VName
eq_PreAlphabetV :: VName
eq_PreAlphabetV = String -> Maybe AltSyntax -> VName
VName String
eq_PreAlphabetS Maybe AltSyntax
forall a. Maybe a
Nothing

{- | String for the name of the axiomatic type class of equivalence
relations part 2 -}
equivTypeClassS :: String
equivTypeClassS :: String
equivTypeClassS = "equiv"

-- | String of the name of CspCASLProver's Event datatype.
eventS :: String
eventS :: String
eventS = "Event"

-- | Type for the CspCASLProver's Event datatype
eventType :: Typ
eventType :: Typ
eventType = Type :: String -> Sort -> [Typ] -> Typ
Type {typeId :: String
typeId = String
eventS,
                  typeSort :: Sort
typeSort = [],
                  typeArgs :: [Typ]
typeArgs = []}

{- | String of the name of constructor for a plain event without a channel,
effectivly this is the channel whos name is Flat. Also used for the names
of the flat types. -}
flatS :: String
flatS :: String
flatS = "Flat"

-- | Function that takes a Term and adds a flat around it
flatOp :: Term -> Term
flatOp :: Term -> Term
flatOp = Term -> Term -> Term
termAppl (String -> Term
conDouble String
flatS)

{- |Name for the lemma which is the collection of our decomposition axioms that
we produce. -}
lemmasCCProverDecompositionThmsS :: String
lemmasCCProverDecompositionThmsS :: String
lemmasCCProverDecompositionThmsS = "ccproverDecompositionAxs"

{- |Name for the lemma which is the collection of our injectivity axioms that we
produce. -}
lemmasCCProverInjectivityThmsS :: String
lemmasCCProverInjectivityThmsS :: String
lemmasCCProverInjectivityThmsS = "ccproverInjectivityThms"

-- | Name for the lemma which is the collection of embedding injectivity axioms.
lemmasEmbInjAxS :: String
lemmasEmbInjAxS :: String
lemmasEmbInjAxS = "allGaEmbInjAx"

-- | Name for the lemma which is the collection of identity axioms.
lemmasIdentityAxS :: String
lemmasIdentityAxS :: String
lemmasIdentityAxS = "allGaIdentityAx"

-- | Name for the lemma which is the collection of not defined bottom axioms.
lemmasNotDefBotAxS :: String
lemmasNotDefBotAxS :: String
lemmasNotDefBotAxS = "allGaNotDefBotAx"

-- | Name for the lemma which is the collection of totality axioms.
lemmasTotalityAxS :: String
lemmasTotalityAxS :: String
lemmasTotalityAxS = "allGaTotAx"

-- | Name for the lemma which is the collection of transitivity axioms.
lemmasTransAxS :: String
lemmasTransAxS :: String
lemmasTransAxS = "allGaTransAx"

{- | Function that takes a sort and outputs the function name for the
corresponing choose function -}
mkChooseFunName :: SORT -> String
mkChooseFunName :: CHANNEL_NAME -> String
mkChooseFunName sort :: CHANNEL_NAME
sort = "choose_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ CHANNEL_NAME -> String
mkPreAlphabetConstructor CHANNEL_NAME
sort

{- | Function that takes a sort and outputs the Isabelle function for the
corresponing choose function -}
mkChooseFunOp :: SORT -> Term -> Term
mkChooseFunOp :: CHANNEL_NAME -> Term -> Term
mkChooseFunOp s :: CHANNEL_NAME
s = Term -> Term -> Term
termAppl (String -> Term
conDouble (CHANNEL_NAME -> String
mkChooseFunName CHANNEL_NAME
s))

{- | Function that takes a sort and outputs the function name for the
corresponing compare_with function -}
mkCompareWithFunName :: SORT -> String
mkCompareWithFunName :: CHANNEL_NAME -> String
mkCompareWithFunName sort :: CHANNEL_NAME
sort = "compare_with_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ CHANNEL_NAME -> String
mkPreAlphabetConstructor CHANNEL_NAME
sort

{- | Function that returns the constructor of PreAlphabet for a given
sort -}
mkPreAlphabetConstructor :: SORT -> String
mkPreAlphabetConstructor :: CHANNEL_NAME -> String
mkPreAlphabetConstructor sort :: CHANNEL_NAME
sort = "C_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ CHANNEL_NAME -> String
convertSort2String CHANNEL_NAME
sort

{- | Function that returns the (Isabelle function for the) constructor of
PreAlphabet for a given sort -}
mkPreAlphabetConstructorOp :: SORT -> Term -> Term
mkPreAlphabetConstructorOp :: CHANNEL_NAME -> Term -> Term
mkPreAlphabetConstructorOp s :: CHANNEL_NAME
s = Term -> Term -> Term
termAppl (String -> Term
conDouble (CHANNEL_NAME -> String
mkPreAlphabetConstructor CHANNEL_NAME
s))

{- | Given a process name this fucntion returns a unique constructor for that
process name. This is a helper functin when buildign the process name data
type. -}
mkProcNameConstructor :: FQ_PROCESS_NAME -> String
mkProcNameConstructor :: FQ_PROCESS_NAME -> String
mkProcNameConstructor fqPn :: FQ_PROCESS_NAME
fqPn = case FQ_PROCESS_NAME
fqPn of
    PROCESS_NAME _ ->
      String -> String
forall a. HasCallStack => String -> a
error "CspCASLProver.Consts.mkProcNameConstructor:\
           \ Tried to make a non fully qualified process name as a\
           \ constructor (string)."
    FQ_PROCESS_NAME pn :: CHANNEL_NAME
pn _ -> CHANNEL_NAME -> String
forall a. Show a => a -> String
show CHANNEL_NAME
pn

{- | Converts a sort in to the corresponding bar sort represented as a
string -}
mkSortBarString :: SORT -> String
mkSortBarString :: CHANNEL_NAME -> String
mkSortBarString s :: CHANNEL_NAME
s = CHANNEL_NAME -> String
convertSort2String CHANNEL_NAME
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
barExtS

-- | Converts a sort in to the corresponding bar sort type
mkSortBarType :: SORT -> Typ
mkSortBarType :: CHANNEL_NAME -> Typ
mkSortBarType sort :: CHANNEL_NAME
sort = Type :: String -> Sort -> [Typ] -> Typ
Type {typeId :: String
typeId = CHANNEL_NAME -> String
mkSortBarString CHANNEL_NAME
sort,
                           typeSort :: Sort
typeSort = [],
                           typeArgs :: [Typ]
typeArgs = []}

{- | Given a sort this function produces the function name (string) of the built
in Isabelle fucntion that corresponds to the abstraction function of the
type that sort_bar. -}
mkSortBarAbsString :: SORT -> String
mkSortBarAbsString :: CHANNEL_NAME -> String
mkSortBarAbsString s :: CHANNEL_NAME
s = "Abs_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ CHANNEL_NAME -> String
convertSort2String CHANNEL_NAME
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
barExtS

{- | Given a sort this function produces the a function on the abstract syntax
of Isabelle that represents the built in Isabelle fucntion that corresponds
to the abstraction function of the type sort_bar. -}
mkSortBarAbsOp :: SORT -> Term -> Term
mkSortBarAbsOp :: CHANNEL_NAME -> Term -> Term
mkSortBarAbsOp s :: CHANNEL_NAME
s = Term -> Term -> Term
termAppl (String -> Term
conDouble (CHANNEL_NAME -> String
mkSortBarAbsString CHANNEL_NAME
s))

{- | Given a sort this function produces the function name (string) of the built
in Isabelle fucntion that corresponds to the representation function of the
type sort_bar. -}
mkSortBarRepString :: SORT -> String
mkSortBarRepString :: CHANNEL_NAME -> String
mkSortBarRepString s :: CHANNEL_NAME
s = "Rep_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ CHANNEL_NAME -> String
convertSort2String CHANNEL_NAME
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
barExtS

{- | Given a sort this function produces the a function on the abstract syntax
of Isabelle that represents the built in Isabelle fucntion that corresponds
to the representation function of the type sort_bar. -}
mkSortBarRepOp :: SORT -> Term -> Term
mkSortBarRepOp :: CHANNEL_NAME -> Term -> Term
mkSortBarRepOp s :: CHANNEL_NAME
s = Term -> Term -> Term
termAppl (String -> Term
conDouble (CHANNEL_NAME -> String
mkSortBarRepString CHANNEL_NAME
s))

{- | Converts asort in to the corresponding flat type for that sort represented
as a string. This is used in the construction of the channels and is linked
with the type event. -}
mkSortFlatString :: SORT -> String
mkSortFlatString :: CHANNEL_NAME -> String
mkSortFlatString s :: CHANNEL_NAME
s = CHANNEL_NAME -> String
convertSort2String CHANNEL_NAME
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
flatS

{- | Created a name for the theory file which stores the alphabet
construction for CspCASLProver. -}
mkThyNameAlphabet :: String -> String
mkThyNameAlphabet :: String -> String
mkThyNameAlphabet thName :: String
thName = String
thName String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_alphabet"

{- | Created a name for the theory file which stores the data encoding
for CspCASLProver. -}
mkThyNameDataEnc :: String -> String
mkThyNameDataEnc :: String -> String
mkThyNameDataEnc thName :: String
thName = String
thName String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_dataenc"

{- | Created a name for the theory file which stores the Alphabet
construction and instances code for CspCASLProver. -}
mkThyNamePreAlphabet :: String -> String
mkThyNamePreAlphabet :: String -> String
mkThyNamePreAlphabet thName :: String
thName = String
thName String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_prealphabet"

{- | Created a name for the theory file which stores the Integration
Theorems for CspCASLProver. -}
mkThyNameIntThms :: String -> String
mkThyNameIntThms :: String -> String
mkThyNameIntThms thName :: String
thName = String
thName String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_integrationThms"

-- | Type for CspCASLProver's preAlphabet quot
preAlphabetQuotType :: Typ
preAlphabetQuotType :: Typ
preAlphabetQuotType = Type :: String -> Sort -> [Typ] -> Typ
Type {typeId :: String
typeId = String
quotS,
                            typeSort :: Sort
typeSort = [],
                            typeArgs :: [Typ]
typeArgs = [Typ
preAlphabetType]}

-- | Name for CspCASLProver's PreAlphabet
preAlphabetS :: String
preAlphabetS :: String
preAlphabetS = "PreAlphabet"

preAlphabetSimS :: String
preAlphabetSimS :: String
preAlphabetSimS = "preAlphabet_sim"

-- | Type for CspCASLProver's PreAlphabet
preAlphabetType :: Typ
preAlphabetType :: Typ
preAlphabetType = Type :: String -> Sort -> [Typ] -> Typ
Type {typeId :: String
typeId = String
preAlphabetS,
                        typeSort :: Sort
typeSort = [],
                        typeArgs :: [Typ]
typeArgs = []}

{- | Name for CspCASLProver's function for mapping process names to
actual processes -}
procMapS :: String
procMapS :: String
procMapS = "ProcMap"

{- | Type for CspCASLProver's function for mapping process names to
actual processes -}
procMapType :: Typ
procMapType :: Typ
procMapType = Typ -> Typ -> Typ
mkFunType Typ
procNameType Typ
cCProverProcType

-- | Name for CspCASLProver's datatype of process names
procNameS :: String
procNameS :: String
procNameS = "ProcName"

-- | Type for CspCASLProver's datatype of process names
procNameType :: Typ
procNameType :: Typ
procNameType = Type :: String -> Sort -> [Typ] -> Typ
Type {typeId :: String
typeId = String
procNameS,
                     typeSort :: Sort
typeSort = [],
                     typeArgs :: [Typ]
typeArgs = []}

-- | Name for CspProver's ('pn, 'a) proc type
procS :: String
procS :: String
procS = "proc"

{- | Name of CspCASLProver's function for projecting a Flat Event back to the
type Alphabet -}
projFlatS :: String
projFlatS :: String
projFlatS = "projFlat"

-- | Apply the CspCASLProvers projFlat function to an isabelle term
projFlatOp :: Term -> Term
projFlatOp :: Term -> Term
projFlatOp = Term -> Term -> Term
termAppl (String -> Term
conDouble String
projFlatS)

-- | Name for IsabelleHOL quot type
quotS :: String
quotS :: String
quotS = "quot"

quotEqualityS :: String
quotEqualityS :: String
quotEqualityS = "quot_equality"

quotientThyS :: String
quotientThyS :: String
quotientThyS = "Quotient_Type"

reflexivityTheoremS :: String
reflexivityTheoremS :: String
reflexivityTheoremS = "eq_refl"

symmetryTheoremS :: String
symmetryTheoremS :: String
symmetryTheoremS = "eq_symm"

transitivityS :: String
transitivityS :: String
transitivityS = "eq_trans"