Skip to content

Commit f7181d3

Browse files
geo2ageo2a
committed
Build existential substitution together with the matching one
1 parent 77c8c57 commit f7181d3

File tree

1 file changed

+65
-36
lines changed

1 file changed

+65
-36
lines changed

‎booster/library/Booster/Pattern/Rewrite.hs

Lines changed: 65 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -304,23 +304,38 @@ applyRule pat@Pattern{ceilConditions} rule =
304304
NE.toList remainder
305305
)
306306
failRewrite $ RuleApplicationUnclear rule pat.term remainder
307-
MatchSuccess substitution -> do
307+
MatchSuccess matchingSubstitution -> do
308+
-- existential variables may be present in rule.rhs and rule.ensures,
309+
-- need to strip prefixes and freshen their names with respect to variables already
310+
-- present in the input pattern and in the unification substitution
311+
varsFromInput <- lift . RewriteT $ asks (.varsToAvoid)
312+
let varsFromPattern = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints)
313+
varsFromSubst = Set.unions . map freeVariables . Map.elems $ matchingSubstitution
314+
forbiddenVars = varsFromInput <> varsFromPattern <> varsFromSubst
315+
existentialSubst =
316+
Map.fromSet
317+
(\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars)
318+
rule.existentials
319+
combinedSubstitution = matchingSubstitution <> existentialSubst
320+
308321
withContext CtxSuccess $ do
309322
logMessage rule
310323
withContext CtxSubstitution
311324
$ logMessage
312325
$ WithJsonMessage
313326
( object
314-
["substitution" .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList substitution)]
327+
[ "substitution"
328+
.= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList combinedSubstitution)
329+
]
315330
)
316331
$ renderOneLineText
317332
$ "Substitution:"
318333
<+> ( hsep $
319334
intersperse "," $
320335
map (\(k, v) -> pretty' @mods k <+> "->" <+> pretty' @mods v) $
321-
Map.toList substitution
336+
Map.toList combinedSubstitution
322337
)
323-
pure substitution
338+
pure combinedSubstitution
324339

325340
-- Also fail the whole rewrite if a rule applies but may introduce
326341
-- an undefined term.
@@ -349,37 +364,29 @@ applyRule pat@Pattern{ceilConditions} rule =
349364
("New path condition ensured, invalidating cache" :: Text)
350365
lift . RewriteT . lift . modify $ \s -> s{equations = mempty}
351366

367+
-- partition ensured constrains into substitution and predicates
352368
let (newSubsitution, newConstraints) = partitionPredicates ensuredConditions
353369

354-
-- existential variables may be present in rule.rhs and rule.ensures,
355-
-- need to strip prefixes and freshen their names with respect to variables already
356-
-- present in the input pattern and in the unification substitution
357-
varsFromInput <- lift . RewriteT $ asks (.varsToAvoid)
358-
let varsFromPattern = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints)
359-
varsFromSubst = Set.unions . map freeVariables . Map.elems $ subst
360-
forbiddenVars = varsFromInput <> varsFromPattern <> varsFromSubst
361-
existentialSubst =
362-
Map.fromSet
363-
(\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars)
364-
rule.existentials
365-
370+
-- merge existing substitution and newly acquired one, applying the latter to the former
366371
normalisedPatternSubst <-
367-
lift $ normaliseSubstitution pat.constraints pat.substitution newSubsitution
368-
369-
-- modify the substitution to include the existentials
370-
let substWithExistentials = subst <> existentialSubst
371-
372+
lift $
373+
normaliseSubstitution
374+
pat.constraints
375+
pat.substitution
376+
newSubsitution
377+
-- NOTE it is necessary to first apply the rule substitution and then the pattern/ensures substitution, but it is suboptimal to traverse the term twice.
378+
-- TODO a substitution composition operator
379+
let rewrittenTerm = substituteInTerm normalisedPatternSubst . substituteInTerm subst $ rule.rhs
380+
substitutedNewConstraints =
381+
Set.fromList $
382+
map
383+
(coerce . substituteInTerm normalisedPatternSubst . substituteInTerm subst . coerce)
384+
newConstraints
372385
let rewritten =
373386
Pattern
374-
(substituteInTerm normalisedPatternSubst . substituteInTerm substWithExistentials $ rule.rhs)
387+
rewrittenTerm
375388
-- adding new constraints that have not been trivially `Top`, substituting the Ex# variables
376-
( pat.constraints
377-
<> ( Set.fromList $
378-
map
379-
(coerce . substituteInTerm normalisedPatternSubst . substituteInTerm substWithExistentials . coerce)
380-
newConstraints
381-
)
382-
)
389+
(pat.constraints <> substitutedNewConstraints)
383390
normalisedPatternSubst
384391
ceilConditions
385392
withContext CtxSuccess $
@@ -396,7 +403,7 @@ applyRule pat@Pattern{ceilConditions} rule =
396403
-- - apply the new substitution to the old substitution
397404
-- - simplify the substituted old substitution, assuming known truth
398405
-- - TODO check for loops?
399-
-- - filter out possible trivial items
406+
-- - TODO filter out possible trivial items?
400407
-- - finally, merge with the new substitution items and return
401408
normaliseSubstitution ::
402409
Set.Set Predicate -> Substitution -> Substitution -> RewriteT io Substitution
@@ -470,15 +477,30 @@ applyRule pat@Pattern{ceilConditions} rule =
470477
concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.requires
471478

