Skip to content

Commit

Permalink
Format with fourmolu
Browse files Browse the repository at this point in the history
  • Loading branch information
github-actions committed Aug 15, 2024
1 parent 039e572 commit 02ed613
Show file tree
Hide file tree
Showing 2 changed files with 23 additions and 6 deletions.
11 changes: 9 additions & 2 deletions booster/library/Booster/Syntax/Json/Internalise.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
18 changes: 14 additions & 4 deletions booster/library/Booster/Syntax/ParsedKore/Internalise.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit 02ed613

Please sign in to comment.