src/Symantic/Parser/Machine/Instructions.hs

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