]> Git — Sourcephile - haskell/symantic-parser.git/blob - src/Symantic/Parser/Grammar/Optimize.hs
machine: open the Instr data-type
[haskell/symantic-parser.git] / 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.Function ((.))
11 import qualified Data.Functor as Functor
12 import qualified Data.Foldable as Foldable
13 import qualified Data.List as List
14 import qualified Language.Haskell.TH.Syntax as TH
15
16 import Symantic.Parser.Grammar.Combinators as Comb
17 import Symantic.Parser.Haskell ()
18 import Symantic.Univariant.Letable
19 import Symantic.Univariant.Trans
20 import qualified Symantic.Parser.Haskell as H
21
22 -- import Debug.Trace (trace)
23
24 -- * Type 'Comb'
25 -- | Pattern-matchable 'Comb'inators of the grammar.
26 -- @(repr)@ is not strictly necessary since it's only a phantom type
27 -- (no constructor use it as a value), but having it:
28 --
29 -- 1. emphasizes that those 'Comb'inators will be 'trans'formed again
30 -- (eg. in 'ViewGrammar' or 'Instr'uctions).
31 --
32 -- 2. Avoid overlapping instances between
33 -- @('Trans' ('Comb' repr) repr)@ and
34 -- @('Trans' ('Comb' repr) ('OptimizeGrammar' letName repr))@
35 data Comb repr a where
36 Pure :: TermGrammar a -> Comb repr a
37 Satisfy ::
38 Satisfiable repr tok =>
39 [ErrorItem tok] ->
40 TermGrammar (tok -> Bool) -> Comb repr tok
41 Item :: Satisfiable repr tok => Comb repr tok
42 Try :: Comb repr a -> Comb repr a
43 Look :: Comb repr a -> Comb repr a
44 NegLook :: Comb repr a -> Comb repr ()
45 Eof :: Comb repr ()
46 (:<*>) :: Comb repr (a -> b) -> Comb repr a -> Comb repr b
47 (:<*) :: Comb repr a -> Comb repr b -> Comb repr a
48 (:*>) :: Comb repr a -> Comb repr b -> Comb repr b
49 (:<|>) :: Comb repr a -> Comb repr a -> Comb repr a
50 Empty :: Comb repr a
51 Branch ::
52 Comb repr (Either a b) ->
53 Comb repr (a -> c) -> Comb repr (b -> c) -> Comb repr c
54 Match :: Eq a =>
55 Comb repr a ->
56 [TermGrammar (a -> Bool)] ->
57 [Comb repr b] -> Comb repr b -> Comb repr b
58 ChainPre :: Comb repr (a -> a) -> Comb repr a -> Comb repr a
59 ChainPost :: Comb repr a -> Comb repr (a -> a) -> Comb repr a
60 Def :: TH.Name -> Comb repr a -> Comb repr a
61 Ref :: Bool -> TH.Name -> Comb repr a
62 infixl 3 :<|>
63 infixl 4 :<*>
64 infixl 4 :<*, :*>
65
66 pattern (:<$>) :: TermGrammar (a -> b) -> Comb repr a -> Comb repr b
67 pattern x :<$> p = Pure x :<*> p
68 pattern (:$>) :: Comb repr a -> TermGrammar b -> Comb repr b
69 pattern (:<$) :: TermGrammar a -> Comb repr b -> Comb repr a
70 pattern p :$> x = p :*> Pure x
71 pattern x :<$ p = Pure x :<* p
72 infixl 4 :<$>, :<$, :$>
73
74 {-
75 pattern (:*>) :: Comb repr a -> Comb repr b -> Comb repr b
76 pattern (:<*) :: Comb repr a -> Comb repr b -> Comb repr a
77 pattern x :<* p = H.Const :<$> x :<*> p
78 pattern p :*> x = H.Id :<$ p :<*> x
79 x .<* p = H.const :<$> x :<*> p
80 x .<$ p = Pure x .<* p
81 p .*> x = H.id .<$ p :<*> x
82 p .$> x = p .*> Pure x
83 -}
84
85 {-
86 pattern (:<$>) :: Defunc (a -> b) -> Fix Combinator a -> Combinator (Fix Combinator) b
87 pattern f :<$> p = (Pure f) :<*> p
88 pattern (:$>) :: Fix Combinator a -> Defunc b -> Combinator (Fix Combinator) b
89 pattern p :$> x = p :*> (Pure x)
90 pattern (:<$) :: Defunc a -> Fix Combinator b -> Combinator (Fix Combinator) a
91 pattern x :<$ p = (Pure x) :<* p
92 -}
93
94
95 instance Applicable (Comb repr) where
96 pure = Pure
97 (<*>) = (:<*>)
98 (<*) = (:<*)
99 (*>) = (:*>)
100 instance Alternable (Comb repr) where
101 (<|>) = (:<|>)
102 empty = Empty
103 try = Try
104 instance Selectable (Comb repr) where
105 branch = Branch
106 instance Matchable (Comb repr) where
107 conditional = Match
108 instance Foldable (Comb repr) where
109 chainPre = ChainPre
110 chainPost = ChainPost
111 instance Satisfiable repr tok => Satisfiable (Comb repr) tok where
112 satisfy = Satisfy
113 instance Lookable (Comb repr) where
114 look = Look
115 negLook = NegLook
116 eof = Eof
117 instance Letable TH.Name (Comb repr) where
118 def = Def
119 ref = Ref
120 instance MakeLetName TH.Name where
121 makeLetName _ = TH.qNewName "name"
122
123 -- Pattern-matchable 'Comb'inators keep enough structure
124 -- to have some of the symantics producing them interpreted again
125 -- (eg. after being modified by 'optimizeGrammar').
126 type instance Output (Comb repr) = repr
127 instance
128 ( Applicable repr
129 , Alternable repr
130 , Selectable repr
131 , Foldable repr
132 , Lookable repr
133 , Matchable repr
134 , Letable TH.Name repr
135 ) => Trans (Comb repr) repr where
136 trans = \case
137 Pure a -> pure (H.optimizeTerm a)
138 Satisfy es p -> satisfy es p
139 Item -> item
140 Try x -> try (trans x)
141 Look x -> look (trans x)
142 NegLook x -> negLook (trans x)
143 Eof -> eof
144 x :<* y -> trans x <* trans y
145 x :*> y -> trans x *> trans y
146 x :<*> y -> trans x <*> trans y
147 x :<|> y -> trans x <|> trans y
148 Empty -> empty
149 Branch lr l r -> branch (trans lr) (trans l) (trans r)
150 Match a ps bs b -> conditional (trans a) ps (trans Functor.<$> bs) (trans b)
151 ChainPre x y -> chainPre (trans x) (trans y)
152 ChainPost x y -> chainPost (trans x) (trans y)
153 Def n x -> def n (trans x)
154 Ref r n -> ref r n
155
156 {-
157 -- * Type 'OptimizeHaskell'
158 newtype OptimizeHaskell letName repr a =
159 OptimizeHaskell { unOptimizeHaskell :: Comb repr a }
160 instance
161 Letable letName (Comb repr) =>
162 Letable letName (OptimizeGrammar letName repr)
163 instance Comb.Applicable (OptimizeGrammar letName repr) where
164 pure a = pure (optimizeTerm a)
165 instance Comb.Alternable (OptimizeGrammar letName repr)
166 instance Comb.Satisfiable repr tok =>
167 Comb.Satisfiable (OptimizeGrammar letName repr) tok
168 instance Comb.Selectable (OptimizeGrammar letName repr)
169 instance Comb.Matchable (OptimizeGrammar letName repr)
170 instance Comb.Lookable (OptimizeGrammar letName repr)
171 instance Comb.Foldable (OptimizeGrammar letName repr)
172 -}
173
174 -- * Type 'OptimizeGrammar'
175 -- | Bottom-up application of 'optimizeCombNode'.
176 newtype OptimizeGrammar letName repr a =
177 OptimizeGrammar { unOptimizeGrammar :: Comb repr a }
178
179 optimizeGrammar ::
180 Trans (OptimizeGrammar TH.Name repr) repr =>
181 OptimizeGrammar TH.Name repr a -> repr a
182 optimizeGrammar = trans
183 instance
184 Trans (Comb repr) repr =>
185 Trans (OptimizeGrammar letName repr) repr where
186 trans = trans . unOptimizeGrammar
187
188 type instance Output (OptimizeGrammar _letName repr) = Comb repr
189 instance Trans (OptimizeGrammar letName repr) (Comb repr) where
190 trans = unOptimizeGrammar
191 instance Trans (Comb repr) (OptimizeGrammar letName repr) where
192 trans = OptimizeGrammar . optimizeCombNode
193 instance Trans1 (Comb repr) (OptimizeGrammar letName repr)
194 instance Trans2 (Comb repr) (OptimizeGrammar letName repr)
195 instance Trans3 (Comb repr) (OptimizeGrammar letName repr)
196
197 instance
198 Letable letName (Comb repr) =>
199 Letable letName (OptimizeGrammar letName repr) where
200 -- Disable useless calls to 'optimizeCombNode'
201 -- because 'Def' or 'Ref' have no matching in it.
202 def n = OptimizeGrammar . def n . unOptimizeGrammar
203 ref r n = OptimizeGrammar (ref r n)
204 instance Comb.Applicable (OptimizeGrammar letName repr)
205 instance Comb.Alternable (OptimizeGrammar letName repr)
206 instance Comb.Satisfiable repr tok =>
207 Comb.Satisfiable (OptimizeGrammar letName repr) tok
208 instance Comb.Selectable (OptimizeGrammar letName repr)
209 instance Comb.Matchable (OptimizeGrammar letName repr)
210 instance Comb.Lookable (OptimizeGrammar letName repr)
211 instance Comb.Foldable (OptimizeGrammar letName repr)
212
213
214 optimizeCombNode :: Comb repr a -> Comb repr a
215
216 ----------------------------------------------
217 -- Destructive optimizations
218 ----------------------------------------------
219
220 optimizeCombNode (Empty :<*> _) =
221 -- trace "App Right Absorption Law" $
222 Empty
223 optimizeCombNode (u :<*> Empty) =
224 -- trace "App Failure Weakening Law" $
225 optimizeCombNode (u :*> Empty)
226 optimizeCombNode (Empty :*> _) =
227 -- trace "App Right Absorption Law" $
228 Empty
229 optimizeCombNode (Empty :<* _) =
230 -- trace "App Right Absorption Law" $
231 Empty
232 optimizeCombNode (u :<* Empty) =
233 -- trace "App Failure Weakening Law" $
234 optimizeCombNode (u :*> Empty)
235 optimizeCombNode (Branch Empty _ _) =
236 -- trace "Branch Absorption Law" $
237 Empty
238 optimizeCombNode (Branch b Empty Empty) =
239 -- trace "Branch Weakening Law" $
240 optimizeCombNode (b :*> Empty)
241 optimizeCombNode (Match Empty _ _ d) =
242 -- trace "Match Absorption Law" $
243 d
244 optimizeCombNode (Match p _ qs Empty)
245 | Foldable.all (\case {Empty -> True; _ -> False}) qs =
246 -- trace "Match Weakening Law" $
247 optimizeCombNode (p :*> Empty)
248
249
250 ----------------------------------------------
251 -- Applicative optimizations
252 ----------------------------------------------
253
254 {- Those laws require to pattern match on some singled-out pure constructors,
255 - but 'optimizeHaskellNode' is normalizing them using lambda abstractions
256 - and thus they will no longer match.
257
258 optimizeCombNode (H.Id :<$> u) =
259 -- trace "Identity Law" $
260 u
261 optimizeCombNode ((H.Flip H.:@ H.Const) :<$> u) =
262 -- trace "Flip Const Optimisation" $
263 optimizeCombNode (u :*> Pure H.id)
264 optimizeCombNode (((H.Flip H.:@ H.Const) :<$> p) :<*> q) =
265 -- trace "Definition of *>" $
266 p :*> q
267 optimizeCombNode ((H.Const :<$> p) :<*> q) =
268 -- trace "Definition of <*" $
269 p :<* q
270 -}
271 optimizeCombNode (f :<$> Pure x) =
272 -- trace "Homomorphism Law" $
273 Pure (f H..@ x)
274 optimizeCombNode (f :<$> (g :<$> p)) =
275 -- NOTE: This is basically a shortcut, it can be caught by the Composition Law and Homomorphism Law
276 -- trace "Functor Composition Law" $
277 optimizeCombNode ((H..) H..@ f H..@ g :<$> p)
278 optimizeCombNode (u :<*> (v :<*> w)) =
279 -- trace "Composition Law" $
280 optimizeCombNode (optimizeCombNode (optimizeCombNode ((H..) :<$> u) :<*> v) :<*> w)
281 optimizeCombNode ((u :*> v) :<*> w) =
282 -- trace "Reassociation Law 1" $
283 optimizeCombNode (u :*> (optimizeCombNode (v :<*> w)))
284 optimizeCombNode (u :<*> (Pure x)) =
285 -- trace "Interchange Law" $
286 optimizeCombNode (H.flip H..@ (H.$) H..@ x :<$> u)
287 optimizeCombNode ((_ :<$> p) :*> q) =
288 -- trace "Right Absorption Law" $
289 p :*> q
290 optimizeCombNode (p :<* (_ :<$> q)) =
291 -- trace "Left Absorption Law"
292 p :<* q
293 optimizeCombNode (u :<*> (v :<* w)) =
294 -- trace "Reassociation Law 2" $
295 optimizeCombNode (optimizeCombNode (u :<*> v) :<* w)
296 optimizeCombNode (u :<*> (v :$> x)) =
297 -- trace "Reassociation Law 3" $
298 optimizeCombNode (optimizeCombNode (u :<*> Pure x) :<* v)
299
300 ----------------------------------------------
301 -- Alternative optimizations
302 ----------------------------------------------
303
304 optimizeCombNode (p@Pure{} :<|> _) =
305 -- trace "Left Catch Law" $
306 p
307 optimizeCombNode (Empty :<|> u) =
308 -- trace "Left Neutral Law" $
309 u
310 optimizeCombNode (u :<|> Empty) =
311 -- trace "Right Neutral Law" $
312 u
313 optimizeCombNode ((u :<|> v) :<|> w) =
314 -- trace "Associativity Law" $
315 u :<|> optimizeCombNode (v :<|> w)
316
317 ----------------------------------------------
318 -- Sequencing optimizations
319 ----------------------------------------------
320
321 optimizeCombNode ((Pure _) :*> u) =
322 -- trace "Identity Law" $
323 u
324 optimizeCombNode ((u :$> _) :*> v) =
325 -- trace "Identity Law" $
326 u :*> v
327 optimizeCombNode (u :*> (v :*> w)) =
328 -- trace "Associativity Law" $
329 optimizeCombNode (optimizeCombNode (u :*> v) :*> w)
330 optimizeCombNode (u :<* (Pure _)) =
331 -- trace "Identity Law" $
332 u
333 optimizeCombNode (u :<* (v :$> _)) =
334 -- trace "Identity Law" $
335 optimizeCombNode (u :<* v)
336 optimizeCombNode (x :<$ u) =
337 -- trace "Commutativity Law" $
338 optimizeCombNode (u :$> x)
339 optimizeCombNode ((u :<* v) :<* w) =
340 -- trace "Associativity Law" $
341 optimizeCombNode (u :<* optimizeCombNode (v :<* w))
342 optimizeCombNode (Look p@Pure{}) =
343 -- trace "Pure Look Law" $
344 p
345 optimizeCombNode (Look p@Empty) =
346 -- trace "Dead Look Law" $
347 p
348 optimizeCombNode (NegLook Pure{}) =
349 -- trace "Pure Negative-Look" $
350 Empty
351 optimizeCombNode (NegLook Empty) =
352 -- trace "Dead Negative-Look" $
353 Pure H.unit
354 optimizeCombNode (NegLook (NegLook p)) =
355 -- trace "Double Negation Law" $
356 optimizeCombNode (Look (Try p :*> Pure H.unit))
357 optimizeCombNode (NegLook (Try p)) =
358 -- trace "Zero Consumption Law" $
359 optimizeCombNode (NegLook p)
360 optimizeCombNode (Look (Look p)) =
361 -- trace "Idempotence Law" $
362 Look p
363 optimizeCombNode (NegLook (Look p)) =
364 -- trace "Right Identity Law" $
365 optimizeCombNode (NegLook p)
366 optimizeCombNode (Look (NegLook p)) =
367 -- trace "Left Identity Law" $
368 NegLook p
369 optimizeCombNode (NegLook (Try p :<|> q)) =
370 -- trace "Transparency Law" $
371 optimizeCombNode (optimizeCombNode (NegLook p) :*> optimizeCombNode (NegLook q))
372 optimizeCombNode (Look p :<|> Look q) =
373 -- trace "Distributivity Law" $
374 optimizeCombNode (Look (optimizeCombNode ((Try p) :<|> q)))
375 optimizeCombNode (Look (p :$> x)) =
376 -- trace "Interchange Law" $
377 optimizeCombNode (optimizeCombNode (Look p) :$> x)
378 optimizeCombNode (Look (f :<$> p)) =
379 -- trace "Interchange Law" $
380 optimizeCombNode (f :<$> optimizeCombNode (Look p))
381 optimizeCombNode (p :<*> NegLook q) =
382 -- trace "Absorption Law" $
383 optimizeCombNode (optimizeCombNode (p :<*> Pure H.unit) :<* NegLook q)
384 optimizeCombNode (NegLook ((p :$> _))) =
385 -- trace "NegLookIdempotence Law" $
386 optimizeCombNode (NegLook p)
387 optimizeCombNode (NegLook ((_ :<$> p))) =
388 -- trace "NegLook Idempotence Law" $
389 optimizeCombNode (NegLook p)
390 optimizeCombNode (Try (p :$> x)) =
391 -- trace "Try Interchange Law" $
392 optimizeCombNode (optimizeCombNode (Try p) :$> x)
393 optimizeCombNode (Try (f :<$> p)) =
394 -- trace "Try Interchange Law" $
395 optimizeCombNode (f :<$> optimizeCombNode (Try p))
396 optimizeCombNode (Branch (Pure (trans -> lr)) l r) =
397 -- trace "Branch Pure Left/Right Law" $
398 case H.value lr of
399 Left value -> optimizeCombNode (l :<*> Pure (trans H.ValueCode{..}))
400 where code = [|| case $$(H.code lr) of Left x -> x ||]
401 Right value -> optimizeCombNode (r :<*> Pure (trans H.ValueCode{..}))
402 where code = [|| case $$(H.code lr) of Right x -> x ||]
403 optimizeCombNode (Branch b (Pure (trans -> l)) (Pure (trans -> r))) =
404 -- trace "Branch Generalised Identity Law" $
405 optimizeCombNode (trans H.ValueCode{..} :<$> b)
406 where
407 value = either (H.value l) (H.value r)
408 code = [|| either $$(H.code l) $$(H.code r) ||]
409 optimizeCombNode (Branch (x :*> y) p q) =
410 -- trace "Interchange Law" $
411 optimizeCombNode (x :*> optimizeCombNode (Branch y p q))
412 optimizeCombNode (Branch b l Empty) =
413 -- trace "Negated Branch Law" $
414 Branch (Pure (trans (H.ValueCode{..})) :<*> b) Empty l
415 where
416 value = either Right Left
417 code = [||either Right Left||]
418 optimizeCombNode (Branch (Branch b Empty (Pure (trans -> lr))) Empty br) =
419 -- trace "Branch Fusion Law" $
420 optimizeCombNode (Branch (optimizeCombNode (Pure (trans H.ValueCode{..}) :<*> b)) Empty br)
421 where
422 value Left{} = Left ()
423 value (Right r) = case H.value lr r of
424 Left _ -> Left ()
425 Right rr -> Right rr
426 code = [|| \case Left{} -> Left ()
427 Right r -> case $$(H.code lr) r of
428 Left _ -> Left ()
429 Right rr -> Right rr ||]
430 optimizeCombNode (f :<$> Branch b l r) =
431 -- trace "Branch Distributivity Law" $
432 optimizeCombNode (Branch b (optimizeCombNode ((H..) H..@ f :<$> l))
433 (optimizeCombNode ((H..) H..@ f :<$> r)))
434 optimizeCombNode (Match a _ps bs Empty)
435 | Foldable.all (\case { Empty -> True; _ -> False }) bs =
436 -- trace "Match Weakening Law" $
437 optimizeCombNode (a :*> Empty)
438 optimizeCombNode (Match (Pure (trans -> a)) ps bs d) =
439 -- trace "Match Pure Law" $
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 optimizeCombNode (f :<$> Match a ps bs d) =
444 -- trace "Match Distributivity Law" $
445 Match a ps (optimizeCombNode . (f :<$>) Functor.<$> bs)
446 (optimizeCombNode (f :<$> d))
447
448 optimizeCombNode x = x