472479
-- filter out any predicates known to be _syntactically_ present in the known prior
473-
toCheck <- lift $ filterOutKnownConstraints pat.constraints ruleRequires
480+
toCheck <-
481+
lift $
482+
filterOutKnownConstraints
483+
(pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
484+
ruleRequires
474485

475486
-- simplify the constraints (one by one in isolation). Stop if false, abort rewrite if indeterminate.
476487
unclearRequires <-
477-
catMaybes <$> mapM (checkConstraint id notAppliedIfBottom pat.constraints) toCheck
488+
catMaybes
489+
<$> mapM
490+
( checkConstraint
491+
id
492+
notAppliedIfBottom
493+
(pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
494+
)
495+
toCheck
478496

479497
-- unclear conditions may have been simplified and
480498
-- could now be syntactically present in the path constraints, filter again
481-
stillUnclear <- lift $ filterOutKnownConstraints pat.constraints unclearRequires
499+
stillUnclear <-
500+
lift $
501+
filterOutKnownConstraints
502+
(pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
503+
unclearRequires
482504

483505
-- check unclear requires-clauses in the context of known constraints (priorKnowledge)
484506
solver <- lift $ RewriteT $ (.smtSolver) <$> ask
@@ -491,7 +513,7 @@ applyRule pat@Pattern{ceilConditions} rule =
491513
failRewrite $
492514
RuleConditionUnclear rule . coerce . foldl1 AndTerm $
493515
map coerce stillUnclear
494-
SMT.checkPredicates solver pat.constraints mempty (Set.fromList stillUnclear) >>= \case
516+
SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList stillUnclear) >>= \case
495517
SMT.IsUnknown{} ->
496518
smtUnclear -- abort rewrite if a solver result was Unknown
497519
SMT.IsInvalid -> do
@@ -507,11 +529,18 @@ applyRule pat@Pattern{ceilConditions} rule =
507529
let ruleEnsures =
508530
concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.ensures
509531
newConstraints <-
510-
catMaybes <$> mapM (checkConstraint id trivialIfBottom pat.constraints) ruleEnsures
532+
catMaybes
533+
<$> mapM
534+
( checkConstraint
535+
id
536+
trivialIfBottom
537+
(pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
538+
)
539+
ruleEnsures
511540

512541
-- check all new constraints together with the known side constraints
513542
solver <- lift $ RewriteT $ (.smtSolver) <$> ask
514-
(lift $ SMT.checkPredicates solver pat.constraints mempty (Set.fromList newConstraints)) >>= \case
543+
(lift $ SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList newConstraints)) >>= \case
515544
SMT.IsInvalid -> do
516545
withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text)
517546
RewriteRuleAppT $ pure Trivial

0 commit comments

Comments
 (0)