{-|
Module      : LogicProof
Description : Provides a way to write logic proofs in Markdown.
Copyright   : (c) 2020-2023 Amy de Buitléir
License     : BSD--3
Maintainer  : amy@nualeargais.ie
Stability   : experimental
Portability : POSIX

See <https://github.com/mhwombat/pandoc-logic-proof> for information
on how to use this filter.
-}

{-# LANGUAGE OverloadedStrings #-}

module Text.Pandoc.Filters.LogicProof
  (
    transform,
    formatProofs
  ) where

import Data.Foldable    (foldl')
import Data.Text        qualified as T
import Text.Pandoc      qualified as P
import Text.Pandoc.Walk (walk)


-- | A transformation that can be used with Hakyll.
transform :: P.Pandoc -> P.Pandoc
transform :: Pandoc -> Pandoc
transform = forall a b. Walkable a b => (a -> a) -> b -> b
walk Block -> Block
formatProofs

-- | Exported for use by the executable.
formatProofs :: P.Block -> P.Block
formatProofs :: Block -> Block
formatProofs x :: Block
x@(P.CodeBlock (Text
_,[Text]
cs,[(Text, Text)]
_) Text
s)
  | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Text]
cs                = Block
x
  | forall a. [a] -> a
head [Text]
cs forall a. Eq a => a -> a -> Bool
== Text
"logicproof" = Proof -> Block
proofToTable forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof -> Proof
renumber forall a b. (a -> b) -> a -> b
$ Text -> Proof
parseProof Text
s
  | Bool
otherwise              = Block
x
formatProofs Block
x = Block
x

type Proof = [ProofRow]

type ProofRow = [T.Text]

proofToTable :: Proof -> P.Block
proofToTable :: Proof -> Block
proofToTable Proof
p = (Text, [Text], [(Text, Text)])
-> Caption
-> [ColSpec]
-> TableHead
-> [TableBody]
-> TableFoot
-> Block
P.Table forall {a}. (Text, [Text], [a])
attr Caption
defaultTableCaption [ColSpec]
colSpecs
                    TableHead
defaultTableHeader [Proof -> TableBody
toTableBody Proof
p]
                    TableFoot
defaultTableFooter
  where attr :: (Text, [Text], [a])
attr = (Text
"",[Text
"logicproof"],[])
        colSpecs :: [ColSpec]
colSpecs = forall a. Int -> a -> [a]
replicate Int
3 ColSpec
defaultColSpec

toTableBody :: Proof -> P.TableBody
toTableBody :: Proof -> TableBody
toTableBody Proof
p = (Text, [Text], [(Text, Text)])
-> RowHeadColumns -> [Row] -> [Row] -> TableBody
P.TableBody (Text, [Text], [(Text, Text)])
P.nullAttr (Int -> RowHeadColumns
P.RowHeadColumns Int
0) []
                  forall a b. (a -> b) -> a -> b
$  forall a b. (a -> b) -> [a] -> [b]
map [Text] -> Row
toTableRow Proof
p

toTableRow :: ProofRow -> P.Row
toTableRow :: [Text] -> Row
toTableRow [Text]
row
  | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Text]
row forall a. Ord a => a -> a -> Bool
< Int
3 = forall a. HasCallStack => [Char] -> a
error [Char]
"short row in logic proof"
  | Bool
otherwise      = (Text, [Text], [(Text, Text)]) -> [Cell] -> Row
P.Row (Text, [Text], [(Text, Text)])
P.nullAttr [Cell]
cells
  where label :: Text
label = forall a. [a] -> a
head [Text]
row
        justification :: Text
justification = forall a. [a] -> a
last [Text]
row
        statement :: Text
statement = forall a. [a] -> a
penultimate [Text]
row
        depth :: Int
depth = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Text]
row forall a. Num a => a -> a -> a
- Int
3
        statement' :: Text
statement' = Int -> Text -> Text
indent Int
depth Text
statement
        cells :: [Cell]
cells = [
                  Text -> Cell
textToCell Text
label,
                  [Block] -> Cell
blocksToCell forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Block -> Block
removePara forall a b. (a -> b) -> a -> b
$ Text -> [Block]
parseBlocks Text
statement',
                  [Block] -> Cell
blocksToCell forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Block -> Block
removePara forall a b. (a -> b) -> a -> b
$ Text -> [Block]
parseBlocks Text
justification
                ]

removePara :: P.Block -> P.Block
removePara :: Block -> Block
removePara (P.Para [Inline]
xs) = [Inline] -> Block
P.Plain [Inline]
xs
removePara Block
x           = Block
x

penultimate :: [a] -> a
penultimate :: forall a. [a] -> a
penultimate = forall a. [a] -> a
last forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
init

indent :: Int -> T.Text -> T.Text
indent :: Int -> Text -> Text
indent Int
0 Text
s = Text
s
indent Int
n Text
s = Text
filler Text -> Text -> Text
`T.append` Text
s
  where filler :: Text
filler = [Char] -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall a. Int -> a -> [a]
replicate Int
n
                     [Char]
"&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"

blocksToCell :: [P.Block] -> P.Cell
blocksToCell :: [Block] -> Cell
blocksToCell
  = (Text, [Text], [(Text, Text)])
-> Alignment -> RowSpan -> ColSpan -> [Block] -> Cell
P.Cell (Text, [Text], [(Text, Text)])
P.nullAttr Alignment
P.AlignDefault (Int -> RowSpan
P.RowSpan Int
1) (Int -> ColSpan
P.ColSpan Int
1)

textToCell :: T.Text -> P.Cell
textToCell :: Text -> Cell
textToCell Text
t
  = (Text, [Text], [(Text, Text)])
