{-# LANGUAGE ConstraintKinds #-} -- For Executable
{-# LANGUAGE DerivingStrategies #-} -- For Show (LetName a)
{-# LANGUAGE PatternSynonyms #-} -- For Fmap, App, …
{-# LANGUAGE UndecidableInstances #-} -- For Cursorable (Cursor inp)
module Symantic.Parser.Machine.Instructions where

import Data.Bool (Bool(..))
import Data.Either (Either)
import Data.Eq (Eq)
import Data.Ord (Ord)
import Data.Function (($), (.))
import Data.Kind (Type)
import System.IO.Unsafe (unsafePerformIO)
import Text.Show (Show(..), showString)
import qualified Data.Functor as Functor
import qualified Language.Haskell.TH as TH
import qualified Language.Haskell.TH.Syntax as TH
import qualified Symantic.Parser.Grammar.Pure as H

import Symantic.Parser.Grammar
import Symantic.Parser.Machine.Input
import Symantic.Univariant.Trans

-- * Type 'Instr'
-- | 'Instr'uctions for the 'Machine'.
data Instr input valueStack (failStack::Peano) returnValue where
  -- | @('Push' x k)@ pushes @(x)@ on the 'valueStack'
  -- and continues with the next 'Instr'uction @(k)@.
  Push ::
    InstrPure v ->
    Instr inp (v ': vs) es ret ->
    Instr inp vs es ret
  -- | @('Pop' k)@ pushes @(x)@ on the 'valueStack'.
  Pop ::
    Instr inp vs es ret ->
    Instr inp (v ': vs) es ret
  -- | @('LiftI2' f k)@ pops two values from the 'valueStack',
  -- and pushes the result of @(f)@ applied to them.
  LiftI2 ::
    InstrPure (x -> y -> z) ->
    Instr inp (z : vs) es ret ->
    Instr inp (y : x : vs) es ret
  -- | @('Fail')@ raises an error from the 'failStack'.
  Fail ::
    [ErrorItem (InputToken inp)] ->
    Instr inp vs ('Succ es) ret
  -- | @('PopFail' k)@ removes a 'FailHandler' from the 'failStack'
  -- and continues with the next 'Instr'uction @(k)@.
  PopFail ::
    Instr inp vs es ret ->
    Instr inp vs ('Succ es) ret
  -- | @('CatchFail' l r)@ tries the @(l)@ 'Instr'uction
  -- in a new failure scope such that if @(l)@ raises a failure, it is caught,
  -- then the input is pushed as it was before trying @(l)@ on the 'valueStack',
  -- and the control flow goes on with the @(r)@ 'Instr'uction.
  CatchFail ::
    Instr inp vs ('Succ es) ret ->
    Instr inp (Cursor inp ': vs) es ret ->
    Instr inp vs es ret
  -- | @('LoadInput' k)@ removes the input from the 'valueStack'
  -- and continues with the next 'Instr'uction @(k)@ using that input.
  LoadInput ::
    Instr inp vs es r ->
    Instr inp (Cursor inp : vs) es r
  -- | @('PushInput' k)@ pushes the input @(inp)@ on the 'valueStack'
  -- and continues with the next 'Instr'uction @(k)@.
  PushInput ::
    Instr inp (Cursor inp ': vs) es ret ->
    Instr inp vs es ret
  -- | @('Case' l r)@.
  Case ::
    Instr inp (x ': vs) es r ->
    Instr inp (y ': vs) es r ->
    Instr inp (Either x y ': vs) es r
  -- | @('Swap' k)@ pops two values on the 'valueStack',
  -- pushes the first popped-out, then the second,
  -- and continues with the next 'Instr'uction @(k)@.
  Swap ::
    Instr inp (x ': y ': vs) es r ->
    Instr inp (y ': x ': vs) es r
  -- | @('Choices' ps bs d)@.
  Choices ::
    [InstrPure (v -> Bool)] ->
    [Instr inp vs es ret] ->
    Instr inp vs es ret ->
    Instr inp (v ': vs) es ret
  -- | @('Subroutine' n v k)@ binds the 'LetName' @(n)@ to the 'Instr'uction's @(v)@,
  -- 'Call's @(n)@ and
  -- continues with the next 'Instr'uction @(k)@.
  Subroutine ::
    LetName v -> Instr inp '[] ('Succ 'Zero) v ->
    Instr inp vs ('Succ es) ret ->
    Instr inp vs ('Succ es) ret
  -- | @('Jump' n k)@ pass the control-flow to the 'Subroutine' named @(n)@.
  Jump ::
    LetName ret ->
    Instr inp '[] ('Succ es) ret
  -- | @('Call' n k)@ pass the control-flow to the 'Subroutine' named @(n)@,
  -- and when it 'Ret'urns, continues with the next 'Instr'uction @(k)@.
  Call ::
    LetName v ->
    Instr inp (v ': vs) ('Succ es) ret ->
    Instr inp vs ('Succ es) ret
  -- | @('Ret')@ returns the value stored in a singleton 'valueStack'.
  Ret ::
    Instr inp '[ret] es ret
  -- | @('Read' expected p k)@ reads a 'Char' @(c)@ from the 'inp'ut,
  -- if @(p c)@ is 'True' then continues with the next 'Instr'uction @(k)@ on,
  -- otherwise 'Fail'.
  Read ::
    [ErrorItem (InputToken inp)] ->
    InstrPure (InputToken inp -> Bool) ->
    Instr inp (InputToken inp ': vs) ('Succ es) ret ->
    Instr inp vs ('Succ es) ret
  DefJoin ::
    LetName v -> Instr inp (v ': vs) es ret ->
    Instr inp vs es ret ->
    Instr inp vs es ret
  RefJoin ::
    LetName v ->
    Instr inp (v ': vs) es ret

-- ** Type 'InstrPure'
data InstrPure a where
  InstrPureHaskell :: H.CombPure a -> InstrPure a

instance Show (InstrPure a) where
  showsPrec p = \case
    InstrPureHaskell x -> showsPrec p x
    InstrPureSameOffset{} -> showString "InstrPureSameOffset"
instance Trans InstrPure TH.CodeQ where
  trans = \case
    InstrPureHaskell x -> trans x
    InstrPureSameOffset x -> x

-- ** Type 'LetName'
newtype LetName a = LetName { unLetName :: TH.Name }
  deriving (Eq)
  deriving newtype Show

-- * Class 'Executable'
type Executable repr =
  ( Stackable repr
  , Branchable repr
  , Failable repr
  , Inputable repr
  , Routinable repr
  , Joinable repr
  )

-- ** Class 'Stackable'
class Stackable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
  push ::
    InstrPure v ->
    repr inp (v ': vs) n ret ->
    repr inp vs n ret
  pop ::
    repr inp vs n ret ->
    repr inp (v ': vs) n ret
  liftI2 ::
    InstrPure (x -> y -> z) ->
    repr inp (z ': vs) es ret ->
    repr inp (y ': x ': vs) es ret
  swap ::
    repr inp (x ': y ': vs) n r ->
    repr inp (y ': x ': vs) n r

-- ** Class 'Branchable'
class Branchable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
  case_ ::
    repr inp (x ': vs) n r ->
    repr inp (y ': vs) n r ->
    repr inp (Either x y ': vs) n r
  choices ::
    [InstrPure (v -> Bool)] ->
    [repr inp vs es ret] ->
    repr inp vs es ret ->
    repr inp (v ': vs) es ret

-- ** Class 'Failable'
class Failable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
  fail :: [ErrorItem (InputToken inp)] -> repr inp vs ('Succ es) ret
  popFail ::
    repr inp vs es ret ->
    repr inp vs ('Succ es) ret
  catchFail ::
    repr inp vs ('Succ es) ret ->
    repr inp (Cursor inp ': vs) es ret ->
    repr inp vs es ret

-- ** Class 'Inputable'
class Inputable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
  loadInput ::
    repr inp vs es r ->
    repr inp (Cursor inp ': vs) es r
  pushInput ::
    repr inp (Cursor inp ': vs) es ret ->
    repr inp vs es ret

-- ** Class 'Routinable'
class Routinable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
  subroutine ::
    LetName v -> repr inp '[] ('Succ 'Zero) v ->
    repr inp vs ('Succ es) ret ->
    repr inp vs ('Succ es) ret
  call ::
    LetName v -> repr inp (v ': vs) ('Succ es) ret ->
    repr inp vs ('Succ es) ret
  ret ::
    repr inp '[ret] es ret
  jump ::
    LetName ret ->
    repr inp '[] ('Succ es) ret

-- ** Class 'Joinable'
class Joinable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
  defJoin ::
    LetName v ->
    repr inp (v ': vs) es ret ->
    repr inp vs es ret ->
    repr inp vs es ret
  refJoin ::
    LetName v ->
    repr inp (v ': vs) es ret

-- ** Class 'Readable'
class Readable (repr :: Type -> [Type] -> Peano -> Type -> Type) (tok::Type) where
  read ::
    tok ~ InputToken inp =>
    [ErrorItem tok] ->
    InstrPure (tok -> Bool) ->
    repr inp (tok ': vs) ('Succ es) ret ->
    repr inp vs ('Succ es) ret

instance
  ( Executable repr
  , Readable repr (InputToken inp)
  ) => Trans (Instr inp vs es) (repr inp vs es) where
  trans = \case
    Push x k -> push x (trans k)
    Pop k -> pop (trans k)
    LiftI2 f k -> liftI2 f (trans k)
    Fail err -> fail err
    PopFail k -> popFail (trans k)
    CatchFail l r -> catchFail (trans l) (trans r)
    LoadInput k -> loadInput (trans k)
    PushInput k -> pushInput (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)
    Subroutine n sub k -> subroutine n (trans sub) (trans k)
    Jump n -> jump n
    Call n k -> call n (trans k)
    Ret -> ret
    Read es p k -> read es p (trans k)
    DefJoin n sub k -> defJoin n (trans sub) (trans k)
    RefJoin n -> refJoin n

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

-- | @('Fmap' f k)@.
pattern Fmap ::
  InstrPure (x -> y) ->
  Instr inp (y ': xs) es ret ->
  Instr inp (x ': xs) es ret
pattern Fmap f k = Push f (LiftI2 (InstrPureHaskell (H.Flip H.:@ (H.:$))) k)

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

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

-- * Type 'Machine'
-- | Making the control-flow explicit.
data Machine inp v = Machine { unMachine ::
  forall vs es ret.
  {-k-}Instr inp (v ': vs) ('Succ es) ret ->
  Instr inp vs ('Succ es) ret
  }

runMachine ::
  forall inp v es repr.
  Executable repr =>
  Readable repr (InputToken inp) =>
  Machine inp v -> repr inp '[] ('Succ es) v
runMachine (Machine auto) =
  trans @(Instr inp '[] ('Succ es)) $
  auto Ret

instance Applicable (Machine inp) where
  pure x = Machine $ Push (InstrPureHaskell x)
  Machine f <*> Machine x = Machine $ f . x . App
  liftA2 f (Machine x) (Machine y) = Machine $
    x . y . LiftI2 (InstrPureHaskell f)
  Machine x *> Machine y = Machine $ x . Pop . y
  Machine x <* Machine y = Machine $ x . y . Pop
instance
  Cursorable (Cursor inp) =>
  Alternable (Machine inp) where
  empty = Machine $ \_k -> Fail []
  Machine l <|> Machine r = Machine $ \k ->
    makeJoin k $ \j ->
    CatchFail
      (l (PopFail j))
      (failIfConsumed (r j))
  try (Machine x) = Machine $ \k ->
    CatchFail (x (PopFail k))
      -- On exception, reset the input,
      -- and propagate the failure.
      (LoadInput (Fail []))

-- | If no input has been consumed by the failing alternative
-- then continue with the given continuation.
-- Otherwise, propagate the 'Fail'ure.
failIfConsumed ::
  Cursorable (Cursor inp) =>
  Instr inp vs ('Succ es) ret ->
  Instr inp (Cursor inp : vs) ('Succ es) ret
failIfConsumed k = PushInput (LiftI2 (InstrPureSameOffset sameOffset) (If k (Fail [])))

-- | @('makeJoin' k f)@ factorizes @(k)@ in @(f)@,
-- by introducing a 'DefJoin' if necessary,
-- and passing the corresponding 'RefJoin' to @(f)@,
-- or @(k)@ as is when factorizing is useless.
makeJoin ::
  Instr inp (v : vs) es ret ->
  (Instr inp (v : vs) es ret -> Instr inp vs es ret) ->
  Instr inp vs es ret
-- Double RefJoin Optimization:
-- If a join-node points directly to another join-node,
-- then reuse it
makeJoin k@RefJoin{} = ($ k)
-- Terminal RefJoin Optimization:
-- If a join-node points directly to a terminal operation,
-- then it's useless to introduce a join-point.
makeJoin k@Ret = ($ k)
makeJoin k =
  let joinName = LetName $ unsafePerformIO $ TH.qNewName "join" in
  \f -> DefJoin joinName k (f (RefJoin joinName))

instance tok ~ InputToken inp => Satisfiable (Machine inp) tok where
  satisfy es p = Machine $ Read es (InstrPureHaskell p)
instance Selectable (Machine inp) where
  branch (Machine lr) (Machine l) (Machine r) = Machine $ \k ->
    makeJoin k $ \j ->
    lr (Case (l (Swap (App j)))
             (r (Swap (App j))))
instance Matchable (Machine inp) where
  conditional ps bs (Machine m) (Machine default_) = Machine $ \k ->
    makeJoin k $ \j ->
    m (Choices (InstrPureHaskell Functor.<$> ps)
               ((\b -> unMachine b j) Functor.<$> bs)
               (default_ j))
instance
  ( Ord (InputToken inp)
  , Cursorable (Cursor inp)
  ) => Lookable (Machine inp) where
  look (Machine x) = Machine $ \k ->
    PushInput (x (Swap (LoadInput k)))
  eof = negLook (satisfy [{-discarded by negLook-}] (H.const H..@ H.bool True))
        -- Set a better failure message
        <|> (Machine $ \_k -> Fail [ErrorItemEnd])
  negLook (Machine x) = Machine $ \k ->
    CatchFail
      -- On x success, discard the result,
      -- and replace this 'CatchFail''s failure handler
      -- by a 'Fail'ure whose 'farthestExpecting' is negated,
      -- then a failure is raised from the input
      -- when entering 'negLook', to avoid odd cases:
      -- - where the failure that made (negLook x)
      --   succeed can get the blame for the overall
      --   failure of the grammar.
      -- - where the overall failure of
      --   the grammar might be blamed on something in x
      --   that, if corrected, still makes x succeed and
      --   (negLook x) fail.
      (PushInput (x (Pop (PopFail (LoadInput (Fail []))))))
      -- On x failure, reset the input,
      -- and go on with the next 'Instr'uctions.
      (LoadInput (Push (InstrPureHaskell H.unit) k))
instance Letable TH.Name (Machine inp) where
  def n v = Machine $ \k ->
    Subroutine (LetName n) (unMachine v Ret) (Call (LetName n) k)
  ref _isRec n = Machine $ \case
    Ret -> Jump (LetName n)
    k -> Call (LetName n) k
instance Cursorable (Cursor inp) => Foldable (Machine inp) where
  {-
  chainPre op p = go <*> p
    where go = (H..) <$> op <*> go <|> pure H.id
  chainPost p op = p <**> go
    where go = (H..) <$> op <*> go <|> pure H.id
  -}