Parse and internalise the syntactic attribute

Fix unit tests

Author: geo2a

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,33 @@ 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)
+
+-- where
+--   readWord8 str =
+--     readT [] = Right 50 -- HACK to accept `simplification()` from internal modules
+--     readT [n]
+--         | Text.null n = Right 50 -- HACK to accept `simplification("")`
+--         | all isDigit (Text.unpack n) = Priority <$> readEither (Text.unpack n)
+--         | otherwise = Left $ "invalid priority value " <> show n
+--     readT ns = Left $ "invalid priority value " <> show ns
+
 instance HasAttributes ParsedSymbol where
     type Attributes ParsedSymbol = SymbolAttributes
 

booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs

@@ -374,6 +374,7 @@ equation ruleLabel lhs rhs priority =
                 , concreteness = Unconstrained
                 , uniqueId = mockUniqueId
                 , smtLemma = Flag False
+                , syntacticClauses = SyntacticClauses []
                 }
         , computedAttributes = ComputedAxiomAttributes False []
         , existentials = mempty

booster/unit-tests/Test/Booster/Pattern/Rewrite.hs

@@ -133,6 +133,7 @@ rule ruleLabel lhs rhs priority =
                 , concreteness = Unconstrained
                 , uniqueId = mockUniqueId
                 , smtLemma = Flag False
+                , syntacticClauses = SyntacticClauses []
                 }
         , computedAttributes = ComputedAxiomAttributes False []
         , existentials = mempty