-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/

-- | Ogma: Runtime Monitor translator: SMV Language Frontend
--   
--   Ogma is a tool to facilitate the integration of safe runtime monitors
--   into other systems. Ogma extends Copilot, a high-level runtime
--   verification framework that generates hard real-time C99 code.
--   
--   This library contains a frontend to read SMV Boolean expressions.
@package ogma-language-smv
@version 1.10.0

-- | The abstract syntax of language SMV.
module Language.SMV.AbsSMV
data BoolSpec
BoolSpecSignal :: Ident -> BoolSpec
BoolSpecConst :: BoolConst -> BoolSpec
BoolSpecNum :: NumExpr -> BoolSpec
BoolSpecCmp :: BoolSpec -> OrdOp -> BoolSpec -> BoolSpec
BoolSpecNeg :: BoolSpec -> BoolSpec
BoolSpecAnd :: BoolSpec -> BoolSpec -> BoolSpec
BoolSpecOr :: BoolSpec -> BoolSpec -> BoolSpec
BoolSpecXor :: BoolSpec -> BoolSpec -> BoolSpec
BoolSpecImplies :: BoolSpec -> BoolSpec -> BoolSpec
BoolSpecEquivs :: BoolSpec -> BoolSpec -> BoolSpec
BoolSpecOp1 :: OpOne -> BoolSpec -> BoolSpec
BoolSpecOp2 :: BoolSpec -> OpTwo -> BoolSpec -> BoolSpec
data NumExpr
NumId :: Ident -> NumExpr
NumConstI :: Integer -> NumExpr
NumConstD :: Double -> NumExpr
NumAdd :: NumExpr -> AdditiveOp -> NumExpr -> NumExpr
NumMult :: NumExpr -> MultOp -> NumExpr -> NumExpr
data AdditiveOp
OpPlus :: AdditiveOp
OpMinus :: AdditiveOp
data MultOp
OpTimes :: MultOp
OpDiv :: MultOp
data BoolConst
BoolConstTrue :: BoolConst
BoolConstFalse :: BoolConst
BoolConstFTP :: BoolConst
BoolConstLAST :: BoolConst
data OpOne
Op1Alone :: Op1Name -> OpOne
Op1MTL :: Op1Name -> OrdOp -> Number -> OpOne
Op1MTLRange :: Op1Name -> Number -> Number -> OpOne
data Number
NumberInt :: Integer -> Number
data OrdOp
OrdOpLT :: OrdOp
OrdOpLE :: OrdOp
OrdOpEQ :: OrdOp
OrdOpNE :: OrdOp
OrdOpGT :: OrdOp
OrdOpGE :: OrdOp
data Op1Name
Op1Pre :: Op1Name
Op1X :: Op1Name
Op1G :: Op1Name
Op1F :: Op1Name
Op1Y :: Op1Name
Op1Z :: Op1Name
Op1Hist :: Op1Name
Op1O :: Op1Name
data OpTwo
Op2S :: OpTwo
Op2T :: OpTwo
Op2V :: OpTwo
Op2U :: OpTwo
newtype Ident
Ident :: String -> Ident
instance GHC.Read.Read Language.SMV.AbsSMV.AdditiveOp
instance GHC.Show.Show Language.SMV.AbsSMV.AdditiveOp
instance GHC.Classes.Ord Language.SMV.AbsSMV.AdditiveOp
instance GHC.Classes.Eq Language.SMV.AbsSMV.AdditiveOp
instance GHC.Read.Read Language.SMV.AbsSMV.MultOp
instance GHC.Show.Show Language.SMV.AbsSMV.MultOp
instance GHC.Classes.Ord Language.SMV.AbsSMV.MultOp
instance GHC.Classes.Eq Language.SMV.AbsSMV.MultOp
instance GHC.Read.Read Language.SMV.AbsSMV.BoolConst
instance GHC.Show.Show Language.SMV.AbsSMV.BoolConst
instance GHC.Classes.Ord Language.SMV.AbsSMV.BoolConst
instance GHC.Classes.Eq Language.SMV.AbsSMV.BoolConst
instance GHC.Read.Read Language.SMV.AbsSMV.Number
instance GHC.Show.Show Language.SMV.AbsSMV.Number
instance GHC.Classes.Ord Language.SMV.AbsSMV.Number
instance GHC.Classes.Eq Language.SMV.AbsSMV.Number
instance GHC.Read.Read Language.SMV.AbsSMV.OrdOp
instance GHC.Show.Show Language.SMV.AbsSMV.OrdOp
instance GHC.Classes.Ord Language.SMV.AbsSMV.OrdOp
instance GHC.Classes.Eq Language.SMV.AbsSMV.OrdOp
instance GHC.Read.Read Language.SMV.AbsSMV.Op1Name
instance GHC.Show.Show Language.SMV.AbsSMV.Op1Name
instance GHC.Classes.Ord Language.SMV.AbsSMV.Op1Name
instance GHC.Classes.Eq Language.SMV.AbsSMV.Op1Name
instance GHC.Read.Read Language.SMV.AbsSMV.OpOne
instance GHC.Show.Show Language.SMV.AbsSMV.OpOne
instance GHC.Classes.Ord Language.SMV.AbsSMV.OpOne
instance GHC.Classes.Eq Language.SMV.AbsSMV.OpOne
instance GHC.Read.Read Language.SMV.AbsSMV.OpTwo
instance GHC.Show.Show Language.SMV.AbsSMV.OpTwo
instance GHC.Classes.Ord Language.SMV.AbsSMV.OpTwo
instance GHC.Classes.Eq Language.SMV.AbsSMV.OpTwo
instance Data.String.IsString Language.SMV.AbsSMV.Ident
instance GHC.Read.Read Language.SMV.AbsSMV.Ident
instance GHC.Show.Show Language.SMV.AbsSMV.Ident
instance GHC.Classes.Ord Language.SMV.AbsSMV.Ident
instance GHC.Classes.Eq Language.SMV.AbsSMV.Ident
instance GHC.Read.Read Language.SMV.AbsSMV.NumExpr
instance GHC.Show.Show Language.SMV.AbsSMV.NumExpr
instance GHC.Classes.Ord Language.SMV.AbsSMV.NumExpr
instance GHC.Classes.Eq Language.SMV.AbsSMV.NumExpr
instance GHC.Read.Read Language.SMV.AbsSMV.BoolSpec
instance GHC.Show.Show Language.SMV.AbsSMV.BoolSpec
instance GHC.Classes.Ord Language.SMV.AbsSMV.BoolSpec
instance GHC.Classes.Eq Language.SMV.AbsSMV.BoolSpec

