{- | Parse digits from type-level 'Char's.

A 'Nothing' indicates the given 'Char' was not a valid digit for the given base.
-}

module Symparsec.Parser.Natural.Digits where

import GHC.TypeLits
import DeFun.Core
import Singleraeh.Equality ( testEqElse )
import Singleraeh.Maybe
import Unsafe.Coerce ( unsafeCoerce )

type SParseDigit parseDigit = Lam SChar (SMaybe SNat) parseDigit

class SingParseDigit parseDigit where
    singParseDigit :: SParseDigit parseDigit

-- | Parse a binary digit (0 or 1).
type family ParseDigitBin (ch :: Char) :: Maybe Natural where
    ParseDigitBin '0' = Just 0
    ParseDigitBin '1' = Just 1
    ParseDigitBin _   = Nothing

type ParseDigitBinSym :: Char ~> Maybe Natural
data ParseDigitBinSym ch
type instance App ParseDigitBinSym ch = ParseDigitBin ch

sParseDigitBinSym :: SParseDigit ParseDigitBinSym
sParseDigitBinSym :: SParseDigit ParseDigitBinSym
sParseDigitBinSym = LamRep SChar (SMaybe SNat) ParseDigitBinSym
-> SParseDigit ParseDigitBinSym
forall a b (a1 :: a -> Type) (b1 :: b -> Type) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (LamRep SChar (SMaybe SNat) ParseDigitBinSym
 -> SParseDigit ParseDigitBinSym)
-> LamRep SChar (SMaybe SNat) ParseDigitBinSym
-> SParseDigit ParseDigitBinSym
forall a b. (a -> b) -> a -> b
$ \SChar x
ch ->
      SChar x
