{-# LANGUAGE ConstraintKinds #-} -- For Machine
{-# LANGUAGE DeriveLift #-} -- For TH.Lift (Failure tok)
{-# 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 Data.Set (Set)
import Text.Show (Show(..))
import Data.String (String)
import qualified Language.Haskell.TH as TH

import Symantic.Parser.Grammar
import Symantic.Parser.Machine.Input
import qualified Symantic.Lang as Prod
import qualified Symantic.Data as Sym

-- * Type 'Splice'
type Splice = Sym.SomeData TH.CodeQ

-- | Lift a 'TH.CodeQ' into a 'Sym.SomeData'.
splice :: TH.CodeQ a -> Splice a
splice x = Sym.SomeData (Sym.Var x)

-- ** 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 'InstrComment'
class InstrComment (repr::ReprInstr) where
  comment :: String -> repr inp vs a -> repr inp vs a

-- ** Class 'InstrValuable'
class InstrValuable (repr::ReprInstr) where
  -- | @('pushValue' x k)@ pushes @(x)@ on the 'valueStack'
  -- and continues with the next 'Instr'uction @(k)@.
  pushValue ::
    Splice v ->
    repr inp (v ': vs) a ->
    repr inp vs a
  -- | @('popValue' k)@ pushes @(x)@ on the 'valueStack'.
  popValue ::
    repr inp vs a ->
    repr inp (v ': vs) a
  -- | @('lift2Value' f k)@ pops two values from the 'valueStack',
  -- and pushes the result of @(f)@ applied to them.
  lift2Value ::
    Splice (x -> y -> z) ->
    repr inp (z ': vs) a ->
    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 ::
    repr inp (x ': y ': vs) a ->
    repr inp (y ': x ': vs) a
  -- | @('mapValue' f k)@.
  mapValue ::
    Splice (x -> y) ->
    repr inp (y ': vs) a ->
    repr inp (x ': vs) a
  mapValue f = pushValue f . lift2Value (Prod.flip Prod..@ (Prod.$))
  -- | @('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 (Prod.$)

-- ** Class 'InstrExceptionable'
class InstrExceptionable (repr::ReprInstr) where
  -- | @('raise' exn)@ raises 'ExceptionLabel' @(exn)@.
  raise :: ExceptionLabel -> repr inp vs a
  -- | @('fail' fs)@ raises 'ExceptionFailure' @(exn)@.
  -- As a special case, giving an empty 'Set' of failures
  -- raises 'ExceptionFailure' without using the current position
  -- to update the farthest error.
  fail :: Set SomeFailure -> repr inp vs a
  -- | @('commit' exn k)@ removes the 'Catcher'
  -- from the 'catchStackByLabel' for the given 'Exception' @(exn)@,
  -- and continues with the next 'Instr'uction @(k)@.
  commit :: Exception -> repr inp vs a -> repr inp vs a
  -- | @('catch' exn l r)@ tries the @(l)@ 'Instr'uction
  -- in a new failure scope such that if @(l)@ raises an exception within @(exn)@, it is caught,
  -- then the input (and its 'Horizon') is pushed
  -- as it was before trying @(l)@ on the 'valueStack' (resp. on the 'horizonStack'),
  -- and the control flow goes on with the @(r)@ 'Instr'uction.
  catch ::
    Exception ->
    {-scope-}repr inp vs ret ->
    {-catcher-}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 ::
    [(Splice (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 [(Prod.id, ok)] ko

-- ** Class 'InstrCallable'
class InstrCallable (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 ::
    LetBindings TH.Name (repr inp '[]) ->
    repr inp vs a ->
    repr inp vs a
  -- | @('call' isRec n k)@ pass the control-flow to the 'DefLet' named @(n)@,
  -- and when it 'Ret'urns, continues with the next 'Instr'uction @(k)@.
  call ::
    Bool ->
    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' isRec n k)@ pass the control-flow to the 'DefLet' named @(n)@.
  jump ::
    Bool ->
    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
  -- | @('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
  -- | @('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

-- ** Class 'InstrReadable'
class InstrReadable (tok::Type) (repr::ReprInstr) where
  -- | @('read' fs p k)@ reads a 'Char' @(c)@ from the input,
  -- if @(p c)@ is 'True' then continues with the next 'Instr'uction @(k)@,
  -- otherwise 'fail'.
  read ::
    tok ~ InputToken inp =>
    Set SomeFailure ->
    Splice (tok -> Bool) ->
    repr inp (tok ': vs) a ->
    repr inp vs a

-- ** Class 'InstrIterable'
class InstrIterable (repr::ReprInstr) where
  -- | @('iter' loop done)@.
  iter ::
    LetName a ->
    repr inp '[] a ->
    repr inp (Cursor inp ': vs) a ->
    repr inp vs a

-- ** Class 'InstrRegisterable'
class InstrRegisterable (repr::ReprInstr) where
  newRegister ::
    UnscopedRegister v ->
    repr inp vs a ->
    repr inp (v : vs) a
  readRegister ::
    UnscopedRegister v ->
    repr inp (v : vs) a ->
    repr inp vs a
  writeRegister ::
    UnscopedRegister v ->
    repr inp vs a ->
    repr inp (v : vs) a

-- | @('modifyRegister' reg k)@
-- modifies the content of register @(reg)@
-- with the function at the 'valueStackHead',
-- then continues with @(k)@.
modifyRegister ::
  InstrRegisterable repr =>
  InstrValuable repr =>
  UnscopedRegister v -> repr inp vs a -> repr inp ((v -> v) : vs) a
modifyRegister r = readRegister r . applyValue . writeRegister r