bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{- |

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederModule :

81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : Isabelle Abstract syntax constants for CSP-Prover operations

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaederCopyright : (c) Andy Gimblett, Liam O'Reilly and Markus Roggenbach,

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder Swansea University 2008

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederMaintainer : csliam@swansea.ac.uk

fbb66ee3e170624835b99f7aa91980753cb5b472Christian MaederStability : provisional

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : portable

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederIsabelle Abstract syntax constants for CSP-Prover operations.

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder-}

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maedermodule CspCASL.CspProver_Consts (

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder cspProver_skipOp,

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder cspProver_stopOp,

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder cspProver_divOp,

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder cspProver_runOp,

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder cspProver_chaosOp,

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder cspProver_action_prefixOp,

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder cspProver_external_prefix_choiceOp,

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder cspProver_internal_prefix_choiceOp,

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder cspProver_sequenceOp,

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder cspProver_external_choiceOp,

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder cspProver_internal_choiceOp,

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder cspProver_interleavingOp,

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder cspProver_synchronousOp,

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder cspProver_general_parallelOp,

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder cspProver_alphabetised_parallelOp,

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder cspProver_hidingOp,

33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maeder cspProver_renamingOp,

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder cspProver_conditionalOp,

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder cspProver_chan_nondeterministic_sendOp

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder) where

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maederimport Isabelle.IsaSign as IsaSign

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport Isabelle.IsaConsts (binVNameAppl, con, termAppl)

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder{- Symbols for CspProver

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian MaederThese symbols and priorities have come from the CSP-Prover source code -}

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski-- SKIP primitive process symbol

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_skipS :: String

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian MaedercspProver_skipS = "SKIP"

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- STOP primitive process symbol

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskicspProver_stopS :: String

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedercspProver_stopS = "STOP"

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder-- DIV primitive process symbol

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_divS :: String

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedercspProver_divS = "DIV"

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- RUN primitive process symbol

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedercspProver_runS :: String

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_runS = "??? RUN ??? - NOT YET DONE"

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- CHAOS primitive process symbol

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedercspProver_chaosS :: String

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_chaosS = "??? CHAOS ??? - NOT YET DONE"

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder-- Action prefix operator symbols

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaedercspProver_action_prefixS :: String

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedercspProver_action_prefixS = "Act_prefix"

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_action_prefixAltS :: String

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_action_prefixAltS = "(_ -> _)"

c44c23429c72f3a709e22a18f2ed6f05fc8cc765Christian MaedercspProver_action_prefixAltArgPrios :: [Int]

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaedercspProver_action_prefixAltArgPrios = [150, 80]

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedercspProver_action_prefixAltOpPrio :: Int

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedercspProver_action_prefixAltOpPrio = 80

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder-- External prefix choice operator symbols

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_external_prefix_choiceS :: String

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_external_prefix_choiceS = "Ext_pre_choice"

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_external_prefix_choiceAltS :: String

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedercspProver_external_prefix_choiceAltS = "(? _:_ -> _)"

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedercspProver_external_prefix_choiceAltArgPrios :: [Int]

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedercspProver_external_prefix_choiceAltArgPrios = [900, 900, 80]

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_external_prefix_choiceAltOpPrio :: Int

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedercspProver_external_prefix_choiceAltOpPrio = 80

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder-- Internal prefix choice operator symbols

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian MaedercspProver_internal_prefix_choiceS :: String

3c62e6ef442caf092adcbecf6fccd957dcd72689Christian MaedercspProver_internal_prefix_choiceS = "Int_pre_choice"

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_internal_prefix_choiceAltS :: String

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_internal_prefix_choiceAltS = "(! _:_ -> _)"

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_internal_prefix_choiceAltArgPrios :: [Int]

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_internal_prefix_choiceAltArgPrios = [900, 900, 80]

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedercspProver_internal_prefix_choiceAltOpPrio :: Int

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedercspProver_internal_prefix_choiceAltOpPrio = 80

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- Sequence combinator operator symbols

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian MaedercspProver_sequenceS :: String

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaedercspProver_sequenceS = "Seq_compo"

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian MaedercspProver_sequenceAltS :: String

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_sequenceAltS = "(_ ;; _)"

f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian MaedercspProver_sequenceAltArgPrios :: [Int]

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedercspProver_sequenceAltArgPrios = [79, 78]