-> SChar '0'
-> ((x ~ '0') => SMaybe SNat (ParseDigitBinSym @@ x))
-> SMaybe SNat (ParseDigitBinSym @@ x)
-> SMaybe SNat (ParseDigitBinSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'0') (SNat 0 -> SMaybe SNat ('Just 0)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @0))
    (SMaybe SNat (ParseDigitBinSym @@ x)
 -> SMaybe SNat (ParseDigitBinSym @@ x))
-> SMaybe SNat (ParseDigitBinSym @@ x)
-> SMaybe SNat (ParseDigitBinSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '1'
-> ((x ~ '1') => SMaybe SNat (ParseDigitBinSym @@ x))
-> SMaybe SNat (ParseDigitBinSym @@ x)
-> SMaybe SNat (ParseDigitBinSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'1') (SNat 1 -> SMaybe SNat ('Just 1)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @1))
    (SMaybe SNat (ParseDigitBinSym @@ x)
 -> SMaybe SNat (ParseDigitBinSym @@ x))
-> SMaybe SNat (ParseDigitBinSym @@ x)
-> SMaybe SNat (ParseDigitBinSym @@ x)
forall a b. (a -> b) -> a -> b
$ SMaybe Any 'Nothing -> SMaybe SNat (ParseDigitBin x)
forall a b. a -> b
unsafeCoerce SMaybe Any 'Nothing
forall {a} (sa :: a -> Type). SMaybe sa 'Nothing
SNothing

instance SingParseDigit ParseDigitBinSym where
    singParseDigit :: SParseDigit ParseDigitBinSym
singParseDigit = SParseDigit ParseDigitBinSym
sParseDigitBinSym

-- | Parse an octal digit (0-7).
type family ParseDigitOct (ch :: Char) :: Maybe Natural where
    ParseDigitOct '0' = Just 0
    ParseDigitOct '1' = Just 1
    ParseDigitOct '2' = Just 2
    ParseDigitOct '3' = Just 3
    ParseDigitOct '4' = Just 4
    ParseDigitOct '5' = Just 5
    ParseDigitOct '6' = Just 6
    ParseDigitOct '7' = Just 7
    ParseDigitOct _   = Nothing

type ParseDigitOctSym :: Char ~> Maybe Natural
data ParseDigitOctSym ch
type instance App ParseDigitOctSym ch = ParseDigitOct ch

sParseDigitOctSym :: SParseDigit ParseDigitOctSym
sParseDigitOctSym :: SParseDigit ParseDigitOctSym
sParseDigitOctSym = LamRep SChar (SMaybe SNat) ParseDigitOctSym
-> SParseDigit ParseDigitOctSym
forall a b (a1 :: a -> Type) (b1 :: b -> Type) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (LamRep SChar (SMaybe SNat) ParseDigitOctSym
 -> SParseDigit ParseDigitOctSym)
-> LamRep SChar (SMaybe SNat) ParseDigitOctSym
-> SParseDigit ParseDigitOctSym
forall a b. (a -> b) -> a -> b
$ \SChar x
ch ->
      SChar x
-> SChar '0'
-> ((x ~ '0') => SMaybe SNat (ParseDigitOctSym @@ x))
-> SMaybe SNat (ParseDigitOctSym @@ x)
-> SMaybe SNat (ParseDigitOctSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'0') (SNat 0 -> SMaybe SNat ('Just 0)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @0))
    (SMaybe SNat (ParseDigitOctSym @@ x)
 -> SMaybe SNat (ParseDigitOctSym @@ x))
-> SMaybe SNat (ParseDigitOctSym @@ x)
-> SMaybe SNat (ParseDigitOctSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '1'
-> ((x ~ '1') => SMaybe SNat (ParseDigitOctSym @@ x))
-> SMaybe SNat (ParseDigitOctSym @@ x)
-> SMaybe SNat (ParseDigitOctSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'1') (SNat 1 -> SMaybe SNat ('Just 1)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @1))
    (SMaybe SNat (ParseDigitOctSym @@ x)
 -> SMaybe SNat (ParseDigitOctSym @@ x))
-> SMaybe SNat (ParseDigitOctSym @@ x)
-> SMaybe SNat (ParseDigitOctSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '2'
-> ((x ~ '2') => SMaybe SNat (ParseDigitOctSym @@ x))
-> SMaybe SNat (ParseDigitOctSym @@ x)
-> SMaybe SNat (ParseDigitOctSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'2') (SNat 2 -> SMaybe SNat ('Just 2)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @2))
    (SMaybe SNat (ParseDigitOctSym @@ x)
 -> SMaybe SNat (ParseDigitOctSym @@ x))
-> SMaybe SNat (ParseDigitOctSym @@ x)
-> SMaybe SNat (ParseDigitOctSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '3'
-> ((x ~ '3') => SMaybe SNat (ParseDigitOctSym @@ x))
-> SMaybe SNat (ParseDigitOctSym @@ x)
-> SMaybe SNat (ParseDigitOctSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'3') (SNat 3 -> SMaybe SNat ('Just 3)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @3))
    (SMaybe SNat (ParseDigitOctSym @@ x)
 -> SMaybe SNat (ParseDigitOctSym @@ x))
-> SMaybe SNat (ParseDigitOctSym @@ x)
-> SMaybe SNat (ParseDigitOctSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '4'
-> ((x ~ '4') => SMaybe SNat (ParseDigitOctSym @@ x))
-> SMaybe SNat (ParseDigitOctSym @@ x)
-> SMaybe SNat (ParseDigitOctSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'4') (SNat 4 -> SMaybe SNat ('Just 4)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @4))
    (SMaybe SNat (ParseDigitOctSym @@ x)
 -> SMaybe SNat (ParseDigitOctSym @@ x))
-> SMaybe SNat (ParseDigitOctSym @@ x)
-> SMaybe SNat (ParseDigitOctSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '5'
-> ((x ~ '5') => SMaybe SNat (ParseDigitOctSym @@ x))
-> SMaybe SNat (ParseDigitOctSym @@ x)
-> SMaybe SNat (ParseDigitOctSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'5') (SNat 5 -> SMaybe SNat ('Just 5)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @5))
    (SMaybe SNat (ParseDigitOctSym @@ x)
 -> SMaybe SNat (ParseDigitOctSym @@ x))
-> SMaybe SNat (ParseDigitOctSym @@ x)
-> SMaybe SNat (ParseDigitOctSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '6'
-> ((x ~ '6') => SMaybe SNat (ParseDigitOctSym @@ x))
-> SMaybe SNat (ParseDigitOctSym @@ x)
-> SMaybe SNat (ParseDigitOctSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'6') (SNat 6 -> SMaybe SNat ('Just 6)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @6))
    (SMaybe SNat (ParseDigitOctSym @@ x)
 -> SMaybe SNat (ParseDigitOctSym @@ x))
-> SMaybe SNat (ParseDigitOctSym @@ x)
-> SMaybe SNat (ParseDigitOctSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '7'
-> ((x ~ '7') => SMaybe SNat (ParseDigitOctSym @@ x))
-> SMaybe SNat (ParseDigitOctSym @@ x)
-> SMaybe SNat (ParseDigitOctSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'7') (SNat 7 -> SMaybe SNat ('Just 7)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @7))
    (SMaybe SNat (ParseDigitOctSym @@ x)
 -> SMaybe SNat (ParseDigitOctSym @@ x))
-> SMaybe SNat (ParseDigitOctSym @@ x)
-> SMaybe SNat (ParseDigitOctSym @@ x)
forall a b. (a -> b) -> a -> b
$ SMaybe Any 'Nothing -> SMaybe SNat (ParseDigitOct x)
forall a b. a -> b
unsafeCoerce SMaybe Any 'Nothing
forall {a} (sa :: a -> Type). SMaybe sa 'Nothing
SNothing

instance SingParseDigit ParseDigitOctSym where
    singParseDigit :: SParseDigit ParseDigitOctSym
singParseDigit = SParseDigit ParseDigitOctSym
sParseDigitOctSym

-- | Parse a decimal digit (0-9).
type family ParseDigitDec (ch :: Char) :: Maybe Natural where
    ParseDigitDec '0' = Just 0
    ParseDigitDec '1' = Just 1
    ParseDigitDec '2' = Just 2
    ParseDigitDec '3' = Just 3
    ParseDigitDec '4' = Just 4
    ParseDigitDec '5' = Just 5
    ParseDigitDec '6' = Just 6
    ParseDigitDec '7' = Just 7
    ParseDigitDec '8' = Just 8
    ParseDigitDec '9' = Just 9
    ParseDigitDec _   = Nothing

type ParseDigitDecSym :: Char ~> Maybe Natural
data ParseDigitDecSym ch
type instance App ParseDigitDecSym ch = ParseDigitDec ch

sParseDigitDecSym :: SParseDigit ParseDigitDecSym
sParseDigitDecSym :: SParseDigit ParseDigitDecSym
sParseDigitDecSym = LamRep SChar (SMaybe SNat) ParseDigitDecSym
-> SParseDigit ParseDigitDecSym
forall a b (a1 :: a -> Type) (b1 :: b -> Type) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (LamRep SChar (SMaybe SNat) ParseDigitDecSym
 -> SParseDigit ParseDigitDecSym)
-> LamRep SChar (SMaybe SNat) ParseDigitDecSym
-> SParseDigit ParseDigitDecSym
forall a b. (a -> b) -> a -> b
$ \SChar x
ch ->
      SChar x
-> SChar '0'
-> ((x ~ '0') => SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'0') (SNat 0 -> SMaybe SNat ('Just 0)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @0))
    (SMaybe SNat (ParseDigitDecSym @@ x)
 -> SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '1'
-> ((x ~ '1') => SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'1') (SNat 1 -> SMaybe SNat ('Just 1)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @1))
    (SMaybe SNat (ParseDigitDecSym @@ x)
 -> SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '2'
-> ((x ~ '2') => SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'2') (SNat 2 -> SMaybe SNat ('Just 2)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @2))
    (SMaybe SNat (ParseDigitDecSym @@ x)
 -> SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '3'
-> ((x ~ '3') => SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'3') (SNat 3 -> SMaybe SNat ('Just 3)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @3))
    (SMaybe SNat (ParseDigitDecSym @@ x)
 -> SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '4'
-> ((x ~ '4') => SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'4') (SNat 4 -> SMaybe SNat ('Just 4)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @4))
    (SMaybe SNat (ParseDigitDecSym @@ x)
 -> SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '5'
-> ((x ~ '5') => SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'5') (SNat 5 -> SMaybe SNat ('Just 5)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @5))
    (SMaybe SNat (ParseDigitDecSym @@ x)
 -> SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '6'
-> ((x ~ '6') => SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'6') (SNat 6 -> SMaybe SNat ('Just 6)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @6))
    (SMaybe SNat (ParseDigitDecSym @@ x)
 -> SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '7'
-> ((x ~ '7') => SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'7') (SNat 7 -> SMaybe SNat ('Just 7)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @7))
    (SMaybe SNat (ParseDigitDecSym @@ x)
 -> SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '8'
-> ((x ~ '8') => SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'8') (SNat 8 -> SMaybe SNat ('Just 8)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @8))
    (SMaybe SNat (ParseDigitDecSym @@ x)
 -> SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '9'
-> ((x ~ '9') => SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'9') (SNat 9 -> SMaybe SNat ('Just 9)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @9))
    (SMaybe SNat (ParseDigitDecSym @@ x)
 -> SMaybe SNat (ParseDigitDecSym @@ x))
-> SMaybe SNat (ParseDigitDecSym @@ x)
-> SMaybe SNat (ParseDigitDecSym @@ x)
forall a b. (a -> b) -> a -> b
$ SMaybe Any 'Nothing -> SMaybe SNat (ParseDigitDec x)
forall a b. a -> b
unsafeCoerce SMaybe Any 'Nothing
forall {a} (sa :: a -> Type). SMaybe sa 'Nothing
SNothing

instance SingParseDigit ParseDigitDecSym where
    singParseDigit :: SParseDigit ParseDigitDecSym
singParseDigit = SParseDigit ParseDigitDecSym
sParseDigitDecSym

-- | Parse a hexadecimal digit (0-9A-Fa-f).
--
-- Both upper and lower case are permitted.
type family ParseDigitHex (ch :: Char) :: Maybe Natural where
    ParseDigitHex '0' = Just  0
    ParseDigitHex '1' = Just  1
    ParseDigitHex '2' = Just  2
    ParseDigitHex '3' = Just  3
    ParseDigitHex '4' = Just  4
    ParseDigitHex '5' = Just  5
    ParseDigitHex '6' = Just  6
    ParseDigitHex '7' = Just  7
    ParseDigitHex '8' = Just  8
    ParseDigitHex '9' = Just  9
    ParseDigitHex 'a' = Just 10
    ParseDigitHex 'A' = Just 10
    ParseDigitHex 'b' = Just 11
    ParseDigitHex 'B' = Just 11
    ParseDigitHex 'c' = Just 12
    ParseDigitHex 'C' = Just 12
    ParseDigitHex 'd' = Just 13
    ParseDigitHex 'D' = Just 13
    ParseDigitHex 'e' = Just 14
    ParseDigitHex 'E' = Just 14
    ParseDigitHex 'f' = Just 15
    ParseDigitHex 'F' = Just 15
    ParseDigitHex _   = Nothing

type ParseDigitHexSym :: Char ~> Maybe Natural
data ParseDigitHexSym ch
type instance App ParseDigitHexSym ch = ParseDigitHex ch

sParseDigitHexSym :: SParseDigit ParseDigitHexSym
sParseDigitHexSym :: SParseDigit ParseDigitHexSym
sParseDigitHexSym = LamRep SChar (SMaybe SNat) ParseDigitHexSym
-> SParseDigit ParseDigitHexSym
forall a b (a1 :: a -> Type) (b1 :: b -> Type) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (LamRep SChar (SMaybe SNat) ParseDigitHexSym
 -> SParseDigit ParseDigitHexSym)
-> LamRep SChar (SMaybe SNat) ParseDigitHexSym
-> SParseDigit ParseDigitHexSym
forall a b. (a -> b) -> a -> b
$ \SChar x
ch ->
      SChar x
-> SChar '0'
-> ((x ~ '0') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'0') (SNat 0 -> SMaybe SNat ('Just 0)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat  @0))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '1'
-> ((x ~ '1') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'1') (SNat 1 -> SMaybe SNat ('Just 1)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat  @1))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '2'
-> ((x ~ '2') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'2') (SNat 2 -> SMaybe SNat ('Just 2)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat  @2))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '3'
-> ((x ~ '3') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'3') (SNat 3 -> SMaybe SNat ('Just 3)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat  @3))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '4'
-> ((x ~ '4') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'4') (SNat 4 -> SMaybe SNat ('Just 4)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat  @4))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '5'
-> ((x ~ '5') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'5') (SNat 5 -> SMaybe SNat ('Just 5)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat  @5))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '6'
-> ((x ~ '6') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'6') (SNat 6 -> SMaybe SNat ('Just 6)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat  @6))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '7'
-> ((x ~ '7') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'7') (SNat 7 -> SMaybe SNat ('Just 7)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat  @7))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '8'
-> ((x ~ '8') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'8') (SNat 8 -> SMaybe SNat ('Just 8)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat  @8))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar '9'
-> ((x ~ '9') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'9') (SNat 9 -> SMaybe SNat ('Just 9)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat  @9))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'a'
-> ((x ~ 'a') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'a') (SNat 10 -> SMaybe SNat ('Just 10)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @10))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'A'
-> ((x ~ 'A') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'A') (SNat 10 -> SMaybe SNat ('Just 10)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @10))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'b'
-> ((x ~ 'b') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'b') (SNat 11 -> SMaybe SNat ('Just 11)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @11))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'B'
-> ((x ~ 'B') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'B') (SNat 11 -> SMaybe SNat ('Just 11)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @11))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'c'
-> ((x ~ 'c') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'c') (SNat 12 -> SMaybe SNat ('Just 12)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @12))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'C'
-> ((x ~ 'C') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'C') (SNat 12 -> SMaybe SNat ('Just 12)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @12))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'd'
-> ((x ~ 'd') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'d') (SNat 13 -> SMaybe SNat ('Just 13)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @13))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'D'
-> ((x ~ 'D') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'D') (SNat 13 -> SMaybe SNat ('Just 13)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @13))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'e'
-> ((x ~ 'e') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'e') (SNat 14 -> SMaybe SNat ('Just 14)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @14))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'E'
-> ((x ~ 'E') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'E') (SNat 14 -> SMaybe SNat ('Just 14)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @14))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'f'
-> ((x ~ 'f') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'f') (SNat 15 -> SMaybe SNat ('Just 15)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @15))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SChar x
-> SChar 'F'
-> ((x ~ 'F') => SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SChar x
ch (forall (c :: Char). KnownChar c => SChar c
SChar @'F') (SNat 15 -> SMaybe SNat ('Just 15)
forall {a} (sa :: a -> Type) (a1 :: a).
sa a1 -> SMaybe sa ('Just a1)
SJust (forall (n :: Nat). KnownNat n => SNat n
SNat @15))
    (SMaybe SNat (ParseDigitHexSym @@ x)
 -> SMaybe SNat (ParseDigitHexSym @@ x))
-> SMaybe SNat (ParseDigitHexSym @@ x)
-> SMaybe SNat (ParseDigitHexSym @@ x)
forall a b. (a -> b) -> a -> b
$ SMaybe Any 'Nothing -> SMaybe SNat (ParseDigitHex x)
forall a b. a -> b
unsafeCoerce SMaybe Any 'Nothing
forall {a} (sa :: a -> Type). SMaybe sa 'Nothing
SNothing

instance SingParseDigit ParseDigitHexSym where
    singParseDigit :: SParseDigit ParseDigitHexSym
singParseDigit = SParseDigit ParseDigitHexSym
sParseDigitHexSym