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   InstrPure :: H.CombPure a -> InstrPure a
 126   InstrPureSameOffset :: CodeQ (cur -> cur -> Bool) -> InstrPure (cur -> cur -> Bool)
 127   InstrP
 128
 129 instance Show (InstrPure a) where
 130   showsPrec p = \case
 131     InstrPure x -> showsPrec p x
 132     InstrPureSameOffset{} -> showString "InstrPureSameOffset"
 133 instance Trans InstrPure TH.CodeQ where
 134   trans = \case
 135     InstrPure x -> trans x
 136     InstrPureSameOffset x -> x
 137
 138 -- ** Type 'LetName'
 139 newtype LetName a = LetName { unLetName :: TH.Name }
 140   deriving (Eq)
 141   deriving newtype Show
 142
 143 -- * Class 'Executable'
 144 type Executable repr =
 145   ( Stackable repr
 146   , Branchable repr
 147   , Failable repr
 148   , Inputable repr
 149   , Routinable repr
 150   , Joinable repr
 151   )
 152
 153 -- ** Class 'Stackable'
 154 class Stackable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
 155   push ::
 156     InstrPure v ->
 157     repr inp (v ': vs) n ret ->
 158     repr inp vs n ret
 159   pop ::
 160     repr inp vs n ret ->
 161     repr inp (v ': vs) n ret
 162   liftI2 ::
 163     InstrPure (x -> y -> z) ->
 164     repr inp (z ': vs) es ret ->
 165     repr inp (y ': x ': vs) es ret
 166   swap ::
 167     repr inp (x ': y ': vs) n r ->
 168     repr inp (y ': x ': vs) n r
 169
 170 -- ** Class 'Branchable'
 171 class Branchable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
 172   case_ ::
 173     repr inp (x ': vs) n r ->
 174     repr inp (y ': vs) n r ->
 175     repr inp (Either x y ': vs) n r
 176   choices ::
 177     [InstrPure (v -> Bool)] ->
 178     [repr inp vs es ret] ->
 179     repr inp vs es ret ->
 180     repr inp (v ': vs) es ret
 181
 182 -- ** Class 'Failable'
 183 class Failable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
 184   fail :: [ErrorItem (InputToken inp)] -> repr inp vs ('Succ es) ret
 185   popFail ::
 186     repr inp vs es ret ->
 187     repr inp vs ('Succ es) ret
 188   catchFail ::
 189     repr inp vs ('Succ es) ret ->
 190     repr inp (Cursor inp ': vs) es ret ->
 191     repr inp vs es ret
 192
 193 -- ** Class 'Inputable'
 194 class Inputable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
 195   loadInput ::
 196     repr inp vs es r ->
 197     repr inp (Cursor inp ': vs) es r
 198   pushInput ::
 199     repr inp (Cursor inp ': vs) es ret ->
 200     repr inp vs es ret
 201
 202 -- ** Class 'Routinable'
 203 class Routinable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
 204   subroutine ::
 205     LetName v -> repr inp '[] ('Succ 'Zero) v ->
 206     repr inp vs ('Succ es) ret ->
 207     repr inp vs ('Succ es) ret
 208   call ::
 209     LetName v -> repr inp (v ': vs) ('Succ es) ret ->
 210     repr inp vs ('Succ es) ret
 211   ret ::
 212     repr inp '[ret] es ret
 213   jump ::
 214     LetName ret ->
 215     repr inp '[] ('Succ es) ret
 216
 217 -- ** Class 'Joinable'
 218 class Joinable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
 219   defJoin ::
 220     LetName v ->
 221     repr inp (v ': vs) es ret ->
 222     repr inp vs es ret ->
 223     repr inp vs es ret
 224   refJoin ::
 225     LetName v ->
 226     repr inp (v ': vs) es ret
 227
 228 -- ** Class 'Readable'
 229 class Readable (repr :: Type -> [Type] -> Peano -> Type -> Type) (tok::Type) where
 230   read ::
 231     tok ~ InputToken inp =>
 232     [ErrorItem tok] ->
 233     InstrPure (tok -> Bool) ->
 234     repr inp (tok ': vs) ('Succ es) ret ->
 235     repr inp vs ('Succ es) ret
 236
 237 instance
 238   ( Executable repr
 239   , Readable repr (InputToken inp)
 240   ) => Trans (Instr inp vs es) (repr inp vs es) where
 241   trans = \case
 242     Push x k -> push x (trans k)
 243     Pop k -> pop (trans k)
 244     LiftI2 f k -> liftI2 f (trans k)
 245     Fail err -> fail err
 246     PopFail k -> popFail (trans k)
 247     CatchFail l r -> catchFail (trans l) (trans r)
 248     LoadInput k -> loadInput (trans k)
 249     PushInput k -> pushInput (trans k)
 250     Case l r -> case_ (trans l) (trans r)
 251     Swap k -> swap (trans k)
 252     Choices ps bs d -> choices ps (trans Functor.<$> bs) (trans d)
 253     Subroutine n sub k -> subroutine n (trans sub) (trans k)
 254     Jump n -> jump n
 255     Call n k -> call n (trans k)
 256     Ret -> ret
 257     Read es p k -> read es p (trans k)
 258     DefJoin n sub k -> defJoin n (trans sub) (trans k)
 259     RefJoin n -> refJoin n
 260
 261 -- ** Type 'Peano'
 262 -- | Type-level natural numbers, using the Peano recursive encoding.
 263 data Peano = Zero | Succ Peano
 264
 265 -- | @('Fmap' f k)@.
 266 pattern Fmap ::
 267   InstrPure (x -> y) ->
 268   Instr inp (y ': xs) es ret ->
 269   Instr inp (x ': xs) es ret
 270 pattern Fmap f k = Push f (LiftI2 (InstrPure (H.Flip H.:@ (H.:$))) k)
 271
 272 -- | @('App' k)@ pops @(x)@ and @(x2y)@ from the 'valueStack',
 273 -- pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
 274 pattern App ::
 275   Instr inp (y : vs) es ret ->
 276   Instr inp (x : (x -> y) : vs) es ret
 277 pattern App k = LiftI2 (InstrPure (H.:$)) k
 278
 279 -- | @('If' ok ko)@ pops a 'Bool' from the 'valueStack'
 280 -- and continues either with the 'Instr'uction @(ok)@ if it is 'True'
 281 -- or @(ko)@ otherwise.
 282 pattern If ::
 283   Instr inp vs es ret ->
 284   Instr inp vs es ret ->
 285   Instr inp (Bool ': vs) es ret
 286 pattern If ok ko = Choices [InstrPure H.Id] [ok] ko
 287
 288 -- * Type 'Machine'
 289 -- | Making the control-flow explicit.
 290 data Machine inp v = Machine { unMachine ::
 291   forall vs es ret.
 292   {-k-}Instr inp (v ': vs) ('Succ es) ret ->
 293   Instr inp vs ('Succ es) ret
 294   }
 295
 296 runMachine ::
 297   forall inp v es repr.
 298   Executable repr =>
 299   Readable repr (InputToken inp) =>
 300   Machine inp v -> repr inp '[] ('Succ es) v
 301 runMachine (Machine auto) =
 302   trans @(Instr inp '[] ('Succ es)) $
 303   auto Ret
 304
 305 instance Applicable (Machine inp) where
 306   pure x = Machine $ Push (InstrPure x)
 307   Machine f <*> Machine x = Machine $ f . x . App
 308   liftA2 f (Machine x) (Machine y) = Machine $
 309     x . y . LiftI2 (InstrPure f)
 310   Machine x *> Machine y = Machine $ x . Pop . y
 311   Machine x <* Machine y = Machine $ x . y . Pop
 312 instance
 313   Cursorable (Cursor inp) =>
 314   Alternable (Machine inp) where
 315   empty = Machine $ \_k -> Fail []
 316   Machine l <|> Machine r = Machine $ \k ->
 317     makeJoin k $ \j ->
 318     CatchFail
 319       (l (PopFail j))
 320       (failIfConsumed (r j))
 321   try (Machine x) = Machine $ \k ->
 322     CatchFail (x (PopFail k))
 323       -- On exception, reset the input,
 324       -- and propagate the failure.
 325       (LoadInput (Fail []))
 326
 327 -- | If no input has been consumed by the failing alternative
 328 -- then continue with the given continuation.
 329 -- Otherwise, propagate the 'Fail'ure.
 330 failIfConsumed ::
 331   Cursorable (Cursor inp) =>
 332   Instr inp vs ('Succ es) ret ->
 333   Instr inp (Cursor inp : vs) ('Succ es) ret
 334 failIfConsumed k = PushInput (LiftI2 (InstrPureSameOffset sameOffset) (If k (Fail [])))
 335
 336 -- | @('makeJoin' k f)@ factorizes @(k)@ in @(f)@,
 337 -- by introducing a 'DefJoin' if necessary,
 338 -- and passing the corresponding 'RefJoin' to @(f)@,
 339 -- or @(k)@ as is when factorizing is useless.
 340 makeJoin ::
 341   Instr inp (v : vs) es ret ->
 342   (Instr inp (v : vs) es ret -> Instr inp vs es ret) ->
 343   Instr inp vs es ret
 344 -- Double RefJoin Optimization:
 345 -- If a join-node points directly to another join-node,
 346 -- then reuse it
 347 makeJoin k@RefJoin{} = ($ k)
 348 -- Terminal RefJoin Optimization:
 349 -- If a join-node points directly to a terminal operation,
 350 -- then it's useless to introduce a join-point.
 351 makeJoin k@Ret = ($ k)
 352 makeJoin k =
 353   let joinName = LetName $ unsafePerformIO $ TH.qNewName "join" in
 354   \f -> DefJoin joinName k (f (RefJoin joinName))
 355
 356 instance tok ~ InputToken inp => Satisfiable (Machine inp) tok where
 357   satisfy es p = Machine $ Read es (InstrPure p)
 358 instance Selectable (Machine inp) where
 359   branch (Machine lr) (Machine l) (Machine r) = Machine $ \k ->
 360     makeJoin k $ \j ->
 361     lr (Case (l (Swap (App j)))
 362              (r (Swap (App j))))
 363 instance Matchable (Machine inp) where
 364   conditional ps bs (Machine m) (Machine default_) = Machine $ \k ->
 365     makeJoin k $ \j ->
 366     m (Choices (InstrPure Functor.<$> ps)
 367                ((\b -> unMachine b j) Functor.<$> bs)
 368                (default_ j))
 369 instance
 370   ( Ord (InputToken inp)
 371   , Cursorable (Cursor inp)
 372   ) => Lookable (Machine inp) where
 373   look (Machine x) = Machine $ \k ->
 374     PushInput (x (Swap (LoadInput k)))
 375   eof = negLook (satisfy [{-discarded by negLook-}] (H.const H..@ H.bool True))
 376         -- Set a better failure message
 377         <|> (Machine $ \_k -> Fail [ErrorItemEnd])
 378   negLook (Machine x) = Machine $ \k ->
 379     CatchFail
 380       -- On x success, discard the result,
 381       -- and replace this 'CatchFail''s failure handler
 382       -- by a 'Fail'ure whose 'farthestExpecting' is negated,
 383       -- then a failure is raised from the input
 384       -- when entering 'negLook', to avoid odd cases:
 385       -- - where the failure that made (negLook x)
 386       --   succeed can get the blame for the overall
 387       --   failure of the grammar.
 388       -- - where the overall failure of
 389       --   the grammar might be blamed on something in x
 390       --   that, if corrected, still makes x succeed and
 391       --   (negLook x) fail.
 392       (PushInput (x (Pop (PopFail (LoadInput (Fail []))))))
 393       -- On x failure, reset the input,
 394       -- and go on with the next 'Instr'uctions.
 395       (LoadInput (Push (InstrPure H.unit) k))
 396 instance Letable TH.Name (Machine inp) where
 397   def n v = Machine $ \k ->
 398     Subroutine (LetName n) (unMachine v Ret) (Call (LetName n) k)
 399   ref _isRec n = Machine $ \case
 400     Ret -> Jump (LetName n)
 401     k -> Call (LetName n) k
 402 instance Cursorable (Cursor inp) => Foldable (Machine inp) where
 403   {-
 404   chainPre op p = go <*> p
 405     where go = (H..) <$> op <*> go <|> pure H.id
 406   chainPost p op = p <**> go
 407     where go = (H..) <$> op <*> go <|> pure H.id
 408   -}