Skip to content

Fix Ac Unification error and Add new integration test #2493

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 12 commits into from
Mar 26, 2021
Merged

Fix Ac Unification error and Add new integration test #2493

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
57e0cd4
added new integration test and removed sort check on internalization
MirceaS Mar 20, 2021
b3dc5f0
Merge branch 'master' into 2378
MirceaS Mar 20, 2021
0f8e890
Format with fourmolu
MirceaS Mar 20, 2021
59ebd44
made a pattern match more strict
MirceaS Mar 23, 2021
75cda60
addressed PR comments
MirceaS Mar 23, 2021
6a470e3
fixed golden file
MirceaS Mar 23, 2021
5d0d7cf
Merge branch 'master' into 2378
MirceaS Mar 23, 2021
d8f4384
Format with fourmolu
MirceaS Mar 23, 2021
afd3c55
refactored a pattern match
MirceaS Mar 25, 2021
9536110
Format with fourmolu
MirceaS Mar 25, 2021
4089366
empty commit for test runs
MirceaS Mar 26, 2021
a848905
Merge branch 'master' into 2378
rv-jenkins Mar 26, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions kore/src/Kore/Builtin/AssociativeCommutative.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -803,13 +803,13 @@ unifyEqualsNormalizedAc
allElements1
allElements2
Nothing
([opaque], []) ->
([opaque@(ElemVar_ _)], []) ->
lift $
unifyEqualsElementLists'
allElements1
allElements2
(Just opaque)
([], [opaque]) ->
([], [opaque@(ElemVar_ _)]) ->
lift $
unifyEqualsElementLists'
allElements2
Expand Down Expand Up @@ -1320,6 +1320,8 @@ unifyEqualsElementLists
, Pretty.indent 4 (unparse first)
, Pretty.indent 2 "second="
, Pretty.indent 4 (unparse second)
, Pretty.indent 2 "opaque="
, Pretty.indent 4 (unparse opaque)
]
where
unifyWithPermutations =
Expand Down
7 changes: 3 additions & 4 deletions kore/src/Kore/Builtin/Map.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -499,10 +499,9 @@ internalize ::
TermLike variable ->
TermLike variable
internalize tools termLike
| fromMaybe False (isMapSort tools sort')
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are we just removing this check because it is redundant? Or is there another reason?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is the check that I asked you about the other day, the one that Evan removed in his PR that I then had to revert. You suggested I leave it in even if it doesn't solve the Issue linked to this PR.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, that is not the check I thought you were removing. It is redundant, and I'm glad to be rid of it, but it doesn't have anything to do with this issue in particular.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So, is it fine to leave it in this PR or should I open a new PR?

, -- Ac.toNormalized is greedy about 'normalizing' opaque terms, we should only
-- apply it if we know the term head is a constructor-like symbol.
App_ symbol _ <- termLike
-- Ac.toNormalized is greedy about 'normalizing' opaque terms, we should only
-- apply it if we know the term head is a constructor-like symbol.
| App_ symbol _ <- termLike
, isConstructorModulo_ symbol =
case Ac.toNormalized @NormalizedMap termLike of
Ac.Bottom -> TermLike.mkBottom sort'
Expand Down
7 changes: 3 additions & 4 deletions kore/src/Kore/Builtin/Set.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -501,10 +501,9 @@ internalize ::
TermLike variable ->
TermLike variable
internalize tools termLike
| fromMaybe False (isSetSort tools sort')
, -- Ac.toNormalized is greedy about 'normalizing' opaque terms, we should only
-- apply it if we know the term head is a constructor-like symbol.
App_ symbol _ <- termLike
-- Ac.toNormalized is greedy about 'normalizing' opaque terms, we should only
-- apply it if we know the term head is a constructor-like symbol.
| App_ symbol _ <- termLike
, isConstructorModulo_ symbol =
case Ac.toNormalized @NormalizedSet termLike of
Ac.Bottom -> TermLike.mkBottom sort'
Expand Down
1 change: 1 addition & 0 deletions test/issue-2378/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
include $(CURDIR)/../include.mk
11 changes: 11 additions & 0 deletions test/issue-2378/test-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
module VERIFICATION
imports TEST

endmodule

module TEST-SPEC
imports VERIFICATION

claim b(keys(_M:Map)) => c

endmodule
1 change: 1 addition & 0 deletions test/issue-2378/test-spec.k.out.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
#Top
14 changes: 14 additions & 0 deletions test/issue-2378/test.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
// Copyright (c) 2020 K Team. All Rights Reserved.

module TEST
imports SET
imports MAP

syntax B ::= b(Set)
| "c"
syntax KItem ::= B

rule b(.Set) => c
rule b(SetItem(_:KItem) S:Set) => b(S)

endmodule