-- | Generating Isabelle/ISAR theory files using 'Text.PrettyPrint'.
module Text.Isar (
    -- * ISAR Output
    Isar(..)
    -- ** Configuration
  , IsarStyle(..)
  , IsarConf(..)
  , defaultIsarConf
  , isPlainStyle
  , isarPlain
  , isarXSymbol

  -- ** Constructions of our security protocol verification theory
  , isaExecutionSystemState

  -- ** Special Symbols
  , isarightArrow
  , isaLongRightArrow
  , isaLParr
  , isaRParr
  , isaLBrack
  , isaRBrack
  , isaMetaAll
  , isaExists
  , isaForall
  , isaLambda
  , isaAnd
  , isaOr
  , isaImplies
  , isaNotIn
  , isaIn
  , isaSubsetEq
  , isaAlpha
  , isaSublocale
  , isaNotEq

    -- * Extensions of 'Text.PrettyPrint'
  , module Text.PrettyPrint.Class
  , nestBetween
  , nestShort
  , nestShort'
  , nestShortNonEmpty
  , nestShortNonEmpty'
  , fixedWidthText
  , symbol
  , numbered
  , numbered'

) where

import Data.List

import Extension.Prelude

import Text.PrettyPrint.Class

-- | The ISAR style to be used for output.
data IsarStyle =
    PlainText
  | XSymbol
  deriving( Eq, Show )

-- | 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.
data IsarConf = IsarConf {
    isarStyle :: IsarStyle
  , isarTrace :: Doc        -- ^ The ISAR code of the trace
  , isarPool  :: Doc        -- ^ The ISAR code of the thread pool
  , isarSubst :: Doc        -- ^ The ISAR code of the substitution
  }
  deriving( Show )

-- | Default configuration: plaintext ISAR style and reachable state @(t,r,s)@.
defaultIsarConf :: IsarConf
defaultIsarConf = IsarConf PlainText (char 't') (char 'r') (char 's')

-- | Check if the plaintext style was chosen.
isPlainStyle :: IsarConf -> Bool
isPlainStyle = (PlainText ==) . isarStyle


-- | Values that can be output as ISAR code.
--
-- Minimal definition: 'isar'
class Isar a where
  isar :: IsarConf -> a -> Doc

-- | Output as ISAR code using 'defaultIsarConf'.
isarPlain :: Isar a => a -> Doc
isarPlain = isar defaultIsarConf

-- | Output as ISAR code using 'defaultIsarConf'
-- with the XSymbol style.
isarXSymbol :: Isar a => a -> Doc
isarXSymbol = isar (defaultIsarConf { isarStyle = XSymbol })

------------------------------------------------------------------------------
-- General pretty printing combinators
------------------------------------------------------------------------------

-- | 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.
nestBetween :: Document d =>
               Int -- ^ Indent of body
            -> d -- ^ Leading document
            -> d -- ^ Finishing document
            -> d -- ^ Body document
            -> d
nestBetween n l r x = sep [l, nest n x, r]

-- | Nest a document surrounded by a leading and a finishing document with an
-- non-compulsory break between lead and body.
nestShort :: Document d =>
             Int -- ^ Indent of body
          -> d -- ^ Leading document
          -> d -- ^ Finishing document
          -> d -- ^ Body document
          -> d
nestShort n lead finish body = sep [lead $$ nest n body, finish]

-- | Nest document between two strings and indent body by @length lead + 1@.
nestShort' :: Document d => String -> String -> d -> d
nestShort' lead finish =
  nestShort (length lead + 1) (text lead) (text finish)

-- | Like 'nestShort' but doesn't print the lead and finish, if the document is
-- empty.
nestShortNonEmpty :: Document d => Int -> d -> d -> d -> d
nestShortNonEmpty n lead finish body =
  caseEmptyDoc emptyDoc (nestShort n lead finish body) body

-- | Like 'nestShort'' but doesn't print the lead and finish, if the document is
-- empty.
nestShortNonEmpty' :: Document d => String -> String -> d -> d
nestShortNonEmpty' lead finish =
  nestShortNonEmpty (length lead + 1) (text lead) (text finish)

-- | 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.
fixedWidthText :: Document d => Int -> String -> d
fixedWidthText n cs
  | length cs <= n  = text cs
  | otherwise = text as <> zeroWidthText bs
  where
  (as,bs) = splitAt n cs

-- | Print string as symbol having width 1.
symbol :: Document d => String -> d
symbol = fixedWidthText 1

-- | Number a list of documents that are vertically separated by the given
-- separator.
numbered :: Document d => d -> [d] -> d
numbered _   [] = emptyDoc
numbered vsep ds =
    foldr1 ($-$) $ intersperse vsep $ map pp $ zip [(1::Int)..] ds
  where
    n         = length ds
    nWidth    = length (show n)
    pp (i, d) = text (flushRight nWidth (show i)) <> d

-- | Number a list of documents with numbers terminated by "." and vertically
-- separate using an empty line.
numbered' :: Document d => [d] -> d
numbered' = numbered (text "") . map (text ". " <>)


------------------------------------------------------------------------------
-- Operational Semantics Constructions
------------------------------------------------------------------------------

-- | Isabelle representation of the exeuction system state of our operational
-- semantics.
isaExecutionSystemState :: IsarConf -> Doc
isaExecutionSystemState conf =
  parens . hcat . punctuate comma $
    [isarTrace conf, isarPool conf, isarSubst conf]


------------------------------------------------------------------------------
-- Isabelle symbols in both styles.
------------------------------------------------------------------------------

