TODO: Preserve pattern sorts in the simplifier

Author: ttuegel

src/main/haskell/kore/src/Kore/Step/OrOfExpandedPattern.hs

@@ -56,7 +56,16 @@ import           Kore.Unparser
 
 {-| 'MultiOr' is a Matching logic or of its children
 
-TODO(virgil): Make this a list-like monad, many things would be nicer.
+-}
+{- TODO (virgil): Make 'getMultiOr' a non-empty list ("Data.NonEmpty").
+
+An empty 'MultiOr' corresponding to 'Bottom' actually discards information about
+the sort of its child patterns! That is a problem for simplification, which
+should preserve pattern sorts.
+
+A non-empty 'MultiOr' would also have a nice symmetry between 'Top' and 'Bottom'
+patterns.
+
 -}
 newtype MultiOr child = MultiOr { getMultiOr :: [child] }
   deriving

src/main/haskell/kore/src/Kore/Step/Simplification/And.hs

@@ -107,6 +107,18 @@ simplify
 {-| simplifies an And given its two 'OrOfExpandedPattern' children.
 
 See 'simplify' for details.
+-}
+{- TODO (virgil): Preserve pattern sorts under simplification.
+
+One way to preserve the required sort annotations is to make 'simplifyEvaluated'
+take an argument of type
+
+> CofreeF (And level) (Valid level) (OrOfExpandedPattern level variable)
+
+instead of two 'OrOfExpandedPattern' arguments. The type of 'makeEvaluate' may
+be changed analogously. The 'Valid' annotation will eventually cache information
+besides the pattern sort, which will make it even more useful to carry around.
+
 -}
 simplifyEvaluated
     ::  ( MetaOrObject level

src/main/haskell/kore/src/Kore/Step/Simplification/Ceil.hs

@@ -75,6 +75,18 @@ simplify
 
 {-| 'simplifyEvaluated' evaluates a ceil given its child, see 'simplify'
 for details.
+-}
+{- TODO (virgil): Preserve pattern sorts under simplification.
+
+One way to preserve the required sort annotations is to make 'simplifyEvaluated'
+take an argument of type
+
+> CofreeF (Ceil level) (Valid level) (OrOfExpandedPattern level variable)
+
+instead of an 'OrOfExpandedPattern' argument. The type of 'makeEvaluate' may
+be changed analogously. The 'Valid' annotation will eventually cache information
+besides the pattern sort, which will make it even more useful to carry around.
+
 -}
 simplifyEvaluated
     ::  ( MetaOrObject level

src/main/haskell/kore/src/Kore/Step/Simplification/Equals.hs

@@ -166,6 +166,18 @@ simplify
   =
     simplifyEvaluated tools substitutionSimplifier first second
 
+{- TODO (virgil): Preserve pattern sorts under simplification.
+
+One way to preserve the required sort annotations is to make 'simplifyEvaluated'
+take an argument of type
+
+> CofreeF (Equals level) (Valid level) (OrOfExpandedPattern level variable)
+
+instead of two 'OrOfExpandedPattern' arguments. The type of 'makeEvaluate' may
+be changed analogously. The 'Valid' annotation will eventually cache information
+besides the pattern sort, which will make it even more useful to carry around.
+
+-}
 simplifyEvaluated
     ::  ( MetaOrObject level
         , SortedVariable variable

src/main/haskell/kore/src/Kore/Step/Simplification/Exists.hs

@@ -96,6 +96,19 @@ simplify
   =
     simplifyEvaluated tools substitutionSimplifier simplifier variable child
 
+{- TODO (virgil): Preserve pattern sorts under simplification.
+
+One way to preserve the required sort annotations is to make 'simplifyEvaluated'
+take an argument of type
+
+> CofreeF (Exists level) (Valid level) (OrOfExpandedPattern level variable)
+
+instead of a 'variable level' and an 'OrOfExpandedPattern' argument. The type of
+'makeEvaluate' may be changed analogously. The 'Valid' annotation will
+eventually cache information besides the pattern sort, which will make it even
+more useful to carry around.
+
+-}
 simplifyEvaluated
     ::  ( MetaOrObject level
         , Ord (variable level)

src/main/haskell/kore/src/Kore/Step/Simplification/Floor.hs

@@ -54,6 +54,19 @@ simplify
   =
     simplifyEvaluatedFloor child
 
+{- TODO (virgil): Preserve pattern sorts under simplification.
+
+One way to preserve the required sort annotations is to make 'simplifyEvaluated'
+take an argument of type
+
+> CofreeF (Floor level) (Valid level) (OrOfExpandedPattern level variable)
+
+instead of an 'OrOfExpandedPattern' argument. The type of 'makeEvaluateFloor'
+may be changed analogously. The 'Valid' annotation will eventually cache
+information besides the pattern sort, which will make it even more useful to
+carry around.
+
+-}
 simplifyEvaluatedFloor
     ::  ( MetaOrObject level
         , SortedVariable variable

src/main/haskell/kore/src/Kore/Step/Simplification/Forall.hs

@@ -60,6 +60,19 @@ simplify
   =
     simplifyEvaluated variable child
 
+{- TODO (virgil): Preserve pattern sorts under simplification.
+
+One way to preserve the required sort annotations is to make 'simplifyEvaluated'
+take an argument of type
+
+> CofreeF (Forall level) (Valid level) (OrOfExpandedPattern level variable)
+
+instead of a 'variable level' and an 'OrOfExpandedPattern' argument. The type of
+'makeEvaluate' may be changed analogously. The 'Valid' annotation will
+eventually cache information besides the pattern sort, which will make it even
+more useful to carry around.
+
+-}
 simplifyEvaluated
     ::  ( MetaOrObject level
         , SortedVariable variable

src/main/haskell/kore/src/Kore/Step/Simplification/Iff.hs

@@ -60,6 +60,18 @@ simplify
 {-| evaluates an 'Iff' given its two 'OrOfExpandedPattern' children.
 
 See 'simplify' for detailed documentation.
+-}
+{- TODO (virgil): Preserve pattern sorts under simplification.
+
+One way to preserve the required sort annotations is to make 'simplifyEvaluated'
+take an argument of type
+
+> CofreeF (Iff level) (Valid level) (OrOfExpandedPattern level variable)
+
+instead of two 'OrOfExpandedPattern' arguments. The type of 'makeEvaluate' may
+be changed analogously. The 'Valid' annotation will eventually cache information
+besides the pattern sort, which will make it even more useful to carry around.
+
 -}
 simplifyEvaluated
     ::  ( MetaOrObject level

src/main/haskell/kore/src/Kore/Step/Simplification/Implies.hs

@@ -69,6 +69,18 @@ simplify
 See 'simplify' for details.
 -}
 -- TODO: Maybe transform this to (not a) \/ b
+{- TODO (virgil): Preserve pattern sorts under simplification.
+
+One way to preserve the required sort annotations is to make 'simplifyEvaluated'
+take an argument of type
+
+> CofreeF (Implies level) (Valid level) (OrOfExpandedPattern level variable)
+
+instead of two 'OrOfExpandedPattern' arguments. The type of 'makeEvaluate' may
+be changed analogously. The 'Valid' annotation will eventually cache information
+besides the pattern sort, which will make it even more useful to carry around.
+
+-}
 simplifyEvaluated
     ::  ( MetaOrObject level
         , SortedVariable variable

src/main/haskell/kore/src/Kore/Step/Simplification/In.hs

@@ -65,6 +65,18 @@ simplify
   =
     simplifyEvaluatedIn tools first second
 
+{- TODO (virgil): Preserve pattern sorts under simplification.
+
+One way to preserve the required sort annotations is to make
+'simplifyEvaluatedIn' take an argument of type
+
+> CofreeF (In level) (Valid level) (OrOfExpandedPattern level variable)
+
+instead of two 'OrOfExpandedPattern' arguments. The type of 'makeEvaluateIn' may
+be changed analogously. The 'Valid' annotation will eventually cache information
+besides the pattern sort, which will make it even more useful to carry around.
+
+-}
 simplifyEvaluatedIn
     ::  ( MetaOrObject level
         , SortedVariable variable