Apply Substitutions to ClaimPatterns When Simplifying (#2764)

* Potentially fix logic, but some tests fail

* Update tests, new integration test

* Format with fourmolu

* update integration tests that output affected configs

* simplify construction of Patterns in tests

Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>

Author: 3 people

kore/src/Kore/Reachability/Claim.hs

@@ -590,9 +590,16 @@ simplify' ::
     Strategy.TransitionT (AppliedRule claim) m claim
 simplify' lensClaimPattern claim = do
     claim' <- simplifyLeftHandSide claim
-    let sideCondition = extractSideCondition claim'
-    simplifyRightHandSide lensClaimPattern sideCondition claim'
+    let claim'' = Lens.over lensClaimPattern applySubstOnRightHandSide claim'
+        sideCondition = extractSideCondition claim''
+    simplifyRightHandSide lensClaimPattern sideCondition claim''
   where
+    applySubstOnRightHandSide claimPat =
+        let substitution = Pattern.substitution $ Lens.view (field @"left") claimPat
+            noLeftSubst = Lens.set (field @"left" . field @"substitution") mempty claimPat
+            appliedSubst = ClaimPattern.applySubstitution substitution noLeftSubst
+         in appliedSubst
+
     extractSideCondition =
         SideCondition.fromConditionWithReplacements
             . Pattern.withoutTerm

kore/test/Test/Kore/Reachability/OnePathStrategy.hs

@@ -808,9 +808,7 @@ test_onePathStrategy =
                         )
                     )
             left' =
-                Pattern.withCondition
-                    Mock.a
-                    (Condition.assign (inject Mock.x) Mock.a)
+                Pattern.fromTermLike Mock.a
             right =
                 Pattern.withCondition
                     (TermLike.mkElemVar Mock.x)

kore/test/Test/Kore/Reachability/Prove.hs

@@ -426,9 +426,7 @@ test_proveClaims =
                                 )
                             )
                         )
-                    , Pattern.withCondition
-                        Mock.b
-                        (Condition.assign (inject Mock.x) Mock.a)
+                    , Pattern.fromTermLike Mock.b
                     ]
             initialPattern =
                 Pattern.fromTermLike

test/issue-2221/test-issue-2221.sh.out.golden

@@ -1,33 +1,10 @@
-/* Created: Kore.Internal.OrPattern.toTermLike */
-/* Spa */
-\and{SortGeneratedTopCell{}}(
+/* Fl Fn D Sfa */
+Lbl'-LT-'generatedTop'-GT-'{}(
+    /* Fl Fn D Sfa Cl */ Lbl'-LT-'k'-GT-'{}(/* Fl Fn D Sfa Cl */ dotk{}()),
     /* Fl Fn D Sfa */
-    Lbl'-LT-'generatedTop'-GT-'{}(
-        /* Fl Fn D Sfa Cl */ Lbl'-LT-'k'-GT-'{}(/* Fl Fn D Sfa Cl */ dotk{}()),
-        /* Fl Fn D Sfa */
-        Lbl'-LT-'generatedCounter'-GT-'{}(
-            /* Fl Fn D Sfa */ Var'Unds'DotVar1:SortInt{}
-        ),
-        /* Fl Fn D Sfa Cl */
-        Lbl'-LT-'size'-GT-'{}(/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1"))
+    Lbl'-LT-'generatedCounter'-GT-'{}(
+        /* Fl Fn D Sfa */ Var'Unds'DotVar1:SortInt{}
     ),
-    /* Spa */
-    \and{SortGeneratedTopCell{}}(
-        /* Spa */
-        \equals{SortMyList{}, SortGeneratedTopCell{}}(
-            /* Fl Fn D Sfa */ Var'Unds'0:SortMyList{},
-            /* Fl Fn D Sfa */
-            Lbl'UndsUndsUnds'LIST-SIZER-SYNTAX'Unds'MyList'Unds'Int'Unds'MyList{}(
-                /* Fl Fn D Sfa */ Var'Unds'E:SortInt{},
-                /* Fl Fn D Sfa Cl */
-                Lbl'Stop'MyList'Unds'LIST-SIZER-SYNTAX'Unds'MyList{}()
-            )
-        ),
-        /* Spa */
-        \equals{SortMyList{}, SortGeneratedTopCell{}}(
-            /* Fl Fn D Sfa */ VarL:SortMyList{},
-            /* Fl Fn D Sfa Cl */
-            Lbl'Stop'MyList'Unds'LIST-SIZER-SYNTAX'Unds'MyList{}()
-        )
-    )
+    /* Fl Fn D Sfa Cl */
+    Lbl'-LT-'size'-GT-'{}(/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1"))
 )