Skip to content

Commit f3b6373

Browse files
MirceaSMircea Sebettuegel
authored
Give Predicate a distinct internal representation (#2099)
Co-authored-by: Mircea Sebe <[email protected]> Co-authored-by: Thomas Tuegel <[email protected]> Co-authored-by: MirceaS <[email protected]> Co-authored-by: ttuegel <[email protected]>
1 parent d96b20f commit f3b6373

File tree

146 files changed

+3258
-2985
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

146 files changed

+3258
-2985
lines changed

‎default.nix

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,7 @@ let
4646
"/*"
4747
"!/stack.yaml"
4848
"!/kore"
49+
"*.cabal"
4950
];
5051
};
5152
inherit checkMaterialization;

‎kore/kore.cabal

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ cabal-version: 2.2
44
--
55
-- see: https://github.com/sol/hpack
66
--
7-
-- hash: 3120f5e24384393d150b1db1b680ac8a0c5d310317b293ba3f29f6848b8c6af7
7+
-- hash: 14a9c3fb13f5926dbd7132316a785e05c02d496c072bab9f8bd7533b1cbc8d41
88

99
name: kore
1010
version: 0.37.0.0
@@ -90,6 +90,7 @@ library
9090
Kore.Attribute.Pattern.Function
9191
Kore.Attribute.Pattern.Functional
9292
Kore.Attribute.Pattern.Simplified
93+
Kore.Attribute.PredicatePattern
9394
Kore.Attribute.Priority
9495
Kore.Attribute.ProductionID
9596
Kore.Attribute.RuleIndex

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

Lines changed: 20 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -38,9 +38,27 @@ import qualified GHC.Generics as GHC
3838

