d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad Kienle{- |

d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad KienleModule : ./CspCASLProver/Consts.hs

d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad KienleDescription : Constants and related fucntions for CspCASLProver

d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad KienleCopyright : (c) Liam O'Reilly and Markus Roggenbach,

d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad Kienle Swansea University 2008

d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad KienleLicense : GPLv2 or higher, see LICENSE.txt

d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad Kienle

d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad KienleMaintainer : csliam@swansea.ac.uk

d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad KienleStability : provisional

d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad KienlePortability : non-portable (imports Logic.Logic)

d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad Kienle

d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad KienleConstants and related fucntions for CspCASLProver.

d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad Kienle

d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad Kienle-}

d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad Kienle

d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad Kienlemodule CspCASLProver.Consts

d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad Kienle ( alphabetS

d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad Kienle , alphabetType

d1d13ae8cda5f9ce5fa6d4aeddb85232a3b3b562Chad Kienle , 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"