Generating Isabelle/ISAR theory files using Text.PrettyPrint
.
- class Isar a where
- data IsarStyle
- data IsarConf = IsarConf {}
- defaultIsarConf :: IsarConf
- isPlainStyle :: IsarConf -> Bool
- isarPlain :: Isar a => a -> Doc
- isarXSymbol :: Isar a => a -> Doc
- isaExecutionSystemState :: IsarConf -> Doc
- isarightArrow :: Document d => IsarConf -> d
- isaLongRightArrow :: Document d => IsarConf -> d
- isaLParr :: Document d => IsarConf -> d
- isaRParr :: Document d => IsarConf -> d
- isaLBrack :: Document d => IsarConf -> d
- isaRBrack :: Document d => IsarConf -> d
- isaMetaAll :: Document d => IsarConf -> d
- isaExists :: Document d => IsarConf -> d
- isaAnd :: Document d => IsarConf -> d
- isaNotIn :: Document d => IsarConf -> d
- isaIn :: Document d => IsarConf -> d
- isaSubsetEq :: Document d => IsarConf -> d
- isaAlpha :: Document d => IsarConf -> d
- isaSublocale :: Document d => IsarConf -> d
- module Text.PrettyPrint.Class
- nestBetween :: Document d => Int -> d -> d -> d -> d
- nestShort :: Document d => Int -> d -> d -> d -> d
- nestShort' :: Document d => String -> String -> d -> d
- nestShortNonEmpty :: Document d => Int -> d -> d -> d -> d
- nestShortNonEmpty' :: Document d => String -> String -> d -> d
- fixedWidthText :: Document d => Int -> String -> d
- symbol :: Document d => String -> d
- numbered :: Document d => d -> [d] -> d
- numbered' :: Document d => [d] -> d
ISAR Output
Values that can be output as ISAR code.
Minimal definition: isar
Configuration
The ISAR style to be used for output.
The configuration to be used for output. Apart from the ISAR style, the configuration also stores the representation of the reachable state of the protocol which we are reasoning about.
Show IsarConf | |
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. |
defaultIsarConf :: IsarConfSource
Default configuration: plaintext ISAR style and reachable state (t,r,s)
.
isPlainStyle :: IsarConf -> BoolSource
Check if the plaintext style was chosen.
isarPlain :: Isar a => a -> DocSource
Output as ISAR code using defaultIsarConf
.
isarXSymbol :: Isar a => a -> DocSource
Output as ISAR code using defaultIsarConf
with the XSymbol style.
Constructions of our security protocol verification theory
isaExecutionSystemState :: IsarConf -> DocSource
Isabelle representation of the exeuction system state of our operational semantics.
Special Symbols
isarightArrow :: Document d => IsarConf -> dSource
A short right arrow: ->
isaLongRightArrow :: Document d => IsarConf -> dSource
A long double right arrow: ==>
isaLParr :: Document d => IsarConf -> dSource
A left parenthesis with an additional vertical line: (|
isaRParr :: Document d => IsarConf -> dSource
A right parenthesis with an additional vertical line: |)
isaMetaAll :: Document d => IsarConf -> dSource
The meta all quantifier: !!
isaSubsetEq :: Document d => IsarConf -> dSource
The non-strict subset symbol.
isaSublocale :: Document d => IsarConf -> dSource
The sublocale sign.
Extensions of Text.PrettyPrint
module Text.PrettyPrint.Class
:: Document d | |
=> Int | Indent of body |
-> d | Leading document |
-> d | Finishing document |
-> d | Body document |
-> d |
Nest a document surrounded by a leading and a finishing document breaking lead, body, and finish onto separate lines, if they don't fit on a single line.
:: Document d | |
=> Int | Indent of body |
-> d | Leading document |
-> d | Finishing document |
-> d | Body document |
-> d |
Nest a document surrounded by a leading and a finishing document with an non-compulsory break between lead and body.
nestShort' :: Document d => String -> String -> d -> dSource
Nest document between two strings and indent body by length lead + 1
.
nestShortNonEmpty :: Document d => Int -> d -> d -> d -> dSource
Like nestShort
but doesn't print the lead and finish, if the document is
empty.
nestShortNonEmpty' :: Document d => String -> String -> d -> dSource
Like nestShort'
but doesn't print the lead and finish, if the document is
empty.
fixedWidthText :: Document d => Int -> String -> dSource
Output text with a fixed width: if it is smaller then nothing happens, otherwise care is taken to make the text appear having the given width.