Intern IDs #3122
Closed
Intern IDs #3122
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Right now I'm getting test failures like this {-
↓ test/Driver.hs
↓ Test
↓ Kore
↓ Unification
↓ UnifierT
↓ mergeAndNormalizeSubstitutions
✗ Predicate from normalizing substitution -}
test/Test/Kore/Unification/UnifierT.hs:357:
Conditional
{ term = _
, predicate =
Predicate
{ getPredicate =
CofreeT
{ runCofreeT =
Identity
{ runIdentity =
_
:<
EqualsF
Equals
{ equalsOperandSort = _
, equalsResultSort = _
, equalsFirst =
TermLike
{ getTermLike =
_
:<
ApplySymbolF
Application
{ applicationSymbolOrAlias =
Symbol
{ symbolConstructor =
InternedId
{ getInternedId =
{- was: "cf" -} "cg"
, internedIdLocation = _
}
, symbolParams = _
, symbolSorts = _
, symbolAttributes = _
}
, applicationChildren = _
}
}
, equalsSecond =
TermLike
{ getTermLike =
_
:<
ApplySymbolF
Application
{ applicationSymbolOrAlias =
Symbol
{ symbolConstructor =
InternedId
{ getInternedId =
{- was: "cg" -} "cf"
, internedIdLocation = _
}
, symbolParams = _
, symbolSorts = _
, symbolAttributes = _
}
, applicationChildren = _
}
}
}
}
}
}
, substitution =
Kore.Internal.Substitution.wrap (Assignment_
{ assignedVariable = _
, assignedTerm =
TermLike
{ getTermLike =
_
:<
ApplySymbolF
Application
{ applicationSymbolOrAlias =
_
, applicationChildren =
TermLike
{ getTermLike =
_
:<
ApplySymbolF
Application
{ applicationSymbolOrAlias =
Symbol
{ symbolConstructor =
InternedId
{ getInternedId =
{- was:
"cf"
-}
"cg"
, internedIdLocation =
_
}
, symbolParams =
_
, symbolSorts =
_
, symbolAttributes =
_
}
, applicationChildren =
_
}
}
:
_
}
}
}
:
_)
}
:
_
|
|
@JKTKops would this diff below be a proper fix for a #3122 (comment) failure? Since it doesn't like variable order — well, let's swap them :) I mean, it's probably not a proper fix, but I've got to ask :) diff --git a/kore/test/Test/Kore/Unification/UnifierT.hs b/kore/test/Test/Kore/Unification/UnifierT.hs
index 7f47e8882..c87cc24f4 100644
--- a/kore/test/Test/Kore/Unification/UnifierT.hs
+++ b/kore/test/Test/Kore/Unification/UnifierT.hs
@@ -336,10 +336,10 @@ test_mergeAndNormalizeSubstitutions =
[ Conditional
{ term = ()
, predicate =
- Predicate.makeEqualsPredicate Mock.cf Mock.cg
+ Predicate.makeEqualsPredicate Mock.cg Mock.cf
, substitution =
Substitution.unsafeWrap
- [(inject Mock.xConfig, Mock.constr10 Mock.cf)]
+ [(inject Mock.xConfig, Mock.constr10 Mock.cg)]
}
]
actual <-
@@ -350,8 +350,8 @@ test_mergeAndNormalizeSubstitutions =
, substitution =
Substitution.wrap $
Substitution.mkUnwrappedSubstitution
- [ (inject Mock.xConfig, Mock.constr10 Mock.cf)
- , (inject Mock.xConfig, Mock.constr10 Mock.cg)
+ [ (inject Mock.xConfig, Mock.constr10 Mock.cg)
+ , (inject Mock.xConfig, Mock.constr10 Mock.cf)
]
}
assertEqual "" expect actual |
|
breakerzirconia
force-pushed
the
intern-ids
branch
from
297e733
to
205f738
Compare
|
|
|
fixed by 8972684 Nix: ✔️ Stack: ✔️ Cabal: ✖️
|
|
|
Couldn't fix this one:
|
|
Couldn't fix this one too — it expects a full-fledged Conditional, but collapses to an empty list instead
|
|
Couldn't fix this one
|
|
|
|
|
|
I just noticed the sharp increase in allocation in this test. Not sure why that happens, it might deserve a closer look. |
|
|
Notes on
|
|
|
@goodlyrottenapple So in bc2db8b I've dropped unwrapping instances for |
|
Hey @develop7 and @goodlyrottenapple . Why did you modify the Also, variable substitutions get ordered according to this instance: . So, now the variable with the smaller interned id should get substituted.Is the test result from the comment above resulting from before/after the change to the instances for |
It's completely my idea; to see what breaks and/or get busy since the call wasn't as fruitful as I expected.
From before, of course. |
|
Alright. I think that many tests make the assumption that variable substitutions will be ordered lexicographically, but now that is no longer the case. Concretely, when we write I've thought about this a bit, and we could try to force the above as follows: This should be quick and it'll allow us to check if this is indeed the issue or not. Ideally, since a lot of the code related to substitutions assumes lexicographical ordering of variable substitutions, we could find a way to ensure that the order on the string Ids is preserved by the order on the interned Ids. If we can't do that, maybe we could mock the interned Id table for the data in |
gromakovsky
force-pushed
the
intern-ids
branch
from
a988b3f
to
42c460f
Compare
|
Closing in favor of #3217. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Fixes #3112
Scope:
Estimate:
Benchmark
report-intern-ids.md
report.pdf
Review checklist
The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.
Currently failing unit tests
https://github.com/runtimeverification/haskell-backend/runs/7230663172?check_suite_focus=true#step:8:27642
https://github.com/runtimeverification/haskell-backend/runs/7230662258?check_suite_focus=true#step:7:15278 https://github.com/runtimeverification/haskell-backend/runs/7230879449?check_suite_focus=true#step:5:27905