Skip to content

Commit 0fa22f7

Browse files
geo2arv-jenkins
geo2a
and
rv-jenkins
authored
Do not output attribute information when unparsing TermLike (#3823)
When pretty-printing a `TermLike`, the term attributes are serialized into text and in-lined into the unparsed Kore term, leading to results like this one: ``` Could not infer the equation requirement: /* Spa */ \equals{SortBool{}, _}( /* T Fn D Spa */ Lbl'Unds-LT-'Int'Unds'{}( /* T Fn D Spa */ Lblf'LParUndsRParUnds'TEST'Unds'Int'Unds'Int{}( /* T Fn D Sfa */ ConfigVarI:SortInt{} ), /* T Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* T Fn D Sfa Cl */ \dv{SortBool{}}("true") ) ``` I'd argue that we do not care as much about the exact attributes of `TermLike`s anymore today. Therefore I propose to remove the attributes, leading to a much cleaner log output: ``` Could not infer the equation requirement: \equals{SortBool{}, _}( Lbl'Unds-LT-'Int'Unds'{}( Lblf'LParUndsRParUnds'TEST'Unds'Int'Unds'Int{}( ConfigVarI:SortInt{} ), \dv{SortInt{}}("0") ), \dv{SortBool{}}("true") ) ``` The integration tests fail, but I will fix them once we have decided if we want this merged. --------- Co-authored-by: rv-jenkins <[email protected]>
1 parent 588f287 commit 0fa22f7

File tree

50 files changed

+78
-1901
lines changed

Some content is hidden

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

50 files changed

+78
-1901
lines changed

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

Lines changed: 1 addition & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -79,7 +79,6 @@ import Kore.Attribute.Pattern.FreeVariables qualified as Attribute.FreeVariables
7979
import Kore.Attribute.Pattern.FreeVariables qualified as FreeVariables
8080
import Kore.Attribute.Pattern.Function qualified as Attribute
8181
import Kore.Attribute.Pattern.Simplified qualified as Attribute
82-
import Kore.Attribute.Pattern.Simplified qualified as Attribute.Simplified
8382
import Kore.Attribute.Pattern.Total qualified as Attribute
8483
import Kore.Attribute.Synthetic
8584
import Kore.Builtin.Encoding qualified as Encoding
@@ -548,12 +547,6 @@ attributeSimplifiedAttribute ::
548547
attributeSimplifiedAttribute patt@TermAttributes{termSimplified} =
549548
assertSimplifiedConsistency patt termSimplified
550549

551-
constructorLikeAttribute ::
552-
TermAttributes variable ->
553-
Attribute.ConstructorLike
554-
constructorLikeAttribute TermAttributes{termConstructorLike} =
555-
termConstructorLike
556-
557550
{- Checks whether the pattern is simplified relative to the given side
558551
condition.
559552
-}
@@ -710,54 +703,13 @@ instance (Unparse variable, Ord variable) => Unparse (TermLike variable) where
710703
| Attribute.hasKnownCreator termCreated ->
711704
Pretty.sep
712705
[ Pretty.pretty termCreated
713-
, attributeRepresentation
714706
, unparse termLikeF
715707
]
716708
| otherwise ->
717-
Pretty.sep [attributeRepresentation, unparse termLikeF]
709+
unparse termLikeF
718710
where
719711
TermAttributes{termCreated} = attrs
720712

721-
attributeRepresentation = case attrs of
722-
(TermAttributes _ _ _ _ _ _ _ _) ->
723-
Pretty.surround
724-
(Pretty.hsep $ map Pretty.pretty representation)
725-
"/* "
726-
" */"
727-
where
728-
representation =
729-
addTotalRepresentation $
730-
addFunctionRepresentation $
731-
addDefinedRepresentation $
732-
addSimplifiedRepresentation $
733-
addConstructorLikeRepresentation []
734-
addTotalRepresentation
735-
| Attribute.isTotal $ termTotal attrs = ("T" :)
736-
| otherwise = id
737-
addFunctionRepresentation
738-
| Attribute.isFunction $ termFunction attrs = ("Fn" :)
739-
| otherwise = id
740-
addDefinedRepresentation
741-
| Attribute.isDefined $ termDefined attrs = ("D" :)
742-
| otherwise = id
743-
addSimplifiedRepresentation =
744-
case simplifiedTag of
745-
Just result -> (result :)
746-
Nothing -> id
747-
where
748-
simplifiedTag =
749-
Attribute.Simplified.unparseTag
750-
(attributeSimplifiedAttribute attrs)
751-
addConstructorLikeRepresentation =
752-
case constructorLike of
753-
Just Attribute.ConstructorLikeHead -> ("Cl" :)
754-
Just Attribute.SortInjectionHead -> ("Cli" :)
755-
Nothing -> id
756-
where
757-
constructorLike =
758-
Attribute.getConstructorLike
759-
(constructorLikeAttribute attrs)
760-
761713
unparse2 term =
762714
case Recursive.project term of
763715
(_ :< pat) -> unparse2 pat

‎kore/test/Test/Kore/Builtin/InternalBytes.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -712,7 +712,7 @@ test_unparse =
712712
[ testCase "unparse using 8-bit encoding" $ do
713713
let input = asInternal "\x00" :: TermLike RewritingVariableName
714714
actual = (show . unparse) input
715-
expect = "/* T Fn D Sfa Cl */ \\dv{Bytes{}}(\"\\x00\")"
715+
expect = "\\dv{Bytes{}}(\"\\x00\")"
716716
assertEqual "" expect actual
717717
]
718718

‎kore/test/Test/Kore/Unification/Unifier.hs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -406,15 +406,15 @@ test_unification =
406406
(UnificationTerm a)
407407
(UnificationTerm dv2)
408408
"Cannot handle Constructor and DomainValue:\n\
409-
\/* T Fn D Sfa Cl */ a{}()\n\
410-
\/* T Fn D Sfa Cl */ \\dv{testSort{}}(/* T Fn D Sfa Cl */ \"dv2\")\n"
409+
\a{}()\n\
410+
\\\dv{testSort{}}(\"dv2\")\n"
411411
, andSimplifyException
412412
"Unmatching domain value + constructor constant"
413413
(UnificationTerm dv1)
414414
(UnificationTerm a)
415415
"Cannot handle DomainValue and Constructor:\n\
416-
\/* T Fn D Sfa Cl */ \\dv{testSort{}}(/* T Fn D Sfa Cl */ \"dv1\")\n\
417-
\/* T Fn D Sfa Cl */ a{}()\n"
416+
\\\dv{testSort{}}(\"dv1\")\n\
417+
\a{}()\n"
418418
, testCase "Unmatching domain value + nonconstructor constant" $
419419
andSimplify
420420
(UnificationTerm dv1)

‎test/imp/sum-save-proofs-spec.k.save-proofs.kore.golden

Lines changed: 22 additions & 94 deletions
Original file line numberDiff line numberDiff line change
@@ -2,98 +2,56 @@
22
module haskell-backend-saved-claims-43943e50-f723-47cd-99fd-07104d664c6d
33
import IMP []
44
import kore []
5-
claim {} /* Spa */
6-
\implies{SortGeneratedTopCell{}}(
7-
/* Spa */
5+
claim {} \implies{SortGeneratedTopCell{}}(
86
\and{SortGeneratedTopCell{}}(
9-
/* Spa */
107
\equals{SortBool{}, SortGeneratedTopCell{}}(
11-
/* T Fn D Sfa Cl */ \dv{SortBool{}}("true"),
12-
/* T Fn D Spa */
8+
\dv{SortBool{}}("true"),
139
Lbl'Unds-GT-Eqls'Int'Unds'{}(
14-
/* T Fn D Sfa */ VarN:SortInt{},
15-
/* T Fn D Sfa Cl */ \dv{SortInt{}}("0")
10+
VarN:SortInt{},
11+
\dv{SortInt{}}("0")
1612
)
1713
),
18-
/* T Fn D Spa */
1914
Lbl'-LT-'generatedTop'-GT-'{}(
20-
/* T Fn D Spa */
2115
Lbl'-LT-'T'-GT-'{}(
22-
/* T Fn D Spa */
2316
Lbl'-LT-'k'-GT-'{}(
24-
/* T Fn D Spa */
2517
kseq{}(
26-
/* T Fn D Sfa Cli */
2718
/* Inj: */ inj{SortStmt{}, SortKItem{}}(
28-
/* T Fn D Sfa Cl */
2919
Lblwhile'LParUndsRParUndsUnds'IMP-SYNTAX'Unds'Stmt'Unds'BExp'Unds'Block{}(
30-
/* T Fn D Sfa Cl */
3120
Lbl'BangUndsUnds'IMP-SYNTAX'Unds'BExp'Unds'BExp{}(
32-
/* T Fn D Sfa Cl */
3321
Lbl'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'Unds'BExp'Unds'AExp'Unds'AExp{}(
34-
/* T Fn D Sfa Cli */
3522
/* Inj: */ inj{SortId{}, SortAExp{}}(
36-
/* T Fn D Sfa Cl */
37-
\dv{SortId{}}(/* T Fn D Sfa Cl */
38-
"n")
23+
\dv{SortId{}}("n")
3924
),
40-
/* T Fn D Sfa Cli */
4125
/* Inj: */ inj{SortInt{}, SortAExp{}}(
42-
/* T Fn D Sfa Cl */
4326
\dv{SortInt{}}("0")
4427
)
4528
)
4629
),
47-
/* T Fn D Sfa Cl */
4830
Lbl'LBraUndsRBraUnds'IMP-SYNTAX'Unds'Block'Unds'Stmt{}(
49-
/* T Fn D Sfa Cl */
5031
Lbl'UndsUndsUnds'IMP-SYNTAX'Unds'Stmt'Unds'Stmt'Unds'Stmt{}(
51-
/* T Fn D Sfa Cl */
5232
Lbl'UndsEqlsUndsSClnUnds'IMP-SYNTAX'Unds'Stmt'Unds'Id'Unds'AExp{}(
53-
/* T Fn D Sfa Cl */
54-
\dv{SortId{}}(/* T Fn D Sfa Cl */
55-
"sum"),
56-
/* T Fn D Sfa Cl */
33+
\dv{SortId{}}("sum"),
5734
Lbl'UndsPlusUndsUnds'IMP-SYNTAX'Unds'AExp'Unds'AExp'Unds'AExp{}(
58-
/* T Fn D Sfa Cl */
5935
Lbl'UndsPlusUndsUnds'IMP-SYNTAX'Unds'AExp'Unds'AExp'Unds'AExp{}(
60-
/* T Fn D Sfa Cli */
6136
/* Inj: */ inj{SortId{}, SortAExp{}}(
62-
/* T Fn D Sfa Cl */
63-
\dv{SortId{}}(/* T Fn D Sfa Cl */
64-
"sum")
37+
\dv{SortId{}}("sum")
6538
),
66-
/* T Fn D Sfa Cli */
6739
/* Inj: */ inj{SortId{}, SortAExp{}}(
68-
/* T Fn D Sfa Cl */
69-
\dv{SortId{}}(/* T Fn D Sfa Cl */
70-
"n")
40+
\dv{SortId{}}("n")
7141
)
7242
),
73-
/* T Fn D Sfa Cli */
7443
/* Inj: */ inj{SortId{}, SortAExp{}}(
75-
/* T Fn D Sfa Cl */
76-
\dv{SortId{}}(/* T Fn D Sfa Cl */
77-
"n")
44+
\dv{SortId{}}("n")
7845
)
7946
)
8047
),
81-
/* T Fn D Sfa Cl */
8248
Lbl'UndsEqlsUndsSClnUnds'IMP-SYNTAX'Unds'Stmt'Unds'Id'Unds'AExp{}(
83-
/* T Fn D Sfa Cl */
84-
\dv{SortId{}}(/* T Fn D Sfa Cl */
85-
"n"),
86-
/* T Fn D Sfa Cl */
49+
\dv{SortId{}}("n"),
8750
Lbl'UndsPlusUndsUnds'IMP-SYNTAX'Unds'AExp'Unds'AExp'Unds'AExp{}(
88-
/* T Fn D Sfa Cli */
8951
/* Inj: */ inj{SortId{}, SortAExp{}}(
90-
/* T Fn D Sfa Cl */
91-
\dv{SortId{}}(/* T Fn D Sfa Cl */
92-
"n")
52+
\dv{SortId{}}("n")
9353
),
94-
/* T Fn D Sfa Cli */
9554
/* Inj: */ inj{SortInt{}, SortAExp{}}(
96-
/* T Fn D Sfa Cl */
9755
\dv{SortInt{}}("-1")
9856
)
9957
)
@@ -102,101 +60,71 @@ module haskell-backend-saved-claims-43943e50-f723-47cd-99fd-07104d664c6d
10260
)
10361
)
10462
),
105-
/* T Fn D Sfa */ Var'Unds'DotVar2:SortK{}
63+
Var'Unds'DotVar2:SortK{}
10664
)
10765
),
108-
/* T Fn D Spa */
10966
Lbl'-LT-'state'-GT-'{}(
110-
/* T Fn D Spa */
11167
/* InternalMap: */ Lbl'Unds'Map'Unds'{}(
11268
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
11369
/* Inj: */ inj{SortId{}, SortKItem{}}(
11470
\dv{SortId{}}("n")
11571
),
116-
/* T Fn D Spa */
11772
/* Inj: */ inj{SortInt{}, SortKItem{}}(
118-
/* T Fn D Sfa */ VarN:SortInt{}
73+
VarN:SortInt{}
11974
)
12075
),
12176
/* concrete element: */ Lbl'UndsPipe'-'-GT-Unds'{}(
12277
/* Inj: */ inj{SortId{}, SortKItem{}}(
12378
\dv{SortId{}}("sum")
12479
),
125-
/* T Fn D Spa */
12680
/* Inj: */ inj{SortInt{}, SortKItem{}}(
127-
/* T Fn D Sfa */ VarS:SortInt{}
81+
VarS:SortInt{}
12882
)
12983
)
13084
)
13185
)
13286
),
133-
/* T Fn D Spa */
134-
Lbl'-LT-'generatedCounter'-GT-'{}(
135-
/* T Fn D Sfa */ Var'Unds'Gen0:SortInt{}
136-
)
87+
Lbl'-LT-'generatedCounter'-GT-'{}(Var'Unds'Gen0:SortInt{})
13788
)
13889
),
139-
/* Spa */
14090
weakAlwaysFinally{SortGeneratedTopCell{}}(
141-
/* Spa */
14291
\exists{SortGeneratedTopCell{}}(
14392
Var'QuesUnds'Gen1:SortInt{},
144-
/* Fn Spa */
14593
Lbl'-LT-'generatedTop'-GT-'{}(
146-
/* Fn Spa */
14794
Lbl'-LT-'T'-GT-'{}(
148-
/* T Fn D Spa */
149-
Lbl'-LT-'k'-GT-'{}(
150-
/* T Fn D Sfa */ Var'Unds'DotVar2:SortK{}
151-
),
152-
/* Fn Spa */
95+
Lbl'-LT-'k'-GT-'{}(Var'Unds'DotVar2:SortK{}),
15396
Lbl'-LT-'state'-GT-'{}(
154-
/* Fn Spa */
15597
Lbl'Unds'Map'Unds'{}(
156-
/* T Fn D Spa */
15798
Lbl'UndsPipe'-'-GT-Unds'{}(
158-
/* T Fn D Sfa Cli */
15999
/* Inj: */ inj{SortId{}, SortKItem{}}(
160-
/* T Fn D Sfa Cl */
161-
\dv{SortId{}}(/* T Fn D Sfa Cl */ "n")
100+
\dv{SortId{}}("n")
162101
),
163-
/* T Fn D Sfa Cli */
164102
/* Inj: */ inj{SortInt{}, SortKItem{}}(
165-
/* T Fn D Sfa Cl */ \dv{SortInt{}}("0")
103+
\dv{SortInt{}}("0")
166104
)
167105
),
168-
/* T Fn D Spa */
169106
Lbl'UndsPipe'-'-GT-Unds'{}(
170-
/* T Fn D Sfa Cli */
171107
/* Inj: */ inj{SortId{}, SortKItem{}}(
172-
/* T Fn D Sfa Cl */
173-
\dv{SortId{}}(/* T Fn D Sfa Cl */ "sum")
108+
\dv{SortId{}}("sum")
174109
),
175-
/* T Fn D Spa */
176110
/* Inj: */ inj{SortInt{}, SortKItem{}}(
177-
/* T Fn D Spa */
178111
Lbl'UndsPlus'Int'Unds'{}(
179-
/* T Fn D Sfa */ VarS:SortInt{},
180-
/* T Fn D Spa */
112+
VarS:SortInt{},
181113
Lbl'UndsStar'Int'Unds'{}(
182-
/* T Fn D Spa */
183114
Lbl'UndsPlus'Int'Unds'{}(
184-
/* T Fn D Sfa */
185115
VarN:SortInt{},
186-
/* T Fn D Sfa Cl */
187116
\dv{SortInt{}}("1")
188117
),
189-
/* T Fn D Sfa */ VarN:SortInt{}
118+
VarN:SortInt{}
190119
)
191120
)
192121
)
193122
)
194123
)
195124
)
196125
),
197-
/* T Fn D Spa */
198126
Lbl'-LT-'generatedCounter'-GT-'{}(
199-
/* T Fn D Sfa */ Var'QuesUnds'Gen1:SortInt{}
127+
Var'QuesUnds'Gen1:SortInt{}
200128
)
201129
)
202130
)

0 commit comments

Comments
 (0)