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 GHC.TypeLits (Symbol)
  18 import qualified Data.Functor as Functor
  19
  20 import Symantic.Parser.Grammar
  21 import Symantic.Parser.Machine.Input
  22 import Symantic.Parser.Machine.Instructions
  23 import Symantic.Univariant.Trans
  24
  25 -- * Data family 'Instr'
  26 -- | 'Instr'uctions for the 'Machine'.
  27 -- This is an extensible data-type.
  28 data family Instr
  29   (instr :: ReprInstr -> Constraint)
  30   (repr :: ReprInstr)
  31   :: ReprInstr
  32
  33 -- | Convenient utility to pattern-match a 'SomeInstr'.
  34 pattern Instr :: Typeable comb =>
  35   Instr comb repr inp vs es a ->
  36   SomeInstr repr inp vs es a
  37 pattern Instr x <- (unSomeInstr -> Just x)
  38
  39 -- ** Type 'SomeInstr'
  40 -- | Some 'Instr'uction existantialized over the actual instruction symantic class.
  41 -- Useful to handle a list of 'Instr'uctions
  42 -- without requiring impredicative quantification.
  43 -- Must be used by pattern-matching
  44 -- on the 'SomeInstr' data-constructor,
  45 -- to bring the constraints in scope.
  46 --
  47 -- As in 'SomeComb', a first pass of optimizations
  48 -- is directly applied in it
  49 -- to avoid introducing an extra newtype,
  50 -- this also give a more comprehensible code.
  51 data SomeInstr repr inp vs es a =
  52   forall instr.
  53   (Trans (Instr instr repr inp vs es) (repr inp vs es), Typeable instr) =>
  54   SomeInstr (Instr instr repr inp vs es a)
  55
  56 instance Trans (SomeInstr repr inp vs es) (repr inp vs es) where
  57   trans (SomeInstr x) = trans x
  58
  59 -- | @(unSomeInstr i :: 'Maybe' ('Instr' comb repr inp vs es a))@
  60 -- extract the data-constructor from the given 'SomeInstr'
  61 -- iif. it belongs to the @('Instr' comb repr a)@ data-instance.
  62 unSomeInstr ::
  63   forall instr repr inp vs es a.
  64   Typeable instr =>
  65   SomeInstr repr inp vs es a ->
  66   Maybe (Instr instr repr inp vs es a)
  67 unSomeInstr (SomeInstr (i::Instr i repr inp vs es a)) =
  68   case typeRep @instr `eqTypeRep` typeRep @i of
  69     Just HRefl -> Just i
  70     Nothing -> Nothing
  71
  72 -- Stackable
  73 data instance Instr Stackable repr inp vs fs a where
  74   -- | @('Push' x k)@ pushes @(x)@ on the 'valueStack'
  75   -- and continues with the next 'Instr'uction @(k)@.
  76   Push ::
  77     TermInstr v ->
  78     SomeInstr repr inp (v ': vs) es a ->
  79     Instr Stackable repr inp vs es a
  80   -- | @('Pop' k)@ pushes @(x)@ on the 'valueStack'.
  81   Pop ::
  82     SomeInstr repr inp vs es a ->
  83     Instr Stackable repr inp (v ': vs) es a
  84   -- | @('LiftI2' f k)@ pops two values from the 'valueStack',
  85   -- and pushes the result of @(f)@ applied to them.
  86   LiftI2 ::
  87     TermInstr (x -> y -> z) ->
  88     SomeInstr repr inp (z : vs) es a ->
  89     Instr Stackable repr inp (y : x : vs) es a
  90   -- | @('Swap' k)@ pops two values on the 'valueStack',
  91   -- pushes the first popped-out, then the second,
  92   -- and continues with the next 'Instr'uction @(k)@.
  93   Swap ::
  94     SomeInstr repr inp (x ': y ': vs) es a ->
  95     Instr Stackable repr inp (y ': x ': vs) es a
  96 instance Stackable repr => Trans (Instr Stackable repr inp vs es) (repr inp vs es) where
  97   trans = \case
  98     Push x k -> push x (trans k)
  99     Pop k -> pop (trans k)
 100     LiftI2 f k -> liftI2 f (trans k)
 101     Swap k -> swap (trans k)
 102 instance Stackable repr => Stackable (SomeInstr repr) where
 103   push _v (Instr (Pop i)) = i
 104   push v i = SomeInstr (Push v i)
 105   pop = SomeInstr . Pop
 106   liftI2 f = SomeInstr . LiftI2 f
 107   swap = SomeInstr . Swap
 108
 109 -- Routinable
 110 data instance Instr Routinable repr inp vs fs a where
 111   -- | @('Subroutine' n v k)@ binds the 'LetName' @(n)@ to the 'Instr'uction's @(v)@,
 112   -- 'Call's @(n)@ and
 113   -- continues with the next 'Instr'uction @(k)@.
 114   Subroutine ::
 115     LetName v -> 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 -> SomeInstr repr inp (v ': vs) es a ->
 217     SomeInstr repr inp vs es a ->
 218     Instr Joinable repr inp vs es a
 219   RefJoin ::
 220     LetName v ->
 221     Instr Joinable repr inp (v ': vs) es a
 222 instance Joinable repr => Trans (Instr Joinable repr inp vs es) (repr inp vs es) where
 223   trans = \case
 224     DefJoin n sub k -> defJoin n (trans sub) (trans k)
 225     RefJoin n -> refJoin n
 226 instance Joinable repr => Joinable (SomeInstr repr) where
 227   defJoin n sub = SomeInstr . DefJoin n sub
 228   refJoin = SomeInstr . RefJoin
 229
 230 -- Readable
 231 data instance Instr (Readable tok) repr inp vs fs a where
 232   -- | @('Read' expected p k)@ reads a 'Char' @(c)@ from the 'inp'ut,
 233   -- if @(p c)@ is 'True' then continues with the next 'Instr'uction @(k)@ on,
 234   -- otherwise 'Fail'.
 235   Read ::
 236     [ErrorItem (InputToken inp)] ->
 237     TermInstr (InputToken inp -> Bool) ->
 238     SomeInstr repr inp (InputToken inp ': vs) ('Succ es) a ->
 239     Instr (Readable tok) repr inp vs ('Succ es) a
 240 instance
 241   ( Readable tok repr, tok ~ InputToken inp ) =>
 242   Trans (Instr (Readable tok) repr inp vs es) (repr inp vs es) where
 243   trans = \case
 244     Read es p k -> read es p (trans k)
 245 instance
 246   ( Readable tok repr, Typeable tok ) =>
 247   Readable tok (SomeInstr repr) where
 248   read es p = SomeInstr . Read es p