Fix unification case between inj and function (#544)

Fix for runtimeverification/kontrol#418 The issue discovered was the failed unification of ``` inj{SortInt{}, SortGas{}}("0") ``` with ``` #if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort( "false", inj{SortInt{},SortGas{}}("0"), inj{SortInt{},SortGas{}}("0") ) ``` which should instead be indeterminate, as the `ite` does in fact evaluate to `inj{SortInt{},SortGas{}}("0")`
runtimeverification · Mar 14, 2024 · 8c26ad4 · 8c26ad4
1 parent ef22c88
commit 8c26ad4
Show file tree

Hide file tree

Showing 2 changed files with 37 additions and 27 deletions.
diff --git a/library/Booster/Pattern/Unify.hs b/library/Booster/Pattern/Unify.hs
@@ -271,16 +271,18 @@ unify1
     term1
     v@Var{} =
         unify1 v term1
--- injection in pattern, no injection in subject: fail (trm cannot be a variable)
+-- injection in pattern, no injection in subject: indeterminate if trm is a function, otherwise fail (trm cannot be a variable)
 unify1
     inj@Injection{}
-    trm =
-        failWith $ DifferentSymbols inj trm
--- injection in subject but not in pattern: fail (trm cannot be a variable)
+    trm = case trm of
+        SymbolApplication symbol _ _ | isFunctionSymbol symbol -> addIndeterminate inj trm
+        _ -> failWith $ DifferentSymbols inj trm
+-- injection in subject but not in pattern: indeterminate if trm is a function, otherwise fail (trm cannot be a variable)
 unify1
     trm
-    inj@Injection{} =
-        failWith $ DifferentSymbols trm inj
+    inj@Injection{} = case trm of
+        SymbolApplication symbol _ _ | isFunctionSymbol symbol -> addIndeterminate trm inj
+        _ -> failWith $ DifferentSymbols trm inj
 ------ Internalised Lists
 -- unification for lists. Only solves simple cases, returns indeterminate otherwise
 unify1

diff --git a/unit-tests/Test/Booster/Pattern/Unify.hs b/unit-tests/Test/Booster/Pattern/Unify.hs
@@ -133,27 +133,35 @@ functions :: TestTree
 functions =
     testGroup
         "Functions (should not unify)"
-        [ let f = app f1 [dv someSort ""]
-           in test "exact same function (but not unifying)" f f $ remainder [(f, f)]
-        , let f1T = app f1 [dv someSort ""]
-              f2T = app f2 [dv someSort ""]
-           in test "different functions" f1T f2T $ remainder [(f1T, f2T)]
-        , let someDv = dv someSort ""
-              f1T = app f1 [someDv]
-              f2T = app f2 [someDv]
-              con3f1 = app con3 [f1T, app con1 [someDv]]
-              con3f2 = app con3 [f2T, app con1 [someDv]]
-           in test "postponed: different functions" con3f1 con3f2 $ remainder [(f1T, f2T)]
-        , let someDv = dv someSort ""
-              f1T = app f1 [someDv]
-              f2T = app f2 [someDv]
-              c1T = app con1 [someDv]
-              c2T = app con2 [someDv]
-              con3f1c1 = app con3 [f1T, c1T]
-              con3f2c2 = app con3 [f2T, c2T]
-           in test "different constrs after different functions" con3f1c1 con3f2c2 $
-                failed (DifferentSymbols c1T c2T)
-        ]
+        $ [ let f = app f1 [dv someSort ""]
+             in test "exact same function (but not unifying)" f f $ remainder [(f, f)]
+          , let f1T = app f1 [dv someSort ""]
+                f2T = app f2 [dv someSort ""]
+             in test "different functions" f1T f2T $ remainder [(f1T, f2T)]
+          , let someDv = dv someSort ""
+                f1T = app f1 [someDv]
+                f2T = app f2 [someDv]
+                con3f1 = app con3 [f1T, app con1 [someDv]]
+                con3f2 = app con3 [f2T, app con1 [someDv]]
+             in test "postponed: different functions" con3f1 con3f2 $ remainder [(f1T, f2T)]
+          , let someDv = dv someSort ""
+                f1T = app f1 [someDv]
+                f2T = app f2 [someDv]
+                c1T = app con1 [someDv]
+                c2T = app con2 [someDv]
+                con3f1c1 = app con3 [f1T, c1T]
+                con3f2c2 = app con3 [f2T, c2T]
+             in test "different constrs after different functions" con3f1c1 con3f2c2 $
+                    failed (DifferentSymbols c1T c2T)
+          ]
+            ++ let f1T = app f1 [dv someSort ""]
+                   dv1 = dv someSort ""
+                   inj1 = Injection aSubsort someSort $ dv aSubsort ""
+                in [ test "function with domain value" f1T dv1 $ remainder [(f1T, dv1)]
+                   , test "domain value with function" dv1 f1T $ remainder [(dv1, f1T)]
+                   , test "function with injection" f1T inj1 $ remainder [(f1T, inj1)]
+                   , test "injection with function" inj1 f1T $ remainder [(inj1, f1T)]
+                   ]
 
 varsAndValues :: TestTree
 varsAndValues =