src/Symantic/Parser/Machine/Instructions.hs

   1 {-# LANGUAGE ConstraintKinds #-} -- For Executable
   2 {-# LANGUAGE DerivingStrategies #-} -- For Show (LetName a)
   3 {-# LANGUAGE PatternSynonyms #-} -- For Instr
   4 {-# LANGUAGE ViewPatterns #-} -- For unSomeInstr
   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.Maybe (Maybe(..))
  11 import Data.Function ((.))
  12 import Data.Kind (Constraint, Type)
  13 import Type.Reflection (Typeable, typeRep, eqTypeRep, (:~~:)(..))
  14 import Text.Show (Show(..))
  15 import qualified Data.Functor as Functor
  16 import qualified Language.Haskell.TH 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 'Peano'
  27 -- | Type-level natural numbers,
  28 -- using the Peano recursive encoding.
  29 data Peano = Zero | Succ Peano
  30
  31 -- * Class 'Executable'
  32 -- | All the 'Instr'uctions.
  33 type Executable tok repr =
  34   ( Branchable repr
  35   , Failable repr
  36   , Inputable repr
  37   , Joinable repr
  38   , Routinable repr
  39   , Stackable repr
  40   , Readable tok repr
  41   )
  42
  43 -- * Data family 'Instr'
  44 -- | 'Instr'uctions for the 'Machine'.
  45 -- This is an extensible data-type.
  46 data family Instr
  47   (instr :: ReprInstr -> Constraint)
  48   (repr :: ReprInstr)
  49   :: ReprInstr
  50
  51 -- | Convenient utility to pattern-match a 'SomeInstr'.
  52 pattern Instr :: Typeable comb =>
  53   Instr comb repr inp vs es a ->
  54   SomeInstr repr inp vs es a
  55 pattern Instr x <- (unSomeInstr -> Just x)
  56
  57 -- ** Type 'ReprInstr'
  58 type ReprInstr = Type -> [Type] -> Peano -> Type -> Type
  59
  60 -- ** Type 'SomeInstr'
  61 -- | Some 'Instr'uction existantialized over the actual instruction symantic class.
  62 -- Useful to handle a list of 'Instr'uctions
  63 -- without requiring impredicative quantification.
  64 -- Must be used by pattern-matching
  65 -- on the 'SomeInstr' data-constructor,
  66 -- to bring the constraints in scope.
  67 data SomeInstr repr inp vs es a =
  68   forall instr.
  69   (Trans (Instr instr repr inp vs es) (repr inp vs es), Typeable instr) =>
  70   SomeInstr (Instr instr repr inp vs es a)
  71
  72 instance Trans (SomeInstr repr inp vs es) (repr inp vs es) where
  73   trans (SomeInstr x) = trans x
  74
  75 -- | @(unSomeInstr i :: 'Maybe' ('Instr' comb repr inp vs es a))@
  76 -- extract the data-constructor from the given 'SomeInstr'
  77 -- iif. it belongs to the @('Instr' comb repr a)@ data-instance.
  78 unSomeInstr ::
  79   forall instr repr inp vs es a.
  80   Typeable instr =>
  81   SomeInstr repr inp vs es a ->
  82   Maybe (Instr instr repr inp vs es a)
  83 unSomeInstr (SomeInstr (i::Instr i repr inp vs es a)) =
  84   case typeRep @instr `eqTypeRep` typeRep @i of
  85     Just HRefl -> Just i
  86     Nothing -> Nothing
  87
  88 -- ** Type 'LetName'
  89 newtype LetName a = LetName { unLetName :: TH.Name }
  90   deriving (Eq)
  91   deriving newtype Show
  92
  93 -- ** Class 'Stackable'
  94 class Stackable (repr::ReprInstr) where
  95   push ::
  96     TermInstr v ->
  97     repr inp (v ': vs) n ret ->
  98     repr inp vs n ret
  99   pop ::
 100     repr inp vs n ret ->
 101     repr inp (v ': vs) n ret
 102   liftI2 ::
 103     TermInstr (x -> y -> z) ->
 104     repr inp (z ': vs) es ret ->
 105     repr inp (y ': x ': vs) es ret
 106   swap ::
 107     repr inp (x ': y ': vs) n r ->
 108     repr inp (y ': x ': vs) n r
 109 data instance Instr Stackable repr inp vs fs a where
 110   -- | @('Push' x k)@ pushes @(x)@ on the 'valueStack'
 111   -- and continues with the next 'Instr'uction @(k)@.
 112   Push ::
 113     TermInstr v ->
 114     SomeInstr repr inp (v ': vs) es a ->
 115     Instr Stackable repr inp vs es a
 116   -- | @('Pop' k)@ pushes @(x)@ on the 'valueStack'.
 117   Pop ::
 118     SomeInstr repr inp vs es a ->
 119     Instr Stackable repr inp (v ': vs) es a
 120   -- | @('LiftI2' f k)@ pops two values from the 'valueStack',
 121   -- and pushes the result of @(f)@ applied to them.
 122   LiftI2 ::
 123     TermInstr (x -> y -> z) ->
 124     SomeInstr repr inp (z : vs) es a ->
 125     Instr Stackable repr inp (y : x : vs) es a
 126   -- | @('Swap' k)@ pops two values on the 'valueStack',
 127   -- pushes the first popped-out, then the second,
 128   -- and continues with the next 'Instr'uction @(k)@.
 129   Swap ::
 130     SomeInstr repr inp (x ': y ': vs) es a ->
 131     Instr Stackable repr inp (y ': x ': vs) es a
 132 instance Stackable repr => Trans (Instr Stackable repr inp vs es) (repr inp vs es) where
 133   trans = \case
 134     Push x k -> push x (trans k)
 135     Pop k -> pop (trans k)
 136     LiftI2 f k -> liftI2 f (trans k)
 137     Swap k -> swap (trans k)
 138 instance Stackable repr => Stackable (SomeInstr repr) where
 139   push v = SomeInstr . Push v
 140   pop = SomeInstr . Pop
 141   liftI2 f = SomeInstr . LiftI2 f
 142   swap = SomeInstr . Swap
 143
 144 -- | @('mapI' f k)@.
 145 mapI ::
 146   Stackable repr =>
 147   TermInstr (x -> y) ->
 148   SomeInstr repr inp (y ': vs) es ret ->
 149   SomeInstr repr inp (x ': vs) es ret
 150 mapI f = push f . liftI2 (H.flip H..@ (H.$))
 151
 152 -- | @('appI' k)@ pops @(x)@ and @(x2y)@ from the 'valueStack',
 153 -- pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
 154 appI ::
 155   Stackable repr =>
 156   SomeInstr repr inp (y ': vs) es a ->
 157   SomeInstr repr inp (x ': (x -> y) ': vs) es a
 158 appI = liftI2 (H.$)
 159
 160 -- ** Class 'Routinable'
 161 class Routinable (repr::ReprInstr) where
 162   subroutine ::
 163     LetName v -> repr inp '[] ('Succ 'Zero) v ->
 164     repr inp vs ('Succ es) ret ->
 165     repr inp vs ('Succ es) ret
 166   call ::
 167     LetName v -> repr inp (v ': vs) ('Succ es) ret ->
 168     repr inp vs ('Succ es) ret
 169   ret ::
 170     repr inp '[ret] es ret
 171   jump ::
 172     LetName ret ->
 173     repr inp '[] ('Succ es) ret
 174 data instance Instr Routinable repr inp vs fs a where
 175   -- | @('Subroutine' n v k)@ binds the 'LetName' @(n)@ to the 'Instr'uction's @(v)@,
 176   -- 'Call's @(n)@ and
 177   -- continues with the next 'Instr'uction @(k)@.
 178   Subroutine ::
 179     LetName v -> SomeInstr repr inp '[] ('Succ 'Zero) v ->
 180     SomeInstr repr inp vs ('Succ es) a ->
 181     Instr Routinable repr inp vs ('Succ es) a
 182   -- | @('Jump' n k)@ pass the control-flow to the 'Subroutine' named @(n)@.
 183   Jump ::
 184     LetName a ->
 185     Instr Routinable repr inp '[] ('Succ es) a
 186   -- | @('Call' n k)@ pass the control-flow to the 'Subroutine' named @(n)@,
 187   -- and when it 'Ret'urns, continues with the next 'Instr'uction @(k)@.
 188   Call ::
 189     LetName v ->
 190     SomeInstr repr inp (v ': vs) ('Succ es) a ->
 191     Instr Routinable repr inp vs ('Succ es) a
 192   -- | @('Ret')@ returns the value stored in a singleton 'valueStack'.
 193   Ret ::
 194     Instr Routinable repr inp '[a] es a
 195 instance Routinable repr => Trans (Instr Routinable repr inp vs es) (repr inp vs es) where
 196   trans = \case
 197     Subroutine n sub k -> subroutine n (trans sub) (trans k)
 198     Jump n -> jump n
 199     Call n k -> call n (trans k)
 200     Ret -> ret
 201 instance Routinable repr => Routinable (SomeInstr repr) where
 202   subroutine n sub = SomeInstr . Subroutine n sub
 203   jump = SomeInstr . Jump
 204   call n = SomeInstr . Call n
 205   ret = SomeInstr Ret
 206
 207 -- ** Class 'Branchable'
 208 class Branchable (repr::ReprInstr) where
 209   caseI ::
 210     repr inp (x ': vs) n r ->
 211     repr inp (y ': vs) n r ->
 212     repr inp (Either x y ': vs) n r
 213   choices ::
 214     [TermInstr (v -> Bool)] ->
 215     [repr inp vs es ret] ->
 216     repr inp vs es ret ->
 217     repr inp (v ': vs) es ret
 218 data instance Instr Branchable repr inp vs fs a where
 219   -- | @('Case' l r)@.
 220   Case ::
 221     SomeInstr repr inp (x ': vs) es a ->
 222     SomeInstr repr inp (y ': vs) es a ->
 223     Instr Branchable repr inp (Either x y ': vs) es a
 224   -- | @('Choices' ps bs d)@.
 225   Choices ::
 226     [TermInstr (v -> Bool)] ->
 227     [SomeInstr repr inp vs es a] ->
 228     SomeInstr repr inp vs es a ->
 229     Instr Branchable repr inp (v ': vs) es a
 230 instance Branchable repr => Trans (Instr Branchable repr inp vs es) (repr inp vs es) where
 231   trans = \case
 232     Case l r -> caseI (trans l) (trans r)
 233     Choices ps bs d -> choices ps (trans Functor.<$> bs) (trans d)
 234 instance Branchable repr => Branchable (SomeInstr repr) where
 235   caseI l = SomeInstr . Case l
 236   choices ps bs = SomeInstr . Choices ps bs
 237
 238 -- | @('ifI' ok ko)@ pops a 'Bool' from the 'valueStack'
 239 -- and continues either with the 'Instr'uction @(ok)@ if it is 'True'
 240 -- or @(ko)@ otherwise.
 241 ifI ::
 242   Branchable repr =>
 243   SomeInstr repr inp vs es a ->
 244   SomeInstr repr inp vs es a ->
 245   SomeInstr repr inp (Bool ': vs) es a
 246 ifI ok ko = SomeInstr (Choices [H.id] [ok] ko)
 247
 248 -- ** Class 'Failable'
 249 class Failable (repr::ReprInstr) where
 250   fail ::
 251     [ErrorItem (InputToken inp)] ->
 252     repr inp vs ('Succ es) ret
 253   popFail ::
 254     repr inp vs es ret ->
 255     repr inp vs ('Succ es) ret
 256   catchFail ::
 257     repr inp vs ('Succ es) ret ->
 258     repr inp (Cursor inp ': vs) es ret ->
 259     repr inp vs es ret
 260 data instance Instr Failable repr inp vs fs a where
 261   -- | @('Fail')@ raises an error from the 'failStack'.
 262   Fail ::
 263     [ErrorItem (InputToken inp)] ->
 264     Instr Failable repr inp vs ('Succ es) a
 265   -- | @('PopFail' k)@ removes a 'FailHandler' from the 'failStack'
 266   -- and continues with the next 'Instr'uction @(k)@.
 267   PopFail ::
 268     SomeInstr repr inp vs es ret ->
 269     Instr Failable repr inp vs ('Succ es) ret
 270   -- | @('CatchFail' l r)@ tries the @(l)@ 'Instr'uction
 271   -- in a new failure scope such that if @(l)@ raises a failure, it is caught,
 272   -- then the input is pushed as it was before trying @(l)@ on the 'valueStack',
 273   -- and the control flow goes on with the @(r)@ 'Instr'uction.
 274   CatchFail ::
 275     SomeInstr repr inp vs ('Succ es) ret ->
 276     SomeInstr repr inp (Cursor inp ': vs) es ret ->
 277     Instr Failable repr inp vs es ret
 278 instance Failable repr => Trans (Instr Failable repr inp vs es) (repr inp vs es) where
 279   trans = \case
 280     Fail err -> fail err
 281     PopFail k -> popFail (trans k)
 282     CatchFail l r -> catchFail (trans l) (trans r)
 283 instance Failable repr => Failable (SomeInstr repr) where
 284   fail = SomeInstr . Fail
 285   popFail = SomeInstr . PopFail
 286   catchFail x = SomeInstr . CatchFail x
 287
 288 -- ** Class 'Inputable'
 289 class Inputable (repr::ReprInstr) where
 290   loadInput ::
 291     repr inp vs es a ->
 292     repr inp (Cursor inp ': vs) es a
 293   pushInput ::
 294     repr inp (Cursor inp ': vs) es a ->
 295     repr inp vs es a
 296 data instance Instr Inputable repr inp vs fs a where
 297   -- | @('LoadInput' k)@ removes the input from the 'valueStack'
 298   -- and continues with the next 'Instr'uction @(k)@ using that input.
 299   LoadInput ::
 300     SomeInstr repr inp vs es a ->
 301     Instr Inputable repr inp (Cursor inp : vs) es a
 302   -- | @('PushInput' k)@ pushes the input @(inp)@ on the 'valueStack'
 303   -- and continues with the next 'Instr'uction @(k)@.
 304   PushInput ::
 305     SomeInstr repr inp (Cursor inp ': vs) es a ->
 306     Instr Inputable repr inp vs es a
 307 instance Inputable repr => Trans (Instr Inputable repr inp vs es) (repr inp vs es) where
 308   trans = \case
 309     LoadInput k -> loadInput (trans k)
 310     PushInput k -> pushInput (trans k)
 311 instance Inputable repr => Inputable (SomeInstr repr) where
 312   loadInput = SomeInstr . LoadInput
 313   pushInput = SomeInstr . PushInput
 314
 315 -- ** Class 'Joinable'
 316 class Joinable (repr::ReprInstr) where
 317   defJoin ::
 318     LetName v ->
 319     repr inp (v ': vs) es a ->
 320     repr inp vs es a ->
 321     repr inp vs es a
 322   refJoin ::
 323     LetName v ->
 324     repr inp (v ': vs) es a
 325 data instance Instr Joinable repr inp vs fs a where
 326   DefJoin ::
 327     LetName v -> SomeInstr repr inp (v ': vs) es a ->
 328     SomeInstr repr inp vs es a ->
 329     Instr Joinable repr inp vs es a
 330   RefJoin ::
 331     LetName v ->
 332     Instr Joinable repr inp (v ': vs) es a
 333 instance Joinable repr => Trans (Instr Joinable repr inp vs es) (repr inp vs es) where
 334   trans = \case
 335     DefJoin n sub k -> defJoin n (trans sub) (trans k)
 336     RefJoin n -> refJoin n
 337 instance Joinable repr => Joinable (SomeInstr repr) where
 338   defJoin n sub = SomeInstr . DefJoin n sub
 339   refJoin = SomeInstr . RefJoin
 340
 341 -- ** Class 'Readable'
 342 class Readable (tok::Type) (repr::ReprInstr) where
 343   read ::
 344     tok ~ InputToken inp =>
 345     [ErrorItem tok] ->
 346     TermInstr (tok -> Bool) ->
 347     repr inp (tok ': vs) ('Succ es) ret ->
 348     repr inp vs ('Succ es) ret
 349 data instance Instr (Readable tok) repr inp vs fs a where
 350   -- | @('Read' expected p k)@ reads a 'Char' @(c)@ from the 'inp'ut,
 351   -- if @(p c)@ is 'True' then continues with the next 'Instr'uction @(k)@ on,
 352   -- otherwise 'Fail'.
 353   Read ::
 354     [ErrorItem (InputToken inp)] ->
 355     TermInstr (InputToken inp -> Bool) ->
 356     SomeInstr repr inp (InputToken inp ': vs) ('Succ es) a ->
 357     Instr (Readable tok) repr inp vs ('Succ es) a
 358 instance
 359   ( Readable tok repr, tok ~ InputToken inp ) =>
 360   Trans (Instr (Readable tok) repr inp vs es) (repr inp vs es) where
 361   trans = \case
 362     Read es p k -> read es p (trans k)
 363 instance
 364   ( Readable tok repr, Typeable tok ) =>
 365   Readable tok (SomeInstr repr) where
 366   read es p = SomeInstr . Read es p