rzk-0.7.4: An experimental proof assistant for synthetic ∞-categories
Safe HaskellSafe-Inferred
LanguageHaskell2010

Language.Rzk.Syntax

Synopsis

Documentation

resolveLayout Source #

Arguments

:: Bool

Whether to use top-level layout.

-> [Token]

Token stream before layout resolution.

-> Either String [Token]

Token stream after layout resolution.

Replace layout syntax with explicit layout tokens.

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.

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