{- |

Module : $Header$

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