Internalise equations with existentials in requires

runtimeverification · Jul 17, 2024 · f957048 · f957048
1 parent 43e5d45
commit f957048
Show file tree

Hide file tree

Showing 2 changed files with 33 additions and 14 deletions.
diff --git 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
@@ -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