From 3f22ee19cc591ce88cb8130c5442e9b344498729 Mon Sep 17 00:00:00 2001
From: Georgy Lukyanov <mail@geo2a.info>
Date: Wed, 9 Aug 2023 10:25:37 +0200
Subject: [PATCH] Reshuffle SimplifyImplicationResult

---
 kore-rpc-types/src/Kore/JsonRpc/Types.hs | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs
index eca173e9ba..b2a8f38137 100644
--- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs
+++ b/kore-rpc-types/src/Kore/JsonRpc/Types.hs
@@ -179,6 +179,7 @@ data GetModelResult = GetModelResult
 
 data SimplifyImplicationResult = SimplifyImplicationResult
     { validity :: ImplicationValidityResult
+    , substitution :: Maybe KoreJson
     , logs :: Maybe [LogEntry]
     }
     deriving stock (Generic, Show, Eq)
@@ -187,8 +188,8 @@ data SimplifyImplicationResult = SimplifyImplicationResult
         via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] SimplifyImplicationResult
 
 data ImplicationValidityResult
-    = -- | implication is valid, constrained substitution returned
-      ImplicationValid KoreJson
+    = -- | implication is valid
+      ImplicationValid
     | -- | implication is invalid, explains why
       ImplicationInvalid ImplicationInvalidReason
     | -- | implication is unknown, explains why
@@ -199,16 +200,20 @@ data ImplicationValidityResult
         via CustomJSON '[] ImplicationValidityResult
 
 data ImplicationInvalidReason
-    = MatchingFailed KoreJson
-    | ConstraintSubsumptionFailed KoreJson
+    = -- | antecedent and consequent do not match
+      MatchingFailed Text
+    | -- | matching was successful, but constraints don't agree: return unsatisfiable core of constraints
+      ConstraintSubsumptionFailed KoreJson
     deriving stock (Generic, Show, Eq)
     deriving
         (FromJSON, ToJSON)
         via CustomJSON '[] ImplicationInvalidReason
 
 data ImplicationUnknownReason
-    = MatchingUnknown KoreJson
-    | ConstraintSubsumptionUnknown KoreJson
+    = -- | matching between antecedent and consequent is indeterminate, return the subterms that caused this
+      MatchingUnknown KoreJson KoreJson
+    | -- | matching was successful, but constraint subsumption is indeterminate: return unknown constraints
+      ConstraintSubsumptionUnknown KoreJson
     deriving stock (Generic, Show, Eq)
     deriving
         (FromJSON, ToJSON)