Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Partial revert of #378 - Fix incorrect KMap injections, received from the LLVM library #417

Merged
merged 2 commits into from
Dec 12, 2023
Merged

Partial revert of #378 - Fix incorrect KMap injections, received from the LLVM library #417

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
aae3e2f
partial revert of #378
goodlyrottenapple Dec 11, 2023
0eee038
Merge branch 'main' into sam/llvm-kmap-injection-fix-partial-revert
goodlyrottenapple Dec 11, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 11 additions & 3 deletions library/Booster/Pattern/Binary.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 (..))
Expand All @@ -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'@
Expand Down Expand Up @@ -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
Expand Down