src/Symantic/Parser/Grammar/Optimizations.hs

   1 {-# LANGUAGE PatternSynonyms #-}
   2 {-# LANGUAGE TemplateHaskell #-}
   3 {-# LANGUAGE ViewPatterns #-}
   4 {-# LANGUAGE UndecidableInstances #-}
   5 module Symantic.Parser.Grammar.Optimizations 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 qualified Prelude as Pre
  12 import Data.String (String)
  13
  14 import System.IO (IO)
  15 import Symantic.Base.Univariant
  16 import Symantic.Parser.Grammar.Combinators
  17 import Symantic.Parser.Grammar.Observations
  18 import Symantic.Parser.Staging hiding (Haskell(..))
  19 import qualified Symantic.Parser.Staging as Hask
  20 -- import qualified Language.Haskell.TH.Syntax as TH
  21
  22 -- * Type 'Comb'
  23 data Comb a where
  24   Pure :: Hask.Haskell a -> Comb a
  25   Satisfy :: Hask.Haskell (Char -> Bool) -> Comb Char
  26   Item :: Comb Char
  27   Try :: Comb a -> Comb a
  28   Look :: Comb a -> Comb a
  29   NegLook :: Comb a -> Comb ()
  30   (:<*>) :: Comb (a -> b) -> Comb a -> Comb b
  31   (:<|>) :: Comb a -> Comb a -> Comb a
  32   Empty :: Comb a
  33   Branch :: Comb (Either a b) -> Comb (a -> c) -> Comb (b -> c) -> Comb c
  34   Match :: Eq a => [Hask.Haskell (a -> Bool)] -> [Comb b] -> Comb a -> Comb b -> Comb b
  35   ChainPre :: Comb (a -> a) -> Comb a -> Comb a
  36   ChainPost :: Comb a -> Comb (a -> a) -> Comb a
  37   Def :: String -> Comb a -> Comb a
  38   Ref :: Bool -> String -> Comb a
  39
  40 pattern (:<$>) :: Hask.Haskell (a -> b) -> Comb a -> Comb b
  41 pattern (:$>) :: Comb a -> Hask.Haskell b -> Comb b
  42 pattern (:<$) :: Hask.Haskell a -> Comb b -> Comb a
  43 pattern (:*>) :: Comb a -> Comb b -> Comb b
  44 pattern (:<*) :: Comb a -> Comb b -> Comb a
  45 pattern x :<$> p = Pure x :<*> p
  46 pattern p :$> x = p :*> Pure x
  47 pattern x :<$ p = Pure x :<* p
  48 pattern x :<* p = Hask.Const :<$> x :<*> p
  49 pattern p :*> x = Hask.Id :<$ p :<*> x
  50
  51 infixl 3 :<|>
  52 infixl 4 :<*>, :<*, :*>
  53 infixl 4 :<$>, :<$, :$>
  54
  55 instance Applicable Comb where
  56   pure = Pure
  57   (<*>) = (:<*>)
  58 instance Alternable Comb where
  59   (<|>) = (:<|>)
  60   empty = Empty
  61   try = Try
  62 instance Selectable Comb where
  63   branch = Branch
  64 instance Matchable Comb where
  65   conditional = Match
  66 instance Foldable Comb where
  67   chainPre = ChainPre
  68   chainPost = ChainPost
  69 instance Charable Comb where
  70   satisfy = Satisfy
  71 instance Lookable Comb where
  72   look = Look
  73   negLook = NegLook
  74 instance Sharable Comb where
  75   def = Def
  76   ref = Ref
  77 instance
  78   ( Applicable repr
  79   , Alternable repr
  80   , Selectable repr
  81   , Foldable repr
  82   , Charable repr
  83   , Lookable repr
  84   , Matchable repr
  85   , Sharable repr
  86   ) =>
  87   Symantic Comb repr where
  88   sym = \case
  89     Pure a -> pure a
  90     Satisfy p -> satisfy p
  91     Item -> item
  92     Try x -> try (sym x)
  93     Look x -> look (sym x)
  94     NegLook x -> negLook (sym x)
  95     x :<*> y -> sym x <*> sym y
  96     x :<|> y -> sym x <|> sym y
  97     Empty -> empty
  98     Branch lr l r -> branch (sym lr) (sym l) (sym r)
  99     Match cs bs a b -> conditional cs (sym Pre.<$> bs) (sym a) (sym b)
 100     ChainPre x y -> chainPre (sym x) (sym y)
 101     ChainPost x y -> chainPost (sym x) (sym y)
 102     Def n x -> def n (sym x)
 103     Ref r n -> ref r n
 104 {-
 105 type instance Unlift Comb = repr
 106 instance
 107   ( Applicable repr
 108   , Alternable repr
 109   , Selectable repr
 110   , Foldable repr
 111   , Charable repr
 112   , Lookable repr
 113   , Matchable repr
 114   , Sharable repr
 115   ) => Unliftable Comb where
 116   unlift = \case
 117     Pure a -> pure a
 118     Satisfy p -> satisfy p
 119     Item -> item
 120     Try x -> try (unlift x)
 121     Look x -> look (unlift x)
 122     NegLook x -> negLook (unlift x)
 123     x :<*> y -> unlift x <*> unlift y
 124     x :<|> y -> unlift x <|> unlift y
 125     Empty -> empty
 126     Branch lr l r -> branch (unlift lr) (unlift l) (unlift r)
 127     Match cs bs a b -> conditional cs (unlift Pre.<$> bs) (unlift a) (unlift b)
 128     ChainPre x y -> chainPre (unlift x) (unlift y)
 129     ChainPost x y -> chainPost (unlift x) (unlift y)
 130     Ref{..} -> let_ let_rec let_name
 131
 132 unComb ::
 133   ( Applicable repr
 134   , Alternable repr
 135   , Selectable repr
 136   , Foldable repr
 137   , Charable repr
 138   , Lookable repr
 139   , Matchable repr
 140   , Sharable repr
 141   ) => Comb repr a -> repr a
 142 unComb = unlift
 143 -}
 144
 145 optComb :: Comb a -> Comb a
 146 optComb = \case
 147   Def n x -> Def n (optComb x)
 148   -- Applicable Right Absorption Law
 149   Empty :<*> _ -> Empty
 150   Empty  :*> _ -> Empty
 151   Empty :<*  _ -> Empty
 152   -- Applicable Failure Weakening Law
 153   u :<*> Empty -> optComb (u :*> Empty)
 154   u :<*  Empty -> optComb (u :*> Empty)
 155   -- Branch Absorption Law
 156   Branch Empty _ _ -> empty
 157   -- Branch Weakening Law
 158   Branch b Empty Empty -> optComb (b :*> Empty)
 159
 160   -- Applicable Identity Law
 161   Hask.Id :<$> x -> x
 162   -- Flip const optimisation
 163   Hask.Flip Hask.:@ Hask.Const :<$> u -> optComb (u :*> Pure Hask.Id)
 164   -- Homomorphism Law
 165   f :<$> Pure x -> Pure (f Hask.:@ x)
 166   -- Functor Composition Law
 167   -- (a shortcut that could also have been be caught
 168   -- by the Composition Law and Homomorphism law)
 169   f :<$> (g :<$> p) -> optComb ((Hask.:.) Hask.:@ f Hask.:@ g :<$> p)
 170   -- Composition Law
 171   u :<*> (v :<*> w) -> optComb (optComb (optComb ((Hask.:.) :<$> u) :<*> v) :<*> w)
 172   -- Definition of *>
 173   Hask.Flip Hask.:@ Hask.Const :<$> p :<*> q -> p :*> q
 174   -- Definition of <*
 175   Hask.Const :<$> p :<*> q -> p :<* q
 176   -- Reassociation Law 1
 177   (u :*> v) :<*> w -> optComb (u :*> optComb (v :<*> w))
 178   -- Interchange Law
 179   u :<*> Pure x -> optComb (Hask.Flip Hask.:@ (Hask.:$) Hask.:@ x :<$> u)
 180   -- Right Absorption Law
 181   (_ :<$> p) :*> q -> p :*> q
 182   -- Left Absorption Law
 183   p :<* (_ :<$> q) -> p :<* q
 184   -- Reassociation Law 2
 185   u :<*> (v :<* w) -> optComb (optComb (u :<*> v) :<* w)
 186   -- Reassociation Law 3
 187   u :<*> (v :$> x) -> optComb (optComb (u :<*> Pure x) :<* v)
 188
 189   -- Left Catch Law
 190   p@Pure{} :<|> _ -> p
 191   -- Left Neutral Law
 192   Empty :<|> u -> u
 193   -- Right Neutral Law
 194   u :<|> Empty -> u
 195   -- Associativity Law
 196   (u :<|> v) :<|> w -> u :<|> optComb (v :<|> w)
 197
 198   -- Identity law
 199   Pure _ :*> u -> u
 200   -- Identity law
 201   (u :$> _) :*> v -> u :*> v
 202   -- Associativity Law
 203   u :*> (v :*> w) -> optComb (optComb (u :*> v) :*> w)
 204   -- Identity law
 205   u :<* Pure _ -> u
 206   -- Identity law
 207   u :<* (v :$> _) -> optComb (u :<* v)
 208   -- Commutativity Law
 209   x :<$ u -> optComb (u :$> x)
 210   -- Associativity Law
 211   (u :<* v) :<* w -> optComb (u :<* optComb (v :<* w))
 212
 213   -- Pure lookahead
 214   Look p@Pure{} -> p
 215   -- Dead lookahead
 216   Look p@Empty -> p
 217   -- Pure negative-lookahead
 218   NegLook Pure{} -> Empty
 219
 220   -- Dead negative-lookahead
 221   NegLook Empty -> Pure Hask.unit
 222   -- Double Negation Law
 223   NegLook (NegLook p) -> optComb (Look (Try p) :*> Pure Hask.unit)
 224   -- Zero Consumption Law
 225   NegLook (Try p) -> optComb (NegLook p)
 226   -- Idempotence Law
 227   Look (Look p) -> Look p
 228   -- Right Identity Law
 229   NegLook (Look p) -> optComb (NegLook p)
 230
 231   -- Left Identity Law
 232   Look (NegLook p) -> NegLook p
 233   -- Transparency Law
 234   NegLook (Try p :<|> q) -> optComb (optComb (NegLook p) :*> optComb (NegLook q))
 235   -- Distributivity Law
 236   Look p :<|> Look q -> optComb (Look (optComb (Try p :<|> q)))
 237   -- Interchange Law
 238   Look (p :$> x) -> optComb (optComb (Look p) :$> x)
 239   -- Interchange law
 240   Look (f :<$> p) -> optComb (f :<$> optComb (Look p))
 241   -- Absorption Law
 242   p :<*> NegLook q -> optComb (optComb (p :<*> Pure Hask.unit) :<* NegLook q)
 243   -- Idempotence Law
 244   NegLook (p :$> _) -> optComb (NegLook p)
 245   -- Idempotence Law
 246   NegLook (_ :<$> p) -> optComb (NegLook p)
 247   -- Interchange Law
 248   Try (p :$> x) -> optComb (optComb (Try p) :$> x)
 249   -- Interchange law
 250   Try (f :<$> p) -> optComb (f :<$> optComb (Try p))
 251
 252   -- pure Left/Right laws
 253   Branch (Pure (unlift -> lr)) l r ->
 254     case getValue lr of
 255      Left v -> optComb (l :<*> Pure (Hask.Haskell (ValueCode (Value v) c)))
 256       where c = Code [|| case $$(getCode lr) of Left x -> x ||]
 257      Right v -> optComb (r :<*> Pure (Hask.Haskell (ValueCode (Value v) c)))
 258       where c = Code [|| case $$(getCode lr) of Right x -> x ||]
 259   -- Generalised Identity law
 260   Branch b (Pure (unlift -> l)) (Pure (unlift -> r)) ->
 261     optComb (Hask.Haskell (ValueCode v c) :<$> b)
 262     where
 263     v = Value (either (getValue l) (getValue r))
 264     c = Code [|| either $$(getCode l) $$(getCode r) ||]
 265   -- Interchange law
 266   Branch (x :*> y) p q ->
 267     optComb (x :*> optComb (Branch y p q))
 268   -- Negated Branch law
 269   Branch b l Empty ->
 270     Branch (Pure (Hask.Haskell (ValueCode v c)) :<*> b) Empty l
 271     where
 272     v = Value (either Right Left)
 273     c = Code [||either Right Left||]
 274   -- Branch Fusion law
 275   Branch (Branch b Empty (Pure (unlift -> lr))) Empty br ->
 276     optComb (Branch (optComb (Pure (Hask.Haskell (ValueCode (Value v) c)) :<*> b)) Empty br)
 277     where
 278     v Left{} = Left ()
 279     v (Right r) = case getValue lr r of
 280                    Left _ -> Left ()
 281                    Right rr -> Right rr
 282     c = Code [|| \case Left{} -> Left ()
 283                        Right r -> case $$(getCode lr) r of
 284                                    Left _ -> Left ()
 285                                    Right rr -> Right rr ||]
 286   -- Distributivity Law
 287   f :<$> Branch b l r -> optComb (Branch b (optComb ((Hask..@) (Hask..) f :<$> l))
 288                                            (optComb ((Hask..@) (Hask..) f :<$> r)))
 289
 290   x -> x
 291
 292
 293 type instance Unlift (Ref repr) = repr
 294 instance Liftable (Ref repr) where
 295   lift x = let n = x in LetNode (makeParserName n) n
 296   lift1 f x = let n = f (let_sub x) in LetNode (makeParserName n) n
 297   lift2 f x y = let n = f (let_sub x) (let_sub y) in LetNode (makeParserName n) n
 298   lift3 f x y z = let n = f (let_sub x) (let_sub y) (let_sub z) in LetNode (makeParserName n) n
 299 instance Applicable repr => Applicable (Ref repr)
 300
 301 data Ref repr a where
 302   LetNode :: { let_id :: IO ParserName, let_sub :: repr a } -> Ref repr a
 303   --LetLeaf :: repr a -> Ref repr a
 304 {-
 305 instance Liftable (Ref (Comb repr)) where
 306   lift c = case c of
 307     Pure a -> LetLeaf c
 308   lift1 f x = case x of
 309     LetLeaf l -> LetLeaf (f l)
 310     LetNode l -> LetLeaf (f l)
 311 instance Applicable (Ref (Comb repr)) where
 312   pure a = LetLeaf (pure a)
 313   x <*> y = LetNode (mkParserName x) (<*>
 314 instance Applicable (Comb (Ref repr)) where
 315   pure a = pure a
 316   x <*> y = LetNode (mkParserName x) (:<*>
 317
 318 -}