Implication (#2210)

* first draft of new Implication type

* addressed PR comments

* Test.Kore.Step.ClaimPattern: captures variables

* fixed capture issue, fixed test, created Implication test set

* small fix

* made implementation cleaner

* removed redundant comment

* addressed most PR comments

* ran stylish

* addressed recent PR comments

* addressed PR comments and refactored code

* added mapVariables function to OrPattern

* Update comment of kore/src/Kore/Step/Implication.hs

Co-authored-by: Thomas Tuegel <[email protected]>

* fixed building and test issues

* build fix

Co-authored-by: Thomas Tuegel <[email protected]>

Author: MirceaS

kore/src/Kore/Internal/OrPattern.hs

@@ -22,6 +22,7 @@ module Kore.Internal.OrPattern
     , toTermLike
     , targetBinder
     , substitute
+    , mapVariables
     , MultiOr.flatten
     , MultiOr.filterOr
     , MultiOr.gather
@@ -246,3 +247,10 @@ substitute
     -> OrPattern variable
 substitute subst =
     fromPatterns . fmap (Pattern.substitute subst) . toPatterns
+
+mapVariables
+    :: (InternalVariable variable1, InternalVariable variable2)
+    => AdjSomeVariableName (variable1 -> variable2)
+    -> OrPattern variable1
+    -> OrPattern variable2
+mapVariables = MultiOr.map . Pattern.mapVariables