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