diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs index ad52f701fe..5c375bb535 100644 --- a/booster/library/Booster/Syntax/Json/Internalise.hs +++ b/booster/library/Booster/Syntax/Json/Internalise.hs @@ -215,8 +215,15 @@ internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition exi variableSort <- lookupInternalSort sortVars definition.sorts p sort let variableName = textToBS var.getId pure $ Internal.Variable{variableSort, variableName} - (term, preds, ceilConditions, subst, unknown) <- internalisePattern allowAlias checkSubsorts sortVars definition p - pure $ IsPattern $ (existentialVars, Internal.Pattern{term,constraints = Set.fromList preds, ceilConditions}, subst, unknown) + (term, preds, ceilConditions, subst, unknown) <- + internalisePattern allowAlias checkSubsorts sortVars definition p + pure $ + IsPattern $ + ( existentialVars + , Internal.Pattern{term, constraints = Set.fromList preds, ceilConditions} + , subst + , unknown + ) where isTop = \case [Syntax.KJTop{sort}] -> Just $ IsTop sort diff --git a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs index 3aef3fe334..4bd05808b0 100644 --- a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs +++ b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs @@ -877,7 +877,12 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do | v `Set.member` existentials' = Util.modifyVarName Util.markAsExVar v | otherwise = Util.modifyVarName Util.markAsRuleVar v (rhs, ensures) <- - internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported partialDefinition ref Nothing renameVariable right + internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported + partialDefinition + ref + Nothing + renameVariable + right let notPreservesDefinednessReasons = -- users can override the definedness computation by an explicit attribute if coerce axAttributes.preserving @@ -936,7 +941,12 @@ internaliseRewriteRule partialDefinition exs aliasName aliasArgs right axAttribu | v `Set.member` existentials' = Util.modifyVarName Util.markAsExVar v | otherwise = Util.modifyVarName Util.markAsRuleVar v (rhs, ensures) <- - internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported partialDefinition ref Nothing renameVariable right + internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported + partialDefinition + ref + Nothing + renameVariable + right let notPreservesDefinednessReasons = -- users can override the definedness computation by an explicit attribute @@ -1006,8 +1016,8 @@ internaliseSimpleEquation partialDef precond left right sortVars attrs partialDef (sourceRef attrs) (Just sortVars) - (Util.modifyVarName ("Eq#" <>)) $ - Syntax.KJAnd left.sort [left, precond] + (Util.modifyVarName ("Eq#" <>)) + $ Syntax.KJAnd left.sort [left, precond] (rhs, ensures) <- internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported partialDef