Fix LIST.in hook for non-constructor-like list elements (#4111)

The previous list hook implementation `LIST.in` was testing membership
based on _syntactic_ equality. This is incorrect if the elements of the
list are not constructor-like (like variables or unevaluated function
calls), `False` cannot be returned in those cases. When all known list
elements are constructor-like, syntactic equality is sufficient. A unit
test was added for this case.

Author: jberthold

booster/library/Booster/Builtin/LIST.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE PatternSynonyms #-}
+
 {- |
 Copyright   : (c) Runtime Verification, 2023
 License     : BSD-3-Clause
@@ -17,14 +19,14 @@ import Data.ByteString.Char8 (ByteString, pack)
 import Data.Map (Map)
 import Data.Map qualified as Map
 
-import Booster.Builtin.BOOL (boolTerm)
 import Booster.Builtin.Base
 import Booster.Builtin.INT
 import Booster.Definition.Attributes.Base (
     KCollectionSymbolNames (..),
     KListDefinition (..),
  )
 import Booster.Pattern.Base
+import Booster.Pattern.Bool (pattern FalseBool, pattern TrueBool)
 
 builtinsLIST :: Map ByteString BuiltinFunction
 builtinsLIST =
@@ -109,11 +111,16 @@ listGetHook args =
 listInHook :: BuiltinFunction
 listInHook [e, KList _ heads rest] =
     case rest of
-        Nothing -> pure $ Just $ boolTerm (e `elem` heads)
+        Nothing
+            | e `elem` heads -> pure $ Just TrueBool
+            | e `notElem` heads
+            , all isConstructorLike_ (e : heads) ->
+                pure $ Just FalseBool
+            | otherwise -> pure Nothing
         Just (_mid, tails)
             | e `elem` tails ->
-                pure $ Just $ boolTerm True
-            | otherwise -> -- could be in opaque _mid
+                pure $ Just TrueBool
+            | otherwise -> -- could be in opaque _mid or not constructor-like
                 pure Nothing
 listInHook args =
     arityError "LIST.in" 2 args

booster/library/Booster/Pattern/Base.hs

@@ -125,6 +125,9 @@ data TermAttributes = TermAttributes
     -- variables, recursive through AndTerm
     , hash :: !Int
     , isConstructorLike :: !Bool
+    -- ^ Means that logic equality is the same as syntactic equality.
+    -- True for domain values and constructor symbols (recursive
+    -- through arg.s), recursive through AndTerm.
     , canBeEvaluated :: !Bool
     -- ^ false for function calls, variables, and AndTerms
     }

booster/unit-tests/Test/Booster/Builtin.hs

@@ -139,6 +139,15 @@ listOfThings n =
     let things = map numDV [1 .. n]
      in KList Fixture.testKListDef things Nothing
 
+listWithVar :: Int -> Int -> Term
+listWithVar n place =
+    case listOfThings n of
+        KList def elems rest ->
+            let variable = [trm| ELEM:SomeSort |]
+                (front, back) = splitAt (max n place) elems
+             in KList def (front <> [variable] <> back) rest
+        _ -> error "unexpected term returned by listOfThings"
+
 -- wrap an Int into an injection to KItem here
 numDV :: Int -> Term
 numDV n =
@@ -158,7 +167,8 @@ testListConcatHook =
             Just empty @=? result
         , testProperty "LIST.concat with an empty list argument" . property $ do
             l <- forAll smallNat
-            let aList = listOfThings l
+            v <- forAll smallNat
+            let aList = listWithVar l v
                 empty = listOfThings 0
             resultR <- evalHook "LIST.concat" [aList, empty]
             Just aList === resultR
@@ -242,6 +252,16 @@ testListInHook =
                 target = numDV 0
             result <- evalHook "LIST.in" [target, list]
             result `shouldBe` False
+        , testProperty
+            "LIST.in is indeterminate when an item is not present in a list with a variable element"
+            . property
+            $ do
+                l <- forAll smallNat
+                v <- forAll smallNat
+                let list = listWithVar l v -- [1 .. v-1, ELEM, v .. l]
+                    target = numDV 0
+                result <- evalHook "LIST.in" [target, list]
+                Nothing === result
         , testProperty "LIST.in is indeterminate when an item is not present (list with opaque middle)"
             . property
             $ do

package/version.sh

@@ -29,9 +29,15 @@ version_sub() {
     local version
     version="$(cat $version_file)"
     sed -i "s/^version: '.*'$/version: '${version}'/" dev-tools/package.yaml
+    sed -i "s/^version:        .*$/version:        ${version}/" dev-tools/hs-backend-booster-dev-tools.cabal
+
     sed -i "s/^version: '.*'$/version: '${version}'/" booster/package.yaml
+    sed -i "s/^version:        .*$/version:        ${version}/" booster/hs-backend-booster.cabal
+
     sed -i "s/^version:        .*$/version:        ${version}/" kore/kore.cabal
+
     sed -i "s/^version:        .*$/version:        ${version}/" ./kore-rpc-types/kore-rpc-types.cabal
+
     sed -i 's/^k-haskell-backend (.*) unstable; urgency=medium$/k-haskell-backend ('"$version"') unstable; urgency=medium/' package/debian/changelog
 }