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