{-# LANGUAGE ConstraintKinds #-} -- For Machine
{-# LANGUAGE DerivingStrategies #-} -- For Show (LetName a)
-- | Semantic of the parsing instructions used
-- to make the parsing control-flow explicit,
-- in the convenient tagless-final encoding.
module Symantic.Parser.Machine.Instructions where

import Data.Bool (Bool(..))
import Data.Either (Either)
import Data.Eq (Eq(..))
import Data.Function ((.))
import Data.Kind (Type)
import GHC.TypeLits (KnownSymbol)
import Text.Show (Show(..))
import Data.Proxy (Proxy(..))
import qualified Language.Haskell.TH as TH
import qualified Symantic.Parser.Haskell as H

import Symantic.Parser.Grammar
import Symantic.Parser.Machine.Input

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

-- * Class 'Machine'
-- | All the 'Instr'uctions.
type Machine tok repr =
  ( InstrBranchable repr
  , InstrExceptionable repr
  , InstrInputable repr
  , InstrJoinable repr
  , InstrLetable repr
  , InstrValuable repr
  , InstrReadable tok repr
  )

-- ** Type 'ReprInstr'
type ReprInstr = {-input-}Type -> {-valueStack-}[Type] -> {-a-}Type -> Type

-- ** Type 'LetName'
-- | 'TH.Name' of a 'defLet' or 'defJoin'
-- indexed by the return type of the factorized 'Instr'uctions.
-- This helps type-inferencing.
newtype LetName a = LetName { unLetName :: TH.Name }
  deriving Eq
  deriving newtype Show

-- ** Class 'InstrValuable'
class InstrValuable (repr::ReprInstr) where
  pushValue ::
    TermInstr v ->
    repr inp (v ': vs) a ->
    repr inp vs a
  popValue ::
    repr inp vs a ->
    repr inp (v ': vs) a
  lift2Value ::
    TermInstr (x -> y -> z) ->
    repr inp (z ': vs) a ->
    repr inp (y ': x ': vs) a
  swapValue ::
    repr inp (x ': y ': vs) a ->
    repr inp (y ': x ': vs) a
  -- | @('mapValue' f k)@.
  mapValue ::
    TermInstr (x -> y) ->
    repr inp (y ': vs) a ->
    repr inp (x ': vs) a
  mapValue f = pushValue f . lift2Value (H.flip H..@ (H.$))
  -- | @('applyValue' k)@ pops @(x)@ and @(x2y)@ from the 'valueStack',
  -- pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
  applyValue ::
    repr inp (y ': vs) a ->
    repr inp (x ': (x -> y) ': vs) a
  applyValue = lift2Value (H.$)

-- ** Class 'InstrExceptionable'
class InstrExceptionable (repr::ReprInstr) where
  -- | @('raiseException' lbl es)@ raises labeled error from the 'failStack'.
  raiseException ::
    KnownSymbol lbl =>
    Proxy lbl ->
    [ErrorItem (InputToken inp)] ->
    repr inp vs a
  -- | Like using 'raiseException' with the @"fail"@ label.
  fail ::
    [ErrorItem (InputToken inp)] ->
    repr inp vs a
  fail = raiseException (Proxy @"fail")
  -- | @('popException' lbl k)@ removes a 'Catcher'
  -- from the @catchStackByLabel@ at given label,
  -- and continues with the next 'Instr'uction @(k)@.
  popException ::
    KnownSymbol lbl =>
    Proxy lbl ->
    repr inp vs a ->
    repr inp vs a
  -- | @('catchException' lbl 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.
  catchException ::
    KnownSymbol lbl =>
    Proxy lbl ->
    repr inp vs ret ->
    repr inp (Cursor inp ': vs) ret ->
    repr inp vs ret

-- ** Class 'InstrBranchable'
class InstrBranchable (repr::ReprInstr) where
  -- | @('caseBranch' l r)@.
  caseBranch ::
    repr inp (x ': vs) r ->
    repr inp (y ': vs) r ->
    repr inp (Either x y ': vs) r
  -- | @('choicesBranch' ps bs d)@.
  choicesBranch ::
    [TermInstr (v -> Bool)] ->
    [repr inp vs a] ->
    repr inp vs a ->
    repr inp (v ': vs) a
  -- | @('ifBranch' ok ko)@ pops a 'Bool' from the 'valueStack'
  -- and continues either with the 'Instr'uction @(ok)@ if it is 'True'
  -- or @(ko)@ otherwise.
  ifBranch ::
    repr inp vs a ->
    repr inp vs a ->
    repr inp (Bool ': vs) a
  ifBranch ok ko = choicesBranch [H.id] [ok] ko

-- ** Class 'InstrLetable'
class InstrLetable (repr::ReprInstr) where
  -- | @('defLet' n v k)@ binds the 'LetName' @(n)@ to the 'Instr'uction's @(v)@,
  -- 'Call's @(n)@ and
  -- continues with the next 'Instr'uction @(k)@.
  defLet ::
    LetName v -> repr inp '[] v ->
    repr inp vs a ->
    repr inp vs a
  -- | @('call' n k)@ pass the control-flow to the 'DefLet' named @(n)@,
  -- and when it 'Ret'urns, continues with the next 'Instr'uction @(k)@.
  call ::
    LetName v -> repr inp (v ': vs) a ->
    repr inp vs a
  -- | @('ret')@ returns the value stored in a singleton 'valueStack'.
  ret ::
    repr inp '[a] a
  -- | @('jump' n k)@ pass the control-flow to the 'DefLet' named @(n)@.
  jump ::
    LetName a ->
    repr inp '[] a

-- ** Class 'InstrJoinable'
class InstrJoinable (repr::ReprInstr) where
  defJoin ::
    LetName v -> repr inp (v ': vs) a ->
    repr inp vs a ->
    repr inp vs a
  refJoin ::
    LetName v ->
    repr inp (v ': vs) a

-- ** Class 'InstrInputable'
class InstrInputable (repr::ReprInstr) where
  -- | @('loadInput' k)@ removes the input from the 'valueStack'
  -- and continues with the next 'Instr'uction @(k)@ using that input.
  loadInput ::
    repr inp vs a ->
    repr inp (Cursor inp ': vs) a
  -- | @('pushInput' k)@ pushes the input @(inp)@ on the 'valueStack'
  -- and continues with the next 'Instr'uction @(k)@.
  pushInput ::
    repr inp (Cursor inp ': vs) a ->
    repr inp vs a

-- ** Class 'InstrReadable'
class InstrReadable (tok::Type) (repr::ReprInstr) 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 'RaiseException'.
  read ::
    tok ~ InputToken inp =>
    [ErrorItem tok] ->
    TermInstr (tok -> Bool) ->
    repr inp (tok ': vs) a ->
    repr inp vs a