3939
import Kore.Attribute.Pattern.ConstructorLike
4040
import Kore.Attribute.Pattern.Created
41+
( Created (..)
42+
, hasKnownCreator
43+
)
4144
import Kore.Attribute.Pattern.Defined
42-
import Kore.Attribute.Pattern.FreeVariables hiding
43-
( freeVariables
45+
( Defined (..)
46+
)
47+
import Kore.Attribute.Pattern.FreeVariables
48+
( FreeVariables
49+
, HasFreeVariables
50+
, bindVariable
51+
, bindVariables
52+
, emptyFreeVariables
53+
, freeVariable
54+
, getFreeElementVariables
55+
, isFreeVariable
56+
, mapFreeVariables
57+
, nullFreeVariables
58+
, toList
59+
, toNames
60+
, toSet
61+
, traverseFreeVariables
4462
)
4563
import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables
4664
( freeVariables

‎kore/src/Kore/Attribute/PredicatePattern.hs

Lines changed: 153 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,153 @@
1+
{- |
2+
Copyright : (c) Runtime Verification, 2020
3+
License : NCSA
4+
5+
-}
6+
7+
{-# LANGUAGE UndecidableInstances #-}
8+
9+
module Kore.Attribute.PredicatePattern
10+
( PredicatePattern (PredicatePattern, freeVariables)
11+
-- simplified is excluded on purpose
12+
, simplifiedAttribute
13+
, isSimplified
14+
, isFullySimplified
15+
, setSimplified
16+
, mapVariables
17+
, traverseVariables
18+
, deleteFreeVariable
19+
, fromPattern
20+
-- * Re-exports
21+
, module Kore.Attribute.Pattern.FreeVariables
22+
) where
23+
24+
import Prelude.Kore
25+
26+
import Control.DeepSeq
27+
( NFData
28+
)
29+
import qualified Control.Lens as Lens
30+
import Data.Generics.Product
31+
import qualified Generics.SOP as SOP
32+
import qualified GHC.Generics as GHC
33+
34+
import Kore.Attribute.Pattern
35+
( Pattern
36+
)
37+
import qualified Kore.Attribute.Pattern as Pattern
38+
import Kore.Attribute.Pattern.FreeVariables hiding
39+
( freeVariables
40+
)
41+
import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables
42+
( freeVariables
43+
)
44+
import Kore.Attribute.Pattern.Simplified hiding
45+
( isFullySimplified
46+
, isSimplified
47+
)
48+
import qualified Kore.Attribute.Pattern.Simplified as Simplified
49+
( isFullySimplified
50+
, isSimplified
51+
)
52+
import Kore.Attribute.Synthetic
53+
import Kore.Debug
54+
import qualified Kore.Internal.SideCondition.SideCondition as SideCondition
55+
( Representation
56+
)
57+
import Kore.Syntax.Variable
58+
59+
{- | @Pattern@ are the attributes of a pattern collected during verification.
60+
-}
61+
data PredicatePattern variable =
62+
PredicatePattern
63+
{ freeVariables :: !(FreeVariables variable)
64+
, simplified :: !Simplified
65+
}
66+
deriving (Eq, GHC.Generic, Show)
67+
68+
instance NFData variable => NFData (PredicatePattern variable)
69+
70+
instance Hashable variable => Hashable (PredicatePattern variable)
71+
72+
instance SOP.Generic (PredicatePattern variable)
73+
74+
instance SOP.HasDatatypeInfo (PredicatePattern variable)
75+
76+
instance Debug variable => Debug (PredicatePattern variable) where
77+
debugPrecBrief _ _ = "_"
78+
79+
instance (Debug variable, Diff variable) => Diff (PredicatePattern variable)
80+
81+
instance
82+
( Functor base
83+
, Synthetic (FreeVariables variable) base
84+
, Synthetic Simplified base
85+
) => Synthetic (PredicatePattern variable) base
86+
where
87+
synthetic base = PredicatePattern
88+
{ freeVariables = synthetic (freeVariables <$> base)
89+
, simplified = synthetic (simplified <$> base)
90+
}
91+
92+
93+
simplifiedAttribute :: PredicatePattern variable -> Simplified
94+
simplifiedAttribute PredicatePattern {simplified} = simplified
95+
96+
{- Checks whether the pattern is simplified relative to the given side
97+
condition.
98+
-}
99+
isSimplified
100+
:: SideCondition.Representation -> PredicatePattern variable -> Bool
101+
isSimplified sideCondition = Simplified.isSimplified sideCondition . simplifiedAttribute
102+
103+
{- Checks whether the pattern is simplified relative to any side condition.
104+
-}
105+
isFullySimplified :: PredicatePattern variable -> Bool
106+
isFullySimplified PredicatePattern {simplified} = Simplified.isFullySimplified simplified
107+
108+
setSimplified :: Simplified -> PredicatePattern variable -> PredicatePattern variable
109+
setSimplified simplified patt = patt { simplified }
110+
111+
{- | Use the provided mapping to replace all variables in a 'Pattern'.
112+
113+
See also: 'traverseVariables'
114+
115+
-}
116+
mapVariables
117+
:: Ord variable2
118+
=> AdjSomeVariableName (variable1 -> variable2)
119+
-> PredicatePattern variable1
120+
-> PredicatePattern variable2
121+
mapVariables adj = Lens.over (field @"freeVariables") (mapFreeVariables adj)
122+
123+
{- | Use the provided traversal to replace the free variables in a 'Pattern'.
124+
125+
See also: 'mapVariables'
126+
127+
-}
128+
traverseVariables
129+
:: forall m variable1 variable2
130+
. Monad m
131+
=> Ord variable2
132+
=> AdjSomeVariableName (variable1 -> m variable2)
133+
-> PredicatePattern variable1
134+
-> m (PredicatePattern variable2)
135+
traverseVariables adj = field @"freeVariables" (traverseFreeVariables adj)
136+
137+
{- | Delete the given variable from the set of free variables.
138+
-}
139+
deleteFreeVariable
140+
:: Ord variable
141+
=> SomeVariable variable
142+
-> PredicatePattern variable
143+
-> PredicatePattern variable
144+
deleteFreeVariable variable =
145+
Lens.over (field @"freeVariables") (bindVariable variable)
146+
147+
148+
instance HasFreeVariables (PredicatePattern variable) variable where
149+
freeVariables = freeVariables
150+
151+
fromPattern :: Pattern variable -> PredicatePattern variable
152+
fromPattern p =
153+
PredicatePattern (Pattern.freeVariables p) (Pattern.simplifiedAttribute p)

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

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -95,13 +95,13 @@ newSetCeilSimplifier
9595
(BuiltinAssocComm NormalizedSet variable)
9696
(OrCondition variable)
9797
newSetCeilSimplifier =
98-
CeilSimplifier $ \ceil@Ceil { ceilResultSort, ceilChild } -> do
98+
CeilSimplifier $ \ceil@Ceil { ceilChild } -> do
9999
let mkInternalAc normalizedAc =
100100
ceilChild { builtinAcChild = wrapAc normalizedAc }
101101
mkNotMember element termLike =
102102
mkInternalAc (fromElement element) { opaque = [termLike] }
103103
& TermLike.mkInternalSet
104-
& makeCeilPredicate ceilResultSort
104+
& makeCeilPredicate
105105
-- TODO (thomas.tuegel): Do not mark this simplified.
106106
-- Marking here may prevent user-defined axioms from applying.
107107
-- At present, we wouldn't apply such an axiom, anyway.
@@ -122,13 +122,13 @@ newMapCeilSimplifier
122122
(BuiltinAssocComm NormalizedMap variable)
123123
(OrCondition variable)
124124
newMapCeilSimplifier =
125-
CeilSimplifier $ \ceil@Ceil { ceilResultSort, ceilChild } -> do
125+
CeilSimplifier $ \ceil@Ceil { ceilChild } -> do
126126
let mkInternalAc normalizedAc =
127127
ceilChild { builtinAcChild = wrapAc normalizedAc }
128128
mkNotMember element termLike =
129129
mkInternalAc (fromElement element') { opaque = [termLike] }
130130
& TermLike.mkInternalMap
131-
& makeCeilPredicate ceilResultSort
131+
& makeCeilPredicate
132132
-- TODO (thomas.tuegel): Do not mark this simplified.
133133
-- Marking here may prevent user-defined axioms from applying.
134134
-- At present, we wouldn't apply such an axiom, anyway.
@@ -185,7 +185,7 @@ newBuiltinAssocCommCeilSimplifier
185185
(BuiltinAssocComm normalized variable)
186186
(OrCondition variable)
187187
newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
188-
CeilSimplifier $ \Ceil { ceilResultSort, ceilChild } -> do
188+
CeilSimplifier $ \Ceil { ceilChild } -> do
189189
let internalAc@InternalAc { builtinAcChild } = ceilChild
190190
sideCondition <- Reader.ask
191191
let normalizedAc = unwrapAc builtinAcChild
@@ -207,7 +207,7 @@ newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
207207
emptyNormalizedAc { opaque = [opaque1, opaque2] }
208208
}
209209
& mkBuiltin
210-
& makeCeilPredicate ceilResultSort
210+
& makeCeilPredicate
211211
-- TODO (thomas.tuegel): Do not mark this simplified.
212212
-- Marking here may prevent user-defined axioms from applying.
213213
-- At present, we wouldn't apply such an axiom, anyway.
@@ -240,7 +240,7 @@ newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
240240

241241
let makeEvaluateTerm, defineAbstractKey, defineOpaque
242242
:: TermLike variable -> MaybeT simplifier (OrCondition variable)
243-
makeEvaluateTerm = makeEvaluateTermCeil sideCondition ceilResultSort
243+
makeEvaluateTerm = makeEvaluateTermCeil sideCondition
244244
defineAbstractKey = makeEvaluateTerm
245245
defineOpaque = makeEvaluateTerm
246246

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

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -93,7 +93,7 @@ import Kore.Internal.Pattern as Pattern
9393
, withCondition
9494
)
9595
import Kore.Internal.Predicate
96-
( makeEqualsPredicate_
96+
( makeEqualsPredicate
9797
)
9898
import qualified Kore.Internal.Predicate as Predicate
9999
import qualified Kore.Internal.SideCondition as SideCondition
@@ -511,13 +511,12 @@ unifyEqualsUnsolved SimplificationType.And a b = do
511511
orCondition <-
512512
makeEvaluateTermCeil
513513
SideCondition.topTODO
514-
predicateSort
515514
unified
516515
predicate <- Monad.Unify.scatter orCondition
517516
return (unified `Pattern.withCondition` predicate)
518517
unifyEqualsUnsolved SimplificationType.Equals a b =
519518
return Pattern.top
520-
{predicate = Predicate.markSimplified $ makeEqualsPredicate_ a b}
519+
{predicate = Predicate.markSimplified $ makeEqualsPredicate a b}
521520

522521
makeDomainValueTerm
523522
:: InternalVariable variable

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -385,9 +385,9 @@ evalEq resultSort arguments@[_intLeft, _intRight] =
385385
empty
386386

387387
mkCeilUnlessDefined termLike
388-
| TermLike.isDefinedPattern termLike = Condition.topOf resultSort
388+
| TermLike.isDefinedPattern termLike = Condition.top
389389
| otherwise =
390-
Condition.fromPredicate (makeCeilPredicate resultSort termLike)
390+
Condition.fromPredicate (makeCeilPredicate termLike)
391391
returnPattern = return . flip Pattern.andCondition conditions
392392
conditions = foldMap mkCeilUnlessDefined arguments
393393

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ import Kore.Internal.Pattern
6161
)
6262
import qualified Kore.Internal.Pattern as Pattern
6363
import Kore.Internal.Predicate
64-
( makeCeilPredicate_
64+
( makeCeilPredicate
6565
)
6666
import qualified Kore.Internal.SideCondition as SideCondition
6767
import Kore.Internal.Symbol
@@ -258,7 +258,7 @@ unifyIfThenElse unifyChildren a b =
258258
worker a b <|> worker b a
259259
where
260260
takeCondition value condition' =
261-
makeCeilPredicate_ (mkAnd (Bool.asInternal sort value) condition')
261+
makeCeilPredicate (mkAnd (Bool.asInternal sort value) condition')
262262
& Condition.fromPredicate
263263
where
264264
sort = termLikeSort condition'

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

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -98,7 +98,6 @@ import qualified Kore.Internal.TermLike as TermLike
9898
import Kore.Sort
9999
( Sort
100100
)
101-
import qualified Kore.Sort as Sort
102101
import Kore.Step.Simplification.NotSimplifier
103102
import Kore.Step.Simplification.Simplify as Simplifier
104103
import Kore.Syntax.Sentence
@@ -340,9 +339,9 @@ evalInKeys resultSort arguments@[_key, _map] =
340339
emptyMap <|> concreteMap <|> symbolicMap
341340
where
342341
mkCeilUnlessDefined termLike
343-
| TermLike.isDefinedPattern termLike = Condition.topOf resultSort
342+
| TermLike.isDefinedPattern termLike = Condition.top
344343
| otherwise =
345-
Condition.fromPredicate (makeCeilPredicate resultSort termLike)
344+
Condition.fromPredicate (makeCeilPredicate termLike)
346345

347346
returnPattern = return . flip Pattern.andCondition conditions
348347
conditions = foldMap mkCeilUnlessDefined arguments
@@ -616,7 +615,7 @@ unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) a b =
616615

617616
defineTerm :: TermLike variable -> MaybeT unifier (Condition variable)
618617
defineTerm termLike =
619-
makeEvaluateTermCeil SideCondition.topTODO Sort.predicateSort termLike
618+
makeEvaluateTermCeil SideCondition.topTODO termLike
620619
>>= Unify.scatter
621620
& lift
622621

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -298,7 +298,7 @@ evalIn resultSort [_elem, _set] = do
298298
returnIfTrueAndDefined result setTerm
299299
| result = do
300300
let condition =
301-
Conditional.fromPredicate $ makeCeilPredicate resultSort setTerm
301+
Conditional.fromPredicate $ makeCeilPredicate setTerm
302302
trueWithCondition =
303303
Pattern.andCondition
304304
(asExpandedBoolPattern result)
@@ -347,7 +347,7 @@ evalDifference
347347
_set2 <- expectBuiltinSet ctx _set2
348348
let definedArgs =
349349
filter (not . TermLike.isDefinedPattern) args
350-
& map (makeCeilPredicate resultSort)
350+
& map makeCeilPredicate
351351
& makeMultipleAndPredicate
352352
& Conditional.fromPredicate
353353
let NormalizedAc

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -651,11 +651,11 @@ instance InternalVariable variable => Pretty (CheckRequiresError variable) where
651651
pretty checkRequiresError =
652652
Pretty.vsep
653653
[ "could not infer the equation requirement:"
654-
, Pretty.indent 4 (unparse equationRequires)
654+
, Pretty.indent 4 (pretty equationRequires)
655655
, "and the matching requirement:"
656-
, Pretty.indent 4 (unparse matchPredicate)
656+
, Pretty.indent 4 (pretty matchPredicate)
657657
, "from the side condition:"
658-
, Pretty.indent 4 (unparse sideCondition)
658+
, Pretty.indent 4 (pretty sideCondition)
659659
]
660660
where
661661
CheckRequiresError { matchPredicate, equationRequires, sideCondition } =

0 commit comments

Comments
 (0)