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