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