{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Language.Rzk.Syntax (
  module Language.Rzk.Syntax.Abs,

  parseModuleSafe,
  parseModule,
  parseModuleRzk,
  parseModuleFile,
  parseTerm,
  Print.Print(..), printTree,
  tryExtractMarkdownCodeBlocks,
  extractMarkdownCodeBlocks,
  tryOrDisplayException,
  tryOrDisplayExceptionIO,
) where

import           Control.Exception          (Exception (..), SomeException,
                                             evaluate, try)

import           Data.Char                  (isSpace)
import qualified Data.List                  as List

import           Language.Rzk.Syntax.Abs
import qualified Language.Rzk.Syntax.Print  as Print

import           Language.Rzk.Syntax.Layout (resolveLayout)
import           Language.Rzk.Syntax.Lex    (tokens)
import           Language.Rzk.Syntax.Par    (pModule, pTerm)

tryOrDisplayException :: Either String a -> IO (Either String a)
tryOrDisplayException :: forall a. Either String a -> IO (Either String a)
tryOrDisplayException = forall a. IO (Either String a) -> IO (Either String a)
tryOrDisplayExceptionIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> IO a
evaluate

tryOrDisplayExceptionIO :: IO (Either String a) -> IO (Either String a)
tryOrDisplayExceptionIO :: forall a. IO (Either String a) -> IO (Either String a)
tryOrDisplayExceptionIO IO (Either String a)
x =
  forall e a. Exception e => IO a -> IO (Either e a)
try IO (Either String a)
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Left (SomeException
ex :: SomeException) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left (forall e. Exception e => e -> String
displayException SomeException
ex))
    Right Either String a
result               -> forall (m :: * -> *) a. Monad m => a -> m a
return Either String a
result

parseModuleSafe :: String -> IO (Either String Module)
parseModuleSafe :: String -> IO (Either String Module)
parseModuleSafe = forall a. Either String a -> IO (Either String a)
tryOrDisplayException forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Either String Module
parseModule

parseModule :: String -> Either String Module
parseModule :: String -> Either String Module
parseModule = [Token] -> Either String Module
pModule forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> [Token] -> [Token]
resolveLayout Bool
True forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Token]
tokens forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
tryExtractMarkdownCodeBlocks String
"rzk"

parseModuleRzk :: String -> Either String Module
parseModuleRzk :: String -> Either String Module
parseModuleRzk = [Token] -> Either String Module
pModule forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> [Token] -> [Token]
resolveLayout Bool
True forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Token]
tokens

parseModuleFile :: FilePath -> IO (Either String Module)
parseModuleFile :: String -> IO (Either String Module)
parseModuleFile String
path = do
  String
source <- String -> IO String
readFile String
path
  String -> IO (Either String Module)
parseModuleSafe String
source

parseTerm :: String -> Either String Term
parseTerm :: String -> Either String Term
parseTerm = [Token] -> Either String Term
pTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Token]
tokens

tryExtractMarkdownCodeBlocks :: String -> String -> String
tryExtractMarkdownCodeBlocks :: String -> String -> String
tryExtractMarkdownCodeBlocks String
alias String
input
  | (String
"```" forall a. Semigroup a => a -> a -> a
<> String
alias forall a. Semigroup a => a -> a -> a
<> String
"\n") forall a. Eq a => [a] -> [a] -> Bool
`List.isInfixOf` String
input = String -> String -> String
extractMarkdownCodeBlocks String
alias String
input
  | Bool
otherwise = String
input

data LineType = NonCode | CodeOf String

