{-# 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 { forall a. LetName a -> Name
unLetName :: TH.Name }
  deriving LetName a -> LetName a -> Bool
(LetName a -> LetName a -> Bool)
-> (LetName a -> LetName a -> Bool) -> Eq (LetName a)
forall a. LetName a -> LetName a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LetName a -> LetName a -> Bool
$c/= :: forall a. LetName a -> LetName a -> Bool
== :: LetName a -> LetName a -> Bool
$c== :: forall a. LetName a -> LetName a -> Bool
Eq
  deriving newtype Int -> LetName a -> ShowS
[LetName a] -> ShowS
LetName a -> String
(Int -> LetName a -> ShowS)
-> (LetName a -> String)
-> ([LetName a] -> ShowS)
-> Show (LetName a)
forall a. Int -> LetName a -> ShowS
forall a. [LetName a] -> ShowS
forall a. LetName a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LetName a] -> ShowS
$cshowList :: forall a. [LetName a] -> ShowS
show :: LetName a -> String
$cshow :: forall a. LetName a -> String
showsPrec :: Int -> LetName a -> ShowS
$cshowsPrec :: forall a. Int -> LetName a -> ShowS
Show

-- ** Class 'Stackable'
class Stackable (repr::ReprInstr) where
  push ::
    TermInstr v ->
    repr inp (v ': vs) es a ->
    repr inp vs es a
  pop ::
    repr inp vs es a ->
    repr inp (v ': vs) es 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) es a ->
    repr inp (y ': x ': vs) es a
  -- | @('mapI' f k)@.
  mapI ::
    TermInstr (x -> y) ->
    repr inp (y ': vs) es a ->
    repr inp (x ': vs) es a
  mapI TermInstr (x -> y)
f = TermInstr (x -> y)
-> repr inp ((x -> y) : x : vs) es a -> repr inp (x : vs) es a
forall (repr :: ReprInstr) v inp (vs :: [*]) (es :: Peano) a.
Stackable repr =>
TermInstr v -> repr inp (v : vs) es a -> repr inp vs es a
push TermInstr (x -> y)
f (repr inp ((x -> y) : x : vs) es a -> repr inp (x : vs) es a)
-> (repr inp (y : vs) es a -> repr inp ((x -> y) : x : vs) es a)
-> repr inp (y : vs) es a
-> repr inp (x : vs) es a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermInstr (x -> (x -> y) -> y)
-> repr inp (y : vs) es a -> repr inp ((x -> y) : x : vs) es a
forall (repr :: ReprInstr) x y z inp (vs :: [*]) (es :: Peano) a.
Stackable repr =>
TermInstr (x -> y -> z)
-> repr inp (z : vs) es a -> repr inp (y : x : vs) es a
liftI2 (Term CodeQ (((x -> y) -> x -> y) -> x -> (x -> y) -> y)
forall (repr :: * -> *) a b c.
Termable repr =>
repr ((a -> b -> c) -> b -> a -> c)
H.flip Term CodeQ (((x -> y) -> x -> y) -> x -> (x -> y) -> y)
-> Term CodeQ ((x -> y) -> x -> y)
-> TermInstr (x -> (x -> y) -> y)
forall (repr :: * -> *) a b.
Termable repr =>
repr (a -> b) -> repr a -> repr b
H..@ Term CodeQ ((x -> y) -> x -> y)
forall (repr :: * -> *) a b.
Termable repr =>
repr ((a -> b) -> a -> b)
(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 = TermInstr ((x -> y) -> x -> y)
-> repr inp (y : vs) es a -> repr inp (x : (x -> y) : vs) es a
forall (repr :: ReprInstr) x y z inp (vs :: [*]) (es :: Peano) a.
Stackable repr =>
TermInstr (x -> y -> z)
-> repr inp (z : vs) es a -> repr inp (y : x : vs) es a
liftI2 TermInstr ((x -> y) -> x -> y)
forall (repr :: * -> *) a b.
Termable repr =>
repr ((a -> b) -> a -> b)
(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) es r ->
    repr inp (y ': vs) es r ->
    repr inp (Either x y ': vs) es 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 repr inp vs es a
ok repr inp vs es a
ko = [TermInstr (Bool -> Bool)]
-> [repr inp vs es a]
-> repr inp vs es a
-> repr inp (Bool : vs) es a
forall (repr :: ReprInstr) v inp (vs :: [*]) (es :: Peano) a.
Branchable repr =>
[TermInstr (v -> Bool)]
-> [repr inp vs es a] -> repr inp vs es a -> repr inp (v : vs) es a
choices [TermInstr (Bool -> Bool)
forall (repr :: * -> *) a. Termable repr => repr (a -> a)
H.id] [repr inp vs es a
ok] repr inp vs es a
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