Data.Type.Symbol.Natural

Parse Naturals from type-level Symbols.

The type functions here may return errors. Use the provided and throw with TypeError, or wrap in your own error handling.

TODO

• Oh dear. Oh dear. Oh dear. If I want to get proper working composition with meaningful errors, where the index pays attention to what we Drop... then I need to write a type-level parser monad. That's it. These parsers need to take in parser state (well, just character index is OK), and emit that state on success. Oh dear. Oh no.

Documentation

type ParseBinarySymbol sym = ParseSymbolDigits 2 ParseBinaryDigitSym sym

Parse a Symbol describing a binary (base 2) natural to its Natural value.

type ParseOctalSymbol sym = ParseSymbolDigits 8 ParseOctalDigitSym sym

Parse a Symbol describing an octal (base 8) natural to its Natural value.

type ParseDecimalSymbol sym = ParseSymbolDigits 10 ParseDecimalDigitSym sym

Parse a Symbol describing a decimal (base 10) natural to its Natural value.

type ParseHexSymbol sym = ParseSymbolDigits 16 ParseHexDigitSym sym

Parse a Symbol describing a hexadecimal (base 16) natural to its Natural value.

type family PrettyE e where ...

Equations

PrettyE 'EEmptySymbol = 'Text "empty symbol"

PrettyE ('EBadDigit base ch idx) = PrettyEBadDigit base ch idx

type family MapLeftPrettyE e where ...

Equations

MapLeftPrettyE ('Right a) = 'Right a

MapLeftPrettyE ('Left e) = 'Left (PrettyE e)

type family FromRightParseResult sym eab where ...

Equations

FromRightParseResult _ ('Right a) = a

FromRightParseResult sym ('Left e) = TypeError (('Text "error while parsing symbol: " :<>: 'Text sym) :$$: PrettyE e)

data E

Constructors

EBadDigit Natural Char Natural

EEmptySymbol

type PrettyEBadDigit base ch idx = (('Text "could not parse character as base " :<>: 'ShowType base) :<>: 'Text " digit") :$$: (('ShowType ch :<>: 'Text " at index ") :<>: 'ShowType idx)

type ParseSymbolDigits base tfDigitValue sym = If (Length sym == 0) ('Left 'EEmptySymbol) (WrapEBadDigit base (ParseSymbolDigits' base tfDigitValue ('Just 0) '\NUL' 0 (Length sym - 1) (UnconsSymbol sym)))

Parse a symbol to a Natural using the given base and digit parser.

type family WrapEBadDigit base eab where ...

Equations

WrapEBadDigit _ ('Right b) = 'Right b

WrapEBadDigit base ('Left '(ch, sym)) = 'Left ('EBadDigit base ch sym)

type family ParseSymbolDigits' base tfParseDigit mn prevCh idx expo mchsym where ...

Equations

ParseSymbolDigits' base tfParseDigit ('Just n) prevCh idx expo 'Nothing = 'Right n

ParseSymbolDigits' base tfParseDigit 'Nothing prevCh idx expo mchsym = 'Left '(prevCh, idx - 1)

ParseSymbolDigits' base tfParseDigit ('Just n) prevCh idx expo ('Just '(ch, sym)) = ParseSymbolDigits' base tfParseDigit (ParseSymbolDigits'Inc (base ^ expo) n (tfParseDigit @@ ch)) ch (idx + 1) (expo - 1) (UnconsSymbol sym)

type family ParseSymbolDigits'Inc mult n mDigit where ...

Equations

ParseSymbolDigits'Inc mult n 'Nothing = 'Nothing

ParseSymbolDigits'Inc mult n ('Just digit) = 'Just (n + (digit * mult))

data ParseBinaryDigitSym a

Instances

type App ParseBinaryDigitSym (a :: Char)

Defined in Data.Type.Symbol.Natural

type App ParseBinaryDigitSym (a :: Char) = ParseBinaryDigit a

data ParseOctalDigitSym a

Instances

type App ParseOctalDigitSym (a :: Char)

Defined in Data.Type.Symbol.Natural

type App ParseOctalDigitSym (a :: Char) = ParseOctalDigit a

data ParseDecimalDigitSym a

Instances

type App ParseDecimalDigitSym (a :: Char)

Defined in Data.Type.Symbol.Natural

type App ParseDecimalDigitSym (a :: Char) = ParseDecimalDigit a

data ParseHexDigitSym a

Instances

type App ParseHexDigitSym (a :: Char)

Defined in Data.Type.Symbol.Natural

type App ParseHexDigitSym (a :: Char) = ParseHexDigit a