diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 5d6388ee3..40c2edcd4 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -13,7 +13,7 @@ concurrency: env: ghc_version: '9.2.8' - hlint_version: '3.4.1' + hlint_version: '3.5' fourmolu_version: '0.12.0.0' hpack_version: '0.34.2' diff --git a/library/Booster/JsonRpc.hs b/library/Booster/JsonRpc.hs index 6954f8560..7afb46ca2 100644 --- a/library/Booster/JsonRpc.hs +++ b/library/Booster/JsonRpc.hs @@ -330,7 +330,7 @@ respond stateVar = mkSimplifyResponse state traceData = RpcTypes.Simplify RpcTypes.SimplifyResult{state, logs = mkTraces duration traceData} - pure $ second (uncurry mkSimplifyResponse) result + pure $ second (uncurry mkSimplifyResponse) (fmap (second (map ApplyEquations.eraseStates)) result) RpcTypes.GetModel req -> withContext req._module $ \case (_, _, Nothing) -> do Log.logErrorNS "booster" "get-model request, not supported without SMT solver" @@ -514,7 +514,7 @@ execStateToKoreJson RpcTypes.ExecuteState{term = t, substitution, predicate} = execResponse :: Maybe Double -> RpcTypes.ExecuteRequest -> - (Natural, Seq (RewriteTrace Pattern), RewriteResult Pattern) -> + (Natural, Seq (RewriteTrace ()), RewriteResult Pattern) -> Map Variable Term -> [Syntax.KorePattern] -> Either ErrorObj (RpcTypes.API 'RpcTypes.Res) @@ -619,21 +619,19 @@ execResponse mbDuration req (d, traces, rr) originalSubstitution unsupported = c logs = let traceLogs = - fmap concat - . mapM + concat . catMaybes . toList $ + fmap ( mkLogRewriteTrace (logSuccessfulRewrites, logFailedRewrites) (logSuccessfulSimplifications, logFailedSimplifications) ) - $ toList traces + traces timingLog = fmap (ProcessingTime $ Just Booster) mbDuration in case (timingLog, traceLogs) of - (Nothing, Nothing) -> Nothing - (Nothing, Just []) -> Nothing - (Nothing, Just xs@(_ : _)) -> Just xs - (Just t, Nothing) -> Just [t] - (Just t, Just xs) -> Just (t : xs) + (Nothing, []) -> Nothing + (Nothing, xs@(_ : _)) -> Just xs + (Just t, xs) -> Just (t : xs) toExecState :: Pattern -> Map Variable Term -> [Syntax.KorePattern] -> RpcTypes.ExecuteState toExecState pat sub unsupported = @@ -650,13 +648,12 @@ toExecState pat sub unsupported = | null unsupported = id | otherwise = maybe (Just allUnsupported) (Just . Syntax.KJAnd termSort . (: unsupported)) -mkLogEquationTrace :: (Bool, Bool) -> ApplyEquations.EquationTrace -> Maybe LogEntry +mkLogEquationTrace :: (Bool, Bool) -> ApplyEquations.EquationTrace () -> Maybe LogEntry mkLogEquationTrace - (logSuccessfulSimplifications, logFailedSimplifications) - ApplyEquations.EquationTrace{subjectTerm, ruleId = uid, result} = - case result of - ApplyEquations.Success rewrittenTrm - | logSuccessfulSimplifications -> + (logSuccessfulSimplifications, logFailedSimplifications) = \case + ApplyEquations.EquationApplied _subjectTerm metadata _rewritten -> + if logSuccessfulSimplifications + then Just $ Simplification { originalTerm @@ -664,94 +661,116 @@ mkLogEquationTrace , origin , result = Success - { rewrittenTerm = - Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ rewrittenTrm) mempty mempty + { rewrittenTerm = Nothing , substitution = Nothing , ruleId = fromMaybe "UNKNOWN" _ruleId } } - ApplyEquations.FailedMatch _failReason - | logFailedSimplifications -> - Just $ - Simplification - { originalTerm - , originalTermIndex - , origin - , result = Failure{reason = "Failed match", _ruleId} - } - ApplyEquations.IndeterminateMatch - | logFailedSimplifications -> - Just $ - Simplification - { originalTerm - , originalTermIndex - , origin - , result = Failure{reason = "Indeterminate match", _ruleId} - } - ApplyEquations.IndeterminateCondition _failedConditions - | logFailedSimplifications -> - Just $ - Simplification - { originalTerm - , originalTermIndex - , origin - , result = Failure{reason = "Indeterminate side-condition", _ruleId} - } - ApplyEquations.ConditionFalse{} - | logFailedSimplifications -> - Just $ - Simplification - { originalTerm - , originalTermIndex - , origin - , result = Failure{reason = "Side-condition is false", _ruleId} - } - ApplyEquations.RuleNotPreservingDefinedness - | logFailedSimplifications -> - Just $ - Simplification - { originalTerm - , originalTermIndex - , origin - , result = Failure{reason = "The equation does not preserve definedness", _ruleId} - } - ApplyEquations.MatchConstraintViolated _ varName - | logFailedSimplifications -> - Just $ - Simplification - { originalTerm - , originalTermIndex - , origin - , result = - Failure - { reason = "Symbolic/concrete constraint violated for variable: " <> Text.decodeUtf8 varName - , _ruleId - } - } - _ -> Nothing - where - originalTerm = Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ subjectTerm) mempty mempty - originalTermIndex = Nothing - origin = Booster - _ruleId = fmap getUniqueId uid + else Nothing + where + originalTerm = Nothing + originalTermIndex = Nothing + origin = Booster + _ruleId = fmap getUniqueId metadata.ruleId + ApplyEquations.EquationNotApplied _subjectTerm metadata result -> + case result of + ApplyEquations.Success rewrittenTrm + | logSuccessfulSimplifications -> + Just $ + Simplification + { originalTerm + , originalTermIndex + , origin + , result = + Success + { rewrittenTerm = + Just $ execStateToKoreJson $ toExecState (Pattern.Pattern_ rewrittenTrm) mempty mempty + , substitution = Nothing + , ruleId = fromMaybe "UNKNOWN" _ruleId + } + } + ApplyEquations.FailedMatch _failReason + | logFailedSimplifications -> + Just $ + Simplification + { originalTerm + , originalTermIndex + , origin + , result = Failure{reason = "Failed match", _ruleId} + } + ApplyEquations.IndeterminateMatch + | logFailedSimplifications -> + Just $ + Simplification + { originalTerm + , originalTermIndex + , origin + , result = Failure{reason = "Indeterminate match", _ruleId} + } + ApplyEquations.IndeterminateCondition _failedConditions + | logFailedSimplifications -> + Just $ + Simplification + { originalTerm + , originalTermIndex + , origin + , result = Failure{reason = "Indeterminate side-condition", _ruleId} + } + ApplyEquations.ConditionFalse{} + | logFailedSimplifications -> + Just $ + Simplification + { originalTerm + , originalTermIndex + , origin + , result = Failure{reason = "Side-condition is false", _ruleId} + } + ApplyEquations.RuleNotPreservingDefinedness + | logFailedSimplifications -> + Just $ + Simplification + { originalTerm + , originalTermIndex + , origin + , result = Failure{reason = "The equation does not preserve definedness", _ruleId} + } + ApplyEquations.MatchConstraintViolated _ varName + | logFailedSimplifications -> + Just $ + Simplification + { originalTerm + , originalTermIndex + , origin + , result = + Failure + { reason = "Symbolic/concrete constraint violated for variable: " <> Text.decodeUtf8 varName + , _ruleId + } + } + _ -> Nothing + where + originalTerm = Nothing + originalTermIndex = Nothing + origin = Booster + _ruleId = fmap getUniqueId metadata.ruleId mkLogRewriteTrace :: (Bool, Bool) -> (Bool, Bool) -> - RewriteTrace Pattern -> + RewriteTrace () -> Maybe [LogEntry] mkLogRewriteTrace (logSuccessfulRewrites, logFailedRewrites) equationLogOpts@(logSuccessfulSimplifications, logFailedSimplifications) = \case - RewriteSingleStep _ uid _ res + RewriteSingleStep _ uid _ _res | logSuccessfulRewrites -> Just $ singleton $ Rewrite { result = Success - { rewrittenTerm = Just $ execStateToKoreJson $ toExecState res mempty mempty + { rewrittenTerm = Nothing , substitution = Nothing , ruleId = maybe "UNKNOWN" getUniqueId uid } diff --git a/library/Booster/Pattern/ApplyEquations.hs b/library/Booster/Pattern/ApplyEquations.hs index 34b9a18d6..3452bdf04 100644 --- a/library/Booster/Pattern/ApplyEquations.hs +++ b/library/Booster/Pattern/ApplyEquations.hs @@ -13,6 +13,8 @@ module Booster.Pattern.ApplyEquations ( EquationPreference (..), EquationFailure (..), EquationTrace (..), + eraseStates, + EquationMetadata (..), ApplyEquationResult (..), applyEquations, handleSimplificationEquation, @@ -131,23 +133,47 @@ data EquationState = EquationState , recursionStack :: [Term] , changed :: Bool , predicates :: Set Predicate - , trace :: Seq EquationTrace + , trace :: Seq (EquationTrace Term) , cache :: SimplifierCache } type SimplifierCache = Map Term Term -data EquationTrace = EquationTrace - { subjectTerm :: Term - , location :: Maybe Location +data EquationMetadata = EquationMetadata + { location :: Maybe Location , label :: Maybe Label , ruleId :: Maybe UniqueId - , result :: ApplyEquationResult } deriving stock (Eq, Show) -instance Pretty EquationTrace where - pretty EquationTrace{subjectTerm, location, label, result} = case result of +-- TODO: refactor ApplyEquationResult into EquationNonApplicableReason or something +data EquationTrace term + = EquationApplied term EquationMetadata term + | EquationNotApplied term EquationMetadata ApplyEquationResult + deriving stock (Eq, Show) + +{- | For the given equation trace, construct a new one, + removing the heavy-weight information (the states), + but keeping the meta-data (rule labels). +-} +eraseStates :: EquationTrace Term -> EquationTrace () +eraseStates = \case + EquationApplied _ metadata _ -> EquationApplied () metadata () + EquationNotApplied _ metadata failureInfo -> EquationNotApplied () metadata failureInfo + +instance Pretty (EquationTrace Term) where + pretty (EquationApplied subjectTerm metadata rewritten) = + vsep + [ "Simplifying term" + , prettyTerm + , "to" + , pretty rewritten + , "using " <> locationInfo + ] + where + locationInfo = pretty metadata.location <> " - " <> pretty metadata.label + prettyTerm = pretty subjectTerm + pretty (EquationNotApplied subjectTerm metadata result) = case result of Success rewritten -> vsep [ "Simplifying term" @@ -201,14 +227,14 @@ instance Pretty EquationTrace where , prettyTerm ] where - locationInfo = pretty location <> " - " <> pretty label + locationInfo = pretty metadata.location <> " - " <> pretty metadata.label prettyTerm = pretty subjectTerm -isMatchFailure, isSuccess :: EquationTrace -> Bool -isMatchFailure EquationTrace{result = FailedMatch{}} = True -isMatchFailure EquationTrace{result = IndeterminateMatch{}} = True +isMatchFailure, isSuccess :: EquationTrace Term -> Bool +isMatchFailure (EquationNotApplied _ _ FailedMatch{}) = True +isMatchFailure (EquationNotApplied _ _ IndeterminateMatch{}) = True isMatchFailure _ = False -isSuccess EquationTrace{result = Success{}} = True +isSuccess EquationApplied{} = True isSuccess _ = False startState :: Map Term Term -> EquationState @@ -286,7 +312,7 @@ runEquationT :: Maybe SMT.SMTContext -> SimplifierCache -> EquationT io a -> - io (Either EquationFailure a, [EquationTrace], SimplifierCache) + io (Either EquationFailure a, [EquationTrace Term], SimplifierCache) runEquationT doTracing definition llvmApi smtSolver sCache (EquationT m) = do (res, endState) <- flip runStateT (startState sCache) $ @@ -341,7 +367,7 @@ evaluateTerm :: Maybe LLVM.API -> Maybe SMT.SMTContext -> Term -> - io (Either EquationFailure Term, [EquationTrace], SimplifierCache) + io (Either EquationFailure Term, [EquationTrace Term], SimplifierCache) evaluateTerm doTracing direction def llvmApi smtSolver = runEquationT doTracing def llvmApi smtSolver mempty . evaluateTerm' direction @@ -365,7 +391,7 @@ evaluatePattern :: Maybe SMT.SMTContext -> SimplifierCache -> Pattern -> - io (Either EquationFailure Pattern, [EquationTrace], SimplifierCache) + io (Either EquationFailure Pattern, [EquationTrace Term], SimplifierCache) evaluatePattern doTracing def mLlvmLibrary smtSolver cache = runEquationT doTracing def mLlvmLibrary smtSolver cache . evaluatePattern' @@ -426,7 +452,7 @@ applyTerm direction pref trm = do Right result -> do when (result /= t) $ do setChanged - traceRuleApplication t Nothing (Just "LLVM") Nothing $ Success result + emitEquationTrace t Nothing (Just "LLVM") Nothing $ Success result pure result else -- use equations apply config t @@ -435,7 +461,7 @@ applyTerm direction pref trm = do Just cached -> do when (t /= cached) $ do setChanged - traceRuleApplication t Nothing (Just "Cache") Nothing $ Success cached + emitEquationTrace t Nothing (Just "Cache") Nothing $ Success cached pure cached -- Bottom-up evaluation traverses AST nodes in post-order but finds work top-down @@ -631,10 +657,14 @@ applyEquations theory handler term = do pure term -- nothing to do, term stays the same processEquations (eq : rest) = do res <- applyEquation term eq - traceRuleApplication term eq.attributes.location eq.attributes.ruleLabel eq.attributes.uniqueId res + emitEquationTrace term eq.attributes.location eq.attributes.ruleLabel eq.attributes.uniqueId res handler (\t -> setChanged >> pure t) (processEquations rest) (pure term) res -traceRuleApplication :: +{- | Trace application or failure to apply an equation + * log into stderr + * accumulate the trace into the state +-} +emitEquationTrace :: MonadLoggerIO io => Term -> Maybe Location -> @@ -642,8 +672,11 @@ traceRuleApplication :: Maybe UniqueId -> ApplyEquationResult -> EquationT io () -traceRuleApplication t loc lbl uid res = do - let newTraceItem = EquationTrace t loc lbl uid res +emitEquationTrace t loc lbl uid res = do + let newTraceItem = + case res of + Success rewritten -> EquationApplied t (EquationMetadata loc lbl uid) rewritten + failure -> EquationNotApplied t (EquationMetadata loc lbl uid) failure prettyItem = pack . renderDefault . pretty $ newTraceItem logOther (LevelOther "Simplify") prettyItem case res of @@ -805,7 +838,7 @@ simplifyConstraint :: Maybe SMT.SMTContext -> SimplifierCache -> Predicate -> - io (Either EquationFailure Predicate, [EquationTrace], SimplifierCache) + io (Either EquationFailure Predicate, [EquationTrace Term], SimplifierCache) simplifyConstraint doTracing def mbApi mbSMT cache (Predicate p) = runEquationT doTracing def mbApi mbSMT cache $ (coerce <$>) . simplifyConstraint' True $ p @@ -817,7 +850,7 @@ simplifyConstraints :: Maybe SMT.SMTContext -> SimplifierCache -> [Predicate] -> - io (Either EquationFailure [Predicate], [EquationTrace], SimplifierCache) + io (Either EquationFailure [Predicate], [EquationTrace Term], SimplifierCache) simplifyConstraints doTracing def mbApi mbSMT cache ps = runEquationT doTracing def mbApi mbSMT cache $ concatMap splitAndBools diff --git a/library/Booster/Pattern/Rewrite.hs b/library/Booster/Pattern/Rewrite.hs index f7f01547d..69ce0bfca 100644 --- a/library/Booster/Pattern/Rewrite.hs +++ b/library/Booster/Pattern/Rewrite.hs @@ -45,6 +45,7 @@ import Booster.Pattern.ApplyEquations ( evaluatePattern, simplifyConstraint, ) +import Booster.Pattern.ApplyEquations qualified as ApplyEquations import Booster.Pattern.Base import Booster.Pattern.Bool import Booster.Pattern.Index (TermIndex (..), kCellTermIndex) @@ -474,9 +475,23 @@ data RewriteTrace pat | -- | attempted rewrite failed RewriteStepFailed (RewriteFailed "Rewrite") | -- | Applied simplification to the pattern - RewriteSimplified [EquationTrace] (Maybe EquationFailure) - deriving stock (Eq, Show) - deriving (Functor, Foldable, Traversable) + RewriteSimplified [EquationTrace (TracePayload pat)] (Maybe EquationFailure) + +type family TracePayload pat where + TracePayload Pattern = Term + TracePayload () = () + +{- | For the given rewrite trace, construct a new one, + removing the heavy-weight information (the states), + but keeping the meta-data (rule labels). +-} +eraseStates :: RewriteTrace Pattern -> RewriteTrace () +eraseStates = \case + RewriteSingleStep rule_label mUniqueId _preState _postState -> RewriteSingleStep rule_label mUniqueId () () + RewriteBranchingStep _state branchMetadata -> RewriteBranchingStep () branchMetadata + RewriteStepFailed failureInfo -> RewriteStepFailed failureInfo + RewriteSimplified equationTraces mbEquationFailure -> + RewriteSimplified (map ApplyEquations.eraseStates equationTraces) mbEquationFailure instance Pretty (RewriteTrace Pattern) where pretty = \case @@ -614,7 +629,7 @@ performRewrite :: -- | terminal rule labels [Text] -> Pattern -> - io (Natural, Seq (RewriteTrace Pattern), RewriteResult Pattern) + io (Natural, Seq (RewriteTrace ()), RewriteResult Pattern) performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalLabels pat = do (rr, RewriteStepsState{counter, traces}) <- flip runStateT rewriteStart $ doSteps False pat @@ -633,7 +648,8 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL showCounter = (<> " steps.") . pack . show - rewriteTrace t = do + emitRewriteTrace :: RewriteTrace Pattern -> StateT RewriteStepsState io () + emitRewriteTrace t = do let prettyT = pack $ renderDefault $ pretty t logRewrite prettyT case t of @@ -642,7 +658,7 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL _other -> pure () when doTracing $ modify $ - \rss@RewriteStepsState{traces} -> rss{traces = traces |> t} + \rss@RewriteStepsState{traces} -> rss{traces = traces |> eraseStates t} incrementCounter = modify $ \rss@RewriteStepsState{counter} -> rss{counter = counter + 1} @@ -658,15 +674,15 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL logTraces traces case res of Right newPattern -> do - rewriteTrace $ RewriteSimplified traces Nothing + emitRewriteTrace $ RewriteSimplified traces Nothing pure $ Just newPattern Left r@(SideConditionFalse _p) -> do logSimplify "A side condition was found to be false, pruning" - rewriteTrace $ RewriteSimplified traces (Just r) + emitRewriteTrace $ RewriteSimplified traces (Just r) pure Nothing Left r@UndefinedTerm{} -> do logSimplify "Term is undefined, pruning" - rewriteTrace $ RewriteSimplified traces (Just r) + emitRewriteTrace $ RewriteSimplified traces (Just r) pure Nothing -- NB any errors here might be caused by simplifying one -- of the constraints, so we cannot use partial results @@ -682,7 +698,7 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL ] ) -- could output term before and after at debug or custom log level - rewriteTrace $ RewriteSimplified traces (Just r) + emitRewriteTrace $ RewriteSimplified traces (Just r) pure $ Just p Left r@(EquationLoop (t : ts)) -> do logError "Equation evaluation loop" @@ -693,11 +709,11 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL <> prettyText l <> ": \n" <> Text.unlines (map (prettyText . fst) termDiffs) - rewriteTrace $ RewriteSimplified traces (Just r) + emitRewriteTrace $ RewriteSimplified traces (Just r) pure $ Just p Left other -> do logError . pack $ "Simplification error during rewrite: " <> show other - rewriteTrace $ RewriteSimplified traces (Just other) + emitRewriteTrace $ RewriteSimplified traces (Just other) pure $ Just p -- Results may change when simplification prunes a false side @@ -762,12 +778,12 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL >>= \case Right (RewriteFinished mlbl uniqueId single, cache) -> do whenJust mlbl $ \lbl -> - rewriteTrace $ RewriteSingleStep lbl uniqueId pat' single + emitRewriteTrace $ RewriteSingleStep lbl uniqueId pat' single updateCache cache incrementCounter doSteps False single Right (terminal@(RewriteTerminal lbl uniqueId single), _cache) -> do - rewriteTrace $ RewriteSingleStep lbl uniqueId pat' single + emitRewriteTrace $ RewriteSingleStep lbl uniqueId pat' single logRewrite $ "Terminal rule after " <> showCounter (counter + 1) incrementCounter @@ -786,11 +802,11 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL RewriteFinished mlbl uniqueId single -> do logRewrite "All but one branch pruned, continuing" whenJust mlbl $ \lbl -> - rewriteTrace $ RewriteSingleStep lbl uniqueId pat' single + emitRewriteTrace $ RewriteSingleStep lbl uniqueId pat' single incrementCounter doSteps False single RewriteBranch pat'' branches -> do - rewriteTrace $ RewriteBranchingStep pat'' $ fmap (\(lbl, uid, _) -> (lbl, uid)) branches + emitRewriteTrace $ RewriteBranchingStep pat'' $ fmap (\(lbl, uid, _) -> (lbl, uid)) branches pure simplified _other -> error "simplifyResult: Unexpected return value" Right (cutPoint@(RewriteCutPoint lbl _ _ _), _) -> do @@ -807,7 +823,7 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL Right (stuck@RewriteStuck{}, cache) -> do logRewrite $ "Stopped after " <> showCounter counter updateCache cache - rewriteTrace $ RewriteStepFailed $ NoApplicableRules pat' + emitRewriteTrace $ RewriteStepFailed $ NoApplicableRules pat' if wasSimplified then pure stuck else withSimplified pat' "Retrying with simplified pattern" (doSteps True) @@ -821,12 +837,12 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL -- unsimplified, simplify and retry rewriting once Left failure@RuleApplicationUnclear{} | not wasSimplified -> do - rewriteTrace $ RewriteStepFailed failure + emitRewriteTrace $ RewriteStepFailed failure -- simplify remainders, substitute and rerun. -- If failed, do the pattern-wide simplfication and rerun again withSimplified pat' "Retrying with simplified pattern" (doSteps True) Left failure -> do - rewriteTrace $ RewriteStepFailed failure + emitRewriteTrace $ RewriteStepFailed failure logAborts . renderText $ pretty failure let msg = "Aborted after " <> showCounter counter if wasSimplified @@ -844,7 +860,7 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL data RewriteStepsState = RewriteStepsState { counter :: !Natural - , traces :: !(Seq (RewriteTrace Pattern)) + , traces :: !(Seq (RewriteTrace ())) , simplifierCache :: SimplifierCache , smtSolver :: Maybe SMT.SMTContext } diff --git a/scripts/hlint.sh b/scripts/hlint.sh index 7d3a96206..27a00dcca 100755 --- a/scripts/hlint.sh +++ b/scripts/hlint.sh @@ -1,6 +1,6 @@ #!/usr/bin/env bash set -euxo pipefail -expected_hlint_version=v3.4.1 +expected_hlint_version=v3.5 hlint=${HLINT:-$(which hlint)} || { echo 'No hlint!' ; exit 1 ; } hlint_version=$(${hlint} --version | head -n1 | cut --field=1 --delimiter=',' | cut --field=2 --delimiter=' ') [[ ${hlint_version} == ${expected_hlint_version} ]] || { echo "Unexpected hlint version, got ${hlint_version}, expected ${expected_hlint_version}" ; exit 1 ; } diff --git a/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev b/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev index 411f3665d..12b421e0d 100644 --- a/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev +++ b/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev @@ -102,96 +102,6 @@ "origin": "booster", "result": { "tag": "success", - "rewritten-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "f" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, "rule-id": "928fbc2c9e62487c0fdc40fb4eeff63c14c06f9cd3e4bdde5c62be73b318d352" } }, @@ -200,96 +110,6 @@ "origin": "booster", "result": { "tag": "success", - "rewritten-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "g" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, "rule-id": "51a4003346d710ea028036ee9bdeaf964113e46e843a8c8f15a8f0f886be1fcf" } }, diff --git a/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.json b/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.json index 411f3665d..12b421e0d 100644 --- a/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.json +++ b/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.json @@ -102,96 +102,6 @@ "origin": "booster", "result": { "tag": "success", - "rewritten-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "f" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, "rule-id": "928fbc2c9e62487c0fdc40fb4eeff63c14c06f9cd3e4bdde5c62be73b318d352" } }, @@ -200,96 +110,6 @@ "origin": "booster", "result": { "tag": "success", - "rewritten-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "g" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, "rule-id": "51a4003346d710ea028036ee9bdeaf964113e46e843a8c8f15a8f0f886be1fcf" } }, diff --git a/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev b/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev index 6e23939ba..92827d700 100644 --- a/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev +++ b/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev @@ -103,96 +103,6 @@ "origin": "booster", "result": { "tag": "success", - "rewritten-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "f" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, "rule-id": "928fbc2c9e62487c0fdc40fb4eeff63c14c06f9cd3e4bdde5c62be73b318d352" } }, @@ -201,96 +111,6 @@ "origin": "booster", "result": { "tag": "success", - "rewritten-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "g" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, "rule-id": "51a4003346d710ea028036ee9bdeaf964113e46e843a8c8f15a8f0f886be1fcf" } } diff --git a/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.json b/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.json index 6e23939ba..92827d700 100644 --- a/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.json +++ b/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.json @@ -103,96 +103,6 @@ "origin": "booster", "result": { "tag": "success", - "rewritten-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "f" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, "rule-id": "928fbc2c9e62487c0fdc40fb4eeff63c14c06f9cd3e4bdde5c62be73b318d352" } }, @@ -201,96 +111,6 @@ "origin": "booster", "result": { "tag": "success", - "rewritten-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "g" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, "rule-id": "51a4003346d710ea028036ee9bdeaf964113e46e843a8c8f15a8f0f886be1fcf" } } diff --git a/test/rpc-integration/test-simplify/response-with-logging.json b/test/rpc-integration/test-simplify/response-with-logging.json index 059c9b276..4e70f4188 100644 --- a/test/rpc-integration/test-simplify/response-with-logging.json +++ b/test/rpc-integration/test-simplify/response-with-logging.json @@ -76,42 +76,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lblf'LParUndsRParUnds'SIMPLIFY'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "34" - } - ] - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - }, "result": { "tag": "failure", "reason": "Failed match", @@ -121,42 +85,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lblf'LParUndsRParUnds'SIMPLIFY'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "34" - } - ] - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - }, "result": { "tag": "failure", "reason": "Failed match", @@ -166,42 +94,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lblf'LParUndsRParUnds'SIMPLIFY'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "34" - } - ] - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - }, "result": { "tag": "failure", "reason": "Failed match", @@ -211,42 +103,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lblf'LParUndsRParUnds'SIMPLIFY'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "34" - } - ] - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - }, "result": { "tag": "failure", "reason": "Failed match", @@ -256,42 +112,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lblf'LParUndsRParUnds'SIMPLIFY'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "34" - } - ] - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - }, "result": { "tag": "failure", "reason": "Indeterminate match", @@ -301,42 +121,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lblf'LParUndsRParUnds'SIMPLIFY'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "34" - } - ] - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - }, "result": { "tag": "failure", "reason": "Indeterminate match", @@ -346,42 +130,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lblf'LParUndsRParUnds'SIMPLIFY'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "34" - } - ] - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - }, "result": { "tag": "failure", "reason": "Symbolic/concrete constraint violated for variable: Eq#VarB", @@ -391,58 +139,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "12" - }, - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lblf'LParUndsRParUnds'SIMPLIFY'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "34" - } - ] - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - ] - } - }, "result": { "tag": "failure", "reason": "Indeterminate match", @@ -452,147 +148,14 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "12" - }, - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lblf'LParUndsRParUnds'SIMPLIFY'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "34" - } - ] - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - ] - } - }, "result": { "tag": "success", - "rewritten-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lblf'LParUndsRParUnds'SIMPLIFY'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "34" - } - ] - }, - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "12" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - ] - } - }, "rule-id": "268b9a7c15e96c6d7eca16bc9022dc880f06a15ca8018eb1854b9836fc3e965c" } }, { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "12" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - }, "result": { "tag": "failure", "reason": "Failed match", @@ -602,35 +165,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "12" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - }, "result": { "tag": "failure", "reason": "Failed match", @@ -640,35 +174,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "12" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - }, "result": { "tag": "failure", "reason": "Failed match", @@ -678,35 +183,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "12" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - }, "result": { "tag": "failure", "reason": "Failed match", @@ -716,35 +192,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "12" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - }, "result": { "tag": "failure", "reason": "Failed match", @@ -754,35 +201,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "12" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - }, "result": { "tag": "failure", "reason": "Failed match", @@ -792,35 +210,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "12" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - }, "result": { "tag": "failure", "reason": "Symbolic/concrete constraint violated for variable: Eq#VarB", @@ -830,58 +219,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lblf'LParUndsRParUnds'SIMPLIFY'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "34" - } - ] - }, - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "12" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - ] - } - }, "result": { "tag": "failure", "reason": "Indeterminate match", @@ -891,58 +228,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lblf'LParUndsRParUnds'SIMPLIFY'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "34" - } - ] - }, - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "12" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - ] - } - }, "result": { "tag": "failure", "reason": "Symbolic/concrete constraint violated for variable: Eq#VarB", @@ -952,58 +237,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lblf'LParUndsRParUnds'SIMPLIFY'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "34" - } - ] - }, - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "12" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - ] - } - }, "result": { "tag": "failure", "reason": "Symbolic/concrete constraint violated for variable: Eq#VarC", @@ -1013,58 +246,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lblf'LParUndsRParUnds'SIMPLIFY'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "34" - } - ] - }, - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "12" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - ] - } - }, "result": { "tag": "failure", "reason": "Indeterminate match", @@ -1074,58 +255,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lblf'LParUndsRParUnds'SIMPLIFY'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "34" - } - ] - }, - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "12" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - ] - } - }, "result": { "tag": "failure", "reason": "Indeterminate match", @@ -1135,58 +264,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lblf'LParUndsRParUnds'SIMPLIFY'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "34" - } - ] - }, - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "12" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - ] - } - }, "result": { "tag": "failure", "reason": "Indeterminate match", @@ -1196,58 +273,6 @@ { "tag": "simplification", "origin": "booster", - "original-term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lblf'LParUndsRParUnds'SIMPLIFY'Unds'Int'Unds'Int", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "34" - } - ] - }, - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "12" - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "56" - } - ] - } - ] - } - }, "result": { "tag": "failure", "reason": "Symbolic/concrete constraint violated for variable: Eq#VarI",