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)
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
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
cspProver_skipS :: String
cspProver_skipS :: String
cspProver_skipS = "SKIP"
cspProver_stopS :: String
cspProver_stopS :: String
cspProver_stopS = "STOP"
cspProver_divS :: String
cspProver_divS :: String
cspProver_divS = "DIV"
cspProver_runS :: String
cspProver_runS :: String
cspProver_runS = "??? RUN ??? - NOT YET DONE"
cspProver_chaosS :: String
cspProver_chaosS :: String
cspProver_chaosS = "??? CHAOS ??? - NOT YET DONE"
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
cspProver_skipOp :: Term
cspProver_skipOp :: Term
cspProver_skipOp = String -> Term
makeCspProverOpNoAlt String
cspProver_skipS
cspProver_stopOp :: Term
cspProver_stopOp :: Term
cspProver_stopOp = String -> Term
makeCspProverOpNoAlt String
cspProver_stopS
cspProver_divOp :: Term
cspProver_divOp :: Term
cspProver_divOp = String -> Term
makeCspProverOpNoAlt String
cspProver_divS
cspProver_runOp :: Term
cspProver_runOp :: Term
cspProver_runOp = String -> Term
makeCspProverOpNoAlt String
cspProver_runS
cspProver_chaosOp :: Term
cspProver_chaosOp :: Term
cspProver_chaosOp = String -> Term
makeCspProverOpNoAlt String
cspProver_chaosS
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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)
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
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
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
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