rzk-0.7.5: An experimental proof assistant for synthetic ∞-categories
Safe HaskellNone
LanguageHaskell2010

Language.Rzk.Syntax.Layout

Synopsis

Documentation

data LayoutDelimiters Source #

Constructors

LayoutDelimiters 

Fields

layoutError Source #

Arguments

:: [Token]

Remaining tokens.

-> String

Error message.

-> a 

Report an error during layout resolution.

resolveLayout Source #

Arguments

:: Bool

Whether to use top-level layout.

-> [Token]

Token stream before layout resolution.

-> [Token]

Token stream after layout resolution.

Replace layout syntax with explicit layout tokens.

type Line = Int Source #

data Block Source #

Entry of the layout stack.

Constructors

Implicit LayoutDelimiters Status Column

An implicit layout block with its start column.

Explicit 

indentation :: Block -> Column Source #

Get current indentation. 0 if we are in an explicit block.

isImplicit :: Block -> Bool Source #

Check if s block is implicit.

data Status Source #

Constructors

Tentative

A layout column that has not been confirmed by a line break

Definitive

A layout column that has been confirmed by a line break.

addImplicit Source #

Arguments

:: LayoutDelimiters

Delimiters of the new block.

-> Position

Position of the layout keyword.

-> Position

Position of the token following the layout keword.

-> [Block] 
-> [Block] 

Add a new implicit layout block.

confirm :: Column -> [Block] -> [Block] Source #

Confirm tentative blocks that are not more indented than col.

afterPrev :: Maybe Token -> Position Source #

Get the position immediately to the right of the given token. If no token is given, gets the first position in the file.

nextPos :: Token -> Position Source #

Get the position immediately to the right of the given token.

tokenLength :: Token -> Int Source #

Get the number of characters in the token.

sToken :: Position -> TokSymbol -> Token Source #

Create a position symbol token.

line :: Token -> Line Source #

Get the line number of a token.

column :: Token -> Column Source #

Get the column number of a token.

newLine :: Maybe Token -> Token -> Bool Source #

Is the following token on a new line?

isLayout :: Token -> Maybe LayoutDelimiters Source #

Check if a word is a layout start token.

isTokenIn :: [TokSymbol] -> Token -> Bool Source #

Check if a token is one of the given symbols.

isStop :: Token -> Bool Source #

Check if a token is a layout stop token.

isLayoutOpen :: Token -> Bool Source #

Check if a token is the layout open token.

isLayoutSep :: Token -> Bool Source #

Check if a token is the layout separator token.

isLayoutClose :: Token -> Bool Source #

Check if a token is the layout close token.

isParenOpen :: Token -> Bool Source #

Check if a token is an opening parenthesis.

isParenClose :: Token -> Bool Source #

Check if a token is a closing parenthesis.