IotaTime.Pattern

Definitions

data PatternError : Type

  A failure encountered while parsing or refining a patterned value.

Totality: total
Visibility: public export
Constructors:

UnexpectedEnd : Integer -> String -> PatternError

UnexpectedCharacter : Integer -> String -> Char -> PatternError

InvalidNumber : Integer -> String -> PatternError

ValueOutOfRange : String -> Integer -> Integer -> Integer -> PatternError

TrailingInput : Integer -> String -> PatternError

InvalidValue : String -> PatternError

PatternParser : Type -> Type

Totality: total
Visibility: public export

record PatternRep : Type -> Type -> Type

  A bidirectional textual representation of a value.
  
  `state` accumulates fields during parsing. `finish` validates that state and
  constructs the value, while `formatPart` projects text from an existing value.

Totality: total
Visibility: export
Constructor: 

MkPattern : state -> (state -> Either PatternError value) -> PatternParser (Either PatternError (state -> state)) -> (value -> String) -> PatternRep state value

Projections:

.finish : PatternRep state value -> state -> Either PatternError value

.formatPart : PatternRep state value -> value -> String

.initialState : PatternRep state value -> state

.parsePart : PatternRep state value -> PatternParser (Either PatternError (state -> state))

Pattern : Type -> Type -> Type

  An opaque bidirectional textual representation of a value.

Totality: total
Visibility: public export

patternInitialState : Pattern state value -> state

Totality: total
Visibility: export

patternFinish : Pattern state value -> state -> Either PatternError value

Totality: total
Visibility: export

patternParsePart : Pattern state value -> PatternParser (Either PatternError (state -> state))

Totality: total
Visibility: export

patternFormatPart : Pattern state value -> value -> String

Totality: total
Visibility: export

record LiteralPatternRep : Type

  Literal text that can be appended to a pattern with `<%`.

Totality: total
Visibility: export
Constructor: 

MkLiteralPattern : String -> LiteralPatternRep

Projection: 

.literalText : LiteralPatternRep -> String

LiteralPattern : Type

  Opaque literal text that can be appended to a pattern with `<%`.

Totality: total
Visibility: public export

string : String -> LiteralPattern

Totality: total
Visibility: public export

char : Char -> LiteralPattern

Totality: total
Visibility: public export

literalField : Pattern state value -> String -> Pattern state value

Totality: total
Visibility: export

(<%) : Pattern state value -> LiteralPattern -> Pattern state value

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 7

pairPattern : (combined -> left) -> (combined -> right) -> (left -> right -> combined) -> Pattern leftState left -> Pattern rightState right -> Pattern (leftState, rightState) combined

Totality: total
Visibility: export

format : Pattern state value -> value -> String

  Format a value using the supplied pattern.

Totality: total
Visibility: public export

parseWith : Pattern state value -> state -> String -> Either PatternError value

  Parse an entire string using an explicit initial field state.
  
  This is useful for partial patterns whose omitted fields should come from
  caller policy rather than the pattern's built-in defaults.

Totality: total
Visibility: public export

parse : Pattern state value -> String -> Either PatternError value

  Parse an entire string using a pattern's default initial state.

Totality: total
Visibility: public export

pSignedInteger : Pattern Integer Integer

  An arbitrary-precision signed decimal integer. Formatting is canonical;
  parsing also accepts leading zeroes and negative zero.

Totality: total
Visibility: public export

numberUpdatePart : (Integer -> state -> state) -> Nat -> Nat -> Integer -> Integer -> PatternParser (Either PatternError (state -> state))

Totality: total
Visibility: export

namedUpdatePart : List (String, field) -> (field -> state -> state) -> PatternParser (Either PatternError (state -> state))

Totality: total
Visibility: export

namedConsumePart : List String -> PatternParser (Either PatternError (state -> state))

Totality: total
Visibility: export

spaceNumberUpdatePart : (Integer -> state -> state) -> Nat -> Integer -> Integer -> PatternParser (Either PatternError (state -> state))

Totality: total
Visibility: export