From 83c33a579af27bb5183d733dd4adc85b1db304ec Mon Sep 17 00:00:00 2001
From: Samuel Balco <goodlyrottenapple@gmail.com>
Date: Tue, 12 Dec 2023 09:53:52 +0000
Subject: [PATCH] Partial revert of #378 -  Fix incorrect KMap injections,
 received from the LLVM library (#417)

This PR revers #378 which included a temporary fix for incorrect
injection sorts coming back from the LLVM backend. We keep the more
specific error message introduced in said PR, in case similar issues
arise in the future.

Closes #321
---
 library/Booster/Pattern/Binary.hs | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/library/Booster/Pattern/Binary.hs b/library/Booster/Pattern/Binary.hs
index 297736c0e..b6de401ab 100644
--- a/library/Booster/Pattern/Binary.hs
+++ b/library/Booster/Pattern/Binary.hs
@@ -18,6 +18,7 @@ import Booster.Definition.Base
 import Booster.Pattern.Base
 import Booster.Pattern.Bool (pattern TrueBool)
 import Booster.Pattern.Util (sortOfTerm)
+import Booster.Prettyprinter (renderDefault)
 import Control.Monad (forM_, unless)
 import Control.Monad.Extra (forM)
 import Control.Monad.Trans.Class (MonadTrans (..))
@@ -34,6 +35,7 @@ import Data.Map qualified as Map
 import Data.Set qualified as Set
 import Data.Word (Word64)
 import GHC.Word (Word8)
+import Prettyprinter (pretty)
 import Text.Printf
 
 -- | tags indicating the next element in a block, see @'decodeBlock'@
@@ -316,9 +318,15 @@ decodeBlock mbSize = do
                 pure $ BTerm $ SymbolApplication symbol (zipWith (const id) sortVars sorts) args
             Right (Just symbol@Symbol{sortVars, argSorts}) -> do
                 args <- forM (zip argSorts bs) $ \case
-                    -- temporarily fix injections until https://github.com/runtimeverification/llvm-backend/issues/886 is closed
-                    (srt, BTerm (Injection from _to trm)) -> pure $ Injection from srt trm
-                    (srt, BTerm trm) -> if sortOfTerm trm /= srt then fail "Term has incorrect sort" else pure trm
+                    (srt, BTerm trm) ->
+                        if sortOfTerm trm /= srt
+                            then
+                                fail $
+                                    "Term has incorrect sort. Expecting "
+                                        <> renderDefault (pretty srt)
+                                        <> " but got "
+                                        <> renderDefault (pretty $ sortOfTerm trm)
+                            else pure trm
                     _ -> fail "Expecting term"
                 pure $ BTerm $ SymbolApplication symbol (zipWith (const id) sortVars sorts) args
             Right Nothing -> fail $ "Unknown symbol " <> show name