{-# LANGUAGE AllowAmbiguousTypes #-} -- For SuccThrowAll uses
{-# 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 'push') 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

-- Stackable
data instance Instr Stackable repr inp vs 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) a ->
    Instr Stackable repr inp vs a
  -- | @('Pop' k)@ pushes @(x)@ on the 'valueStack'.
  Pop ::
    SomeInstr repr inp vs a ->
    Instr Stackable repr inp (v ': vs) 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) a ->
    Instr Stackable repr inp (y : x : vs) 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) a ->
    Instr Stackable repr inp (y ': x ': vs) a
instance Stackable repr => Trans (Instr Stackable repr inp vs) (repr inp vs) 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 (Instr (Pop i)) = i
  push v i = SomeInstr (Push v i)
  pop = SomeInstr . Pop
  liftI2 f = SomeInstr . LiftI2 f
  swap = SomeInstr . Swap

-- Routinable
data instance Instr Routinable repr inp vs 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 '[] v ->
    SomeInstr repr inp vs a ->
    Instr Routinable repr inp vs a
  -- | @('Jump' n k)@ pass the control-flow to the 'Subroutine' named @(n)@.
  Jump ::
    LetName a ->
    Instr Routinable repr inp '[] 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) a ->
    Instr Routinable repr inp vs a
  -- | @('Ret')@ returns the value stored in a singleton 'valueStack'.
  Ret ::
    Instr Routinable repr inp '[a] a
instance Routinable repr => Trans (Instr Routinable repr inp vs) (repr inp vs) 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

-- Branchable
data instance Instr Branchable repr inp vs a where
  -- | @('Case' l r)@.
  Case ::
    SomeInstr repr inp (x ': vs) a ->
    SomeInstr repr inp (y ': vs) a ->
    Instr Branchable repr inp (Either x y ': vs) a
  -- | @('Choices' ps bs d)@.
  Choices ::
    [TermInstr (v -> Bool)] ->
    [SomeInstr repr inp vs a] ->
    SomeInstr repr inp vs a ->
    Instr Branchable repr inp (v ': vs) a
instance Branchable repr => Trans (Instr Branchable repr inp vs) (repr inp vs) 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

-- Raisable
data instance Instr Raisable repr inp vs a where
  -- | @('Raise' lbl)@ raises labeled error from the 'failStack'.
  Raise ::
    KnownSymbol lbl =>
    Proxy lbl ->
    [ErrorItem (InputToken inp)] ->
    Instr Raisable repr inp vs a
  -- | @('PopThrow' k)@ removes a 'RaiseHandler' from the 'throwListStack' at given label,
  -- and continues with the next 'Instr'uction @(k)@.
  PopThrow ::
    KnownSymbol lbl =>
    Proxy lbl ->
    SomeInstr repr inp vs ret ->
    Instr Raisable repr inp vs ret
  -- | @('CatchThrow' 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.
  CatchThrow ::
    KnownSymbol lbl =>
    Proxy lbl ->
    SomeInstr repr inp vs ret ->
    SomeInstr repr inp (Cursor inp ': vs) ret ->
    Instr Raisable repr inp vs ret
instance Raisable repr => Trans (Instr Raisable repr inp vs) (repr inp vs) where
  trans = \case
    Raise lbl err -> raise lbl err
    PopThrow lbl k -> popThrow lbl (trans k)
    CatchThrow lbl l r -> catchThrow lbl (trans l) (trans r)
instance Raisable repr => Raisable (SomeInstr repr) where
  raise lbl = SomeInstr . Raise lbl
  popThrow lbl = SomeInstr . PopThrow lbl
  catchThrow lbl x = SomeInstr . CatchThrow lbl x

-- Inputable
data instance Instr Inputable repr inp vs 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 a ->
    Instr Inputable repr inp (Cursor inp : vs) 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) a ->
    Instr Inputable repr inp vs a
instance Inputable repr => Trans (Instr Inputable repr inp vs) (repr inp vs) 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

-- Joinable
data instance Instr Joinable repr inp vs a where
  DefJoin ::
    LetName v ->
    SomeInstr repr inp (v ': vs) a ->
    SomeInstr repr inp vs a ->
    Instr Joinable repr inp vs a
  RefJoin ::
    LetName v ->
    Instr Joinable repr inp (v ': vs) a
instance Joinable repr => Trans (Instr Joinable repr inp vs) (repr inp vs) 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

-- Readable
data instance Instr (Readable tok) repr inp vs 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 'Raise'.
  Read ::
    [ErrorItem (InputToken inp)] ->
    TermInstr (InputToken inp -> Bool) ->
    SomeInstr repr inp (InputToken inp ': vs) a ->
    Instr (Readable tok) repr inp vs a
instance
  ( Readable tok repr, tok ~ InputToken inp ) =>
  Trans (Instr (Readable tok) repr inp vs) (repr inp vs) 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