{-# LANGUAGE UndecidableInstances #-}

module Symparsec.Parser.Skip where

import Symparsec.Parser.Common
import GHC.TypeLits hiding ( ErrorMessage(..) )
import TypeLevelShow.Natural ( ShowNatDec, sShowNatDec )
import Data.Type.Equality
import Singleraeh.Tuple
import Singleraeh.Either
import Singleraeh.Natural
import DeFun.Core
import Unsafe.Coerce ( unsafeCoerce )

-- | Skip forward @n@ characters. Fails if fewer than @n@ characters are
--   available'.
type Skip :: Natural -> PParser Natural ()
type Skip n = 'PParser SkipChSym SkipEndSym n

sSkip :: SNat n -> SParser SNat SUnit (Skip n)
sSkip :: forall (n :: Nat). SNat n -> SParser SNat SUnit (Skip n)
sSkip SNat n
n = SParserChSym SNat SUnit SkipChSym
-> SParserEndSym SNat SUnit SkipEndSym
-> SNat n
-> SParser SNat SUnit ('PParser SkipChSym SkipEndSym 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 SNat SUnit SkipChSym
sSkipChSym SParserEndSym SNat SUnit SkipEndSym
sSkipEndSym SNat n
n

instance KnownNat n => SingParser (Skip n) where
    type PS (Skip n) = SNat
    type PR (Skip n) = SUnit
    singParser' :: SParser (PS (Skip n)) (PR (Skip n)) (Skip n)
singParser' = SNat n -> SParser SNat SUnit (Skip n)
forall (n :: Nat). SNat n -> SParser SNat SUnit (Skip n)
sSkip SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat

type SkipCh :: PParserCh Natural ()
type family SkipCh ch n where
    SkipCh _ 0 = Done '()
    SkipCh _ n = Cont (n-1)

type SkipChSym :: ParserChSym Natural ()
data SkipChSym f
type instance App SkipChSym f = SkipChSym1 f

type SkipChSym1 :: ParserChSym1 Natural ()
data SkipChSym1 ch n
type instance App (SkipChSym1 ch) n = SkipCh ch n

sSkipChSym :: SParserChSym SNat SUnit SkipChSym
sSkipChSym :: SParserChSym SNat SUnit SkipChSym
sSkipChSym = LamRep2 SChar SNat (SResult SNat SUnit) SkipChSym
-> SParserChSym SNat SUnit SkipChSym
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 SNat (SResult SNat SUnit) SkipChSym
 -> SParserChSym SNat SUnit SkipChSym)
-> LamRep2 SChar SNat (SResult SNat SUnit) SkipChSym
-> SParserChSym SNat SUnit SkipChSym
forall a b. (a -> b) -> a -> b
$ \SChar x
_ SNat y
n ->
    case SNat y -> SNat 0 -> Maybe (y :~: 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 y
n (forall (n :: Nat). KnownNat n => SNat n
SNat @0) of
      Just y :~: 0
Refl -> SUnit '() -> SResult SNat SUnit ('Done '())
forall {r} {s} (sr :: r -> Type) (r1 :: r) (ss :: s -> Type).
sr r1 -> SResult ss sr ('Done r1)
SDone SUnit '()
SUnit
      Maybe (y :~: 0)
Nothing   -> SResult SNat Any ('Cont (y - 1))
-> SResult SNat SUnit ((SkipChSym @@ x) @@ y)
forall a b. a -> b
unsafeCoerce (SResult SNat Any ('Cont (y - 1))
 -> SResult SNat SUnit ((SkipChSym @@ x) @@ y))
-> SResult SNat Any ('Cont (y - 1))
-> SResult SNat SUnit ((SkipChSym @@ x) @@ y)
forall a b. (a -> b) -> a -> b
$ SNat (y - 1) -> SResult SNat Any ('Cont (y - 1))
forall {s} {r} (ss :: s -> Type) (s1 :: s) (sr :: r -> Type).
ss s1 -> SResult ss sr ('Cont s1)
SCont (SNat (y - 1) -> SResult SNat Any ('Cont (y - 1)))
-> SNat (y - 1) -> SResult SNat Any ('Cont (y - 1))
forall a b. (a -> b) -> a -> b
$ SNat y
n SNat y -> SNat 1 -> SNat (y - 1)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- (forall (n :: Nat). KnownNat n => SNat n
SNat @1)

type SkipEnd :: PParserEnd Natural ()
type family SkipEnd n where
    SkipEnd 0 = Right '()
    SkipEnd n = Left (ESkipPastEnd n)

type ESkipPastEnd n = EBase "Skip"
    (      Text "tried to skip "
      :<>: Text (ShowNatDec n) :<>: Text " chars from empty string")
eSkipPastEnd :: SNat n -> SE (ESkipPastEnd n)
eSkipPastEnd :: forall (n :: Nat). SNat n -> SE (ESkipPastEnd n)
eSkipPastEnd SNat n
n = SSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym n)
-> (KnownSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym n) =>
    SE
      ('EBase
         "Skip"
         (('Text "tried to skip "
           ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
          ':<>: 'Text " chars from empty string")))
-> SE
     ('EBase
        "Skip"
        (('Text "tried to skip "
          ':<>: '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
n) SE
  ('EBase
     "Skip"
     (('Text "tried to skip "
       ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
      ':<>: 'Text " chars from empty string"))
KnownSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym n) =>
SE
  ('EBase
     "Skip"
     (('Text "tried to skip "
       ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
      ':<>: 'Text " chars from empty string"))
forall (e :: PE). SingE e => SE e
singE

type SkipEndSym :: ParserEndSym Natural ()
data SkipEndSym n
type instance App SkipEndSym n = SkipEnd n

sSkipEndSym :: SParserEndSym SNat SUnit SkipEndSym
sSkipEndSym :: SParserEndSym SNat SUnit SkipEndSym
sSkipEndSym = LamRep SNat (SResultEnd SUnit) SkipEndSym
-> SParserEndSym SNat SUnit SkipEndSym
forall a b (a1 :: a -> Type) (b1 :: b -> Type) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (LamRep SNat (SResultEnd SUnit) SkipEndSym
 -> SParserEndSym SNat SUnit SkipEndSym)
-> LamRep SNat (SResultEnd SUnit) SkipEndSym
-> SParserEndSym SNat SUnit SkipEndSym
forall a b. (a -> b) -> a -> b
$ \SNat x
n ->
    case SNat x -> SNat 0 -> Maybe (x :~: 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 x
n (forall (n :: Nat). KnownNat n => SNat n
SNat @0) of
      Just x :~: 0
Refl -> SUnit '() -> SEither SE SUnit ('Right '())
forall {r} {l} (sr :: r -> Type) (r1 :: r) (sl :: l -> Type).
sr r1 -> SEither sl sr ('Right r1)
SRight SUnit '()
SUnit
      Maybe (x :~: 0)
Nothing   -> SEither
  SE
  Any
  ('Left
     ('EBase
        "Skip"
        (('Text "tried to skip "
          ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym x))
         ':<>: 'Text " chars from empty string")))
-> SResultEnd SUnit (SkipEndSym @@ x)
forall a b. a -> b
unsafeCoerce (SEither
   SE
   Any
   ('Left
      ('EBase
         "Skip"
         (('Text "tried to skip "
           ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym x))
          ':<>: 'Text " chars from empty string")))
 -> SResultEnd SUnit (SkipEndSym @@ x))
-> SEither
     SE
     Any
     ('Left
        ('EBase
           "Skip"
           (('Text "tried to skip "
             ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym x))
            ':<>: 'Text " chars from empty string")))
-> SResultEnd SUnit (SkipEndSym @@ x)
forall a b. (a -> b) -> a -> b
$ SE
  ('EBase
     "Skip"
     (('Text "tried to skip "
       ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym x))
      ':<>: 'Text " chars from empty string"))
-> SEither
     SE
     Any
     ('Left
        ('EBase
           "Skip"
           (('Text "tried to skip "
             ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym x))
            ':<>: '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
      "Skip"
      (('Text "tried to skip "
        ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym x))
       ':<>: 'Text " chars from empty string"))
 -> SEither
      SE
      Any
      ('Left
         ('EBase
            "Skip"
            (('Text "tried to skip "
              ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym x))
             ':<>: 'Text " chars from empty string"))))
-> SE
     ('EBase
        "Skip"
        (('Text "tried to skip "
          ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym x))
         ':<>: 'Text " chars from empty string"))
-> SEither
     SE
     Any
     ('Left
        ('EBase
           "Skip"
           (('Text "tried to skip "
             ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym x))
            ':<>: 'Text " chars from empty string")))
forall a b. (a -> b) -> a -> b
$ SNat x
-> SE
     ('EBase
        "Skip"
        (('Text "tried to skip "
          ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym x))
         ':<>: 'Text " chars from empty string"))
forall (n :: Nat). SNat n -> SE (ESkipPastEnd n)
eSkipPastEnd SNat x
n