src/Symantic/Parser/Machine/Optimize.hs

   1 {-# LANGUAGE PatternSynonyms #-} -- For Instr
   2 {-# LANGUAGE ViewPatterns #-} -- For unSomeInstr
   3 {-# LANGUAGE UndecidableInstances #-}
   4 -- | Initial encoding with bottom-up optimizations of 'Instr'uctions,
   5 -- re-optimizing downward as needed after each optimization.
   6 -- There is only one optimization (for 'push') so far,
   7 -- but the introspection enabled by the 'Instr' data-type
   8 -- is also useful to optimize with more context in the 'Machine'.
   9 module Symantic.Parser.Machine.Optimize where
  10
  11 import Data.Bool (Bool(..))
  12 import Data.Either (Either)
  13 import Data.Maybe (Maybe(..))
  14 import Data.Function ((.))
  15 import Data.Kind (Constraint)
  16 import Type.Reflection (Typeable, typeRep, eqTypeRep, (:~~:)(..))
  17 import qualified Data.Functor as Functor
  18
  19 import Symantic.Parser.Grammar
  20 import Symantic.Parser.Machine.Input
  21 import Symantic.Parser.Machine.Instructions
  22 import Symantic.Univariant.Trans
  23
  24 -- * Data family 'Instr'
  25 -- | 'Instr'uctions of the 'Machine'.
  26 -- This is an extensible data-type.
  27 data family Instr
  28   (instr :: ReprInstr -> Constraint)
  29   (repr :: ReprInstr)
  30   :: ReprInstr
  31
  32 -- | Convenient utility to pattern-match a 'SomeInstr'.
  33 pattern Instr :: Typeable comb =>
  34   Instr comb repr inp vs es a ->
  35   SomeInstr repr inp vs es a
  36 pattern Instr x <- (unSomeInstr -> Just x)
  37
  38 -- ** Type 'SomeInstr'
  39 -- | Some 'Instr'uction existantialized over the actual instruction symantic class.
  40 -- Useful to handle a list of 'Instr'uctions
  41 -- without requiring impredicative quantification.
  42 -- Must be used by pattern-matching
  43 -- on the 'SomeInstr' data-constructor,
  44 -- to bring the constraints in scope.
  45 --
  46 -- As in 'SomeComb', a first pass of optimizations
  47 -- is directly applied in it
  48 -- to avoid introducing an extra newtype,
  49 -- this also give a more comprehensible code.
  50 data SomeInstr repr inp vs es a =
  51   forall instr.
  52   (Trans (Instr instr repr inp vs es) (repr inp vs es), Typeable instr) =>
  53   SomeInstr (Instr instr repr inp vs es a)
  54
  55 instance Trans (SomeInstr repr inp vs es) (repr inp vs es) where
  56   trans (SomeInstr x) = trans x
  57
  58 -- | @(unSomeInstr i :: 'Maybe' ('Instr' comb repr inp vs es a))@
  59 -- extract the data-constructor from the given 'SomeInstr'
  60 -- iif. it belongs to the @('Instr' comb repr a)@ data-instance.
  61 unSomeInstr ::
  62   forall instr repr inp vs es a.
  63   Typeable instr =>
  64   SomeInstr repr inp vs es a ->
  65   Maybe (Instr instr repr inp vs es a)
  66 unSomeInstr (SomeInstr (i::Instr i repr inp vs es a)) =
  67   case typeRep @instr `eqTypeRep` typeRep @i of
  68     Just HRefl -> Just i
  69     Nothing -> Nothing
  70
  71 -- Stackable
  72 data instance Instr Stackable repr inp vs fs a where
  73   -- | @('Push' x k)@ pushes @(x)@ on the 'valueStack'
  74   -- and continues with the next 'Instr'uction @(k)@.
  75   Push ::
  76     TermInstr v ->
  77     SomeInstr repr inp (v ': vs) es a ->
  78     Instr Stackable repr inp vs es a
  79   -- | @('Pop' k)@ pushes @(x)@ on the 'valueStack'.
  80   Pop ::
  81     SomeInstr repr inp vs es a ->
  82     Instr Stackable repr inp (v ': vs) es a
  83   -- | @('LiftI2' f k)@ pops two values from the 'valueStack',
  84   -- and pushes the result of @(f)@ applied to them.
  85   LiftI2 ::
  86     TermInstr (x -> y -> z) ->
  87     SomeInstr repr inp (z : vs) es a ->
  88     Instr Stackable repr inp (y : x : vs) es a
  89   -- | @('Swap' k)@ pops two values on the 'valueStack',
  90   -- pushes the first popped-out, then the second,
  91   -- and continues with the next 'Instr'uction @(k)@.
  92   Swap ::
  93     SomeInstr repr inp (x ': y ': vs) es a ->
  94     Instr Stackable repr inp (y ': x ': vs) es a
  95 instance Stackable repr => Trans (Instr Stackable repr inp vs es) (repr inp vs es) where
  96   trans = \case
  97     Push x k -> push x (trans k)
  98     Pop k -> pop (trans k)
  99     LiftI2 f k -> liftI2 f (trans k)
 100     Swap k -> swap (trans k)
 101 instance Stackable repr => Stackable (SomeInstr repr) where
 102   push _v (Instr (Pop i)) = i
 103   push v i = SomeInstr (Push v i)
 104   pop = SomeInstr . Pop
 105   liftI2 f = SomeInstr . LiftI2 f
 106   swap = SomeInstr . Swap
 107
 108 -- Routinable
 109 data instance Instr Routinable repr inp vs fs a where
 110   -- | @('Subroutine' n v k)@ binds the 'LetName' @(n)@ to the 'Instr'uction's @(v)@,
 111   -- 'Call's @(n)@ and
 112   -- continues with the next 'Instr'uction @(k)@.
 113   Subroutine ::
 114     LetName v -> SomeInstr repr inp '[] ('Succ 'Zero) v ->
 115     SomeInstr repr inp vs ('Succ es) a ->
 116     Instr Routinable repr inp vs ('Succ es) a
 117   -- | @('Jump' n k)@ pass the control-flow to the 'Subroutine' named @(n)@.
 118   Jump ::
 119     LetName a ->
 120     Instr Routinable repr inp '[] ('Succ es) a
 121   -- | @('Call' n k)@ pass the control-flow to the 'Subroutine' named @(n)@,
 122   -- and when it 'Ret'urns, continues with the next 'Instr'uction @(k)@.
 123   Call ::
 124     LetName v ->
 125     SomeInstr repr inp (v ': vs) ('Succ es) a ->
 126     Instr Routinable repr inp vs ('Succ es) a
 127   -- | @('Ret')@ returns the value stored in a singleton 'valueStack'.
 128   Ret ::
 129     Instr Routinable repr inp '[a] es a
 130 instance Routinable repr => Trans (Instr Routinable repr inp vs es) (repr inp vs es) where
 131   trans = \case
 132     Subroutine n sub k -> subroutine n (trans sub) (trans k)
 133     Jump n -> jump n
 134     Call n k -> call n (trans k)
 135     Ret -> ret
 136 instance Routinable repr => Routinable (SomeInstr repr) where
 137   subroutine n sub = SomeInstr . Subroutine n sub
 138   jump = SomeInstr . Jump
 139   call n = SomeInstr . Call n
 140   ret = SomeInstr Ret
 141
 142 -- Branchable
 143 data instance Instr Branchable repr inp vs fs a where
 144   -- | @('Case' l r)@.
 145   Case ::
 146     SomeInstr repr inp (x ': vs) es a ->
 147     SomeInstr repr inp (y ': vs) es a ->
 148     Instr Branchable repr inp (Either x y ': vs) es a
 149   -- | @('Choices' ps bs d)@.
 150   Choices ::
 151     [TermInstr (v -> Bool)] ->
 152     [SomeInstr repr inp vs es a] ->
 153     SomeInstr repr inp vs es a ->
 154     Instr Branchable repr inp (v ': vs) es a
 155 instance Branchable repr => Trans (Instr Branchable repr inp vs es) (repr inp vs es) where
 156   trans = \case
 157     Case l r -> caseI (trans l) (trans r)
 158     Choices ps bs d -> choices ps (trans Functor.<$> bs) (trans d)
 159 instance Branchable repr => Branchable (SomeInstr repr) where
 160   caseI l = SomeInstr . Case l
 161   choices ps bs = SomeInstr . Choices ps bs
 162
 163 -- Failable
 164 data instance Instr Failable repr inp vs fs a where
 165   -- | @('Fail')@ raises an error from the 'failStack'.
 166   Fail ::
 167     [ErrorItem (InputToken inp)] ->
 168     Instr Failable repr inp vs ('Succ es) a
 169   -- | @('PopFail' k)@ removes a 'FailHandler' from the 'failStack'
 170   -- and continues with the next 'Instr'uction @(k)@.
 171   PopFail ::
 172     SomeInstr repr inp vs es ret ->
 173     Instr Failable repr inp vs ('Succ es) ret
 174   -- | @('CatchFail' l r)@ tries the @(l)@ 'Instr'uction
 175   -- in a new failure scope such that if @(l)@ raises a failure, it is caught,
 176   -- then the input is pushed as it was before trying @(l)@ on the 'valueStack',
 177   -- and the control flow goes on with the @(r)@ 'Instr'uction.
 178   CatchFail ::
 179     SomeInstr repr inp vs ('Succ es) ret ->
 180     SomeInstr repr inp (Cursor inp ': vs) es ret ->
 181     Instr Failable repr inp vs es ret
 182 instance Failable repr => Trans (Instr Failable repr inp vs es) (repr inp vs es) where
 183   trans = \case
 184     Fail err -> fail err
 185     PopFail k -> popFail (trans k)
 186     CatchFail l r -> catchFail (trans l) (trans r)
 187 instance Failable repr => Failable (SomeInstr repr) where
 188   fail = SomeInstr . Fail
 189   popFail = SomeInstr . PopFail
 190   catchFail x = SomeInstr . CatchFail x
 191
 192 -- Inputable
 193 data instance Instr Inputable repr inp vs fs a where
 194   -- | @('LoadInput' k)@ removes the input from the 'valueStack'
 195   -- and continues with the next 'Instr'uction @(k)@ using that input.
 196   LoadInput ::
 197     SomeInstr repr inp vs es a ->
 198     Instr Inputable repr inp (Cursor inp : vs) es a
 199   -- | @('PushInput' k)@ pushes the input @(inp)@ on the 'valueStack'
 200   -- and continues with the next 'Instr'uction @(k)@.
 201   PushInput ::
 202     SomeInstr repr inp (Cursor inp ': vs) es a ->
 203     Instr Inputable repr inp vs es a
 204 instance Inputable repr => Trans (Instr Inputable repr inp vs es) (repr inp vs es) where
 205   trans = \case
 206     LoadInput k -> loadInput (trans k)
 207     PushInput k -> pushInput (trans k)
 208 instance Inputable repr => Inputable (SomeInstr repr) where
 209   loadInput = SomeInstr . LoadInput
 210   pushInput = SomeInstr . PushInput
 211
 212 -- Joinable
 213 data instance Instr Joinable repr inp vs fs a where
 214   DefJoin ::
 215     LetName v -> SomeInstr repr inp (v ': vs) es a ->
 216     SomeInstr repr inp vs es a ->
 217     Instr Joinable repr inp vs es a
 218   RefJoin ::
 219     LetName v ->
 220     Instr Joinable repr inp (v ': vs) es a
 221 instance Joinable repr => Trans (Instr Joinable repr inp vs es) (repr inp vs es) where
 222   trans = \case
 223     DefJoin n sub k -> defJoin n (trans sub) (trans k)
 224     RefJoin n -> refJoin n
 225 instance Joinable repr => Joinable (SomeInstr repr) where
 226   defJoin n sub = SomeInstr . DefJoin n sub
 227   refJoin = SomeInstr . RefJoin
 228
 229 -- Readable
 230 data instance Instr (Readable tok) repr inp vs fs a where
 231   -- | @('Read' expected p k)@ reads a 'Char' @(c)@ from the 'inp'ut,
 232   -- if @(p c)@ is 'True' then continues with the next 'Instr'uction @(k)@ on,
 233   -- otherwise 'Fail'.
 234   Read ::
 235     [ErrorItem (InputToken inp)] ->
 236     TermInstr (InputToken inp -> Bool) ->
 237     SomeInstr repr inp (InputToken inp ': vs) ('Succ es) a ->
 238     Instr (Readable tok) repr inp vs ('Succ es) a
 239 instance
 240   ( Readable tok repr, tok ~ InputToken inp ) =>
 241   Trans (Instr (Readable tok) repr inp vs es) (repr inp vs es) where
 242   trans = \case
 243     Read es p k -> read es p (trans k)
 244 instance
 245   ( Readable tok repr, Typeable tok ) =>
 246   Readable tok (SomeInstr repr) where
 247   read es p = SomeInstr . Read es p