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 existentialized 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 ->
 115     SomeInstr repr inp '[] ('Succ 'Zero) v ->
 116     SomeInstr repr inp vs ('Succ es) a ->
 117     Instr Routinable repr inp vs ('Succ es) a
 118   -- | @('Jump' n k)@ pass the control-flow to the 'Subroutine' named @(n)@.
 119   Jump ::
 120     LetName a ->
 121     Instr Routinable repr inp '[] ('Succ es) a
 122   -- | @('Call' n k)@ pass the control-flow to the 'Subroutine' named @(n)@,
 123   -- and when it 'Ret'urns, continues with the next 'Instr'uction @(k)@.
 124   Call ::
 125     LetName v ->
 126     SomeInstr repr inp (v ': vs) ('Succ es) a ->
 127     Instr Routinable repr inp vs ('Succ es) a
 128   -- | @('Ret')@ returns the value stored in a singleton 'valueStack'.
 129   Ret ::
 130     Instr Routinable repr inp '[a] es a
 131 instance Routinable repr => Trans (Instr Routinable repr inp vs es) (repr inp vs es) where
 132   trans = \case
 133     Subroutine n sub k -> subroutine n (trans sub) (trans k)
 134     Jump n -> jump n
 135     Call n k -> call n (trans k)
 136     Ret -> ret
 137 instance Routinable repr => Routinable (SomeInstr repr) where
 138   subroutine n sub = SomeInstr . Subroutine n sub
 139   jump = SomeInstr . Jump
 140   call n = SomeInstr . Call n
 141   ret = SomeInstr Ret
 142
 143 -- Branchable
 144 data instance Instr Branchable repr inp vs fs a where
 145   -- | @('Case' l r)@.
 146   Case ::
 147     SomeInstr repr inp (x ': vs) es a ->
 148     SomeInstr repr inp (y ': vs) es a ->
 149     Instr Branchable repr inp (Either x y ': vs) es a
 150   -- | @('Choices' ps bs d)@.
 151   Choices ::
 152     [TermInstr (v -> Bool)] ->
 153     [SomeInstr repr inp vs es a] ->
 154     SomeInstr repr inp vs es a ->
 155     Instr Branchable repr inp (v ': vs) es a
 156 instance Branchable repr => Trans (Instr Branchable repr inp vs es) (repr inp vs es) where
 157   trans = \case
 158     Case l r -> caseI (trans l) (trans r)
 159     Choices ps bs d -> choices ps (trans Functor.<$> bs) (trans d)
 160 instance Branchable repr => Branchable (SomeInstr repr) where
 161   caseI l = SomeInstr . Case l
 162   choices ps bs = SomeInstr . Choices ps bs
 163
 164 -- Failable
 165 data instance Instr Failable repr inp vs fs a where
 166   -- | @('Fail')@ raises an error from the 'failStack'.
 167   Fail ::
 168     [ErrorItem (InputToken inp)] ->
 169     Instr Failable repr inp vs ('Succ es) a
 170   -- | @('PopFail' k)@ removes a 'FailHandler' from the 'failStack'
 171   -- and continues with the next 'Instr'uction @(k)@.
 172   PopFail ::
 173     SomeInstr repr inp vs es ret ->
 174     Instr Failable repr inp vs ('Succ es) ret
 175   -- | @('CatchFail' l r)@ tries the @(l)@ 'Instr'uction
 176   -- in a new failure scope such that if @(l)@ raises a failure, it is caught,
 177   -- then the input is pushed as it was before trying @(l)@ on the 'valueStack',
 178   -- and the control flow goes on with the @(r)@ 'Instr'uction.
 179   CatchFail ::
 180     SomeInstr repr inp vs ('Succ es) ret ->
 181     SomeInstr repr inp (Cursor inp ': vs) es ret ->
 182     Instr Failable repr inp vs es ret
 183 instance Failable repr => Trans (Instr Failable repr inp vs es) (repr inp vs es) where
 184   trans = \case
 185     Fail err -> fail err
 186     PopFail k -> popFail (trans k)
 187     CatchFail l r -> catchFail (trans l) (trans r)
 188 instance Failable repr => Failable (SomeInstr repr) where
 189   fail = SomeInstr . Fail
 190   popFail = SomeInstr . PopFail
 191   catchFail x = SomeInstr . CatchFail x
 192
 193 -- Inputable
 194 data instance Instr Inputable repr inp vs fs a where
 195   -- | @('LoadInput' k)@ removes the input from the 'valueStack'
 196   -- and continues with the next 'Instr'uction @(k)@ using that input.
 197   LoadInput ::
 198     SomeInstr repr inp vs es a ->
 199     Instr Inputable repr inp (Cursor inp : vs) es a
 200   -- | @('PushInput' k)@ pushes the input @(inp)@ on the 'valueStack'
 201   -- and continues with the next 'Instr'uction @(k)@.
 202   PushInput ::
 203     SomeInstr repr inp (Cursor inp ': vs) es a ->
 204     Instr Inputable repr inp vs es a
 205 instance Inputable repr => Trans (Instr Inputable repr inp vs es) (repr inp vs es) where
 206   trans = \case
 207     LoadInput k -> loadInput (trans k)
 208     PushInput k -> pushInput (trans k)
 209 instance Inputable repr => Inputable (SomeInstr repr) where
 210   loadInput = SomeInstr . LoadInput
 211   pushInput = SomeInstr . PushInput
 212
 213 -- Joinable
 214 data instance Instr Joinable repr inp vs fs a where
 215   DefJoin ::
 216     LetName v ->
 217     SomeInstr repr inp (v ': vs) es a ->
 218     SomeInstr repr inp vs es a ->
 219     Instr Joinable repr inp vs es a
 220   RefJoin ::
 221     LetName v ->
 222     Instr Joinable repr inp (v ': vs) es a
 223 instance Joinable repr => Trans (Instr Joinable repr inp vs es) (repr inp vs es) where
 224   trans = \case
 225     DefJoin n sub k -> defJoin n (trans sub) (trans k)
 226     RefJoin n -> refJoin n
 227 instance Joinable repr => Joinable (SomeInstr repr) where
 228   defJoin n sub = SomeInstr . DefJoin n sub
 229   refJoin = SomeInstr . RefJoin
 230
 231 -- Readable
 232 data instance Instr (Readable tok) repr inp vs fs a where
 233   -- | @('Read' expected p k)@ reads a 'Char' @(c)@ from the 'inp'ut,
 234   -- if @(p c)@ is 'True' then continues with the next 'Instr'uction @(k)@ on,
 235   -- otherwise 'Fail'.
 236   Read ::
 237     [ErrorItem (InputToken inp)] ->
 238     TermInstr (InputToken inp -> Bool) ->
 239     SomeInstr repr inp (InputToken inp ': vs) ('Succ es) a ->
 240     Instr (Readable tok) repr inp vs ('Succ es) a
 241 instance
 242   ( Readable tok repr, tok ~ InputToken inp ) =>
 243   Trans (Instr (Readable tok) repr inp vs es) (repr inp vs es) where
 244   trans = \case
 245     Read es p k -> read es p (trans k)
 246 instance
 247   ( Readable tok repr, Typeable tok ) =>
 248   Readable tok (SomeInstr repr) where
 249   read es p = SomeInstr . Read es p