From 635445f9b4618581955a27bf2ec82174b522afb7 Mon Sep 17 00:00:00 2001
From: Nishant Rodrigues <nishantjr@gmail.com>
Date: Wed, 6 May 2020 13:25:52 -0500
Subject: [PATCH] kore: getReturnSort: Case of \mu, \or, \and

---
 prover/lang/kore-lang.md                   | 22 ++++++++++++++++++++++
 prover/t/ltl/until-implies-eventually.kore |  6 +++---
 2 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/prover/lang/kore-lang.md b/prover/lang/kore-lang.md
index aba705bc1..851a24f7f 100644
--- a/prover/lang/kore-lang.md
+++ b/prover/lang/kore-lang.md
@@ -317,6 +317,28 @@ module KORE-HELPERS
   rule [[ getReturnSort( R ( ARGS ) )  => S ]]
        <declaration> symbol R ( _ ) : S </declaration>
 
+  rule getReturnSort(\mu _ . Phi) => getReturnSort(Phi)
+  rule getReturnSort(\or(P, Ps)) => unionSort(getReturnSort(P), getReturnSort(\or(Ps)))
+  rule getReturnSort(\or(.Patterns)) => BottomSort
+  rule getReturnSort(\and(P, Ps)) => intersectSort(getReturnSort(P), getReturnSort(\and(Ps)))
+  rule getReturnSort(\and(.Patterns)) => TopSort
+  rule getReturnSort(_:SetVariable) => TopSort
+
+  syntax Sort ::= "TopSort"         [token]
+                | "BottomSort"      [token]
+
+  syntax Sort ::= unionSort(Sort, Sort) [function]
+  rule unionSort(TopSort, S) => TopSort
+  rule unionSort(S, TopSort) => TopSort
+  rule unionSort(BottomSort, S) => S
+  rule unionSort(S, BottomSort) => S
+
+  syntax Sort ::= intersectSort(Sort, Sort) [function]
+  rule intersectSort(TopSort, S) => S
+  rule intersectSort(S, TopSort) => S
+  rule intersectSort(BottomSort, S) => BottomSort
+  rule intersectSort(S, BottomSort) => BottomSort
+
   syntax Bool ::= isUnfoldable(Symbol) [function]
   rule [[ isUnfoldable(S:Symbol) => true ]]
        <declaration> axiom _ : \forall {_} \iff-lfp(S(_), _) </declaration>
diff --git a/prover/t/ltl/until-implies-eventually.kore b/prover/t/ltl/until-implies-eventually.kore
index a0d1a3087..6f1587545 100644
--- a/prover/t/ltl/until-implies-eventually.kore
+++ b/prover/t/ltl/until-implies-eventually.kore
@@ -1,4 +1,4 @@
-symbol next(State) : State
+symbol next(TopSort) : TopSort
 
 // there is always a next state
 axiom inf: next(\top())
@@ -7,8 +7,8 @@ axiom inf: next(\top())
 axiom lin: \implies(next(#X), \not(next(\not(#X))))
 
 // phi1 U phi2 => []phi2
-claim \implies( \mu #X . \or(PHI2, \and(PHI1, next(#X)))
-              , \mu #X . \or(PHI2, next(#X))
+claim \implies( \mu #X . \or(#PHI2, \and(#PHI1, next(#X)))
+              , \mu #X . \or(#PHI2, next(#X))
               )
 
 /*