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 -- | 'TH.Name' of a 'subroutine' or 'defJoin'
  46 -- indexed by the return type of the factorized 'Instr'uctions.
  47 -- This helps type-inferencing.
  48 newtype LetName a = LetName { unLetName :: TH.Name }
  49   deriving Eq
  50   deriving newtype Show
  51
  52 -- ** Class 'Stackable'
  53 class Stackable (repr::ReprInstr) where
  54   push ::
  55     TermInstr v ->
  56     repr inp (v ': vs) n a ->
  57     repr inp vs n a
  58   pop ::
  59     repr inp vs n a ->
  60     repr inp (v ': vs) n a
  61   liftI2 ::
  62     TermInstr (x -> y -> z) ->
  63     repr inp (z ': vs) es a ->
  64     repr inp (y ': x ': vs) es a
  65   swap ::
  66     repr inp (x ': y ': vs) n r ->
  67     repr inp (y ': x ': vs) n r
  68   -- | @('mapI' f k)@.
  69   mapI ::
  70     TermInstr (x -> y) ->
  71     repr inp (y ': vs) es a ->
  72     repr inp (x ': vs) es a
  73   mapI f = push f . liftI2 (H.flip H..@ (H.$))
  74   -- | @('appI' k)@ pops @(x)@ and @(x2y)@ from the 'valueStack',
  75   -- pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
  76   appI ::
  77     repr inp (y ': vs) es a ->
  78     repr inp (x ': (x -> y) ': vs) es a
  79   appI = liftI2 (H.$)
  80
  81 -- ** Class 'Routinable'
  82 class Routinable (repr::ReprInstr) where
  83   subroutine ::
  84     LetName v -> repr inp '[] ('Succ 'Zero) v ->
  85     repr inp vs ('Succ es) a ->
  86     repr inp vs ('Succ es) a
  87   call ::
  88     LetName v -> repr inp (v ': vs) ('Succ es) a ->
  89     repr inp vs ('Succ es) a
  90   ret ::
  91     repr inp '[a] es a
  92   jump ::
  93     LetName a ->
  94     repr inp '[] ('Succ es) a
  95
  96 -- ** Class 'Branchable'
  97 class Branchable (repr::ReprInstr) where
  98   caseI ::
  99     repr inp (x ': vs) n r ->
 100     repr inp (y ': vs) n r ->
 101     repr inp (Either x y ': vs) n r
 102   choices ::
 103     [TermInstr (v -> Bool)] ->
 104     [repr inp vs es a] ->
 105     repr inp vs es a ->
 106     repr inp (v ': vs) es a
 107   -- | @('ifI' ok ko)@ pops a 'Bool' from the 'valueStack'
 108   -- and continues either with the 'Instr'uction @(ok)@ if it is 'True'
 109   -- or @(ko)@ otherwise.
 110   ifI ::
 111     repr inp vs es a ->
 112     repr inp vs es a ->
 113     repr inp (Bool ': vs) es a
 114   ifI ok ko = choices [H.id] [ok] ko
 115
 116 -- ** Class 'Failable'
 117 class Failable (repr::ReprInstr) where
 118   fail ::
 119     [ErrorItem (InputToken inp)] ->
 120     repr inp vs ('Succ es) a
 121   popFail ::
 122     repr inp vs es a ->
 123     repr inp vs ('Succ es) a
 124   catchFail ::
 125     repr inp vs ('Succ es) a ->
 126     repr inp (Cursor inp ': vs) es a ->
 127     repr inp vs es a
 128
 129 -- ** Class 'Inputable'
 130 class Inputable (repr::ReprInstr) where
 131   loadInput ::
 132     repr inp vs es a ->
 133     repr inp (Cursor inp ': vs) es a
 134   pushInput ::
 135     repr inp (Cursor inp ': vs) es a ->
 136     repr inp vs es a
 137
 138 -- ** Class 'Joinable'
 139 class Joinable (repr::ReprInstr) where
 140   defJoin ::
 141     LetName v ->
 142     repr inp (v ': vs) es a ->
 143     repr inp vs es a ->
 144     repr inp vs es a
 145   refJoin ::
 146     LetName v ->
 147     repr inp (v ': vs) es a
 148
 149 -- ** Class 'Readable'
 150 class Readable (tok::Type) (repr::ReprInstr) where
 151   read ::
 152     tok ~ InputToken inp =>
 153     [ErrorItem tok] ->
 154     TermInstr (tok -> Bool) ->
 155     repr inp (tok ': vs) ('Succ es) a ->
 156     repr inp vs ('Succ es) a