-> Alignment -> RowSpan -> ColSpan -> [Block] -> Cell
P.Cell (Text, [Text], [(Text, Text)])
P.nullAttr Alignment
P.AlignDefault (Int -> RowSpan
P.RowSpan Int
1) (Int -> ColSpan
P.ColSpan Int
1)
      [ [Inline] -> Block
P.Plain [Text -> Inline
P.Str Text
t] ]

parseProof :: T.Text -> Proof
parseProof :: Text -> Proof
parseProof = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a -> b) -> [a] -> [b]
map Text -> Text
trim  forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text -> [Text]
T.splitOn Text
"|") forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Text]
T.lines

renumber :: Proof -> Proof
renumber :: Proof -> Proof
renumber Proof
proofRows = forall a b. (a -> b) -> [a] -> [b]
map ([(Text, Text)] -> [Text] -> [Text]
fillInReferences [(Text, Text)]
refs) Proof
proofRows'
  where proofRows' :: Proof
proofRows' = Proof -> Proof
renumber' Proof
proofRows
        refs :: [(Text, Text)]
refs = Proof -> [(Text, Text)]
makeLookupTable Proof
proofRows'

renumber' :: Proof -> Proof
renumber' :: Proof -> Proof
renumber' = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {a}. Show a => a -> [Text] -> [Text]
f [(Int
1 :: Int)..]
  where f :: a -> [Text] -> [Text]
f a
n [Text]
row = [Char] -> Text
T.pack (forall a. Show a => a -> [Char]
show a
n) forall a. a -> [a] -> [a]
: [Text]
row

makeLookupTable :: Proof -> [(T.Text, T.Text)]
makeLookupTable :: Proof -> [(Text, Text)]
makeLookupTable = forall a b. (a -> b) -> [a] -> [b]
map [Text] -> (Text, Text)
f
  where f :: [Text] -> (Text, Text)
f (Text
new : Text
old : [Text]
_) = ([Char] -> Text
T.pack ([Char]
"(@" forall a. [a] -> [a] -> [a]
++ Text -> [Char]
T.unpack Text
old forall a. [a] -> [a] -> [a]
++ [Char]
")"), Text
new)
        f [Text]
_               = forall a. HasCallStack => [Char] -> a
error [Char]
"short row in logic proof"

fillInReferences :: [(T.Text, T.Text)] -> ProofRow -> ProofRow
fillInReferences :: [(Text, Text)] -> [Text] -> [Text]
fillInReferences [(Text, Text)]
refs (Text
label : Text
_ : [Text]
fields)
  = (Text
label Text -> Text -> Text
`T.append` Text
".") forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map ([(Text, Text)] -> Text -> Text
multiReplace [(Text, Text)]
refs) [Text]
fields
fillInReferences [(Text, Text)]
_ [Text]
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"short row in logic proof"

multiReplace :: [(T.Text, T.Text)] -> T.Text -> T.Text
multiReplace :: [(Text, Text)] -> Text -> Text
multiReplace [(Text, Text)]
refs Text
haystack = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Text -> (Text, Text) -> Text
replace Text
haystack [(Text, Text)]
refs

replace :: T.Text -> (T.Text, T.Text) -> T.Text
replace :: Text -> (Text, Text) -> Text
replace Text
haystack (Text
needle, Text
label) = Text -> Text -> Text -> Text
T.replace Text
needle Text
label Text
haystack

trim :: T.Text -> T.Text
trim :: Text -> Text
trim Text
s
  | Text -> Bool
T.null Text
s       = Text
s
  | Text -> Char
T.head Text
s forall a. Eq a => a -> a -> Bool
== Char
' ' = Text -> Text
trim (Text -> Text
T.tail Text
s)
  | Text -> Char
T.last Text
s forall a. Eq a => a -> a -> Bool
== Char
' ' = Text -> Text
trim (Text -> Text
T.init Text
s)
  | Bool
otherwise      = Text
s




readDefaults :: P.ReaderOptions
readDefaults :: ReaderOptions
readDefaults = forall a. Default a => a
P.def { readerStandalone :: Bool
P.readerStandalone = Bool
True,
                       readerExtensions :: Extensions
P.readerExtensions = Extensions
P.pandocExtensions }

parseBlocks :: T.Text -> [P.Block]
parseBlocks :: Text -> [Block]
parseBlocks Text
s = forall {a}. Show a => Either a Pandoc -> [Block]
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PandocPure a -> Either PandocError a
P.runPure forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(PandocMonad m, ToSources a) =>
ReaderOptions -> a -> m Pandoc
P.readMarkdown ReaderOptions
readDefaults Text
s
  where f :: Either a Pandoc -> [Block]
f (Right (P.Pandoc Meta
_ [Block]
bs)) = [Block]
bs
        f (Left a
e) = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"readMarkdown failed: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
e

defaultColSpec :: P.ColSpec
defaultColSpec :: ColSpec
defaultColSpec = (Alignment
P.AlignDefault, ColWidth
P.ColWidthDefault)

defaultTableCaption :: P.Caption
defaultTableCaption :: Caption
defaultTableCaption = Maybe [Inline] -> [Block] -> Caption
P.Caption forall a. Maybe a
Nothing []

defaultTableHeader :: P.TableHead
defaultTableHeader :: TableHead
defaultTableHeader = (Text, [Text], [(Text, Text)]) -> [Row] -> TableHead
P.TableHead (Text, [Text], [(Text, Text)])
P.nullAttr []

defaultTableFooter :: P.TableFoot
defaultTableFooter :: TableFoot
defaultTableFooter = (Text, [Text], [(Text, Text)]) -> [Row] -> TableFoot
P.TableFoot (Text, [Text], [(Text, Text)])
P.nullAttr []