{-# LANGUAGE AllowAmbiguousTypes #-} -- For SuccThrowAll uses
{-# 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 =
  ( Branchable repr
  , Raisable repr
  , Inputable repr
  , Joinable repr
  , Routinable repr
  , Stackable repr
  , Readable tok repr
  )

-- ** Type 'ReprInstr'
type ReprInstr = Type -> [Type] -> Type -> Type

-- ** Type 'LetName'
-- | 'TH.Name' of a 'subroutine' 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 'Stackable'
class Stackable (repr::ReprInstr) where
  push ::
    TermInstr v ->
    repr inp (v ': vs) a ->
    repr inp vs a
  pop ::
    repr inp vs a ->
    repr inp (v ': vs) a
  liftI2 ::
    TermInstr (x -> y -> z) ->
    repr inp (z ': vs) a ->
    repr inp (y ': x ': vs) a
  swap ::
    repr inp (x ': y ': vs) a ->
    repr inp (y ': x ': vs) a
  -- | @('mapI' f k)@.
  mapI ::
    TermInstr (x -> y) ->
    repr inp (y ': vs) a ->
    repr inp (x ': vs) a
  mapI f = push f . liftI2 (H.flip H..@ (H.$))
  -- | @('appI' k)@ pops @(x)@ and @(x2y)@ from the 'valueStack',
  -- pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
  appI ::
    repr inp (y ': vs) a ->
    repr inp (x ': (x -> y) ': vs) a
  appI = liftI2 (H.$)

-- ** Class 'Routinable'
class Routinable (repr::ReprInstr) where
  subroutine ::
    LetName v -> repr inp '[] v ->
    repr inp vs a ->
    repr inp vs a
  call ::
    LetName v -> repr inp (v ': vs) a ->
    repr inp vs a
  ret ::
    repr inp '[a] a
  jump ::
    LetName a ->
    repr inp '[] a

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

-- ** Class 'Raisable'
class Raisable (repr::ReprInstr) where
  --type ThrowableConstraint repr (lbl::Symbol) (fs::[(Symbol, Peano)]) :: Constraint
  raise ::
    --ThrowableConstraint repr lbl =>
    KnownSymbol lbl =>
    Proxy lbl ->
    [ErrorItem (InputToken inp)] ->
    repr inp vs a
  fail ::
    --ThrowableConstraint repr "fail" =>
    [ErrorItem (InputToken inp)] ->
    repr inp vs a
  fail = raise (Proxy @"fail")
  popThrow ::
    --ThrowableConstraint repr lbl =>
    KnownSymbol lbl =>
    Proxy lbl ->
    repr inp vs a ->
    repr inp vs a
  catchThrow ::
    --ThrowableConstraint repr lbl =>
    KnownSymbol lbl =>
    Proxy lbl ->
    repr inp vs ret ->
    repr inp (Cursor inp ': vs) ret ->
    repr inp vs ret

-- ** Class 'Inputable'
class Inputable (repr::ReprInstr) where
  loadInput ::
    repr inp vs a ->
    repr inp (Cursor inp ': vs) a
  pushInput ::
    repr inp (Cursor inp ': vs) a ->
    repr inp vs a

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