Scyther.Theory.Pretty
Description
Pretty printing a security protocol theory.
- newtype TaggedIdentityT t m a = TaggedIdentityT {
- unTaggedIdentityT :: m a
- runTaggedIdentityT :: t -> TaggedIdentityT t m a -> m a
- data SlimOutput = SlimOutput
- class (Applicative m, Monad m) => MarkupMonad m where
- withGraph :: Document d => Dot a -> m d -> m d
- withExplanation :: Document d => String -> m d -> m d
- theoremRef :: Document d => Protocol -> String -> m d
- theoremDef :: Document d => Theorem -> m d -> m d
- keyword :: Document d => String -> m d -> m d
- noteCases :: Document d => Dot a -> [(String, Dot b)] -> [(String, Dot b)] -> m d -> m d
- class MarkupMonad m => PrettyMonad m where
- prettyTID :: TID -> m Doc
- prettyAgentId :: AgentId -> m Doc
- prettyMessage :: Message -> m Doc
- prettyFacts :: Facts -> m ([Doc], [Doc], [Doc])
- prettyFormula :: Mapping -> Formula -> m Doc
- prettySequent :: Sequent -> m Doc
- ensureProofMode :: (Bool, Bool) -> m Doc
- withFactsMode :: (Bool, Bool) -> m Doc -> m Doc
- prettyTrivial :: Sequent -> TrivReason -> m Doc
- prettyMissing :: Sequent -> String -> m Doc
- prettySaturate :: Sequent -> m Doc
- prettyForwardContradiction :: m Doc -> m Doc
- prettyForwardResolution :: m Doc -> Sequent -> Mapping -> m Doc
- prettyNextCase :: m Doc
- prettyChainRuleSplitCases :: [ChainRuleCase] -> m ([ChainRuleCase], [ChainRuleCase])
- prettyChainRuleApplication :: m Doc -> m Doc
- prettyChainRuleCase :: (String, [Either TID AgentId]) -> m Doc
- prettyChainRuleQED :: Message -> [ChainRuleCase] -> m Doc
- prettyTypeCheckInduction :: Protocol -> String -> Typing -> (m Doc, m Doc -> m Doc, m Doc)
- prettyTypingCase :: String -> Typing -> String -> Sequent -> m Doc
- prettySplitEqCase :: PrettyMonad m => String -> m Doc
- prettySplitEqApplication :: PrettyMonad m => MsgEq -> m Doc
- prettySplitEqQed :: PrettyMonad m => m Doc
- prettyComment :: String -> m Doc
- prettyProtoDef :: Protocol -> [Theorem] -> m Doc
- prettyTheorem :: Theorem -> m Doc
- prettyTheoryDef :: String -> Doc -> m Doc
- prettyTheory :: PrettyMonad m => Theory -> m Doc
- prettySoundness :: Applicative f => Theory -> f Doc
Documentation
newtype TaggedIdentityT t m a Source
Constructors
| TaggedIdentityT | |
Fields
| |
Instances
| MonadTrans (TaggedIdentityT t) | |
| Monad m => Monad (TaggedIdentityT t m) | |
| Functor m => Functor (TaggedIdentityT t m) | |
| Applicative m => Applicative (TaggedIdentityT t m) | |
| MarkupMonad m => PrettyMonad (TaggedIdentityT SlimOutput m) | A slim output mode for better readability. |
| MarkupMonad m => MarkupMonad (TaggedIdentityT t m) |
runTaggedIdentityT :: t -> TaggedIdentityT t m a -> m aSource
data SlimOutput Source
Phantom type marking slim output.
Constructors
| SlimOutput |
Instances
| MarkupMonad m => PrettyMonad (TaggedIdentityT SlimOutput m) | A slim output mode for better readability. |
class (Applicative m, Monad m) => MarkupMonad m whereSource
A monad for inserting markup into output.
Methods
withGraph :: Document d => Dot a -> m d -> m dSource
withExplanation :: Document d => String -> m d -> m dSource
theoremRef :: Document d => Protocol -> String -> m dSource
theoremDef :: Document d => Theorem -> m d -> m dSource
Instances
| MarkupMonad Identity | |
| MarkupMonad HtmlMarkup | |
| MarkupMonad m => MarkupMonad (ReaderT r m) | |
| MarkupMonad m => MarkupMonad (TaggedIdentityT t m) |
class MarkupMonad m => PrettyMonad m whereSource
A pretty printing monad allowing for economically replacing parts of the pretty printer.
Methods
prettyTID :: TID -> m DocSource
prettyAgentId :: AgentId -> m DocSource
prettyMessage :: Message -> m DocSource
prettyFacts :: Facts -> m ([Doc], [Doc], [Doc])Source
prettyFormula :: Mapping -> Formula -> m DocSource
prettySequent :: Sequent -> m DocSource
ensureProofMode :: (Bool, Bool) -> m DocSource
withFactsMode :: (Bool, Bool) -> m Doc -> m DocSource
prettyTrivial :: Sequent -> TrivReason -> m DocSource
prettyMissing :: Sequent -> String -> m DocSource
prettySaturate :: Sequent -> m DocSource
prettyForwardContradiction :: m Doc -> m DocSource
prettyForwardResolution :: m Doc -> Sequent -> Mapping -> m DocSource
prettyNextCase :: m DocSource
prettyChainRuleSplitCases :: [ChainRuleCase] -> m ([ChainRuleCase], [ChainRuleCase])Source
prettyChainRuleApplication :: m Doc -> m DocSource
prettyChainRuleCase :: (String, [Either TID AgentId]) -> m DocSource
prettyChainRuleQED :: Message -> [ChainRuleCase] -> m DocSource
prettyTypeCheckInduction :: Protocol -> String -> Typing -> (m Doc, m Doc -> m Doc, m Doc)Source
prettyTypingCase :: String -> Typing -> String -> Sequent -> m DocSource
prettySplitEqCase :: PrettyMonad m => String -> m DocSource
prettySplitEqApplication :: PrettyMonad m => MsgEq -> m DocSource
prettySplitEqQed :: PrettyMonad m => m DocSource
prettyComment :: String -> m DocSource
prettyProtoDef :: Protocol -> [Theorem] -> m DocSource
prettyTheorem :: Theorem -> m DocSource
prettyTheoryDef :: String -> Doc -> m DocSource
Instances
| MarkupMonad m => PrettyMonad (ReaderT IsarConf m) | Pretty printing as an ISAR theory file is accomplished by using a reader monad transformer with an ISAR output configuration as the environment. |
| MarkupMonad m => PrettyMonad (TaggedIdentityT SlimOutput m) | A slim output mode for better readability. |
prettyTheory :: PrettyMonad m => Theory -> m DocSource
Pretty print a theory.
prettySoundness :: Applicative f => Theory -> f DocSource
Pretty print soundness information.