src/Symantic/Parser/Grammar/Optimize.hs

   1 {-# LANGUAGE PatternSynonyms #-} -- For Comb and OptC
   2 {-# LANGUAGE TemplateHaskell #-} -- For branch
   3 {-# LANGUAGE ViewPatterns #-} -- For unSomeComb
   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.Function ((.))
  11 import Data.Maybe (Maybe(..))
  12 import qualified Data.Functor as Functor
  13 import qualified Data.Foldable as Foldable
  14 import qualified Data.List as List
  15 import qualified Language.Haskell.TH.Syntax as TH
  16 import Data.Kind (Constraint, Type)
  17 import Type.Reflection (Typeable, typeRep, eqTypeRep, (:~~:)(..))
  18
  19 import Symantic.Parser.Grammar.Combinators as Comb
  20 import Symantic.Parser.Haskell ()
  21 import Symantic.Univariant.Letable
  22 import Symantic.Univariant.Trans
  23 import qualified Symantic.Parser.Haskell as H
  24
  25 {-
  26 import Data.Function (($), flip)
  27 import Debug.Trace (trace)
  28
  29 (&) = flip ($)
  30 infix 0 &
  31 -}
  32
  33 -- * Data family 'Comb'
  34 -- | 'Comb'uctions for the 'Machine'.
  35 -- This is an extensible data-type.
  36 data family Comb
  37   (comb :: ReprComb -> Constraint)
  38   (repr :: ReprComb)
  39   :: ReprComb
  40
  41 -- | Convenient utility to pattern-match a 'SomeComb'.
  42 pattern Comb :: Typeable comb =>
  43   Comb comb repr a ->
  44   SomeComb repr a
  45 pattern Comb x <- (unSomeComb -> Just x)
  46
  47 -- ** Type 'ReprComb'
  48 type ReprComb = Type -> Type
  49
  50 -- ** Type 'SomeComb'
  51 -- | Some 'Comb'inator existentialized over the actual combinator symantic class.
  52 -- Useful to handle a list of 'Comb'inators
  53 -- without requiring impredicative quantification.
  54 -- Must be used by pattern-matching
  55 -- on the 'SomeComb' data-constructor,
  56 -- to bring the constraints in scope.
  57 data SomeComb repr a =
  58   forall comb.
  59   (Trans (Comb comb repr) repr, Typeable comb) =>
  60   SomeComb (Comb comb repr a)
  61
  62 instance Trans (SomeComb repr) repr where
  63   trans (SomeComb x) = trans x
  64
  65 -- | @(unSomeComb c :: 'Maybe' ('Comb' comb repr a))@
  66 -- extract the data-constructor from the given 'SomeComb'
  67 -- iif. it belongs to the @('Comb' comb repr a)@ data-instance.
  68 unSomeComb ::
  69   forall comb repr a.
  70   Typeable comb =>
  71   SomeComb repr a -> Maybe (Comb comb repr a)
  72 unSomeComb (SomeComb (c::Comb c repr a)) =
  73   case typeRep @comb `eqTypeRep` typeRep @c of
  74     Just HRefl -> Just c
  75     Nothing -> Nothing
  76
  77 -- Applicable
  78 data instance Comb Applicable repr a where
  79   Pure :: TermGrammar a -> Comb Applicable repr a
  80   (:<*>:) :: SomeComb repr (a -> b) -> SomeComb repr a -> Comb Applicable repr b
  81   (:<*:) :: SomeComb repr a -> SomeComb repr b -> Comb Applicable repr a
  82   (:*>:) :: SomeComb repr a -> SomeComb repr b -> Comb Applicable repr b
  83 infixl 4 :<*>:, :<*:, :*>:
  84 pattern (:<$>:) :: TermGrammar (a -> b) -> SomeComb repr a -> Comb Applicable repr b
  85 pattern t :<$>: x <- Comb (Pure t) :<*>: x
  86 pattern (:$>:) :: SomeComb repr a -> TermGrammar b -> Comb Applicable repr b
  87 pattern x :$>: t <- x :*>: Comb (Pure t)
  88 instance Applicable repr => Trans (Comb Applicable repr) repr where
  89   trans = \case
  90     Pure x -> pure (H.optimizeTerm x)
  91     f :<*>: x -> trans f <*> trans x
  92     x :<*: y -> trans x <* trans y
  93     x :*>: y -> trans x *> trans y
  94 instance Applicable repr => Applicable (SomeComb repr) where
  95   pure = SomeComb . Pure
  96   (<*>) f = SomeComb . (:<*>:) f
  97   (<*) x = SomeComb . (:<*:) x
  98   (*>) x = SomeComb . (:*>:) x
  99
 100 -- Alternable
 101 data instance Comb Alternable repr a where
 102   Empty :: Comb Alternable repr a
 103   (:<|>:) :: SomeComb repr a -> SomeComb repr a -> Comb Alternable repr a
 104   Try :: SomeComb repr a -> Comb Alternable repr a
 105 infixl 3 :<|>:
 106 instance Alternable repr => Trans (Comb Alternable repr) repr where
 107   trans = \case
 108     Empty -> empty
 109     f :<|>: x -> trans f <|> trans x
 110     Try x -> try (trans x)
 111 instance Alternable repr => Alternable (SomeComb repr) where
 112   empty = SomeComb Empty
 113   (<|>) f = SomeComb . (:<|>:) f
 114   try = SomeComb . Try
 115
 116 -- Selectable
 117 data instance Comb Selectable repr a where
 118   Branch ::
 119     SomeComb repr (Either a b) ->
 120     SomeComb repr (a -> c) ->
 121     SomeComb repr (b -> c) ->
 122     Comb Selectable repr c
 123 instance Selectable repr => Trans (Comb Selectable repr) repr where
 124   trans = \case
 125     Branch lr l r -> branch (trans lr) (trans l) (trans r)
 126 instance Selectable repr => Selectable (SomeComb repr) where
 127   branch lr l = SomeComb . Branch lr l
 128
 129 -- Matchable
 130 data instance Comb Matchable repr a where
 131   Conditional :: Eq a =>
 132     SomeComb repr a ->
 133     [TermGrammar (a -> Bool)] ->
 134     [SomeComb repr b] ->
 135     SomeComb repr b ->
 136     Comb Matchable repr b
 137 instance Matchable repr => Trans (Comb Matchable repr) repr where
 138   trans = \case
 139     Conditional a ps bs b -> conditional (trans a) ps (trans Functor.<$> bs) (trans b)
 140 instance Matchable repr => Matchable (SomeComb repr) where
 141   conditional a ps bs = SomeComb . Conditional a ps bs
 142
 143 -- Foldable
 144 data instance Comb Foldable repr a where
 145   ChainPreC :: SomeComb repr (a -> a) -> SomeComb repr a -> Comb Foldable repr a
 146   ChainPostC :: SomeComb repr a -> SomeComb repr (a -> a) -> Comb Foldable repr a
 147 instance Foldable repr => Trans (Comb Foldable repr) repr where
 148   trans = \case
 149     ChainPreC x y -> chainPre (trans x) (trans y)
 150     ChainPostC x y -> chainPost (trans x) (trans y)
 151 instance Foldable repr => Foldable (SomeComb repr) where
 152   chainPre x = SomeComb . ChainPreC x
 153   chainPost x = SomeComb . ChainPostC x
 154
 155 -- Lookable
 156 data instance Comb Lookable repr a where
 157   Look :: SomeComb repr a -> Comb Lookable repr a
 158   NegLook :: SomeComb repr a -> Comb Lookable repr ()
 159   Eof :: Comb Lookable repr ()
 160 instance Lookable repr => Trans (Comb Lookable repr) repr where
 161   trans = \case
 162     Look x -> look (trans x)
 163     NegLook x -> negLook (trans x)
 164     Eof -> eof
 165 instance Lookable repr => Lookable (SomeComb repr) where
 166   look = SomeComb . Look
 167   negLook = SomeComb . NegLook
 168   eof = SomeComb Eof
 169
 170 -- Satisfiable
 171 data instance Comb (Satisfiable tok) repr a where
 172   Satisfy ::
 173     Satisfiable tok repr =>
 174     [ErrorItem tok] ->
 175     TermGrammar (tok -> Bool) ->
 176     Comb (Satisfiable tok) repr tok
 177   Item ::
 178     Satisfiable tok repr =>
 179     Comb (Satisfiable tok) repr tok
 180 instance Satisfiable tok repr => Trans (Comb (Satisfiable tok) repr) repr where
 181   trans = \case
 182     Satisfy es p -> satisfy es p
 183     Item -> item
 184 instance
 185   (Satisfiable tok repr, Typeable tok) =>
 186   Satisfiable tok (SomeComb repr) where
 187   satisfy es = SomeComb . Satisfy es
 188   item = SomeComb Item
 189
 190 -- Letable
 191 data instance Comb (Letable letName) repr a where
 192   Def :: letName -> SomeComb repr a -> Comb (Letable letName) repr a
 193   Ref :: Bool -> letName -> Comb (Letable letName) repr a
 194 instance Letable letName repr => Trans (Comb (Letable letName) repr) repr where
 195   trans = \case
 196     Def n v -> def n (trans v)
 197     Ref isRec n -> ref isRec n
 198 instance
 199   (Letable letName repr, Typeable letName) =>
 200   Letable letName (SomeComb repr) where
 201   def n = SomeComb . Def n
 202   ref isRec = SomeComb . Ref isRec
 203 instance MakeLetName TH.Name where
 204   makeLetName _ = TH.qNewName "name"
 205
 206 -- * Type 'OptimizeGrammar'
 207 type OptimizeGrammar = OptComb
 208
 209 optimizeGrammar ::
 210   Trans (OptComb TH.Name repr) repr =>
 211   OptComb TH.Name repr a -> repr a
 212 optimizeGrammar = trans
 213
 214 -- ** Type 'OptComb'
 215 newtype OptComb letName repr a =
 216         OptComb { unOptComb :: SomeComb repr a }
 217 -- | Matching an 'OptComb'.
 218 pattern OptC :: Typeable comb => Comb comb repr a -> OptComb letName repr a
 219 pattern OptC x <- (unSomeComb . unOptComb -> Just x)
 220 instance
 221   Trans (SomeComb repr) repr =>
 222   Trans (OptComb letName repr) repr where
 223   trans = trans . unOptComb
 224
 225 instance
 226   ( Applicable repr
 227   , Alternable repr
 228   , Lookable repr
 229   , Selectable repr
 230   , Matchable repr
 231   ) => Applicable (OptComb letName repr) where
 232   pure = OptComb . pure
 233
 234   f <$> OptC (Branch b l r) =
 235     branch (OptComb b)
 236       ((H..) H..@ f <$> OptComb l)
 237       ((H..) H..@ f <$> OptComb r)
 238     -- & trace "Branch Distributivity Law"
 239   f <$> OptC (Conditional a ps bs d) =
 240     conditional (OptComb a) ps
 241       ((f <$>) . OptComb Functor.<$> bs)
 242       (f <$> OptComb d)
 243     -- & trace "Conditional Distributivity Law"
 244   -- Being careful here to use (<*>),
 245   -- instead of OptComb (f <$> unOptComb x),
 246   -- in order to apply the optimizations of (<*>).
 247   f <$> x = pure f <*> x
 248
 249   x <$ u = u $> x
 250     -- & trace "Commutativity Law"
 251
 252   OptC Empty <*> _ = empty
 253     -- & trace "App Right Absorption Law"
 254   u <*> OptC Empty = u *> empty
 255     -- & trace "App Failure Weakening Law"
 256   OptC (Pure f) <*> OptC (Pure x) = pure (f H..@ x)
 257     -- & trace "Homomorphism Law"
 258   OptC (Pure f) <*> OptC (g :<$>: p) =
 259     -- This is basically a shortcut,
 260     -- it can be caught by the Composition Law
 261     -- and Homomorphism Law.
 262     (H..) H..@ f H..@ g <$> OptComb p
 263     -- & trace "Functor Composition Law"
 264   u <*> OptC (v :<*>: w) =
 265     (((H..) <$> u) <*> OptComb v) <*> OptComb w
 266     -- & trace "Composition Law"
 267   u <*> OptC (Pure x) =
 268     H.flip H..@ (H.$) H..@ x <$> u
 269     -- & trace "Interchange Law"
 270   OptC (u :*>: v) <*> w =
 271     OptComb u *> (OptComb v <*> w)
 272     -- & trace "Reassociation Law 1"
 273   u <*> OptC (v :<*: w) =
 274     (u <*> OptComb v) <* OptComb w
 275     -- & trace "Reassociation Law 2"
 276   u <*> OptC (v :$>: x) =
 277     (u <*> pure x) <* OptComb v
 278     -- & trace "Reassociation Law 3"
 279   p <*> OptC (NegLook q) =
 280     (p <*> pure H.unit) <* negLook (OptComb q)
 281     -- & trace "Absorption Law"
 282   OptComb x <*> OptComb y = OptComb (x <*> y)
 283
 284   OptC Empty *> _ = empty
 285     -- & trace "App Right Absorption Law"
 286   OptC (_ :<$>: p) *> q = OptComb p *> q
 287     -- & trace "Right Absorption Law"
 288   OptC Pure{} *> u = u
 289     -- & trace "Identity Law"
 290   OptC (u :$>: _) *> v = OptComb u *> v
 291     -- & trace "Identity Law"
 292   u *> OptC (v :*>: w) =
 293     (u *> OptComb v) *> OptComb w
 294     -- & trace "Associativity Law"
 295   OptComb x *> OptComb y = OptComb (x *> y)
 296
 297   OptC Empty <* _ = empty
 298     -- & trace "App Right Absorption Law"
 299   u <* OptC Empty = u *> empty
 300     -- & trace "App Failure Weakening Law"
 301   p <* OptC (_ :<$>: q) = p <* OptComb q
 302     -- & trace "Left Absorption Law"
 303   u <* OptC Pure{} = u
 304     -- & trace "Identity Law"
 305   u <* OptC (v :$>: _) = u <* OptComb v
 306     -- & trace "Identity Law"
 307   OptC (u :<*: v) <* w = OptComb u <* (OptComb v <* w)
 308     -- & trace "Associativity Law"
 309   OptComb x <* OptComb y = OptComb (x <* y)
 310 instance
 311   ( Applicable repr
 312   , Alternable repr
 313   , Lookable repr
 314   , Selectable repr
 315   , Matchable repr
 316   ) => Alternable (OptComb letName repr) where
 317   empty = OptComb empty
 318
 319   p@(OptC Pure{}) <|> _ = p
 320     -- & trace "Left Catch Law"
 321   OptC Empty <|> u = u
 322     -- & trace "Left Neutral Law"
 323   u <|> OptC Empty = u
 324     -- & trace "Right Neutral Law"
 325   OptC (u :<|>: v) <|> w = OptComb u <|> (OptComb v <|> w)
 326     -- & trace "Associativity Law"
 327   OptC (Look p) <|> OptC (Look q) =
 328     look (try (OptComb p) <|> OptComb q)
 329     -- & trace "Distributivity Law"
 330   OptComb x <|> OptComb y = OptComb (x <|> y)
 331
 332   try (OptC (p :$>: x)) = try (OptComb p) $> x
 333     -- & trace "Try Interchange Law"
 334   try (OptC (f :<$>: p)) = f <$> try (OptComb p)
 335     -- & trace "Try Interchange Law"
 336   try (OptComb x) = OptComb (try x)
 337 instance
 338   ( Applicable repr
 339   , Alternable repr
 340   , Lookable repr
 341   , Selectable repr
 342   , Matchable repr
 343   ) => Lookable (OptComb letName repr) where
 344   look p@(OptC Pure{}) = p
 345     -- & trace "Pure Look Law"
 346   look p@(OptC Empty) = p
 347     -- & trace "Dead Look Law"
 348   look (OptC (Look x)) = look (OptComb x)
 349     -- & trace "Idempotence Law"
 350   look (OptC (NegLook x)) = negLook (OptComb x)
 351     -- & trace "Left Identity Law"
 352   look (OptC (p :$>: x)) = look (OptComb p) $> x
 353     -- & trace "Interchange Law"
 354   look (OptC (f :<$>: p)) = f <$> look (OptComb p)
 355     -- & trace "Interchange Law"
 356   look (OptComb x) = OptComb (look x)
 357
 358   negLook (OptC Pure{}) = empty
 359     -- & trace "Pure Negative-Look"
 360   negLook (OptC Empty) = pure H.unit
 361     -- & trace "Dead Negative-Look"
 362   negLook (OptC (NegLook x)) =
 363     look (try (OptComb x) *> pure H.unit)
 364     -- & trace "Double Negation Law"
 365   negLook (OptC (Try x)) = negLook (OptComb x)
 366     -- & trace "Zero Consumption Law"
 367   negLook (OptC (Look x)) = negLook (OptComb x)
 368     -- & trace "Right Identity Law"
 369   negLook (OptC (Comb (Try p) :<|>: q)) =
 370     negLook (OptComb p) *> negLook (OptComb q)
 371     -- & trace "Transparency Law"
 372   negLook (OptC (p :$>: _)) = negLook (OptComb p)
 373     -- & trace "NegLook Idempotence Law"
 374   negLook (OptComb x) = OptComb (negLook x)
 375
 376   eof = OptComb eof
 377 instance
 378   ( Applicable repr
 379   , Alternable repr
 380   , Lookable repr
 381   , Selectable repr
 382   , Matchable repr
 383   ) => Selectable (OptComb letName repr) where
 384   branch (OptC Empty) _ _ = empty
 385     -- & trace "Branch Absorption Law"
 386   branch b (OptC Empty) (OptC Empty) = b *> empty
 387     -- & trace "Branch Weakening Law"
 388   branch (OptC (Pure (trans -> lr))) l r =
 389     case H.value lr of
 390       Left value -> l <*> pure (trans H.ValueCode{..})
 391         where code = [|| case $$(H.code lr) of Left x -> x ||]
 392       Right value -> r <*> pure (trans H.ValueCode{..})
 393         where code = [|| case $$(H.code lr) of Right x -> x ||]
 394     -- & trace "Branch Pure Left/Right Law" $
 395   branch b (OptC (Pure (trans -> l))) (OptC (Pure (trans -> r))) =
 396     trans H.ValueCode{..} <$> b
 397     -- & trace "Branch Generalised Identity Law"
 398     where
 399     value = either (H.value l) (H.value r)
 400     code = [|| either $$(H.code l) $$(H.code r) ||]
 401   branch (OptC (x :*>: y)) p q =
 402     OptComb x *> branch (OptComb y) p q
 403     -- & trace "Interchange Law"
 404   branch b l (OptC Empty) =
 405     branch (pure (trans (H.ValueCode{..})) <*> b) empty l
 406     -- & trace "Negated Branch Law"
 407     where
 408     value = either Right Left
 409     code = [||either Right Left||]
 410   branch (OptC (Branch b (Comb Empty) (Comb (Pure (trans -> lr))))) (OptC Empty) br =
 411     branch (pure (trans H.ValueCode{..}) <*> OptComb b) empty br
 412     -- & trace "Branch Fusion Law"
 413     where
 414     value Left{} = Left ()
 415     value (Right r) = case H.value lr r of
 416                         Left _ -> Left ()
 417                         Right rr -> Right rr
 418     code = [|| \case Left{} -> Left ()
 419                      Right r -> case $$(H.code lr) r of
 420                                   Left _ -> Left ()
 421                                   Right rr -> Right rr ||]
 422   branch (OptComb b) (OptComb l) (OptComb r) =
 423     OptComb (branch b l r)
 424 instance
 425   ( Applicable repr
 426   , Alternable repr
 427   , Lookable repr
 428   , Selectable repr
 429   , Matchable repr
 430   ) => Matchable (OptComb letName repr) where
 431   conditional (OptC Empty) _ _ d = d
 432     -- & trace "Conditional Absorption Law"
 433   conditional p _ qs (OptC Empty)
 434     | Foldable.all (\case { OptC Empty -> True; _ -> False }) qs = p *> empty
 435       -- & trace "Conditional Weakening Law"
 436   conditional a _ps bs (OptC Empty)
 437     | Foldable.all (\case { OptC Empty -> True; _ -> False }) bs = a *> empty
 438       -- & trace "Conditional Weakening Law"
 439   conditional (OptC (Pure (trans -> a))) ps bs d =
 440     Foldable.foldr (\(trans -> p, b) next ->
 441       if H.value p (H.value a) then b else next
 442     ) d (List.zip ps bs)
 443     -- & trace "Conditional Pure Law"
 444   conditional (OptComb a) ps bs (OptComb d) =
 445     OptComb (conditional a ps (unOptComb Functor.<$> bs) d)
 446 instance
 447   (Letable letName repr, Typeable letName) =>
 448   Letable letName (OptComb letName repr) where
 449   def n (OptComb x) = OptComb (def n x)
 450   ref isRec n = OptComb (ref isRec n)
 451 instance
 452   Foldable repr =>
 453   Foldable (OptComb letName repr) where
 454   chainPre (OptComb f) (OptComb x) = OptComb (chainPre f x)
 455   chainPost (OptComb x) (OptComb f) = OptComb (chainPost x f)
 456 instance
 457   (Satisfiable tok repr, Typeable tok) =>
 458   Satisfiable tok (OptComb letName repr) where
 459   satisfy es p = OptComb (satisfy es p)