Implication

[MirceaS]

---

New Implication type tying together the definitions and functions of Claim and Rule that diverged.
See Issue #2192

Reviewer checklist

• Test coverage: stack test --coverage
• Public API documentation: stack haddock

[ttuegel]

I updated your test to show how variables can be captured.

[ttuegel]

Suggested change

	assertBool "Variable was captured" (not $ isFreeVariable (inject $ variableName x) freeVars)
	assertBool "Expected variable is not captured" (not $ isFreeVariable (inject $ variableName x) freeVars)

[MirceaS]

@ttuegel Shouldn't the assert message go like "Expected variable IS captured" because that message is what gets shown when the assertion fails.

[ttuegel]

Our other tests take the form:

assert... "a statement that should be true" arguments...

[MirceaS]

How about a compromise that follows the style in Test.Kore.Equation.Sentence, that is "Expected -something that should have been true-" (In this case "Expected the expected variable to not be captured")?

[ttuegel]

subst needs to be restricted to variables that actually appear in the existentials list.

renameExistentials (Map.fromList [("x", "u"), ("y", "v")])
  Implication { existentials = ["x"], right = {- "y" occurs free -} }

If this is only used internally, it should be fine to have an assertion that every key in the map appears in existentials.

[ttuegel]

Since this is used internally, it is fine to keep the type as it is, but we should add an assertion that the sorts of variables do not change.

[ttuegel]

Let's introduce a mapVariables function in Kore.Internal.OrPattern which combines OrPattern.map and Pattern.mapVariables. I'm sure this combination is used elsewhere, too.