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

Safe Haskell	None
Language	Haskell2010

Language.Rzk.Syntax.Layout

Synopsis

data LayoutDelimiters = LayoutDelimiters {
- delimSep :: TokSymbol
- delimOpen :: Maybe TokSymbol
- delimClose :: Maybe TokSymbol
}
layoutWords :: [(TokSymbol, LayoutDelimiters)]
layoutStopWords :: [TokSymbol]
layoutOpen :: [TokSymbol]
layoutClose :: [TokSymbol]
layoutSep :: [TokSymbol]
parenOpen :: [TokSymbol]
parenClose :: [TokSymbol]
layoutError :: [Token] -> String -> a
resolveLayout :: Bool -> [Token] -> [Token]
type Position = Posn
type Line = Int
type Column = Int
data Block
- = Implicit LayoutDelimiters Status Column
- | Explicit
indentation :: Block -> Column
isImplicit :: Block -> Bool
data Status
- = Tentative
- | Definitive
addImplicit :: LayoutDelimiters -> Position -> Position -> [Block] -> [Block]
confirm :: Column -> [Block] -> [Block]
afterPrev :: Maybe Token -> Position
nextPos :: Token -> Position
tokenLength :: Token -> Int
sToken :: Position -> TokSymbol -> Token
line :: Token -> Line
column :: Token -> Column
newLine :: Maybe Token -> Token -> Bool
isLayout :: Token -> Maybe LayoutDelimiters
isTokenIn :: [TokSymbol] -> Token -> Bool
isStop :: Token -> Bool
isLayoutOpen :: Token -> Bool
isLayoutSep :: Token -> Bool
isLayoutClose :: Token -> Bool
isParenOpen :: Token -> Bool
isParenClose :: Token -> Bool

Documentation

data LayoutDelimiters Source #

Constructors

LayoutDelimiters
Fields delimSep :: TokSymbol delimOpen :: Maybe TokSymbol Nothing for toplevel layout. delimClose :: Maybe TokSymbol Nothing for toplevel layout.

layoutWords :: [(TokSymbol, LayoutDelimiters)] Source #

layoutStopWords :: [TokSymbol] Source #

layoutOpen :: [TokSymbol] Source #

layoutClose :: [TokSymbol] Source #

layoutSep :: [TokSymbol] Source #

parenOpen :: [TokSymbol] Source #

parenClose :: [TokSymbol] Source #

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 Position = Posn Source #

type Line = Int Source #

type Column = 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.