{-# 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 (Symbol)
import Text.Show (Show(..))
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

-- * Type 'Peano'
-- | Type-level natural numbers,
-- using the Peano recursive encoding.
data Peano = Zero | Succ Peano

-- * Class 'Machine'
-- | All the 'Instr'uctions.
type Machine tok repr =
  ( Branchable repr
  , Failable repr
  , Inputable repr
  , Joinable repr
  , Routinable repr
  , Stackable repr
  , Readable tok repr
  )

-- ** Type 'ReprInstr'
type ReprInstr = Type -> [Type] -> Peano -> 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) n a ->
    repr inp vs n a
  pop ::
    repr inp vs n a ->
    repr inp (v ': vs) n a
  liftI2 ::
    TermInstr (x -> y -> z) ->
    repr inp (z ': vs) es a ->
    repr inp (y ': x ': vs) es a
  swap ::
    repr inp (x ': y ': vs) n r ->
    repr inp (y ': x ': vs) n r
  -- | @('mapI' f k)@.
  mapI ::
    TermInstr (x -> y) ->
    repr inp (y ': vs) es a ->
    repr inp (x ': vs) es 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) es a ->
    repr inp (x ': (x -> y) ': vs) es a
  appI = liftI2 (H.$)

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

-- ** Class 'Branchable'
class Branchable (repr::ReprInstr) where
  caseI ::
    repr inp (x ': vs) n r ->
    repr inp (y ': vs) n r ->
    repr inp (Either x y ': vs) n r
  choices ::
    [TermInstr (v -> Bool)] ->
    [repr inp vs es a] ->
    repr inp vs es a ->
    repr inp (v ': vs) es 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 es a ->
    repr inp vs es a ->
    repr inp (Bool ': vs) es a
  ifI ok ko = choices [H.id] [ok] ko

-- ** Class 'Failable'
class Failable (repr::ReprInstr) where
  fail ::
    [ErrorItem (InputToken inp)] ->
    repr inp vs ('Succ es) a
  popFail ::
    repr inp vs es a ->
    repr inp vs ('Succ es) a
  catchFail ::
    repr inp vs ('Succ es) a ->
    repr inp (Cursor inp ': vs) es a ->
    repr inp vs es a

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

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

-- ** Class 'Readable'
class Readable (tok::Type) (repr::ReprInstr) where
  read ::
    tok ~ InputToken inp =>
    [ErrorItem tok] ->
    TermInstr (tok -> Bool) ->
    repr inp (tok ': vs) ('Succ es) a ->
    repr inp vs ('Succ es) a