{-# LANGUAGE PatternSynonyms #-} -- For Instr
{-# LANGUAGE ViewPatterns #-} -- For unSomeInstr
-- | 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.Function ((.))
import Data.Kind (Constraint)
import Data.Maybe (Maybe(..))
import Data.Set (Set)
import Type.Reflection (Typeable, typeRep, eqTypeRep, (:~~:)(..))
import qualified Data.Functor as Functor
import qualified Language.Haskell.TH as TH

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

import Debug.Trace

-- * Data family 'Instr'
-- | 'Instr'uctions of the 'Machine'.
-- This is an extensible data-type.
data family Instr
  (instr :: ReprInstr -> Constraint)
  :: 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 undestandable 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 ::
    Splice v ->
    SomeInstr repr inp (v ': vs) a ->
    Instr InstrValuable repr inp vs a
  PopValue ::
    SomeInstr repr inp vs a ->
    Instr InstrValuable repr inp (v ': vs) a
  Lift2Value ::
    Splice (x -> y -> z) ->
    SomeInstr repr inp (z : vs) a ->
    Instr InstrValuable repr inp (y : x : vs) a
  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 -> trace "trans.pushValue" (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
  Raise ::
    ExceptionLabel ->
    Instr InstrExceptionable repr inp vs a
  Fail ::
    Set SomeFailure ->
    Instr InstrExceptionable repr inp vs a
  Commit ::
    Exception ->
    SomeInstr repr inp vs ret ->
    Instr InstrExceptionable repr inp vs ret
  Catch ::
    Exception ->
    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
    Raise exn -> raise exn
    Fail fs -> fail fs
    Commit exn k -> commit exn (trans k)
    Catch exn l r -> catch exn (trans l) (trans r)
instance InstrExceptionable repr => InstrExceptionable (SomeInstr repr) where
  raise = SomeInstr . Raise
  fail = SomeInstr . Fail
  commit exn = SomeInstr . Commit exn
  catch exn x = SomeInstr . Catch exn 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 ::
    [Splice (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

-- InstrCallable
data instance Instr InstrCallable repr inp vs a where
  DefLet ::
    LetBindings TH.Name (SomeInstr repr inp '[]) ->
    SomeInstr repr inp vs a ->
    Instr InstrCallable repr inp vs a
  Call ::
    LetName v ->
    SomeInstr repr inp (v ': vs) a ->
    Instr InstrCallable repr inp vs a
  Ret ::
    Instr InstrCallable repr inp '[a] a
  Jump ::
    LetName a ->
    Instr InstrCallable repr inp '[] a
instance InstrCallable repr => Trans (Instr InstrCallable repr inp vs) (repr inp vs) where
  trans = \case
    DefLet subs k -> defLet ((\(SomeLet sub) -> SomeLet (trans sub)) Functor.<$> subs) (trans k)
    Jump n -> jump n
    Call n k -> call n (trans k)
    Ret -> ret
instance InstrCallable repr => InstrCallable (SomeInstr repr) where
  defLet subs = SomeInstr . DefLet subs
  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
  PushInput ::
    SomeInstr repr inp (Cursor inp ': vs) a ->
    Instr InstrInputable repr inp vs a
  LoadInput ::
    SomeInstr repr inp vs a ->
    Instr InstrInputable repr inp (Cursor inp ': vs) a
instance InstrInputable repr => Trans (Instr InstrInputable repr inp vs) (repr inp vs) where
  trans = \case
    PushInput k -> pushInput (trans k)
    LoadInput k -> loadInput (trans k)
instance InstrInputable repr => InstrInputable (SomeInstr repr) where
  pushInput = SomeInstr . PushInput
  loadInput = SomeInstr . LoadInput

-- InstrReadable
data instance Instr (InstrReadable tok) repr inp vs a where
  Read ::
    Set SomeFailure ->
    Splice (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 fs p k -> read fs p (trans k)
instance
  ( InstrReadable tok repr, Typeable tok ) =>
  InstrReadable tok (SomeInstr repr) where
  read fs p = SomeInstr . Read fs p