{-# LANGUAGE UndecidableInstances #-}

module Symparsec.Parser.While where

import Symparsec.Parser.Common
import DeFun.Core
import GHC.TypeLits
import Singleraeh.Bool
import Singleraeh.Either
import Symparsec.Parser.While.Predicates

-- | Run the given parser while the given character predicate succeeds.
type family While chPred p where
    While chPred ('PParser pCh pEnd s0) = While' chPred pCh pEnd s0
type While' chPred pCh pEnd s0 = 'PParser (WhileChSym chPred pCh pEnd) pEnd s0

sWhile
    :: Lam SChar SBool chPred
    -> SParser ss sr ('PParser pCh pEnd s0)
    -> SParser ss sr (While' chPred pCh pEnd s0)
sWhile :: forall {s} {r} (chPred :: Char ~> Bool) (ss :: s -> Type)
       (sr :: r -> Type) (pCh :: ParserChSym s r)
       (pEnd :: ParserEndSym s r) (s0 :: s).
Lam SChar SBool chPred
-> SParser ss sr ('PParser pCh pEnd s0)
-> SParser ss sr (While' chPred pCh pEnd s0)
sWhile Lam SChar SBool chPred
chPred (SParser SParserChSym ss sr pCh
pCh SParserEndSym ss sr pEnd
pEnd ss s0
s0) =
    SParserChSym ss sr (WhileChSym chPred pCh pEnd)
-> SParserEndSym ss sr pEnd
-> ss s0
-> SParser ss sr ('PParser (WhileChSym chPred pCh pEnd) pEnd s0)
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 (Lam SChar SBool chPred
-> SParserChSym ss sr pCh
-> SParserEndSym ss sr pEnd
-> SParserChSym ss sr (WhileChSym chPred pCh pEnd)
forall {s} {r} (chPred :: Char ~> Bool) (ss :: s -> Type)
       (sr :: r -> Type) (pCh :: Char ~> (s ~> PResult s r))
       (pEnd :: s ~> Either PE r).
Lam SChar SBool chPred
-> SParserChSym ss sr pCh
-> SParserEndSym ss sr pEnd
-> SParserChSym ss sr (WhileChSym chPred pCh pEnd)
sWhileChSym Lam SChar SBool chPred
chPred SParserChSym ss sr pCh
SParserChSym ss sr pCh
pCh SParserEndSym ss sr pEnd
SParserEndSym ss sr pEnd
pEnd) SParserEndSym ss sr pEnd
SParserEndSym ss sr pEnd
pEnd ss s0
ss s0
s0

instance
  ( p ~ 'PParser pCh pEnd s0, SingParser p
  , SingChPred chPred
  ) => SingParser (While' chPred pCh pEnd s0) where
    type PS (While' chPred pCh pEnd s0) = PS ('PParser pCh pEnd s0)
    type PR (While' chPred pCh pEnd s0) = PR ('PParser pCh pEnd s0)
    singParser' :: SParser
  (PS (While' chPred pCh pEnd s0))
  (PR (While' chPred pCh pEnd s0))
  (While' chPred pCh pEnd s0)
singParser' = Lam SChar SBool chPred
-> SParser
     (PS ('PParser pCh pEnd s0))
     (PR ('PParser pCh pEnd s0))
     ('PParser pCh pEnd s0)
-> SParser
     (PS ('PParser pCh pEnd s0))
     (PR ('PParser pCh pEnd s0))
     (While' chPred pCh pEnd s0)
forall {s} {r} (chPred :: Char ~> Bool) (ss :: s -> Type)
       (sr :: r -> Type) (pCh :: ParserChSym s r)
       (pEnd :: ParserEndSym s r) (s0 :: s).
Lam SChar SBool chPred
-> SParser ss sr ('PParser pCh pEnd s0)
-> SParser ss sr (While' chPred pCh pEnd s0)
sWhile (forall (chPred :: Char ~> Bool).
SingChPred chPred =>
Lam SChar SBool chPred
singChPred @chPred) (forall {s} {r} (p :: PParser s r).
SingParser p =>
SParser (PS p) (PR p) p
forall (p :: PParser s r). SingParser p => SParser (PS p) (PR p) p
singParser @p)

type WhileCh chPred pCh pEnd ch s = WhileCh' pCh pEnd ch s (chPred @@ ch)
type family WhileCh' pCh pEnd ch s res where
    WhileCh' pCh pEnd ch s True  = pCh @@ ch @@ s
    WhileCh' pCh pEnd ch s False = WhileCh'' (pEnd @@ s)

type family WhileCh'' res where
    WhileCh'' (Right r) = Done r
    WhileCh'' (Left  e) = Err (EWhile e)

type EWhile e = EIn "While" e
eWhile :: SE e -> SE (EWhile e)
eWhile :: forall (e :: PE). SE e -> SE (EWhile e)
eWhile SE e
e = SE e -> (SingE e => SE (EWhile e)) -> SE (EWhile e)
forall (e :: PE) r. SE e -> (SingE e => r) -> r
withSingE SE e
e ((SingE e => SE (EWhile e)) -> SE (EWhile e))
-> (SingE e => SE (EWhile e)) -> SE (EWhile e)
forall a b. (a -> b) -> a -> b
$ SE (EWhile e)
SingE e => SE (EWhile e)
forall (e :: PE). SingE e => SE e
singE

type WhileChSym
    :: (Char ~> Bool)
    -> ParserChSym  s r
    -> ParserEndSym s r
    -> ParserChSym  s r
data WhileChSym chPred pCh pEnd f
type instance App (WhileChSym chPred pCh pEnd) f = WhileChSym1 chPred pCh pEnd f

type WhileChSym1
    :: (Char ~> Bool)
    -> ParserChSym  s r
    -> ParserEndSym s r
    -> ParserChSym1 s r
data WhileChSym1 chPred pCh pEnd ch s
type instance App (WhileChSym1 chPred pCh pEnd ch) s = WhileCh chPred pCh pEnd ch s

sWhileChSym
    :: Lam SChar SBool chPred
    -> SParserChSym  ss sr pCh
    -> SParserEndSym ss sr pEnd
    -> SParserChSym  ss sr (WhileChSym chPred pCh pEnd)
sWhileChSym :: forall {s} {r} (chPred :: Char ~> Bool) (ss :: s -> Type)
       (sr :: r -> Type) (pCh :: Char ~> (s ~> PResult s r))
       (pEnd :: s ~> Either PE r).
Lam SChar SBool chPred
-> SParserChSym ss sr pCh
-> SParserEndSym ss sr pEnd
-> SParserChSym ss sr (WhileChSym chPred pCh pEnd)
sWhileChSym Lam SChar SBool chPred
chPred SParserChSym ss sr pCh
pCh SParserEndSym ss sr pEnd
pEnd = LamRep2 SChar ss (SResult ss sr) (WhileChSym chPred pCh pEnd)
-> Lam2 SChar ss (SResult ss sr) (WhileChSym chPred pCh pEnd)
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 ss (SResult ss sr) (WhileChSym chPred pCh pEnd)
 -> Lam2 SChar ss (SResult ss sr) (WhileChSym chPred pCh pEnd))
-> LamRep2 SChar ss (SResult ss sr) (WhileChSym chPred pCh pEnd)
-> Lam2 SChar ss (SResult ss sr) (WhileChSym chPred pCh pEnd)
forall a b. (a -> b) -> a -> b
$ \SChar x
ch ss y
s ->
    case Lam SChar SBool chPred
chPred Lam SChar SBool chPred -> SChar x -> SBool (chPred @@ 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
      SBool (chPred @@ x)
STrue  -> SParserChSym ss sr pCh
pCh SParserChSym ss sr pCh
-> SChar x -> Lam ss (SResult ss sr) (App pCh 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 Lam ss (SResult ss sr) (App pCh x)
-> ss y -> SResult ss sr (App pCh x @@ y)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ ss y
s
      SBool (chPred @@ x)
SFalse ->
        case SParserEndSym ss sr pEnd
pEnd SParserEndSym ss sr pEnd -> ss y -> SResultEnd sr (pEnd @@ y)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ ss y
s of
          SRight sr r1
r -> sr r1 -> SResult ss sr ('Done r1)
forall {r} {s} (sr :: r -> Type) (r1 :: r) (ss :: s -> Type).
sr r1 -> SResult ss sr ('Done r1)
SDone sr r1
r
          SLeft  SE l1
e -> SE (EWhile l1) -> SResult ss sr ('Err (EWhile l1))
forall {s} {r} (e :: PE) (ss :: s -> Type) (sr :: r -> Type).
SE e -> SResult ss sr ('Err e)
SErr (SE (EWhile l1) -> SResult ss sr ('Err (EWhile l1)))
-> SE (EWhile l1) -> SResult ss sr ('Err (EWhile l1))
forall a b. (a -> b) -> a -> b
$ SE l1 -> SE (EWhile l1)
forall (e :: PE). SE e -> SE (EWhile e)
eWhile SE l1
e