Remove the EvaluatedF marker from TermLike (#2469)

* removed the EvaluatedF marker from TermLike

* removed some redundant imports

Co-authored-by: rv-jenkins <admin@runtimeverification.com>

Author: MirceaS

kore/src/Kore/Builtin/Builtin.hs

@@ -311,9 +311,8 @@ applicationEvaluator impl =
             (TermLike variable)
         -> simplifier (AttemptedAxiom variable)
     evaluator sideCondition (_ :< app) = do
-        let app' = fmap TermLike.removeEvaluated app
         getAttemptedAxiom
-            (impl sideCondition app' >>= appliedFunction)
+            (impl sideCondition app >>= appliedFunction)
 
 {- | Run a parser on a verified domain value.
 

kore/src/Kore/Builtin/External.hs

@@ -12,7 +12,6 @@ module Kore.Builtin.External
 
 import Prelude.Kore
 
-import qualified Control.Comonad.Trans.Cofree as Cofree
 import Data.Functor.Const
     ( Const (..)
     )
@@ -123,10 +122,6 @@ externalize =
             TopF topF -> Syntax.TopF topF
             VariableF variableF -> Syntax.VariableF variableF
             InhabitantF inhabitantF -> Syntax.InhabitantF inhabitantF
-            EvaluatedF evaluatedF ->
-                Cofree.tailF
-                $ worker
-                $ getEvaluated evaluatedF
             EndiannessF endiannessF ->
                 Syntax.ApplicationF
                 $ mapHead Symbol.toSymbolOrAlias

kore/src/Kore/Internal/SideCondition.hs

@@ -449,10 +449,7 @@ simplifyConjunctionByAssumption (toList -> andPredicates) =
 
     size :: TermLike variable -> Int
     size =
-        Recursive.fold $ \(_ :< termLikeF) ->
-            case termLikeF of
-                TermLike.EvaluatedF evaluated -> TermLike.getEvaluated evaluated
-                _ -> 1 + sum termLikeF
+        Recursive.fold $ \(_ :< termLikeF) -> 1 + sum termLikeF
 
     predSize :: Predicate variable -> Int
     predSize =

kore/src/Kore/Internal/TermLike.hs

@@ -10,7 +10,6 @@ License     : NCSA
 module Kore.Internal.TermLike
     ( TermLikeF (..)
     , TermLike (..)
-    , Evaluated (..)
     , extractAttributes
     , isSimplified
     , isSimplifiedSomeCondition
@@ -27,7 +26,6 @@ module Kore.Internal.TermLike
     , hasConstructorLikeTop
     , freeVariables
     , refreshVariables
-    , removeEvaluated
     , termLikeSort
     , hasFreeVariable
     , withoutFreeVariable
@@ -89,7 +87,6 @@ module Kore.Internal.TermLike
     , mkSort
     , mkSortVariable
     , mkInhabitant
-    , mkEvaluated
     , mkEndianness
     , mkSignedness
     -- * Predicate constructors
@@ -144,7 +141,6 @@ module Kore.Internal.TermLike
     , pattern ElemVar_
     , pattern SetVar_
     , pattern StringLiteral_
-    , pattern Evaluated_
     , pattern Endianness_
     , pattern Signedness_
     , pattern Inj_
@@ -652,7 +648,6 @@ forceSortPredicate
   =
     case pattern' of
         -- Recurse
-        EvaluatedF evaluated -> EvaluatedF (Right <$> evaluated)
         -- Predicates: Force sort and stop.
         BottomF bottom' -> BottomF bottom' { bottomSort = forcedSort }
         TopF top' -> TopF top' { topSort = forcedSort }
@@ -791,14 +786,6 @@ forceSorts operandSorts children =
         , Pretty.indent 4 (Unparser.arguments children)
         ]
 
-{- | Remove `Evaluated` if it appears on the top of the `TermLike`.
--}
-removeEvaluated :: TermLike variable -> TermLike variable
-removeEvaluated termLike@(Recursive.project -> (_ :< termLikeF)) =
-    case termLikeF of
-        EvaluatedF (Evaluated e) -> removeEvaluated e
-        _                        -> termLike
-
 {- | Construct an 'Application' pattern.
 
 The result sort of the 'Alias' must be provided. The sorts of arguments
@@ -1460,13 +1447,6 @@ mkInhabitant
     -> TermLike variable
 mkInhabitant = updateCallStack . synthesize . InhabitantF . Inhabitant
 
-mkEvaluated
-    :: HasCallStack
-    => Ord variable
-    => TermLike variable
-    -> TermLike variable
-mkEvaluated = updateCallStack . synthesize . EvaluatedF . Evaluated
-
 {- | Construct an 'Endianness' pattern.
  -}
 mkEndianness
@@ -1730,8 +1710,6 @@ pattern SetVar_ :: SetVariable variable -> TermLike variable
 
 pattern StringLiteral_ :: Text -> TermLike variable
 
-pattern Evaluated_ :: TermLike variable -> TermLike variable
-
 pattern And_ andSort andFirst andSecond <-
     (Recursive.project -> _ :< AndF And { andSort, andFirst, andSecond })
 
@@ -1880,9 +1858,6 @@ pattern ElemVar_ elemVariable <- Var_ (retract -> Just elemVariable)
 pattern StringLiteral_ str <-
     (Recursive.project -> _ :< StringLiteralF (Const (StringLiteral str)))
 
-pattern Evaluated_ child <-
-    (Recursive.project -> _ :< EvaluatedF (Evaluated child))
-
 pattern Endianness_ :: Endianness -> TermLike child
 pattern Endianness_ endianness <-
     (Recursive.project -> _ :< EndiannessF (Const endianness))

kore/src/Kore/Internal/TermLike/TermLike.hs

@@ -8,8 +8,7 @@ License     : NCSA
 {-# LANGUAGE UndecidableInstances #-}
 
 module Kore.Internal.TermLike.TermLike
-    ( Evaluated (..)
-    , TermLike (..)
+    ( TermLike (..)
     , TermLikeF (..)
     , retractKey
     , extractAttributes
@@ -120,34 +119,6 @@ import Kore.Variables.Binding
 import qualified Pretty
 import qualified SQL
 
-{- | @Evaluated@ wraps patterns which are fully evaluated.
-
-Fully-evaluated patterns will not be simplified further because no progress
-could be made.
-
- -}
-newtype Evaluated child = Evaluated { getEvaluated :: child }
-    deriving (Eq, Ord, Show)
-    deriving (Foldable, Functor, Traversable)
-    deriving (GHC.Generic)
-    deriving anyclass (Hashable, NFData)
-    deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
-    deriving anyclass (Debug, Diff)
-
-instance Unparse child => Unparse (Evaluated child) where
-    unparse evaluated =
-        Pretty.vsep ["/* evaluated: */", Unparser.unparseGeneric evaluated]
-    unparse2 evaluated =
-        Pretty.vsep ["/* evaluated: */", Unparser.unparse2Generic evaluated]
-
-instance Synthetic syn Evaluated where
-    synthetic = getEvaluated
-    {-# INLINE synthetic #-}
-
-instance {-# OVERLAPS #-} Synthetic Pattern.Simplified Evaluated where
-    synthetic = const Pattern.fullySimplified
-    {-# INLINE synthetic #-}
-
 {- | 'TermLikeF' is the 'Base' functor of internal term-like patterns.
 
 -}
@@ -174,7 +145,6 @@ data TermLikeF variable child
     | RewritesF       !(Rewrites Sort child)
     | TopF            !(Top Sort child)
     | InhabitantF     !(Inhabitant child)
-    | EvaluatedF      !(Evaluated child)
     | StringLiteralF  !(Const StringLiteral child)
     | InternalBoolF   !(Const InternalBool child)
     | InternalBytesF  !(Const InternalBytes child)
@@ -226,7 +196,6 @@ instance
             RewritesF rewrites -> synthetic rewrites
             TopF top -> synthetic top
             InhabitantF inhabitant -> synthetic inhabitant
-            EvaluatedF evaluated -> synthetic evaluated
             StringLiteralF stringLiteral -> synthetic stringLiteral
             InternalBoolF internalBool -> synthetic internalBool
             InternalBytesF internalBytes -> synthetic internalBytes
@@ -264,7 +233,6 @@ instance Synthetic Sort (TermLikeF variable) where
             RewritesF rewrites -> synthetic rewrites
             TopF top -> synthetic top
             InhabitantF inhabitant -> synthetic inhabitant
-            EvaluatedF evaluated -> synthetic evaluated
             StringLiteralF stringLiteral -> synthetic stringLiteral
             InternalBoolF internalBool -> synthetic internalBool
             InternalBytesF internalBytes -> synthetic internalBytes
@@ -302,7 +270,6 @@ instance Synthetic Pattern.Functional (TermLikeF variable) where
             RewritesF rewrites -> synthetic rewrites
             TopF top -> synthetic top
             InhabitantF inhabitant -> synthetic inhabitant
-            EvaluatedF evaluated -> synthetic evaluated
             StringLiteralF stringLiteral -> synthetic stringLiteral
             InternalBoolF internalBool -> synthetic internalBool
             InternalBytesF internalBytes -> synthetic internalBytes
@@ -340,7 +307,6 @@ instance Synthetic Pattern.Function (TermLikeF variable) where
             RewritesF rewrites -> synthetic rewrites
             TopF top -> synthetic top
             InhabitantF inhabitant -> synthetic inhabitant
-            EvaluatedF evaluated -> synthetic evaluated
             StringLiteralF stringLiteral -> synthetic stringLiteral
             InternalBoolF internalBool -> synthetic internalBool
             InternalBytesF internalBytes -> synthetic internalBytes
@@ -378,7 +344,6 @@ instance Synthetic Pattern.Defined (TermLikeF variable) where
             RewritesF rewrites -> synthetic rewrites
             TopF top -> synthetic top
             InhabitantF inhabitant -> synthetic inhabitant
-            EvaluatedF evaluated -> synthetic evaluated
             StringLiteralF stringLiteral -> synthetic stringLiteral
             InternalBoolF internalBool -> synthetic internalBool
             InternalBytesF internalBytes -> synthetic internalBytes
@@ -416,7 +381,6 @@ instance Synthetic Pattern.Simplified (TermLikeF variable) where
             RewritesF rewrites -> synthetic rewrites
             TopF top -> synthetic top
             InhabitantF inhabitant -> synthetic inhabitant
-            EvaluatedF evaluated -> synthetic evaluated
             StringLiteralF stringLiteral -> synthetic stringLiteral
             InternalBoolF internalBool -> synthetic internalBool
             InternalBytesF internalBytes -> synthetic internalBytes
@@ -454,7 +418,6 @@ instance Synthetic Pattern.ConstructorLike (TermLikeF variable) where
             RewritesF rewrites -> synthetic rewrites
             TopF top -> synthetic top
             InhabitantF inhabitant -> synthetic inhabitant
-            EvaluatedF evaluated -> synthetic evaluated
             StringLiteralF stringLiteral -> synthetic stringLiteral
             InternalBoolF internalBool -> synthetic internalBool
             InternalBytesF internalBytes -> synthetic internalBytes
@@ -752,8 +715,6 @@ instance
             TopF Top { topSort } -> locationFromAst topSort
             VariableF (Const variable) -> locationFromAst variable
             InhabitantF Inhabitant { inhSort } -> locationFromAst inhSort
-            EvaluatedF Evaluated { getEvaluated } ->
-                locationFromAst getEvaluated
             InjF Inj { injChild } -> locationFromAst injChild
             SignednessF (Const signedness) -> locationFromAst signedness
             EndiannessF (Const endianness) -> locationFromAst endianness
@@ -821,7 +782,6 @@ traverseVariablesF adj =
         InternalSetF setP -> pure (InternalSetF setP)
         TopF topP -> pure (TopF topP)
         InhabitantF s -> pure (InhabitantF s)
-        EvaluatedF childP -> pure (EvaluatedF childP)
         EndiannessF endianness -> pure (EndiannessF endianness)
         SignednessF signedness -> pure (SignednessF signedness)
         InjF inj -> pure (InjF inj)

kore/src/Kore/Step/SMT/Translate.hs

@@ -153,7 +153,6 @@ translatePredicateWith sideCondition translateTerm predicate =
     translatePredicatePatternWorker :: p -> Translator variable m SExpr
     translatePredicatePatternWorker pat =
         case Cofree.tailF (Recursive.project pat) of
-            EvaluatedF child -> translatePredicatePattern (getEvaluated child)
             -- Logical connectives: translate as connectives
             AndF and' -> translatePredicateAnd and'
             BottomF _ -> return (SMT.bool False)

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

@@ -390,7 +390,6 @@ makeSimplifiedCeil
   where
     needsChildCeils = case termLikeF of
         ApplyAliasF _ -> False
-        EvaluatedF  _ -> False
         EndiannessF _ -> True
         SignednessF _ -> True
         AndF _ -> True

kore/src/Kore/Step/Simplification/TermLike.hs

@@ -369,7 +369,6 @@ simplify sideCondition = \termLike ->
             -- Unimplemented cases
             ApplyAliasF _ -> doNotSimplify
             -- Do not simplify non-simplifiable patterns.
-            EvaluatedF  _ -> doNotSimplify
             EndiannessF _ -> doNotSimplify
             SignednessF _ -> doNotSimplify
             --

kore/test/Test/ConsistentKore.hs

@@ -90,7 +90,6 @@ import Kore.Internal.TermLike
     , mkCeil
     , mkElemVar
     , mkEquals
-    , mkEvaluated
     , mkExists
     , mkFloor
     , mkForall
@@ -332,7 +331,6 @@ _checkTermImplemented term@(Recursive.project -> _ :< termF) =
     checkTermF (InternalListF _) = term
     checkTermF (InternalMapF _) = term
     checkTermF (InternalSetF _) = term
-    checkTermF (EvaluatedF _) = term
     checkTermF (InhabitantF _) = term  -- Not implemented.
     checkTermF (EndiannessF _) = term  -- Not implemented.
     checkTermF (SignednessF _) = term  -- Not implemented.
@@ -358,7 +356,6 @@ termGenerators = do
             , orGenerator
             , rewritesGenerator
             , topGenerator
-            , evaluatedGenerator
             ]
     literals <- filterGeneratorsAndGroup
         (catMaybes
@@ -587,9 +584,6 @@ rewritesGenerator = binaryOperatorGenerator mkRewrites
 topGenerator :: TermGenerator
 topGenerator = nullaryFreeSortOperatorGenerator mkTop
 
-evaluatedGenerator :: TermGenerator
-evaluatedGenerator = unaryOperatorGenerator mkEvaluated
-
 maybeStringLiteralGenerator :: Setup -> Maybe TermGenerator
 maybeStringLiteralGenerator Setup {maybeStringLiteralSort} =
     case maybeStringLiteralSort of

kore/test/Test/Kore/Builtin/Int.hs

@@ -11,8 +11,6 @@ module Test.Kore.Builtin.Int
     , test_and, test_or, test_xor, test_not
     , test_shl, test_shr
     , test_pow, test_powmod, test_log2
-    , test_tdiv_evaluated_arguments
-    , test_ediv_evaluated_arguments
     , test_unifyEqual_NotEqual
     , test_unifyEqual_Equal
     , test_unifyAnd_NotEqual
@@ -57,9 +55,6 @@ import Data.Bits
     , (.&.)
     , (.|.)
     )
-import Data.Semigroup
-    ( Endo (..)
-    )
 import qualified Data.Text as Text
 
 import Kore.Builtin.Int
@@ -281,10 +276,6 @@ test_abs = testUnary absIntSymbol abs
 test_tdiv :: TestTree
 test_tdiv = testPartialBinary tdivIntSymbol tdiv
 
-test_tdiv_evaluated_arguments :: TestTree
-test_tdiv_evaluated_arguments =
-    testDivEvaluatedArguments tdivIntSymbol tdiv
-
 test_tmod :: TestTree
 test_tmod = testPartialBinary tmodIntSymbol tmod
 
@@ -297,10 +288,6 @@ test_tmodZero = testPartialBinaryZero tmodIntSymbol tmod
 test_ediv_property :: TestTree
 test_ediv_property = testPartialBinary edivIntSymbol ediv
 
-test_ediv_evaluated_arguments :: TestTree
-test_ediv_evaluated_arguments =
-    testDivEvaluatedArguments edivIntSymbol ediv
-
 test_emod_property :: TestTree
 test_emod_property = testPartialBinary emodIntSymbol emod
 
@@ -400,25 +387,6 @@ test_euclidian_division_theorem =
                 internalIntValue
             _ -> error "Expecting builtin int."
 
-testDivEvaluatedArguments
-    :: Symbol
-    -> (Integer -> Integer -> Maybe Integer)
-    -> TestTree
-testDivEvaluatedArguments symbol expected =
-    testPropertyWithSolver (Text.unpack name) $ do
-        a <- forAll genInteger
-        b <- forAll genInteger
-        na <- forAll $ Gen.integral (Range.linear 0 5)
-        nb <- forAll $ Gen.integral (Range.linear 0 5)
-        let expect = asPartialPattern $ expected a b
-        actual <- evaluateT
-            $ mkApplySymbol symbol [evaluated na a, evaluated nb b]
-        (===) expect actual
-  where
-    name = expectHook edivIntSymbol <> " with evaluated arguments"
-    compose n f = appEndo $ stimes (n :: Integer) (Endo f)
-    evaluated n x = compose n mkEvaluated $ asInternal x
-
 -- Bitwise operations
 test_and :: TestTree
 test_and = testBinary andIntSymbol (.&.)