0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian MaedercspProver_sequenceAltOpPrio :: Int

89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaedercspProver_sequenceAltOpPrio = 78

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- External choice operator symbols

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_external_choiceS :: String

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedercspProver_external_choiceS = "Ext_choice"

836e72a3c413366ba9801726f3b249c7791cb9caChristian MaedercspProver_external_choiceAltS :: String

836e72a3c413366ba9801726f3b249c7791cb9caChristian MaedercspProver_external_choiceAltS = "( _ [+] _)"

89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaedercspProver_external_choiceAltArgPrios :: [Int]

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_external_choiceAltArgPrios = [72, 73]

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_external_choiceAltOpPrio :: Int

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedercspProver_external_choiceAltOpPrio = 72

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder

2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder-- Internal choice operator symbols

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedercspProver_internal_choiceS :: String

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedercspProver_internal_choiceS = "Int_choice"

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_internal_choiceAltS :: String

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedercspProver_internal_choiceAltS = "(_ |~| _)"

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedercspProver_internal_choiceAltArgPrios :: [Int]

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaedercspProver_internal_choiceAltArgPrios = [64, 65]

89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaedercspProver_internal_choiceAltOpPrio :: Int

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_internal_choiceAltOpPrio = 64

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- Interleaving parallel operator symbols

d48085f765fca838c1d972d2123601997174583dChristian MaedercspProver_interleavingS :: String

797f811e57952d59e73b8cd03b667eef276db972Christian MaedercspProver_interleavingS = "Interleave"

89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaedercspProver_interleavingAltS :: String

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedercspProver_interleavingAltS = "(_ ||| _)"

3daa82a175c7cfabf22455aa77c4beda327404e4Christian MaedercspProver_interleavingAltArgPrios :: [Int]

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedercspProver_interleavingAltArgPrios = [76, 77]

3daa82a175c7cfabf22455aa77c4beda327404e4Christian MaedercspProver_interleavingAltOpPrio :: Int

3daa82a175c7cfabf22455aa77c4beda327404e4Christian MaedercspProver_interleavingAltOpPrio = 76

3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder

3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder-- Synchronous parallel operator symbols

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedercspProver_synchronousS :: String

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedercspProver_synchronousS = "Synchro"

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedercspProver_synchronousAltS :: String

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaedercspProver_synchronousAltS = "(_ || _)"

89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaedercspProver_synchronousAltArgPrios :: [Int]

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian MaedercspProver_synchronousAltArgPrios = [76, 77]

149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian MaedercspProver_synchronousAltOpPrio :: Int

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_synchronousAltOpPrio = 76

1738d16957389457347bee85075d3d33d002158fChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- Generalised parallel operator symbols

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian MaedercspProver_general_parallelS :: String

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_general_parallelS = "Parallel"

89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaedercspProver_general_parallelAltS :: String

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_general_parallelAltS = "(_ |[_]| _)"

304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian MaedercspProver_general_parallelAltArgPrios :: [Int]

304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian MaedercspProver_general_parallelAltArgPrios = [76, 0, 77]

304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian MaedercspProver_general_parallelAltOpPrio :: Int

304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian MaedercspProver_general_parallelAltOpPrio = 76

304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder-- Alphabetised parallel operator symbols

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedercspProver_alphabetised_parallelS :: String

e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian MaedercspProver_alphabetised_parallelS = "Alpha_parallel"

e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian MaedercspProver_alphabetised_parallelAltS :: String

e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian MaedercspProver_alphabetised_parallelAltS = "(_ |[_,_]| _)"

e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian MaedercspProver_alphabetised_parallelAltArgPrios :: [Int]

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaedercspProver_alphabetised_parallelAltArgPrios = [76, 0, 0, 77]

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedercspProver_alphabetised_parallelAltOpPrio :: Int

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_alphabetised_parallelAltOpPrio = 76

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder-- Hiding operator symbols

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedercspProver_hidingS :: String

2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercspProver_hidingS = "Hiding"

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaedercspProver_hidingAltS :: String

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaedercspProver_hidingAltS = "(_ -- _)"

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaedercspProver_hidingAltArgPrios :: [Int]

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedercspProver_hidingAltArgPrios = [84, 85]

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