src/Symantic/Parser/Automaton/Instructions.hs

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