Safe Haskell	Safe-Inferred
Language	Haskell2010

Language.Rzk.Syntax

Synopsis

module Language.Rzk.Syntax.Abs
parseModuleSafe :: String -> IO (Either String Module)
parseModule :: String -> Either String Module
parseModuleRzk :: String -> Either String Module
parseModuleFile :: FilePath -> IO (Either String Module)
parseTerm :: String -> Either String Term
class Print a where
- prt :: Int -> a -> Doc
printTree :: Print a => a -> String
tryExtractMarkdownCodeBlocks :: String -> String -> String
extractMarkdownCodeBlocks :: String -> String -> String
tryOrDisplayException :: Either String a -> IO (Either String a)
tryOrDisplayExceptionIO :: IO (Either String a) -> IO (Either String a)

Documentation

module Language.Rzk.Syntax.Abs

parseModuleSafe :: String -> IO (Either String Module) Source #

parseModule :: String -> Either String Module Source #

parseModuleRzk :: String -> Either String Module Source #

parseModuleFile :: FilePath -> IO (Either String Module) Source #

parseTerm :: String -> Either String Term Source #

class Print a where Source #

The printer class does the job.

Methods

prt :: Int -> a -> Doc Source #

Instances

Instances details

Print HoleIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> HoleIdentToken -> Doc Source #
Print VarIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> VarIdentToken -> Doc Source #
Print String Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> String -> Doc Source #
Print Integer Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> Integer -> Doc Source #
Print Char Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> Char -> Doc Source #
Print Double Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> Double -> Doc Source #
Print (Command' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> Command' a -> Doc Source #
Print (DeclUsedVars' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> DeclUsedVars' a -> Doc Source #
Print (HoleIdent' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> HoleIdent' a -> Doc Source #
Print (Language' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> Language' a -> Doc Source #
Print (LanguageDecl' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> LanguageDecl' a -> Doc Source #
Print (Module' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> Module' a -> Doc Source #
Print (Param' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> Param' a -> Doc Source #
Print (ParamDecl' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> ParamDecl' a -> Doc Source #
Print (Pattern' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> Pattern' a -> Doc Source #
Print (Restriction' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> Restriction' a -> Doc Source #
Print (SectionName' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> SectionName' a -> Doc Source #
Print (Term' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> Term' a -> Doc Source #
Print (VarIdent' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> VarIdent' a -> Doc Source #
Print [Command' a] Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> [Command' a] -> Doc Source #
Print [Param' a] Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> [Param' a] -> Doc Source #
Print [Pattern' a] Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> [Pattern' a] -> Doc Source #
Print [Restriction' a] Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> [Restriction' a] -> Doc Source #
Print [Term' a] Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> [Term' a] -> Doc Source #
Print [VarIdent' a] Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> [VarIdent' a] -> Doc Source #
Print a => Print [a] Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> [a] -> Doc Source #

printTree :: Print a => a -> String Source #

Like printTree, but does not insert newlines for curly braces.

tryExtractMarkdownCodeBlocks :: String -> String -> String Source #

extractMarkdownCodeBlocks :: String -> String -> String Source #

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

tryOrDisplayException :: Either String a -> IO (Either String a) Source #

tryOrDisplayExceptionIO :: IO (Either String a) -> IO (Either String a) Source #