Skip to content

Commit 636cda8

Browse files
committed
Merge remote-tracking branch 'origin/master' into release
2 parents b811bc3 + b5d3b9f commit 636cda8

23 files changed

+3814
-1987
lines changed

booster/library/Booster/Definition/Util.hs

Lines changed: 5 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ import Booster.Definition.Attributes.Base
3030
import Booster.Definition.Base
3131
import Booster.Definition.Ceil (ComputeCeilSummary (..))
3232
import Booster.Pattern.Base
33-
import Booster.Pattern.Index (CellIndex (..), TermIndex (..))
33+
import Booster.Pattern.Index (TermIndex (..))
3434
import Booster.Pattern.Pretty
3535
import Booster.Prettyprinter
3636
import Booster.Util
@@ -111,16 +111,16 @@ instance Pretty Summary where
111111
: tableView prettyLabel prettyLabel summary.subSorts
112112
)
113113
<> ( "Rewrite rules by term index:"
114-
: tableView prettyTermIndex pretty summary.rewriteRules
114+
: tableView pretty pretty summary.rewriteRules
115115
)
116116
<> ( "Function equations by term index:"
117-
: tableView prettyTermIndex pretty summary.functionRules
117+
: tableView pretty pretty summary.functionRules
118118
)
119119
<> ( "Simplifications by term index:"
120-
: tableView prettyTermIndex pretty summary.simplifications
120+
: tableView pretty pretty summary.simplifications
121121
)
122122
<> ( "Ceils:"
123-
: tableView prettyTermIndex prettyCeilRule summary.ceils
123+
: tableView pretty prettyCeilRule summary.ceils
124124
)
125125
<> [mempty]
126126
where
@@ -140,13 +140,6 @@ instance Pretty Summary where
140140

141141
prettyLabel = either error (pretty . BS.unpack) . decodeLabel
142142

143-
prettyTermIndex :: TermIndex -> Doc a
144-
prettyTermIndex (TermIndex ixs) = Pretty.sep $ map prettyCellIndex ixs
145-
146-
prettyCellIndex Anything = "Anything"
147-
prettyCellIndex (TopSymbol sym) = prettyLabel sym
148-
prettyCellIndex None = "None"
149-
150143
prettyCeilRule :: RewriteRule r -> Doc a
151144
prettyCeilRule RewriteRule{lhs, rhs} =
152145
"#Ceil(" <+> pretty' @['Decoded, 'Truncated] lhs <+> ") =>" <+> pretty' @['Decoded, 'Truncated] rhs

booster/library/Booster/Pattern/ApplyEquations.hs

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -802,7 +802,7 @@ applyEquations theory handler term = do
802802
withContext CtxAbort $ logMessage ("Index 'None'" :: Text)
803803
throw (IndexIsNone term)
804804
let
805-
indexes = Set.toList $ Idx.coveringIndexes index
805+
indexes = Set.toList $ Map.keysSet theory `Idx.covering` index
806806
equationsFor i = fromMaybe Map.empty $ Map.lookup i theory
807807
-- neither simplification nor function equations should need groups,
808808
-- since simplification priority is just a suggestion and function equations
@@ -1172,7 +1172,9 @@ simplifyConstraint' :: LoggerMIO io => Bool -> Term -> EquationT io Term
11721172
-- 'true \equals P' using simplifyBool if they are concrete, or using
11731173
-- evaluateTerm.
11741174
simplifyConstraint' recurseIntoEvalBool = \case
1175-
t@(Term TermAttributes{canBeEvaluated} _)
1175+
t@(Term TermAttributes{isEvaluated, canBeEvaluated} _)
1176+
| isEvaluated ->
1177+
pure t
11761178
| isConcrete t && canBeEvaluated -> do
11771179
mbApi <- (.llvmApi) <$> getConfig
11781180
case mbApi of

booster/library/Booster/Pattern/Index.hs

Lines changed: 129 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -7,34 +7,48 @@ Everything to do with term indexing.
77
module Booster.Pattern.Index (
88
CellIndex (..),
99
TermIndex (..),
10+
-- Flat lattice
11+
(^<=^),
12+
invert,
13+
-- compute index cover for rule selection
14+
covering,
15+
-- indexing
1016
compositeTermIndex,
1117
kCellTermIndex,
1218
termTopIndex,
13-
coveringIndexes,
19+
-- helpers
1420
hasNone,
21+
noFunctions,
1522
) where
1623

