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