{-# LANGUAGE UndecidableInstances #-}

module Symparsec.Parser.Natural where

import Symparsec.Parser.Common
import Symparsec.Parser.Natural.Digits
import DeFun.Core
import GHC.TypeLits hiding ( ErrorMessage(..) )
import TypeLevelShow.Natural ( ShowNatDec, sShowNatDec )
import Singleraeh.Maybe
import Singleraeh.Either
import Singleraeh.Natural

-- | Parse a binary (base 2) natural.
type NatBin = NatBase  2 ParseDigitBinSym

-- | Parse an octal (base 8) natural.
type NatOct = NatBase  8 ParseDigitOctSym

-- | Parse a decimal (base 10) natural.
type NatDec = NatBase 10 ParseDigitDecSym

-- | Parse a hexadecimal (base 16) natural. Permits mixed-case (@0-9A-Fa-f@).
type NatHex = NatBase 16 ParseDigitHexSym

-- | Parse a natural in the given base, using the given digit parser.
type NatBase
    :: Natural -> (Char ~> Maybe Natural) -> PParser (Maybe Natural) Natural
type NatBase base parseDigit =
    'PParser (NatBaseChSym base parseDigit) NatBaseEndSym Nothing

sNatBase
    :: SNat base
    -> SParseDigit parseDigit
    -> SParser (SMaybe SNat) SNat (NatBase base parseDigit)
sNatBase :: forall (base :: Nat) (parseDigit :: Char ~> Maybe Nat).
SNat base
-> SParseDigit parseDigit
-> SParser (SMaybe SNat) SNat (NatBase base parseDigit)
sNatBase SNat base
base SParseDigit parseDigit
parseDigit =
    SParserChSym (SMaybe SNat) SNat (NatBaseChSym base parseDigit)
-> SParserEndSym (SMaybe SNat) SNat NatBaseEndSym
-> SMaybe SNat 'Nothing
-> SParser
     (SMaybe SNat)
     SNat
     ('PParser (NatBaseChSym base parseDigit) NatBaseEndSym 'Nothing)
forall {s} {r} (ss :: s -> Type) (sr :: r -> Type)
       (pCh :: ParserChSym s r) (pEnd :: ParserEndSym s r) (s0 :: s).
SParserChSym ss sr pCh
-> SParserEndSym ss sr pEnd
-> ss s0
-> SParser ss sr ('PParser pCh pEnd s0)
SParser (SNat base
-> SParseDigit parseDigit
-> SParserChSym (SMaybe SNat) SNat (NatBaseChSym base parseDigit)
forall (base :: Nat) (parseDigit :: Char ~> Maybe Nat).
SNat base
-> SParseDigit parseDigit
-> SParserChSym (SMaybe SNat) SNat (NatBaseChSym base parseDigit)
sNatBaseChSym SNat base
base SParseDigit parseDigit
parseDigit) SParserEndSym (SMaybe SNat) SNat NatBaseEndSym
sNatBaseEndSym SMaybe SNat 'Nothing
forall {a} (sa :: a -> Type). SMaybe sa 'Nothing
SNothing

instance (KnownNat base, SingParseDigit parseDigit)
  => SingParser (NatBase base parseDigit) where
    type PS (NatBase base parseDigit) = SMaybe SNat
    type PR (NatBase base parseDigit) = SNat
    singParser' :: SParser
  (PS (NatBase base parseDigit))
  (PR (NatBase base parseDigit))
  (NatBase base parseDigit)
singParser' = SNat base
-> SParseDigit parseDigit
-> SParser (SMaybe SNat) SNat (NatBase base parseDigit)
forall (base :: Nat) (parseDigit :: Char ~> Maybe Nat).
SNat base
-> SParseDigit parseDigit
-> SParser (SMaybe SNat) SNat (NatBase base parseDigit)
sNatBase SNat base
forall (n :: Nat). KnownNat n => SNat n
natSing SParseDigit parseDigit
forall (parseDigit :: Char ~> Maybe Nat).
SingParseDigit parseDigit =>
SParseDigit parseDigit
singParseDigit

type NatBaseCh
    :: Natural
    -> (Char ~> Maybe Natural)
    -> PParserCh (Maybe Natural) Natural
type NatBaseCh base parseDigit ch mn = NatBaseCh' base mn (parseDigit @@ ch)

type family NatBaseCh' base mn mDigit where
    NatBaseCh' base (Just n) (Just digit) = Cont (Just (n * base + digit))
    NatBaseCh' base Nothing  (Just digit) = Cont (Just digit)
    NatBaseCh' base mn       Nothing      = Err (EInvalidDigit base)

type EInvalidDigit base = EBase "NatBase"
    (Text "not a base " :<>: Text (ShowNatDec base) :<>: Text " digit")
eInvalidDigit :: SNat base -> SE (EInvalidDigit base)
eInvalidDigit :: forall (base :: Nat). SNat base -> SE (EInvalidDigit base)
eInvalidDigit SNat base
base = SSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym base)
-> (KnownSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym base) =>
    SE
      ('EBase
         "NatBase"
         (('Text "not a base "
           ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym base))
          ':<>: 'Text " digit")))
