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 import Symantic.Univariant.Trans
  14
  15 -- * Class 'InputPosition'
  16 -- | TODO
  17 class InputPosition inp where
  18
  19 -- * Type 'Instr'
  20 -- | 'Instr'uctions for the 'Automaton'.
  21 data Instr input valueStack (exceptionStack::Peano) returnValue a where
  22   -- | @('Ret')@ returns the value in a singleton value-stack.
  23   Ret :: Instr inp '[ret] es ret a
  24   -- | @('Push' x k)@ pushes @(x)@ on the value-stack and continues with the next 'Instr'uction @(k)@.
  25   Push :: InstrPure x -> Instr inp (x ': vs) es ret a -> Instr inp vs es ret a
  26   -- | @('Pop' k)@ pushes @(x)@ on the value-stack.
  27   Pop :: Instr inp vs es ret a -> Instr inp (x ': vs) es ret a
  28   -- | @('LiftI2' f k)@ pops two values from the value-stack, and pushes the result of @(f)@ applied to them.
  29   LiftI2 :: InstrPure (x -> y -> z) -> Instr inp (z : vs) es ret a -> Instr inp (y : x : vs) es ret a
  30   -- | @('Fail')@ raises an error from the exception-stack.
  31   Fail :: Instr inp vs ('Succ es) ret a
  32   -- | @('Commit' k)@ removes an exception from the exception-stack and continues with the next 'Instr'uction @(k)@.
  33   Commit :: Instr inp vs es ret a -> Instr inp vs ('Succ es) ret a
  34   -- | @('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.
  35   Catch :: Instr inp vs ('Succ es) ret a -> Instr inp (inp ': vs) es ret a -> Instr inp vs es ret a
  36   -- | @('Seek' k)@ removes the input from the value-stack and continues with the next 'Instr'uction @(k)@.
  37   Seek :: Instr inp vs es r a -> Instr inp (inp : vs) es r a
  38   -- | @('Tell' k)@ pushes the input @(inp)@ on the value-stack and continues with the next 'Instr'uction @(k)@.
  39   Tell :: Instr inp (inp ': vs) es ret a -> Instr inp vs es ret a
  40   -- | @('Case' l r)@.
  41   Case :: Instr inp (x ': vs) n r a -> Instr inp (y ': vs) n r a -> Instr inp (Either x y ': vs) n r a
  42   -- | @('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)@.
  43   Swap :: Instr inp (x ': y ': vs) n r a -> Instr inp (y ': x ': vs) n r a
  44   -- | @('Choices' ps bs d)@.
  45   Choices :: [InstrPure (x -> Bool)] -> [Instr inp vs es ret a] -> Instr inp vs es ret a -> Instr inp (x ': vs) es ret a
  46
  47 -- ** Type 'InstrPure'
  48 data InstrPure a
  49   =  InstrPureHaskell (Hask.Haskell a)
  50   |  InstrPureSameOffset
  51
  52 -- * Class 'Executable'
  53 -- | Tagless-Final encoding of 'Instr'uctions.
  54 class Executable repr where
  55   ret :: repr inp '[ret] (n::Peano) ret a
  56   push :: InstrPure x -> repr inp (x ': vs) n ret a -> repr inp vs n ret a
  57   pop :: repr inp vs n ret a -> repr inp (x ': vs) n ret a
  58   liftI2 :: InstrPure (x -> y -> z) -> repr inp (z ': vs) es ret a -> repr inp (y ': x ': vs) es ret a
  59   fail :: repr inp vs ('Succ es) ret a
  60   commit :: repr inp vs es ret a -> repr inp vs ('Succ es) ret a
  61   catch :: repr inp vs ('Succ es) ret a -> repr inp (inp ': vs) es ret a -> repr inp vs es ret a
  62   seek :: repr inp vs es r a -> repr inp (inp ': vs) es r a
  63   tell :: repr inp (inp ': vs) es ret a -> repr inp vs es ret a
  64   case_ :: repr inp (x ': vs) n r a -> repr inp (y ': vs) n r a -> repr inp (Either x y ': vs) n r a
  65   swap :: repr inp (x ': y ': vs) n r a -> repr inp (y ': x ': vs) n r a
  66   choices :: [InstrPure (x -> Bool)] -> [repr inp vs es ret a] -> repr inp vs es ret a -> repr inp (x ': vs) es ret a
  67
  68 instance
  69   Executable repr =>
  70   Trans (Instr inp vs es ret) (repr inp vs es ret) where
  71   trans = \case
  72     Ret -> ret
  73     Push x k -> push x (trans k)
  74     Pop k -> pop (trans k)
  75     LiftI2 f k -> liftI2 f (trans k)
  76     Fail -> fail
  77     Commit k -> commit (trans k)
  78     Catch l r -> catch (trans l) (trans r)
  79     Seek k -> seek (trans k)
  80     Tell k -> tell (trans k)
  81     Case l r -> case_ (trans l) (trans r)
  82     Swap k -> swap (trans k)
  83     Choices ps bs d -> choices ps (trans Functor.<$> bs) (trans d)
  84
  85
  86 -- ** Type 'Peano'
  87 -- | Type-level natural numbers, using the Peano recursive encoding.
  88 data Peano = Zero | Succ Peano
  89
  90 -- | @('App' k)@ pops @(x)@ and @(x2y)@ from the value-stack, pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
  91 pattern App :: Instr inp (y : vs) es ret a -> Instr inp (x : (x -> y) : vs) es ret a
  92 pattern App k = LiftI2 (InstrPureHaskell (Hask.:$)) k
  93
  94 -- | @('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.
  95 pattern If :: Instr inp vs es ret a -> Instr inp vs es ret a -> Instr inp (Bool ': vs) es ret a
  96 pattern If ok ko = Choices [InstrPureHaskell Hask.Id] [ok] ko
  97
  98 parsecHandler :: InputPosition inp => Instr inp vs ('Succ es) ret a -> Instr inp (inp : vs) ('Succ es) ret a
  99 parsecHandler k = Tell (LiftI2 InstrPureSameOffset (If k Fail))
 100
 101 -- * Type 'Automaton'
 102 -- | Making the control-flow explicit.
 103 data Automaton inp a x = Automaton { unAutomaton ::
 104   forall vs es ret.
 105   {-next-}Instr inp (x ': vs) ('Succ es) ret a ->
 106   Instr inp vs ('Succ es) ret a
 107   }
 108
 109 automaton ::
 110   forall inp a es repr.
 111   Executable repr =>
 112   Automaton inp a a -> (repr inp '[] ('Succ es) a) a
 113 automaton =
 114   trans @(Instr inp '[] ('Succ es) a) .
 115   ($ Ret) .
 116   unAutomaton
 117
 118 instance Applicable (Automaton inp a) where
 119   pure x = Automaton $ Push (InstrPureHaskell x)
 120   Automaton f <*> Automaton x = Automaton $ f . x . App
 121   liftA2 f (Automaton x) (Automaton y) = Automaton $
 122     x . y . LiftI2 (InstrPureHaskell f)
 123   Automaton x *> Automaton y = Automaton $ x . Pop . y
 124   Automaton x <* Automaton y = Automaton $ x . y . Pop
 125 instance
 126   InputPosition inp =>
 127   Alternable (Automaton inp a) where
 128   empty = Automaton $ \_k -> Fail
 129   Automaton l <|> Automaton r = Automaton $ \k ->
 130     -- TODO: join points
 131     Catch (l (Commit k)) (parsecHandler (r k))
 132   try (Automaton x) = Automaton $ \k ->
 133     Catch (x (Commit k)) (Seek Fail)
 134 instance Selectable (Automaton inp a) where
 135   branch (Automaton lr) (Automaton l) (Automaton r) = Automaton $ \k ->
 136     -- TODO: join points
 137     lr (Case (l (Swap (App k)))
 138              (r (Swap (App k))))
 139 instance Matchable (Automaton inp a) where
 140   conditional ps bs (Automaton a) (Automaton def) =
 141     Automaton $ \k ->
 142       -- TODO: join points
 143       a (Choices (InstrPureHaskell Functor.<$> ps) ((\b -> unAutomaton b k) Functor.<$> bs) (def k))
 144 instance Lookable (Automaton inp a) where
 145   look (Automaton x) = Automaton $ \k ->
 146     Tell (x (Swap (Seek k)))
 147   negLook (Automaton x) = Automaton $ \k ->
 148     Catch (Tell (x (Pop (Seek (Commit Fail)))))
 149           (Seek (Push (InstrPureHaskell Hask.unit) k))