{-# 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 )
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