src/Symantic/Parser/Automaton/Instructions.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE NoPolyKinds #-}
   3 {-# LANGUAGE PatternSynonyms #-}
   4 {-# LANGUAGE ViewPatterns #-}
   5 module Symantic.Parser.Automaton.Instructions where
   6
   7 import Data.Bool (Bool)
   8 import Data.Either (Either)
   9 import Data.Function (($), (.))
  10 import Symantic.Parser.Grammar
  11 import qualified Data.Functor as Functor
  12 import qualified Symantic.Parser.Staging as Hask
  13
  14 {-
  15 class Automatable repr where
  16   ret :: repr inp '[ret] n ret a
  17   push :: x -> repr inp (x ': vs) n ret a -> repr inp vs n ret a
  18   pop :: repr inp vs n ret a -> repr inp (x ': vs) n ret a
  19 -}
  20
  21 class InputPosition inp where
  22
  23 -- * Type 'Instr'
  24 -- | 'Instr'uctions for the 'Automaton'.
  25 data Instr input valueStack (exceptionStack::Peano) returnValue a where
  26   -- | @('Ret')@ returns the value in a singleton value-stack.
  27   Ret :: Instr inp '[ret] es ret a
  28   -- | @('Push' x k)@ pushes @(x)@ on the value-stack and continues with the next 'Instr'uction @(k)@.
  29   Push :: InstrPure x -> Instr inp (x ': vs) es ret a -> Instr inp vs es ret a
  30   -- | @('Pop' k)@ pushes @(x)@ on the value-stack.
  31   Pop :: Instr inp vs es ret a -> Instr inp (x ': vs) es ret a
  32   -- | @('Lift2' f k)@ pops two values from the value-stack, and pushes the result of @(f)@ applied to them.
  33   Lift2 :: InstrPure (x -> y -> z) -> Instr inp (z : vs) es ret a -> Instr inp (y : x : vs) es ret a
  34   -- | @('Fail')@ raises an error from the exception-stack.
  35   Fail :: Instr inp vs ('Succ es) ret a
  36   -- | @('Commit' k)@ removes an exception from the exception-stack and continues with the next 'Instr'uction @(k)@.
  37   Commit :: Instr inp vs es ret a -> Instr inp vs ('Succ es) ret a
  38   -- | @('Catch' l r)@ tries the @(l)@ 'Instr'uction, if it raises an exception, catches it, pushes the input on the value-stack and continues with the @(r)@ 'Instr'uction.
  39   Catch :: Instr inp vs ('Succ es) ret a -> Instr inp (inp ': vs) es ret a -> Instr inp vs es ret a
  40   -- | @('Seek' k)@ removes the input from the value-stack and continues with the next 'Instr'uction @(k)@.
  41   Seek :: Instr inp vs es r a -> Instr inp (inp : vs) es r a
  42   -- | @('Tell' k)@ pushes the input @(inp)@ on the value-stack and continues with the next 'Instr'uction @(k)@.
  43   Tell :: Instr inp (inp ': vs) es ret a -> Instr inp vs es ret a
  44   Case :: Instr inp (x : vs) n r a -> Instr inp (y : vs) n r a -> Instr inp (Either x y : vs) n r a
  45   -- | @('Swap' k)@ pops two values on the value-stack, pushes the first popped-out, then the second, and continues with the next 'Instr'uction @(k)@.
  46   Swap :: Instr inp (x : y : vs) n r a -> Instr inp (y : x : vs) n r a
  47   Choices :: [InstrPure (x -> Bool)] -> [Instr inp vs es ret a] -> Instr inp vs es ret a -> Instr inp (x ': vs) es ret a
  48
  49 -- ** Type 'InstrPure'
  50 data InstrPure a
  51   =  InstrPureHaskell (Hask.Haskell a)
  52   |  InstrPureSameOffset
  53
  54 -- ** Type 'Peano'
  55 -- | Type-level natural numbers, using the Peano recursive encoding.
  56 data Peano = Zero | Succ Peano
  57
  58 -- | @('App' k)@ pops @(x)@ and @(x2y)@ from the value-stack, pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
  59 pattern App :: Instr inp (y : vs) es ret a -> Instr inp (x : (x -> y) : vs) es ret a
  60 pattern App k = Lift2 (InstrPureHaskell (Hask.:$)) k
  61
  62 -- | @('If' ok ko)@ pops a 'Bool' from the value-stack and continues either with the 'Instr'uction @(ok)@ if it is 'True' or @(ko)@ otherwise.
  63 pattern If :: Instr inp vs es ret a -> Instr inp vs es ret a -> Instr inp (Bool ': vs) es ret a
  64 pattern If ok ko = Choices [InstrPureHaskell Hask.Id] [ok] ko
  65
  66 parsecHandler :: InputPosition inp => Instr inp vs ('Succ es) ret a -> Instr inp (inp : vs) ('Succ es) ret a
  67 parsecHandler k = Tell (Lift2 InstrPureSameOffset (If k Fail))
  68
  69 -- * Type 'Automaton'
  70 -- | Making the control-flow explicit.
  71 data Automaton inp a x = Automaton { unAutomaton ::
  72   forall vs es ret.
  73   {-next-}Instr inp (x ': vs) ('Succ es) ret a ->
  74   Instr inp vs ('Succ es) ret a
  75   }
  76
  77 instance Applicable (Automaton inp a) where
  78   pure x = Automaton $ Push (InstrPureHaskell x)
  79   Automaton f <*> Automaton x = Automaton $ f . x . App
  80   liftA2 f (Automaton x) (Automaton y) = Automaton $
  81     x . y . Lift2 (InstrPureHaskell f)
  82   Automaton x *> Automaton y = Automaton $ x . Pop . y
  83   Automaton x <* Automaton y = Automaton $ x . y . Pop
  84 instance
  85   InputPosition inp =>
  86   Alternable (Automaton inp a) where
  87   empty = Automaton $ \_k -> Fail
  88   Automaton l <|> Automaton r = Automaton $ \k ->
  89     -- TODO: join points
  90     Catch (l (Commit k)) (parsecHandler (r k))
  91   try (Automaton x) = Automaton $ \k ->
  92     Catch (x (Commit k)) (Seek Fail)
  93 instance Selectable (Automaton inp a) where
  94   branch (Automaton lr) (Automaton l) (Automaton r) =
  95     Automaton $ \k ->
  96       -- TODO: join points
  97       lr (Case (l (Swap (App k)))
  98                (r (Swap (App k))))
  99 instance Matchable (Automaton inp a) where
 100   conditional ps bs (Automaton a) (Automaton def) =
 101     Automaton $ \k ->
 102       -- TODO: join points
 103       a (Choices (InstrPureHaskell Functor.<$> ps) ((\b -> unAutomaton b k) Functor.<$> bs) (def k))