src/Symantic/Parser/Machine/Instructions.hs

   1 {-# LANGUAGE ConstraintKinds #-} -- For Machine
   2 {-# LANGUAGE DerivingStrategies #-} -- For Show (LetName a)
   3 -- | Semantic of the parsing instructions used
   4 -- to make the parsing control-flow explicit,
   5 -- in the convenient tagless-final encoding.
   6 module Symantic.Parser.Machine.Instructions where
   7
   8 import Data.Bool (Bool(..))
   9 import Data.Either (Either)
  10 import Data.Eq (Eq(..))
  11 import Data.Function ((.))
  12 import Data.Kind (Type)
  13 -- import GHC.TypeLits (Symbol)
  14 import Text.Show (Show(..))
  15 import qualified Language.Haskell.TH as TH
  16 import qualified Symantic.Parser.Haskell as H
  17
  18 import Symantic.Parser.Grammar
  19 import Symantic.Parser.Machine.Input
  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 'Machine'
  30 -- | All the 'Instr'uctions.
  31 type Machine 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 -- ** Type 'ReprInstr'
  42 type ReprInstr = Type -> [Type] -> Peano -> Type -> Type
  43
  44 -- ** Type 'LetName'
  45 newtype LetName a = LetName { unLetName :: TH.Name }
  46   deriving (Eq)
  47   deriving newtype Show
  48
  49 -- ** Class 'Stackable'
  50 class Stackable (repr::ReprInstr) where
  51   push ::
  52     TermInstr v ->
  53     repr inp (v ': vs) n a ->
  54     repr inp vs n a
  55   pop ::
  56     repr inp vs n a ->
  57     repr inp (v ': vs) n a
  58   liftI2 ::
  59     TermInstr (x -> y -> z) ->
  60     repr inp (z ': vs) es a ->
  61     repr inp (y ': x ': vs) es a
  62   swap ::
  63     repr inp (x ': y ': vs) n r ->
  64     repr inp (y ': x ': vs) n r
  65   -- | @('mapI' f k)@.
  66   mapI ::
  67     TermInstr (x -> y) ->
  68     repr inp (y ': vs) es a ->
  69     repr inp (x ': vs) es a
  70   mapI f = push f . liftI2 (H.flip H..@ (H.$))
  71   -- | @('appI' k)@ pops @(x)@ and @(x2y)@ from the 'valueStack',
  72   -- pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
  73   appI ::
  74     repr inp (y ': vs) es a ->
  75     repr inp (x ': (x -> y) ': vs) es a
  76   appI = liftI2 (H.$)
  77
  78 -- ** Class 'Routinable'
  79 class Routinable (repr::ReprInstr) where
  80   subroutine ::
  81     LetName v -> repr inp '[] ('Succ 'Zero) v ->
  82     repr inp vs ('Succ es) a ->
  83     repr inp vs ('Succ es) a
  84   call ::
  85     LetName v -> repr inp (v ': vs) ('Succ es) a ->
  86     repr inp vs ('Succ es) a
  87   ret ::
  88     repr inp '[a] es a
  89   jump ::
  90     LetName a ->
  91     repr inp '[] ('Succ es) a
  92
  93 -- ** Class 'Branchable'
  94 class Branchable (repr::ReprInstr) where
  95   caseI ::
  96     repr inp (x ': vs) n r ->
  97     repr inp (y ': vs) n r ->
  98     repr inp (Either x y ': vs) n r
  99   choices ::
 100     [TermInstr (v -> Bool)] ->
 101     [repr inp vs es a] ->
 102     repr inp vs es a ->
 103     repr inp (v ': vs) es a
 104   -- | @('ifI' ok ko)@ pops a 'Bool' from the 'valueStack'
 105   -- and continues either with the 'Instr'uction @(ok)@ if it is 'True'
 106   -- or @(ko)@ otherwise.
 107   ifI ::
 108     repr inp vs es a ->
 109     repr inp vs es a ->
 110     repr inp (Bool ': vs) es a
 111   ifI ok ko = choices [H.id] [ok] ko
 112
 113 -- ** Class 'Failable'
 114 class Failable (repr::ReprInstr) where
 115   fail ::
 116     [ErrorItem (InputToken inp)] ->
 117     repr inp vs ('Succ es) a
 118   popFail ::
 119     repr inp vs es a ->
 120     repr inp vs ('Succ es) a
 121   catchFail ::
 122     repr inp vs ('Succ es) a ->
 123     repr inp (Cursor inp ': vs) es a ->
 124     repr inp vs es a
 125
 126 -- ** Class 'Inputable'
 127 class Inputable (repr::ReprInstr) where
 128   loadInput ::
 129     repr inp vs es a ->
 130     repr inp (Cursor inp ': vs) es a
 131   pushInput ::
 132     repr inp (Cursor inp ': vs) es a ->
 133     repr inp vs es a
 134
 135 -- ** Class 'Joinable'
 136 class Joinable (repr::ReprInstr) where
 137   defJoin ::
 138     LetName v ->
 139     repr inp (v ': vs) es a ->
 140     repr inp vs es a ->
 141     repr inp vs es a
 142   refJoin ::
 143     LetName v ->
 144     repr inp (v ': vs) es a
 145
 146 -- ** Class 'Readable'
 147 class Readable (tok::Type) (repr::ReprInstr) where
 148   read ::
 149     tok ~ InputToken inp =>
 150     [ErrorItem tok] ->
 151     TermInstr (tok -> Bool) ->
 152     repr inp (tok ': vs) ('Succ es) a ->
 153     repr inp vs ('Succ es) a