src/Symantic/Parser/Machine/Instructions.hs

   1 {-# LANGUAGE ConstraintKinds #-} -- For Executable
   2 {-# LANGUAGE DerivingStrategies #-} -- For Show (LetName a)
   3 {-# LANGUAGE PatternSynonyms #-} -- For Fmap, App, …
   4 {-# LANGUAGE UndecidableInstances #-} -- For Cursorable (Cursor inp)
   5 module Symantic.Parser.Machine.Instructions where
   6
   7 import Data.Bool (Bool(..))
   8 import Data.Either (Either)
   9 import Data.Eq (Eq)
  10 import Data.Ord (Ord)
  11 import Data.Function (($), (.))
  12 import Data.Kind (Type)
  13 import System.IO.Unsafe (unsafePerformIO)
  14 import Text.Show (Show(..), showString)
  15 import qualified Data.Functor as Functor
  16 import qualified Language.Haskell.TH as TH
  17 import qualified Language.Haskell.TH.Syntax as TH
  18 import qualified Symantic.Parser.Grammar.Pure as H
  19
  20 import Symantic.Parser.Grammar
  21 import Symantic.Parser.Machine.Input
  22 import Symantic.Univariant.Trans
  23
  24 -- * Type 'Instr'
  25 -- | 'Instr'uctions for the 'Machine'.
  26 data Instr input valueStack (failStack::Peano) returnValue where
  27   -- | @('Push' x k)@ pushes @(x)@ on the 'valueStack'
  28   -- and continues with the next 'Instr'uction @(k)@.
  29   Push ::
  30     InstrPure v ->
  31     Instr inp (v ': vs) es ret ->
  32     Instr inp vs es ret
  33   -- | @('Pop' k)@ pushes @(x)@ on the 'valueStack'.
  34   Pop ::
  35     Instr inp vs es ret ->
  36     Instr inp (v ': vs) es ret
  37   -- | @('LiftI2' f k)@ pops two values from the 'valueStack',
  38   -- and pushes the result of @(f)@ applied to them.
  39   LiftI2 ::
  40     InstrPure (x -> y -> z) ->
  41     Instr inp (z : vs) es ret ->
  42     Instr inp (y : x : vs) es ret
  43   -- | @('Fail')@ raises an error from the 'failStack'.
  44   Fail ::
  45     [ErrorItem (InputToken inp)] ->
  46     Instr inp vs ('Succ es) ret
  47   -- | @('PopFail' k)@ removes a 'FailHandler' from the 'failStack'
  48   -- and continues with the next 'Instr'uction @(k)@.
  49   PopFail ::
  50     Instr inp vs es ret ->
  51     Instr inp vs ('Succ es) ret
  52   -- | @('CatchFail' l r)@ tries the @(l)@ 'Instr'uction
  53   -- in a new failure scope such that if @(l)@ raises a failure, it is caught,
  54   -- then the input is pushed as it was before trying @(l)@ on the 'valueStack',
  55   -- and the control flow goes on with the @(r)@ 'Instr'uction.
  56   CatchFail ::
  57     Instr inp vs ('Succ es) ret ->
  58     Instr inp (Cursor inp ': vs) es ret ->
  59     Instr inp vs es ret
  60   -- | @('LoadInput' k)@ removes the input from the 'valueStack'
  61   -- and continues with the next 'Instr'uction @(k)@ using that input.
  62   LoadInput ::
  63     Instr inp vs es r ->
  64     Instr inp (Cursor inp : vs) es r
  65   -- | @('PushInput' k)@ pushes the input @(inp)@ on the 'valueStack'
  66   -- and continues with the next 'Instr'uction @(k)@.
  67   PushInput ::
  68     Instr inp (Cursor inp ': vs) es ret ->
  69     Instr inp vs es ret
  70   -- | @('Case' l r)@.
  71   Case ::
  72     Instr inp (x ': vs) es r ->
  73     Instr inp (y ': vs) es r ->
  74     Instr inp (Either x y ': vs) es r
  75   -- | @('Swap' k)@ pops two values on the 'valueStack',
  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 ->
  80     Instr inp (y ': x ': vs) es r
  81   -- | @('Choices' ps bs d)@.
  82   Choices ::
  83     [InstrPure (v -> Bool)] ->
  84     [Instr inp vs es ret] ->
  85     Instr inp vs es ret ->
  86     Instr inp (v ': vs) es ret
  87   -- | @('Subroutine' n v k)@ binds the 'LetName' @(n)@ to the 'Instr'uction's @(v)@,
  88   -- 'Call's @(n)@ and
  89   -- continues with the next 'Instr'uction @(k)@.
  90   Subroutine ::
  91     LetName v -> Instr inp '[] ('Succ 'Zero) v ->
  92     Instr inp vs ('Succ es) ret ->
  93     Instr inp vs ('Succ es) ret
  94   -- | @('Jump' n k)@ pass the control-flow to the 'Subroutine' named @(n)@.
  95   Jump ::
  96     LetName ret ->
  97     Instr inp '[] ('Succ es) ret
  98   -- | @('Call' n k)@ pass the control-flow to the 'Subroutine' named @(n)@,
  99   -- and when it 'Ret'urns, continues with the next 'Instr'uction @(k)@.
 100   Call ::
 101     LetName v ->
 102     Instr inp (v ': vs) ('Succ es) ret ->
 103     Instr inp vs ('Succ es) ret
 104   -- | @('Ret')@ returns the value stored in a singleton 'valueStack'.
 105   Ret ::
 106     Instr inp '[ret] es ret
 107   -- | @('Read' expected p k)@ reads a 'Char' @(c)@ from the 'inp'ut,
 108   -- if @(p c)@ is 'True' then continues with the next 'Instr'uction @(k)@ on,
 109   -- otherwise 'Fail'.
 110   Read ::
 111     [ErrorItem (InputToken inp)] ->
 112     InstrPure (InputToken inp -> Bool) ->
 113     Instr inp (InputToken inp ': vs) ('Succ es) ret ->
 114     Instr inp vs ('Succ es) ret
 115   DefJoin ::
 116     LetName v -> Instr inp (v ': vs) es ret ->
 117     Instr inp vs es ret ->
 118     Instr inp vs es ret
 119   RefJoin ::
 120     LetName v ->
 121     Instr inp (v ': vs) es ret
 122
 123 -- ** Type 'InstrPure'
 124 data InstrPure a where
 125   InstrPureHaskell :: H.CombPure a -> InstrPure a
 126
 127 instance Show (InstrPure a) where
 128   showsPrec p = \case
 129     InstrPureHaskell x -> showsPrec p x
 130     InstrPureSameOffset{} -> showString "InstrPureSameOffset"
 131 instance Trans InstrPure TH.CodeQ where
 132   trans = \case
 133     InstrPureHaskell x -> trans x
 134     InstrPureSameOffset x -> x
 135
 136 -- ** Type 'LetName'
 137 newtype LetName a = LetName { unLetName :: TH.Name }
 138   deriving (Eq)
 139   deriving newtype Show
 140
 141 -- * Class 'Executable'
 142 type Executable repr =
 143   ( Stackable repr
 144   , Branchable repr
 145   , Failable repr
 146   , Inputable repr
 147   , Routinable repr
 148   , Joinable repr
 149   )
 150
 151 -- ** Class 'Stackable'
 152 class Stackable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
 153   push ::
 154     InstrPure v ->
 155     repr inp (v ': vs) n ret ->
 156     repr inp vs n ret
 157   pop ::
 158     repr inp vs n ret ->
 159     repr inp (v ': vs) n ret
 160   liftI2 ::
 161     InstrPure (x -> y -> z) ->
 162     repr inp (z ': vs) es ret ->
 163     repr inp (y ': x ': vs) es ret
 164   swap ::
 165     repr inp (x ': y ': vs) n r ->
 166     repr inp (y ': x ': vs) n r
 167
 168 -- ** Class 'Branchable'
 169 class Branchable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
 170   case_ ::
 171     repr inp (x ': vs) n r ->
 172     repr inp (y ': vs) n r ->
 173     repr inp (Either x y ': vs) n r
 174   choices ::
 175     [InstrPure (v -> Bool)] ->
 176     [repr inp vs es ret] ->
 177     repr inp vs es ret ->
 178     repr inp (v ': vs) es ret
 179
 180 -- ** Class 'Failable'
 181 class Failable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
 182   fail :: [ErrorItem (InputToken inp)] -> repr inp vs ('Succ es) ret
 183   popFail ::
 184     repr inp vs es ret ->
 185     repr inp vs ('Succ es) ret
 186   catchFail ::
 187     repr inp vs ('Succ es) ret ->
 188     repr inp (Cursor inp ': vs) es ret ->
 189     repr inp vs es ret
 190
 191 -- ** Class 'Inputable'
 192 class Inputable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
 193   loadInput ::
 194     repr inp vs es r ->
 195     repr inp (Cursor inp ': vs) es r
 196   pushInput ::
 197     repr inp (Cursor inp ': vs) es ret ->
 198     repr inp vs es ret
 199
 200 -- ** Class 'Routinable'
 201 class Routinable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
 202   subroutine ::
 203     LetName v -> repr inp '[] ('Succ 'Zero) v ->
 204     repr inp vs ('Succ es) ret ->
 205     repr inp vs ('Succ es) ret
 206   call ::
 207     LetName v -> repr inp (v ': vs) ('Succ es) ret ->
 208     repr inp vs ('Succ es) ret
 209   ret ::
 210     repr inp '[ret] es ret
 211   jump ::
 212     LetName ret ->
 213     repr inp '[] ('Succ es) ret
 214
 215 -- ** Class 'Joinable'
 216 class Joinable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
 217   defJoin ::
 218     LetName v ->
 219     repr inp (v ': vs) es ret ->
 220     repr inp vs es ret ->
 221     repr inp vs es ret
 222   refJoin ::
 223     LetName v ->
 224     repr inp (v ': vs) es ret
 225
 226 -- ** Class 'Readable'
 227 class Readable (repr :: Type -> [Type] -> Peano -> Type -> Type) (tok::Type) where
 228   read ::
 229     tok ~ InputToken inp =>
 230     [ErrorItem tok] ->
 231     InstrPure (tok -> Bool) ->
 232     repr inp (tok ': vs) ('Succ es) ret ->
 233     repr inp vs ('Succ es) ret
 234
 235 instance
 236   ( Executable repr
 237   , Readable repr (InputToken inp)
 238   ) => Trans (Instr inp vs es) (repr inp vs es) where
 239   trans = \case
 240     Push x k -> push x (trans k)
 241     Pop k -> pop (trans k)
 242     LiftI2 f k -> liftI2 f (trans k)
 243     Fail err -> fail err
 244     PopFail k -> popFail (trans k)
 245     CatchFail l r -> catchFail (trans l) (trans r)
 246     LoadInput k -> loadInput (trans k)
 247     PushInput k -> pushInput (trans k)
 248     Case l r -> case_ (trans l) (trans r)
 249     Swap k -> swap (trans k)
 250     Choices ps bs d -> choices ps (trans Functor.<$> bs) (trans d)
 251     Subroutine n sub k -> subroutine n (trans sub) (trans k)
 252     Jump n -> jump n
 253     Call n k -> call n (trans k)
 254     Ret -> ret
 255     Read es p k -> read es p (trans k)
 256     DefJoin n sub k -> defJoin n (trans sub) (trans k)
 257     RefJoin n -> refJoin n
 258
 259 -- ** Type 'Peano'
 260 -- | Type-level natural numbers, using the Peano recursive encoding.
 261 data Peano = Zero | Succ Peano
 262
 263 -- | @('Fmap' f k)@.
 264 pattern Fmap ::
 265   InstrPure (x -> y) ->
 266   Instr inp (y ': xs) es ret ->
 267   Instr inp (x ': xs) es ret
 268 pattern Fmap f k = Push f (LiftI2 (InstrPureHaskell (H.Flip H.:@ (H.:$))) k)
 269
 270 -- | @('App' k)@ pops @(x)@ and @(x2y)@ from the 'valueStack',
 271 -- pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
 272 pattern App ::
 273   Instr inp (y : vs) es ret ->
 274   Instr inp (x : (x -> y) : vs) es ret
 275 pattern App k = LiftI2 (InstrPureHaskell (H.:$)) k
 276
 277 -- | @('If' ok ko)@ pops a 'Bool' from the 'valueStack'
 278 -- and continues either with the 'Instr'uction @(ok)@ if it is 'True'
 279 -- or @(ko)@ otherwise.
 280 pattern If ::
 281   Instr inp vs es ret ->
 282   Instr inp vs es ret ->
 283   Instr inp (Bool ': vs) es ret
 284 pattern If ok ko = Choices [InstrPureHaskell H.Id] [ok] ko
 285
 286 -- * Type 'Machine'
 287 -- | Making the control-flow explicit.
 288 data Machine inp v = Machine { unMachine ::
 289   forall vs es ret.
 290   {-k-}Instr inp (v ': vs) ('Succ es) ret ->
 291   Instr inp vs ('Succ es) ret
 292   }
 293
 294 runMachine ::
 295   forall inp v es repr.
 296   Executable repr =>
 297   Readable repr (InputToken inp) =>
 298   Machine inp v -> repr inp '[] ('Succ es) v
 299 runMachine (Machine auto) =
 300   trans @(Instr inp '[] ('Succ es)) $
 301   auto Ret
 302
 303 instance Applicable (Machine inp) where
 304   pure x = Machine $ Push (InstrPureHaskell x)
 305   Machine f <*> Machine x = Machine $ f . x . App
 306   liftA2 f (Machine x) (Machine y) = Machine $
 307     x . y . LiftI2 (InstrPureHaskell f)
 308   Machine x *> Machine y = Machine $ x . Pop . y
 309   Machine x <* Machine y = Machine $ x . y . Pop
 310 instance
 311   Cursorable (Cursor inp) =>
 312   Alternable (Machine inp) where
 313   empty = Machine $ \_k -> Fail []
 314   Machine l <|> Machine r = Machine $ \k ->
 315     makeJoin k $ \j ->
 316     CatchFail
 317       (l (PopFail j))
 318       (failIfConsumed (r j))
 319   try (Machine x) = Machine $ \k ->
 320     CatchFail (x (PopFail k))
 321       -- On exception, reset the input,
 322       -- and propagate the failure.
 323       (LoadInput (Fail []))
 324
 325 -- | If no input has been consumed by the failing alternative
 326 -- then continue with the given continuation.
 327 -- Otherwise, propagate the 'Fail'ure.
 328 failIfConsumed ::
 329   Cursorable (Cursor inp) =>
 330   Instr inp vs ('Succ es) ret ->
 331   Instr inp (Cursor inp : vs) ('Succ es) ret
 332 failIfConsumed k = PushInput (LiftI2 (InstrPureSameOffset sameOffset) (If k (Fail [])))
 333
 334 -- | @('makeJoin' k f)@ factorizes @(k)@ in @(f)@,
 335 -- by introducing a 'DefJoin' if necessary,
 336 -- and passing the corresponding 'RefJoin' to @(f)@,
 337 -- or @(k)@ as is when factorizing is useless.
 338 makeJoin ::
 339   Instr inp (v : vs) es ret ->
 340   (Instr inp (v : vs) es ret -> Instr inp vs es ret) ->
 341   Instr inp vs es ret
 342 -- Double RefJoin Optimization:
 343 -- If a join-node points directly to another join-node,
 344 -- then reuse it
 345 makeJoin k@RefJoin{} = ($ k)
 346 -- Terminal RefJoin Optimization:
 347 -- If a join-node points directly to a terminal operation,
 348 -- then it's useless to introduce a join-point.
 349 makeJoin k@Ret = ($ k)
 350 makeJoin k =
 351   let joinName = LetName $ unsafePerformIO $ TH.qNewName "join" in
 352   \f -> DefJoin joinName k (f (RefJoin joinName))
 353
 354 instance tok ~ InputToken inp => Satisfiable (Machine inp) tok where
 355   satisfy es p = Machine $ Read es (InstrPureHaskell p)
 356 instance Selectable (Machine inp) where
 357   branch (Machine lr) (Machine l) (Machine r) = Machine $ \k ->
 358     makeJoin k $ \j ->
 359     lr (Case (l (Swap (App j)))
 360              (r (Swap (App j))))
 361 instance Matchable (Machine inp) where
 362   conditional ps bs (Machine m) (Machine default_) = Machine $ \k ->
 363     makeJoin k $ \j ->
 364     m (Choices (InstrPureHaskell Functor.<$> ps)
 365                ((\b -> unMachine b j) Functor.<$> bs)
 366                (default_ j))
 367 instance
 368   ( Ord (InputToken inp)
 369   , Cursorable (Cursor inp)
 370   ) => Lookable (Machine inp) where
 371   look (Machine x) = Machine $ \k ->
 372     PushInput (x (Swap (LoadInput k)))
 373   eof = negLook (satisfy [{-discarded by negLook-}] (H.const H..@ H.bool True))
 374         -- Set a better failure message
 375         <|> (Machine $ \_k -> Fail [ErrorItemEnd])
 376   negLook (Machine x) = Machine $ \k ->
 377     CatchFail
 378       -- On x success, discard the result,
 379       -- and replace this 'CatchFail''s failure handler
 380       -- by a 'Fail'ure whose 'farthestExpecting' is negated,
 381       -- then a failure is raised from the input
 382       -- when entering 'negLook', to avoid odd cases:
 383       -- - where the failure that made (negLook x)
 384       --   succeed can get the blame for the overall
 385       --   failure of the grammar.
 386       -- - where the overall failure of
 387       --   the grammar might be blamed on something in x
 388       --   that, if corrected, still makes x succeed and
 389       --   (negLook x) fail.
 390       (PushInput (x (Pop (PopFail (LoadInput (Fail []))))))
 391       -- On x failure, reset the input,
 392       -- and go on with the next 'Instr'uctions.
 393       (LoadInput (Push (InstrPureHaskell H.unit) k))
 394 instance Letable TH.Name (Machine inp) where
 395   def n v = Machine $ \k ->
 396     Subroutine (LetName n) (unMachine v Ret) (Call (LetName n) k)
 397   ref _isRec n = Machine $ \case
 398     Ret -> Jump (LetName n)
 399     k -> Call (LetName n) k
 400 instance Cursorable (Cursor inp) => Foldable (Machine inp) where
 401   {-
 402   chainPre op p = go <*> p
 403     where go = (H..) <$> op <*> go <|> pure H.id
 404   chainPost p op = p <**> go
 405     where go = (H..) <$> op <*> go <|> pure H.id
 406   -}