-> SE
     ('EBase
        "NatBase"
        (('Text "not a base "
          ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym base))
         ':<>: 'Text " digit"))
forall (s :: Symbol) r. SSymbol s -> (KnownSymbol s => r) -> r
withKnownSymbol (SNat base -> SSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym base)
forall (n :: Nat). SNat n -> SSymbol (ShowNatDec n)
sShowNatDec SNat base
base) SE
  ('EBase
     "NatBase"
     (('Text "not a base "
       ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym base))
      ':<>: 'Text " digit"))
KnownSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym base) =>
SE
  ('EBase
     "NatBase"
     (('Text "not a base "
       ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym base))
      ':<>: 'Text " digit"))
forall (e :: PE). SingE e => SE e
singE

type NatBaseChSym
    :: Natural
    -> (Char ~> Maybe Natural)
    -> ParserChSym (Maybe Natural) Natural
data NatBaseChSym base parseDigit f
type instance App (NatBaseChSym base parseDigit) f =
    NatBaseChSym1 base parseDigit f

type NatBaseChSym1
    :: Natural
    -> (Char ~> Maybe Natural)
    -> ParserChSym1 (Maybe Natural) Natural
data NatBaseChSym1 base parseDigit ch mn
type instance App (NatBaseChSym1 base parseDigit ch) mn =
    NatBaseCh base parseDigit ch mn

sNatBaseChSym
    :: SNat base
    -> SParseDigit parseDigit
    -> SParserChSym (SMaybe SNat) SNat (NatBaseChSym base parseDigit)
sNatBaseChSym :: forall (base :: Nat) (parseDigit :: Char ~> Maybe Nat).
SNat base
-> SParseDigit parseDigit
-> SParserChSym (SMaybe SNat) SNat (NatBaseChSym base parseDigit)
sNatBaseChSym SNat base
base SParseDigit parseDigit
parseDigit = LamRep2
  SChar
  (SMaybe SNat)
  (SResult (SMaybe SNat) SNat)
  (NatBaseChSym base parseDigit)
-> Lam2
     SChar
     (SMaybe SNat)
     (SResult (SMaybe SNat) SNat)
     (NatBaseChSym base parseDigit)
forall {a1} {a2} {b1} (a3 :: a1 -> Type) (b2 :: a2 -> Type)
       (c :: b1 -> Type) (fun :: a1 ~> (a2 ~> b1)).
LamRep2 a3 b2 c fun -> Lam2 a3 b2 c fun
Lam2 (LamRep2
   SChar
   (SMaybe SNat)
   (SResult (SMaybe SNat) SNat)
   (NatBaseChSym base parseDigit)
 -> Lam2
      SChar
      (SMaybe SNat)
      (SResult (SMaybe SNat) SNat)
      (NatBaseChSym base parseDigit))
-> LamRep2
     SChar
     (SMaybe SNat)
     (SResult (SMaybe SNat) SNat)
     (NatBaseChSym base parseDigit)
-> Lam2
     SChar
     (SMaybe SNat)
     (SResult (SMaybe SNat) SNat)
     (NatBaseChSym base parseDigit)
forall a b. (a -> b) -> a -> b
$ \SChar x
ch SMaybe SNat y
mn ->
    case SParseDigit parseDigit
parseDigit SParseDigit parseDigit -> SChar x -> SMaybe SNat (parseDigit @@ x)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ SChar x
ch of
      SJust SNat a1
digit ->
        case SMaybe SNat y
mn of
          SJust SNat a1
