Check whether all existential variables are quantified when internali…

…sing rules

library/Booster/Pattern/Util.hs

@@ -13,6 +13,7 @@ module Booster.Pattern.Util (
     modifyVarName,
     modifyVarNameConcreteness,
     freeVariables,
+    freeVariablesPattern,
     isConstructorSymbol,
     isSortInjectionSymbol,
     isFunctionSymbol,
@@ -200,6 +201,9 @@ modifyVarNameConcreteness f = \case
 freeVariables :: Term -> Set Variable
 freeVariables (Term attributes _) = attributes.variables
 
+freeVariablesPattern :: Pattern -> Set Variable
+freeVariablesPattern p = Set.unions $ map freeVariables $ p.term : (map coerce . Set.toList) p.constraints
+
 isConcrete :: Term -> Bool
 isConcrete = Set.null . freeVariables
 

library/Booster/Prettyprinter.hs

@@ -28,6 +28,7 @@ module Booster.Prettyprinter (
     escapeCharT,
     unparseAssoc',
     unparseConcat',
+    list,
 ) where
 
 import Control.Arrow ((>>>)) -- TODO: remove

library/Booster/Syntax/ParsedKore/Internalise.hs

@@ -798,7 +798,15 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do
             | v `Set.member` existentials' = Util.modifyVarName Util.markAsExVar v
             | otherwise = Util.modifyVarName Util.markAsRuleVar v
     rhs <- internalisePattern' ref renameVariable right
-    let notPreservesDefinednessReasons =
+    let lhsVars =
+            Set.map (\v@Variable{variableName} -> v{variableName = Util.stripMarker variableName}) $
+                Util.freeVariablesPattern lhs
+        rhsVars =
+            Set.filter (\v -> not $ v `Set.member` existentials') $
+                Set.map (\v@Variable{variableName} -> v{variableName = Util.stripMarker variableName}) $
+                    Util.freeVariablesPattern rhs
+
+        notPreservesDefinednessReasons =
             -- users can override the definedness computation by an explicit attribute
             if coerce axAttributes.preserving
                 then []
@@ -811,6 +819,11 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do
         computedAttributes =
             ComputedAxiomAttributes{notPreservesDefinednessReasons, containsAcSymbols}
         existentials = Set.map (Util.modifyVarName Util.markAsExVar) existentials'
+
+    unless (rhsVars `Set.isSubsetOf` lhsVars) $
+        throwE $
+            UnboundVariables ref $
+                rhsVars `Set.difference` lhsVars
     return
         RewriteRule
             { lhs = lhs.term
@@ -1288,6 +1301,7 @@ data DefinitionError
     | DefinitionTermOrPredicateError SourceRef TermOrPredicateError
     | ElemSymbolMalformed Def.Symbol
     | ElemSymbolNotFound Def.SymbolName
+    | UnboundVariables SourceRef (Set Variable)
     deriving stock (Eq, Show)
 
 instance Pretty DefinitionError where
@@ -1323,6 +1337,11 @@ instance Pretty DefinitionError where
             pretty $ "Element{} symbol is malformed: " <> show sym
         ElemSymbolNotFound sym ->
             pretty $ "Expected an element{} symbol " <> show sym
+        UnboundVariables ref vars ->
+            "Unbound variable "
+                <> Booster.Prettyprinter.list "" "" (map pretty $ Set.toList vars)
+                <> " in rule "
+                <> pretty ref
 
 {- | ToJSON instance (user-facing for add-module endpoint):
 Renders the error string as 'error', with minimal context.