From 5defe0abb25685821764d40a18dfd7e8fdfc7375 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 13 Jun 2025 10:21:36 +1000 Subject: [PATCH 1/3] Fix LIST.in hook for non-constructor-like list elements 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. --- booster/library/Booster/Builtin/LIST.hs | 15 +++++++++++---- booster/library/Booster/Pattern/Base.hs | 3 +++ booster/unit-tests/Test/Booster/Builtin.hs | 22 +++++++++++++++++++++- 3 files changed, 35 insertions(+), 5 deletions(-) diff --git a/booster/library/Booster/Builtin/LIST.hs b/booster/library/Booster/Builtin/LIST.hs index 89b02a1754..5636bcce3c 100644 --- a/booster/library/Booster/Builtin/LIST.hs +++ b/booster/library/Booster/Builtin/LIST.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE PatternSynonyms #-} + {- | Copyright : (c) Runtime Verification, 2023 License : BSD-3-Clause @@ -17,7 +19,6 @@ 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 ( @@ -25,6 +26,7 @@ import Booster.Definition.Attributes.Base ( 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 + | not (e `elem` 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 diff --git a/booster/library/Booster/Pattern/Base.hs b/booster/library/Booster/Pattern/Base.hs index f8991bc259..3d64019e5b 100644 --- a/booster/library/Booster/Pattern/Base.hs +++ b/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 } diff --git a/booster/unit-tests/Test/Booster/Builtin.hs b/booster/unit-tests/Test/Booster/Builtin.hs index c394926f9a..281faa2cb5 100644 --- a/booster/unit-tests/Test/Booster/Builtin.hs +++ b/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 From d9d801e3b6ea89bc9baba0efe74e56f2f8027919 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 13 Jun 2025 15:08:24 +1000 Subject: [PATCH 2/3] hlint --- booster/library/Booster/Builtin/LIST.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/booster/library/Booster/Builtin/LIST.hs b/booster/library/Booster/Builtin/LIST.hs index 5636bcce3c..8e3eaeadca 100644 --- a/booster/library/Booster/Builtin/LIST.hs +++ b/booster/library/Booster/Builtin/LIST.hs @@ -113,7 +113,7 @@ listInHook [e, KList _ heads rest] = case rest of Nothing | e `elem` heads -> pure $ Just TrueBool - | not (e `elem` heads) + | e `notElem` heads , all isConstructorLike_ (e : heads) -> pure $ Just FalseBool | otherwise -> pure Nothing From a4ef886ec2629a7cf05e66adfc70b65adbc41fb9 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 13 Jun 2025 15:37:00 +1000 Subject: [PATCH 3/3] replace version in (generated but git-controlled) cabal files, too --- package/version.sh | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/package/version.sh b/package/version.sh index b1453753f8..6f923a9ab5 100755 --- a/package/version.sh +++ b/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 }