{-# LANGUAGE UndecidableInstances #-}

module Symparsec.Parser where

import DeFun.Core
import GHC.TypeLits ( type Symbol )
import GHC.TypeNats ( type Natural )

import Singleraeh.Demote
import Data.Kind ( type Type )
import GHC.TypeLits ( type SSymbol, fromSSymbol )
import GHC.TypeNats ( type SNat, fromSNat )
import Singleraeh.List
--import Singleraeh.Symbol

-- | Parser state.
data State str n = State
  -- | Remaining input.
  { forall str n. State str n -> str
remaining :: str

  -- | Remaining permitted length.
  --
  -- Must be less than or equal to the actual length of the remaining input.
  -- Parsers must use this field when reading from input:
  --
  -- * if ==0, treat as end of input.
  -- * if  >0 but remaining input is empty, unrecoverable parser error
  --
  -- This extra bookkeeping permits much simpler parser design, specifically for
  -- parsers that act on a substring of the input.
  , forall str n. State str n -> n
length :: n

  -- | Index in the input string.
  --
  -- Overall index. Used for nicer error reporting after parse completion.
  , forall str n. State str n -> n
index :: n
  } deriving stock Int -> State str n -> ShowS
[State str n] -> ShowS
State str n -> String
(Int -> State str n -> ShowS)
-> (State str n -> String)
-> ([State str n] -> ShowS)
-> Show (State str n)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall str n. (Show str, Show n) => Int -> State str n -> ShowS
forall str n. (Show str, Show n) => [State str n] -> ShowS
forall str n. (Show str, Show n) => State str n -> String
$cshowsPrec :: forall str n. (Show str, Show n) => Int -> State str n -> ShowS
showsPrec :: Int -> State str n -> ShowS
$cshow :: forall str n. (Show str, Show n) => State str n -> String
show :: State str n -> String
$cshowList :: forall str n. (Show str, Show n) => [State str n] -> ShowS
showList :: [State str n] -> ShowS
Show

-- | Promoted 'State'.
type PState = State Symbol Natural

-- | Singled 'State'.
data SState (s :: PState) where
    SState :: SSymbol rem -> SNat len -> SNat idx -> SState ('State rem len idx)

-- | Demote an 'SState'.
demoteSState :: SState s -> State String Natural
demoteSState :: forall (s :: PState). SState s -> State String Natural
demoteSState (SState SSymbol rem
srem SNat len
slen SNat idx
sidx) =
    String -> Natural -> Natural -> State String Natural
forall str n. str -> n -> n -> State str n
State (SSymbol rem -> String
forall (s :: Symbol). SSymbol s -> String
fromSSymbol SSymbol rem
srem) (SNat len -> Natural
forall (n :: Natural). SNat n -> Natural
fromSNat SNat len
slen) (SNat idx -> Natural
forall (n :: Natural). SNat n -> Natural
fromSNat SNat idx
sidx)

instance Demotable SState where
    type Demote SState = State String Natural
    demote :: forall (k1 :: PState). SState k1 -> Demote SState
demote = SState k1 -> Demote SState
SState k1 -> State String Natural
forall (s :: PState). SState s -> State String Natural
demoteSState

{-
data Span n = Span
  { start :: n
  , end   :: n
  } deriving stock Show
-}

data Error str = Error
  { forall str. Error str -> [str]
detail :: [str]
  } deriving stock Int -> Error str -> ShowS
[Error str] -> ShowS
Error str -> String
(Int -> Error str -> ShowS)
-> (Error str -> String)
-> ([Error str] -> ShowS)
-> Show (Error str)
forall str. Show str => Int -> Error str -> ShowS
forall str. Show str => [Error str] -> ShowS
forall str. Show str => Error str -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall str. Show str => Int -> Error str -> ShowS
showsPrec :: Int -> Error str -> ShowS
$cshow :: forall str. Show str => Error str -> String
show :: Error str -> String
$cshowList :: forall str. Show str => [Error str] -> ShowS
showList :: [Error str] -> ShowS
Show

-- | Promoted 'Error'.
type PError = Error Symbol

-- | Singled 'Error'.
data SError (e :: PError) where
    SError :: SList SSymbol detail -> SError ('Error detail)

-- | Demote an 'SError'.
demoteSError :: SError e -> Error String
demoteSError :: forall (e :: PError). SError e -> Error String
demoteSError (SError SList SSymbol detail
sdetail) = [String] -> Error String
forall str. [str] -> Error str
Error ([String] -> Error String) -> [String] -> Error String
forall a b. (a -> b) -> a -> b
$ (forall (s :: Symbol). SSymbol s -> String)
-> SList SSymbol detail -> [String]
forall {a} da (sa :: a -> Type) (as :: [a]).
(forall (a1 :: a). sa a1 -> da) -> SList sa as -> [da]
demoteSList SSymbol a1 -> String
forall (s :: Symbol). SSymbol s -> String
fromSSymbol SList SSymbol detail
sdetail

instance Demotable SError where
    type Demote SError = Error String
    demote :: forall (k1 :: PError). SError k1 -> Demote SError
demote = SError k1 -> Demote SError
SError k1 -> Error String
forall (e :: PError). SError e -> Error String
demoteSError

-- | Parser completion: result, and final state.
--
-- TODO: megaparsec also returns a bool indicating if any input was consumed.
-- Unsure what it's used for.
data Reply str n a = Reply
  { forall str n a. Reply str n a -> Result str n a
result :: Result str n a -- ^ Parse result.
  , forall str n a. Reply str n a -> State str n
state  :: State str n    -- ^ Final parser state.
  } deriving stock Int -> Reply str n a -> ShowS
[Reply str n a] -> ShowS
Reply str n a -> String
(Int -> Reply str n a -> ShowS)
-> (Reply str n a -> String)
-> ([Reply str n a] -> ShowS)
-> Show (Reply str n a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall str n a.
(Show a, Show str, Show n) =>
Int -> Reply str n a -> ShowS
forall str n a.
(Show a, Show str, Show n) =>
[Reply str n a] -> ShowS
forall str n a.
(Show a, Show str, Show n) =>
Reply str n a -> String
$cshowsPrec :: forall str n a.
(Show a, Show str, Show n) =>
Int -> Reply str n a -> ShowS
showsPrec :: Int -> Reply str n a -> ShowS
$cshow :: forall str n a.
(Show a, Show str, Show n) =>
Reply str n a -> String
show :: Reply str n a -> String
$cshowList :: forall str n a.
(Show a, Show str, Show n) =>
[Reply str n a] -> ShowS
showList :: [Reply str n a] -> ShowS
Show

-- | Promoted 'Reply'.
type PReply = Reply Symbol Natural

-- | Singled 'Reply'.
data SReply (sa :: a -> Type) (rep :: PReply a) where
    SReply :: SResult sa result -> SState state -> SReply sa ('Reply result state)

-- | Demote an 'SReply.
demoteSReply
    :: (forall a. sa a -> da)
    -> SReply sa rep
    -> Reply String Natural da
demoteSReply :: forall {a} (sa :: a -> Type) da (rep :: PReply a).
(forall (a :: a). sa a -> da)
-> SReply sa rep -> Reply String Natural da
demoteSReply forall (a :: a). sa a -> da
demoteSA (SReply SResult sa result
sresult SState state
sstate) =
    Result String Natural da
-> State String Natural -> Reply String Natural da
forall str n a. Result str n a -> State str n -> Reply str n a
Reply ((forall (a :: a). sa a -> da)
-> SResult sa result -> Result String Natural da
forall {a} (sa :: a -> Type) da (res :: PResult a).
(forall (a :: a). sa a -> da)
-> SResult sa res -> Result String Natural da
demoteSResult sa a -> da
forall (a :: a). sa a -> da
demoteSA SResult sa result
sresult) (SState state -> State String Natural
forall (s :: PState). SState s -> State String Natural
demoteSState SState state
sstate)

instance Demotable sa => Demotable (SReply sa) where
    type Demote (SReply sa) = Reply String Natural (Demote sa)
    demote :: forall (k1 :: PReply a). SReply sa k1 -> Demote (SReply sa)
demote = (forall (a :: a). sa a -> Demote sa)
-> SReply sa k1 -> Reply String Natural (Demote sa)
forall {a} (sa :: a -> Type) da (rep :: PReply a).
(forall (a :: a). sa a -> da)
-> SReply sa rep -> Reply String Natural da
demoteSReply sa a -> Demote sa
forall (a :: a). sa a -> Demote sa
forall k (sk :: k -> Type) (k1 :: k).
Demotable sk =>
sk k1 -> Demote sk
demote

-- | Parse result: a value, or an error.
data Result str n a = OK a            -- ^ Parser succeeded.
                    | Err (Error str) -- ^ Parser failed.
    deriving stock Int -> Result str n a -> ShowS
[Result str n a] -> ShowS
Result str n a -> String
(Int -> Result str n a -> ShowS)
-> (Result str n a -> String)
-> ([Result str n a] -> ShowS)
-> Show (Result str n a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall str k (n :: k) a.
(Show a, Show str) =>
Int -> Result str n a -> ShowS
forall str k (n :: k) a.
(Show a, Show str) =>
[Result str n a] -> ShowS
forall str k (n :: k) a.
(Show a, Show str) =>
Result str n a -> String
$cshowsPrec :: forall str k (n :: k) a.
(Show a, Show str) =>
Int -> Result str n a -> ShowS
showsPrec :: Int -> Result str n a -> ShowS
$cshow :: forall str k (n :: k) a.
(Show a, Show str) =>
Result str n a -> String
show :: Result str n a -> String
$cshowList :: forall str k (n :: k) a.
(Show a, Show str) =>
[Result str n a] -> ShowS
showList :: [Result str n a] -> ShowS
Show

-- | Promoted 'Result'.
type PResult = Result Symbol Natural

--type SState = State 
--type SResult :: _ -> Type
-- TODO ^ how to do explicit kind signature for GADT?

-- | Singled 'Result'.
data SResult (sa :: a -> Type) (res :: PResult a) where
    SOK  :: sa a     -> SResult sa (OK a)
    SErr :: SError e -> SResult sa (Err e)

-- | Demote an 'SResult'.
demoteSResult
    :: (forall a. sa a -> da)
    -> SResult sa res
    -> Result String Natural da
demoteSResult :: forall {a} (sa :: a -> Type) da (res :: PResult a).
(forall (a :: a). sa a -> da)
-> SResult sa res -> Result String Natural da
demoteSResult forall (a :: a). sa a -> da
demoteSA = \case
  SOK  sa a
sa -> da -> Result String Natural da
forall {k} str (n :: k) a. a -> Result str n a
OK  (da -> Result String Natural da) -> da -> Result String Natural da
forall a b. (a -> b) -> a -> b
$ sa a -> da
forall (a :: a). sa a -> da
demoteSA sa a
sa
  SErr SError e
se -> Error String -> Result String Natural da
forall {k} str (n :: k) a. Error str -> Result str n a
Err (Error String -> Result String Natural da)
-> Error String -> Result String Natural da
forall a b. (a -> b) -> a -> b
$ SError e -> Error String
forall (e :: PError). SError e -> Error String
demoteSError SError e
se

instance Demotable sa => Demotable (SResult sa) where
    type Demote (SResult sa) = Result String Natural (Demote sa)
    demote :: forall (k1 :: PResult a). SResult sa k1 -> Demote (SResult sa)
demote = (forall (a :: a). sa a -> Demote sa)
-> SResult sa k1 -> Result String Natural (Demote sa)
forall {a} (sa :: a -> Type) da (res :: PResult a).
(forall (a :: a). sa a -> da)
-> SResult sa res -> Result String Natural da
demoteSResult sa a -> Demote sa
forall (a :: a). sa a -> Demote sa
forall k (sk :: k -> Type) (k1 :: k).
Demotable sk =>
sk k1 -> Demote sk
demote

-- | A parser is a function on parser state.
type Parser str n a = State str n -> Reply str n a

-- | Promoted 'Parser': a defunctionalization symbol to a function on promoted
--   parser state.
type PParser a = PState ~> PReply a

-- | Singled 'Parser'.
type SParser sa p = Lam SState (SReply sa) p
--data SParser (sa :: a -> Type) (p :: PParser a) where
 --   SParser :: Lam SState (SReply sa) (PParser a)

--class SingParser (p :: PParser a) where
--    singParser :: SParser sa p