{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DerivingStrategies #-}
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 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 = H.Term TH.CodeQ
data Peano = Zero | Succ Peano
type Machine tok repr =
( Branchable repr
, Failable repr
, Inputable repr
, Joinable repr
, Routinable repr
, Stackable repr
, Readable tok repr
)
type ReprInstr = Type -> [Type] -> Peano -> Type -> Type
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 (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 ::
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 ::
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 (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 (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 ::
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 (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 (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 (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 (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