{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoPolyKinds #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
module Symantic.Parser.Automaton.Instructions where

import Data.Bool (Bool)
import Data.Either (Either)
import Data.Function (($), (.))
import Symantic.Parser.Grammar
import qualified Data.Functor as Functor
import qualified Symantic.Parser.Staging as Hask
import Symantic.Univariant.Trans

-- * Class 'InputPosition'
-- | TODO
class InputPosition inp where

-- * Type 'Instr'
-- | 'Instr'uctions for the 'Automaton'.
data Instr input valueStack (exceptionStack::Peano) returnValue a where
  -- | @('Ret')@ returns the value in a singleton value-stack.
  Ret :: Instr inp '[ret] es ret a
  -- | @('Push' x k)@ pushes @(x)@ on the value-stack and continues with the next 'Instr'uction @(k)@.
  Push :: InstrPure x -> Instr inp (x ': vs) es ret a -> Instr inp vs es ret a
  -- | @('Pop' k)@ pushes @(x)@ on the value-stack.
  Pop :: Instr inp vs es ret a -> Instr inp (x ': vs) es ret a
  -- | @('LiftI2' f k)@ pops two values from the value-stack, and pushes the result of @(f)@ applied to them.
  LiftI2 :: InstrPure (x -> y -> z) -> Instr inp (z : vs) es ret a -> Instr inp (y : x : vs) es ret a
  -- | @('Fail')@ raises an error from the exception-stack.
  Fail :: Instr inp vs ('Succ es) ret a
  -- | @('Commit' k)@ removes an exception from the exception-stack and continues with the next 'Instr'uction @(k)@.
  Commit :: Instr inp vs es ret a -> Instr inp vs ('Succ es) ret a
  -- | @('Catch' l r)@ tries the @(l)@ 'Instr'uction, if it raises an exception, catches it, pushes the input on the value-stack and continues with the @(r)@ 'Instr'uction.
  Catch :: Instr inp vs ('Succ es) ret a -> Instr inp (inp ': vs) es ret a -> Instr inp vs es ret a
  -- | @('Seek' k)@ removes the input from the value-stack and continues with the next 'Instr'uction @(k)@.
  Seek :: Instr inp vs es r a -> Instr inp (inp : vs) es r a
  -- | @('Tell' k)@ pushes the input @(inp)@ on the value-stack and continues with the next 'Instr'uction @(k)@.
  Tell :: Instr inp (inp ': vs) es ret a -> Instr inp vs es ret a
  -- | @('Case' l r)@.
  Case :: Instr inp (x ': vs) n r a -> Instr inp (y ': vs) n r a -> Instr inp (Either x y ': vs) n r a
  -- | @('Swap' k)@ pops two values on the value-stack, pushes the first popped-out, then the second, and continues with the next 'Instr'uction @(k)@.
  Swap :: Instr inp (x ': y ': vs) n r a -> Instr inp (y ': x ': vs) n r a
  -- | @('Choices' ps bs d)@.
  Choices :: [InstrPure (x -> Bool)] -> [Instr inp vs es ret a] -> Instr inp vs es ret a -> Instr inp (x ': vs) es ret a

-- ** Type 'InstrPure'
data InstrPure a
  =  InstrPureHaskell (Hask.Haskell a)
  |  InstrPureSameOffset

-- * Class 'Executable'
-- | Tagless-Final encoding of 'Instr'uctions.
class Executable repr where
  ret :: repr inp '[ret] (n::Peano) ret a
  push :: InstrPure x -> repr inp (x ': vs) n ret a -> repr inp vs n ret a
  pop :: repr inp vs n ret a -> repr inp (x ': vs) n ret a
  liftI2 :: InstrPure (x -> y -> z) -> repr inp (z ': vs) es ret a -> repr inp (y ': x ': vs) es ret a
  fail :: repr inp vs ('Succ es) ret a
  commit :: repr inp vs es ret a -> repr inp vs ('Succ es) ret a
  catch :: repr inp vs ('Succ es) ret a -> repr inp (inp ': vs) es ret a -> repr inp vs es ret a
  seek :: repr inp vs es r a -> repr inp (inp ': vs) es r a
  tell :: repr inp (inp ': vs) es ret a -> repr inp vs es ret a
  case_ :: repr inp (x ': vs) n r a -> repr inp (y ': vs) n r a -> repr inp (Either x y ': vs) n r a
  swap :: repr inp (x ': y ': vs) n r a -> repr inp (y ': x ': vs) n r a
  choices :: [InstrPure (x -> Bool)] -> [repr inp vs es ret a] -> repr inp vs es ret a -> repr inp (x ': vs) es ret a

instance
  Executable repr =>
  Trans (Instr inp vs es ret) (repr inp vs es ret) where
  trans = \case
    Ret -> ret
    Push x k -> push x (trans k)
    Pop k -> pop (trans k)
    LiftI2 f k -> liftI2 f (trans k)
    Fail -> fail
    Commit k -> commit (trans k)
    Catch l r -> catch (trans l) (trans r)
    Seek k -> seek (trans k)
    Tell k -> tell (trans k)
    Case l r -> case_ (trans l) (trans r)
    Swap k -> swap (trans k)
    Choices ps bs d -> choices ps (trans Functor.<$> bs) (trans d)


-- ** Type 'Peano'
-- | Type-level natural numbers, using the Peano recursive encoding.
data Peano = Zero | Succ Peano

-- | @('App' k)@ pops @(x)@ and @(x2y)@ from the value-stack, pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
pattern App :: Instr inp (y : vs) es ret a -> Instr inp (x : (x -> y) : vs) es ret a
pattern App k = LiftI2 (InstrPureHaskell (Hask.:$)) k

-- | @('If' ok ko)@ pops a 'Bool' from the value-stack and continues either with the 'Instr'uction @(ok)@ if it is 'True' or @(ko)@ otherwise.
pattern If :: Instr inp vs es ret a -> Instr inp vs es ret a -> Instr inp (Bool ': vs) es ret a
pattern If ok ko = Choices [InstrPureHaskell Hask.Id] [ok] ko

parsecHandler :: InputPosition inp => Instr inp vs ('Succ es) ret a -> Instr inp (inp : vs) ('Succ es) ret a
parsecHandler k = Tell (LiftI2 InstrPureSameOffset (If k Fail))

-- * Type 'Automaton'
-- | Making the control-flow explicit.
data Automaton inp a x = Automaton { unAutomaton ::
  forall vs es ret.
  {-next-}Instr inp (x ': vs) ('Succ es) ret a ->
  Instr inp vs ('Succ es) ret a
  }

automaton ::
  forall inp a es repr.
  Executable repr =>
  Automaton inp a a -> (repr inp '[] ('Succ es) a) a
automaton =
  trans @(Instr inp '[] ('Succ es) a) .
  ($ Ret) .
  unAutomaton

instance Applicable (Automaton inp a) where
  pure x = Automaton $ Push (InstrPureHaskell x)
  Automaton f <*> Automaton x = Automaton $ f . x . App
  liftA2 f (Automaton x) (Automaton y) = Automaton $
    x . y . LiftI2 (InstrPureHaskell f)
  Automaton x *> Automaton y = Automaton $ x . Pop . y
  Automaton x <* Automaton y = Automaton $ x . y . Pop
instance
  InputPosition inp =>
  Alternable (Automaton inp a) where
  empty = Automaton $ \_k -> Fail
  Automaton l <|> Automaton r = Automaton $ \k ->
    -- TODO: join points
    Catch (l (Commit k)) (parsecHandler (r k))
  try (Automaton x) = Automaton $ \k ->
    Catch (x (Commit k)) (Seek Fail)
instance Selectable (Automaton inp a) where
  branch (Automaton lr) (Automaton l) (Automaton r) = Automaton $ \k ->
    -- TODO: join points
    lr (Case (l (Swap (App k)))
             (r (Swap (App k))))
instance Matchable (Automaton inp a) where
  conditional ps bs (Automaton a) (Automaton def) =
    Automaton $ \k ->
      -- TODO: join points
      a (Choices (InstrPureHaskell Functor.<$> ps) ((\b -> unAutomaton b k) Functor.<$> bs) (def k))
instance Lookable (Automaton inp a) where
  look (Automaton x) = Automaton $ \k ->
    Tell (x (Swap (Seek k)))
  negLook (Automaton x) = Automaton $ \k ->
    Catch (Tell (x (Pop (Seek (Commit Fail)))))
          (Seek (Push (InstrPureHaskell Hask.unit) k))