Skip to content

Commit 7a49019

Browse files
ttuegelttuegel
committed
Fully specify instances Recursive, Corecursive
Specifying all class functions for these instances for `PurePattern` and `KorePattern` allows us to take advantage of specialized implementations in the parent instances. (I originally wrote this patch when I was on a performance wild-goose chase. In the end, this is worth less than 0.5% on performance, but I wasn't going to throw it away.)
1 parent 174499f commit 7a49019

File tree

2 files changed

+189
-22
lines changed

2 files changed

+189
-22
lines changed

‎src/main/haskell/kore/src/Kore/AST/Kore.hs

Lines changed: 102 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -46,8 +46,10 @@ module Kore.AST.Kore
4646
import Control.Comonad
4747
import Control.Comonad.Trans.Cofree
4848
( Cofree, CofreeF (..), ComonadCofree (..) )
49+
import qualified Control.Comonad.Trans.Env as Env
4950
import Control.DeepSeq
5051
( NFData (..) )
52+
import qualified Data.Bifunctor as Bifunctor
5153
import Data.Deriving
5254
( makeLiftCompare, makeLiftEq, makeLiftShowsPrec )
5355
import Data.Functor.Classes
@@ -108,6 +110,7 @@ instance
108110
Eq1 (UnifiedPattern domain variable)
109111
where
110112
liftEq = $(makeLiftEq ''UnifiedPattern)
113+
{-# INLINE liftEq #-}
111114

112115
instance
113116
( Ord1 (Pattern Meta domain variable)
@@ -116,6 +119,7 @@ instance
116119
Ord1 (UnifiedPattern domain variable)
117120
where
118121
liftCompare = $(makeLiftCompare ''UnifiedPattern)
122+
{-# INLINE liftCompare #-}
119123

120124
instance
121125
( Show1 (Pattern Meta domain variable)
@@ -137,6 +141,7 @@ instance
137141
salt `hashWithSalt` (0::Int) `hashWithSalt` metaP
138142
UnifiedObjectPattern objectP ->
139143
salt `hashWithSalt` (1::Int) `hashWithSalt` objectP
144+
{-# INLINE hashWithSalt #-}
140145

141146
-- |View a 'Meta' or an 'Object' 'Pattern' as an 'UnifiedPattern'
142147
asUnifiedPattern
@@ -194,7 +199,6 @@ deriving instance
194199
) =>
195200
Traversable (UnifiedPattern domain variable)
196201

197-
198202
{- | The abstract syntax of Kore.
199203
200204
@KorePattern@ covers the 'Object' and 'Meta' levels of Kore, corresponding to
@@ -232,6 +236,7 @@ instance
232236
(Recursive.project -> _ :< pat2)
233237
=
234238
liftEq eqWorker pat1 pat2
239+
{-# INLINE (==) #-}
235240

236241
instance
237242
( OrdMetaOrObject variable
@@ -246,6 +251,7 @@ instance
246251
(Recursive.project -> _ :< pat2)
247252
=
248253
liftCompare compareWorker pat1 pat2
254+
{-# INLINE compare #-}
249255

250256
deriving instance
251257
( Show annotation
@@ -264,6 +270,7 @@ instance
264270
Hashable (KorePattern domain variable annotation)
265271
where
266272
hashWithSalt salt (Recursive.project -> _ :< pat) = hashWithSalt salt pat
273+
{-# INLINE hashWithSalt #-}
267274

268275
instance
269276
( Functor domain
@@ -285,17 +292,109 @@ instance
285292
Functor domain =>
286293
Recursive (KorePattern domain variable annotation)
287294
where
288-
project (KorePattern embedded) =
295+
project = \(KorePattern embedded) ->
289296
case Recursive.project embedded of
290297
Compose (Identity projected) -> KorePattern <$> projected
298+
{-# INLINE project #-}
299+
300+
cata alg = \(KorePattern fixed) ->
301+
Recursive.cata
302+
(\(Compose (Identity base)) -> alg base)
303+
fixed
304+
{-# INLINE cata #-}
305+
306+
para alg = \(KorePattern fixed) ->
307+
Recursive.para
308+
(\(Compose (Identity base)) ->
309+
alg (Bifunctor.first KorePattern <$> base)
310+
)
311+
fixed
312+
{-# INLINE para #-}
313+
314+
gpara dist alg = \(KorePattern fixed) ->
315+
Recursive.gpara
316+
(\(Compose (Identity base)) -> Compose . Identity <$> dist base)
317+
(\(Compose (Identity base)) -> alg (Env.local KorePattern <$> base))
318+
fixed
319+
{-# INLINE gpara #-}
320+
321+
prepro pre alg = \(KorePattern fixed) ->
322+
Recursive.prepro
323+
(\(Compose (Identity base)) -> (Compose . Identity) (pre base))
324+
(\(Compose (Identity base)) -> alg base)
325+
fixed
326+
{-# INLINE prepro #-}
327+
328+
gprepro dist pre alg = \(KorePattern fixed) ->
329+
Recursive.gprepro
330+
(\(Compose (Identity base)) -> Compose . Identity <$> dist base)
331+
(\(Compose (Identity base)) -> (Compose . Identity) (pre base))
332+
(\(Compose (Identity base)) -> alg base)
333+
fixed
334+
{-# INLINE gprepro #-}
291335

292336
instance
293337
Functor domain =>
294338
Corecursive (KorePattern domain variable annotation)
295339
where
296-
embed projected =
340+
embed = \projected ->
297341
(KorePattern . Recursive.embed . Compose . Identity)
298342
(getKorePattern <$> projected)
343+
{-# INLINE embed #-}
344+
345+
ana coalg = KorePattern . ana0
346+
where
347+
ana0 =
348+
Recursive.ana (Compose . Identity . coalg)
349+
{-# INLINE ana #-}
350+
351+
apo coalg = KorePattern . apo0
352+
where
353+
apo0 =
354+
Recursive.apo
355+
(\a ->
356+
(Compose . Identity)
357+
(Bifunctor.first getKorePattern <$> coalg a)
358+
)
359+
{-# INLINE apo #-}
360+
361+
postpro post coalg = KorePattern . postpro0
362+
where
363+
postpro0 =
364+
Recursive.postpro
365+
(\(Compose (Identity base)) -> (Compose . Identity) (post base))
366+
(Compose . Identity . coalg)
367+
{-# INLINE postpro #-}
368+
369+
gpostpro dist post coalg = KorePattern . gpostpro0
370+
where
371+
gpostpro0 =
372+
Recursive.gpostpro
373+
(Compose . Identity . dist . (<$>) (runIdentity . getCompose))
374+
(\(Compose (Identity base)) -> (Compose . Identity) (post base))
375+
(Compose . Identity . coalg)
376+
{-# INLINE gpostpro #-}
377+
378+
instance
379+
Functor domain =>
380+
Comonad (KorePattern domain variable)
381+
where
382+
extract = \(KorePattern fixed) -> extract fixed
383+
{-# INLINE extract #-}
384+
duplicate = \(KorePattern fixed) -> KorePattern (extend KorePattern fixed)
385+
{-# INLINE duplicate #-}
386+
extend extending = \(KorePattern fixed) ->
387+
KorePattern (extend (extending . KorePattern) fixed)
388+
{-# INLINE extend #-}
389+
390+
instance
391+
Functor domain =>
392+
ComonadCofree
393+
(UnifiedPattern domain variable)
394+
(KorePattern domain variable)
395+
where
396+
unwrap = \(KorePattern fixed) -> KorePattern <$> unwrap fixed
397+
{-# INLINE unwrap #-}
299398

300399
-- | View an annotated 'Meta' or 'Object' 'Pattern' as a 'KorePattern'
301400
asKorePattern
@@ -321,18 +420,6 @@ eraseAnnotations =
321420
UnifiedMetaPattern _ -> UnifiedMeta Annotation.Null :< unified
322421
UnifiedObjectPattern _ -> UnifiedObject Annotation.Null :< unified
323422

324-
instance Functor dom => Comonad (KorePattern dom var) where
325-
extract (KorePattern a) = extract a
326-
duplicate (KorePattern a) = KorePattern (extend KorePattern a)
327-
extend extending (KorePattern a) =
328-
KorePattern (extend (extending . KorePattern) a)
329-
330-
instance
331-
Functor domain =>
332-
ComonadCofree (UnifiedPattern domain variable) (KorePattern domain variable)
333-
where
334-
unwrap (KorePattern a) = KorePattern <$> unwrap a
335-
336423
-- | View a 'Meta' or 'Object' 'Pattern' as a 'KorePattern'
337424
asCommonKorePattern
338425
:: MetaOrObject level

‎src/main/haskell/kore/src/Kore/AST/Pure.hs

Lines changed: 87 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,10 @@ module Kore.AST.Pure
3939
import Control.Comonad
4040
import Control.Comonad.Trans.Cofree
4141
( Cofree, CofreeF (..), ComonadCofree (..) )
42+
import qualified Control.Comonad.Trans.Env as Env
4243
import Control.DeepSeq
4344
( NFData (..) )
45+
import qualified Data.Bifunctor as Bifunctor
4446
import Data.Functor.Classes
4547
import Data.Functor.Compose
4648
( Compose (..) )
@@ -107,6 +109,7 @@ instance
107109
(Recursive.project -> _ :< pat2)
108110
=
109111
liftEq eqWorker pat1 pat2
112+
{-# INLINE (==) #-}
110113

111114
instance
112115
( Ord level
@@ -122,6 +125,7 @@ instance
122125
(Recursive.project -> _ :< pat2)
123126
=
124127
liftCompare compareWorker pat1 pat2
128+
{-# INLINE compare #-}
125129

126130
deriving instance
127131
( Show annotation
@@ -140,6 +144,7 @@ instance
140144
Hashable (PurePattern level domain variable annotation)
141145
where
142146
hashWithSalt salt (Recursive.project -> _ :< pat) = hashWithSalt salt pat
147+
{-# INLINE hashWithSalt #-}
143148

144149
instance
145150
( Functor domain
@@ -160,34 +165,109 @@ instance
160165
Functor domain =>
161166
Recursive (PurePattern level domain variable annotation)
162167
where
163-
project (PurePattern embedded) =
168+
project = \(PurePattern embedded) ->
164169
case Recursive.project embedded of
165170
Compose (Identity projected) -> PurePattern <$> projected
171+
{-# INLINE project #-}
172+
173+
cata alg = \(PurePattern fixed) ->
174+
Recursive.cata
175+
(\(Compose (Identity base)) -> alg base)
176+
fixed
177+
{-# INLINE cata #-}
178+
179+
para alg = \(PurePattern fixed) ->
180+
Recursive.para
181+
(\(Compose (Identity base)) ->
182+
alg (Bifunctor.first PurePattern <$> base)
183+
)
184+
fixed
185+
{-# INLINE para #-}
186+
187+
gpara dist alg = \(PurePattern fixed) ->
188+
Recursive.gpara
189+
(\(Compose (Identity base)) -> Compose . Identity <$> dist base)
190+
(\(Compose (Identity base)) -> alg (Env.local PurePattern <$> base))
191+
fixed
192+
{-# INLINE gpara #-}
193+
194+
prepro pre alg = \(PurePattern fixed) ->
195+
Recursive.prepro
196+
(\(Compose (Identity base)) -> (Compose . Identity) (pre base))
197+
(\(Compose (Identity base)) -> alg base)
198+
fixed
199+
{-# INLINE prepro #-}
200+
201+
gprepro dist pre alg = \(PurePattern fixed) ->
202+
Recursive.gprepro
203+
(\(Compose (Identity base)) -> Compose . Identity <$> dist base)
204+
(\(Compose (Identity base)) -> (Compose . Identity) (pre base))
205+
(\(Compose (Identity base)) -> alg base)
206+
fixed
207+
{-# INLINE gprepro #-}
166208

167209
instance
168210
Functor domain =>
169211
Corecursive (PurePattern level domain variable annotation)
170212
where
171-
embed projected =
213+
embed = \projected ->
172214
(PurePattern . Recursive.embed . Compose . Identity)
173215
(getPurePattern <$> projected)
216+
{-# INLINE embed #-}
217+
218+
ana coalg = PurePattern . ana0
219+
where
220+
ana0 =
221+
Recursive.ana (Compose . Identity . coalg)
222+
{-# INLINE ana #-}
223+
224+
apo coalg = PurePattern . apo0
225+
where
226+
apo0 =
227+
Recursive.apo
228+
(\a ->
229+
(Compose . Identity)
230+
(Bifunctor.first getPurePattern <$> coalg a)
231+
)
232+
{-# INLINE apo #-}
233+
234+
postpro post coalg = PurePattern . postpro0
235+
where
236+
postpro0 =
237+
Recursive.postpro
238+
(\(Compose (Identity base)) -> (Compose . Identity) (post base))
239+
(Compose . Identity . coalg)
240+
{-# INLINE postpro #-}
241+
242+
gpostpro dist post coalg = PurePattern . gpostpro0
243+
where
244+
gpostpro0 =
245+
Recursive.gpostpro
246+
(Compose . Identity . dist . (<$>) (runIdentity . getCompose))
247+
(\(Compose (Identity base)) -> (Compose . Identity) (post base))
248+
(Compose . Identity . coalg)
249+
{-# INLINE gpostpro #-}
174250

175251
instance
176252
Functor domain =>
177253
Comonad (PurePattern level domain variable)
178254
where
179-
extract (PurePattern a) = extract a
180-
duplicate (PurePattern a) = PurePattern (extend PurePattern a)
181-
extend extending (PurePattern a) =
182-
PurePattern (extend (extending . PurePattern) a)
255+
extract = \(PurePattern fixed) -> extract fixed
256+
{-# INLINE extract #-}
257+
duplicate = \(PurePattern fixed) -> PurePattern (extend PurePattern fixed)
258+
{-# INLINE duplicate #-}
259+
extend extending = \(PurePattern fixed) ->
260+
PurePattern (extend (extending . PurePattern) fixed)
261+
{-# INLINE extend #-}
183262

184263
instance
185264
Functor domain =>
186265
ComonadCofree
187266
(Pattern level domain variable)
188267
(PurePattern level domain variable)
189268
where
190-
unwrap (PurePattern a) = PurePattern <$> unwrap a
269+
unwrap = \(PurePattern fixed) -> PurePattern <$> unwrap fixed
270+
{-# INLINE unwrap #-}
191271

192272
instance Functor domain
193273
=> TopBottom (PurePattern level domain variable annotation)

0 commit comments

Comments
 (0)