Fix collections internalisation (#3841)

Fix pattern synonyms to store e.g. {...REST} as just REST

---------

Co-authored-by: github-actions <[email protected]>

Author: goodlyrottenapple

booster/library/Booster/Pattern/Base.hs

@@ -596,17 +596,20 @@ pattern KMap def keyVals rest <- Term _ (KMapF def keyVals rest)
                     r -> ([], r)
                 newKeyVals = sortAndDeduplicate $ keyVals ++ keyVals'
                 newRest = rest'
-             in Term
-                    argAttributes
-                        { hash =
-                            Hashable.hash
-                                ( "KMap" :: ByteString
-                                , def
-                                , map (\(k, v) -> (hash $ getAttributes k, hash $ getAttributes v)) newKeyVals
-                                , hash . getAttributes <$> newRest
-                                )
-                        }
-                    $ KMapF def newKeyVals newRest
+             in case (newKeyVals, newRest) of
+                    ([], Just r) -> r
+                    _ ->
+                        Term
+                            argAttributes
+                                { hash =
+                                    Hashable.hash
+                                        ( "KMap" :: ByteString
+                                        , def
+                                        , map (\(k, v) -> (hash $ getAttributes k, hash $ getAttributes v)) newKeyVals
+                                        , hash . getAttributes <$> newRest
+                                        )
+                                }
+                            $ KMapF def newKeyVals newRest
 
 pattern KList :: KListDefinition -> [Term] -> Maybe (Term, [Term]) -> Term
 pattern KList def heads rest <- Term _ (KListF def heads rest)
@@ -630,18 +633,21 @@ pattern KList def heads rest <- Term _ (KListF def heads rest)
                                 (\(m, ts) -> (heads <> heads', Just (m, ts <> tails)))
                                 rest'
                     other -> (heads, other)
-             in Term
-                    argAttributes
-                        { hash =
-                            Hashable.hash
-                                ( "KList" :: ByteString
-                                , def
-                                , map (hash . getAttributes) newHeads
-                                , fmap (hash . getAttributes . fst) newRest
-                                , fmap (map (hash . getAttributes) . snd) newRest
-                                )
-                        }
-                    $ KListF def newHeads newRest
+             in case (newHeads, newRest) of
+                    ([], Just (r, [])) -> r
+                    _ ->
+                        Term
+                            argAttributes
+                                { hash =
+                                    Hashable.hash
+                                        ( "KList" :: ByteString
+                                        , def
+                                        , map (hash . getAttributes) newHeads
+                                        , fmap (hash . getAttributes . fst) newRest
+                                        , fmap (map (hash . getAttributes) . snd) newRest
+                                        )
+                                }
+                            $ KListF def newHeads newRest
 
 pattern KSet :: KSetDefinition -> [Term] -> Maybe Term -> Term
 pattern KSet def elements rest <- Term _ (KSetF def elements rest)
@@ -662,17 +668,20 @@ pattern KSet def elements rest <- Term _ (KSetF def elements rest)
                     other -> ([], other)
                 newElements = sortAndDeduplicate $ elements <> elements'
                 newRest = rest'
-             in Term
-                    argAttributes
-                        { hash =
-                            Hashable.hash
-                                ( "KSet" :: ByteString
-                                , def
-                                , map (hash . getAttributes) newElements
-                                , fmap (hash . getAttributes) newRest
-                                )
-                        }
-                    $ KSetF def newElements newRest
+             in case (newElements, newRest) of
+                    ([], Just r) -> r
+                    _ ->
+                        Term
+                            argAttributes
+                                { hash =
+                                    Hashable.hash
+                                        ( "KSet" :: ByteString
+                                        , def
+                                        , map (hash . getAttributes) newElements
+                                        , fmap (hash . getAttributes) newRest
+                                        )
+                                }
+                            $ KSetF def newElements newRest
 {-# COMPLETE AndTerm, SymbolApplication, DomainValue, Var, Injection, KMap, KList, KSet #-}
 
 -- hard-wired injection symbol

booster/unit-tests/Test/Booster/Pattern/InternalCollections.hs

@@ -89,6 +89,9 @@ listInternalisation =
                     replicate 4 $
                         inList [trm| \dv{SomeSort{}}("after variable") |]
            in testCase "mixing a list" $ internalise (listConcat before listAfter) @=? mixedList
+        , testCase "[...REST] normalises to REST" $
+            KList Fixture.testKListDef [] (Just ([trm| REST:SortTestList{} |], []))
+                @=? [trm| REST:SortTestList{} |]
         ]
   where
     internalise = internaliseKList Fixture.testKListDef
@@ -178,6 +181,8 @@ setInternalisation =
                     (Just $ SymbolApplication Fixture.setConcatSym [] [var1, var2])
            in testCase "two variables and some concrete elements in set, concat pushed inwards" $
                 result @=? internalise twoVarsSet
+        , testCase "{...REST} normalises to REST" $
+            KSet Fixture.testKSetDef [] (Just [trm| REST:SortTestSet{} |]) @=? [trm| REST:SortTestSet{} |]
         ]
   where
     internalise = internaliseKSet Fixture.testKSetDef
@@ -270,6 +275,9 @@ mapSmartConstructors =
             let input = makeKMapWithRest [1, 2, 3] (makeKMapWithRest [1, 2, 4] [trm| REST:SortTestMap{}|])
                 expected = makeKMapWithRest [1, 2, 3, 4] [trm| REST:SortTestMap{}|]
              in input @=? expected
+        , testCase "{...REST} normalises to REST" $
+            KMap Fixture.testKMapDefinition [] (Just [trm| REST:SortTestMap{} |])
+                @=? [trm| REST:SortTestMap{} |]
         ]
   where
     -- produced a map of identities for all input ints: x1 |-> x1, x2 |-> x2 ...