src/Symantic/Parser/Automaton/Instructions.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE NoPolyKinds #-}
   4 {-# LANGUAGE PatternSynonyms #-}
   5 {-# LANGUAGE ViewPatterns #-}
   6 module Symantic.Parser.Automaton.Instructions where
   7
   8 import Data.Bool (Bool)
   9 import Data.Either (Either)
  10 import Data.Eq (Eq)
  11 import Data.Function (($), (.))
  12 import Text.Show (Show)
  13 import qualified Data.Functor as Functor
  14 import qualified Language.Haskell.TH.Syntax as TH
  15 import qualified Symantic.Parser.Staging as Hask
  16
  17 import Symantic.Parser.Grammar
  18 import Symantic.Univariant.Trans
  19
  20 -- * Class 'InputPosition'
  21 -- | TODO
  22 class InputPosition inp where
  23
  24 -- * Type 'Instr'
  25 -- | 'Instr'uctions for the 'Automaton'.
  26 data Instr input valueStack (exceptionStack::Peano) returnValue a where
  27   -- | @('Ret')@ returns the value in a singleton value-stack.
  28   Ret :: Instr inp '[ret] es ret a
  29   -- | @('Push' x k)@ pushes @(x)@ on the value-stack and continues with the next 'Instr'uction @(k)@.
  30   Push :: InstrPure x -> Instr inp (x ': vs) es ret a -> Instr inp vs es ret a
  31   -- | @('Pop' k)@ pushes @(x)@ on the value-stack.
  32   Pop :: Instr inp vs es ret a -> Instr inp (x ': vs) es ret a
  33   -- | @('LiftI2' f k)@ pops two values from the value-stack, and pushes the result of @(f)@ applied to them.
  34   LiftI2 :: InstrPure (x -> y -> z) -> Instr inp (z : vs) es ret a -> Instr inp (y : x : vs) es ret a
  35   -- | @('Fail')@ raises an error from the exception-stack.
  36   Fail :: Instr inp vs ('Succ es) ret a
  37   -- | @('Commit' k)@ removes an exception from the exception-stack and continues with the next 'Instr'uction @(k)@.
  38   Commit :: Instr inp vs es ret a -> Instr inp vs ('Succ es) ret a
  39   -- | @('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.
  40   Catch :: Instr inp vs ('Succ es) ret a -> Instr inp (inp ': vs) es ret a -> Instr inp vs es ret a
  41   -- | @('Seek' k)@ removes the input from the value-stack and continues with the next 'Instr'uction @(k)@.
  42   Seek :: Instr inp vs es r a -> Instr inp (inp : vs) es r a
  43   -- | @('Tell' k)@ pushes the input @(inp)@ on the value-stack and continues with the next 'Instr'uction @(k)@.
  44   Tell :: Instr inp (inp ': vs) es ret a -> Instr inp vs es ret a
  45   -- | @('Case' l r)@.
  46   Case :: Instr inp (x ': vs) es r a -> Instr inp (y ': vs) es r a -> Instr inp (Either x y ': vs) es r a
  47   -- | @('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)@.
  48   Swap :: Instr inp (x ': y ': vs) es r a -> Instr inp (y ': x ': vs) es r a
  49   -- | @('Choices' ps bs d)@.
  50   Choices :: [InstrPure (x -> Bool)] -> [Instr inp vs es ret a] -> Instr inp vs es ret a -> Instr inp (x ': vs) es ret a
  51   Call :: Addr ret -> Instr inp (x ': xs) ('Succ es) ret a -> Instr inp xs ('Succ es) ret a
  52   Jump :: Addr ret -> Instr inp '[] ('Succ es) ret a
  53   Label :: Addr ret -> Instr inp (xs) ('Succ es) ret a -> Instr inp xs ('Succ es) ret a
  54
  55 -- ** Type 'InstrPure'
  56 data InstrPure a
  57   =  InstrPureHaskell (Hask.Haskell a)
  58   |  InstrPureSameOffset
  59   deriving (Show)
  60
  61 -- ** Type 'Addr'
  62 newtype Addr a = Addr { unLabel :: TH.Name }
  63   deriving (Eq, Show)
  64
  65 -- * Class 'Executable'
  66 type Executable repr =
  67   ( Stackable repr
  68   , Branchable repr
  69   , Exceptionable repr
  70   , Inputable repr
  71   , Routinable repr
  72   )
  73
  74 -- ** Class 'Stackable'
  75 class Stackable (repr :: * -> [*] -> Peano -> * -> * -> *) where
  76   push :: InstrPure x -> repr inp (x ': vs) n ret a -> repr inp vs n ret a
  77   pop :: repr inp vs n ret a -> repr inp (x ': vs) n ret a
  78   liftI2 :: InstrPure (x -> y -> z) -> repr inp (z ': vs) es ret a -> repr inp (y ': x ': vs) es ret a
  79   swap :: repr inp (x ': y ': vs) n r a -> repr inp (y ': x ': vs) n r a
  80
  81 -- ** Class 'Branchable'
  82 class Branchable (repr :: * -> [*] -> Peano -> * -> * -> *) where
  83   case_ :: repr inp (x ': vs) n r a -> repr inp (y ': vs) n r a -> repr inp (Either x y ': vs) n r a
  84   choices :: [InstrPure (x -> Bool)] -> [repr inp vs es ret a] -> repr inp vs es ret a -> repr inp (x ': vs) es ret a
  85
  86 -- ** Class 'Exceptionable'
  87 class Exceptionable (repr :: * -> [*] -> Peano -> * -> * -> *) where
  88   fail :: repr inp vs ('Succ es) ret a
  89   commit :: repr inp vs es ret a -> repr inp vs ('Succ es) ret a
  90   catch :: repr inp vs ('Succ es) ret a -> repr inp (inp ': vs) es ret a -> repr inp vs es ret a
  91
  92 -- ** Class 'Inputable'
  93 class Inputable (repr :: * -> [*] -> Peano -> * -> * -> *) where
  94   seek :: repr inp vs es r a -> repr inp (inp ': vs) es r a
  95   tell :: repr inp (inp ': vs) es ret a -> repr inp vs es ret a
  96
  97 -- ** Class 'Routinable'
  98 class Routinable (repr :: * -> [*] -> Peano -> * -> * -> *) where
  99   label :: Addr ret -> repr inp vs ('Succ es) ret a -> repr inp vs ('Succ es) ret a
 100   call :: Addr ret -> repr inp (x ': vs) ('Succ es) ret a -> repr inp vs ('Succ es) ret a
 101   ret :: repr inp '[ret] es ret a
 102   jump :: Addr ret -> repr inp '[] ('Succ es) ret a
 103
 104 instance
 105   ( Stackable repr
 106   , Branchable repr
 107   , Exceptionable repr
 108   , Inputable repr
 109   , Routinable repr
 110   ) => Trans (Instr inp vs es ret) (repr inp vs es ret) where
 111   trans = \case
 112     Push x k -> push x (trans k)
 113     Pop k -> pop (trans k)
 114     LiftI2 f k -> liftI2 f (trans k)
 115     Fail -> fail
 116     Commit k -> commit (trans k)
 117     Catch l r -> catch (trans l) (trans r)
 118     Seek k -> seek (trans k)
 119     Tell k -> tell (trans k)
 120     Case l r -> case_ (trans l) (trans r)
 121     Swap k -> swap (trans k)
 122     Choices ps bs d -> choices ps (trans Functor.<$> bs) (trans d)
 123     Label n k -> label n (trans k)
 124     Call n (k::Instr inp (x ': vs) ('Succ es') ret a) ->
 125       call n (trans k :: repr inp (x ': vs) ('Succ es') ret a)
 126     Ret -> ret
 127     Jump n -> jump n
 128
 129 -- ** Type 'Peano'
 130 -- | Type-level natural numbers, using the Peano recursive encoding.
 131 data Peano = Zero | Succ Peano
 132
 133 -- | @('App' k)@ pops @(x)@ and @(x2y)@ from the value-stack, pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
 134 pattern App :: Instr inp (y : vs) es ret a -> Instr inp (x : (x -> y) : vs) es ret a
 135 pattern App k = LiftI2 (InstrPureHaskell (Hask.:$)) k
 136
 137 -- | @('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.
 138 pattern If :: Instr inp vs es ret a -> Instr inp vs es ret a -> Instr inp (Bool ': vs) es ret a
 139 pattern If ok ko = Choices [InstrPureHaskell Hask.Id] [ok] ko
 140
 141 parsecHandler :: InputPosition inp => Instr inp vs ('Succ es) ret a -> Instr inp (inp : vs) ('Succ es) ret a
 142 parsecHandler k = Tell (LiftI2 InstrPureSameOffset (If k Fail))
 143
 144 -- * Type 'Automaton'
 145 -- | Making the control-flow explicit.
 146 data Automaton inp a x = Automaton { unAutomaton ::
 147   forall vs es ret.
 148   {-next-}Instr inp (x ': vs) ('Succ es) ret a ->
 149   Instr inp vs ('Succ es) ret a
 150   }
 151
 152 automaton ::
 153   forall inp a es repr.
 154   Executable repr =>
 155   Automaton inp a a -> (repr inp '[] ('Succ es) a) a
 156 automaton =
 157   trans @(Instr inp '[] ('Succ es) a) .
 158   ($ Ret) .
 159   unAutomaton
 160
 161 instance Applicable (Automaton inp a) where
 162   pure x = Automaton $ Push (InstrPureHaskell x)
 163   Automaton f <*> Automaton x = Automaton $ f . x . App
 164   liftA2 f (Automaton x) (Automaton y) = Automaton $
 165     x . y . LiftI2 (InstrPureHaskell f)
 166   Automaton x *> Automaton y = Automaton $ x . Pop . y
 167   Automaton x <* Automaton y = Automaton $ x . y . Pop
 168 instance
 169   InputPosition inp =>
 170   Alternable (Automaton inp a) where
 171   empty = Automaton $ \_k -> Fail
 172   Automaton l <|> Automaton r = Automaton $ \k ->
 173     -- TODO: join points
 174     Catch (l (Commit k)) (parsecHandler (r k))
 175   try (Automaton x) = Automaton $ \k ->
 176     Catch (x (Commit k)) (Seek Fail)
 177 instance Selectable (Automaton inp a) where
 178   branch (Automaton lr) (Automaton l) (Automaton r) = Automaton $ \k ->
 179     -- TODO: join points
 180     lr (Case (l (Swap (App k)))
 181              (r (Swap (App k))))
 182 instance Matchable (Automaton inp a) where
 183   conditional ps bs (Automaton a) (Automaton default_) =
 184     Automaton $ \k ->
 185       -- TODO: join points
 186       a (Choices (InstrPureHaskell Functor.<$> ps) ((\b -> unAutomaton b k) Functor.<$> bs) (default_ k))
 187 instance Lookable (Automaton inp a) where
 188   look (Automaton x) = Automaton $ \k ->
 189     Tell (x (Swap (Seek k)))
 190   negLook (Automaton x) = Automaton $ \k ->
 191     Catch (Tell (x (Pop (Seek (Commit Fail)))))
 192           (Seek (Push (InstrPureHaskell Hask.unit) k))
 193 instance Letable TH.Name (Automaton inp a) where
 194   def n (Automaton x) = Automaton $ \k ->
 195     Label (Addr n) (x k)
 196   ref _isRec n = Automaton $ \case
 197     Ret -> Jump (Addr n)
 198     k -> Call (Addr n) k