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