]> Git — Sourcephile - haskell/symantic-parser.git/blob - src/Symantic/Parser/Grammar/Optimize.hs
remove useless benchmarks
[haskell/symantic-parser.git] / src / Symantic / Parser / Grammar / Optimize.hs
1 {-# LANGUAGE PatternSynonyms #-} -- For Comb
2 {-# LANGUAGE TemplateHaskell #-} -- For branch
3 {-# LANGUAGE ViewPatterns #-} -- For unSomeComb
4 {-# OPTIONS_GHC -fno-warn-orphans #-} -- For MakeLetName TH.Name
5 -- | Bottom-up optimization of 'Comb'inators,
6 -- reexamining downward as needed after each optimization.
7 module Symantic.Parser.Grammar.Optimize where
8
9 import Data.Bool (Bool(..))
10 import Data.Either (Either(..), either)
11 import Data.Eq (Eq(..))
12 import Data.Function (($), (.))
13 import Data.Kind (Constraint)
14 import Data.Maybe (Maybe(..))
15 import Data.Set (Set)
16 import Data.Functor.Identity (Identity(..))
17 import Data.Functor.Product (Product(..))
18 import Type.Reflection (Typeable, typeRep, eqTypeRep, (:~~:)(..))
19 import qualified Data.Foldable as Foldable
20 import qualified Data.Functor as Functor
21 import qualified Data.List as List
22
23 import Symantic.Parser.Grammar.Combinators hiding (code)
24 import Symantic.Parser.Grammar.Production
25 import Symantic.Univariant.Letable
26 import Symantic.Univariant.Trans
27 import qualified Symantic.Parser.Grammar.Production as Prod
28 import qualified Symantic.Univariant.Data as H
29 import qualified Symantic.Univariant.Lang as H
30
31 {-
32 import Data.Function (($), flip)
33 import Debug.Trace (trace)
34
35 (&) = flip ($)
36 infix 0 &
37 -}
38
39 -- * Type 'OptimizeGrammar'
40 type OptimizeGrammar = SomeComb
41
42 optimizeGrammar ::
43 Trans (SomeComb repr) repr =>
44 SomeComb repr a -> repr a
45 optimizeGrammar = trans
46
47 -- * Data family 'Comb'
48 -- | 'Comb'inators of the 'Grammar'.
49 -- This is an extensible data-type.
50 data family Comb
51 (comb :: ReprComb -> Constraint)
52 :: ReprComb -> ReprComb
53
54 -- | Convenient utility to pattern-match a 'SomeComb'.
55 pattern Comb :: Typeable comb => Comb comb repr a -> SomeComb repr a
56 pattern Comb x <- (unSomeComb -> Just x)
57
58 -- ** Type 'SomeComb'
59 -- | Some 'Comb'inator existentialized over the actual combinator symantic class.
60 -- Useful to handle a list of 'Comb'inators
61 -- without requiring impredicative quantification.
62 -- Must be used by pattern-matching
63 -- on the 'SomeComb' data-constructor,
64 -- to bring the constraints in scope.
65 --
66 -- The optimizations are directly applied within it,
67 -- to avoid introducing an extra newtype,
68 -- this also give a more understandable code.
69 data SomeComb repr a =
70 forall comb.
71 (Trans (Comb comb repr) repr, Typeable comb) =>
72 SomeComb (Comb comb repr a)
73
74 instance Trans (SomeComb repr) repr where
75 trans (SomeComb x) = trans x
76
77 -- | @(unSomeComb c :: 'Maybe' ('Comb' comb repr a))@
78 -- extract the data-constructor from the given 'SomeComb'
79 -- iif. it belongs to the @('Comb' comb repr a)@ data-instance.
80 unSomeComb ::
81 forall comb repr a.
82 Typeable comb =>
83 SomeComb repr a -> Maybe (Comb comb repr a)
84 unSomeComb (SomeComb (c::Comb c repr a)) =
85 case typeRep @comb `eqTypeRep` typeRep @c of
86 Just HRefl -> Just c
87 Nothing -> Nothing
88
89 -- CombAlternable
90 data instance Comb CombAlternable repr a where
91 Alt :: Exception -> SomeComb repr a -> SomeComb repr a -> Comb CombAlternable repr a
92 Empty :: Comb CombAlternable repr a
93 Failure :: SomeFailure -> Comb CombAlternable repr a
94 Throw :: ExceptionLabel -> Comb CombAlternable repr a
95 Try :: SomeComb repr a -> Comb CombAlternable repr a
96 instance CombAlternable repr => Trans (Comb CombAlternable repr) repr where
97 trans = \case
98 Alt exn x y -> alt exn (trans x) (trans y)
99 Empty -> empty
100 Failure sf -> failure sf
101 Throw exn -> throw exn
102 Try x -> try (trans x)
103 instance
104 ( CombAlternable repr
105 , CombApplicable repr
106 , CombLookable repr
107 , CombMatchable repr
108 , CombSelectable repr
109 ) => CombAlternable (SomeComb repr) where
110 empty = SomeComb Empty
111 failure sf = SomeComb (Failure sf)
112
113 alt _exn p@(Comb Pure{}) _ = p
114 -- & trace "Left Catch Law"
115 alt _exn (Comb Empty) u = u
116 -- & trace "Left Neutral Law"
117 alt _exn u (Comb Empty) = u
118 -- & trace "Right Neutral Law"
119 alt exn (Comb (Alt exn' u v)) w | exn' == exn = u <|> (v <|> w)
120 -- See Lemma 1 (Associativity of choice for labeled PEGs)
121 -- in https://doi.org/10.1145/2851613.2851750
122 -- & trace "Associativity Law"
123 alt exn (Comb (Look p)) (Comb (Look q)) = look (alt exn (try p) q)
124 -- & trace "Distributivity Law"
125 alt exn x y = SomeComb (Alt exn x y)
126
127 throw exn = SomeComb (Throw exn)
128
129 try (Comb (p :$>: x)) = try p $> x
130 -- & trace "Try Interchange Law"
131 try (Comb (f :<$>: p)) = f <$> try p
132 -- & trace "Try Interchange Law"
133 try x = SomeComb (Try x)
134
135 -- CombApplicable
136 data instance Comb CombApplicable repr a where
137 Pure :: Production a -> Comb CombApplicable repr a
138 (:<*>:) :: SomeComb repr (a -> b) -> SomeComb repr a -> Comb CombApplicable repr b
139 (:<*:) :: SomeComb repr a -> SomeComb repr b -> Comb CombApplicable repr a
140 (:*>:) :: SomeComb repr a -> SomeComb repr b -> Comb CombApplicable repr b
141 infixl 4 :<*>:, :<*:, :*>:
142 pattern (:<$>:) :: Production (a -> b) -> SomeComb repr a -> Comb CombApplicable repr b
143 pattern t :<$>: x <- Comb (Pure t) :<*>: x
144 pattern (:$>:) :: SomeComb repr a -> Production b -> Comb CombApplicable repr b
145 pattern x :$>: t <- x :*>: Comb (Pure t)
146 instance CombApplicable repr => Trans (Comb CombApplicable repr) repr where
147 trans = \case
148 Pure x -> pure (optimizeProduction x)
149 f :<*>: x -> trans f <*> trans x
150 x :<*: y -> trans x <* trans y
151 x :*>: y -> trans x *> trans y
152 instance
153 ( CombApplicable repr
154 , CombAlternable repr
155 , CombLookable repr
156 , CombMatchable repr
157 , CombSelectable repr
158 ) => CombApplicable (SomeComb repr) where
159 pure = SomeComb . Pure
160 f <$> Comb (Branch b l r) =
161 branch b
162 ((H..) H..@ f <$> l)
163 ((H..) H..@ f <$> r)
164 -- & trace "Branch Distributivity Law"
165 f <$> Comb (Conditional a ps bs d) =
166 conditional a ps
167 ((f <$>) Functor.<$> bs)
168 (f <$> d)
169 -- & trace "Conditional Distributivity Law"
170 -- Being careful here to use (<*>),
171 -- instead of SomeComb (f <$> unOptComb x),
172 -- in order to apply the optimizations of (<*>).
173 f <$> x = pure f <*> x
174
175 x <$ u = u $> x
176 -- & trace "Commutativity Law"
177
178 Comb Empty <*> _ = empty
179 -- & trace "App Right Absorption Law"
180 u <*> Comb Empty = u *> empty
181 -- & trace "App Failure Weakening Law"
182 Comb (Pure f) <*> Comb (Pure x) = pure (f H..@ x)
183 -- & trace "Homomorphism Law"
184 {-
185 Comb (Pure f) <*> Comb (g :<$>: p) =
186 -- This is basically a shortcut,
187 -- it can be caught by one Composition Law
188 -- and two Homomorphism Law.
189 (H..) H..@ f H..@ g <$> p
190 -- & trace "Functor Composition Law"
191 -}
192 u <*> Comb (Pure x) = H.flip H..@ (H.$) H..@ x <$> u
193 -- & trace "Interchange Law"
194 u <*> Comb (v :<*>: w) = (((H..) <$> u) <*> v) <*> w
195 -- & trace "Composition Law"
196 Comb (u :*>: v) <*> w = u *> (v <*> w)
197 -- & trace "Reassociation Law 1"
198 u <*> Comb (v :<*: w) = (u <*> v) <* w
199 -- & trace "Reassociation Law 2"
200 u <*> Comb (v :$>: x) = (u <*> pure x) <* v
201 -- & trace "Reassociation Law 3"
202 p <*> Comb (NegLook q) =
203 (p <*> pure H.unit) <* negLook q
204 -- & trace "Absorption Law"
205 x <*> y = SomeComb (x :<*>: y)
206
207 Comb Empty *> _ = empty
208 -- & trace "App Right Absorption Law"
209 Comb (_ :<$>: p) *> q = p *> q
210 -- & trace "Right Absorption Law"
211 Comb Pure{} *> u = u
212 -- & trace "Identity Law"
213 Comb (u :$>: _) *> v = u *> v
214 -- & trace "Identity Law"
215 u *> Comb (v :*>: w) = (u *> v) *> w
216 -- & trace "Associativity Law"
217 x *> y = SomeComb (x :*>: y)
218
219 Comb Empty <* _ = empty
220 -- & trace "App Right Absorption Law"
221 u <* Comb Empty = u *> empty
222 -- & trace "App Failure Weakening Law"
223 p <* Comb (_ :<$>: q) = p <* q
224 -- & trace "Left Absorption Law"
225 u <* Comb Pure{} = u
226 -- & trace "Identity Law"
227 u <* Comb (v :$>: _) = u <* v
228 -- & trace "Identity Law"
229 Comb (u :<*: v) <* w = u <* (v <* w)
230 -- & trace "Associativity Law"
231 x <* y = SomeComb (x :<*: y)
232
233 -- CombFoldable
234 data instance Comb CombFoldable repr a where
235 ChainPreC :: SomeComb repr (a -> a) -> SomeComb repr a -> Comb CombFoldable repr a
236 ChainPostC :: SomeComb repr a -> SomeComb repr (a -> a) -> Comb CombFoldable repr a
237 instance CombFoldable repr => Trans (Comb CombFoldable repr) repr where
238 trans = \case
239 ChainPreC x y -> chainPre (trans x) (trans y)
240 ChainPostC x y -> chainPost (trans x) (trans y)
241 instance CombFoldable repr => CombFoldable (SomeComb repr) where
242 chainPre x = SomeComb . ChainPreC x
243 chainPost x = SomeComb . ChainPostC x
244
245 -- Letable
246 data instance Comb (Letable letName) repr a where
247 Shareable :: letName -> SomeComb repr a -> Comb (Letable letName) repr a
248 Ref :: Bool -> letName -> Comb (Letable letName) repr a
249 instance
250 Letable letName repr =>
251 Trans (Comb (Letable letName) repr) repr where
252 trans = \case
253 Shareable n x -> shareable n (trans x)
254 Ref isRec n -> ref isRec n
255 instance
256 (Letable letName repr, Typeable letName) =>
257 Letable letName (SomeComb repr) where
258 shareable n = SomeComb . Shareable n
259 ref isRec = SomeComb . Ref isRec
260
261 -- Letsable
262 data instance Comb (Letsable letName) repr a where
263 Lets :: LetBindings letName (SomeComb repr) ->
264 SomeComb repr a -> Comb (Letsable letName) repr a
265 instance
266 Letsable letName repr =>
267 Trans (Comb (Letsable letName) repr) repr where
268 trans = \case
269 Lets defs x -> lets ((\(SomeLet sub) -> SomeLet (trans sub)) Functor.<$> defs) (trans x)
270 instance
271 (Letsable letName repr, Typeable letName) =>
272 Letsable letName (SomeComb repr) where
273 lets defs = SomeComb . Lets defs
274
275 -- CombLookable
276 data instance Comb CombLookable repr a where
277 Look :: SomeComb repr a -> Comb CombLookable repr a
278 NegLook :: SomeComb repr a -> Comb CombLookable repr ()
279 Eof :: Comb CombLookable repr ()
280 instance CombLookable repr => Trans (Comb CombLookable repr) repr where
281 trans = \case
282 Look x -> look (trans x)
283 NegLook x -> negLook (trans x)
284 Eof -> eof
285 instance
286 ( CombAlternable repr
287 , CombApplicable repr
288 , CombLookable repr
289 , CombSelectable repr
290 , CombMatchable repr
291 ) => CombLookable (SomeComb repr) where
292 look p@(Comb Pure{}) = p
293 -- & trace "Pure Look Law"
294 look p@(Comb Empty) = p
295 -- & trace "Dead Look Law"
296 look (Comb (Look x)) = look x
297 -- & trace "Idempotence Law"
298 look (Comb (NegLook x)) = negLook x
299 -- & trace "Left Identity Law"
300 look (Comb (p :$>: x)) = look p $> x
301 -- & trace "Interchange Law"
302 look (Comb (f :<$>: p)) = f <$> look p
303 -- & trace "Interchange Law"
304 look x = SomeComb (Look x)
305
306 negLook (Comb Pure{}) = empty
307 -- & trace "Pure Negative-Look"
308 negLook (Comb Empty) = pure H.unit
309 -- & trace "Dead Negative-Look"
310 negLook (Comb (NegLook x)) = look (try x *> pure H.unit)
311 -- & trace "Double Negation Law"
312 negLook (Comb (Try x)) = negLook x
313 -- & trace "Zero Consumption Law"
314 negLook (Comb (Look x)) = negLook x
315 -- & trace "Right Identity Law"
316 negLook (Comb (Alt _exn (Comb (Try p)) q)) = negLook p *> negLook q
317 -- FIXME: see if this really holds for all exceptions.
318 -- & trace "Transparency Law"
319 negLook (Comb (p :$>: _)) = negLook p
320 -- & trace "NegLook Idempotence Law"
321 negLook x = SomeComb (NegLook x)
322
323 eof = SomeComb Eof
324
325 -- CombMatchable
326 data instance Comb CombMatchable repr a where
327 Conditional :: Eq a =>
328 SomeComb repr a ->
329 [Production (a -> Bool)] ->
330 [SomeComb repr b] ->
331 SomeComb repr b ->
332 Comb CombMatchable repr b
333 instance CombMatchable repr => Trans (Comb CombMatchable repr) repr where
334 trans = \case
335 Conditional a ps bs b ->
336 conditional (trans a)
337 (optimizeProduction Functor.<$> ps)
338 (trans Functor.<$> bs) (trans b)
339 instance
340 ( CombApplicable repr
341 , CombAlternable repr
342 , CombLookable repr
343 , CombSelectable repr
344 , CombMatchable repr
345 ) => CombMatchable (SomeComb repr) where
346 conditional (Comb Empty) _ _ d = d
347 -- & trace "Conditional Absorption Law"
348 conditional p _ qs (Comb Empty)
349 | Foldable.all (\case { Comb Empty -> True; _ -> False }) qs = p *> empty
350 -- & trace "Conditional Weakening Law"
351 conditional a _ps bs (Comb Empty)
352 | Foldable.all (\case { Comb Empty -> True; _ -> False }) bs = a *> empty
353 -- & trace "Conditional Weakening Law"
354 conditional (Comb (Pure a)) ps bs d =
355 Foldable.foldr (\(p, b) next ->
356 if runValue (p H..@ a) then b else next
357 ) d (List.zip ps bs)
358 -- & trace "Conditional Pure Law"
359 conditional a ps bs d = SomeComb (Conditional a ps bs d)
360
361 -- CombSatisfiable
362 data instance Comb (CombSatisfiable tok) repr a where
363 -- | To include the @('Set' 'SomeFailure')@ is a little kludge
364 -- it would be cleaner to be able to pattern-match
365 -- on @(alt exn (Comb 'Satisfy'{}) (Failure{}))@
366 -- when generating 'Program', but this is not easily possible then
367 -- because data types have already been converted back to class methods,
368 -- hence pattern-matching is no longer possible
369 -- (at least not without reintroducing data types).
370 SatisfyOrFail ::
371 CombSatisfiable tok repr =>
372 Set SomeFailure ->
373 Production (tok -> Bool) ->
374 Comb (CombSatisfiable tok) repr tok
375 instance
376 CombSatisfiable tok repr =>
377 Trans (Comb (CombSatisfiable tok) repr) repr where
378 trans = \case
379 SatisfyOrFail fs p -> satisfyOrFail fs (optimizeProduction p)
380 instance
381 (CombSatisfiable tok repr, Typeable tok) =>
382 CombSatisfiable tok (SomeComb repr) where
383 satisfyOrFail fs = SomeComb . SatisfyOrFail fs
384
385 -- CombSelectable
386 data instance Comb CombSelectable repr a where
387 Branch ::
388 SomeComb repr (Either a b) ->
389 SomeComb repr (a -> c) ->
390 SomeComb repr (b -> c) ->
391 Comb CombSelectable repr c
392 instance CombSelectable repr => Trans (Comb CombSelectable repr) repr where
393 trans = \case
394 Branch lr l r -> branch (trans lr) (trans l) (trans r)
395 instance
396 ( CombApplicable repr
397 , CombAlternable repr
398 , CombLookable repr
399 , CombSelectable repr
400 , CombMatchable repr
401 ) => CombSelectable (SomeComb repr) where
402 branch (Comb Empty) _ _ = empty
403 -- & trace "Branch Absorption Law"
404 branch b (Comb Empty) (Comb Empty) = b *> empty
405 -- & trace "Branch Weakening Law"
406 branch (Comb (Pure lr)) l r =
407 case runValue lr of
408 Left value -> l <*> pure (Pair v c)
409 where
410 v = H.SomeData $ H.Var $ Identity value
411 c = H.SomeData $ H.Var
412 [|| case $$(runCode lr) of Left x -> x ||]
413 Right value -> r <*> pure (Pair v c)
414 where
415 v = H.SomeData $ H.Var $ Identity value
416 c = H.SomeData $ H.Var
417 [|| case $$(runCode lr) of Right x -> x ||]
418 -- & trace "Branch Pure Either Law"
419 branch b (Comb (Pure l)) (Comb (Pure r)) =
420 Pair v c <$> b
421 -- & trace "Branch Generalised Identity Law"
422 where
423 v = H.SomeData $ H.Var $ Identity $ either (runValue l) (runValue r)
424 c = H.SomeData $ H.Var [|| either $$(runCode l) $$(runCode r) ||]
425 branch (Comb (x :*>: y)) p q = x *> branch y p q
426 -- & trace "Interchange Law"
427 branch b l (Comb Empty) =
428 branch (pure (Pair v c) <*> b) empty l
429 -- & trace "Negated Branch Law"
430 where
431 v = H.SomeData $ H.Var $ Identity $ either Right Left
432 c = H.SomeData $ H.Var $ [||either Right Left||]
433 branch (Comb (Branch b (Comb Empty) (Comb (Pure lr)))) (Comb Empty) br =
434 branch (pure (Pair v c) <*> b) empty br
435 -- & trace "Branch Fusion Law"
436 where
437 v = H.SomeData $ H.Var $ Identity $ \case
438 Left{} -> Left ()
439 Right r ->
440 case runValue lr r of
441 Left{} -> Left ()
442 Right rr -> Right rr
443 c = H.SomeData $ H.Var
444 [|| \case Left{} -> Left ()
445 Right r -> case $$(runCode lr) r of
446 Left{} -> Left ()
447 Right rr -> Right rr ||]
448 branch b l r = SomeComb (Branch b l r)