src/Symantic/Parser/Grammar/Optimize.hs

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