Skip to content

Commit be7e561

Browse files
breakerzirconiagithub-actions
breakerzirconia
and
github-actions
authored
Attempt the monomorphization of various functions and datatypes (#3178)
* Monomorphize evaluateApplication, BuiltinAndAxiomSimplifier * Monomorphize SMT.evaluator * Monomorphize simplifyRuleLhs and Kore.Exec * Format with fourmolu * Monomorphize Kore.Rewrite & Kore.Builtin.AssociativeCommutative * Monomorphize some of the Builtin modules * Monomorphize Kore.Builtin.*, prepare for specialization * Monomorphize Kore.{Equation, ModelChecker}.* * Format with fourmolu * Monomorphize Kore.Rewrite.*, add liftSimplifier to Kore.Simplify.* * Format with fourmolu * Remove mapNotSimplifier Co-authored-by: github-actions <github-actions@github.com>
1 parent 71f6302 commit be7e561

33 files changed

+262
-316
lines changed

‎kore/src/Kore/Builtin/AssocComm/CeilSimplifier.hs‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -107,6 +107,12 @@ newSetCeilSimplifier =
107107
)
108108
ceil
109109

110+
-- {-# SPECIALIZE newSetCeilSimplifier ::
111+
-- CeilSimplifier
112+
-- Simplifier
113+
-- (BuiltinAssocComm NormalizedSet RewritingVariableName)
114+
-- (OrCondition RewritingVariableName) #-}
115+
110116
newMapCeilSimplifier ::
111117
forall simplifier.
112118
MonadReader (SideCondition RewritingVariableName) simplifier =>
@@ -140,6 +146,12 @@ newMapCeilSimplifier =
140146
)
141147
ceil
142148

