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