n  -> SMaybe SNat ('Just ((a1 * base) + a1))
-> SResult (SMaybe SNat) SNat ('Cont ('Just ((a1 * base) + a1)))
forall {s} {r} (ss :: s -> Type) (s1 :: s) (sr :: r -> Type).
ss s1 -> SResult ss sr ('Cont s1)
SCont (SMaybe SNat ('Just ((a1 * base) + a1))
 -> SResult (SMaybe SNat) SNat ('Cont ('Just ((a1 * base) + a1))))
-> SMaybe SNat ('Just ((a1 * base) + a1))
-> SResult (SMaybe SNat) SNat ('Cont ('Just ((a1 * base) + a1)))
forall a b. (a -> b) -> a -> b
$ SNat ((a1 * base) + a1) -> SMaybe SNat ('Just ((a1 * base) + a1))
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (SNat ((a1 * base) + a1) -> SMaybe SNat ('Just ((a1 * base) + a1)))
-> SNat ((a1 * base) + a1)
-> SMaybe SNat ('Just ((a1 * base) + a1))
forall a b. (a -> b) -> a -> b
$ SNat a1
n SNat a1 -> SNat base -> SNat (a1 * base)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n * m)
%* SNat base
base SNat (a1 * base) -> SNat a1 -> SNat ((a1 * base) + a1)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat a1
digit
          SMaybe SNat y
SNothing -> SMaybe SNat ('Just a1)
-> SResult (SMaybe SNat) SNat ('Cont ('Just a1))
forall {s} {r} (ss :: s -> Type) (s1 :: s) (sr :: r -> Type).
ss s1 -> SResult ss sr ('Cont s1)
SCont (SMaybe SNat ('Just a1)
 -> SResult (SMaybe SNat) SNat ('Cont ('Just a1)))
-> SMaybe SNat ('Just a1)
-> SResult (SMaybe SNat) SNat ('Cont ('Just a1))
forall a b. (a -> b) -> a -> b
$ SNat a1 -> SMaybe SNat ('Just a1)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust SNat a1
digit
      SMaybe SNat (parseDigit @@ x)
SNothing -> SE
  ('EBase
     "NatBase"
     (('Text "not a base "
       ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym base))
      ':<>: 'Text " digit"))
-> SResult
     (SMaybe SNat)
     SNat
     ('Err
        ('EBase
           "NatBase"
           (('Text "not a base "
             ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym base))
            ':<>: 'Text " digit")))
forall {s} {r} (e :: PE) (ss :: s -> Type) (sr :: r -> Type).
SE e -> SResult ss sr ('Err e)
SErr (SE
   ('EBase
      "NatBase"
      (('Text "not a base "
        ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym base))
       ':<>: 'Text " digit"))
 -> SResult
      (SMaybe SNat)
      SNat
      ('Err
         ('EBase
            "NatBase"
            (('Text "not a base "
              ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym base))
             ':<>: 'Text " digit"))))
-> SE
     ('EBase
        "NatBase"
        (('Text "not a base "
          ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym base))
         ':<>: 'Text " digit"))
-> SResult
     (SMaybe SNat)
     SNat
     ('Err
        ('EBase
           "NatBase"
           (('Text "not a base "
             ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym base))
            ':<>: 'Text " digit")))
forall a b. (a -> b) -> a -> b
$ SNat base
-> SE
     ('EBase
        "NatBase"
        (('Text "not a base "
          ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym base))
         ':<>: 'Text " digit"))
forall (base :: Nat). SNat base -> SE (EInvalidDigit base)
eInvalidDigit SNat base
base

type family NatBaseEnd mn where
    NatBaseEnd (Just n) = Right n
    NatBaseEnd Nothing  = Left EEmpty

type EEmpty = EBase "NatBase" (Text "no digits parsed")
eEmpty :: SE EEmpty
eEmpty :: SE EEmpty
eEmpty = SE EEmpty
forall (e :: PE). SingE e => SE e
singE

type NatBaseEndSym :: ParserEndSym (Maybe Natural) Natural
data NatBaseEndSym mn
type instance App NatBaseEndSym mn = NatBaseEnd mn

sNatBaseEndSym :: SParserEndSym (SMaybe SNat) SNat NatBaseEndSym
sNatBaseEndSym :: SParserEndSym (SMaybe SNat) SNat NatBaseEndSym
sNatBaseEndSym = LamRep (SMaybe SNat) (SResultEnd SNat) NatBaseEndSym
-> SParserEndSym (SMaybe SNat) SNat NatBaseEndSym
forall a b (a1 :: a -> Type) (b1 :: b -> Type) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (LamRep (SMaybe SNat) (SResultEnd SNat) NatBaseEndSym
 -> SParserEndSym (SMaybe SNat) SNat NatBaseEndSym)
-> LamRep (SMaybe SNat) (SResultEnd SNat) NatBaseEndSym
-> SParserEndSym (SMaybe SNat) SNat NatBaseEndSym
forall a b. (a -> b) -> a -> b
$ \case
  SJust SNat a1
n  -> SNat a1 -> SEither SE SNat ('Right a1)
forall {r} {l} (sr :: r -> Type) (r1 :: r) (sl :: l -> Type).
sr r1 -> SEither sl sr ('Right r1)
SRight SNat a1
n
  SMaybe SNat x
SNothing -> SE EEmpty -> SEither SE SNat ('Left EEmpty)
forall {l} {r} (sl :: l -> Type) (l1 :: l) (sr :: r -> Type).
sl l1 -> SEither sl sr ('Left l1)
SLeft SE EEmpty
eEmpty