Remove _PREDICATE sort #2604
Closed
Remove _PREDICATE sort #2604
Conversation
This file contains hidden or 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
Boarders
added a commit
that referenced
this pull request
May 25, 2021
Remove the predicate sort in favour of using known sorts at all call sites. This mostly adds sort arguments to various functions that previously implicitly used _PREDICATE sort. In turn this means removing the various underbar methods previously in `Kore.Internal.TermLike`.
Boarders
added a commit
that referenced
this pull request
May 26, 2021
Remove the predicate sort in favour of using known sorts at all call sites. This mostly adds sort arguments to various functions that previously implicitly used _PREDICATE sort. In turn this means removing the various underbar methods previously in `Kore.Internal.TermLike`.
ttuegel
pushed a commit
that referenced
this pull request
Jun 26, 2021
Remove the predicate sort in favour of using known sorts at all call sites. This mostly adds sort arguments to various functions that previously implicitly used _PREDICATE sort. In turn this means removing the various underbar methods previously in `Kore.Internal.TermLike`.
rv-jenkins
added a commit
that referenced
this pull request
Aug 17, 2021
* Remove _PREDICATE sort (#2604) Remove the predicate sort in favour of using known sorts at all call sites. This mostly adds sort arguments to various functions that previously implicitly used _PREDICATE sort. In turn this means removing the various underbar methods previously in `Kore.Internal.TermLike`. * Kore.Repl.Interpreter: Unparse \bottom with variable sort * Kore.Exec: Unparse \bottom with variable sort * Test.Kore.ASTVerifier.DefinitionVerifier.Imports: Use explicit sorts * Test.Kore.Step.Simplification.Forall: Use explicit sorts * Test.Kore.Step.Simplification.InternalList: Use explicit sorts * Test.Kore.Step.Simplification.InternalMap: Use explicit sorts * Test.Kore.Step.Simplification.InternalSet: Use explicit sorts * Test.Kore.Step.Simplification.Top: Use explicit sorts * Test.Kore.Step.Simplification.Bottom: Use explicit sorts * NotSimplifier: Use Not.simplify * Test.Kore.Step.Simplification: Use explicit sorts * Test.Kore.Step.Simplification.Floor: Use explicit sorts * Test.Kore.Step.Simplification.Equals: Use explicit sorts * Add instance Pretty (Pattern _) * Test.Kore.Step.Simplification.AndTerms: Use explicit sorts * Test.Kore.Builtin.Int: Use explicit sorts * Test.Kore.Exec: Use explicit sorts * Test.Kore.Internal.Pattern: Use explicit sorts * Test.Kore.Equation.Application: Use explicit sorts * Test.Kore.Internal.OrPattern: Use explicit sorts * Test.Kore.Builtin.KEqual: Use explicit sorts * Test.Kore.Builtin.List: Use explicit sorts * Test.Kore.Builtin.Map: Use explicit sorts * Test.Kore.Builtin.Set: Use explicit sorts * Test.Kore.Builtin.String: Use explicit sorts * Test.Kore.Internal.Predicate: Use explicit sorts * Test.Kore.Internal.SideCondition: Use explicit sorts * Test.Kore.Reachability.Claim: Use explicit sorts * Test.Kore.Reachability.OnePathStrategy: Use explicit sorts * Test.Kore.Reachability.Prove: Use explicit sorts * Test.Kore.Repl.Interpreter: Use explicit sorts * Test.Kore.Step.AntiLeft: Use explicit sorts * Test.Kore.Step.Axiom.Identifier: Use explicit sorts * Test.Kore.Step.Axiom.Matcher: Use explicit sorts * Test.Kore.Step.Axiom.Registry: Use explicit sorts * Test.Kore.Step.Function.Integration: Use explicit sorts * Test.Kore.Step.Function.Implication: Use explicit sorts * Test.Kore.Step.RewriteStep: Use explicit sorts * Test.Kore.Step.Rule: Use explicit sorts * Test.Kore.Step.Rule.Combine: Use explicit sorts * Test.Kore.Step.Simplification.And: Use explicit sorts * Fix some tests * Format with fourmolu * Fix test * Use child sort in predicate forall simplifier * Apply suggestions given by pedantic * Apply hlint * Fix one more test * Use bool's sort in unifyIntEq and unifyStringEq * Fix tests broken because incorrect merge with master * Use bool's sort in unifyKequalsEq's eraseTerm * Use initialSort instead of "R" dummy sort for exec's result * Fix the left unit tests * Do some cleanup * Validate.hs Cleanup: Use types to suggest that the sort variable "_" is used only for pretty printing * Add TODO for implementing Predicate.mapVariables without converting to TermLike * Rename OrPattern.top to OrPattern.topOf and fix documentation * Equals.makeEvaluate: don't replace second term * Remove unused module and clean Forall.hs's export list * Remove redundant parentheses * Remove redundant do * Use "_" sort variable instead of Mock.testSort for pretty printing * Address some comments * Remove Sort parameter from Top.simplify * Remove Sort parameter from InternalSet.simplify * Use pattern sort in Or.hs if available * Address Raoul's comments * Format with fourmolu * Rebuild * Use sameSort with different sorts * Address comments * Format with fourmolu * Rebuild Co-authored-by: Boarders <callan.mcgill@gmail.com> Co-authored-by: Andrei Burdușa <andrei.burdusa@zoho.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com>
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 #2152.
Review checklist
The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.