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.Haskell (ValueCode(..), Value(..), getValue, code)
  19 import Symantic.Univariant.Letable
  20 import Symantic.Univariant.Trans
  21 import qualified Symantic.Parser.Haskell 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.Haskell a -> Comb repr a
  38   Satisfy ::
  39     Satisfiable repr tok =>
  40     [ErrorItem tok] ->
  41     H.Haskell (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.Haskell (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.Haskell (a -> b) -> Comb repr a -> Comb repr b
  62 pattern (:$>) :: Comb repr a -> H.Haskell b -> Comb repr b
  63 pattern (:<$) :: H.Haskell 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   _ :<*> Empty ->
 196     -- In Parsley: this is only a weakening to u :*> Empty
 197     -- but here :*> is an alias to :<*>
 198     -- hence it would loop on itself forever.
 199     -- trace "App Left Absorption Law" $
 200     Empty
 201   -- App Composition Law
 202   u :<*> (v :<*> w) ->
 203     -- trace "App Composition Law" $
 204     optimizeCombNode (optimizeCombNode (optimizeCombNode ((H.:.) :<$> u) :<*> v) :<*> w)
 205   -- App Interchange Law
 206   u :<*> Pure x ->
 207     -- trace "App Interchange Law" $
 208     optimizeCombNode (H.Flip H..@ (H.:$) H..@ x :<$> u)
 209   -- App Left Absorption Law
 210   p :<* (_ :<$> q) ->
 211     -- trace "App Left Absorption Law" $
 212     p :<* q
 213   -- App Right Absorption Law
 214   (_ :<$> p) :*> q ->
 215     -- trace "App Right Absorption Law" $
 216     p :*> q
 217   -- App Pure Left Identity Law
 218   Pure _ :*> u ->
 219     -- trace "App Pure Left Identity Law" $
 220     u
 221   -- App Functor Left Identity Law
 222   (u :$> _) :*> v ->
 223     -- trace "App Functor Left Identity Law" $
 224     u :*> v
 225   -- App Pure Right Identity Law
 226   u :<* Pure _ ->
 227     -- trace "App Pure Right Identity Law" $
 228     u
 229   -- App Functor Right Identity Law
 230   u :<* (v :$> _) ->
 231     -- trace "App Functor Right Identity Law" $
 232     optimizeCombNode (u :<* v)
 233   -- App Left Associativity Law
 234   (u :<* v) :<* w ->
 235     -- trace "App Left Associativity Law" $
 236     optimizeCombNode (u :<* optimizeCombNode (v :<* w))
 237
 238   -- Alt Left CatchFail Law
 239   p@Pure{} :<|> _ ->
 240     -- trace "Alt Left CatchFail Law" $
 241     p
 242   -- Alt Left Neutral Law
 243   Empty :<|> u ->
 244     -- trace "Alt Left Neutral Law" $
 245     u
 246   -- All Right Neutral Law
 247   u :<|> Empty ->
 248     -- trace "Alt Right Neutral Law" $
 249     u
 250   -- Alt Associativity Law
 251   (u :<|> v) :<|> w ->
 252     -- trace "Alt Associativity Law" $
 253     u :<|> optimizeCombNode (v :<|> w)
 254
 255   -- Look Pure Law
 256   Look p@Pure{} ->
 257     -- trace "Look Pure Law" $
 258     p
 259   -- Look Empty Law
 260   Look p@Empty ->
 261     -- trace "Look Empty Law" $
 262     p
 263   -- NegLook Pure Law
 264   NegLook Pure{} ->
 265     -- trace "NegLook Pure Law" $
 266     Empty
 267   -- NegLook Empty Law
 268   NegLook Empty ->
 269     -- trace "NegLook Dead Law" $
 270     Pure H.unit
 271   -- NegLook Double Negation Law
 272   NegLook (NegLook p) ->
 273     -- trace "NegLook Double Negation Law" $
 274     optimizeCombNode (Look (Try p) :*> Pure H.unit)
 275   -- NegLook Zero Consumption Law
 276   NegLook (Try p) ->
 277     -- trace "NegLook Zero Consumption Law" $
 278     optimizeCombNode (NegLook p)
 279   -- Idempotence Law
 280   Look (Look p) ->
 281     -- trace "Look Idempotence Law" $
 282     Look p
 283   -- Look Right Identity Law
 284   NegLook (Look p) ->
 285     -- trace "Look Right Identity Law" $
 286     optimizeCombNode (NegLook p)
 287   -- Look Left Identity Law
 288   Look (NegLook p) ->
 289     -- trace "Look Left Identity Law" $
 290     NegLook p
 291   -- NegLook Transparency Law
 292   NegLook (Try p :<|> q) ->
 293     -- trace "NegLook Transparency Law" $
 294     optimizeCombNode (optimizeCombNode (NegLook p) :*> optimizeCombNode (NegLook q))
 295   -- Look Distributivity Law
 296   Look p :<|> Look q ->
 297     -- trace "Look Distributivity Law" $
 298     optimizeCombNode (Look (optimizeCombNode (Try p :<|> q)))
 299   -- Look Interchange Law
 300   Look (f :<$> p) ->
 301     -- trace "Look Interchange Law" $
 302     optimizeCombNode (f :<$> optimizeCombNode (Look p))
 303   -- NegLook Idempotence Right Law
 304   NegLook (_ :<$> p) ->
 305     -- trace "NegLook Idempotence Law" $
 306     optimizeCombNode (NegLook p)
 307   -- Try Interchange Law
 308   Try (f :<$> p) ->
 309     -- trace "Try Interchange Law" $
 310     optimizeCombNode (f :<$> optimizeCombNode (Try p))
 311
 312   -- Branch Absorption Law
 313   Branch Empty _ _ ->
 314     -- trace "Branch Absorption Law" $
 315     empty
 316   -- Branch Weakening Law
 317   Branch b Empty Empty ->
 318     -- trace "Branch Weakening Law" $
 319     optimizeCombNode (b :*> Empty)
 320   -- Branch Pure Left/Right Laws
 321   Branch (Pure (trans -> lr)) l r ->
 322     -- trace "Branch Pure Left/Right Law" $
 323     case getValue lr of
 324      Left v -> optimizeCombNode (l :<*> Pure (H.Haskell (ValueCode (Value v) c)))
 325       where c = [|| case $$(code lr) of Left x -> x ||]
 326      Right v -> optimizeCombNode (r :<*> Pure (H.Haskell (ValueCode (Value v) c)))
 327       where c = [|| case $$(code lr) of Right x -> x ||]
 328   -- Branch Generalised Identity Law
 329   Branch b (Pure (trans -> l)) (Pure (trans -> r)) ->
 330     -- trace "Branch Generalised Identity Law" $
 331     optimizeCombNode (H.Haskell (ValueCode v c) :<$> b)
 332     where
 333     v = Value (either (getValue l) (getValue r))
 334     c = [|| either $$(code l) $$(code r) ||]
 335   -- Branch Interchange Law
 336   Branch (x :*> y) p q ->
 337     -- trace "Branch Interchange Law" $
 338     optimizeCombNode (x :*> optimizeCombNode (Branch y p q))
 339   -- Branch Empty Right Law
 340   Branch b l Empty ->
 341     -- trace " Branch Empty Right Law" $
 342     Branch (Pure (H.Haskell (ValueCode v c)) :<*> b) Empty l
 343     where
 344     v = Value (either Right Left)
 345     c = [||either Right Left||]
 346   -- Branch Fusion Law
 347   Branch (Branch b Empty (Pure (trans -> lr))) Empty br ->
 348     -- trace "Branch Fusion Law" $
 349     optimizeCombNode (Branch (optimizeCombNode (Pure (H.Haskell (ValueCode (Value v) c)) :<*> b))
 350                              Empty br)
 351     where
 352     v Left{} = Left ()
 353     v (Right r) = case getValue lr r of
 354                    Left _ -> Left ()
 355                    Right rr -> Right rr
 356     c = [|| \case Left{} -> Left ()
 357                   Right r -> case $$(code lr) r of
 358                               Left _ -> Left ()
 359                               Right rr -> Right rr ||]
 360   -- Branch Distributivity Law
 361   f :<$> Branch b l r ->
 362     -- trace "Branch Distributivity Law" $
 363     optimizeCombNode (Branch b (optimizeCombNode ((H..@) (H..) f :<$> l))
 364                                (optimizeCombNode ((H..@) (H..) f :<$> r)))
 365
 366   -- Match Absorption Law
 367   Match _ _ Empty d ->
 368     -- trace "Match Absorption Law" $
 369     d
 370   -- Match Weakening Law
 371   Match _ bs a Empty
 372     | all (\case {Empty -> True; _ -> False}) bs ->
 373       -- trace "Match Weakening Law" $
 374       optimizeCombNode (a :*> Empty)
 375   -- Match Pure Law
 376   Match ps bs (Pure (trans -> a)) d ->
 377     -- trace "Match Pure Law" $
 378     foldr (\(trans -> p, b) next ->
 379       if getValue p (getValue a) then b else next
 380     ) d (List.zip ps bs)
 381   -- Match Distributivity Law
 382   f :<$> Match ps bs a d ->
 383     -- trace "Match Distributivity Law" $
 384     Match ps (optimizeCombNode . (f :<$>) Functor.<$> bs) a
 385              (optimizeCombNode (f :<$> d))
 386
 387   {- Possibly useless laws to be tested
 388   Empty  :*> _ -> Empty
 389   Empty :<*  _ -> Empty
 390   -- App Definition of *> Law
 391   H.Flip H..@ H.Const :<$> p :<*> q ->
 392     -- -- trace "EXTRALAW: App Definition of *> Law" $
 393     p :*> q
 394   -- App Definition of <* Law
 395   H.Const :<$> p :<*> q ->
 396     -- -- trace "EXTRALAW: App Definition of <* Law" $
 397     p :<* q
 398
 399   -- Functor Composition Law
 400   -- (a shortcut that could also have been be caught
 401   -- by the Composition Law and Homomorphism Law)
 402   f :<$> (g :<$> p) ->
 403     -- -- trace "EXTRALAW: Functor Composition Law" $
 404     optimizeCombNode ((H.:.) H..@ f H..@ g :<$> p)
 405   -- Applicable Failure Weakening Law
 406   u :<*  Empty ->
 407     -- -- trace "EXTRALAW: App Failure Weakening Law" $
 408     optimizeCombNode (u :*> Empty)
 409   Try (p :$> x) ->
 410     -- -- trace "EXTRALAW: Try Interchange Right Law" $
 411     optimizeCombNode (optimizeCombNode (Try p) :$> x)
 412   -- App Reassociation Law 1
 413   (u :*> v) :<*> w ->
 414     -- -- trace "EXTRALAW: App Reassociation Law 1" $
 415     optimizeCombNode (u :*> optimizeCombNode (v :<*> w))
 416   -- App Reassociation Law 2
 417   u :<*> (v :<* w) ->
 418     -- -- trace "EXTRALAW: App Reassociation Law 2" $
 419     optimizeCombNode (optimizeCombNode (u :<*> v) :<* w)
 420   -- App Right Associativity Law
 421   u :*> (v :*> w) ->
 422     -- -- trace "EXTRALAW: App Right Associativity Law" $
 423     optimizeCombNode (optimizeCombNode (u :*> v) :*> w)
 424   -- App Reassociation Law 3
 425   u :<*> (v :$> x) ->
 426     -- -- trace "EXTRALAW: App Reassociation Law 3" $
 427     optimizeCombNode (optimizeCombNode (u :<*> Pure x) :<* v)
 428
 429   Look (p :$> x) ->
 430     optimizeCombNode (optimizeCombNode (Look p) :$> x)
 431   NegLook (p :$> _) -> optimizeCombNode (NegLook p)
 432
 433   -- NegLook Absorption Law
 434   p :<*> NegLook q ->
 435     -- trace "EXTRALAW: Neglook Absorption Law" $
 436     optimizeCombNode (optimizeCombNode (p :<*> Pure H.unit) :<* NegLook q)
 437     -- Infinite loop, because :<* expands to :<*>
 438   -}
 439
 440   x -> x