{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE NoPolyKinds #-}
{-# LANGUAGE ViewPatterns #-}
module Symantic.Parser.Automaton.Instructions where

import Data.Function (($))
import Symantic.Univariant.Trans
import Symantic.Parser.Grammar
import qualified Symantic.Parser.Staging as Hask

{-
class Automatable repr where
  ret :: repr inp '[r] n r a
  push :: x -> repr inp (x ': xs) n r a -> repr inp xs n r a
  pop :: repr inp xs n r a -> repr inp (x ': xs) n r a
-}

data Instr inp xs n r a where
  Ret :: Instr inp '[r] n r a
  Push :: Hask.Haskell x -> Instr inp (x ': xs) n r a -> Instr inp xs n r a
  Pop :: Instr inp xs n r a -> Instr inp (x ': xs) n r a
  Lift2 :: Hask.Haskell (x -> y -> z) -> Instr inp (z : xs) n r a -> Instr inp (y : x : xs) n r a

pattern App :: Instr inp (y : xs) n r a -> Instr inp (x : (x -> y) : xs) n r a
pattern App k = Lift2 (Hask.:$) k


data Automaton inp a x = Automaton { unAutomaton ::
  forall xs n r.
  Instr inp (x ': xs) n r a ->
  Instr inp xs n r a
  }

instance Trans (Grammar) (Automaton inp a) where
  trans g =
    case g of
      Pure x -> Automaton $ \k -> Push x k
      (trans -> Automaton f) :<*> (trans -> Automaton x) ->
        Automaton $ \k -> f (x (App k))