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