src/Symantic/Parser/Machine/Optimize.hs

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