-- | A 'not in' symbol: @~:@
isaNotIn :: Document d => IsarConf -> d
isaNotIn conf
  | isPlainStyle conf = text "~:"
  | otherwise         = symbol "\\<notin>"

-- | An 'in' symbol: @:@
isaIn :: Document d => IsarConf -> d
isaIn conf
  | isPlainStyle conf  = text ":"
  | otherwise         = symbol "\\<in>"

-- | A left parenthesis with an additional vertical line: @(|@
isaLParr :: Document d => IsarConf -> d
isaLParr conf
  | isPlainStyle conf = text "(|"
  | otherwise         = symbol "\\<lparr>"

-- | A right parenthesis with an additional vertical line: @|)@
isaRParr :: Document d => IsarConf -> d
isaRParr conf
  | isPlainStyle conf = text "|)"
  | otherwise         = symbol "\\<rparr>"

-- | A left bracket with an additional vertical line: @[|@
isaLBrack :: Document d => IsarConf -> d
isaLBrack conf
  | isPlainStyle conf = text "[|"
  | otherwise         = symbol "\\<lbrakk>"

-- | A right bracket with an additional vertical line: @|]@
isaRBrack :: Document d => IsarConf -> d
isaRBrack conf
  | isPlainStyle conf = text "|]"
  | otherwise         = symbol "\\<rbrakk>"

-- | A short right arrow: @->@
isarightArrow :: Document d => IsarConf -> d
isarightArrow conf
  | isPlainStyle conf = text "->"
  | otherwise         = fixedWidthText 2 "\\<rightarrow>"

-- | A long double right arrow: @==>@
isaLongRightArrow :: Document d => IsarConf -> d
isaLongRightArrow conf
  | isPlainStyle conf = text "==>"
  | otherwise         = fixedWidthText 3 "\\<Longrightarrow>"


-- | The greek letter alpha: @\\<alpha>@
isaAlpha :: Document d => IsarConf -> d
isaAlpha conf
  | isPlainStyle conf = text "\\<alpha>"
  | otherwise         = symbol "\\<alpha>"

-- | The meta all quantifier: @!!@
isaMetaAll :: Document d => IsarConf -> d
isaMetaAll conf
  | isPlainStyle conf = text "!! "
  | otherwise         = symbol "\\<And>"

-- | The exists symbol: @?@
isaExists :: Document d => IsarConf -> d
isaExists conf
  | isPlainStyle conf = text "? "
  | otherwise         = symbol "\\<exists>"

-- | The forall symbol: @!@
isaForall :: Document d => IsarConf -> d
isaForall conf
  | isPlainStyle conf = text "! "
  | otherwise         = symbol "\\<forall>"

-- | The lambda symbol: @%@
isaLambda :: Document d => IsarConf -> d
isaLambda conf
  | isPlainStyle conf = text "% "
  | otherwise         = symbol "\\<lambda>"

-- | The logical and symbol: @&@
isaAnd :: Document d => IsarConf -> d
isaAnd conf
  | isPlainStyle conf = text "&"
  | otherwise         = symbol "\\<and>"

-- | The logical or symbol: @|@
isaOr :: Document d => IsarConf -> d
isaOr conf
  | isPlainStyle conf = text "|"
  | otherwise         = symbol "\\<or>"

-- | The logical and symbol: @-->@
isaImplies :: Document d => IsarConf -> d
isaImplies conf
  | isPlainStyle conf = text "-->"
  | otherwise         = symbol "\\<longrightarrow>"

-- | The non-strict subset symbol.
isaSubsetEq :: Document d => IsarConf -> d
isaSubsetEq conf
  | isPlainStyle conf = text "<="
  | otherwise         = symbol "\\<subseteq>"

-- | The sublocale sign.
isaSublocale :: Document d => IsarConf -> d
isaSublocale conf
  | isPlainStyle conf = text "<"
  | otherwise         = symbol "\\<subseteq>"

-- | The not equal symbol: @~=@
isaNotEq :: Document d => IsarConf -> d
isaNotEq conf
  | isPlainStyle conf = text "~="
  | otherwise         = symbol "\\<noteq>"

------------------------------------------------------------------------------
-- Isabelle theory components
------------------------------------------------------------------------------

{- TODO: Finish, if it is used

isaTheory :: Document d =>
             String     -- ^ Theory name
          -> [String]   -- ^ Imported theories
          -> d          -- ^ Theory body
          -> d          -- ^ The complete theory statement.
isaTheory name imports body =
  text "theory" <-> text name $-$
  text "imports" $-$
  nest 2 (vcat $ map (text . (++"\"") . ('"':)) imports) $-$
  text "begin" $-$ text "" $-$
  body $-$
  text "" $-$ text "end"


-- | An logic identifier; properly escaped if needed.
-- TODO: Add escaping
logicIdent :: String -> Doc
logicIdent = text


-- | A generic text command.
genTextCmd :: String -> String -> Doc
genTextCmd name content =
  sep [text name <> text "{*", nest 2 (fsep . map text $ words content), text "*}"]

chapter = genTextCmd "chapter"
section = genTextCmd "section"
subsection = genTextCmd "subsection"
subsubsection = genTextCmd "subsubsection"
paragraph = genTextCmd "text"

-- | A comment.
comment :: String -> Doc
comment content = nestShort' "(*" "*)" (fsep $ map text $ words content)

-- | Switch into a proof context.
context :: String -> Doc -> Doc
context name body = vcat [text name <-> text "begin", body, text "end"]

-}