module Language.SMV.LexSMV
alex_tab_size :: Int
alex_base :: AlexAddr
alex_table :: AlexAddr
alex_check :: AlexAddr
alex_deflt :: AlexAddr
alex_accept :: Array Int (AlexAcc user)
alex_actions :: Array Int (Posn -> String -> Token)
alex_action_1 :: Posn -> String -> Token
alex_action_2 :: Posn -> String -> Token
alex_action_3 :: Posn -> String -> Token
alex_action_4 :: Posn -> String -> Token
data AlexAddr
AlexA# :: Addr# -> AlexAddr
alexIndexInt16OffAddr :: AlexAddr -> Int# -> Int#
alexIndexInt32OffAddr :: AlexAddr -> Int# -> Int#
quickIndex :: Array Int (AlexAcc (Any :: Type)) -> Int -> AlexAcc (Any :: Type)
data AlexReturn a
AlexEOF :: AlexReturn a
AlexError :: !AlexInput -> AlexReturn a
AlexSkip :: !AlexInput -> !Int -> AlexReturn a
AlexToken :: !AlexInput -> !Int -> a -> AlexReturn a
alexScan :: (Posn, Char, [Byte], String) -> Int -> AlexReturn (Posn -> String -> Token)
alexScanUser :: t -> (Posn, Char, [Byte], String) -> Int -> AlexReturn (Posn -> String -> Token)
alex_scan_tkn :: t -> t -> Int# -> AlexInput -> Int# -> AlexLastAcc -> (AlexLastAcc, (Posn, Char, [Byte], String))
data AlexLastAcc
AlexNone :: AlexLastAcc
AlexLastAcc :: !Int -> !AlexInput -> !Int -> AlexLastAcc
AlexLastSkip :: !AlexInput -> !Int -> AlexLastAcc
data AlexAcc user
AlexAccNone :: AlexAcc user
AlexAcc :: Int -> AlexAcc user
AlexAccSkip :: AlexAcc user

-- | Create a token with position.
tok :: (String -> Tok) -> Posn -> String -> Token

-- | Token without position.
data Tok

