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