From f957048e0390a392ed3a7a5189d2c3201bdf6f55 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 17 Jul 2024 18:17:20 +0200 Subject: [PATCH] Internalise equations with existentials in requires --- .../library/Booster/Pattern/ApplyEquations.hs | 1 + .../Booster/Syntax/ParsedKore/Internalise.hs | 46 +++++++++++++------ 2 files changed, 33 insertions(+), 14 deletions(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 47ca4a6ab8..5b963179f6 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -727,6 +727,7 @@ applyEquation term rule = getPrettyModifiers >>= \case ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> do -- ensured by internalisation: no existentials in equations + -- TODO allow existentials, but only in the requires clause unless (null rule.existentials) $ do withContext CtxAbort $ logMessage ("Equation with existentials" :: Text) diff --git a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs index 4949ae0871..34dbd590d7 100644 --- a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs +++ b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs @@ -767,11 +767,17 @@ extractExistentials = \case <$> extractExistentials arg other -> (other, []) +-- | Useful for getting the requires clause of a simplification axiom, i.e. throwing away the \in conjuncts +getFirstConjunct :: Syntax.KorePattern -> Syntax.KorePattern +getFirstConjunct = \case + Syntax.KJAnd{patterns = (headConjunct : _)} -> headConjunct + other -> other + internaliseAxiom :: PartialDefinition -> ParsedAxiom -> Except DefinitionError (Maybe AxiomResult) -internaliseAxiom (Partial partialDefinition) parsedAxiom = +internaliseAxiom (Partial partialDefinition) parsedAxiom = do classifyAxiom parsedAxiom >>= maybe (pure Nothing) processAxiom where processAxiom :: AxiomData -> Except DefinitionError (Maybe AxiomResult) @@ -854,7 +860,10 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do -- to avoid name clashes with patterns from the user; -- filter out literal `Top` constraints lhs <- internalisePattern' ref (Util.modifyVarName Util.markAsRuleVar) left - existentials' <- fmap Set.fromList $ withExcept (DefinitionPatternError ref) $ mapM mkVar exs + existentials' <- + fmap Set.fromList $ + withExcept (DefinitionPatternError ref) $ + mapM (mkVar partialDefinition right) exs let renameVariable v | v `Set.member` existentials' = Util.modifyVarName Util.markAsExVar v | otherwise = Util.modifyVarName Util.markAsRuleVar v @@ -895,10 +904,11 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do DefinitionPatternError ref (NotSupported (head unsupported)) pure $ removeTrueBools $ Util.modifyVariables f pat - mkVar (name, sort) = do - variableSort <- lookupInternalSort Nothing partialDefinition.sorts right sort - let variableName = textToBS name.getId - pure $ Variable{variableSort, variableName} +mkVar :: KoreDefinition -> Syntax.KorePattern -> (Id, Sort) -> Except PatternError Variable +mkVar partialDefinition right (name, sort) = do + variableSort <- lookupInternalSort Nothing partialDefinition.sorts right sort + let variableName = textToBS name.getId + pure $ Variable{variableSort, variableName} internaliseRewriteRule :: KoreDefinition -> @@ -929,7 +939,10 @@ internaliseRewriteRule partialDefinition exs aliasName aliasArgs right axAttribu fmap (removeTrueBools . Util.modifyVariables (Util.modifyVarName Util.markAsRuleVar)) $ retractPattern result `orFailWith` DefinitionTermOrPredicateError ref (PatternExpected result) - existentials' <- fmap Set.fromList $ withExcept (DefinitionPatternError ref) $ mapM mkVar exs + existentials' <- + fmap Set.fromList $ + withExcept (DefinitionPatternError ref) $ + mapM (mkVar partialDefinition right) exs let renameVariable v | v `Set.member` existentials' = Util.modifyVarName Util.markAsExVar v | otherwise = Util.modifyVarName Util.markAsRuleVar v @@ -963,11 +976,6 @@ internaliseRewriteRule partialDefinition exs aliasName aliasArgs right axAttribu , existentials } where - mkVar (name, sort) = do - variableSort <- lookupInternalSort Nothing partialDefinition.sorts right sort - let variableName = textToBS name.getId - pure $ Variable{variableSort, variableName} - internalisePattern' ref f t = do (pat, substitution, unsupported) <- withExcept (DefinitionPatternError ref) $ @@ -1028,8 +1036,18 @@ internaliseSimpleEquation partialDef precond left right sortVars attrs | not (coerce attrs.simplification) = error $ "internaliseSimpleEquation should only be called for simplifications" <> show attrs | Syntax.KJApp{} <- left = do + -- extract the top-level existentials from precond and strip them + let (precondNoExists, existentials) = Debug.trace (show precond) $ extractExistentials (getFirstConjunct precond) + + let ref = Debug.trace (show precondNoExists) $ sourceRef attrs + + existentials' <- + fmap Set.fromList $ + withExcept (DefinitionPatternError ref) $ + mapM (mkVar partialDef left) existentials + -- this ensures that `left` is a _term_ (invariant guarded by classifyAxiom) - lhs <- internalisePattern' $ Syntax.KJAnd left.sort [left, precond] + lhs <- internalisePattern' $ Syntax.KJAnd left.sort [left, precondNoExists] rhs <- internalisePattern' right let -- checking the lhs term, too, as a safe approximation @@ -1057,7 +1075,7 @@ internaliseSimpleEquation partialDef precond left right sortVars attrs , ensures = rhs.constraints , attributes , computedAttributes - , existentials = Set.empty + , existentials = existentials' } | otherwise = -- we hit a simplification with top level ML connective or an