{-# LANGUAGE UndecidableInstances #-}

module Symparsec.Parser.Take where

import Symparsec.Parser.Common
import Singleraeh.Symbol ( RevCharsToSymbol, revCharsToSymbol )
import Singleraeh.List ( SList(..) )
import Singleraeh.Tuple ( STuple2(..) )
import Data.Type.Equality
import Singleraeh.Natural ( (%-) )
import Singleraeh.Either ( SEither(..) )
import TypeLevelShow.Natural
import GHC.TypeLits hiding ( ErrorMessage(..) )
import Unsafe.Coerce ( unsafeCoerce )
import DeFun.Core

-- | Return the next @n@ characters.
type Take n = 'PParser TakeChSym TakeEndSym '(n, '[])

type STakeS = STuple2 SNat (SList SChar)
type  TakeS = (Natural, [Char])

sTake :: SNat n -> SParser STakeS SSymbol (Take n)
sTake :: forall (n :: Nat). SNat n -> SParser STakeS SSymbol (Take n)
sTake SNat n
n = SParserChSym STakeS SSymbol TakeChSym
-> SParserEndSym STakeS SSymbol TakeEndSym
-> STakeS '(n, '[])
-> SParser STakeS SSymbol ('PParser TakeChSym TakeEndSym '(n, '[]))
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 SParserChSym STakeS SSymbol TakeChSym
sTakeChSym SParserEndSym STakeS SSymbol TakeEndSym
sTakeEndSym (SNat n -> SList SChar '[] -> STakeS '(n, '[])
forall {a} {b} (sa :: a -> Type) (a1 :: a) (sb :: b -> Type)
       (b1 :: b).
sa a1 -> sb b1 -> STuple2 sa sb '(a1, b1)
STuple2 SNat n
n SList SChar '[]
forall {a} (sa :: a -> Type). SList sa '[]
SNil)

instance KnownNat n => SingParser (Take n) where
    type PS (Take n) = STakeS
    type PR (Take n) = SSymbol
    singParser' :: SParser (PS (Take n)) (PR (Take n)) (Take n)
singParser' = SNat n -> SParser STakeS SSymbol (Take n)
forall (n :: Nat). SNat n -> SParser STakeS SSymbol (Take n)
sTake SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat

type TakeCh :: PParserCh TakeS Symbol
type family TakeCh ch s where
    TakeCh ch '(0, chs) = Done (RevCharsToSymbol chs)
    TakeCh ch '(n, chs) = Cont '(n-1, ch : chs)

type TakeChSym :: ParserChSym TakeS Symbol
data TakeChSym f
type instance App TakeChSym f = TakeChSym1 f

sTakeChSym :: SParserChSym STakeS SSymbol TakeChSym
sTakeChSym :: SParserChSym STakeS SSymbol TakeChSym
sTakeChSym = LamRep2 SChar STakeS (SResult STakeS SSymbol) TakeChSym
-> SParserChSym STakeS SSymbol TakeChSym
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 STakeS (SResult STakeS SSymbol) TakeChSym
 -> SParserChSym STakeS SSymbol TakeChSym)
-> LamRep2 SChar STakeS (SResult STakeS SSymbol) TakeChSym
-> SParserChSym STakeS SSymbol TakeChSym
forall a b. (a -> b) -> a -> b
$ \SChar x
ch (STuple2 SNat a1
n SList SChar b1
chs) ->
    case SNat a1 -> SNat 0 -> Maybe (a1 :~: 0)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SNat a1
n (forall (n :: Nat). KnownNat n => SNat n
SNat @0) of
      Just a1 :~: 0
Refl -> SSymbol (RevCharsToSymbol' "" b1)
-> SResult STakeS SSymbol ('Done (RevCharsToSymbol' "" b1))
forall {r} {s} (sr :: r -> Type) (r1 :: r) (ss :: s -> Type).
sr r1 -> SResult ss sr ('Done r1)
SDone (SSymbol (RevCharsToSymbol' "" b1)
 -> SResult STakeS SSymbol ('Done (RevCharsToSymbol' "" b1)))
-> SSymbol (RevCharsToSymbol' "" b1)
-> SResult STakeS SSymbol ('Done (RevCharsToSymbol' "" b1))
forall a b. (a -> b) -> a -> b
$ SList SChar b1 -> SSymbol (RevCharsToSymbol' "" b1)
forall (chs :: [Char]).
SList SChar chs -> SSymbol (RevCharsToSymbol chs)
revCharsToSymbol SList SChar b1
chs
      Maybe (a1 :~: 0)
Nothing   ->
        SResult STakeS Any ('Cont '(a1 - 1, x : b1))
-> SResult STakeS SSymbol ((TakeChSym @@ x) @@ y)
forall a b. a -> b
unsafeCoerce (SResult STakeS Any ('Cont '(a1 - 1, x : b1))
 -> SResult STakeS SSymbol ((TakeChSym @@ x) @@ y))
-> SResult STakeS Any ('Cont '(a1 - 1, x : b1))
-> SResult STakeS SSymbol ((TakeChSym @@ x) @@ y)
forall a b. (a -> b) -> a -> b
$ STuple2 SNat (SList SChar) '(a1 - 1, x : b1)
-> SResult STakeS Any ('Cont '(a1 - 1, x : b1))
forall {s} {r} (ss :: s -> Type) (s1 :: s) (sr :: r -> Type).
ss s1 -> SResult ss sr ('Cont s1)
SCont (STuple2 SNat (SList SChar) '(a1 - 1, x : b1)
 -> SResult STakeS Any ('Cont '(a1 - 1, x : b1)))
-> STuple2 SNat (SList SChar) '(a1 - 1, x : b1)
-> SResult STakeS Any ('Cont '(a1 - 1, x : b1))
forall a b. (a -> b) -> a -> b
$ SNat (a1 - 1)
-> SList SChar (x : b1)
-> STuple2 SNat (SList SChar) '(a1 - 1, x : b1)
forall {a} {b} (sa :: a -> Type) (a1 :: a) (sb :: b -> Type)
       (b1 :: b).
sa a1 -> sb b1 -> STuple2 sa sb '(a1, b1)
STuple2 (SNat a1
n SNat a1 -> SNat 1 -> SNat (a1 - 1)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- (forall (n :: Nat). KnownNat n => SNat n
SNat @1)) (SChar x -> SList SChar b1 -> SList SChar (x : b1)
forall {a} (sa :: a -> Type) (a1 :: a) (as1 :: [a]).
sa a1 -> SList sa as1 -> SList sa (a1 : as1)
SCons SChar x
ch SList SChar b1
chs)

type TakeChSym1 :: ParserChSym1 TakeS Symbol
data TakeChSym1 ch s
type instance App (TakeChSym1 ch) s = TakeCh ch s

type TakeEnd :: PParserEnd TakeS Symbol
type family TakeEnd s where
    TakeEnd '(0, chs) = Right (RevCharsToSymbol chs)
    TakeEnd '(n, _)   = Left (ETakeEnd n)

type ETakeEnd n = EBase "Take"
    (      Text "tried to take "
      :<>: Text (ShowNatDec n) :<>: Text " chars from empty string")

eTakeEnd :: SNat n -> SE (ETakeEnd n)
eTakeEnd :: forall (n :: Nat). SNat n -> SE (ETakeEnd n)
eTakeEnd SNat n
sn = SSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym n)
-> (KnownSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym n) =>
    SE
      ('EBase
         "Take"
         (('Text "tried to take "
           ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
          ':<>: 'Text " chars from empty string")))
-> SE
     ('EBase
        "Take"
        (('Text "tried to take "
          ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
         ':<>: 'Text " chars from empty string"))
forall (s :: Symbol) r. SSymbol s -> (KnownSymbol s => r) -> r
withKnownSymbol (SNat n -> SSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym n)
forall (n :: Nat). SNat n -> SSymbol (ShowNatDec n)
sShowNatDec SNat n
sn) SE
  ('EBase
     "Take"
     (('Text "tried to take "
       ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
      ':<>: 'Text " chars from empty string"))
KnownSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym n) =>
SE
  ('EBase
     "Take"
     (('Text "tried to take "
       ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
      ':<>: 'Text " chars from empty string"))
forall (e :: PE). SingE e => SE e
singE

type TakeEndSym :: ParserEndSym TakeS Symbol
data TakeEndSym s
type instance App TakeEndSym s = TakeEnd s

sTakeEndSym :: SParserEndSym STakeS SSymbol TakeEndSym
sTakeEndSym :: SParserEndSym STakeS SSymbol TakeEndSym
sTakeEndSym = LamRep STakeS (SResultEnd SSymbol) TakeEndSym
-> SParserEndSym STakeS SSymbol TakeEndSym
forall a b (a1 :: a -> Type) (b1 :: b -> Type) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (LamRep STakeS (SResultEnd SSymbol) TakeEndSym
 -> SParserEndSym STakeS SSymbol TakeEndSym)
-> LamRep STakeS (SResultEnd SSymbol) TakeEndSym
-> SParserEndSym STakeS SSymbol TakeEndSym
forall a b. (a -> b) -> a -> b
$ \(STuple2 SNat a1
n SList SChar b1
chs) ->
    case SNat a1 -> SNat 0 -> Maybe (a1 :~: 0)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SNat a1
n (forall (n :: Nat). KnownNat n => SNat n
SNat @0) of
      Just a1 :~: 0
Refl -> SSymbol (RevCharsToSymbol' "" b1)
-> SEither SE SSymbol ('Right (RevCharsToSymbol' "" b1))
forall {r} {l} (sr :: r -> Type) (r1 :: r) (sl :: l -> Type).
sr r1 -> SEither sl sr ('Right r1)
SRight (SSymbol (RevCharsToSymbol' "" b1)
 -> SEither SE SSymbol ('Right (RevCharsToSymbol' "" b1)))
-> SSymbol (RevCharsToSymbol' "" b1)
-> SEither SE SSymbol ('Right (RevCharsToSymbol' "" b1))
forall a b. (a -> b) -> a -> b
$ SList SChar b1 -> SSymbol (RevCharsToSymbol' "" b1)
forall (chs :: [Char]).
SList SChar chs -> SSymbol (RevCharsToSymbol chs)
revCharsToSymbol SList SChar b1
chs
      Maybe (a1 :~: 0)
Nothing   -> SEither
  SE
  Any
  ('Left
     ('EBase
        "Take"
        (('Text "tried to take "
          ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
         ':<>: 'Text " chars from empty string")))
-> SResultEnd SSymbol (TakeEndSym @@ x)
forall a b. a -> b
unsafeCoerce (SEither
   SE
   Any
   ('Left
      ('EBase
         "Take"
         (('Text "tried to take "
           ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
          ':<>: 'Text " chars from empty string")))
 -> SResultEnd SSymbol (TakeEndSym @@ x))
-> SEither
     SE
     Any
     ('Left
        ('EBase
           "Take"
           (('Text "tried to take "
             ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
            ':<>: 'Text " chars from empty string")))
-> SResultEnd SSymbol (TakeEndSym @@ x)
forall a b. (a -> b) -> a -> b
$ SE
  ('EBase
     "Take"
     (('Text "tried to take "
       ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
      ':<>: 'Text " chars from empty string"))
-> SEither
     SE
     Any
     ('Left
        ('EBase
           "Take"
           (('Text "tried to take "
             ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
            ':<>: 'Text " chars from empty string")))
forall {l} {r} (sl :: l -> Type) (l1 :: l) (sr :: r -> Type).
sl l1 -> SEither sl sr ('Left l1)
SLeft (SE
   ('EBase
      "Take"
      (('Text "tried to take "
        ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
       ':<>: 'Text " chars from empty string"))
 -> SEither
      SE
      Any
      ('Left
         ('EBase
            "Take"
            (('Text "tried to take "
              ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
             ':<>: 'Text " chars from empty string"))))
-> SE
     ('EBase
        "Take"
        (('Text "tried to take "
          ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
         ':<>: 'Text " chars from empty string"))
-> SEither
     SE
     Any
     ('Left
        ('EBase
           "Take"
           (('Text "tried to take "
             ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
            ':<>: 'Text " chars from empty string")))
forall a b. (a -> b) -> a -> b
$ SNat a1
-> SE
     ('EBase
        "Take"
        (('Text "tried to take "
          ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
         ':<>: 'Text " chars from empty string"))
forall (n :: Nat). SNat n -> SE (ETakeEnd n)
eTakeEnd SNat a1
n