WIP Syntactic simplifications

booster/library/Booster/Definition/Attributes/Base.hs

@@ -35,6 +35,7 @@ module Booster.Definition.Attributes.Base (
     Position (..),
     FileSource (..),
     Priority (..),
+    SyntacticClauses (..),
     pattern IsIdem,
     pattern IsNotIdem,
     pattern IsAssoc,
@@ -97,6 +98,7 @@ data AxiomAttributes = AxiomAttributes
     , preserving :: Flag "preservingDefinedness" -- this will override the computed attribute
     , concreteness :: Concreteness
     , smtLemma :: Flag "isSMTLemma"
+    , syntacticClauses :: SyntacticClauses -- indices of conjuncts in rule.requires to be checked syntactically
     }
     deriving stock (Eq, Ord, Show, Generic)
     deriving anyclass (NFData)
@@ -174,6 +176,10 @@ data SymbolType
     deriving stock (Eq, Ord, Show, Generic, Data, Lift)
     deriving anyclass (NFData, Hashable)
 
+newtype SyntacticClauses = SyntacticClauses [Word8]
+    deriving stock (Eq, Ord, Read, Show)
+    deriving newtype (NFData)
+
 pattern IsIdem, IsNotIdem :: Flag "isIdem"
 pattern IsIdem = Flag True
 pattern IsNotIdem = Flag False

booster/library/Booster/Definition/Attributes/Reader.hs

@@ -70,6 +70,7 @@ instance HasAttributes ParsedAxiom where
             <*> (attributes .! "preserves-definedness")
             <*> readConcreteness attributes
             <*> (attributes .! "smt-lemma")
+            <*> readSyntacticClauses attributes
       where
         -- Some rewrite rules are dynamically generated and injected into
         -- a running server using the RPC "add-module" endpoint.
@@ -153,6 +154,24 @@ readConcreteness attributes = do
         [name, sort] -> Right (Text.encodeUtf8 name, Text.encodeUtf8 sort)
         _ -> Left "Invalid variable"
 
+{- | Reads 'syntactic' attribute, returning the set of integer indices.
+     Reports an error if any of the integers are non-positive or there are duplicates.
+     Defaults to an empty set.
+-}
+readSyntacticClauses :: ParsedAttributes -> Except Text SyntacticClauses
+readSyntacticClauses attributes = do
+    syntacticClauses <-
+        maybe (pure Nothing) ((Just <$>) . mapM (except . readWord8)) $
+            getAttribute "syntactic" attributes
+    case syntacticClauses of
+        Nothing -> pure $ SyntacticClauses []
+        Just [] -> pure $ SyntacticClauses []
+        Just more -> pure $ SyntacticClauses more
+  where
+    readWord8 str
+        | all isDigit (Text.unpack str) = first Text.pack $ readEither (Text.unpack str)
+        | otherwise = Left $ "invalid syntactic clause" <> (Text.pack $ show str)
+
 instance HasAttributes ParsedSymbol where
     type Attributes ParsedSymbol = SymbolAttributes
 

booster/library/Booster/JsonRpc.hs

@@ -83,7 +83,7 @@ import Booster.Syntax.ParsedKore.Internalise (
     addToDefinitions,
     definitionErrorToRpcError,
  )
-import Booster.Util (Flag (..), constructorName)
+import Booster.Util (Flag (..))
 import Kore.JsonRpc.Error qualified as RpcError
 import Kore.JsonRpc.Server (ErrorObj (..), JsonRpcHandler (..), Respond)
 import Kore.JsonRpc.Types qualified as RpcTypes
@@ -269,7 +269,7 @@ respond stateVar request =
                             (Left (ApplyEquations.EquationLoop _terms), _) ->
                                 pure . Left . RpcError.backendError $ RpcError.Aborted "equation loop detected"
                             (Left other, _) ->
-                                pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
+                                pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . show $ other)
                     -- predicate only
                     Right (Predicates ps)
                         | null ps.boolPredicates && null ps.ceilPredicates && null ps.substitution && null ps.unsupported ->

booster/library/Booster/Pattern/Match.hs

@@ -10,6 +10,7 @@ module Booster.Pattern.Match (
     FailReason (..),
     Substitution,
     matchTerms,
+    matchTermsWithSubst,
     checkSubsort,
     SortError (..),
 ) where
@@ -121,6 +122,10 @@ instance FromModifiersT mods => Pretty (PrettyWithModifiers mods FailReason) whe
 
 type Substitution = Map Variable Term
 
+-- | Specialisation of @matchTermsWithSubst@ to an empty initial substitution
+matchTerms :: MatchType -> KoreDefinition -> Term -> Term -> MatchResult
+matchTerms matchType def = matchTermsWithSubst matchType def mempty
+
 {- | Attempts to find a simple unifying substitution for the given
    terms.
 
@@ -131,8 +136,9 @@ type Substitution = Map Variable Term
    to ensure that we always produce a matching substitution without having to check
    after running the matcher
 -}
-matchTerms :: MatchType -> KoreDefinition -> Term -> Term -> MatchResult
-matchTerms matchType KoreDefinition{sorts} term1 term2 =
+matchTermsWithSubst ::
+    MatchType -> KoreDefinition -> Substitution -> Term -> Term -> MatchResult
+matchTermsWithSubst matchType KoreDefinition{sorts} knownSubst term1 term2 =
     let runMatch :: MatchState -> MatchResult
         runMatch =
             fromEither
@@ -153,7 +159,7 @@ matchTerms matchType KoreDefinition{sorts} term1 term2 =
             else
                 runMatch
                     State
-                        { mSubstitution = Map.empty
+                        { mSubstitution = knownSubst
                         , mQueue = Seq.singleton (term1, term2) -- PriorityQueue.singleton (term1, term2) RegularTerm ()
                         , mMapQueue = mempty
                         , mIndeterminate = []

booster/test/rpc-integration/resources/kompile-from-double-definition.sh

@@ -39,7 +39,7 @@ esac
 llvm-kompile ${NAME}.llvm.kore ./dt c -- \
              -fPIC -std=c++17 -o interpreter \
              $PLUGIN_LIBS $PLUGIN_INCLUDE $PLUGIN_CPP \
-             -lcrypto -lssl $LPROCPS -lsecp256k1
+             -lcrypto -lssl -lsecp256k1 $LPROCPS
 mv interpreter.* ${NAME}.dylib
 
 # remove temporary artefacts