{- |
Module      :  $Header$
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 = "Alphabet"

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

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

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

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

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

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

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

-- | Convert a SORT to a string
convertSort2String :: SORT -> String
convertSort2String s = transString $ showIsaTypeT s Main_thy

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

-- |  Theory file name for CSP_F of CSP-Prover
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 = "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_PreAlphabetS Nothing

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

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

-- | Type for the CspCASLProver's Event datatype
eventType :: Typ
eventType = Type {typeId = eventS,
                  typeSort = [],
                  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 = "Flat"

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

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

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

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

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

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

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

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

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

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

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

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

{- | Function that returns the (Isabelle function for the) constructor of
PreAlphabet for a given sort -}
mkPreAlphabetConstructorOp :: SORT -> Term -> Term
mkPreAlphabetConstructorOp s = termAppl (conDouble (mkPreAlphabetConstructor 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 fqPn = case fqPn of
    PROCESS_NAME _ ->
      error "CspCASLProver.Consts.mkProcNameConstructor:\
           \ Tried to make a non fully qualified process name as a\
           \ constructor (string)."
    FQ_PROCESS_NAME pn _ -> show pn

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

-- | Converts a sort in to the corresponding bar sort type
mkSortBarType :: SORT -> Typ
mkSortBarType sort = Type {typeId = mkSortBarString sort,
                           typeSort = [],
                           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 s = "Abs_" ++ convertSort2String s ++ 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 s = termAppl (conDouble (mkSortBarAbsString 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 s = "Rep_" ++ convertSort2String s ++ 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 s = termAppl (conDouble (mkSortBarRepString 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 s = convertSort2String s ++ "_" ++ flatS

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

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

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

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

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

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

preAlphabetSimS :: String
preAlphabetSimS = "preAlphabet_sim"

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

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

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

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

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

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

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

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

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

quotEqualityS :: String
quotEqualityS = "quot_equality"

quotientThyS :: String
quotientThyS = "Quotient_Type"

reflexivityTheoremS :: String
reflexivityTheoremS = "eq_refl"

symmetryTheoremS :: String
symmetryTheoremS = "eq_symm"

transitivityS :: String
transitivityS = "eq_trans"
