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