149+
-- {-# SPECIALIZE newMapCeilSimplifier ::
150+
-- CeilSimplifier
151+
-- Simplifier
152+
-- (BuiltinAssocComm NormalizedMap RewritingVariableName)
153+
-- (OrCondition RewritingVariableName) #-}
154+
143155
{- | Generalize a 'MapElement' by replacing the 'MapValue' with a variable.
144156
145157
The variable is renamed if required to avoid the given 'FreeVariables' and any
@@ -221,6 +233,21 @@ newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
221233
evaluated <- makeEvaluateTermCeil sideCondition termLike
222234
return (multiAnd <> MultiAnd.singleton evaluated)
223235

236+
-- {-# SPECIALIZE newBuiltinAssocCommCeilSimplifier ::
237+
-- forall normalized.
238+
-- Ord (Element normalized (TermLike RewritingVariableName)) =>
239+
-- Ord (Value normalized (TermLike RewritingVariableName)) =>
240+
-- Hashable (Element normalized (TermLike RewritingVariableName)) =>
241+
-- Hashable (Value normalized (TermLike RewritingVariableName)) =>
242+
-- Traversable (Value normalized) =>
243+
-- AcWrapper normalized =>
244+
-- MkBuiltinAssocComm normalized RewritingVariableName ->
245+
-- MkNotMember normalized RewritingVariableName ->
246+
-- CeilSimplifier
247+
-- Simplifier
248+
-- (BuiltinAssocComm normalized RewritingVariableName)
249+
-- (OrCondition RewritingVariableName) #-}
250+
224251
definePairWiseElements ::
225252
forall normalized simplifier.
226253
Ord (Element normalized (TermLike RewritingVariableName)) =>
@@ -323,6 +350,17 @@ definePairWiseElements mkBuiltin mkNotMember internalAc pairWiseElements = do
323350
& OrCondition.fromPredicate
324351
& MultiAnd.singleton
325352

353+
-- {-# SPECIALIZE definePairWiseElements ::
354+
-- forall normalized.
355+
-- Ord (Element normalized (TermLike RewritingVariableName)) =>
356+
-- Hashable (Element normalized (TermLike RewritingVariableName)) =>
357+
-- AcWrapper normalized =>
358+
-- MkBuiltinAssocComm normalized RewritingVariableName ->
359+
-- MkNotMember normalized RewritingVariableName ->
360+
-- InternalAc Key normalized (TermLike RewritingVariableName) ->
361+
-- PairWiseElements normalized Key (TermLike RewritingVariableName) ->
362+
-- MaybeT Simplifier (MultiAnd (OrCondition RewritingVariableName)) #-}
363+
326364
fromElement ::
327365
AcWrapper normalized =>
328366
Element normalized (TermLike RewritingVariableName) ->

‎kore/src/Kore/Builtin/AssociativeCommutative.hs‎

Lines changed: 8 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -529,13 +529,12 @@ addElementDisjoint (list, existing) (key, value) =
529529

530530
-- | Given a @NormalizedAc@, returns it as a function result.
531531
returnAc ::
532-
( MonadSimplify m
533-
, InternalVariable variable
532+
( InternalVariable variable
534533
, TermWrapper normalized
535534
) =>
536535
Sort ->
537536
TermNormalizedAc normalized variable ->
538-
m (Pattern variable)
537+
Simplifier (Pattern variable)
539538
returnAc resultSort ac = do
540539
tools <- Simplifier.askMetadataTools
541540
asInternal tools resultSort ac
@@ -546,13 +545,12 @@ returnAc resultSort ac = do
546545
as a function result.
547546
-}
548547
returnConcreteAc ::
549-
( MonadSimplify m
550-
, InternalVariable variable
548+
( InternalVariable variable
551549
, TermWrapper normalized
552550
) =>
553551
Sort ->
554552
HashMap Key (Value normalized (TermLike variable)) ->
555-
m (Pattern variable)
553+
Simplifier (Pattern variable)
556554
returnConcreteAc resultSort concrete =
557555
(returnAc resultSort . wrapAc)
558556
NormalizedAc
@@ -622,15 +620,14 @@ asPattern tools resultSort =
622620
NormalizedOrBottom, providind the result in the form of a function result.
623621
-}
624622
evalConcatNormalizedOrBottom ::
625-
forall normalized simplifier variable.
626-
( MonadSimplify simplifier
627-
, InternalVariable variable
623+
forall normalized variable.
624+
( InternalVariable variable
628625
, TermWrapper normalized
629626
) =>
630627
Sort ->
631628
NormalizedOrBottom normalized variable ->
632629
NormalizedOrBottom normalized variable ->
633-
MaybeT simplifier (Pattern variable)
630+
MaybeT Simplifier (Pattern variable)
634631
evalConcatNormalizedOrBottom resultSort Bottom _ =
635632
return (Pattern.bottomOf resultSort)
636633
evalConcatNormalizedOrBottom resultSort _ Bottom =
@@ -639,7 +636,7 @@ evalConcatNormalizedOrBottom
639636
resultSort
640637
(Normalized normalized1)
641638
(Normalized normalized2) =
642-
maybe (return $ Pattern.bottomOf resultSort) (returnAc resultSort) $
639+
maybe (return $ Pattern.bottomOf resultSort) (lift . returnAc resultSort) $
643640
concatNormalized normalized1 normalized2
644641

645642
disjointMap :: Ord a => Hashable a => [(a, b)] -> Maybe (HashMap a b)

‎kore/src/Kore/Builtin/Builtin.hs‎

Lines changed: 6 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -114,7 +114,7 @@ import Kore.Simplify.Simplify (
114114
AttemptedAxiom (..),
115115
AttemptedAxiomResults (..),
116116
BuiltinAndAxiomSimplifier (..),
117-
MonadSimplify,
117+
Simplifier,
118118
TermSimplifier,
119119
applicationAxiomSimplifier,
120120
)
@@ -275,14 +275,13 @@ ternaryOperator extractVal asPattern ctx op =
275275
_ -> wrongArity (Text.unpack ctx)
276276

277277
type Function =
278-
forall variable simplifier.
278+
forall variable.
279279
InternalVariable variable =>
280280
HasCallStack =>
281-
MonadSimplify simplifier =>
282281
SideCondition variable ->
283282
Sort ->
284283
[TermLike variable] ->
285-
MaybeT simplifier (Pattern variable)
284+
MaybeT Simplifier (Pattern variable)
286285

287286
functionEvaluator :: Function -> BuiltinAndAxiomSimplifier
288287
functionEvaluator impl =
@@ -293,26 +292,24 @@ functionEvaluator impl =
293292
impl sideCondition resultSort args
294293

295294
applicationEvaluator ::
296-
( forall variable simplifier.
295+
( forall variable.
297296
InternalVariable variable =>
298-
MonadSimplify simplifier =>
299297
SideCondition variable ->
300298
Application Symbol (TermLike variable) ->
301-
MaybeT simplifier (Pattern variable)
299+
MaybeT Simplifier (Pattern variable)
302300
) ->
303301
BuiltinAndAxiomSimplifier
304302
applicationEvaluator impl =
305303
applicationAxiomSimplifier evaluator
306304
where
307305
evaluator ::
308306
InternalVariable variable =>
309-
MonadSimplify simplifier =>
310307
SideCondition variable ->
311308
CofreeF
312309
(Application Symbol)
313310
(TermAttributes variable)
314311
(TermLike variable) ->
315-
simplifier (AttemptedAxiom variable)
312+
Simplifier (AttemptedAxiom variable)
316313
evaluator sideCondition (_ :< app) = do
317314
getAttemptedAxiom
318315
(impl sideCondition app >>= appliedFunction)

‎kore/src/Kore/Builtin/KEqual.hs‎

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -145,15 +145,15 @@ builtinFunctions =
145145
]
146146

147147
evalKEq ::
148-
forall variable simplifier.
149-
(InternalVariable variable, MonadSimplify simplifier) =>
148+
forall variable.
149+
(InternalVariable variable) =>
150150
Bool ->
151151
SideCondition variable ->
152152
CofreeF
153153
(Application Symbol)
154154
(TermAttributes variable)
155155
(TermLike variable) ->
156-
simplifier (AttemptedAxiom variable)
156+
Simplifier (AttemptedAxiom variable)
157157
evalKEq true _ (valid :< app) =
158158
case applicationChildren of
159159
[t1, t2] -> Builtin.getAttemptedAxiom (evalEq t1 t2)
@@ -164,7 +164,7 @@ evalKEq true _ (valid :< app) =
164164
evalEq ::
165165
TermLike variable ->
166166
TermLike variable ->
167-
MaybeT simplifier (AttemptedAxiom variable)
167+
MaybeT Simplifier (AttemptedAxiom variable)
168168
evalEq termLike1 termLike2
169169
| termLike1 == termLike2 =
170170
Builtin.appliedFunction $ Bool.asPattern sort true
@@ -177,14 +177,12 @@ evalKEq true _ (valid :< app) =
177177
Builtin.appliedFunction $ Bool.asPattern sort (not true)
178178

179179
evalKIte ::
180-
forall simplifier.
181-
MonadSimplify simplifier =>
182180
SideCondition RewritingVariableName ->
183181
CofreeF
184182
(Application Symbol)
185183
(TermAttributes RewritingVariableName)
186184
(TermLike RewritingVariableName) ->
187-
simplifier (AttemptedAxiom RewritingVariableName)
185+
Simplifier (AttemptedAxiom RewritingVariableName)
188186
evalKIte _ (_ :< app) =
189187
case app of
190188
Application{applicationChildren = [expr, t1, t2]} ->

‎kore/src/Kore/Builtin/List.hs‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -249,18 +249,18 @@ expectConcreteBuiltinList ctx =
249249
. expectBuiltinList ctx
250250

251251
returnList ::
252-
(MonadSimplify m, InternalVariable variable) =>
252+
(InternalVariable variable) =>
253253
Sort ->
254254
Seq (TermLike variable) ->
255-
m (Pattern variable)
255+
Simplifier (Pattern variable)
256256
returnList builtinListSort builtinListChild = do
257257
tools <- Simplifier.askMetadataTools
258258
return $ asPattern tools builtinListSort builtinListChild
259259

260260
evalElement :: Builtin.Function
261261
evalElement _ resultSort =
262262
\case
263-
[elem'] -> returnList resultSort (Seq.singleton elem')
263+
[elem'] -> lift $ returnList resultSort (Seq.singleton elem')
264264
_ -> Builtin.wrongArity elementKey
265265

266266
evalGet :: Builtin.Function
@@ -291,7 +291,7 @@ evalUpdate _ resultSort [_list, _ix, value] = do
291291
_ix <- fromInteger <$> Int.expectBuiltinInt getKey _ix
292292
let len = Seq.length _list
293293
if _ix >= 0 && _ix < len
294-
then returnList resultSort (Seq.update _ix value _list)
294+
then lift $ returnList resultSort (Seq.update _ix value _list)
295295
else return (Pattern.bottomOf resultSort)
296296
evalUpdate _ _ _ = Builtin.wrongArity updateKey
297297

@@ -307,7 +307,7 @@ evalIn _ _ _ = Builtin.wrongArity inKey
307307
evalUnit :: Builtin.Function
308308
evalUnit _ resultSort =
309309
\case
310-
[] -> returnList resultSort Seq.empty
310+
[] -> lift $ returnList resultSort Seq.empty
311311
_ -> Builtin.wrongArity "LIST.unit"
312312

313313
evalConcat :: Builtin.Function
@@ -325,7 +325,7 @@ evalConcat _ resultSort [_list1, _list2] = do
325325
bothConcrete = do
326326
_list1 <- expectBuiltinList concatKey _list1
327327
_list2 <- expectBuiltinList concatKey _list2
328-
returnList resultSort (_list1 <> _list2)
328+
lift $ returnList resultSort (_list1 <> _list2)
329329
leftIdentity <|> rightIdentity <|> bothConcrete
330330
evalConcat _ _ _ = Builtin.wrongArity concatKey
331331

@@ -342,7 +342,7 @@ evalMake :: Builtin.Function
342342
evalMake _ resultSort [_len, value] = do
343343
_len <- fromInteger <$> Int.expectBuiltinInt getKey _len
344344
if _len >= 0
345-
then returnList resultSort (Seq.replicate _len value)
345+
then lift $ returnList resultSort (Seq.replicate _len value)
346346
else return (Pattern.bottomOf resultSort)
347347
evalMake _ _ _ = Builtin.wrongArity sizeKey
348348

@@ -361,7 +361,7 @@ evalUpdateAll _ resultSort [_list1, _ix, _list2] = do
361361
let unchanged1 = Seq.take _ix _list1
362362
unchanged2 = Seq.drop (_ix + length _list2) _list1
363363
in returnList resultSort (unchanged1 <> _list2 <> unchanged2)
364-
result
364+
lift result
365365
evalUpdateAll _ _ _ = Builtin.wrongArity updateKey
366366

367367
-- | Implement builtin function evaluation.

0 commit comments

Comments
 (0)