{-# LANGUAGE ConstraintKinds #-} -- For Executable
{-# LANGUAGE DerivingStrategies #-} -- For Show (LetName a)
{-# LANGUAGE PatternSynonyms #-} -- For Instr
{-# LANGUAGE ViewPatterns #-} -- For unSomeInstr
module Symantic.Parser.Machine.Instructions where

import Data.Bool (Bool(..))
import Data.Either (Either)
import Data.Eq (Eq(..))
import Data.Maybe (Maybe(..))
import Data.Function ((.))
import Data.Kind (Constraint, Type)
import Type.Reflection (Typeable, typeRep, eqTypeRep, (:~~:)(..))
import Text.Show (Show(..))
import qualified Data.Functor as Functor
import qualified Language.Haskell.TH as TH
import qualified Symantic.Parser.Haskell as H

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

-- * Type 'TermInstr'
type TermInstr = H.Term TH.CodeQ

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

-- * Class 'Executable'
-- | All the 'Instr'uctions.
type Executable tok repr =
  ( Branchable repr
  , Failable repr
  , Inputable repr
  , Joinable repr
  , Routinable repr
  , Stackable repr
  , Readable tok repr
  )

-- * Data family 'Instr'
-- | 'Instr'uctions for the 'Machine'.
-- This is an extensible data-type.
data family Instr
  (instr :: ReprInstr -> Constraint)
  (repr :: ReprInstr)
  :: ReprInstr

-- | Convenient utility to pattern-match a 'SomeInstr'.
pattern Instr :: Typeable comb =>
  Instr comb repr inp vs es a ->
  SomeInstr repr inp vs es a
pattern Instr x <- (unSomeInstr -> Just x)

-- ** Type 'ReprInstr'
type ReprInstr = Type -> [Type] -> Peano -> Type -> Type

-- ** Type 'SomeInstr'
-- | Some 'Instr'uction existantialized over the actual instruction symantic class.
-- Useful to handle a list of 'Instr'uctions
-- without requiring impredicative quantification.
-- Must be used by pattern-matching
-- on the 'SomeInstr' data-constructor,
-- to bring the constraints in scope.
data SomeInstr repr inp vs es a =
  forall instr.
  (Trans (Instr instr repr inp vs es) (repr inp vs es), Typeable instr) =>
  SomeInstr (Instr instr repr inp vs es a)

instance Trans (SomeInstr repr inp vs es) (repr inp vs es) where
  trans (SomeInstr x) = trans x

-- | @(unSomeInstr i :: 'Maybe' ('Instr' comb repr inp vs es a))@
-- extract the data-constructor from the given 'SomeInstr'
-- iif. it belongs to the @('Instr' comb repr a)@ data-instance.
unSomeInstr ::
  forall instr repr inp vs es a.
  Typeable instr =>
  SomeInstr repr inp vs es a ->
  Maybe (Instr instr repr inp vs es a)
unSomeInstr (SomeInstr (i::Instr i repr inp vs es a)) =
  case typeRep @instr `eqTypeRep` typeRep @i of
    Just HRefl -> Just i
    Nothing -> Nothing

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

-- ** Class 'Stackable'
class Stackable (repr::ReprInstr) where
  push ::
    TermInstr 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 ::
    TermInstr (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
data instance Instr Stackable repr inp vs fs a where
  -- | @('Push' x k)@ pushes @(x)@ on the 'valueStack'
  -- and continues with the next 'Instr'uction @(k)@.
  Push ::
    TermInstr v ->
    SomeInstr repr inp (v ': vs) es a ->
    Instr Stackable repr inp vs es a
  -- | @('Pop' k)@ pushes @(x)@ on the 'valueStack'.
  Pop ::
    SomeInstr repr inp vs es a ->
    Instr Stackable repr inp (v ': vs) es a
  -- | @('LiftI2' f k)@ pops two values from the 'valueStack',
  -- and pushes the result of @(f)@ applied to them.
  LiftI2 ::
    TermInstr (x -> y -> z) ->
    SomeInstr repr inp (z : vs) es a ->
    Instr Stackable repr inp (y : x : vs) es a
  -- | @('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 ::
    SomeInstr repr inp (x ': y ': vs) es a ->
    Instr Stackable repr inp (y ': x ': vs) es a
instance Stackable repr => Trans (Instr Stackable repr 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)
    Swap k -> swap (trans k)
instance Stackable repr => Stackable (SomeInstr repr) where
  push v = SomeInstr . Push v
  pop = SomeInstr . Pop
  liftI2 f = SomeInstr . LiftI2 f
  swap = SomeInstr . Swap

-- | @('mapI' f k)@.
mapI ::
  Stackable repr =>
  TermInstr (x -> y) ->
  SomeInstr repr inp (y ': vs) es ret ->
  SomeInstr repr inp (x ': vs) es ret
mapI f = push f . liftI2 (H.flip H..@ (H.$))

-- | @('appI' k)@ pops @(x)@ and @(x2y)@ from the 'valueStack',
-- pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
appI ::
  Stackable repr =>
  SomeInstr repr inp (y ': vs) es a ->
  SomeInstr repr inp (x ': (x -> y) ': vs) es a
appI = liftI2 (H.$)

-- ** Class 'Routinable'
class Routinable (repr::ReprInstr) 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
data instance Instr Routinable repr inp vs fs a where
  -- | @('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 -> SomeInstr repr inp '[] ('Succ 'Zero) v ->
    SomeInstr repr inp vs ('Succ es) a ->
    Instr Routinable repr inp vs ('Succ es) a
  -- | @('Jump' n k)@ pass the control-flow to the 'Subroutine' named @(n)@.
  Jump ::
    LetName a ->
    Instr Routinable repr inp '[] ('Succ es) a
  -- | @('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 ->
    SomeInstr repr inp (v ': vs) ('Succ es) a ->
    Instr Routinable repr inp vs ('Succ es) a
  -- | @('Ret')@ returns the value stored in a singleton 'valueStack'.
  Ret ::
    Instr Routinable repr inp '[a] es a
instance Routinable repr => Trans (Instr Routinable repr inp vs es) (repr inp vs es) where
  trans = \case
    Subroutine n sub k -> subroutine n (trans sub) (trans k)
    Jump n -> jump n
    Call n k -> call n (trans k)
    Ret -> ret
instance Routinable repr => Routinable (SomeInstr repr) where
  subroutine n sub = SomeInstr . Subroutine n sub
  jump = SomeInstr . Jump
  call n = SomeInstr . Call n
  ret = SomeInstr Ret

-- ** Class 'Branchable'
class Branchable (repr::ReprInstr) where
  caseI ::
    repr inp (x ': vs) n r ->
    repr inp (y ': vs) n r ->
    repr inp (Either x y ': vs) n r
  choices ::
    [TermInstr (v -> Bool)] ->
    [repr inp vs es ret] ->
    repr inp vs es ret ->
    repr inp (v ': vs) es ret
data instance Instr Branchable repr inp vs fs a where
  -- | @('Case' l r)@.
  Case ::
    SomeInstr repr inp (x ': vs) es a ->
    SomeInstr repr inp (y ': vs) es a ->
    Instr Branchable repr inp (Either x y ': vs) es a
  -- | @('Choices' ps bs d)@.
  Choices ::
    [TermInstr (v -> Bool)] ->
    [SomeInstr repr inp vs es a] ->
    SomeInstr repr inp vs es a ->
    Instr Branchable repr inp (v ': vs) es a
instance Branchable repr => Trans (Instr Branchable repr inp vs es) (repr inp vs es) where
  trans = \case
    Case l r -> caseI (trans l) (trans r)
    Choices ps bs d -> choices ps (trans Functor.<$> bs) (trans d)
instance Branchable repr => Branchable (SomeInstr repr) where
  caseI l = SomeInstr . Case l
  choices ps bs = SomeInstr . Choices ps bs

-- | @('ifI' ok ko)@ pops a 'Bool' from the 'valueStack'
-- and continues either with the 'Instr'uction @(ok)@ if it is 'True'
-- or @(ko)@ otherwise.
ifI ::
  Branchable repr =>
  SomeInstr repr inp vs es a ->
  SomeInstr repr inp vs es a ->
  SomeInstr repr inp (Bool ': vs) es a
ifI ok ko = SomeInstr (Choices [H.id] [ok] ko)

-- ** Class 'Failable'
class Failable (repr::ReprInstr) 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
data instance Instr Failable repr inp vs fs a where
  -- | @('Fail')@ raises an error from the 'failStack'.
  Fail ::
    [ErrorItem (InputToken inp)] ->
    Instr Failable repr inp vs ('Succ es) a
  -- | @('PopFail' k)@ removes a 'FailHandler' from the 'failStack'
  -- and continues with the next 'Instr'uction @(k)@.
  PopFail ::
    SomeInstr repr inp vs es ret ->
    Instr Failable repr 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 ::
    SomeInstr repr inp vs ('Succ es) ret ->
    SomeInstr repr inp (Cursor inp ': vs) es ret ->
    Instr Failable repr inp vs es ret
instance Failable repr => Trans (Instr Failable repr inp vs es) (repr inp vs es) where
  trans = \case
    Fail err -> fail err
    PopFail k -> popFail (trans k)
    CatchFail l r -> catchFail (trans l) (trans r)
instance Failable repr => Failable (SomeInstr repr) where
  fail = SomeInstr . Fail
  popFail = SomeInstr . PopFail
  catchFail x = SomeInstr . CatchFail x

-- ** Class 'Inputable'
class Inputable (repr::ReprInstr) where
  loadInput ::
    repr inp vs es a ->
    repr inp (Cursor inp ': vs) es a
  pushInput ::
    repr inp (Cursor inp ': vs) es a ->
    repr inp vs es a
data instance Instr Inputable repr inp vs fs a where
  -- | @('LoadInput' k)@ removes the input from the 'valueStack'
  -- and continues with the next 'Instr'uction @(k)@ using that input.
  LoadInput ::
    SomeInstr repr inp vs es a ->
    Instr Inputable repr inp (Cursor inp : vs) es a
  -- | @('PushInput' k)@ pushes the input @(inp)@ on the 'valueStack'
  -- and continues with the next 'Instr'uction @(k)@.
  PushInput ::
    SomeInstr repr inp (Cursor inp ': vs) es a ->
    Instr Inputable repr inp vs es a
instance Inputable repr => Trans (Instr Inputable repr inp vs es) (repr inp vs es) where
  trans = \case
    LoadInput k -> loadInput (trans k)
    PushInput k -> pushInput (trans k)
instance Inputable repr => Inputable (SomeInstr repr) where
  loadInput = SomeInstr . LoadInput
  pushInput = SomeInstr . PushInput

-- ** Class 'Joinable'
class Joinable (repr::ReprInstr) where
  defJoin ::
    LetName v ->
    repr inp (v ': vs) es a ->
    repr inp vs es a ->
    repr inp vs es a
  refJoin ::
    LetName v ->
    repr inp (v ': vs) es a
data instance Instr Joinable repr inp vs fs a where
  DefJoin ::
    LetName v -> SomeInstr repr inp (v ': vs) es a ->
    SomeInstr repr inp vs es a ->
    Instr Joinable repr inp vs es a
  RefJoin ::
    LetName v ->
    Instr Joinable repr inp (v ': vs) es a
instance Joinable repr => Trans (Instr Joinable repr inp vs es) (repr inp vs es) where
  trans = \case
    DefJoin n sub k -> defJoin n (trans sub) (trans k)
    RefJoin n -> refJoin n
instance Joinable repr => Joinable (SomeInstr repr) where
  defJoin n sub = SomeInstr . DefJoin n sub
  refJoin = SomeInstr . RefJoin

-- ** Class 'Readable'
class Readable (tok::Type) (repr::ReprInstr) where
  read ::
    tok ~ InputToken inp =>
    [ErrorItem tok] ->
    TermInstr (tok -> Bool) ->
    repr inp (tok ': vs) ('Succ es) ret ->
    repr inp vs ('Succ es) ret
data instance Instr (Readable tok) repr inp vs fs a where
  -- | @('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)] ->
    TermInstr (InputToken inp -> Bool) ->
    SomeInstr repr inp (InputToken inp ': vs) ('Succ es) a ->
    Instr (Readable tok) repr inp vs ('Succ es) a
instance
  ( Readable tok repr, tok ~ InputToken inp ) =>
  Trans (Instr (Readable tok) repr inp vs es) (repr inp vs es) where
  trans = \case
    Read es p k -> read es p (trans k)
instance
  ( Readable tok repr, Typeable tok ) =>
  Readable tok (SomeInstr repr) where
  read es p = SomeInstr . Read es p