{-# LANGUAGE UndecidableInstances #-}
module Data.Type.Symbol.Natural where
import Data.Type.Char.Digits
import GHC.TypeLits
import Data.Type.Bool ( type If )
import Data.Type.Equality ( type (==) )
import DeFun.Core ( type (~>), type App, type (@@) )
import Data.Type.Symbol ( type Length )
type ParseBinarySymbol sym = ParseSymbolDigits 2 ParseBinaryDigitSym sym
type ParseOctalSymbol sym = ParseSymbolDigits 8 ParseOctalDigitSym sym
type ParseDecimalSymbol sym = ParseSymbolDigits 10 ParseDecimalDigitSym sym
type ParseHexSymbol sym = ParseSymbolDigits 16 ParseHexDigitSym sym
type family PrettyE e where
PrettyE 'EEmptySymbol = 'Text "empty symbol"
PrettyE ('EBadDigit base ch idx) = PrettyEBadDigit base ch idx
type family MapLeftPrettyE e where
MapLeftPrettyE ('Right a) = 'Right a
MapLeftPrettyE ('Left e) = 'Left (PrettyE e)
type family FromRightParseResult sym eab where
FromRightParseResult _ ('Right a) = a
FromRightParseResult sym ('Left e) = TypeError
( 'Text "error while parsing symbol: " :<>: 'Text sym
:$$: PrettyE e
)
data E = 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) '\0' 0 (Length sym - 1) (UnconsSymbol sym)))
type family WrapEBadDigit base eab where
WrapEBadDigit _ ('Right b) = 'Right b
WrapEBadDigit base ('Left '(ch, sym)) = 'Left ('EBadDigit base ch sym)
type ParseSymbolDigits'
:: Natural
-> (Char ~> Maybe Natural)
-> Maybe Natural
-> Char
-> Natural
-> Natural
-> Maybe (Char, Symbol)
-> Either (Char, Natural) Natural
type family ParseSymbolDigits' base tfParseDigit mn prevCh idx expo mchsym where
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
ParseSymbolDigits'Inc mult n 'Nothing = 'Nothing
ParseSymbolDigits'Inc mult n ('Just digit) = 'Just (n + digit*mult)
type ParseBinaryDigitSym :: Char ~> Maybe Natural
data ParseBinaryDigitSym a
type instance App ParseBinaryDigitSym a = ParseBinaryDigit a
type ParseOctalDigitSym :: Char ~> Maybe Natural
data ParseOctalDigitSym a
type instance App ParseOctalDigitSym a = ParseOctalDigit a
type ParseDecimalDigitSym :: Char ~> Maybe Natural
data ParseDecimalDigitSym a
type instance App ParseDecimalDigitSym a = ParseDecimalDigit a
type ParseHexDigitSym :: Char ~> Maybe Natural
data ParseHexDigitSym a
type instance App ParseHexDigitSym a = ParseHexDigit a