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