transform rawTerm(inj{SortX,SortKItem}(X)) => X while deserialising L…

…LVM data Reference: runtimeverification/llvm-backend#916
runtimeverification · Dec 20, 2023 · 49d7a78 · 49d7a78
1 parent 4ab3fc3
commit 49d7a78
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/library/Booster/Pattern/Binary.hs b/library/Booster/Pattern/Binary.hs
@@ -288,6 +288,12 @@ decodeBlock mbSize = do
             False -> m >> whileNotEnded m
 
     mkSymbolApplication :: ByteString -> [Sort] -> [Block] -> DecodeM Block
+    -- automatically transform `rawTerm(inj{SortX, KItem}(X))` to X:SortX
+    -- see https://github.com/runtimeverification/llvm-backend/issues/916
+    mkSymbolApplication "rawTerm" [] [BTerm t]
+        | Injection sort SortKItem t' <- t
+        , sort == sortOfTerm t' =
+            pure $ BTerm t'
     mkSymbolApplication "\\and" _ [BTerm t1, BTerm t2] = pure $ BTerm $ AndTerm t1 t2
     mkSymbolApplication "\\and" _ bs =
         argError "AndTerm" [BTerm undefined, BTerm undefined] bs