{- |
Module : ./CspCASLProver/CspProverConsts.hs
Description : Isabelle Abstract syntax constants for CSP-Prover operations
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 : portable
Isabelle Abstract syntax constants for CSP-Prover operations.
-}
module CspCASLProver.CspProverConsts
( cspProverbinEqF
, cspProver_NamedProcOp
, cspProver_skipOp
, cspProver_stopOp
, cspProver_divOp
, cspProver_runOp
, cspProver_chaosOp
, cspProver_action_prefixOp
, cspProver_external_prefix_choiceOp
, cspProver_internal_prefix_choiceOp
, cspProver_sequenceOp
, cspProver_external_choiceOp
, cspProver_internal_choiceOp
, cspProver_interleavingOp
, cspProver_synchronousOp
, cspProver_general_parallelOp
, cspProver_alphabetised_parallelOp
, cspProver_hidingOp
, cspProver_renamingOp
, cspProver_conditionalOp
, cspProver_chan_nondeterministic_sendOp
, cspProver_chan_sendOp
, cspProver_chan_recOp
) where
import Isabelle.IsaSign as IsaSign
import Isabelle.IsaConsts (binVNameAppl, con, termAppl)
{- Symbols for CspProver
These symbols and priorities have come from the CSP-Prover source code -}
-- | binary junctors
cspProverEqV :: VName
cspProverEqV = VName "op =F" $ Just $ AltSyntax "(_ =F/ _)" [50, 51] 50
cspProverbinEqF :: Term -> Term -> Term
cspProverbinEqF = binVNameAppl cspProverEqV
-- | Name Process symbol
cspProver_NamedProcS :: String
cspProver_NamedProcS = "Proc_name"
cspProver_NamedProcAltS :: String
cspProver_NamedProcAltS = "($ _)"
cspProver_NamedProcAltArgPrios :: [Int]
cspProver_NamedProcAltArgPrios = [900]
cspProver_NamedProcAltOpPrio :: Int
cspProver_NamedProcAltOpPrio = 90
-- | SKIP primitive process symbol
cspProver_skipS :: String
cspProver_skipS = "SKIP"
-- | STOP primitive process symbol
cspProver_stopS :: String
cspProver_stopS = "STOP"
-- | DIV primitive process symbol
cspProver_divS :: String
cspProver_divS = "DIV"
-- | RUN primitive process symbol
cspProver_runS :: String
cspProver_runS = "??? RUN ??? - NOT YET DONE"
-- | CHAOS primitive process symbol
cspProver_chaosS :: String
cspProver_chaosS = "??? CHAOS ??? - NOT YET DONE"
-- | Action prefix operator symbols
cspProver_action_prefixS :: String
cspProver_action_prefixS = "Action_prefix"
cspProver_action_prefixAltS :: String
cspProver_action_prefixAltS = "(_ -> _)"
cspProver_action_prefixAltArgPrios :: [Int]
cspProver_action_prefixAltArgPrios = [150, 80]
cspProver_action_prefixAltOpPrio :: Int
cspProver_action_prefixAltOpPrio = 80
-- | External prefix choice operator symbols
cspProver_external_prefix_choiceS :: String
cspProver_external_prefix_choiceS = "External_pre_choice"
cspProver_external_prefix_choiceAltS :: String
cspProver_external_prefix_choiceAltS = "(? _:_ -> _)"
cspProver_external_prefix_choiceAltArgPrios :: [Int]
cspProver_external_prefix_choiceAltArgPrios = [900, 900, 80]
cspProver_external_prefix_choiceAltOpPrio :: Int
cspProver_external_prefix_choiceAltOpPrio = 80
-- | Internal prefix choice operator symbols
cspProver_internal_prefix_choiceS :: String
cspProver_internal_prefix_choiceS = "Internal_pre_choice"
cspProver_internal_prefix_choiceAltS :: String
cspProver_internal_prefix_choiceAltS = "(! _:_ -> _)"
cspProver_internal_prefix_choiceAltArgPrios :: [Int]
cspProver_internal_prefix_choiceAltArgPrios = [900, 900, 80]
cspProver_internal_prefix_choiceAltOpPrio :: Int
cspProver_internal_prefix_choiceAltOpPrio = 80
-- | Sequence combinator operator symbols
cspProver_sequenceS :: String
cspProver_sequenceS = "Seq_compo"
cspProver_sequenceAltS :: String
cspProver_sequenceAltS = "(_ ;; _)"
cspProver_sequenceAltArgPrios :: [Int]
cspProver_sequenceAltArgPrios = [79, 78]
cspProver_sequenceAltOpPrio :: Int
cspProver_sequenceAltOpPrio = 78
-- | External choice operator symbols
cspProver_external_choiceS :: String
cspProver_external_choiceS = "Ext_choice"
cspProver_external_choiceAltS :: String
cspProver_external_choiceAltS = "( _ [+] _)"
cspProver_external_choiceAltArgPrios :: [Int]
cspProver_external_choiceAltArgPrios = [72, 73]
cspProver_external_choiceAltOpPrio :: Int
cspProver_external_choiceAltOpPrio = 72
-- | Internal choice operator symbols
cspProver_internal_choiceS :: String
cspProver_internal_choiceS = "Int_choice"
cspProver_internal_choiceAltS :: String
cspProver_internal_choiceAltS = "(_ |~| _)"
cspProver_internal_choiceAltArgPrios :: [Int]
cspProver_internal_choiceAltArgPrios = [64, 65]
cspProver_internal_choiceAltOpPrio :: Int
cspProver_internal_choiceAltOpPrio = 64
-- | Interleaving parallel operator symbols
cspProver_interleavingS :: String
cspProver_interleavingS = "Interleave"
cspProver_interleavingAltS :: String
cspProver_interleavingAltS = "(_ ||| _)"
cspProver_interleavingAltArgPrios :: [Int]
cspProver_interleavingAltArgPrios = [76, 77]
cspProver_interleavingAltOpPrio :: Int
cspProver_interleavingAltOpPrio = 76
-- | Synchronous parallel operator symbols
cspProver_synchronousS :: String
cspProver_synchronousS = "Synchro"
cspProver_synchronousAltS :: String
cspProver_synchronousAltS = "(_ || _)"
cspProver_synchronousAltArgPrios :: [Int]
cspProver_synchronousAltArgPrios = [76, 77]
cspProver_synchronousAltOpPrio :: Int
cspProver_synchronousAltOpPrio = 76
-- | Generalised parallel operator symbols
cspProver_general_parallelS :: String
cspProver_general_parallelS = "Parallel"
cspProver_general_parallelAltS :: String
cspProver_general_parallelAltS = "(_ |[_]| _)"
cspProver_general_parallelAltArgPrios :: [Int]
cspProver_general_parallelAltArgPrios = [76, 0, 77]
cspProver_general_parallelAltOpPrio :: Int
cspProver_general_parallelAltOpPrio = 76
-- | Alphabetised parallel operator symbols
cspProver_alphabetised_parallelS :: String
cspProver_alphabetised_parallelS = "Alpha_parallel"
cspProver_alphabetised_parallelAltS :: String
cspProver_alphabetised_parallelAltS = "(_ |[_,_]| _)"
cspProver_alphabetised_parallelAltArgPrios :: [Int]
cspProver_alphabetised_parallelAltArgPrios = [76, 0, 0, 77]
cspProver_alphabetised_parallelAltOpPrio :: Int
cspProver_alphabetised_parallelAltOpPrio = 76
-- | Hiding operator symbols
cspProver_hidingS :: String
cspProver_hidingS = "Hiding"
cspProver_hidingAltS :: String
cspProver_hidingAltS = "(_ -- _)"
cspProver_hidingAltArgPrios :: [Int]
cspProver_hidingAltArgPrios = [84, 85]
cspProver_hidingAltOpPrio :: Int
cspProver_hidingAltOpPrio = 85
-- | Renaming operator symbols
cspProver_renamingS :: String
cspProver_renamingS = "Renaming"
cspProver_renamingAltS :: String
cspProver_renamingAltS = "(_ [[_]])"
cspProver_renamingAltArgPrios :: [Int]
cspProver_renamingAltArgPrios = [84, 0]
cspProver_renamingAltOpPrio :: Int
cspProver_renamingAltOpPrio = 84
-- | Conditional operator symbols
cspProver_conditionalS :: String
cspProver_conditionalS = "IF"
cspProver_conditionalAltS :: String
cspProver_conditionalAltS = "(IF _ THEN _ ELSE _)"
cspProver_conditionalAltArgPrios :: [Int]
cspProver_conditionalAltArgPrios = [900, 88, 88]
cspProver_conditionalAltArgOpPrio :: Int
cspProver_conditionalAltArgOpPrio = 88
-- | Channel non-deterministic send operator symbols
cspProver_chan_nondeterministic_sendS :: String
cspProver_chan_nondeterministic_sendS = "Nondet_send_prefix"
cspProver_chan_nondeterministic_sendAltS :: String
cspProver_chan_nondeterministic_sendAltS = "(_ !? _ : _ -> _)"
cspProver_chan_nondeterministic_sendAltArgPrios :: [Int]
cspProver_chan_nondeterministic_sendAltArgPrios = [900, 900, 1000, 80]
cspProver_chan_nondeterministic_sendAltArgOpPrio :: Int
cspProver_chan_nondeterministic_sendAltArgOpPrio = 80
-- | Channel send operator symbols
cspProver_chan_sendS :: String
cspProver_chan_sendS = "Send_prefix"
cspProver_chan_sendAltS :: String
cspProver_chan_sendAltS = "(_ ! _ -> _)"
cspProver_chan_sendAltArgPrios :: [Int]
cspProver_chan_sendAltArgPrios = [900, 1000, 80]
cspProver_chan_sendAltArgOpPrio :: Int
cspProver_chan_sendAltArgOpPrio = 80
-- | Channel receive operator symbols
cspProver_chan_recS :: String
cspProver_chan_recS = "Rec_prefix"
cspProver_chan_recAltS :: String
cspProver_chan_recAltS = "(_ ? _ : _ -> _)"
cspProver_chan_recAltArgPrios :: [Int]
cspProver_chan_recAltArgPrios = [900, 900, 1000, 80]
cspProver_chan_recAltArgOpPrio :: Int
cspProver_chan_recAltArgOpPrio = 80
-- Isabelle Terms representing the operations for CspProver
-- | Name Process operator
cspProver_NamedProcOp :: Term -> Term
cspProver_NamedProcOp =
makeUnaryCspProverOp cspProver_NamedProcS
cspProver_NamedProcAltS
cspProver_NamedProcAltArgPrios
cspProver_NamedProcAltOpPrio
-- | SKIP primitive process operator
cspProver_skipOp :: Term
cspProver_skipOp = makeCspProverOpNoAlt cspProver_skipS
-- | STOP primitive process operator
cspProver_stopOp :: Term
cspProver_stopOp = makeCspProverOpNoAlt cspProver_stopS
-- | DIV primitive process operator
cspProver_divOp :: Term
cspProver_divOp = makeCspProverOpNoAlt cspProver_divS
-- | RUN primitive process operator
cspProver_runOp :: Term
cspProver_runOp = makeCspProverOpNoAlt cspProver_runS
-- | CHAOS primitive process operator
cspProver_chaosOp :: Term
cspProver_chaosOp = makeCspProverOpNoAlt cspProver_chaosS
-- | Action prefix operator
cspProver_action_prefixOp :: Term -> Term -> Term
cspProver_action_prefixOp =
makeBinCspProverOp cspProver_action_prefixS
cspProver_action_prefixAltS
cspProver_action_prefixAltArgPrios
cspProver_action_prefixAltOpPrio
-- | External prefix choice operator
cspProver_external_prefix_choiceOp :: Term -> Term -> Term -> Term
cspProver_external_prefix_choiceOp =
makeTriCspProverOp cspProver_external_prefix_choiceS
cspProver_external_prefix_choiceAltS
cspProver_external_prefix_choiceAltArgPrios
cspProver_external_prefix_choiceAltOpPrio
-- | Internal prefix choice operator
cspProver_internal_prefix_choiceOp :: Term -> Term -> Term -> Term
cspProver_internal_prefix_choiceOp =
makeTriCspProverOp cspProver_internal_prefix_choiceS
cspProver_internal_prefix_choiceAltS
cspProver_internal_prefix_choiceAltArgPrios
cspProver_internal_prefix_choiceAltOpPrio
-- | Sequence combinator operator
cspProver_sequenceOp :: Term -> Term -> Term
cspProver_sequenceOp =
makeBinCspProverOp cspProver_sequenceS
cspProver_sequenceAltS
cspProver_sequenceAltArgPrios
cspProver_sequenceAltOpPrio
-- | External choice operator
cspProver_external_choiceOp :: Term -> Term -> Term
cspProver_external_choiceOp =
makeBinCspProverOp cspProver_external_choiceS
cspProver_external_choiceAltS
cspProver_external_choiceAltArgPrios
cspProver_external_choiceAltOpPrio
-- | Internal choice operator
cspProver_internal_choiceOp :: Term -> Term -> Term
cspProver_internal_choiceOp =
makeBinCspProverOp cspProver_internal_choiceS
cspProver_internal_choiceAltS
cspProver_internal_choiceAltArgPrios
cspProver_internal_choiceAltOpPrio
-- | Interleaving parallel operator
cspProver_interleavingOp :: Term -> Term -> Term
cspProver_interleavingOp =
makeBinCspProverOp cspProver_interleavingS
cspProver_interleavingAltS
cspProver_interleavingAltArgPrios
cspProver_interleavingAltOpPrio
-- | Synchronous parallel operator
cspProver_synchronousOp :: Term -> Term -> Term
cspProver_synchronousOp =
makeBinCspProverOp cspProver_synchronousS
cspProver_synchronousAltS
cspProver_synchronousAltArgPrios
cspProver_synchronousAltOpPrio
-- | Generalised parallel operator
cspProver_general_parallelOp :: Term -> Term -> Term -> Term
cspProver_general_parallelOp =
makeTriCspProverOp cspProver_general_parallelS
cspProver_general_parallelAltS
cspProver_general_parallelAltArgPrios
cspProver_general_parallelAltOpPrio
-- | Alphabetised parallel operator symbols
cspProver_alphabetised_parallelOp :: Term -> Term -> Term -> Term -> Term
cspProver_alphabetised_parallelOp =
makeQuadCspProverOp cspProver_alphabetised_parallelS
cspProver_alphabetised_parallelAltS
cspProver_alphabetised_parallelAltArgPrios
cspProver_alphabetised_parallelAltOpPrio
-- | Hiding operator
cspProver_hidingOp :: Term -> Term -> Term
cspProver_hidingOp =
makeBinCspProverOp cspProver_hidingS
cspProver_hidingAltS
cspProver_hidingAltArgPrios
cspProver_hidingAltOpPrio
-- | Renaming operator
cspProver_renamingOp :: Term -> Term -> Term
cspProver_renamingOp =
makeBinCspProverOp cspProver_renamingS
cspProver_renamingAltS
cspProver_renamingAltArgPrios
cspProver_renamingAltOpPrio
-- | Conditional operator
cspProver_conditionalOp :: Term -> Term -> Term -> Term
cspProver_conditionalOp =
makeTriCspProverOp cspProver_conditionalS
cspProver_conditionalAltS
cspProver_conditionalAltArgPrios
cspProver_conditionalAltArgOpPrio
-- | Channel non-deterministic send operator
cspProver_chan_nondeterministic_sendOp :: Term -> Term -> Term -> Term -> Term
cspProver_chan_nondeterministic_sendOp =
makeQuadCspProverOp cspProver_chan_nondeterministic_sendS
cspProver_chan_nondeterministic_sendAltS
cspProver_chan_nondeterministic_sendAltArgPrios
cspProver_chan_nondeterministic_sendAltArgOpPrio
-- | Channel send operator
cspProver_chan_sendOp :: Term -> Term -> Term -> Term
cspProver_chan_sendOp =
makeTriCspProverOp cspProver_chan_sendS
cspProver_chan_sendAltS
cspProver_chan_sendAltArgPrios
cspProver_chan_sendAltArgOpPrio
-- | Channel receive operator
cspProver_chan_recOp :: Term -> Term -> Term -> Term -> Term
cspProver_chan_recOp =
makeQuadCspProverOp cspProver_chan_recS
cspProver_chan_recAltS
cspProver_chan_recAltArgPrios
cspProver_chan_recAltArgOpPrio
{- | Create an Isabelle Term representing a (Unary) CspProver operator
with no alternative syntax -}
makeCspProverOpNoAlt :: String -> Term
makeCspProverOpNoAlt opName =
con (VName opName Nothing)
{- | Create an Isabelle Term representing a CspProver operator with
alternative syntax for a single parameter -}
makeUnaryCspProverOp :: String -> String -> [Int] -> Int -> Term -> Term
makeUnaryCspProverOp opName altSyntax altArgPrios altOpPrio t1 =
let vname = VName opName $ Just $ AltSyntax altSyntax altArgPrios altOpPrio
in termAppl (con vname) t1
{- | Create an Isabelle Term representing a CspProver operator with
alternative syntax for two parameters -}
makeBinCspProverOp :: String -> String -> [Int] -> Int -> Term -> Term -> Term
makeBinCspProverOp opName altSyntax altArgPrios altOpPrio t1 t2 =
let vname = VName opName $ Just $ AltSyntax altSyntax altArgPrios altOpPrio
in binVNameAppl vname t1 t2
{- | Create an Isabelle Term representing a CspProver operator (with 3
parameters) with alternative syntax -}
makeTriCspProverOp :: String -> String -> [Int] -> Int -> Term -> Term ->
Term -> Term
makeTriCspProverOp opName altSyntax altArgPrios altOpPrio t1 t2 t3 =
let vname = VName opName $ Just $ AltSyntax altSyntax altArgPrios altOpPrio
in termAppl (binVNameAppl vname t1 t2) t3
{- | Create an Isabelle Term representing a CspProver operator (with 4
parameters) with alternative syntax -}
makeQuadCspProverOp :: String -> String -> [Int] -> Int -> Term -> Term ->
Term -> Term -> Term
makeQuadCspProverOp opName altSyntax altArgPrios altOpPrio t1 t2 t3 t4 =
let vname = VName opName $ Just $ AltSyntax altSyntax altArgPrios altOpPrio
in termAppl (termAppl (binVNameAppl vname t1 t2) t3) t4