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