{-# 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 = tryOrDisplayExceptionIO . evaluate tryOrDisplayExceptionIO :: IO (Either String a) -> IO (Either String a) tryOrDisplayExceptionIO x = try x >>= \case Left (ex :: SomeException) -> return (Left (displayException ex)) Right result -> return result parseModuleSafe :: String -> IO (Either String Module) parseModuleSafe = tryOrDisplayException . parseModule parseModule :: String -> Either String Module parseModule = pModule . resolveLayout True . tokens . tryExtractMarkdownCodeBlocks "rzk" parseModuleRzk :: String -> Either String Module parseModuleRzk = pModule . resolveLayout True . tokens parseModuleFile :: FilePath -> IO (Either String Module) parseModuleFile path = do source <- readFile path parseModuleSafe source parseTerm :: String -> Either String Term parseTerm = pTerm . tokens tryExtractMarkdownCodeBlocks :: String -> String -> String tryExtractMarkdownCodeBlocks alias input | ("```" <> alias <> "\n") `List.isInfixOf` input = extractMarkdownCodeBlocks alias input | otherwise = 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 -- -- -- #lang rzk-1 -- -- -- -- #def x : U -- := U -- -- -- extractMarkdownCodeBlocks :: String -> String -> String extractMarkdownCodeBlocks alias = unlines . blankNonCode NonCode . map trim . lines where blankNonCode _prevType [] = [] blankNonCode prevType (line : lines_) = case prevType of CodeOf lang | line == "```" -> "" : blankNonCode NonCode lines_ | lang == alias -> line : blankNonCode prevType lines_ | otherwise -> "" : blankNonCode prevType lines_ NonCode -> "" : blankNonCode (identifyCodeBlockStart line) lines_ trim = List.dropWhileEnd isSpace identifyCodeBlockStart :: String -> LineType identifyCodeBlockStart line | prefix == "```" = case words suffix of [] -> CodeOf "text" -- default to text ('{':'.':lang) : _options -> CodeOf lang -- ``` {.rzk ... "{" : ('.':lang) : _options -> CodeOf lang -- ``` { .rzk ... lang : _options -> CodeOf lang -- ```rzk ... | otherwise = NonCode where (prefix, suffix) = List.splitAt 3 line -- * Overriding BNFC pretty-printer -- | Like 'Print.printTree', but does not insert newlines for curly braces. printTree :: Print.Print a => a -> String printTree = render . Print.prt 0 -- | Like 'Print.render', but does not insert newlines for curly braces. render :: Print.Doc -> String render d = rend 0 False (map ($ "") $ d []) "" where rend :: Int -- ^ Indentation level. -> Bool -- ^ Pending indentation to be output before next character? -> [String] -> ShowS rend i p = \case "[" :ts -> char '[' . rend i False ts "(" :ts -> char '(' . rend i False 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 [";"] -> char ';' ";" :ts -> char ';' . new i ts t : ts@(s:_) | closingOrPunctuation s -> pending . showString t . rend i False ts t :ts -> pending . space t . rend i False ts [] -> id where -- Output character after pending indentation. char :: Char -> ShowS char c = pending . showChar c -- Output pending indentation. pending :: ShowS pending = if p then indent i else id -- Indentation (spaces) for given indentation level. indent :: Int -> ShowS indent i = Print.replicateS (2*i) (showChar ' ') -- Continue rendering in new line with new indentation. new :: Int -> [String] -> ShowS new j ts = showChar '\n' . rend j True 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 t s = case (all isSpace t, null spc, null rest) of (True , _ , True ) -> [] -- remove trailing space (False, _ , True ) -> t -- remove trailing space (False, True, False) -> t ++ ' ' : s -- add space if none _ -> t ++ s where (spc, rest) = span isSpace s closingOrPunctuation :: String -> Bool closingOrPunctuation [c] = c `elem` closerOrPunct closingOrPunctuation _ = False closerOrPunct :: String closerOrPunct = ")],;"