src/Symantic/Parser/Grammar/Optimize.hs

   1 {-# LANGUAGE PatternSynonyms #-} -- For Comb
   2 {-# LANGUAGE TemplateHaskell #-} -- For branch
   3 {-# LANGUAGE ViewPatterns #-} -- For unSomeComb
   4 {-# OPTIONS_GHC -fno-warn-orphans #-} -- For MakeLetName TH.Name
   5 -- | Bottom-up optimization of 'Comb'inators,
   6 -- reexamining downward as needed after each optimization.
   7 module Symantic.Parser.Grammar.Optimize where
   8
   9 import Data.Bool (Bool(..))
  10 import Data.Either (Either(..), either)
  11 import Data.Eq (Eq(..))
  12 import Data.Function (($), (.))
  13 import Data.Kind (Constraint)
  14 import Data.Maybe (Maybe(..))
  15 import Data.Set (Set)
  16 import Data.Functor.Identity (Identity(..))
  17 import Data.Functor.Product (Product(..))
  18 import Type.Reflection (Typeable, typeRep, eqTypeRep, (:~~:)(..))
  19 import qualified Data.Foldable as Foldable
  20 import qualified Data.Functor as Functor
  21 import qualified Data.List as List
  22
  23 import Symantic.Parser.Grammar.Combinators
  24 import Symantic.Parser.Grammar.Production
  25 import Symantic.Derive
  26 import Symantic.ObserveSharing
  27 import qualified Symantic.Data as Prod
  28 import qualified Symantic.Lang as Prod
  29
  30 {-
  31 import Data.Function (($), flip)
  32 import Debug.Trace (trace)
  33
  34 (&) = flip ($)
  35 infix 0 &
  36 -}
  37
  38 -- * Type 'OptimizeGrammar'
  39 type OptimizeGrammar = SomeComb
  40
  41 optimizeGrammar ::
  42   Derivable (SomeComb repr) =>
  43   SomeComb repr a -> repr a
  44 optimizeGrammar = derive
  45
  46 -- * Data family 'Comb'
  47 -- | 'Comb'inators of the 'Grammar'.
  48 -- This is an extensible data-type.
  49 data family Comb
  50   (comb :: ReprComb -> Constraint)
  51   :: ReprComb -> ReprComb
  52 type instance Derived (Comb comb repr) = repr
  53
  54 -- | Convenient utility to pattern-match a 'SomeComb'.
  55 pattern Comb :: Typeable comb => Comb comb repr a -> SomeComb repr a
  56 pattern Comb x <- (unSomeComb -> Just x)
  57
  58 -- ** Type 'SomeComb'
  59 -- | Some 'Comb'inator existentialized over the actual combinator symantic class.
  60 -- Useful to handle a list of 'Comb'inators
  61 -- without requiring impredicative quantification.
  62 -- Must be used by pattern-matching
  63 -- on the 'SomeComb' data-constructor,
  64 -- to bring the constraints in scope.
  65 --
  66 -- The optimizations are directly applied within it,
  67 -- to avoid introducing an extra newtype,
  68 -- this also give a more understandable code.
  69 data SomeComb repr a =
  70   forall comb.
  71   (Derivable (Comb comb repr), Typeable comb) =>
  72   SomeComb (Comb comb repr a)
  73
  74 type instance Derived (SomeComb repr) = repr
  75 instance Derivable (SomeComb repr) where
  76   derive (SomeComb x) = derive x
  77
  78 -- | @(unSomeComb c :: 'Maybe' ('Comb' comb repr a))@
  79 -- extract the data-constructor from the given 'SomeComb'
  80 -- iif. it belongs to the @('Comb' comb repr a)@ data-instance.
  81 unSomeComb ::
  82   forall comb repr a.
  83   Typeable comb =>
  84   SomeComb repr a -> Maybe (Comb comb repr a)
  85 unSomeComb (SomeComb (c::Comb c repr a)) =
  86   case typeRep @comb `eqTypeRep` typeRep @c of
  87     Just HRefl -> Just c
  88     Nothing -> Nothing
  89
  90 -- CombAlternable
  91 data instance Comb CombAlternable repr a where
  92   Alt :: Exception -> SomeComb repr a -> SomeComb repr a -> Comb CombAlternable repr a
  93   Empty :: Comb CombAlternable repr a
  94   Failure :: SomeFailure -> Comb CombAlternable repr a
  95   Throw :: ExceptionLabel -> Comb CombAlternable repr a
  96   Try :: SomeComb repr a -> Comb CombAlternable repr a
  97 instance CombAlternable repr => Derivable (Comb CombAlternable repr) where
  98   derive = \case
  99     Alt exn x y -> alt exn (derive x) (derive y)
 100     Empty -> empty
 101     Failure sf -> failure sf
 102     Throw exn -> throw exn
 103     Try x -> try (derive x)
 104 instance
 105   ( CombAlternable repr
 106   , CombApplicable repr
 107   , CombLookable repr
 108   , CombMatchable repr
 109   , CombSelectable repr
 110   ) => CombAlternable (SomeComb repr) where
 111   empty = SomeComb Empty
 112   failure sf = SomeComb (Failure sf)
 113
 114   alt _exn p@(Comb Pure{}) _ = p
 115     -- & trace "Left Catch Law"
 116   alt _exn (Comb Empty) u = u
 117     -- & trace "Left Neutral Law"
 118   alt _exn u (Comb Empty) = u
 119     -- & trace "Right Neutral Law"
 120   alt exn (Comb (Alt exn' u v)) w | exn' == exn = u <|> (v <|> w)
 121     -- See Lemma 1 (Associativity of choice for labeled PEGs)
 122     -- in https://doi.org/10.1145/2851613.2851750
 123     -- & trace "Associativity Law"
 124   alt exn (Comb (Look p)) (Comb (Look q)) = look (alt exn (try p) q)
 125     -- & trace "Distributivity Law"
 126   alt exn x y = SomeComb (Alt exn x y)
 127
 128   throw exn = SomeComb (Throw exn)
 129
 130   try (Comb (p :$>: x)) = try p $> x
 131     -- & trace "Try Interchange Law"
 132   try (Comb (f :<$>: p)) = f <$> try p
 133     -- & trace "Try Interchange Law"
 134   try x = SomeComb (Try x)
 135
 136 -- CombApplicable
 137 data instance Comb CombApplicable repr a where
 138   Pure :: Production a -> Comb CombApplicable repr a
 139   (:<*>:) :: SomeComb repr (a -> b) -> SomeComb repr a -> Comb CombApplicable repr b
 140   (:<*:) :: SomeComb repr a -> SomeComb repr b -> Comb CombApplicable repr a
 141   (:*>:) :: SomeComb repr a -> SomeComb repr b -> Comb CombApplicable repr b
 142 infixl 4 :<*>:, :<*:, :*>:
 143 pattern (:<$>:) :: Production (a -> b) -> SomeComb repr a -> Comb CombApplicable repr b
 144 pattern t :<$>: x <- Comb (Pure t) :<*>: x
 145 pattern (:$>:) :: SomeComb repr a -> Production b -> Comb CombApplicable repr b
 146 pattern x :$>: t <- x :*>: Comb (Pure t)
 147 instance CombApplicable repr => Derivable (Comb CombApplicable repr) where
 148   derive = \case
 149     Pure x -> pure (optimizeProduction x)
 150     f :<*>: x -> derive f <*> derive x
 151     x :<*: y -> derive x <* derive y
 152     x :*>: y -> derive x *> derive y
 153 instance
 154   ( CombApplicable repr
 155   , CombAlternable repr
 156   , CombLookable repr
 157   , CombMatchable repr
 158   , CombSelectable repr
 159   ) => CombApplicable (SomeComb repr) where
 160   pure = SomeComb . Pure
 161   f <$> Comb (Branch b l r) =
 162     branch b
 163       ((Prod..) Prod..@ f <$> l)
 164       ((Prod..) Prod..@ f <$> r)
 165     -- & trace "Branch Distributivity Law"
 166   f <$> Comb (Conditional a ps bs d) =
 167     conditional a ps
 168       ((f <$>) Functor.<$> bs)
 169       (f <$> d)
 170     -- & trace "Conditional Distributivity Law"
 171   -- Being careful here to use (<*>),
 172   -- instead of SomeComb (f <$> unOptComb x),
 173   -- in order to apply the optimizations of (<*>).
 174   f <$> x = pure f <*> x
 175
 176   x <$ u = u $> x
 177     -- & trace "Commutativity Law"
 178
 179   Comb Empty <*> _ = empty
 180     -- & trace "App Right Absorption Law"
 181   u <*> Comb Empty = u *> empty
 182     -- & trace "App Failure Weakening Law"
 183   Comb (Pure f) <*> Comb (Pure x) = pure (f Prod..@ x)
 184     -- & trace "Homomorphism Law"
 185   {-
 186   Comb (Pure f) <*> Comb (g :<$>: p) =
 187     -- This is basically a shortcut,
 188     -- it can be caught by one Composition Law
 189     -- and two Homomorphism Law.
 190     (Prod..) Prod..@ f Prod..@ g <$> p
 191     -- & trace "Functor Composition Law"
 192   -}
 193   u <*> Comb (Pure x) = Prod.flip Prod..@ (Prod.$) Prod..@ x <$> u
 194     -- & trace "Interchange Law"
 195   u <*> Comb (v :<*>: w) = (((Prod..) <$> u) <*> v) <*> w
 196     -- & trace "Composition Law"
 197   Comb (u :*>: v) <*> w = u *> (v <*> w)
 198     -- & trace "Reassociation Law 1"
 199   u <*> Comb (v :<*: w) = (u <*> v) <* w
 200     -- & trace "Reassociation Law 2"
 201   u <*> Comb (v :$>: x) = (u <*> pure x) <* v
 202     -- & trace "Reassociation Law 3"
 203   p <*> Comb (NegLook q) =
 204     (p <*> pure Prod.unit) <* negLook q
 205     -- & trace "Absorption Law"
 206   x <*> y = SomeComb (x :<*>: y)
 207
 208   Comb Empty *> _ = empty
 209     -- & trace "App Right Absorption Law"
 210   Comb (_ :<$>: p) *> q = p *> q
 211     -- & trace "Right Absorption Law"
 212   Comb Pure{} *> u = u
 213     -- & trace "Identity Law"
 214   Comb (u :$>: _) *> v = u *> v
 215     -- & trace "Identity Law"
 216   u *> Comb (v :*>: w) = (u *> v) *> w
 217     -- & trace "Associativity Law"
 218   x *> y = SomeComb (x :*>: y)
 219
 220   Comb Empty <* _ = empty
 221     -- & trace "App Right Absorption Law"
 222   u <* Comb Empty = u *> empty
 223     -- & trace "App Failure Weakening Law"
 224   p <* Comb (_ :<$>: q) = p <* q
 225     -- & trace "Left Absorption Law"
 226   u <* Comb Pure{} = u
 227     -- & trace "Identity Law"
 228   u <* Comb (v :$>: _) = u <* v
 229     -- & trace "Identity Law"
 230   Comb (u :<*: v) <* w = u <* (v <* w)
 231     -- & trace "Associativity Law"
 232   x <* y = SomeComb (x :<*: y)
 233
 234 -- CombFoldable
 235 data instance Comb CombFoldable repr a where
 236   ChainPreC :: SomeComb repr (a -> a) -> SomeComb repr a -> Comb CombFoldable repr a
 237   ChainPostC :: SomeComb repr a -> SomeComb repr (a -> a) -> Comb CombFoldable repr a
 238 instance CombFoldable repr => Derivable (Comb CombFoldable repr) where
 239   derive = \case
 240     ChainPreC x y -> chainPre (derive x) (derive y)
 241     ChainPostC x y -> chainPost (derive x) (derive y)
 242 instance CombFoldable repr => CombFoldable (SomeComb repr) where
 243   chainPre x = SomeComb . ChainPreC x
 244   chainPost x = SomeComb . ChainPostC x
 245
 246 -- Letable
 247 data instance Comb (Letable letName) repr a where
 248   Shareable :: letName -> SomeComb repr a -> Comb (Letable letName) repr a
 249   Ref :: Bool -> letName -> Comb (Letable letName) repr a
 250 instance
 251   Letable letName repr =>
 252   Derivable (Comb (Letable letName) repr) where
 253   derive = \case
 254     Shareable n x -> shareable n (derive x)
 255     Ref isRec n -> ref isRec n
 256 instance
 257   (Letable letName repr, Typeable letName) =>
 258   Letable letName (SomeComb repr) where
 259   shareable n = SomeComb . Shareable n
 260   ref isRec = SomeComb . Ref isRec
 261
 262 -- Letsable
 263 data instance Comb (Letsable letName) repr a where
 264   Lets :: LetBindings letName (SomeComb repr) ->
 265           SomeComb repr a -> Comb (Letsable letName) repr a
 266 instance
 267   Letsable letName repr =>
 268   Derivable (Comb (Letsable letName) repr) where
 269   derive = \case
 270     Lets defs x -> lets ((\(SomeLet sub) -> SomeLet (derive sub)) Functor.<$> defs) (derive x)
 271 instance
 272   (Letsable letName repr, Typeable letName) =>
 273   Letsable letName (SomeComb repr) where
 274   lets defs = SomeComb . Lets defs
 275
 276 -- CombLookable
 277 data instance Comb CombLookable repr a where
 278   Look :: SomeComb repr a -> Comb CombLookable repr a
 279   NegLook :: SomeComb repr a -> Comb CombLookable repr ()
 280   Eof :: Comb CombLookable repr ()
 281 instance CombLookable repr => Derivable (Comb CombLookable repr) where
 282   derive = \case
 283     Look x -> look (derive x)
 284     NegLook x -> negLook (derive x)
 285     Eof -> eof
 286 instance
 287   ( CombAlternable repr
 288   , CombApplicable repr
 289   , CombLookable repr
 290   , CombSelectable repr
 291   , CombMatchable repr
 292   ) => CombLookable (SomeComb repr) where
 293   look p@(Comb Pure{}) = p
 294     -- & trace "Pure Look Law"
 295   look p@(Comb Empty) = p
 296     -- & trace "Dead Look Law"
 297   look (Comb (Look x)) = look x
 298     -- & trace "Idempotence Law"
 299   look (Comb (NegLook x)) = negLook x
 300     -- & trace "Left Identity Law"
 301   look (Comb (p :$>: x)) = look p $> x
 302     -- & trace "Interchange Law"
 303   look (Comb (f :<$>: p)) = f <$> look p
 304     -- & trace "Interchange Law"
 305   look x = SomeComb (Look x)
 306
 307   negLook (Comb Pure{}) = empty
 308     -- & trace "Pure Negative-Look"
 309   negLook (Comb Empty) = pure Prod.unit
 310     -- & trace "Dead Negative-Look"
 311   negLook (Comb (NegLook x)) = look (try x *> pure Prod.unit)
 312     -- & trace "Double Negation Law"
 313   negLook (Comb (Try x)) = negLook x
 314     -- & trace "Zero Consumption Law"
 315   negLook (Comb (Look x)) = negLook x
 316     -- & trace "Right Identity Law"
 317   negLook (Comb (Alt _exn (Comb (Try p)) q)) = negLook p *> negLook q
 318     -- FIXME: see if this really holds for all exceptions.
 319     -- & trace "Transparency Law"
 320   negLook (Comb (p :$>: _)) = negLook p
 321     -- & trace "NegLook Idempotence Law"
 322   negLook x = SomeComb (NegLook x)
 323
 324   eof = SomeComb Eof
 325
 326 -- CombMatchable
 327 data instance Comb CombMatchable repr a where
 328   Conditional :: Eq a =>
 329     SomeComb repr a ->
 330     [Production (a -> Bool)] ->
 331     [SomeComb repr b] ->
 332     SomeComb repr b ->
 333     Comb CombMatchable repr b
 334 instance CombMatchable repr => Derivable (Comb CombMatchable repr) where
 335   derive = \case
 336     Conditional a ps bs b ->
 337       conditional (derive a)
 338         (optimizeProduction Functor.<$> ps)
 339         (derive Functor.<$> bs) (derive b)
 340 instance
 341   ( CombApplicable repr
 342   , CombAlternable repr
 343   , CombLookable repr
 344   , CombSelectable repr
 345   , CombMatchable repr
 346   ) => CombMatchable (SomeComb repr) where
 347   conditional (Comb Empty) _ _ d = d
 348     -- & trace "Conditional Absorption Law"
 349   conditional p _ qs (Comb Empty)
 350     | Foldable.all (\case { Comb Empty -> True; _ -> False }) qs = p *> empty
 351       -- & trace "Conditional Weakening Law"
 352   conditional a _ps bs (Comb Empty)
 353     | Foldable.all (\case { Comb Empty -> True; _ -> False }) bs = a *> empty
 354       -- & trace "Conditional Weakening Law"
 355   conditional (Comb (Pure a)) ps bs d =
 356     Foldable.foldr (\(p, b) next ->
 357       if runValue (p Prod..@ a) then b else next
 358     ) d (List.zip ps bs)
 359     -- & trace "Conditional Pure Law"
 360   conditional a ps bs d = SomeComb (Conditional a ps bs d)
 361
 362 -- CombSatisfiable
 363 data instance Comb (CombSatisfiable tok) repr a where
 364   -- | To include the @('Set' 'SomeFailure')@ is a little kludge
 365   -- it would be cleaner to be able to pattern-match
 366   -- on @(alt exn (Comb 'Satisfy'{}) (Failure{}))@
 367   -- when generating 'Program', but this is not easily possible then
 368   -- because data types have already been converted back to class methods,
 369   -- hence pattern-matching is no longer possible
 370   -- (at least not without reintroducing data types).
 371   SatisfyOrFail ::
 372     CombSatisfiable tok repr =>
 373     Set SomeFailure ->
 374     Production (tok -> Bool) ->
 375     Comb (CombSatisfiable tok) repr tok
 376 instance
 377   CombSatisfiable tok repr =>
 378   Derivable (Comb (CombSatisfiable tok) repr) where
 379   derive = \case
 380     SatisfyOrFail fs p -> satisfyOrFail fs (optimizeProduction p)
 381 instance
 382   (CombSatisfiable tok repr, Typeable tok) =>
 383   CombSatisfiable tok (SomeComb repr) where
 384   satisfyOrFail fs = SomeComb . SatisfyOrFail fs
 385
 386 -- CombSelectable
 387 data instance Comb CombSelectable repr a where
 388   Branch ::
 389     SomeComb repr (Either a b) ->
 390     SomeComb repr (a -> c) ->
 391     SomeComb repr (b -> c) ->
 392     Comb CombSelectable repr c
 393 instance CombSelectable repr => Derivable (Comb CombSelectable repr) where
 394   derive = \case
 395     Branch lr l r -> branch (derive lr) (derive l) (derive r)
 396 instance
 397   ( CombApplicable repr
 398   , CombAlternable repr
 399   , CombLookable repr
 400   , CombSelectable repr
 401   , CombMatchable repr
 402   ) => CombSelectable (SomeComb repr) where
 403   branch (Comb Empty) _ _ = empty
 404     -- & trace "Branch Absorption Law"
 405   branch b (Comb Empty) (Comb Empty) = b *> empty
 406     -- & trace "Branch Weakening Law"
 407   branch (Comb (Pure lr)) l r =
 408     case runValue lr of
 409       Left value -> l <*> pure (Pair v c)
 410         where
 411         v = Prod.SomeData $ Prod.Var $ Identity value
 412         c = Prod.SomeData $ Prod.Var
 413           [|| case $$(runCode lr) of Left x -> x ||]
 414       Right value -> r <*> pure (Pair v c)
 415         where
 416         v = Prod.SomeData $ Prod.Var $ Identity value
 417         c = Prod.SomeData $ Prod.Var
 418           [|| case $$(runCode lr) of Right x -> x ||]
 419     -- & trace "Branch Pure Either Law"
 420   branch b (Comb (Pure l)) (Comb (Pure r)) =
 421     Pair v c <$> b
 422     -- & trace "Branch Generalised Identity Law"
 423     where
 424     v = Prod.SomeData $ Prod.Var $ Identity $ either (runValue l) (runValue r)
 425     c = Prod.SomeData $ Prod.Var [|| either $$(runCode l) $$(runCode r) ||]
 426   branch (Comb (x :*>: y)) p q = x *> branch y p q
 427     -- & trace "Interchange Law"
 428   branch b l (Comb Empty) =
 429     branch (pure (Pair v c) <*> b) empty l
 430     -- & trace "Negated Branch Law"
 431     where
 432     v = Prod.SomeData $ Prod.Var $ Identity $ either Right Left
 433     c = Prod.SomeData $ Prod.Var $ [||either Right Left||]
 434   branch (Comb (Branch b (Comb Empty) (Comb (Pure lr)))) (Comb Empty) br =
 435     branch (pure (Pair v c) <*> b) empty br
 436     -- & trace "Branch Fusion Law"
 437     where
 438     v = Prod.SomeData $ Prod.Var $ Identity $ \case
 439       Left{} -> Left ()
 440       Right r ->
 441         case runValue lr r of
 442           Left{} -> Left ()
 443           Right rr -> Right rr
 444     c = Prod.SomeData $ Prod.Var
 445       [|| \case Left{} -> Left ()
 446                 Right r -> case $$(runCode lr) r of
 447                              Left{} -> Left ()
 448                              Right rr -> Right rr ||]
 449   branch b l r = SomeComb (Branch b l r)