-- | Extract code for a given alias (e.g. "rzk" or "haskell") from a Markdown file
-- by replacing any lines that do not belong to the code in that language with blank lines.
-- This way the line numbers are preserved correctly from the original file.
--
-- All of the following notations are supported to start a code block:
--
-- * @```rzk@
-- * @```{.rzk title=\"Example\"}@
-- * @``` { .rzk title=\"Example\" }@
--
-- >>> example = "Example:\n```rzk\n#lang rzk-1\n```\nasd asd\n```rzk\n#def x : U\n  := U\n``` \nasda"
-- >>> putStrLn example
-- Example:
-- ```rzk
-- #lang rzk-1
-- ```
-- asd asd
-- ```rzk
-- #def x : U
--   := U
-- ```
-- asda
-- >>> putStrLn $ extractMarkdownCodeBlocks "rzk" example
-- <BLANKLINE>
-- <BLANKLINE>
-- #lang rzk-1
-- <BLANKLINE>
-- <BLANKLINE>
-- <BLANKLINE>
-- #def x : U
--   := U
-- <BLANKLINE>
-- <BLANKLINE>
-- <BLANKLINE>
extractMarkdownCodeBlocks :: String -> String -> String
extractMarkdownCodeBlocks :: String -> String -> String
extractMarkdownCodeBlocks String
alias = [String] -> String
unlines forall b c a. (b -> c) -> (a -> b) -> a -> c
. LineType -> [String] -> [String]
blankNonCode LineType
NonCode forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map String -> String
trim forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines
  where
    blankNonCode :: LineType -> [String] -> [String]
blankNonCode LineType
_prevType [] = []
    blankNonCode LineType
prevType (String
line : [String]
lines_) =
      case LineType
prevType of
        CodeOf String
lang
          | String
line forall a. Eq a => a -> a -> Bool
== String
"```" -> String
"" forall a. a -> [a] -> [a]
: LineType -> [String] -> [String]
blankNonCode LineType
NonCode [String]
lines_
          | String
lang forall a. Eq a => a -> a -> Bool
== String
alias -> String
line forall a. a -> [a] -> [a]
: LineType -> [String] -> [String]
blankNonCode LineType
prevType [String]
lines_
          | Bool
otherwise     -> String
""   forall a. a -> [a] -> [a]
: LineType -> [String] -> [String]
blankNonCode LineType
prevType [String]
lines_
        LineType
NonCode -> String
"" forall a. a -> [a] -> [a]
: LineType -> [String] -> [String]
blankNonCode (String -> LineType
identifyCodeBlockStart String
line) [String]
lines_

    trim :: String -> String
trim = forall a. (a -> Bool) -> [a] -> [a]
List.dropWhileEnd Char -> Bool
isSpace

identifyCodeBlockStart :: String -> LineType
identifyCodeBlockStart :: String -> LineType
identifyCodeBlockStart String
line
  | String
prefix forall a. Eq a => a -> a -> Bool
== String
"```" =
      case String -> [String]
words String
suffix of
        []                          -> String -> LineType
CodeOf String
"text" -- default to text
        (Char
'{':Char
'.':String
lang) : [String]
_options   -> String -> LineType
CodeOf String
lang   -- ``` {.rzk ...
        String
"{" : (Char
'.':String
lang) : [String]
_options -> String -> LineType
CodeOf String
lang   -- ``` { .rzk ...
        String
lang : [String]
_options             -> String -> LineType
CodeOf String
lang   -- ```rzk ...
  | Bool
otherwise = LineType
NonCode
  where
    (String
prefix, String
suffix) = forall a. Int -> [a] -> ([a], [a])
List.splitAt Int
3 String
line

-- * Overriding BNFC pretty-printer

-- | Like 'Print.printTree', but does not insert newlines for curly braces.
printTree :: Print.Print a => a -> String
printTree :: forall a. Print a => a -> String
printTree = Doc -> String
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Print a => Int -> a -> Doc
Print.prt Int
0

-- | Like 'Print.render', but does not insert newlines for curly braces.
render :: Print.Doc -> String
render :: Doc -> String
render Doc
d = Int -> Bool -> [String] -> String -> String
rend Int
0 Bool
False (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a -> b) -> a -> b
$ String
"") forall a b. (a -> b) -> a -> b
$ Doc
d []) String
""
  where
  rend
    :: Int        -- ^ Indentation level.
    -> Bool       -- ^ Pending indentation to be output before next character?
    -> [String]
    -> ShowS
  rend :: Int -> Bool -> [String] -> String -> String
rend Int
i Bool
p = \case
      String
"["      :[String]
ts -> Char -> String -> String
char Char
'[' forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bool -> [String] -> String -> String
rend Int
i Bool
False [String]
ts
      String
"("      :[String]
ts -> Char -> String -> String
char Char
'(' forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bool -> [String] -> String -> String
rend Int
i Bool
False [String]
ts
      -- "{"      :ts -> onNewLine i     p . showChar   '{'  . new (i+1) ts
      -- "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts
      -- "}"      :ts -> onNewLine (i-1) p . showChar   '}'  . new (i-1) ts
      [String
";"]        -> Char -> String -> String
char Char
';'
      String
";"      :[String]
ts -> Char -> String -> String
char Char
';' forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [String] -> String -> String
new Int
i [String]
ts
      String
t  : ts :: [String]
ts@(String
s:[String]
_) | String -> Bool
closingOrPunctuation String
s
                   -> String -> String
pending forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bool -> [String] -> String -> String
rend Int
i Bool
False [String]
ts
      String
t        :[String]
ts -> String -> String
pending forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
space String
t      forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bool -> [String] -> String -> String
rend Int
i Bool
False [String]
ts
      []           -> forall a. a -> a
id
    where
    -- Output character after pending indentation.
    char :: Char -> ShowS
    char :: Char -> String -> String
char Char
c = String -> String
pending forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> String -> String
showChar Char
c

    -- Output pending indentation.
    pending :: ShowS
    pending :: String -> String
pending = if Bool
p then Int -> String -> String
indent Int
i else forall a. a -> a
id

  -- Indentation (spaces) for given indentation level.
  indent :: Int -> ShowS
  indent :: Int -> String -> String
indent Int
i = Int -> (String -> String) -> String -> String
Print.replicateS (Int
2forall a. Num a => a -> a -> a
*Int
i) (Char -> String -> String
showChar Char
' ')

  -- Continue rendering in new line with new indentation.
  new :: Int -> [String] -> ShowS
  new :: Int -> [String] -> String -> String
new Int
j [String]
ts = Char -> String -> String
showChar Char
'\n' forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bool -> [String] -> String -> String
rend Int
j Bool
True [String]
ts

  -- -- Make sure we are on a fresh line.
  -- onNewLine :: Int -> Bool -> ShowS
  -- onNewLine i p = (if p then id else showChar '\n') . indent i

  -- Separate given string from following text by a space (if needed).
  space :: String -> ShowS
  space :: String -> String -> String
space String
t String
s =
    case (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace String
t, forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
spc, forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
rest) of
      (Bool
True , Bool
_   , Bool
True ) -> []             -- remove trailing space
      (Bool
False, Bool
_   , Bool
True ) -> String
t              -- remove trailing space
      (Bool
False, Bool
True, Bool
False) -> String
t forall a. [a] -> [a] -> [a]
++ Char
' ' forall a. a -> [a] -> [a]
: String
s   -- add space if none
      (Bool, Bool, Bool)
_                    -> String
t forall a. [a] -> [a] -> [a]
++ String
s
    where
      (String
spc, String
rest) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isSpace String
s

  closingOrPunctuation :: String -> Bool
  closingOrPunctuation :: String -> Bool
closingOrPunctuation [Char
c] = Char
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
closerOrPunct
  closingOrPunctuation String
_   = Bool
False

  closerOrPunct :: String
  closerOrPunct :: String
closerOrPunct = String
")],;"