1724
import Control.Applicative (Alternative (..), asum)
1825
import Control.DeepSeq (NFData)
26+
import Data.ByteString.Char8 (ByteString, unpack)
1927
import Data.Functor.Foldable (embed, para)
2028
import Data.Maybe (fromMaybe)
2129
import Data.Set (Set)
2230
import Data.Set qualified as Set
2331
import GHC.Generics (Generic)
32+
import Prettyprinter (Doc, Pretty, pretty, sep)
2433

2534
import Booster.Pattern.Base
35+
import Booster.Util (decodeLabel)
2636

2737
{- | Index data allowing for a quick lookup of potential axioms.
2838
2939
A @Term@ is indexed by inspecting the top term component of one or
3040
more given cells. A @TermIndex@ is a list of @CellIndex@es.
3141
32-
The @CellIndex@ of a cell containing a @SymbolApplication@ node is the
33-
symbol at the top. Other terms that are not symbol applications have
34-
index @Anything@.
42+
The @CellIndex@ of a cell reflects the top constructor of the term.
43+
For @SymbolApplication@s, constructors and functions are distinguished,
44+
for @DomainValue@s, the actual value (as a string) is part of the index.
45+
Internalised collections have special indexes, Variables have index @Anything@.
46+
47+
NB Indexes are _unsorted_. For instance, @IdxVal "42"@ is the index of
48+
both String "42" _and_ Integer 42.
3549
3650
Rather than making the term indexing function partial, we introduce a
37-
unique bottom element @None@ to the index type (to make it a lattice).
51+
unique bottom element @IdxNone@ to the index type (to make it a lattice).
3852
This can then handle @AndTerm@ by indexing both arguments and
3953
combining them.
4054
@@ -47,52 +61,117 @@ newtype TermIndex = TermIndex [CellIndex]
4761
deriving anyclass (NFData)
4862

4963
data CellIndex
50-
= None -- bottom element
51-
| TopSymbol SymbolName
64+
= IdxNone -- bottom element
65+
| IdxCons SymbolName
66+
| IdxFun SymbolName
67+
| IdxVal ByteString
68+
| IdxMap
69+
| IdxList
70+
| IdxSet
5271
| Anything -- top element
53-
-- should we have | Value Sort ?? (see Term type)
5472
deriving stock (Eq, Ord, Show, Generic)
5573
deriving anyclass (NFData)
5674

57-
{- | Combines two indexes (an "infimum" function on the index lattice).
75+
{- | Index lattice class. This is mostly just a _flat lattice_ but also
76+
needs to support a special 'invert' method for the subject term index.
77+
-}
78+
class IndexLattice a where
79+
(^<=^) :: a -> a -> Bool
80+
81+
invert :: a -> a
82+
83+
{- | Partial less-or-equal for CellIndex (implies partial order)
84+
85+
Anything
86+
____________/ | \_______________________________________...
87+
/ / | | \ \
88+
IdxList ..IdxSet IdxVal "x"..IdxVal "y" IdxCons "A".. IdxFun "f"..
89+
\_________|__ | _______|____________|____________/____...
90+
\ | /
91+
IdxNone
92+
-}
93+
instance IndexLattice CellIndex where
94+
IdxNone ^<=^ _ = True
95+
a ^<=^ IdxNone = a == IdxNone
96+
_ ^<=^ Anything = True
97+
Anything ^<=^ a = a == Anything
98+
a ^<=^ b = a == b
99+
100+
invert IdxNone = Anything
101+
invert Anything = IdxNone
102+
invert a = a
103+
104+
-- | Partial less-or-equal for TermIndex (product lattice)
105+
instance IndexLattice TermIndex where
106+
TermIndex idxs1 ^<=^ TermIndex idxs2 = and $ zipWith (^<=^) idxs1 idxs2
107+
108+
invert (TermIndex idxs) = TermIndex (map invert idxs)
109+
110+
{- | Combines two indexes ("infimum" or "meet" function on the index lattice).
58111
59112
This is useful for terms containing an 'AndTerm': Any term that
60113
matches an 'AndTerm t1 t2' must match both 't1' and 't2', so 't1'
61114
and 't2' must have "compatible" indexes for this to be possible.
62115
-}
63116
instance Semigroup CellIndex where
64-
None <> _ = None
65-
_ <> None = None
117+
IdxNone <> _ = IdxNone
118+
_ <> IdxNone = IdxNone
66119
x <> Anything = x
67120
Anything <> x = x
68-
s@(TopSymbol s1) <> TopSymbol s2
69-
| s1 == s2 = s
70-
| otherwise = None -- incompatible indexes
121+
idx1 <> idx2
122+
| idx1 == idx2 = idx1
123+
| otherwise = IdxNone
71124

72-
{- | Compute all indexes that cover the given index, for rule lookup.
125+
-- | Pretty instances
126+
instance Pretty TermIndex where
127+
pretty (TermIndex ixs) = sep $ map pretty ixs
73128

74-
An index B is said to "cover" another index A if all parts of B are
75-
either equal to the respective parts of A, or 'Anything'.
129+
instance Pretty CellIndex where
130+
pretty IdxNone = "_|_"
131+
pretty Anything = "***"
132+
pretty (IdxCons sym) = "C--" <> prettyLabel sym
133+
pretty (IdxFun sym) = "F--" <> prettyLabel sym
134+
pretty (IdxVal sym) = "V--" <> prettyLabel sym
135+
pretty IdxMap = "Map"
136+
pretty IdxList = "List"
137+
pretty IdxSet = "Set"
76138

77-
When selecting candidate rules for a term, we must consider all
78-
rules whose index has either the exact same @CellIndex@ or
79-
@Anything@ at every position of their @TermIndex@.
80-
-}
81-
coveringIndexes :: TermIndex -> Set TermIndex
82-
coveringIndexes (TermIndex ixs) =
83-
Set.fromList . map TermIndex $ orAnything ixs
84-
where
85-
orAnything :: [CellIndex] -> [[CellIndex]]
86-
orAnything [] = [[]]
87-
orAnything (i : is) =
88-
let rest = orAnything is
89-
in map (i :) rest <> map (Anything :) rest
139+
prettyLabel :: ByteString -> Doc a
140+
prettyLabel = either error (pretty . unpack) . decodeLabel
90141

91-
{- | Check whether a @TermIndex@ has @None@ in any position (this
142+
{- | Check whether a @TermIndex@ has @IdxNone@ in any position (this
92143
means no match will be possible).
93144
-}
94145
hasNone :: TermIndex -> Bool
95-
hasNone (TermIndex ixs) = None `elem` ixs
146+
hasNone (TermIndex ixs) = IdxNone `elem` ixs
147+
148+
-- | turns IdxFun _ into Anything (for rewrite rule selection)
149+
noFunctions :: TermIndex -> TermIndex
150+
noFunctions (TermIndex ixs) = TermIndex (map funsAnything ixs)
151+
where
152+
funsAnything IdxFun{} = Anything
153+
funsAnything other = other
154+
155+
{- | Computes all indexes that "cover" the given index, for rule lookup.
156+
157+
An index B is said to "cover" an index A if all components of B are
158+
greater or equal to those of the respective component of A inverted.
159+
160+
* For components of A that are distinct from @Anything@, this means
161+
the component of B is equal to that of A or @Anything@.
162+
* For components of A that are @IdxNone@, the respective component of B
163+
_must_ be @Anything@. However, if A contains @IdxNone@ no match is
164+
possible anyway.
165+
* For components of A that are @Anything@, B can contain an
166+
arbitrary index (@IdxNone@ will again have no chance of a match,
167+
though).
168+
169+
When selecting candidate rules for a term, we must consider all
170+
rules whose index has either the exact same @CellIndex@ or
171+
@Anything@ at every position of their @TermIndex@.
172+
-}
173+
covering :: Set TermIndex -> TermIndex -> Set TermIndex
174+
covering prior ix = Set.filter (invert ix ^<=^) prior
96175

97176
-- | Indexes a term by the heads of K sequences in given cells.
98177
compositeTermIndex :: [SymbolName] -> Term -> TermIndex
@@ -162,11 +241,25 @@ stripSortInjections = \case
162241
termTopIndex :: Term -> TermIndex
163242
termTopIndex = TermIndex . (: []) . cellTopIndex
164243

244+
-- | Cell top indexes form a lattice with a flat partial ordering
165245
cellTopIndex :: Term -> CellIndex
166246
cellTopIndex = \case
167-
SymbolApplication symbol _ _ ->
168-
TopSymbol symbol.name
247+
ConsApplication symbol _ _ ->
248+
IdxCons symbol.name
249+
FunctionApplication symbol _ _ ->
250+
IdxFun symbol.name
251+
DomainValue _ v ->
252+
IdxVal v
253+
Var{} ->
254+
Anything
255+
KMap{} ->
256+
IdxMap
257+
KList{} ->
258+
IdxList
259+
KSet{} ->
260+
IdxSet
261+
-- look-through
262+
Injection _ _ t ->
263+
cellTopIndex t
169264
AndTerm t1 t2 ->
170265
cellTopIndex t1 <> cellTopIndex t2
171-
_other ->
172-
Anything

booster/library/Booster/Pattern/Rewrite.hs

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -179,7 +179,13 @@ rewriteStep cutLabels terminalLabels pat = do
179179
termIdx = getIndex pat.term
180180
when (Idx.hasNone termIdx) $ throw (TermIndexIsNone pat.term)
181181
let
182-
indexes = Set.toList $ Idx.coveringIndexes termIdx
182+
indexes =
183+
Set.toList $ Map.keysSet def.rewriteTheory `Idx.covering` Idx.noFunctions termIdx
184+
-- Function calls in the index have to be generalised to
185+
-- `Anything` for rewriting because they may evaluate to any
186+
-- category of terms. If there are any function calls in the
187+
-- subject, the rewrite can only succeed if the function call
188+
-- is matched to a variable.
183189
rulesFor i = fromMaybe Map.empty $ Map.lookup i def.rewriteTheory
184190
rules =
185191
map snd . Map.toAscList . Map.unionsWith (<>) $ map rulesFor indexes
@@ -761,7 +767,7 @@ data RewriteFailed k
761767
RewriteSortError (RewriteRule k) Term SortError
762768
| -- | An error was detected during matching
763769
InternalMatchError Text
764-
| -- | Term has index 'None', no rule should apply
770+
| -- | Term has index 'IdxNone', no rule should apply
765771
TermIndexIsNone Term
766772
deriving stock (Eq, Show)
767773

@@ -817,7 +823,7 @@ instance FromModifiersT mods => Pretty (PrettyWithModifiers mods (RewriteFailed
817823
, pretty $ show sortError
818824
]
819825
TermIndexIsNone term ->
820-
"Term index is None for term " <> pretty' @mods term
826+
"Term index is IdxNone for term " <> pretty' @mods term
821827
InternalMatchError err -> "An internal error occured" <> pretty err
822828

823829
ruleLabelOrLoc :: RewriteRule k -> Doc a

booster/test/internalisation/bool.kore.report

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -18,37 +18,37 @@ Subsorts:
1818
- SortBool: SortBool
1919
Rewrite rules by term index:
2020
Function equations by term index:
21-
- Lbl_=/=Bool_: /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (960, 8)
22-
- Lbl_andBool_: 4
21+
- F--Lbl_=/=Bool_: /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (960, 8)
22+
- F--Lbl_andBool_: 4
2323
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (933, 8)
2424
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (932, 8)
2525
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (934, 8)
2626
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (931, 8)
27-
- Lbl_andThenBool_: 4
27+
- F--Lbl_andThenBool_: 4
2828
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (938, 8)
2929
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (937, 8)
3030
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (939, 8)
3131
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (936, 8)
32-
- Lbl_impliesBool_: 4
32+
- F--Lbl_impliesBool_: 4
3333
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (958, 8)
3434
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (957, 8)
3535
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (956, 8)
3636
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (955, 8)
37-
- Lbl_orBool_: 4
37+
- F--Lbl_orBool_: 4
3838
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (948, 8)
3939
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (946, 8)
4040
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (947, 8)
4141
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (945, 8)
42-
- Lbl_orElseBool_: 4
42+
- F--Lbl_orElseBool_: 4
4343
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (953, 8)
4444
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (951, 8)
4545
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (952, 8)
4646
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (950, 8)
47-
- Lbl_xorBool_: 3
47+
- F--Lbl_xorBool_: 3
4848
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (943, 8)
4949
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (942, 8)
5050
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (941, 8)
51-
- LblnotBool_: 2
51+
- F--LblnotBool_: 2
5252
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (929, 8)
5353
- /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md : (928, 8)
5454
Simplifications by term index:

0 commit comments

Comments
 (0)