{- |

Module :

Description : Isabelle Abstract syntax constants for CSP-Prover operations

Copyright : (c) Andy Gimblett, Liam O'Reilly and Markus Roggenbach,

Swansea University 2008

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : csliam@swansea.ac.uk

Stability : provisional

Portability : portable

Isabelle Abstract syntax constants for CSP-Prover operations.

-}

module CspCASL.CspProver_Consts (

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,

) 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

-- 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 = "Act_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 = "Ext_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 = "Int_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

-- Only works if pretty printed using the alternative syntax

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

-- Isabelle Terms representing the operations for CspProver

-- | 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

-- | Conditional operator

cspProver_chan_nondeterministic_sendOp :: 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

-- 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

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