-- | Reserved word or symbol.
TK :: {-# UNPACK #-} !TokSymbol -> Tok

-- | String literal.
TL :: !String -> Tok

-- | Integer literal.
TI :: !String -> Tok

-- | Identifier.
TV :: !String -> Tok

-- | Float literal.
TD :: !String -> Tok

-- | Character literal.
TC :: !String -> Tok

-- | Smart constructor for Tok for the sake of backwards
--   compatibility.
pattern TS :: String -> Int -> Tok

-- | Keyword or symbol tokens have a unique ID.
data TokSymbol
TokSymbol :: String -> !Int -> TokSymbol

-- | Keyword or symbol text.
[tsText] :: TokSymbol -> String

-- | Unique ID.
[tsID] :: TokSymbol -> !Int

-- | Token with position.
data Token
PT :: Posn -> Tok -> Token
Err :: Posn -> Token

-- | Pretty print a position.
printPosn :: Posn -> String

-- | Pretty print the position of the first token in the list.
tokenPos :: [Token] -> String

-- | Get the position of a token.
tokenPosn :: Token -> Posn

-- | Get line and column of a token.
tokenLineCol :: Token -> (Int, Int)

-- | Get line and column of a position.
posLineCol :: Posn -> (Int, Int)

-- | Convert a token into "position token" form.
mkPosToken :: Token -> ((Int, Int), String)

-- | Convert a token to its text.
tokenText :: Token -> String

-- | Convert a token to a string.
prToken :: Token -> String

-- | Finite map from text to token organized as binary search tree.
data BTree

-- | Nil (leaf).
N :: BTree

-- | Binary node.
B :: String -> Tok -> BTree -> BTree -> BTree

-- | Convert potential keyword into token or use fallback conversion.
eitherResIdent :: (String -> Tok) -> String -> Tok

-- | The keywords and symbols of the language organized as binary search
--   tree.
resWords :: BTree

-- | Unquote string literal.
unescapeInitTail :: String -> String
data Posn
Pn :: !Int -> !Int -> !Int -> Posn
alexStartPos :: Posn
alexMove :: Posn -> Char -> Posn
type Byte = Word8
type AlexInput = (Posn, Char, [Byte], String)
tokens :: String -> [Token]
alexGetByte :: AlexInput -> Maybe (Byte, AlexInput)
alexInputPrevChar :: AlexInput -> Char

-- | Encode a Haskell String to a list of Word8 values, in UTF8 format.
utf8Encode :: Char -> [Word8]
instance GHC.Show.Show Language.SMV.LexSMV.TokSymbol
instance GHC.Classes.Ord Language.SMV.LexSMV.Tok
instance GHC.Show.Show Language.SMV.LexSMV.Tok
instance GHC.Classes.Eq Language.SMV.LexSMV.Tok
instance GHC.Show.Show Language.SMV.LexSMV.BTree
instance GHC.Classes.Ord Language.SMV.LexSMV.Posn
instance GHC.Show.Show Language.SMV.LexSMV.Posn
instance GHC.Classes.Eq Language.SMV.LexSMV.Posn
instance GHC.Classes.Ord Language.SMV.LexSMV.Token
instance GHC.Show.Show Language.SMV.LexSMV.Token
instance GHC.Classes.Eq Language.SMV.LexSMV.Token
instance GHC.Classes.Eq Language.SMV.LexSMV.TokSymbol
instance GHC.Classes.Ord Language.SMV.LexSMV.TokSymbol

module Language.SMV.ParSMV
happyError :: [Token] -> Err a
myLexer :: String -> [Token]
pBoolSpec :: [Token] -> Err BoolSpec

-- | Pretty-printer for Language.
module Language.SMV.PrintSMV

-- | The top-level printing method.
printTree :: Print a => a -> String
type Doc = [ShowS] -> [ShowS]
doc :: ShowS -> Doc
render :: Doc -> String
parenth :: Doc -> Doc
concatS :: [ShowS] -> ShowS
concatD :: [Doc] -> Doc
replicateS :: Int -> ShowS -> ShowS

-- | The printer class does the job.
class Print a
prt :: Print a => Int -> a -> Doc
printString :: String -> Doc
mkEsc :: Char -> Char -> ShowS
prPrec :: Int -> Int -> Doc -> Doc
instance Language.SMV.PrintSMV.Print a => Language.SMV.PrintSMV.Print [a]
instance Language.SMV.PrintSMV.Print GHC.Types.Char
instance Language.SMV.PrintSMV.Print GHC.Base.String
instance Language.SMV.PrintSMV.Print GHC.Num.Integer.Integer
instance Language.SMV.PrintSMV.Print GHC.Types.Double
instance Language.SMV.PrintSMV.Print Language.SMV.AbsSMV.Ident
instance Language.SMV.PrintSMV.Print Language.SMV.AbsSMV.BoolSpec
instance Language.SMV.PrintSMV.Print Language.SMV.AbsSMV.NumExpr
instance Language.SMV.PrintSMV.Print Language.SMV.AbsSMV.AdditiveOp
instance Language.SMV.PrintSMV.Print Language.SMV.AbsSMV.MultOp
instance Language.SMV.PrintSMV.Print Language.SMV.AbsSMV.BoolConst
instance Language.SMV.PrintSMV.Print Language.SMV.AbsSMV.OpOne
instance Language.SMV.PrintSMV.Print Language.SMV.AbsSMV.Number
instance Language.SMV.PrintSMV.Print Language.SMV.AbsSMV.OrdOp
instance Language.SMV.PrintSMV.Print Language.SMV.AbsSMV.Op1Name
instance Language.SMV.PrintSMV.Print Language.SMV.AbsSMV.OpTwo

module Language.SMV.Substitution
substituteBoolExpr :: Foldable t => t (String, String) -> BoolSpec -> BoolSpec
subsName :: Eq b => (b, b) -> b -> b
subBS :: (String, String) -> BoolSpec -> BoolSpec
mapBoolSpecIdent :: (String -> String) -> BoolSpec -> BoolSpec
mapNumExprIdent :: (String -> String) -> NumExpr -> NumExpr
