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