{-# LANGUAGE PatternSynonyms #-} -- For Instr
{-# LANGUAGE ViewPatterns #-} -- For unSomeInstr
{-# LANGUAGE UndecidableInstances #-}
-- | Initial encoding with bottom-up optimizations of 'Instr'uctions,
-- re-optimizing downward as needed after each optimization.
-- There is only one optimization (for 'pushValue') so far,
-- but the introspection enabled by the 'Instr' data-type
-- is also useful to optimize with more context in the 'Machine'.
module Symantic.Parser.Machine.Optimize where

import Data.Bool (Bool(..))
import Data.Either (Either)
import Data.Maybe (Maybe(..))
import Data.Function ((.))
import Data.Kind (Constraint)
import Data.Proxy (Proxy(..))
import GHC.TypeLits (KnownSymbol)
import Type.Reflection (Typeable, typeRep, eqTypeRep, (:~~:)(..))
import qualified Data.Functor as Functor

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

-- * Data family 'Instr'
-- | 'Instr'uctions of 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 a ->
  SomeInstr repr inp vs a
pattern Instr x <- (unSomeInstr -> Just x)

-- ** Type 'SomeInstr'
-- | Some 'Instr'uction existentialized 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.
--
-- As in 'SomeComb', a first pass of optimizations
-- is directly applied in it
-- to avoid introducing an extra newtype,
-- this also give a more comprehensible code.
data SomeInstr repr inp vs a =
  forall instr.
  (Trans (Instr instr repr inp vs) (repr inp vs), Typeable instr) =>
  SomeInstr (Instr instr repr inp vs a)

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

-- | @(unSomeInstr i :: 'Maybe' ('Instr' comb repr inp vs 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 a.
  Typeable instr =>
  SomeInstr repr inp vs a ->
  Maybe (Instr instr repr inp vs a)
unSomeInstr (SomeInstr (i::Instr i repr inp vs a)) =
  case typeRep @instr `eqTypeRep` typeRep @i of
    Just HRefl -> Just i
    Nothing -> Nothing

-- InstrValuable
data instance Instr InstrValuable repr inp vs a where
  -- | @('PushValue' x k)@ pushes @(x)@ on the 'valueStack'
  -- and continues with the next 'Instr'uction @(k)@.
  PushValue ::
    TermInstr v ->
    SomeInstr repr inp (v ': vs) a ->
    Instr InstrValuable repr inp vs a
  -- | @('PopValue' k)@ pushes @(x)@ on the 'valueStack'.
  PopValue ::
    SomeInstr repr inp vs a ->
    Instr InstrValuable repr inp (v ': vs) a
  -- | @('Lift2Value' f k)@ pops two values from the 'valueStack',
  -- and pushes the result of @(f)@ applied to them.
  Lift2Value ::
    TermInstr (x -> y -> z) ->
    SomeInstr repr inp (z : vs) a ->
    Instr InstrValuable repr inp (y : x : vs) a
  -- | @('SwapValue' k)@ pops two values on the 'valueStack',
  -- pushes the first popped-out, then the second,
  -- and continues with the next 'Instr'uction @(k)@.
  SwapValue ::
    SomeInstr repr inp (x ': y ': vs) a ->
    Instr InstrValuable repr inp (y ': x ': vs) a
instance InstrValuable repr => Trans (Instr InstrValuable repr inp vs) (repr inp vs) where
  trans = \case
    PushValue x k -> pushValue x (trans k)
    PopValue k -> popValue (trans k)
    Lift2Value f k -> lift2Value f (trans k)
    SwapValue k -> swapValue (trans k)
instance InstrValuable repr => InstrValuable (SomeInstr repr) where
  pushValue _v (Instr (PopValue i)) = i
  pushValue v i = SomeInstr (PushValue v i)
  popValue = SomeInstr . PopValue
  lift2Value f = SomeInstr . Lift2Value f
  swapValue = SomeInstr . SwapValue

-- InstrExceptionable
data instance Instr InstrExceptionable repr inp vs a where
  RaiseException ::
    KnownSymbol lbl =>
    Proxy lbl ->
    [ErrorItem (InputToken inp)] ->
    Instr InstrExceptionable repr inp vs a
  PopException ::
    KnownSymbol lbl =>
    Proxy lbl ->
    SomeInstr repr inp vs ret ->
    Instr InstrExceptionable repr inp vs ret
  CatchException ::
    KnownSymbol lbl =>
    Proxy lbl ->
    SomeInstr repr inp vs ret ->
    SomeInstr repr inp (Cursor inp ': vs) ret ->
    Instr InstrExceptionable repr inp vs ret
instance InstrExceptionable repr => Trans (Instr InstrExceptionable repr inp vs) (repr inp vs) where
  trans = \case
    RaiseException lbl err -> raiseException lbl err
    PopException lbl k -> popException lbl (trans k)
    CatchException lbl l r -> catchException lbl (trans l) (trans r)
instance InstrExceptionable repr => InstrExceptionable (SomeInstr repr) where
  raiseException lbl = SomeInstr . RaiseException lbl
  popException lbl = SomeInstr . PopException lbl
  catchException lbl x = SomeInstr . CatchException lbl x

-- InstrBranchable
data instance Instr InstrBranchable repr inp vs a where
  CaseBranch ::
    SomeInstr repr inp (x ': vs) a ->
    SomeInstr repr inp (y ': vs) a ->
    Instr InstrBranchable repr inp (Either x y ': vs) a
  ChoicesBranch ::
    [TermInstr (v -> Bool)] ->
    [SomeInstr repr inp vs a] ->
    SomeInstr repr inp vs a ->
    Instr InstrBranchable repr inp (v ': vs) a
instance InstrBranchable repr => Trans (Instr InstrBranchable repr inp vs) (repr inp vs) where
  trans = \case
    CaseBranch l r -> caseBranch (trans l) (trans r)
    ChoicesBranch ps bs d -> choicesBranch ps (trans Functor.<$> bs) (trans d)
instance InstrBranchable repr => InstrBranchable (SomeInstr repr) where
  caseBranch l = SomeInstr . CaseBranch l
  choicesBranch ps bs = SomeInstr . ChoicesBranch ps bs

-- InstrLetable
data instance Instr InstrLetable repr inp vs a where
  DefLet ::
    LetName v ->
    SomeInstr repr inp '[] v ->
    SomeInstr repr inp vs a ->
    Instr InstrLetable repr inp vs a
  Call ::
    LetName v ->
    SomeInstr repr inp (v ': vs) a ->
    Instr InstrLetable repr inp vs a
  Ret ::
    Instr InstrLetable repr inp '[a] a
  Jump ::
    LetName a ->
    Instr InstrLetable repr inp '[] a
instance InstrLetable repr => Trans (Instr InstrLetable repr inp vs) (repr inp vs) where
  trans = \case
    DefLet n sub k -> defLet n (trans sub) (trans k)
    Jump n -> jump n
    Call n k -> call n (trans k)
    Ret -> ret
instance InstrLetable repr => InstrLetable (SomeInstr repr) where
  defLet n sub = SomeInstr . DefLet n sub
  jump = SomeInstr . Jump
  call n = SomeInstr . Call n
  ret = SomeInstr Ret

-- InstrJoinable
data instance Instr InstrJoinable repr inp vs a where
  DefJoin ::
    LetName v ->
    SomeInstr repr inp (v ': vs) a ->
    SomeInstr repr inp vs a ->
    Instr InstrJoinable repr inp vs a
  RefJoin ::
    LetName v ->
    Instr InstrJoinable repr inp (v ': vs) a
instance InstrJoinable repr => Trans (Instr InstrJoinable repr inp vs) (repr inp vs) where
  trans = \case
    DefJoin n sub k -> defJoin n (trans sub) (trans k)
    RefJoin n -> refJoin n
instance InstrJoinable repr => InstrJoinable (SomeInstr repr) where
  defJoin n sub = SomeInstr . DefJoin n sub
  refJoin = SomeInstr . RefJoin

-- InstrInputable
data instance Instr InstrInputable repr inp vs a where
  LoadInput ::
    SomeInstr repr inp vs a ->
    Instr InstrInputable repr inp (Cursor inp : vs) a
  PushInput ::
    SomeInstr repr inp (Cursor inp ': vs) a ->
    Instr InstrInputable repr inp vs a
instance InstrInputable repr => Trans (Instr InstrInputable repr inp vs) (repr inp vs) where
  trans = \case
    LoadInput k -> loadInput (trans k)
    PushInput k -> pushInput (trans k)
instance InstrInputable repr => InstrInputable (SomeInstr repr) where
  loadInput = SomeInstr . LoadInput
  pushInput = SomeInstr . PushInput

-- InstrReadable
data instance Instr (InstrReadable tok) repr inp vs a where
  Read ::
    [ErrorItem (InputToken inp)] ->
    TermInstr (InputToken inp -> Bool) ->
    SomeInstr repr inp (InputToken inp ': vs) a ->
    Instr (InstrReadable tok) repr inp vs a
instance
  ( InstrReadable tok repr, tok ~ InputToken inp ) =>
  Trans (Instr (InstrReadable tok) repr inp vs) (repr inp vs) where
  trans = \case
    Read es p k -> read es p (trans k)
instance
  ( InstrReadable tok repr, Typeable tok ) =>
  InstrReadable tok (SomeInstr repr) where
  read es p = SomeInstr . Read es p