{-# LANGUAGE ConstraintKinds #-} -- For Executable
{-# LANGUAGE DerivingStrategies #-} -- For Show (LetName a)
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

-- | @(isInstr @instr i)@ returns a proof
-- that @(i)@ is within the extension @(instr)@
-- of the 'Instr' data-type, or 'Nothing' if it is not.
isInstr ::
  forall (instr0 :: ReprInstr -> Constraint) instr1 repr inp vs es a.
  Typeable instr0 =>
  Typeable instr1 =>
  Instr instr1 repr inp vs es a -> Maybe (instr0:~~:instr1)
isInstr _i = eqTypeRep (typeRep @instr0) (typeRep @instr1)

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

-- ** Type 'SomeInstr'
-- | Some 'Instr'uction existentialized over the actual instruction data-type.
-- 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

-- ** 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