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

  parseModuleSafe,
  parseModule,
  parseModuleRzk,
  parseModuleFile,
  parseTerm,
  resolveLayout,
  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.Layout as Layout
import qualified Language.Rzk.Syntax.Print  as Print

import           Language.Rzk.Syntax.Lex    (tokens, Token)
import           Language.Rzk.Syntax.Par    (pModule, pTerm)
import GHC.IO (unsafePerformIO)

tryOrDisplayException :: Either String a -> IO (Either String a)
tryOrDisplayException :: forall a. Either String a -> IO (Either String a)
tryOrDisplayException = IO (Either String a) -> IO (Either String a)
forall a. IO (Either String a) -> IO (Either String a)
tryOrDisplayExceptionIO (IO (Either String a) -> IO (Either String a))
-> (Either String a -> IO (Either String a))
-> Either String a
-> IO (Either String a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either String a -> IO (Either String a)
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 =
  IO (Either String a) -> IO (Either SomeException (Either String a))
forall e a. Exception e => IO a -> IO (Either e a)
try IO (Either String a)
x IO (Either SomeException (Either String a))
-> (Either SomeException (Either String a) -> IO (Either String a))
-> IO (Either String a)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Left (SomeException
ex :: SomeException) -> Either String a -> IO (Either String a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Either String a
forall a b. a -> Either a b
Left (SomeException -> String
forall e. Exception e => e -> String
displayException SomeException
ex))
    Right Either String a
result               -> Either String a -> IO (Either String a)
forall a. a -> IO a
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 = Either String Module -> IO (Either String Module)
forall a. Either String a -> IO (Either String a)
tryOrDisplayException (Either String Module -> IO (Either String Module))
-> (String -> Either String Module)
-> String
-> IO (Either String Module)
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 ([Token] -> Either String Module)
-> (String -> [Token]) -> String -> Either String Module
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> [Token] -> [Token]
Layout.resolveLayout Bool
True ([Token] -> [Token]) -> (String -> [Token]) -> String -> [Token]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Token]
tokens (String -> [Token]) -> (String -> String) -> String -> [Token]
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 ([Token] -> Either String Module)
-> (String -> [Token]) -> String -> Either String Module
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> [Token] -> [Token]
Layout.resolveLayout Bool
True ([Token] -> [Token]) -> (String -> [Token]) -> String -> [Token]
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 ([Token] -> Either String Term)
-> (String -> [Token]) -> String -> Either String Term
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
"```" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
alias String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n") String -> String -> Bool
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 ([String] -> String) -> (String -> [String]) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LineType -> [String] -> [String]
blankNonCode LineType
NonCode ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
trim ([String] -> [String])
-> (String -> [String]) -> String -> [String]
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 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"```" -> String
"" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: LineType -> [String] -> [String]
blankNonCode LineType
NonCode [String]
lines_
          | String
lang String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
alias -> String
line String -> [String] -> [String]
forall a. a -> [a] -> [a]
: LineType -> [String] -> [String]
blankNonCode LineType
prevType [String]
lines_
          | Bool
otherwise     -> String
""   String -> [String] -> [String]
forall a. a -> [a] -> [a]
: LineType -> [String] -> [String]
blankNonCode LineType
prevType [String]
lines_
        LineType
NonCode -> String
"" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: LineType -> [String] -> [String]
blankNonCode (String -> LineType
identifyCodeBlockStart String
line) [String]
lines_

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

identifyCodeBlockStart :: String -> LineType
identifyCodeBlockStart :: String -> LineType
identifyCodeBlockStart String
line
  | String
prefix String -> String -> Bool
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) = Int -> String -> (String, String)
forall a. Int -> [a] -> ([a], [a])
List.splitAt Int
3 String
line

-- * Making BNFC resolveLayout safer

-- | Replace layout syntax with explicit layout tokens.
resolveLayout
  :: Bool      -- ^ Whether to use top-level layout.
  -> [Token]   -- ^ Token stream before layout resolution.
  -> Either String [Token]   -- ^ Token stream after layout resolution.
resolveLayout :: Bool -> [Token] -> Either String [Token]
resolveLayout Bool
isTopLevel [Token]
toks = IO (Either String [Token]) -> Either String [Token]
forall a. IO a -> a
unsafePerformIO (IO (Either String [Token]) -> Either String [Token])
-> IO (Either String [Token]) -> Either String [Token]
forall a b. (a -> b) -> a -> b
$ do
  -- NOTE: we use (length . show) as poor man's Control.DeepSeq.force
  -- NOTE: this is required to force all resolveLayout error's to come out
  IO Int -> IO (Either SomeException Int)
forall e a. Exception e => IO a -> IO (Either e a)
try (Int -> IO Int
forall a. a -> IO a
evaluate (String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Token] -> String
forall a. Show a => a -> String
show [Token]
resolvedToks))) IO (Either SomeException Int)
-> (Either SomeException Int -> IO (Either String [Token]))
-> IO (Either String [Token])
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Left (SomeException
err :: SomeException) -> Either String [Token] -> IO (Either String [Token])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Either String [Token]
forall a b. a -> Either a b
Left (SomeException -> String
forall e. Exception e => e -> String
displayException SomeException
err))
    Right Int
_ -> Either String [Token] -> IO (Either String [Token])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Token] -> Either String [Token]
forall a b. b -> Either a b
Right [Token]
resolvedToks)
  where
    resolvedToks :: [Token]
resolvedToks = Bool -> [Token] -> [Token]
Layout.resolveLayout Bool
isTopLevel [Token]
toks

-- * 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 (Doc -> String) -> (a -> Doc) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> Doc
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 (((String -> String) -> String) -> [String -> String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"") ([String -> String] -> [String]) -> [String -> String] -> [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
'[' (String -> String) -> (String -> String) -> String -> String
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
'(' (String -> String) -> (String -> String) -> String -> String
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
';' (String -> String) -> (String -> String) -> String -> String
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 (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
t (String -> String) -> (String -> String) -> String -> String
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 (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
space String
t      (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bool -> [String] -> String -> String
rend Int
i Bool
False [String]
ts
      []           -> String -> String
forall a. a -> a
id
    where
    -- Output character after pending indentation.
    char :: Char -> ShowS
    char :: Char -> String -> String
char Char
c = String -> String
pending (String -> String) -> (String -> String) -> String -> String
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 String -> String
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
2Int -> Int -> Int
forall 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' (String -> String) -> (String -> String) -> String -> String
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 ((Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace String
t, String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
spc, String -> Bool
forall a. [a] -> Bool
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 String -> String -> String
forall a. [a] -> [a] -> [a]
++ Char
' ' Char -> String -> String
forall a. a -> [a] -> [a]
: String
s   -- add space if none
      (Bool, Bool, Bool)
_                    -> String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
    where
      (String
spc, String
rest) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isSpace String
s

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

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