Parser.Rule.Source

Reexports

Definitions

record ParserState : (Type -> Type) -> Type

  This version of the Parser's state is parameterized over
  the container for SemanticDecorations. The parser should
  only work the ParsingState type below and after parsing
  is complete, use the regular State type.

Totality: total
Visibility: public export
Constructor: 

MkState : container ASemanticDecoration -> List String -> ParserState container

Projections:

.decorations : ParserState container -> container ASemanticDecoration

.holeNames : ParserState container -> List String

.decorations : ParserState container -> container ASemanticDecoration

Totality: total
Visibility: public export

decorations : ParserState container -> container ASemanticDecoration

Totality: total
Visibility: public export

.holeNames : ParserState container -> List String

Totality: total
Visibility: public export

holeNames : ParserState container -> List String

Totality: total
Visibility: public export

ParsingState : Type

  This state needs to provide efficient concatenation.

Totality: total
Visibility: public export

State : Type

  This is the final state after parsing. We no longer
  need to support efficient concatenation.

Totality: total
Visibility: public export

toState : ParsingState -> State

Totality: total
Visibility: export

BRule : Bool -> Type -> Type

Totality: total
Visibility: public export

Rule : Type -> Type

Totality: total
Visibility: public export

EmptyRule : Type -> Type

Totality: total
Visibility: public export

actD : ASemanticDecoration -> EmptyRule ()

Totality: total
Visibility: export

actH : String -> EmptyRule ()

Totality: total
Visibility: export

debugInfo : Rule DebugInfo

Totality: total
Visibility: export

eoi : EmptyRule ()

Totality: total
Visibility: export

constant : Rule Constant

Totality: total
Visibility: export

decorationFromBounded : OriginDesc -> Decoration -> WithBounds a -> ASemanticDecoration

Totality: total
Visibility: export

optDocumentation : OriginDesc -> EmptyRule String

Totality: total
Visibility: export

intLit : Rule Integer

Totality: total
Visibility: export

onOffLit : Rule Bool

Totality: total
Visibility: export

simpleStrLit : Rule String

Totality: total
Visibility: export

strLitLines : Rule (List1 String)

  String literal split by line wrap (not striped).

Totality: total
Visibility: export

strBegin : Rule Nat

Totality: total
Visibility: export

multilineBegin : Rule Nat

Totality: total
Visibility: export

strEnd : Rule ()

Totality: total
Visibility: export

interpBegin : Rule ()

Totality: total
Visibility: export

interpEnd : Rule ()

Totality: total
Visibility: export

simpleStr : Rule String

Totality: total
Visibility: export

simpleMultiStr : Rule String

Totality: total
Visibility: export

aDotIdent : Rule String

Totality: total
Visibility: export

postfixProj : Rule Name

Totality: total
Visibility: export

symbol : String -> Rule ()

Totality: total
Visibility: export

anyReservedSymbol : Rule String

Totality: total
Visibility: export

anyKeyword : Rule String

Totality: total
Visibility: export

keyword : String -> Rule ()

Totality: total
Visibility: export

exactIdent : String -> Rule ()

Totality: total
Visibility: export

pragma : String -> Rule ()

Totality: total
Visibility: export

cgDirective : Rule String

Totality: total
Visibility: export

builtinType : Rule BuiltinType

Totality: total
Visibility: export

unqualifiedOperatorName : Rule String

Totality: total
Visibility: export

operator : Rule Name

Totality: total
Visibility: export

namespacedIdent : Rule (Maybe Namespace, String)

Totality: total
Visibility: export

namespaceId : Rule Namespace

Totality: total
Visibility: export

namespacedSymbol : String -> Rule (Maybe Namespace)

Totality: total
Visibility: export

moduleIdent : Rule ModuleIdent

Totality: total
Visibility: export

unqualifiedName : Rule String

Totality: total
Visibility: export

userName : Rule Name

Totality: total
Visibility: export

holeName : Rule String

Totality: total
Visibility: export

anyReservedIdent : Rule (WithBounds String)

Totality: total
Visibility: export

opNonNS : Rule Name

Totality: total
Visibility: export

fixityNS : Rule HidingDirective

Totality: total
Visibility: export

name : Rule Name

Totality: total
Visibility: export

capitalisedName : Rule Name

Totality: total
Visibility: export

capitalisedIdent : Rule String

Totality: total
Visibility: export

dataConstructorName : Rule Name

Totality: total
Visibility: export

dataTypeName : Rule Name

Totality: total
Visibility: export

IndentInfo : Type

Totality: total
Visibility: export

init : IndentInfo

Totality: total
Visibility: export

continue : IndentInfo -> EmptyRule ()

  Fail if this is the end of a block entry or end of file

Totality: total
Visibility: export

mustContinue : IndentInfo -> Maybe String -> EmptyRule ()

  As 'continue' but failing is fatal (i.e. entire parse fails)

Totality: total
Visibility: export

atEnd : IndentInfo -> EmptyRule ()

  Check we're at the end of a block entry, given the start column
  of the block.
  It's the end if we have a terminating token, or the next token starts
  in or before indent. Works by looking ahead but not consuming.

Totality: total
Visibility: export

atEndIndent : IndentInfo -> EmptyRule ()

Totality: total
Visibility: export

block : (IndentInfo -> Rule ty) -> EmptyRule (List ty)

Totality: total
Visibility: export

blockAfter : Int -> (IndentInfo -> Rule ty) -> EmptyRule (List ty)

  `blockAfter col rule` parses a `rule`-block indented by at
  least `col` spaces (unless the block is explicitly delimited
  by curly braces). `rule` is a function of the actual indentation
  level.

Totality: total
Visibility: export

blockWithOptHeaderAfter : Int -> (IndentInfo -> Rule hd) -> (IndentInfo -> Rule ty) -> EmptyRule (Maybe hd, List ty)

Totality: total
Visibility: export

nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List1 ty)

Totality: total
Visibility: export

nonEmptyBlockAfter : Int -> (IndentInfo -> Rule ty) -> Rule (List1 ty)

  `nonEmptyBlockAfter col rule` parses a non-empty `rule`-block indented
  by at least `col` spaces (unless the block is explicitly delimited
  by curly braces). `rule` is a function of the actual indentation
  level.

Totality: total
Visibility: export