content: {- |
  Module      :
  Description :  Isabelle Abstract syntax constants for CSP-Prover operations
  Copyright   :  (c) Andy Gimblett, 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 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
  