src/Symantic/Parser/Grammar/Optimize.hs

   1 {-# LANGUAGE PatternSynonyms #-} -- For aliased combinators
   2 {-# LANGUAGE TemplateHaskell #-} -- For optimizeCombNode
   3 {-# LANGUAGE ViewPatterns #-} -- For optimizeCombNode
   4 {-# OPTIONS_GHC -fno-warn-orphans #-} -- For MakeLetName TH.Name
   5 module Symantic.Parser.Grammar.Optimize where
   6
   7 import Data.Bool (Bool(..))
   8 import Data.Either (Either(..), either)
   9 import Data.Eq (Eq(..))
  10 import Data.Foldable (all, foldr)
  11 import Data.Function ((.))
  12 import Data.Kind (Type)
  13 import qualified Data.Functor as Functor
  14 import qualified Data.List as List
  15 import qualified Language.Haskell.TH.Syntax as TH
  16
  17 import Symantic.Parser.Grammar.Combinators as Comb
  18 import Symantic.Parser.Grammar.Pure (ValueCode(..), Value(..), getValue, getCode)
  19 import Symantic.Univariant.Letable
  20 import Symantic.Univariant.Trans
  21 import qualified Symantic.Parser.Grammar.Pure as H
  22
  23 -- import Debug.Trace (trace)
  24
  25 -- * Type 'Comb'
  26 -- | Pattern-matchable 'Comb'inators of the grammar.
  27 -- @(repr)@ is not strictly necessary since it's only a phantom type
  28 -- (no constructor use it as a value), but having it:
  29 --
  30 -- 1. emphasizes that those 'Comb'inators will be 'trans'formed again
  31 --    (eg. in 'DumpComb' or 'Instr'uctions).
  32 --
  33 -- 2. Avoid overlapping instances between
  34 --    @('Trans' ('Comb' repr) repr)@ and
  35 --    @('Trans' ('Comb' repr) ('OptimizeComb' letName repr))@
  36 data Comb (repr :: Type -> Type) a where
  37   Pure :: H.CombPure a -> Comb repr a
  38   Satisfy ::
  39     Satisfiable repr tok =>
  40     [ErrorItem tok] ->
  41     H.CombPure (tok -> Bool) -> Comb repr tok
  42   Item :: Satisfiable repr tok => Comb repr tok
  43   Try :: Comb repr a -> Comb repr a
  44   Look :: Comb repr a -> Comb repr a
  45   NegLook :: Comb repr a -> Comb repr ()
  46   Eof :: Comb repr ()
  47   (:<*>) :: Comb repr (a -> b) -> Comb repr a -> Comb repr b
  48   (:<|>) :: Comb repr a -> Comb repr a -> Comb repr a
  49   Empty :: Comb repr a
  50   Branch ::
  51     Comb repr (Either a b) ->
  52     Comb repr (a -> c) -> Comb repr (b -> c) -> Comb repr c
  53   Match :: Eq a =>
  54     [H.CombPure (a -> Bool)] ->
  55     [Comb repr b] -> Comb repr a -> Comb repr b -> Comb repr b
  56   ChainPre :: Comb repr (a -> a) -> Comb repr a -> Comb repr a
  57   ChainPost :: Comb repr a -> Comb repr (a -> a) -> Comb repr a
  58   Def :: TH.Name -> Comb repr a -> Comb repr a
  59   Ref :: Bool -> TH.Name -> Comb repr a
  60
  61 pattern (:<$>) :: H.CombPure (a -> b) -> Comb repr a -> Comb repr b
  62 pattern (:$>) :: Comb repr a -> H.CombPure b -> Comb repr b
  63 pattern (:<$) :: H.CombPure a -> Comb repr b -> Comb repr a
  64 pattern (:*>) :: Comb repr a -> Comb repr b -> Comb repr b
  65 pattern (:<*) :: Comb repr a -> Comb repr b -> Comb repr a
  66 pattern x :<$> p = Pure x :<*> p
  67 pattern p :$> x = p :*> Pure x
  68 pattern x :<$ p = Pure x :<* p
  69 pattern x :<* p = H.Const :<$> x :<*> p
  70 pattern p :*> x = H.Id :<$ p :<*> x
  71
  72 infixl 3 :<|>
  73 infixl 4 :<*>, :<*, :*>
  74 infixl 4 :<$>, :<$, :$>
  75
  76 instance Applicable (Comb repr) where
  77   pure = Pure
  78   (<*>) = (:<*>)
  79 instance Alternable (Comb repr) where
  80   (<|>) = (:<|>)
  81   empty = Empty
  82   try = Try
  83 instance Selectable (Comb repr) where
  84   branch = Branch
  85 instance Matchable (Comb repr) where
  86   conditional = Match
  87 instance Foldable (Comb repr) where
  88   chainPre = ChainPre
  89   chainPost = ChainPost
  90 instance Satisfiable repr tok => Satisfiable (Comb repr) tok where
  91   satisfy = Satisfy
  92 instance Lookable (Comb repr) where
  93   look = Look
  94   negLook = NegLook
  95   eof = Eof
  96 instance Letable TH.Name (Comb repr) where
  97   def = Def
  98   ref = Ref
  99 instance MakeLetName TH.Name where
 100   makeLetName _ = TH.qNewName "name"
 101
 102 -- Pattern-matchable 'Comb'inators keep enough structure
 103 -- to have some of the symantics producing them interpreted again
 104 -- (eg. after being modified by 'optimizeComb').
 105 type instance Output (Comb repr) = repr
 106 instance
 107   ( Applicable repr
 108   , Alternable repr
 109   , Selectable repr
 110   , Foldable repr
 111   , Lookable repr
 112   , Matchable repr
 113   , Letable TH.Name repr
 114   ) => Trans (Comb repr) repr where
 115   trans = \case
 116     Pure a -> pure a
 117     Satisfy es p -> satisfy es p
 118     Item -> item
 119     Try x -> try (trans x)
 120     Look x -> look (trans x)
 121     NegLook x -> negLook (trans x)
 122     Eof -> eof
 123     x :<*> y -> trans x <*> trans y
 124     x :<|> y -> trans x <|> trans y
 125     Empty -> empty
 126     Branch lr l r -> branch (trans lr) (trans l) (trans r)
 127     Match ps bs a b -> conditional ps (trans Functor.<$> bs) (trans a) (trans b)
 128     ChainPre x y -> chainPre (trans x) (trans y)
 129     ChainPost x y -> chainPost (trans x) (trans y)
 130     Def n x -> def n (trans x)
 131     Ref r n -> ref r n
 132
 133 -- * Type 'OptimizeComb'
 134 -- Bottom-up application of 'optimizeCombNode'.
 135 newtype OptimizeComb letName repr a =
 136         OptimizeComb { unOptimizeComb :: Comb repr a }
 137
 138 optimizeComb ::
 139   Trans (OptimizeComb TH.Name repr) repr =>
 140   OptimizeComb TH.Name repr a -> repr a
 141 optimizeComb = trans
 142 instance
 143   Trans (Comb repr) repr =>
 144   Trans (OptimizeComb letName repr) repr where
 145   trans = trans . unOptimizeComb
 146
 147 type instance Output (OptimizeComb _letName repr) = Comb repr
 148 instance Trans (OptimizeComb letName repr) (Comb repr) where
 149   trans = unOptimizeComb
 150 instance Trans (Comb repr) (OptimizeComb letName repr) where
 151   trans = OptimizeComb . optimizeCombNode
 152 instance Trans1 (Comb repr) (OptimizeComb letName repr)
 153 instance Trans2 (Comb repr) (OptimizeComb letName repr)
 154 instance Trans3 (Comb repr) (OptimizeComb letName repr)
 155
 156 instance
 157   Letable letName (Comb repr) =>
 158   Letable letName (OptimizeComb letName repr) where
 159   -- Disable useless calls to 'optimizeCombNode'
 160   -- because 'Def' or 'Ref' have no matching in it.
 161   def n = OptimizeComb . def n . unOptimizeComb
 162   ref r n = OptimizeComb (ref r n)
 163 instance Comb.Applicable (OptimizeComb letName repr)
 164 instance Comb.Alternable (OptimizeComb letName repr)
 165 instance Comb.Satisfiable repr tok =>
 166          Comb.Satisfiable (OptimizeComb letName repr) tok
 167 instance Comb.Selectable (OptimizeComb letName repr)
 168 instance Comb.Matchable (OptimizeComb letName repr)
 169 instance Comb.Lookable (OptimizeComb letName repr)
 170 instance Comb.Foldable (OptimizeComb letName repr)
 171
 172 optimizeCombNode :: Comb repr a -> Comb repr a
 173 optimizeCombNode = \case
 174   -- Functor Identity Law
 175   H.Id :<$> x ->
 176     -- trace "Functor Identity Law" $
 177     x
 178   -- Functor Commutativity Law
 179   x :<$ u ->
 180     -- trace "Functor Commutativity Law" $
 181     optimizeCombNode (u :$> x)
 182   -- Functor Flip Const Law
 183   H.Flip H.:@ H.Const :<$> u ->
 184     -- trace "Functor Flip Const Law" $
 185     optimizeCombNode (u :*> Pure H.Id)
 186   -- Functor Homomorphism Law
 187   f :<$> Pure x ->
 188     -- trace "Functor Homomorphism Law" $
 189     Pure (f H..@ x)
 190
 191   -- App Right Absorption Law
 192   Empty :<*> _ ->
 193     -- trace "App Right Absorption Law" $
 194     Empty
 195   -- App Left Absorption Law
 196   _ :<*> Empty ->
 197     -- In Parsley: this is only a weakening to u :*> Empty
 198     -- but here :*> is an alias to :<*>
 199     -- hence it would loop on itself forever.
 200     -- trace "App Left Absorption Law" $
 201     Empty
 202   -- App Composition Law
 203   u :<*> (v :<*> w) ->
 204     -- trace "App Composition Law" $
 205     optimizeCombNode (optimizeCombNode (optimizeCombNode ((H.:.) :<$> u) :<*> v) :<*> w)
 206   -- App Interchange Law
 207   u :<*> Pure x ->
 208     -- trace "App Interchange Law" $
 209     optimizeCombNode (H.Flip H..@ (H.:$) H..@ x :<$> u)
 210   -- App Left Absorption Law
 211   p :<* (_ :<$> q) ->
 212     -- trace "App Left Absorption Law" $
 213     p :<* q
 214   -- App Right Absorption Law
 215   (_ :<$> p) :*> q ->
 216     -- trace "App Right Absorption Law" $
 217     p :*> q
 218   -- App Pure Left Identity Law
 219   Pure _ :*> u ->
 220     -- trace "App Pure Left Identity Law" $
 221     u
 222   -- App Functor Left Identity Law
 223   (u :$> _) :*> v ->
 224     -- trace "App Functor Left Identity Law" $
 225     u :*> v
 226   -- App Pure Right Identity Law
 227   u :<* Pure _ ->
 228     -- trace "App Pure Right Identity Law" $
 229     u
 230   -- App Functor Right Identity Law
 231   u :<* (v :$> _) ->
 232     -- trace "App Functor Right Identity Law" $
 233     optimizeCombNode (u :<* v)
 234   -- App Left Associativity Law
 235   (u :<* v) :<* w ->
 236     -- trace "App Left Associativity Law" $
 237     optimizeCombNode (u :<* optimizeCombNode (v :<* w))
 238
 239   -- Alt Left CatchFail Law
 240   p@Pure{} :<|> _ ->
 241     -- trace "Alt Left CatchFail Law" $
 242     p
 243   -- Alt Left Neutral Law
 244   Empty :<|> u ->
 245     -- trace "Alt Left Neutral Law" $
 246     u
 247   -- All Right Neutral Law
 248   u :<|> Empty ->
 249     -- trace "Alt Right Neutral Law" $
 250     u
 251   -- Alt Associativity Law
 252   (u :<|> v) :<|> w ->
 253     -- trace "Alt Associativity Law" $
 254     u :<|> optimizeCombNode (v :<|> w)
 255
 256   -- Look Pure Law
 257   Look p@Pure{} ->
 258     -- trace "Look Pure Law" $
 259     p
 260   -- Look Empty Law
 261   Look p@Empty ->
 262     -- trace "Look Empty Law" $
 263     p
 264   -- NegLook Pure Law
 265   NegLook Pure{} ->
 266     -- trace "NegLook Pure Law" $
 267     Empty
 268   -- NegLook Empty Law
 269   NegLook Empty ->
 270     -- trace "NegLook Dead Law" $
 271     Pure H.unit
 272   -- NegLook Double Negation Law
 273   NegLook (NegLook p) ->
 274     -- trace "NegLook Double Negation Law" $
 275     optimizeCombNode (Look (Try p) :*> Pure H.unit)
 276   -- NegLook Zero Consumption Law
 277   NegLook (Try p) ->
 278     -- trace "NegLook Zero Consumption Law" $
 279     optimizeCombNode (NegLook p)
 280   -- Idempotence Law
 281   Look (Look p) ->
 282     -- trace "Look Idempotence Law" $
 283     Look p
 284   -- Look Right Identity Law
 285   NegLook (Look p) ->
 286     -- trace "Look Right Identity Law" $
 287     optimizeCombNode (NegLook p)
 288   -- Look Left Identity Law
 289   Look (NegLook p) ->
 290     -- trace "Look Left Identity Law" $
 291     NegLook p
 292   -- NegLook Transparency Law
 293   NegLook (Try p :<|> q) ->
 294     -- trace "NegLook Transparency Law" $
 295     optimizeCombNode (optimizeCombNode (NegLook p) :*> optimizeCombNode (NegLook q))
 296   -- Look Distributivity Law
 297   Look p :<|> Look q ->
 298     -- trace "Look Distributivity Law" $
 299     optimizeCombNode (Look (optimizeCombNode (Try p :<|> q)))
 300   -- Look Interchange Law
 301   Look (f :<$> p) ->
 302     -- trace "Look Interchange Law" $
 303     optimizeCombNode (f :<$> optimizeCombNode (Look p))
 304   -- NegLook Idempotence Right Law
 305   NegLook (_ :<$> p) ->
 306     -- trace "NegLook Idempotence Law" $
 307     optimizeCombNode (NegLook p)
 308   -- Try Interchange Law
 309   Try (f :<$> p) ->
 310     -- trace "Try Interchange Law" $
 311     optimizeCombNode (f :<$> optimizeCombNode (Try p))
 312
 313   -- Branch Absorption Law
 314   Branch Empty _ _ ->
 315     -- trace "Branch Absorption Law" $
 316     empty
 317   -- Branch Weakening Law
 318   Branch b Empty Empty ->
 319     -- trace "Branch Weakening Law" $
 320     optimizeCombNode (b :*> Empty)
 321   -- Branch Pure Left/Right Laws
 322   Branch (Pure (trans -> lr)) l r ->
 323     -- trace "Branch Pure Left/Right Law" $
 324     case getValue lr of
 325       Left v -> optimizeCombNode (l :<*> Pure (H.CombPure (ValueCode (Value v) c)))
 326         where c = [|| case $$(getCode lr) of Left x -> x ||]
 327       Right v -> optimizeCombNode (r :<*> Pure (H.CombPure (ValueCode (Value v) c)))
 328         where c = [|| case $$(getCode lr) of Right x -> x ||]
 329   -- Branch Generalised Identity Law
 330   Branch b (Pure (trans -> l)) (Pure (trans -> r)) ->
 331     -- trace "Branch Generalised Identity Law" $
 332     optimizeCombNode (H.CombPure (ValueCode v c) :<$> b)
 333     where
 334     v = Value (either (getValue l) (getValue r))
 335     c = [|| either $$(getCode l) $$(getCode r) ||]
 336   -- Branch Interchange Law
 337   Branch (x :*> y) p q ->
 338     -- trace "Branch Interchange Law" $
 339     optimizeCombNode (x :*> optimizeCombNode (Branch y p q))
 340   -- Branch Empty Right Law
 341   Branch b l Empty ->
 342     -- trace " Branch Empty Right Law" $
 343     Branch (Pure (H.CombPure (ValueCode v c)) :<*> b) Empty l
 344     where
 345     v = Value (either Right Left)
 346     c = [||either Right Left||]
 347   -- Branch Fusion Law
 348   Branch (Branch b Empty (Pure (trans -> lr))) Empty br ->
 349     -- trace "Branch Fusion Law" $
 350     optimizeCombNode (Branch (optimizeCombNode (Pure (H.CombPure (ValueCode (Value v) c)) :<*> b))
 351                              Empty br)
 352     where
 353     v Left{} = Left ()
 354     v (Right r) = case getValue lr r of
 355                    Left _ -> Left ()
 356                    Right rr -> Right rr
 357     c = [|| \case Left{} -> Left ()
 358                   Right r -> case $$(getCode lr) r of
 359                                Left _ -> Left ()
 360                                Right rr -> Right rr ||]
 361   -- Branch Distributivity Law
 362   f :<$> Branch b l r ->
 363     -- trace "Branch Distributivity Law" $
 364     optimizeCombNode (Branch b (optimizeCombNode ((H..@) (H..) f :<$> l))
 365                                (optimizeCombNode ((H..@) (H..) f :<$> r)))
 366
 367   -- Match Absorption Law
 368   Match _ _ Empty d ->
 369     -- trace "Match Absorption Law" $
 370     d
 371   -- Match Weakening Law
 372   Match _ bs a Empty
 373     | all (\case {Empty -> True; _ -> False}) bs ->
 374       -- trace "Match Weakening Law" $
 375       optimizeCombNode (a :*> Empty)
 376   -- Match Pure Law
 377   Match ps bs (Pure (trans -> a)) d ->
 378     -- trace "Match Pure Law" $
 379     foldr (\(trans -> p, b) next ->
 380       if getValue p (getValue a) then b else next
 381     ) d (List.zip ps bs)
 382   -- Match Distributivity Law
 383   f :<$> Match ps bs a d ->
 384     -- trace "Match Distributivity Law" $
 385     Match ps (optimizeCombNode . (f :<$>) Functor.<$> bs) a
 386              (optimizeCombNode (f :<$> d))
 387
 388   {- Possibly useless laws to be tested
 389   Empty  :*> _ -> Empty
 390   Empty :<*  _ -> Empty
 391   -- App Definition of *> Law
 392   H.Flip H..@ H.Const :<$> p :<*> q ->
 393     -- -- trace "EXTRALAW: App Definition of *> Law" $
 394     p :*> q
 395   -- App Definition of <* Law
 396   H.Const :<$> p :<*> q ->
 397     -- -- trace "EXTRALAW: App Definition of <* Law" $
 398     p :<* q
 399
 400   -- Functor Composition Law
 401   -- (a shortcut that could also have been be caught
 402   -- by the Composition Law and Homomorphism Law)
 403   f :<$> (g :<$> p) ->
 404     -- -- trace "EXTRALAW: Functor Composition Law" $
 405     optimizeCombNode ((H.:.) H..@ f H..@ g :<$> p)
 406   -- Applicable Failure Weakening Law
 407   u :<*  Empty ->
 408     -- -- trace "EXTRALAW: App Failure Weakening Law" $
 409     optimizeCombNode (u :*> Empty)
 410   Try (p :$> x) ->
 411     -- -- trace "EXTRALAW: Try Interchange Right Law" $
 412     optimizeCombNode (optimizeCombNode (Try p) :$> x)
 413   -- App Reassociation Law 1
 414   (u :*> v) :<*> w ->
 415     -- -- trace "EXTRALAW: App Reassociation Law 1" $
 416     optimizeCombNode (u :*> optimizeCombNode (v :<*> w))
 417   -- App Reassociation Law 2
 418   u :<*> (v :<* w) ->
 419     -- -- trace "EXTRALAW: App Reassociation Law 2" $
 420     optimizeCombNode (optimizeCombNode (u :<*> v) :<* w)
 421   -- App Right Associativity Law
 422   u :*> (v :*> w) ->
 423     -- -- trace "EXTRALAW: App Right Associativity Law" $
 424     optimizeCombNode (optimizeCombNode (u :*> v) :*> w)
 425   -- App Reassociation Law 3
 426   u :<*> (v :$> x) ->
 427     -- -- trace "EXTRALAW: App Reassociation Law 3" $
 428     optimizeCombNode (optimizeCombNode (u :<*> Pure x) :<* v)
 429
 430   Look (p :$> x) ->
 431     optimizeCombNode (optimizeCombNode (Look p) :$> x)
 432   NegLook (p :$> _) -> optimizeCombNode (NegLook p)
 433
 434   -- NegLook Absorption Law
 435   p :<*> NegLook q ->
 436     -- trace "EXTRALAW: Neglook Absorption Law" $
 437     optimizeCombNode (optimizeCombNode (p :<*> Pure H.unit) :<* NegLook q)
 438     -- Infinite loop, because :<* expands to :<*>
 439   -}
 440
 441   x -> x