Make RPC implication types match the ones in Booster

runtimeverification · Aug 9, 2023 · 27c81b4 · 27c81b4
1 parent 501ad4c
commit 27c81b4
Showing 1 changed file with 6 additions and 4 deletions.
diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs
@@ -192,21 +192,23 @@ data ImplicationValidityResult
     | -- | implication is invalid, explains why
       ImplicationInvalid ImplicationInvalidReason
     | -- | implication is unknown, explains why
-      ImplicationUnknown ImplicationInvalidReason
+      ImplicationUnknown ImplicationUnknownReason
     deriving stock (Generic, Show, Eq)
     deriving
         (FromJSON, ToJSON)
         via CustomJSON '[] ImplicationValidityResult
 
 data ImplicationInvalidReason
-    = ImplicationTermsDontUnify KoreJson
-    | ImplicationConstraintSubsumptionFailed KoreJson
+    = MatchingFailed KoreJson
+    | ConstraintSubsumptionFailed KoreJson
     deriving stock (Generic, Show, Eq)
     deriving
         (FromJSON, ToJSON)
         via CustomJSON '[] ImplicationInvalidReason
 
-data ImplicationUnknownReason = ImplicationConstraintSubsumptionUnknown KoreJson
+data ImplicationUnknownReason
+    = MatchingUnknown KoreJson
+    | ConstraintSubsumptionUnknown KoreJson
     deriving stock (Generic, Show, Eq)
     deriving
         (FromJSON, ToJSON)