regenerate tests and mis cleanup

library/Booster/Pattern/Rewrite.hs

@@ -399,11 +399,11 @@ data RewriteFailed k
       RuleConditionUnclear (RewriteRule k) Predicate
     | -- | A rewrite rule does not preserve definedness
       DefinednessUnclear (RewriteRule k) Pattern [NotPreservesDefinednessReason]
-    | -- | A unification produced a non-match substitution
+    | -- | A matching produced a non-match substitution
       UnificationIsNotMatch (RewriteRule k) Term Substitution
-    | -- | A sort error was detected during unification
+    | -- | A sort error was detected during m,atching
       RewriteSortError (RewriteRule k) Term SortError
-    | -- | A sort error was detected during unification
+    | -- | An error was detected during matching
       InternalMatchError Text
     | -- | Term has index 'None', no rule should apply
       TermIndexIsNone Term

library/Booster/Pattern/UnifiedMatcher.hs

@@ -1,5 +1,3 @@
-{-# LANGUAGE PatternSynonyms #-}
-
 {- |
 Copyright   : (c) Runtime Verification, 2022
 License     : BSD-3-Clause
@@ -118,14 +116,15 @@ instance Pretty FailReason where
 type Substitution = Map Variable Term
 
 {- | Attempts to find a simple unifying substitution for the given
-   terms. Only constructor symbols are considered (no functions).
+   terms.
 
    The returned substitution is oriented towards 'term1', i.e.,
    prefers to replace its variables if given a choice.
 
-   This code calls `error` for internal errors (e.g., function
-   arguments that should not be possible), assuming the caller will
-   catch and handle those errors.
+   TODO: This should not be the case and we need to re-factor the code further
+   to ensure that we always produce a matching substitution without having to check
+   after running the matcher
+
 -}
 matchTerms :: MatchType -> KoreDefinition -> Term -> Term -> MatchResult
 matchTerms matchType KoreDefinition{sorts} term1 term2 =

test/rpc-integration/test-log-simplify-json/test.sh

@@ -11,12 +11,16 @@ echo "arguments=$*"
 diff="git diff --no-index"
 # remove "--regenerate" and tweak $diff if it is present
 
+regenerate () {
+    cp $2 $1
+}
+
 client_args=""
 for arg in $*; do
     case "$arg" in
         --regenerate)
             echo "Re-generating expectation files"
-            diff="tee"
+            diff="regenerate"
             ;;
         *)
             client_args+=" $arg"