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