Remove SymbolOrAliasSorts

src/main/haskell/kore/app/exec/Main.hs

@@ -13,8 +13,6 @@ import           Data.Maybe
                  ( fromMaybe )
 import           Data.Proxy
                  ( Proxy (..) )
-import           Data.Reflection
-                 ( give )
 import           Data.Semigroup
                  ( (<>) )
 import qualified Data.Set as Set
@@ -35,13 +33,12 @@ import           System.IO
 import           Data.Limit
                  ( Limit (..) )
 import           Kore.AST.Kore
-                 ( CommonKorePattern )
+                 ( CommonKorePattern, VerifiedKorePattern )
 import           Kore.AST.Pure
 import           Kore.AST.PureToKore
                  ( patternKoreToPure )
 import           Kore.AST.Sentence
-import qualified Kore.ASTUtils.SmartConstructors as Pattern
-import           Kore.ASTUtils.SmartPatterns
+import           Kore.AST.Valid
 import           Kore.ASTVerifier.DefinitionVerifier
                  ( AttributesVerification (DoNotVerifyAttributes),
                  defaultAttributesVerification,
@@ -52,8 +49,6 @@ import           Kore.Error
 import           Kore.Exec
 import           Kore.IndexedModule.IndexedModule
                  ( IndexedModule (..), VerifiedModule )
-import           Kore.IndexedModule.MetadataTools
-                 ( MetadataTools (..), extractMetadataTools )
 import           Kore.Parser.Parser
                  ( fromKore, fromKorePattern )
 import           Kore.Predicate.Predicate
@@ -341,7 +336,7 @@ externalizeFreshVars pat = Recursive.fold renameFreshLocal pat
         -> CommonStepPattern level
     renameFreshLocal (_ :< VariablePattern v@(Variable {variableName}))
       | name `Set.member` freshVarsIds =
-        Var_ v {
+        mkVar v {
             variableName = variableName
                 { getId =
                     freshPrefix <> Text.filter (/= '_') name
@@ -451,7 +446,7 @@ mainWithOptions
                 Just specIndexedModule ->
                     either
                         (\pat -> (ExitFailure 1, pat))
-                        (\_ -> (ExitSuccess, Pattern.mkTop))
+                        (\_ -> (ExitSuccess, mkTop $ mkSortVariable "R" ))
                     <$> prove
                             stepLimit
                             indexedModule
@@ -502,30 +497,23 @@ mainPatternParseAndVerify
     :: VerifiedModule StepperAttributes
     -> String
     -> IO (CommonStepPattern Object)
-mainPatternParseAndVerify indexedModule patternFileName
-  = do
+mainPatternParseAndVerify indexedModule patternFileName = do
     parsedPattern <- mainPatternParse patternFileName
-    mainPatternVerify indexedModule parsedPattern
-    return (makePurePattern parsedPattern)
+    makePurePattern <$> mainPatternVerify indexedModule parsedPattern
 
 mainParseSearchPattern
     :: VerifiedModule StepperAttributes
     -> String
     -> IO (CommonExpandedPattern Object)
-mainParseSearchPattern indexedModule patternFileName
-  = do
-    let
-        metadataTools :: MetadataTools Object StepperAttributes
-        metadataTools = extractMetadataTools indexedModule
-        MetadataTools { symbolOrAliasSorts } = metadataTools
+mainParseSearchPattern indexedModule patternFileName = do
     purePattern <- mainPatternParseAndVerify indexedModule patternFileName
     case purePattern of
         And_ _ term predicateTerm -> return
             Predicated
                 { term
                 , predicate =
                     either (error . printError) id
-                        (give symbolOrAliasSorts makePredicate predicateTerm)
+                        (makePredicate predicateTerm)
                 , substitution = mempty
                 }
         _ -> error "Unexpected non-conjunctive pattern"
@@ -581,7 +569,7 @@ verifyDefinitionWithBase maybeBaseModule willChkAttr definition =
         Right indexedDefinition -> return indexedDefinition
 
 makePurePattern
-    :: CommonKorePattern
+    :: VerifiedKorePattern
     -> CommonStepPattern Object
 makePurePattern pat =
     case patternKoreToPure Object pat of

src/main/haskell/kore/app/parser/Main.hs

@@ -121,7 +121,8 @@ main = do
             when willVerify $ do
                 indexedModule <-
                     mainModule (ModuleName mainModuleName) indexedModules
-                mainPatternVerify indexedModule parsedPattern
+                _ <- mainPatternVerify indexedModule parsedPattern
+                return ()
             when willPrintPattern $
                 putStrLn (prettyPrintToString parsedPattern)
 

src/main/haskell/kore/app/share/GlobalMain.hs

@@ -178,15 +178,12 @@ mainPatternVerify
     :: VerifiedModule attrs
     -- ^ Module containing definitions visible in the pattern
     -> CommonKorePattern -- ^ Parsed pattern to check well-formedness
-    -> IO ()
-mainPatternVerify verifiedModule patt =
-    do
-      verifyResult <-
+    -> IO VerifiedKorePattern
+mainPatternVerify verifiedModule patt = do
+    verifyResult <-
         clockSomething "Verifying the pattern"
             (runPatternVerifier context $ verifyStandalonePattern Nothing patt)
-      case verifyResult of
-        Left err1 -> error (printError err1)
-        Right _   -> return ()
+    either (error . printError) return verifyResult
   where
     Builtin.Verifiers { patternVerifier } = Builtin.koreVerifiers
     indexedModule =

src/main/haskell/kore/bench/exec/Main.hs

@@ -8,7 +8,9 @@ import           Data.Function
 import           Data.Limit
                  ( Limit (Unlimited) )
 import qualified Data.Map as Map
+import qualified Data.Set as Set
 
+import qualified Kore.AST.Kore as Kore
 import           Kore.AST.Pure
 import           Kore.AST.PureToKore
                  ( patternKoreToPure )
@@ -17,12 +19,15 @@ import           Kore.AST.Sentence
 import           Kore.ASTVerifier.DefinitionVerifier
                  ( AttributesVerification (DoNotVerifyAttributes),
                  verifyAndIndexDefinition )
+import qualified Kore.ASTVerifier.PatternVerifier as PatternVerifier
+import qualified Kore.Attribute.Null as Attribute
 import qualified Kore.Builtin as Builtin
 import           Kore.Error
                  ( printError )
 import           Kore.Exec
 import           Kore.IndexedModule.IndexedModule
-                 ( IndexedModule (..), VerifiedModule )
+                 ( IndexedModule (..), VerifiedModule,
+                 mapIndexedModulePatterns )
 import           Kore.Parser.Parser
                  ( fromKore, fromKorePattern )
 import           Kore.Step.Pattern
@@ -125,6 +130,7 @@ execBenchmark root kFile definitionFile mainModuleName test =
     envWithCleanup setUp cleanUp $ bench name . nfIO . execution
   where
     name = takeFileName test
+    setUp :: IO (VerifiedModule StepperAttributes, CommonStepPattern Object)
     setUp = do
         kompile
         definition <- readFile $ root </> definitionFile
@@ -139,12 +145,30 @@ execBenchmark root kFile definitionFile mainModuleName test =
             Just verifiedModule =
                 fmap constructorFunctions
                     $ Map.lookup mainModuleName verifiedModules
+            indexedModule =
+                mapIndexedModulePatterns
+                    Kore.eraseAnnotations
+                    verifiedModule
         pat <- parseProgram
         let
             parsedPattern = either error id $ fromKorePattern "" pat
+            verifiedPattern =
+                either (error . printError) id
+                $ PatternVerifier.runPatternVerifier context
+                $ PatternVerifier.verifyStandalonePattern Nothing parsedPattern
+              where
+                context =
+                    PatternVerifier.Context
+                        { builtinPatternVerifier =
+                            Builtin.patternVerifier Builtin.koreVerifiers
+                        , indexedModule = Attribute.Null <$ indexedModule
+                        , declaredSortVariables = Set.empty
+                        , declaredVariables =
+                            PatternVerifier.emptyDeclaredVariables
+                        }
             purePattern =
                 either (error . printError) id
-                    $ patternKoreToPure Object parsedPattern
+                $ patternKoreToPure Object verifiedPattern
         return (verifiedModule, purePattern)
     execution
         :: (VerifiedModule StepperAttributes, CommonStepPattern Object)

src/main/haskell/kore/src/Kore/AST/Builders.hs

@@ -16,7 +16,6 @@ module Kore.AST.Builders
     , bottom_ -- TODO: not used yet
     , ceilS_ -- TODO: not used yet
     , ceil_ -- TODO: not used yet
-    , parameterizedDomainValue_
     , equalsAxiom_
     , equalsS_
     , equals_
@@ -45,6 +44,7 @@ module Kore.AST.Builders
 
 import           Control.Comonad.Trans.Cofree
                  ( CofreeF (..) )
+import           Data.Functor.Classes
 import           Data.Proxy
                  ( Proxy (..) )
 import           Data.Text
@@ -56,7 +56,6 @@ import           Kore.AST.BuildersImpl
 import           Kore.AST.Pure
 import           Kore.AST.Sentence
 import           Kore.ASTHelpers
-import qualified Kore.Domain.Builtin as Domain
 import           Kore.Error
 
 {-|'sortParameter' defines a sort parameter that can be used in declarations.
@@ -78,6 +77,7 @@ applyPS
     ::  ( Functor domain
         , SentenceSymbolOrAlias s
         , Show level
+        , Show1 domain
         , Show (Pattern level domain Variable child)
         , child ~ CommonPurePattern level domain
         )
@@ -113,6 +113,7 @@ applyS
     ::  ( Functor domain
         , SentenceSymbolOrAlias s
         , Show level
+        , Show1 domain
         , Show (Pattern level domain Variable child)
         , child ~ CommonPurePattern level domain
         )
@@ -202,7 +203,7 @@ alias_
     -> Sort level
     -> [Variable level]
     -- ^ The left-hand side of the alias: the alias applied to these variables
-    -> CommonPurePattern level domain
+    -> PurePattern level domain Variable (Annotation.Null level)
     -- ^ The right-hand side of the alias
     -> PureSentenceAlias level domain
 alias_ name location = parameterizedAlias_ name location []
@@ -217,7 +218,7 @@ parameterizedAlias_
     -> Sort level
     -> [Variable level]
     -- ^ The left-hand side of the alias: the alias applied to these variables
-    -> CommonPurePattern level domain
+    -> PurePattern level domain Variable (Annotation.Null level)
     -- ^ The right-hand side of the alias
     -> PureSentenceAlias level domain
 parameterizedAlias_
@@ -270,6 +271,7 @@ equalsS_
     ::  ( Functor domain
         , MetaOrObject level
         , Show (CommonPurePattern level domain)
+        , Show1 domain
         )
     => Sort level
     -> CommonPurePatternStub level domain
@@ -283,6 +285,7 @@ equals_
     ::  ( Functor domain
         , MetaOrObject level
         , Show (CommonPurePattern level domain)
+        , Show1 domain
         )
     => CommonPurePatternStub level domain
     -> CommonPurePatternStub level domain
@@ -295,6 +298,7 @@ inS_
     ::  ( Functor domain
         , MetaOrObject level
         , Show (CommonPurePattern level domain)
+        , Show1 domain
         )
     => Sort level
     -> CommonPurePatternStub level domain
@@ -308,6 +312,7 @@ in_
     ::  ( Functor domain
         , MetaOrObject level
         , Show (CommonPurePattern level domain)
+        , Show1 domain
         )
     => CommonPurePatternStub level domain
     -> CommonPurePatternStub level domain
@@ -322,6 +327,7 @@ ceilS_
         , child ~ CommonPurePattern level domain
         , Show child
         , Show (Pattern level domain Variable child)
+        , Show1 domain
         )
     => Sort level
     -> CommonPurePatternStub level domain
@@ -336,6 +342,7 @@ ceil_
         , child ~ CommonPurePattern level domain
         , Show child
         , Show (Pattern level domain Variable child)
+        , Show1 domain
         )
     => CommonPurePatternStub level domain
     -> CommonPurePatternStub level domain
@@ -349,6 +356,7 @@ floorS_
         , child ~ CommonPurePattern level domain
         , Show child
         , Show (Pattern level domain Variable child)
+        , Show1 domain
         )
     => Sort level
     -> CommonPurePatternStub level domain
@@ -363,6 +371,7 @@ floor_
         , child ~ CommonPurePattern level domain
         , Show child
         , Show (Pattern level domain Variable child)
+        , Show1 domain
         )
     => CommonPurePatternStub level domain
     -> CommonPurePatternStub level domain
@@ -500,25 +509,6 @@ next_ =
                 }
         )
 
