{- |

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"