content: {- |
  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 = "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"
  