src/Symantic/Parser/Machine/Instructions.hs

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