diff --git a/test/llvm-integration/LLVM.hs b/test/llvm-integration/LLVM.hs index 65aa54eec..34157b3c3 100644 --- a/test/llvm-integration/LLVM.hs +++ b/test/llvm-integration/LLVM.hs @@ -90,6 +90,10 @@ llvmSpec = it "should work with latin-1strings" $ hedgehog . propertyTest . latin1Prop + describe "LLVM hooked Map simplifications" $ + it "should preserve singleton maps" $ + hedgehog . propertyTest . mapKItemInjProp + -------------------------------------------------- -- individual hedgehog property tests and helpers @@ -147,6 +151,18 @@ latin1Prop api = property $ do | otherwise -> error $ "Unexpected sort " <> show s otherTerm -> error $ "Unexpected term " <> show otherTerm +mapKItemInjProp :: Internal.API -> Property +mapKItemInjProp api = property $ do + let k = intTerm 2 + let v = intTerm 2 + LLVM.simplifyTerm api testDef (elem k v) (SortApp "SortMapInt2Int" []) === elem k v + where + elem k v = + SymbolApplication + (kmapElementSymbol sortMapInt2Int) + [] + [k, v] + ------------------------------------------------------------ runKompile :: IO () @@ -277,7 +293,7 @@ sortMapInt2Int = , elementSymbolName = "Lbl'Unds'Int2Int'Pipe'-'-GT-Unds'" , concatSymbolName = "Lbl'Unds'MapInt2Int'Unds'" } - , keySortName = "SortInt" + , keySortName = "SortWrappedInt" , elementSortName = "SortInt" , mapSortName = "SortMapInt2Int" } @@ -1363,7 +1379,7 @@ defSymbols = , Symbol { name = "Lbl'Unds'Int2Int'Pipe'-'-GT-Unds'" , sortVars = [] - , argSorts = [SortApp "SortInt" [], SortApp "SortInt" []] + , argSorts = [SortApp "SortWrappedInt" [], SortApp "SortInt" []] , resultSort = SortApp "SortMapInt2Int" [] , attributes = SymbolAttributes diff --git a/test/llvm-integration/definition/llvm.k b/test/llvm-integration/definition/llvm.k index 766f3c4cd..0e9b3219d 100644 --- a/test/llvm-integration/definition/llvm.k +++ b/test/llvm-integration/definition/llvm.k @@ -5,6 +5,7 @@ module LLVM imports MAP imports SET imports K-EQUAL + imports MAP-INT2INT syntax Num ::= Even | Odd syntax Even ::= Zero() | Two() | Four() | Six() | Eight() | Ten() @@ -39,3 +40,30 @@ module LLVM rule div2(Ten()) => Five() endmodule + +module MAP-INT2INT + imports INT + + syntax WrappedInt + + syntax WrappedInt ::= wrap(Int) [symbol, klabel(wrapInt)] + syntax Int ::= unwrap(WrappedInt) [function, total, injective, symbol, klabel(unwrapInt)] + rule unwrap(wrap(A:Int)) => A + + syntax MapInt2Int [hook(MAP.Map)] + syntax MapInt2Int ::= MapInt2Int MapInt2Int + [ left, function, hook(MAP.concat), klabel(_MapInt2Int_), + symbol, assoc, comm, unit(.MapInt2Int), element(_Int2Int|->_), + index(0), format(%1%n%2) + ] + syntax MapInt2Int ::= ".MapInt2Int" + [ function, total, hook(MAP.unit), + klabel(.MapInt2Int), symbol, latex(\dotCt{MapInt2Int}) + ] + syntax MapInt2Int ::= WrappedInt "Int2Int|->" WrappedInt + [ function, total, hook(MAP.element), + klabel(_Int2Int|->_), symbol, + latex({#1}\mapsto{#2}), injective + ] + +endmodule