src/Symantic/Parser/Automaton/Instructions.hs

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