--- |Builds a 'PatternStub' representing 'DomainValue' given a 'Sort' and
--- a'String' for its operand.
-parameterizedDomainValue_
-    :: Sort Object
-    -> String
-    -> CommonPurePatternStub Object Domain.Builtin
-parameterizedDomainValue_ sort str =
-    SortedPatternStub
-        SortedPattern
-        { sortedPatternSort = sort
-        , sortedPatternPattern =
-            DomainValuePattern DomainValue
-                { domainValueSort = sort
-                , domainValueChild =
-                    (Domain.BuiltinPattern . asPurePattern . (mempty :<))
-                        (StringLiteralPattern $ StringLiteral str)
-                }
-        }
-
 -- |Builds a 'PatternStub' representing 'Rewrites' given 'PatternStub's for its
 -- operands.
 rewrites_
@@ -546,6 +536,7 @@ parameterizedAxiom_
         , child ~ CommonPurePattern level domain
         , Show child
         , Show (Pattern level domain Variable child)
+        , Show1 domain
         )
     => [SortVariable level]
     -> CommonPurePatternStub level domain
@@ -564,9 +555,10 @@ parameterizedAxiom_
     SentenceAxiom
         { sentenceAxiomParameters = parameters
         , sentenceAxiomPattern =
-            quantifyFreeVariables s (asPurePattern $ Annotation.Null :< p)
+            quantifyFreeVariables s (asPurePattern $ mempty :< p)
         , sentenceAxiomAttributes = Attributes []
         }
+
 {-|Creates an axiom with no sort parameters from a pattern.
 -}
 axiom_
@@ -575,6 +567,7 @@ axiom_
         , MetaOrObject level
         , child ~ CommonPurePattern level domain
         , Show child
+        , Show1 domain
         , Show (Pattern level domain Variable child)
         )
     => CommonPurePatternStub level domain
@@ -594,6 +587,7 @@ parameterizedEqualsAxiom_
         , MetaOrObject level
         , child ~ CommonPurePattern level domain
         , Show child
+        , Show1 domain
         , Show (Pattern level domain Variable child)
         )
     => [SortVariable level]
@@ -618,6 +612,7 @@ equalsAxiom_
         , MetaOrObject level
         , child ~ CommonPurePattern level domain
         , Show child
+        , Show1 domain
         , Show (Pattern level domain Variable child)
         )
     => SortVariable level