Skip to content

Commit 8585c19

Browse files
ttuegelttuegel
authored
Add class Substitute (#2702)
1 parent 6a50966 commit 8585c19

35 files changed

+573
-593
lines changed

‎kore/src/Kore/Attribute/Pattern/FreeVariables.hs‎

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,9 @@ import Prelude.Kore hiding (
3838
toList,
3939
)
4040

41-
newtype FreeVariables variable = FreeVariables {getFreeVariables :: Map (SomeVariableName variable) Sort}
41+
newtype FreeVariables variable = FreeVariables
42+
{ getFreeVariables :: Map (SomeVariableName variable) Sort
43+
}
4244
deriving stock (Eq, Ord, Show)
4345
deriving stock (GHC.Generic)
4446
deriving anyclass (NFData)
@@ -50,7 +52,11 @@ instance Hashable variable => Hashable (FreeVariables variable) where
5052
hashWithSalt salt = hashWithSalt salt . toList
5153
{-# INLINE hashWithSalt #-}
5254

53-
instance Synthetic (FreeVariables variable) (Const (SomeVariable variable)) where
55+
instance
56+
Synthetic
57+
(FreeVariables variable)
58+
(Const (SomeVariable variable))
59+
where
5460
synthetic (Const var) = freeVariable var
5561
{-# INLINE synthetic #-}
5662

‎kore/src/Kore/Equation/Application.hs‎

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,6 @@ import Kore.Internal.Predicate (
8080
makeAndPredicate,
8181
makeNotPredicate,
8282
)
83-
import qualified Kore.Internal.Predicate as Predicate
8483
import Kore.Internal.SideCondition (
8584
SideCondition,
8685
)
@@ -106,6 +105,7 @@ import Kore.Step.Simplification.Simplify (
106105
)
107106
import qualified Kore.Step.Simplification.Simplify as Simplifier
108107
import qualified Kore.Step.Substitution as Substitution
108+
import Kore.Substitute
109109
import Kore.Syntax.Id (
110110
AstLocation (..),
111111
FileLocation (..),
@@ -293,10 +293,8 @@ applyMatchResult equation matchResult@(predicate, substitution) = do
293293
, applyMatchErrors = x :| xs
294294
}
295295
_ -> return ()
296-
let predicate' =
297-
Predicate.substitute orientedSubstitution predicate
298-
equation' =
299-
Equation.substitute orientedSubstitution equation
296+
let predicate' = substitute orientedSubstitution predicate
297+
equation' = substitute orientedSubstitution equation
300298
return (equation', predicate')
301299
where
302300
orientedSubstitution = Substitution.orientSubstitution occursInEquation substitution

‎kore/src/Kore/Equation/Equation.hs‎

Lines changed: 31 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ module Kore.Equation.Equation (
1010
refreshVariables,
1111
isSimplificationRule,
1212
equationPriority,
13-
substitute,
1413
identifiers,
1514
) where
1615

@@ -49,12 +48,14 @@ import Kore.Internal.Symbol (
4948
import Kore.Internal.TermLike (
5049
InternalVariable,
5150
TermLike,
51+
mkVar,
5252
)
5353
import qualified Kore.Internal.TermLike as TermLike
5454
import Kore.Sort
5555
import Kore.Step.Step (
5656
Renaming,
5757
)
58+
import Kore.Substitute
5859
import Kore.Syntax.Application (
5960
Application (..),
6061
)
@@ -142,6 +143,25 @@ instance SQL.Column (Equation VariableName) where
142143
defineColumn = SQL.defineForeignKeyColumn
143144
toColumn = SQL.toForeignKeyColumn
144145

146+
instance InternalVariable variable => Substitute (Equation variable) where
147+
type TermType (Equation variable) = TermLike variable
148+
149+
type VariableNameType (Equation variable) = variable
150+
151+
substitute assignments equation =
152+
Equation
153+
{ requires = substitute assignments (requires equation)
154+
, argument = substitute assignments <$> argument equation
155+
, antiLeft = substitute assignments <$> antiLeft equation
156+
, left = substitute assignments (left equation)
157+
, right = substitute assignments (right equation)
158+
, ensures = substitute assignments (ensures equation)
159+
, attributes = attributes equation
160+
}
161+
162+
rename = substitute . fmap mkVar
163+
{-# INLINE rename #-}
164+
145165
toTermLike ::
146166
InternalVariable variable =>
147167
Sort ->
@@ -261,8 +281,8 @@ refreshVariables ::
261281
refreshVariables
262282
(FreeVariables.toNames -> avoid)
263283
equation@(Equation _ _ _ _ _ _ _) =
264-
let rename :: Map (SomeVariableName variable) (SomeVariable variable)
265-
rename =
284+
let rename' :: Map (SomeVariableName variable) (SomeVariable variable)
285+
rename' =
266286
FreeVariables.toSet originalFreeVariables
267287
& Fresh.refreshVariables avoid
268288
lookupSomeVariableName ::
@@ -273,7 +293,7 @@ refreshVariables
273293
lookupSomeVariableName variable =
274294
do
275295
let injected = inject @(SomeVariableName _) variable
276-
someVariableName <- variableName <$> Map.lookup injected rename
296+
someVariableName <- variableName <$> Map.lookup injected rename'
277297
retract someVariableName
278298
& fromMaybe variable
279299
adj :: AdjSomeVariableName (variable -> variable)
@@ -295,12 +315,12 @@ refreshVariables
295315
( variableName variable
296316
, TermLike.mkVar (mapSomeVariable adj variable)
297317
)
298-
left' = TermLike.substitute subst left
299-
requires' = Predicate.substitute subst requires
300-
argument' = Predicate.substitute subst <$> argument
301-
antiLeft' = Predicate.substitute subst <$> antiLeft
302-
right' = TermLike.substitute subst right
303-
ensures' = Predicate.substitute subst ensures
318+
left' = substitute subst left
319+
requires' = substitute subst requires
320+
argument' = substitute subst <$> argument
321+
antiLeft' = substitute subst <$> antiLeft
322+
right' = substitute subst right
323+
ensures' = substitute subst ensures
304324
attributes' = Attribute.mapAxiomVariables adj attributes
305325
equation' =
306326
equation
@@ -312,7 +332,7 @@ refreshVariables
312332
, ensures = ensures'
313333
, attributes = attributes'
314334
}
315-
in (rename, equation')
335+
in (rename', equation')
316336
where
317337
Equation
318338
{ requires
@@ -334,32 +354,6 @@ isSimplificationRule Equation{attributes} =
334354
equationPriority :: Equation variable -> Integer
335355
equationPriority = Attribute.getPriorityOfAxiom . attributes
336356

337-
substitute ::
338-
InternalVariable variable =>
339-
Map (SomeVariableName variable) (TermLike variable) ->
340-
Equation variable ->
341-
Equation variable
342-
substitute assignments equation =
343-
Equation
344-
{ requires = Predicate.substitute assignments requires
345-
, argument = Predicate.substitute assignments <$> argument
346-
, antiLeft = Predicate.substitute assignments <$> antiLeft
347-
, left = TermLike.substitute assignments left
348-
, right = TermLike.substitute assignments right
349-
, ensures = Predicate.substitute assignments ensures
350-
, attributes
351-
}
352-
where
353-
Equation
354-
{ requires
355-
, argument
356-
, antiLeft
357-
, left
358-
, right
359-
, ensures
360-
, attributes
361-
} = equation
362-
363357
{- | The list of identifiers for an 'Equation'.
364358
365359
The identifiers are:

‎kore/src/Kore/Equation/Simplification.hs‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ import Kore.Step.Simplification.Simplify (
3535
MonadSimplify,
3636
)
3737
import qualified Kore.Step.Simplification.Simplify as Simplifier
38+
import Kore.Substitute
3839
import Kore.TopBottom
3940
import qualified Logic
4041
import Prelude.Kore
@@ -76,11 +77,11 @@ simplifyEquation equation@(Equation _ _ _ _ _ _ _) =
7677
let Conditional{substitution, predicate} = simplifiedCond
7778
lift $ Monad.unless (isTop predicate) (throwE equation)
7879
let subst = Substitution.toMap substitution
79-
left' = TermLike.substitute subst left
80-
requires' = Predicate.substitute subst requires
81-
antiLeft' = Predicate.substitute subst <$> antiLeft
82-
right' = TermLike.substitute subst right
83-
ensures' = Predicate.substitute subst ensures
80+
left' = substitute subst left
81+
requires' = substitute subst requires
82+
antiLeft' = substitute subst <$> antiLeft
83+
right' = substitute subst right
84+
ensures' = substitute subst ensures
8485
return
8586
Equation
8687
{ left = TermLike.forgetSimplified left'

‎kore/src/Kore/Internal/Conditional.hs‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,8 +57,10 @@ import Kore.Internal.TermLike (
5757
Sort,
5858
SubstitutionOrd,
5959
TermLike,
60+
mkVar,
6061
termLikeSort,
6162
)
63+
import Kore.Substitute
6264
import Kore.TopBottom (
6365
TopBottom (..),
6466
)
@@ -229,6 +231,28 @@ instance
229231
@(Map (SomeVariable variable) (TermLike variable))
230232
@(Substitution variable)
231233

234+
instance
235+
( Substitute child
236+
, TermType child ~ TermLike variable
237+
, VariableNameType child ~ variable
238+
, InternalVariable variable
239+
) =>
240+
Substitute (Conditional variable child)
241+
where
242+
type TermType (Conditional variable child) = TermLike variable
243+
244+
type VariableNameType (Conditional variable child) = variable
245+
246+
substitute subst Conditional{term, predicate, substitution} =
247+
Conditional
248+
{ term = substitute subst term
249+
, predicate = substitute subst predicate
250+
, substitution = substitute subst substitution
251+
}
252+
253+
rename = substitute . fmap mkVar
254+
{-# INLINE rename #-}
255+
232256
prettyConditional ::
233257
Sort ->
234258
-- | term

‎kore/src/Kore/Internal/MultiOr.hs‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,14 @@ import GHC.Exts (
4242
)
4343
import qualified GHC.Generics as GHC
4444
import qualified Generics.SOP as SOP
45+
import Kore.Attribute.Pattern.FreeVariables (
46+
HasFreeVariables (..),
47+
)
4548
import Kore.Debug
49+
import Kore.Internal.Variable (
50+
InternalVariable,
51+
)
52+
import Kore.Substitute
4653
import Kore.Syntax.Application (
4754
Application (..),
4855
)
@@ -106,6 +113,31 @@ instance (Ord child, TopBottom child) => From [child] (MultiOr child) where
106113
instance From (MultiOr child) [child] where
107114
from = getMultiOr
108115

116+
instance
117+
(Ord variable, HasFreeVariables child variable) =>
118+
HasFreeVariables (MultiOr child) variable
119+
where
120+
freeVariables = foldMap freeVariables
121+
{-# INLINE freeVariables #-}
122+
123+
instance
124+
( InternalVariable (VariableNameType child)
125+
, Ord child
126+
, TopBottom child
127+
, Substitute child
128+
) =>
129+
Substitute (MultiOr child)
130+
where
131+
type TermType (MultiOr child) = TermType child
132+
133+
type VariableNameType (MultiOr child) = VariableNameType child
134+
135+
substitute = map . substitute
136+
{-# INLINE substitute #-}
137+
138+
rename = map . rename
139+
{-# INLINE rename #-}
140+
109141
bottom :: MultiOr term
110142
bottom = MultiOr []
111143

‎kore/src/Kore/Internal/OrPattern.hs‎

Lines changed: 0 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@ module Kore.Internal.OrPattern (
2121
toPattern,
2222
toTermLike,
2323
targetBinder,
24-
substitute,
2524
mapVariables,
2625
MultiOr.flatten,
2726
MultiOr.filterOr,
@@ -31,9 +30,6 @@ module Kore.Internal.OrPattern (
3130
MultiOr.traverse,
3231
) where
3332

34-
import Data.Map.Strict (
35-
Map,
36-
)
3733
import Kore.Internal.Condition (
3834
Condition,
3935
)
@@ -244,14 +240,6 @@ targetBinder Binder{binderVariable, binderChild} =
244240
, binderChild = newChild
245241
}
246242

247-
substitute ::
248-
InternalVariable variable =>
249-
Map (SomeVariableName variable) (TermLike variable) ->
250-
OrPattern variable ->
251-
OrPattern variable
252-
substitute subst =
253-
fromPatterns . fmap (Pattern.substitute subst) . toPatterns
254-
255243
mapVariables ::
256244
(InternalVariable variable1, InternalVariable variable2) =>
257245
AdjSomeVariableName (variable1 -> variable2) ->

‎kore/src/Kore/Internal/Pattern.hs‎

Lines changed: 0 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,6 @@ module Kore.Internal.Pattern (
3232
simplifiedAttribute,
3333
assign,
3434
requireDefined,
35-
substitute,
3635
fromMultiAnd,
3736

3837
-- * Re-exports
@@ -45,9 +44,6 @@ module Kore.Internal.Pattern (
4544
Condition,
4645
) where
4746

48-
import Data.Map.Strict (
49-
Map,
50-
)
5147
import Kore.Attribute.Pattern.FreeVariables (
5248
freeVariables,
5349
getFreeElementVariables,
@@ -392,22 +388,6 @@ requireDefined Conditional{term, predicate, substitution} =
392388
Predicate.makeCeilPredicate term
393389
}
394390

395-
{- | Apply a normalized 'Substitution' to a 'Pattern'.
396-
397-
The 'Substitution' of the result will not be normalized.
398-
-}
399-
substitute ::
400-
InternalVariable variable =>
401-
Map (SomeVariableName variable) (TermLike variable) ->
402-
Pattern variable ->
403-
Pattern variable
404-
substitute subst Conditional{term, predicate, substitution} =
405-
Conditional
406-
{ term = TermLike.substitute subst term
407-
, predicate = Predicate.substitute subst predicate
408-
, substitution = Substitution.substitute subst substitution
409-
}
410-
411391
fromMultiAnd ::
412392
InternalVariable variable =>
413393
MultiAnd (Pattern variable) ->

0 commit comments

Comments
 (0)