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