{- |
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
cspProverEqV = String -> Maybe AltSyntax -> VName
VName "op =F" (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ String -> [Int] -> Int -> AltSyntax
AltSyntax "(_ =F/ _)" [50, 51] 50

cspProverbinEqF :: Term -> Term -> Term
cspProverbinEqF :: Term -> Term -> Term
cspProverbinEqF = VName -> Term -> Term -> Term
binVNameAppl VName
cspProverEqV

-- | Name Process symbol
cspProver_NamedProcS :: String
cspProver_NamedProcS :: String
cspProver_NamedProcS = "Proc_name"
cspProver_NamedProcAltS :: String
cspProver_NamedProcAltS :: String
cspProver_NamedProcAltS = "($ _)"
cspProver_NamedProcAltArgPrios :: [Int]
cspProver_NamedProcAltArgPrios :: [Int]
cspProver_NamedProcAltArgPrios = [900]
cspProver_NamedProcAltOpPrio :: Int
cspProver_NamedProcAltOpPrio :: Int
cspProver_NamedProcAltOpPrio = 90

-- | SKIP primitive process symbol
cspProver_skipS :: String
cspProver_skipS :: String
cspProver_skipS = "SKIP"

-- | STOP primitive process symbol
cspProver_stopS :: String
cspProver_stopS :: String
cspProver_stopS = "STOP"

-- | DIV primitive process symbol
cspProver_divS :: String
cspProver_divS :: String
cspProver_divS = "DIV"

-- | RUN primitive process symbol
cspProver_runS :: String
cspProver_runS :: String
cspProver_runS = "??? RUN ??? - NOT YET DONE"

-- | CHAOS primitive process symbol
cspProver_chaosS :: String
cspProver_chaosS :: String
cspProver_chaosS = "??? CHAOS ??? - NOT YET DONE"

-- | Action prefix operator symbols
cspProver_action_prefixS :: String
cspProver_action_prefixS :: String
cspProver_action_prefixS = "Action_prefix"
cspProver_action_prefixAltS :: String
cspProver_action_prefixAltS :: String
cspProver_action_prefixAltS = "(_ -> _)"
cspProver_action_prefixAltArgPrios :: [Int]
cspProver_action_prefixAltArgPrios :: [Int]
cspProver_action_prefixAltArgPrios = [150, 80]
cspProver_action_prefixAltOpPrio :: Int
cspProver_action_prefixAltOpPrio :: Int
cspProver_action_prefixAltOpPrio = 80

-- | External prefix choice operator symbols
cspProver_external_prefix_choiceS :: String
cspProver_external_prefix_choiceS :: String
cspProver_external_prefix_choiceS = "External_pre_choice"
cspProver_external_prefix_choiceAltS :: String
cspProver_external_prefix_choiceAltS :: String
cspProver_external_prefix_choiceAltS = "(? _:_ -> _)"
cspProver_external_prefix_choiceAltArgPrios :: [Int]
cspProver_external_prefix_choiceAltArgPrios :: [Int]
cspProver_external_prefix_choiceAltArgPrios = [900, 900, 80]
cspProver_external_prefix_choiceAltOpPrio :: Int
cspProver_external_prefix_choiceAltOpPrio :: Int
cspProver_external_prefix_choiceAltOpPrio = 80

-- | Internal prefix choice operator symbols
cspProver_internal_prefix_choiceS :: String
cspProver_internal_prefix_choiceS :: String
cspProver_internal_prefix_choiceS = "Internal_pre_choice"
cspProver_internal_prefix_choiceAltS :: String
cspProver_internal_prefix_choiceAltS :: String
cspProver_internal_prefix_choiceAltS = "(! _:_ -> _)"
cspProver_internal_prefix_choiceAltArgPrios :: [Int]
cspProver_internal_prefix_choiceAltArgPrios :: [Int]
cspProver_internal_prefix_choiceAltArgPrios = [900, 900, 80]
cspProver_internal_prefix_choiceAltOpPrio :: Int
cspProver_internal_prefix_choiceAltOpPrio :: Int
cspProver_internal_prefix_choiceAltOpPrio = 80

-- | Sequence combinator operator symbols
cspProver_sequenceS :: String
cspProver_sequenceS :: String
cspProver_sequenceS = "Seq_compo"
cspProver_sequenceAltS :: String
cspProver_sequenceAltS :: String
cspProver_sequenceAltS = "(_ ;; _)"
cspProver_sequenceAltArgPrios :: [Int]
cspProver_sequenceAltArgPrios :: [Int]
cspProver_sequenceAltArgPrios = [79, 78]
cspProver_sequenceAltOpPrio :: Int
cspProver_sequenceAltOpPrio :: Int
cspProver_sequenceAltOpPrio = 78

-- | External choice operator symbols
cspProver_external_choiceS :: String
cspProver_external_choiceS :: String
cspProver_external_choiceS = "Ext_choice"
cspProver_external_choiceAltS :: String
cspProver_external_choiceAltS :: String
cspProver_external_choiceAltS = "( _ [+] _)"
cspProver_external_choiceAltArgPrios :: [Int]
cspProver_external_choiceAltArgPrios :: [Int]
cspProver_external_choiceAltArgPrios = [72, 73]
cspProver_external_choiceAltOpPrio :: Int
cspProver_external_choiceAltOpPrio :: Int
cspProver_external_choiceAltOpPrio = 72

-- | Internal choice operator symbols
cspProver_internal_choiceS :: String
cspProver_internal_choiceS :: String
cspProver_internal_choiceS = "Int_choice"
cspProver_internal_choiceAltS :: String
cspProver_internal_choiceAltS :: String
cspProver_internal_choiceAltS = "(_ |~| _)"
cspProver_internal_choiceAltArgPrios :: [Int]
cspProver_internal_choiceAltArgPrios :: [Int]
cspProver_internal_choiceAltArgPrios = [64, 65]
cspProver_internal_choiceAltOpPrio :: Int
cspProver_internal_choiceAltOpPrio :: Int
cspProver_internal_choiceAltOpPrio = 64

-- | Interleaving parallel operator symbols
cspProver_interleavingS :: String
cspProver_interleavingS :: String
cspProver_interleavingS = "Interleave"
cspProver_interleavingAltS :: String
cspProver_interleavingAltS :: String
cspProver_interleavingAltS = "(_ ||| _)"
cspProver_interleavingAltArgPrios :: [Int]
cspProver_interleavingAltArgPrios :: [Int]
cspProver_interleavingAltArgPrios = [76, 77]
cspProver_interleavingAltOpPrio :: Int
cspProver_interleavingAltOpPrio :: Int
cspProver_interleavingAltOpPrio = 76

-- | Synchronous parallel operator symbols
cspProver_synchronousS :: String
cspProver_synchronousS :: String
cspProver_synchronousS = "Synchro"
cspProver_synchronousAltS :: String
cspProver_synchronousAltS :: String
cspProver_synchronousAltS = "(_ || _)"
cspProver_synchronousAltArgPrios :: [Int]
cspProver_synchronousAltArgPrios :: [Int]
cspProver_synchronousAltArgPrios = [76, 77]
cspProver_synchronousAltOpPrio :: Int
cspProver_synchronousAltOpPrio :: Int
cspProver_synchronousAltOpPrio = 76

-- | Generalised parallel operator symbols
cspProver_general_parallelS :: String
cspProver_general_parallelS :: String
cspProver_general_parallelS = "Parallel"
cspProver_general_parallelAltS :: String
cspProver_general_parallelAltS :: String
cspProver_general_parallelAltS = "(_ |[_]| _)"
cspProver_general_parallelAltArgPrios :: [Int]
cspProver_general_parallelAltArgPrios :: [Int]
cspProver_general_parallelAltArgPrios = [76, 0, 77]
cspProver_general_parallelAltOpPrio :: Int
cspProver_general_parallelAltOpPrio :: Int
cspProver_general_parallelAltOpPrio = 76

-- | Alphabetised parallel operator symbols
cspProver_alphabetised_parallelS :: String
cspProver_alphabetised_parallelS :: String
cspProver_alphabetised_parallelS = "Alpha_parallel"
cspProver_alphabetised_parallelAltS :: String
cspProver_alphabetised_parallelAltS :: String
cspProver_alphabetised_parallelAltS = "(_ |[_,_]| _)"
cspProver_alphabetised_parallelAltArgPrios :: [Int]
cspProver_alphabetised_parallelAltArgPrios :: [Int]
cspProver_alphabetised_parallelAltArgPrios = [76, 0, 0, 77]
cspProver_alphabetised_parallelAltOpPrio :: Int
cspProver_alphabetised_parallelAltOpPrio :: Int
cspProver_alphabetised_parallelAltOpPrio = 76

-- | Hiding operator symbols
cspProver_hidingS :: String
cspProver_hidingS :: String
cspProver_hidingS = "Hiding"
cspProver_hidingAltS :: String
cspProver_hidingAltS :: String
cspProver_hidingAltS = "(_ -- _)"
cspProver_hidingAltArgPrios :: [Int]
cspProver_hidingAltArgPrios :: [Int]
cspProver_hidingAltArgPrios = [84, 85]
cspProver_hidingAltOpPrio :: Int
cspProver_hidingAltOpPrio :: Int
cspProver_hidingAltOpPrio = 85

-- | Renaming operator symbols
cspProver_renamingS :: String
cspProver_renamingS :: String
cspProver_renamingS = "Renaming"
cspProver_renamingAltS :: String
cspProver_renamingAltS :: String
cspProver_renamingAltS = "(_ [[_]])"
cspProver_renamingAltArgPrios :: [Int]
cspProver_renamingAltArgPrios :: [Int]
cspProver_renamingAltArgPrios = [84, 0]
cspProver_renamingAltOpPrio :: Int
cspProver_renamingAltOpPrio :: Int
cspProver_renamingAltOpPrio = 84

-- | Conditional operator symbols
cspProver_conditionalS :: String
cspProver_conditionalS :: String
cspProver_conditionalS = "IF"
cspProver_conditionalAltS :: String
cspProver_conditionalAltS :: String
cspProver_conditionalAltS = "(IF _ THEN _ ELSE _)"
cspProver_conditionalAltArgPrios :: [Int]
cspProver_conditionalAltArgPrios :: [Int]
cspProver_conditionalAltArgPrios = [900, 88, 88]
cspProver_conditionalAltArgOpPrio :: Int
cspProver_conditionalAltArgOpPrio :: Int
cspProver_conditionalAltArgOpPrio = 88

-- | Channel non-deterministic send operator symbols
cspProver_chan_nondeterministic_sendS :: String
cspProver_chan_nondeterministic_sendS :: String
cspProver_chan_nondeterministic_sendS = "Nondet_send_prefix"
cspProver_chan_nondeterministic_sendAltS :: String
cspProver_chan_nondeterministic_sendAltS :: String
cspProver_chan_nondeterministic_sendAltS = "(_ !? _ : _ -> _)"
cspProver_chan_nondeterministic_sendAltArgPrios :: [Int]
cspProver_chan_nondeterministic_sendAltArgPrios :: [Int]
cspProver_chan_nondeterministic_sendAltArgPrios = [900, 900, 1000, 80]
cspProver_chan_nondeterministic_sendAltArgOpPrio :: Int
cspProver_chan_nondeterministic_sendAltArgOpPrio :: Int
cspProver_chan_nondeterministic_sendAltArgOpPrio = 80

-- | Channel send operator symbols
cspProver_chan_sendS :: String
cspProver_chan_sendS :: String
cspProver_chan_sendS = "Send_prefix"
cspProver_chan_sendAltS :: String
cspProver_chan_sendAltS :: String
cspProver_chan_sendAltS = "(_ ! _ -> _)"
cspProver_chan_sendAltArgPrios :: [Int]
cspProver_chan_sendAltArgPrios :: [Int]
cspProver_chan_sendAltArgPrios = [900, 1000, 80]
cspProver_chan_sendAltArgOpPrio :: Int
cspProver_chan_sendAltArgOpPrio :: Int
cspProver_chan_sendAltArgOpPrio = 80

-- | Channel receive operator symbols
cspProver_chan_recS :: String
cspProver_chan_recS :: String
cspProver_chan_recS = "Rec_prefix"
cspProver_chan_recAltS :: String
cspProver_chan_recAltS :: String
cspProver_chan_recAltS = "(_ ? _ : _ -> _)"
cspProver_chan_recAltArgPrios :: [Int]
cspProver_chan_recAltArgPrios :: [Int]
cspProver_chan_recAltArgPrios = [900, 900, 1000, 80]
cspProver_chan_recAltArgOpPrio :: Int
cspProver_chan_recAltArgOpPrio :: Int
cspProver_chan_recAltArgOpPrio = 80

-- Isabelle Terms representing the operations for CspProver

-- | Name Process operator
cspProver_NamedProcOp :: Term -> Term
cspProver_NamedProcOp :: Term -> Term
cspProver_NamedProcOp =
    String -> String -> [Int] -> Int -> Term -> Term
makeUnaryCspProverOp String
cspProver_NamedProcS
                         String
cspProver_NamedProcAltS
                         [Int]
cspProver_NamedProcAltArgPrios
                         Int
cspProver_NamedProcAltOpPrio

-- | SKIP primitive process operator
cspProver_skipOp :: Term
cspProver_skipOp :: Term
cspProver_skipOp = String -> Term
makeCspProverOpNoAlt String
cspProver_skipS

-- | STOP primitive process operator
cspProver_stopOp :: Term
cspProver_stopOp :: Term
cspProver_stopOp = String -> Term
makeCspProverOpNoAlt String
cspProver_stopS

-- | DIV primitive process operator
cspProver_divOp :: Term
cspProver_divOp :: Term
cspProver_divOp = String -> Term
makeCspProverOpNoAlt String
cspProver_divS

-- | RUN primitive process operator
cspProver_runOp :: Term
cspProver_runOp :: Term
cspProver_runOp = String -> Term
makeCspProverOpNoAlt String
cspProver_runS

-- | CHAOS primitive process operator
cspProver_chaosOp :: Term
cspProver_chaosOp :: Term
cspProver_chaosOp = String -> Term
makeCspProverOpNoAlt String
cspProver_chaosS

-- | Action prefix operator
cspProver_action_prefixOp :: Term -> Term -> Term
cspProver_action_prefixOp :: Term -> Term -> Term
cspProver_action_prefixOp =
    String -> String -> [Int] -> Int -> Term -> Term -> Term
makeBinCspProverOp String
cspProver_action_prefixS
                       String
cspProver_action_prefixAltS
                       [Int]
cspProver_action_prefixAltArgPrios
                       Int
cspProver_action_prefixAltOpPrio

-- | External prefix choice operator
cspProver_external_prefix_choiceOp :: Term -> Term -> Term -> Term
cspProver_external_prefix_choiceOp :: Term -> Term -> Term -> Term
cspProver_external_prefix_choiceOp =
    String -> String -> [Int] -> Int -> Term -> Term -> Term -> Term
makeTriCspProverOp String
cspProver_external_prefix_choiceS
                       String
cspProver_external_prefix_choiceAltS
                       [Int]
cspProver_external_prefix_choiceAltArgPrios
                       Int
cspProver_external_prefix_choiceAltOpPrio

-- | Internal prefix choice operator
cspProver_internal_prefix_choiceOp :: Term -> Term -> Term -> Term
cspProver_internal_prefix_choiceOp :: Term -> Term -> Term -> Term
cspProver_internal_prefix_choiceOp =
    String -> String -> [Int] -> Int -> Term -> Term -> Term -> Term
makeTriCspProverOp String
cspProver_internal_prefix_choiceS
                       String
cspProver_internal_prefix_choiceAltS
                       [Int]
cspProver_internal_prefix_choiceAltArgPrios
                       Int
cspProver_internal_prefix_choiceAltOpPrio

-- | Sequence combinator operator
cspProver_sequenceOp :: Term -> Term -> Term
cspProver_sequenceOp :: Term -> Term -> Term
cspProver_sequenceOp =
    String -> String -> [Int] -> Int -> Term -> Term -> Term
makeBinCspProverOp String
cspProver_sequenceS
                       String
cspProver_sequenceAltS
                       [Int]
cspProver_sequenceAltArgPrios
                       Int
cspProver_sequenceAltOpPrio

-- | External choice operator
cspProver_external_choiceOp :: Term -> Term -> Term
cspProver_external_choiceOp :: Term -> Term -> Term
cspProver_external_choiceOp =
    String -> String -> [Int] -> Int -> Term -> Term -> Term
makeBinCspProverOp String
cspProver_external_choiceS
                       String
cspProver_external_choiceAltS
                       [Int]
cspProver_external_choiceAltArgPrios
                       Int
cspProver_external_choiceAltOpPrio

-- | Internal choice operator
cspProver_internal_choiceOp :: Term -> Term -> Term
cspProver_internal_choiceOp :: Term -> Term -> Term
cspProver_internal_choiceOp =
    String -> String -> [Int] -> Int -> Term -> Term -> Term
makeBinCspProverOp String
cspProver_internal_choiceS
                       String
cspProver_internal_choiceAltS
                       [Int]
cspProver_internal_choiceAltArgPrios
                       Int
cspProver_internal_choiceAltOpPrio

-- | Interleaving parallel operator
cspProver_interleavingOp :: Term -> Term -> Term
cspProver_interleavingOp :: Term -> Term -> Term
cspProver_interleavingOp =
    String -> String -> [Int] -> Int -> Term -> Term -> Term
makeBinCspProverOp String
cspProver_interleavingS
                       String
cspProver_interleavingAltS
                       [Int]
cspProver_interleavingAltArgPrios
                       Int
cspProver_interleavingAltOpPrio

-- | Synchronous parallel operator
cspProver_synchronousOp :: Term -> Term -> Term
cspProver_synchronousOp :: Term -> Term -> Term
cspProver_synchronousOp =
    String -> String -> [Int] -> Int -> Term -> Term -> Term
makeBinCspProverOp String
cspProver_synchronousS
                       String
cspProver_synchronousAltS
                       [Int]
cspProver_synchronousAltArgPrios
                       Int
cspProver_synchronousAltOpPrio

-- | Generalised parallel operator
cspProver_general_parallelOp :: Term -> Term -> Term -> Term
cspProver_general_parallelOp :: Term -> Term -> Term -> Term
cspProver_general_parallelOp =
    String -> String -> [Int] -> Int -> Term -> Term -> Term -> Term
makeTriCspProverOp String
cspProver_general_parallelS
                       String
cspProver_general_parallelAltS
                       [Int]
cspProver_general_parallelAltArgPrios
                       Int
cspProver_general_parallelAltOpPrio

-- | Alphabetised parallel operator symbols
cspProver_alphabetised_parallelOp :: Term -> Term -> Term -> Term -> Term
cspProver_alphabetised_parallelOp :: Term -> Term -> Term -> Term -> Term
cspProver_alphabetised_parallelOp =
    String
-> String -> [Int] -> Int -> Term -> Term -> Term -> Term -> Term
makeQuadCspProverOp String
cspProver_alphabetised_parallelS
                    String
cspProver_alphabetised_parallelAltS
                    [Int]
cspProver_alphabetised_parallelAltArgPrios
                    Int
cspProver_alphabetised_parallelAltOpPrio

-- | Hiding operator
cspProver_hidingOp :: Term -> Term -> Term
cspProver_hidingOp :: Term -> Term -> Term
cspProver_hidingOp =
    String -> String -> [Int] -> Int -> Term -> Term -> Term
makeBinCspProverOp String
cspProver_hidingS
                       String
cspProver_hidingAltS
                       [Int]
cspProver_hidingAltArgPrios
                       Int
cspProver_hidingAltOpPrio

-- | Renaming operator
cspProver_renamingOp :: Term -> Term -> Term
cspProver_renamingOp :: Term -> Term -> Term
cspProver_renamingOp =
    String -> String -> [Int] -> Int -> Term -> Term -> Term
makeBinCspProverOp String
cspProver_renamingS
                       String
cspProver_renamingAltS
                       [Int]
cspProver_renamingAltArgPrios
                       Int
cspProver_renamingAltOpPrio

-- | Conditional operator
cspProver_conditionalOp :: Term -> Term -> Term -> Term
cspProver_conditionalOp :: Term -> Term -> Term -> Term
cspProver_conditionalOp =
    String -> String -> [Int] -> Int -> Term -> Term -> Term -> Term
makeTriCspProverOp String
cspProver_conditionalS
                       String
cspProver_conditionalAltS
                       [Int]
cspProver_conditionalAltArgPrios
                       Int
cspProver_conditionalAltArgOpPrio

-- | Channel non-deterministic send operator
cspProver_chan_nondeterministic_sendOp :: Term -> Term -> Term -> Term -> Term
cspProver_chan_nondeterministic_sendOp :: Term -> Term -> Term -> Term -> Term
cspProver_chan_nondeterministic_sendOp =
    String
-> String -> [Int] -> Int -> Term -> Term -> Term -> Term -> Term
makeQuadCspProverOp String
cspProver_chan_nondeterministic_sendS
                        String
cspProver_chan_nondeterministic_sendAltS
                        [Int]
cspProver_chan_nondeterministic_sendAltArgPrios
                        Int
cspProver_chan_nondeterministic_sendAltArgOpPrio

-- | Channel send operator
cspProver_chan_sendOp :: Term -> Term -> Term -> Term
cspProver_chan_sendOp :: Term -> Term -> Term -> Term
cspProver_chan_sendOp =
    String -> String -> [Int] -> Int -> Term -> Term -> Term -> Term
makeTriCspProverOp String
cspProver_chan_sendS
                       String
cspProver_chan_sendAltS
                       [Int]
cspProver_chan_sendAltArgPrios
                       Int
cspProver_chan_sendAltArgOpPrio

-- | Channel receive operator
cspProver_chan_recOp :: Term -> Term -> Term -> Term -> Term
cspProver_chan_recOp :: Term -> Term -> Term -> Term -> Term
cspProver_chan_recOp =
    String
-> String -> [Int] -> Int -> Term -> Term -> Term -> Term -> Term
makeQuadCspProverOp String
cspProver_chan_recS
                        String
cspProver_chan_recAltS
                        [Int]
cspProver_chan_recAltArgPrios
                        Int
cspProver_chan_recAltArgOpPrio

{- | Create an Isabelle Term representing a (Unary) CspProver operator
with no alternative syntax -}
makeCspProverOpNoAlt :: String -> Term
makeCspProverOpNoAlt :: String -> Term
makeCspProverOpNoAlt opName :: String
opName =
    VName -> Term
con (String -> Maybe AltSyntax -> VName
VName String
opName Maybe AltSyntax
forall a. Maybe a
Nothing)

{- | Create an Isabelle Term representing a CspProver operator with
alternative syntax for a single parameter -}
makeUnaryCspProverOp :: String -> String -> [Int] -> Int -> Term -> Term
makeUnaryCspProverOp :: String -> String -> [Int] -> Int -> Term -> Term
makeUnaryCspProverOp opName :: String
opName altSyntax :: String
altSyntax altArgPrios :: [Int]
altArgPrios altOpPrio :: Int
altOpPrio t1 :: Term
t1 =
    let vname :: VName
vname = String -> Maybe AltSyntax -> VName
VName String
opName (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ String -> [Int] -> Int -> AltSyntax
AltSyntax String
altSyntax [Int]
altArgPrios Int
altOpPrio
    in Term -> Term -> Term
termAppl (VName -> Term
con VName
vname) Term
t1

{- | Create an Isabelle Term representing a CspProver operator with
alternative syntax for two parameters -}
makeBinCspProverOp :: String -> String -> [Int] -> Int -> Term -> Term -> Term
makeBinCspProverOp :: String -> String -> [Int] -> Int -> Term -> Term -> Term
makeBinCspProverOp opName :: String
opName altSyntax :: String
altSyntax altArgPrios :: [Int]
altArgPrios altOpPrio :: Int
altOpPrio t1 :: Term
t1 t2 :: Term
t2 =
    let vname :: VName
vname = String -> Maybe AltSyntax -> VName
VName String
opName (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ String -> [Int] -> Int -> AltSyntax
AltSyntax String
altSyntax [Int]
altArgPrios Int
altOpPrio
    in VName -> Term -> Term -> Term
binVNameAppl VName
vname Term
t1 Term
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 :: String -> String -> [Int] -> Int -> Term -> Term -> Term -> Term
makeTriCspProverOp opName :: String
opName altSyntax :: String
altSyntax altArgPrios :: [Int]
altArgPrios altOpPrio :: Int
altOpPrio t1 :: Term
t1 t2 :: Term
t2 t3 :: Term
t3 =
    let vname :: VName
vname = String -> Maybe AltSyntax -> VName
VName String
opName (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ String -> [Int] -> Int -> AltSyntax
AltSyntax String
altSyntax [Int]
altArgPrios Int
altOpPrio
    in Term -> Term -> Term
termAppl (VName -> Term -> Term -> Term
binVNameAppl VName
vname Term
t1 Term
t2) Term
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 :: String
-> String -> [Int] -> Int -> Term -> Term -> Term -> Term -> Term
makeQuadCspProverOp opName :: String
opName altSyntax :: String
altSyntax altArgPrios :: [Int]
altArgPrios altOpPrio :: Int
altOpPrio t1 :: Term
t1 t2 :: Term
t2 t3 :: Term
t3 t4 :: Term
t4 =
    let vname :: VName
vname = String -> Maybe AltSyntax -> VName
VName String
opName (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ String -> [Int] -> Int -> AltSyntax
AltSyntax String
altSyntax [Int]
altArgPrios Int
altOpPrio
    in Term -> Term -> Term
termAppl (Term -> Term -> Term
termAppl (VName -> Term -> Term -> Term
binVNameAppl VName
vname Term
t1 Term
t2) Term
t3) Term
t4