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 Data.Kind (Type)
  14 import qualified Data.Functor as Functor
  15 import qualified Data.List as List
  16 import qualified Language.Haskell.TH.Syntax as TH
  17
  18 import Symantic.Parser.Grammar.Combinators as Comb
  19 import Symantic.Parser.Staging (ValueCode(..), Value(..), getValue, code)
  20 import Symantic.Univariant.Letable
  21 import Symantic.Univariant.Trans
  22 import qualified Symantic.Parser.Staging as H
  23
  24 -- import Debug.Trace (trace)
  25
  26 -- * Type 'Comb'
  27 -- | Pattern-matchable 'Comb'inators of the grammar.
  28 -- @(repr)@ is not strictly necessary since it's only a phantom type
  29 -- (no constructor use it as a value), but having it:
  30 --
  31 -- 1. emphasizes that those 'Comb'inators will be 'trans'formed again
  32 --    (eg. in 'DumpComb' or 'Instr'uctions).
  33 --
  34 -- 2. Avoid overlapping instances between
  35 --    @('Trans' ('Comb' repr) repr)@ and
  36 --    @('Trans' ('Comb' repr) ('OptimizeComb' letName repr))@
  37 data Comb (repr :: Type -> Type) a where
  38   Pure :: H.Haskell a -> Comb repr a
  39   Satisfy :: H.Haskell (Char -> Bool) -> Comb repr Char
  40   Item :: Comb repr Char
  41   Try :: Comb repr a -> Comb repr a
  42   Look :: Comb repr a -> Comb repr a
  43   NegLook :: Comb repr a -> Comb repr ()
  44   (:<*>) :: Comb repr (a -> b) -> Comb repr a -> Comb repr b
  45   (:<|>) :: Comb repr a -> Comb repr a -> Comb repr a
  46   Empty :: Comb repr a
  47   Branch :: Comb repr (Either a b) -> Comb repr (a -> c) -> Comb repr (b -> c) -> Comb repr c
  48   Match :: Eq a => [H.Haskell (a -> Bool)] -> [Comb repr b] -> Comb repr a -> Comb repr b -> Comb repr b
  49   ChainPre :: Comb repr (a -> a) -> Comb repr a -> Comb repr a
  50   ChainPost :: Comb repr a -> Comb repr (a -> a) -> Comb repr a
  51   Def :: TH.Name -> Comb repr a -> Comb repr a
  52   Ref :: Bool -> TH.Name -> Comb repr a
  53
  54 pattern (:<$>) :: H.Haskell (a -> b) -> Comb repr a -> Comb repr b
  55 pattern (:$>) :: Comb repr a -> H.Haskell b -> Comb repr b
  56 pattern (:<$) :: H.Haskell a -> Comb repr b -> Comb repr a
  57 pattern (:*>) :: Comb repr a -> Comb repr b -> Comb repr b
  58 pattern (:<*) :: Comb repr a -> Comb repr b -> Comb repr a
  59 pattern x :<$> p = Pure x :<*> p
  60 pattern p :$> x = p :*> Pure x
  61 pattern x :<$ p = Pure x :<* p
  62 pattern x :<* p = H.Const :<$> x :<*> p
  63 pattern p :*> x = H.Id :<$ p :<*> x
  64
  65 infixl 3 :<|>
  66 infixl 4 :<*>, :<*, :*>
  67 infixl 4 :<$>, :<$, :$>
  68
  69 instance Applicable (Comb repr) where
  70   pure = Pure
  71   (<*>) = (:<*>)
  72 instance Alternable (Comb repr) where
  73   (<|>) = (:<|>)
  74   empty = Empty
  75   try = Try
  76 instance Selectable (Comb repr) where
  77   branch = Branch
  78 instance Matchable (Comb repr) where
  79   conditional = Match
  80 instance Foldable (Comb repr) where
  81   chainPre = ChainPre
  82   chainPost = ChainPost
  83 instance Charable (Comb repr) where
  84   satisfy = Satisfy
  85 instance Lookable (Comb repr) where
  86   look = Look
  87   negLook = NegLook
  88 instance Letable TH.Name (Comb repr) where
  89   def = Def
  90   ref = Ref
  91 instance MakeLetName TH.Name where
  92   makeLetName _ = TH.qNewName "name"
  93
  94 -- Pattern-matchable 'Comb'inators keep enough structure
  95 -- to have some of the symantics producing them interpreted again
  96 -- (eg. after being modified by 'optimizeComb').
  97 type instance Output (Comb repr) = repr
  98 instance
  99   ( Applicable repr
 100   , Alternable repr
 101   , Selectable repr
 102   , Foldable repr
 103   , Charable repr
 104   , Lookable repr
 105   , Matchable repr
 106   , Letable TH.Name repr
 107   ) => Trans (Comb repr) repr where
 108   trans = \case
 109     Pure a -> pure a
 110     Satisfy p -> satisfy p
 111     Item -> item
 112     Try x -> try (trans x)
 113     Look x -> look (trans x)
 114     NegLook x -> negLook (trans x)
 115     x :<*> y -> trans x <*> trans y
 116     x :<|> y -> trans x <|> trans y
 117     Empty -> empty
 118     Branch lr l r -> branch (trans lr) (trans l) (trans r)
 119     Match ps bs a b -> conditional ps (trans Functor.<$> bs) (trans a) (trans b)
 120     ChainPre x y -> chainPre (trans x) (trans y)
 121     ChainPost x y -> chainPost (trans x) (trans y)
 122     Def n x -> def n (trans x)
 123     Ref r n -> ref r n
 124
 125 -- * Type 'OptimizeComb'
 126 -- Bottom-up application of 'optimizeCombNode'.
 127 newtype OptimizeComb letName repr a = OptimizeComb { unOptimizeComb :: Comb repr a }
 128
 129 optimizeComb ::
 130   Trans (OptimizeComb TH.Name repr) repr =>
 131   OptimizeComb TH.Name repr a -> repr a
 132 optimizeComb = trans
 133 instance
 134   Trans (Comb repr) repr =>
 135   Trans (OptimizeComb letName repr) repr where
 136   trans = trans . unOptimizeComb
 137
 138 type instance Output (OptimizeComb _letName repr) = Comb repr
 139 instance Trans (OptimizeComb letName repr) (Comb repr) where
 140   trans = unOptimizeComb
 141 instance Trans (Comb repr) (OptimizeComb letName repr) where
 142   trans = OptimizeComb . optimizeCombNode
 143 instance Trans1 (Comb repr) (OptimizeComb letName repr)
 144 instance Trans2 (Comb repr) (OptimizeComb letName repr)
 145 instance Trans3 (Comb repr) (OptimizeComb letName repr)
 146
 147 instance
 148   Letable letName (Comb repr) =>
 149   Letable letName (OptimizeComb letName repr) where
 150   -- Disable useless calls to 'optimizeCombNode'
 151   -- because 'Def' or 'Ref' have no matching in it.
 152   def n = OptimizeComb . def n . unOptimizeComb
 153   ref r n = OptimizeComb (ref r n)
 154 instance Comb.Applicable (OptimizeComb letName repr)
 155 instance Comb.Alternable (OptimizeComb letName repr)
 156 instance Comb.Charable (OptimizeComb letName repr)
 157 instance Comb.Selectable (OptimizeComb letName repr)
 158 instance Comb.Matchable (OptimizeComb letName repr)
 159 instance Comb.Lookable (OptimizeComb letName repr)
 160 instance Comb.Foldable (OptimizeComb letName repr)
 161
 162 optimizeCombNode :: Comb repr a -> Comb repr a
 163 optimizeCombNode = \case
 164   -- Functor Identity Law
 165   H.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   H.Flip H.:@ H.Const :<$> u ->
 174     -- trace "Functor Flip Const Law" $
 175     optimizeCombNode (u :*> Pure H.Id)
 176   -- Functor Homomorphism Law
 177   f :<$> Pure x ->
 178     -- trace "Functor Homomorphism Law" $
 179     Pure (f H..@ 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 ((H.:.) :<$> u) :<*> v) :<*> w)
 195   -- App Interchange Law
 196   u :<*> Pure x ->
 197     -- trace "App Interchange Law" $
 198     optimizeCombNode (H.Flip H..@ (H.:$) H..@ 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 H.unit
 261   -- NegLook Double Negation Law
 262   NegLook (NegLook p) ->
 263     -- trace "NegLook Double Negation Law" $
 264     optimizeCombNode (Look (Try p) :*> Pure H.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 H.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 (H.Haskell (ValueCode (Value v) c)))
 319       where c = [|| case $$(code lr) of Left x -> x ||]
 320      Right v -> optimizeCombNode (r :<*> Pure (H.Haskell (ValueCode (Value v) c)))
 321       where c = [|| case $$(code 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 (H.Haskell (ValueCode v c) :<$> b)
 326     where
 327     v = Value (either (getValue l) (getValue r))
 328     c = [|| either $$(code l) $$(code 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 (H.Haskell (ValueCode v c)) :<*> b) Empty l
 337     where
 338     v = Value (either Right Left)
 339     c = [||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 (H.Haskell (ValueCode (Value v) c)) :<*> b))
 344                              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 = [|| \case Left{} -> Left ()
 351                   Right r -> case $$(code 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 ((H..@) (H..) f :<$> l))
 358                                (optimizeCombNode ((H..@) (H..) f :<$> r)))
 359
 360   -- Match Absorption Law
 361   Match _ _ Empty d ->
 362     -- trace "Match Absorption Law" $
 363     d
 364   -- Match Weakening Law
 365   Match _ bs a Empty
 366     | all (\case {Empty -> True; _ -> False}) bs ->
 367       -- trace "Match Weakening Law" $
 368       optimizeCombNode (a :*> Empty)
 369   -- Match Pure Law
 370   Match ps bs (Pure (trans -> a)) d ->
 371     -- trace "Match Pure Law" $
 372     foldr (\(trans -> p, b) next ->
 373       if getValue p (getValue a) then b else next
 374     ) d (List.zip ps bs)
 375   -- Match Distributivity Law
 376   f :<$> Match ps bs a d ->
 377     -- trace "Match Distributivity Law" $
 378     Match ps (optimizeCombNode . (f :<$>) Functor.<$> bs) a
 379              (optimizeCombNode (f :<$> d))
 380
 381   {- Possibly useless laws to be tested
 382   Empty  :*> _ -> Empty
 383   Empty :<*  _ -> Empty
 384   -- App Definition of *> Law
 385   H.Flip H..@ H.Const :<$> p :<*> q ->
 386     -- trace "EXTRALAW: App Definition of *> Law" $
 387     p :*> q
 388   -- App Definition of <* Law
 389   H.Const :<$> p :<*> q ->
 390     -- trace "EXTRALAW: App Definition of <* Law" $
 391     p :<* q
 392
 393   -- Functor Composition Law
 394   -- (a shortcut that could also have been be caught
 395   -- by the Composition Law and Homomorphism Law)
 396   f :<$> (g :<$> p) ->
 397     -- trace "EXTRALAW: Functor Composition Law" $
 398     optimizeCombNode ((H.:.) H..@ f H..@ g :<$> p)
 399   -- Applicable Failure Weakening Law
 400   u :<*  Empty ->
 401     -- trace "EXTRALAW: App Failure Weakening Law" $
 402     optimizeCombNode (u :*> Empty)
 403   Try (p :$> x) ->
 404     -- trace "EXTRALAW: Try Interchange Right Law" $
 405     optimizeCombNode (optimizeCombNode (Try p) :$> x)
 406   -- App Reassociation Law 1
 407   (u :*> v) :<*> w ->
 408     -- trace "EXTRALAW: App Reassociation Law 1" $
 409     optimizeCombNode (u :*> optimizeCombNode (v :<*> w))
 410   -- App Reassociation Law 2
 411   u :<*> (v :<* w) ->
 412     -- trace "EXTRALAW: App Reassociation Law 2" $
 413     optimizeCombNode (optimizeCombNode (u :<*> v) :<* w)
 414   -- App Right Associativity Law
 415   u :*> (v :*> w) ->
 416     -- trace "EXTRALAW: App Right Associativity Law" $
 417     optimizeCombNode (optimizeCombNode (u :*> v) :*> w)
 418   -- App Reassociation Law 3
 419   u :<*> (v :$> x) ->
 420     -- trace "EXTRALAW: App Reassociation Law 3" $
 421     optimizeCombNode (optimizeCombNode (u :<*> Pure x) :<* v)
 422
 423   Look (p :$> x) ->
 424     optimizeCombNode (optimizeCombNode (Look p) :$> x)
 425   NegLook (p :$> _) -> optimizeCombNode (NegLook p)
 426
 427   -}
 428
 429   x -> x