Parse left- and right-assoc

kore/app/share/GlobalMain.hs

@@ -108,6 +108,7 @@ import System.Clock
     , getTime
     )
 import qualified System.Environment as Env
+import qualified Text.Megaparsec as Parser
 
 import Kore.ASTVerifier.DefinitionVerifier
     ( sortModuleClaims
@@ -132,12 +133,9 @@ import Kore.Parser
     ( ParsedPattern
     , parseKoreDefinition
     )
-import Kore.Parser.Lexeme
-    ( moduleNameIdParser
-    )
+import qualified Kore.Parser.Lexer as Lexer
 import Kore.Parser.ParserUtils
-    ( endOfInput
-    , parseOnly
+    ( parseOnly
     )
 import Kore.Step.Strategy
     ( GraphSearchOrder (..)
@@ -184,7 +182,7 @@ parseModuleName metaName longName helpMsg =
 readModuleName :: Options.ReadM ModuleName
 readModuleName = do
     opt <- str
-    case parseOnly (moduleNameIdParser <* endOfInput) "<command-line>" opt of
+    case parseOnly (Lexer.parseModuleName <* Parser.eof) "<command-line>" opt of
         Left err        -> readerError err
         Right something -> pure something
 

kore/package.yaml

@@ -11,8 +11,6 @@ category:            Language
 extra-source-files:
   - README.md
   - CHANGELOG.md
-  - test/resources/*.kore
-  - test/resources/*.kore.golden
 
 data-dir: data
 

kore/src/Kore/AST/Error.hs

@@ -89,7 +89,7 @@ withLocationAndContext location message =
  -}
 withSentenceSymbolContext
     :: MonadError (Error e) error
-    => SentenceSymbol patternType
+    => SentenceSymbol
     -> error a
     -> error a
 withSentenceSymbolContext
@@ -133,7 +133,7 @@ withSentenceClaimContext _ = withContext "claim declaration"
  -}
 withSentenceSortContext
     :: MonadError (Error e) error
-    => SentenceSort patternType
+    => SentenceSort
     -> error a
     -> error a
 withSentenceSortContext SentenceSort { sentenceSortName } =
@@ -144,7 +144,7 @@ withSentenceSortContext SentenceSort { sentenceSortName } =
  -}
 withSentenceHookContext
     :: MonadError (Error e) error
-    => SentenceHook patternType
+    => SentenceHook
     -> error a
     -> error a
 withSentenceHookContext =
@@ -167,7 +167,7 @@ withSentenceHookContext =
 {- | Locate the given import declaration in the error context.
  -}
 withSentenceImportContext
-    :: SentenceImport patternType
+    :: SentenceImport
     -> error a
     -> error a
 withSentenceImportContext _ = id

kore/src/Kore/ASTVerifier/ModuleVerifier.hs

@@ -134,7 +134,7 @@ The named modules are verified and imported into the current 'VerifiedModule'.
 verifyImports :: [ParsedSentence] -> SentenceVerifier ()
 verifyImports = traverse_ verifyImport . mapMaybe projectSentenceImport
 
-verifyImport :: SentenceImport ParsedPattern -> SentenceVerifier ()
+verifyImport :: SentenceImport -> SentenceVerifier ()
 verifyImport sentence =
     withSentenceImportContext sentence $ do
         let SentenceImport { sentenceImportAttributes = attrs0 } = sentence

kore/src/Kore/ASTVerifier/PatternVerifier/PatternVerifier.hs

@@ -275,7 +275,7 @@ withDeclaredVariables declaredVariables' =
 applicationSortsFromSymbolOrAliasSentence
     :: SentenceSymbolOrAlias sentence
     => SymbolOrAlias
-    -> sentence pat
+    -> sentence
     -> PatternVerifier ApplicationSorts
 applicationSortsFromSymbolOrAliasSentence symbolOrAlias sentence = do
     Context { declaredSortVariables } <- Reader.ask

kore/src/Kore/ASTVerifier/SentenceVerifier.hs

@@ -152,7 +152,7 @@ type SentenceVerifier = StateT VerifiedModule' Verifier
 
 {- | Look up a sort declaration.
  -}
-findSort :: Id -> SentenceVerifier (SentenceSort Verified.Pattern)
+findSort :: Id -> SentenceVerifier SentenceSort
 findSort identifier = do
     verifiedModule <- State.get
     findIndexedSort verifiedModule identifier
@@ -197,7 +197,7 @@ verifyHookedSorts =
     traverse_ verifyHookedSortSentence
     . mapMaybe projectSentenceHookedSort
 
-verifyHookedSortSentence :: SentenceSort ParsedPattern -> SentenceVerifier ()
+verifyHookedSortSentence :: SentenceSort -> SentenceVerifier ()
 verifyHookedSortSentence sentence =
     withSentenceHookContext (SentenceHookedSort sentence) $ do
         let SentenceSort { sentenceSortAttributes } = sentence
@@ -224,9 +224,7 @@ verifyHookedSymbols =
     traverse_ verifyHookedSymbolSentence
     . mapMaybe projectSentenceHookedSymbol
 
-verifyHookedSymbolSentence
-    :: SentenceSymbol ParsedPattern
-    -> SentenceVerifier ()
+verifyHookedSymbolSentence :: SentenceSymbol -> SentenceVerifier ()
 verifyHookedSymbolSentence sentence =
     withSentenceHookContext (SentenceHookedSymbol sentence) $ do
         let SentenceSymbol { sentenceSymbolAttributes } = sentence
@@ -262,7 +260,7 @@ verifySymbols = traverse_ verifySymbolSentence . mapMaybe project
         projectSentenceSymbol sentence <|> projectSentenceHookedSymbol sentence
 
 verifySymbolSentence
-    :: SentenceSymbol ParsedPattern
+    :: SentenceSymbol
     -> SentenceVerifier Verified.SentenceSymbol
 verifySymbolSentence sentence =
     withSentenceSymbolContext sentence $ do
@@ -272,15 +270,14 @@ verifySymbolSentence sentence =
         mapM_ (verifySort findSort variables) sorts
         let resultSort = sentenceSymbolResultSort sentence
         verifySort findSort variables resultSort
-        verified <- traverse verifyNoPatterns sentence
         attrs <- parseAttributes' $ sentenceSymbolAttributes sentence
         let isConstructor =
                 Attribute.Symbol.isConstructor
                 . Attribute.Symbol.constructor
                 $ attrs
-        when isConstructor (verifyConstructor verified)
-        State.modify' $ addSymbol verified attrs
-        return verified
+        when isConstructor (verifyConstructor sentence)
+        State.modify' $ addSymbol sentence attrs
+        return sentence
   where
     addSymbol verified attrs =
         Lens.over
@@ -425,15 +422,14 @@ verifySorts = traverse_ verifySortSentence . mapMaybe project
         projectSentenceSort sentence <|> projectSentenceHookedSort sentence
 
 verifySortSentence
-    :: SentenceSort ParsedPattern
+    :: SentenceSort
     -> SentenceVerifier Verified.SentenceSort
 verifySortSentence sentence =
     withSentenceSortContext sentence $ do
         _ <- buildDeclaredSortVariables $ sentenceSortParameters sentence
-        verified <- traverse verifyNoPatterns sentence
-        attrs <- parseAttributes' $ sentenceSortAttributes verified
-        State.modify' $ addSort verified attrs
-        return verified
+        attrs <- parseAttributes' $ sentenceSortAttributes sentence
+        State.modify' $ addSort sentence attrs
+        return sentence
   where
     addSort verified attrs =
         Lens.over

kore/src/Kore/ASTVerifier/SortVerifier.hs

@@ -22,7 +22,7 @@ import Kore.Syntax.Definition
 {-|'verifySort' verifies the welformedness of a Kore 'Sort'. -}
 verifySort
     :: MonadError (Error VerifyError) m
-    => (Id -> m (SentenceSort patternType))
+    => (Id -> m SentenceSort)
     -- ^ Provides a sortMetaSorts description.
     -> Set.Set SortVariable
     -- ^ Sort variables visible here.
@@ -64,10 +64,10 @@ verifySort findSortDescription declaredSortVariables (SortActualSort sort)
 
 verifySortMatchesDeclaration
     :: MonadError (Error VerifyError) m
-    => (Id -> m (SentenceSort patternType))
+    => (Id -> m SentenceSort)
     -> Set.Set SortVariable
     -> SortActual
-    -> SentenceSort patternType'
+    -> SentenceSort
     -> m VerifySuccess
 verifySortMatchesDeclaration
     findSortDescription declaredSortVariables sort sortDescription

kore/src/Kore/Builtin/Verifiers.hs

@@ -124,8 +124,7 @@ type SortDeclVerifier =
 newtype SortVerifier =
     SortVerifier
         { runSortVerifier
-            :: forall patternType
-            .  (Id -> Either (Error VerifyError) (SentenceSort patternType))
+            :: (Id -> Either (Error VerifyError) SentenceSort)
             -> Sort
             -> Either (Error VerifyError) ()
         }
@@ -136,8 +135,7 @@ type SortDeclVerifiers = HashMap Text SortDeclVerifier
 newtype SymbolVerifier =
     SymbolVerifier
         { runSymbolVerifier
-            :: forall patternType
-            .  (Id -> Either (Error VerifyError) (SentenceSort patternType))
+            :: (Id -> Either (Error VerifyError) SentenceSort)
             -> ParsedSentenceSymbol
             -> Either (Error VerifyError) ()
         }
@@ -435,8 +433,7 @@ verifySort builtinName =
     SortVerifier worker
   where
     worker
-        :: forall patternType
-        .  (Id -> Either (Error VerifyError) (SentenceSort patternType))
+        :: (Id -> Either (Error VerifyError) SentenceSort)
         -> Sort
         -> Either (Error VerifyError) ()
     worker findSort (SortActualSort SortActual { sortActualName }) = do
@@ -457,8 +454,7 @@ verifySortHasDomainValues :: SortVerifier
 verifySortHasDomainValues = SortVerifier worker
   where
     worker
-        :: forall patternType
-        .  (Id -> Either (Error VerifyError) (SentenceSort patternType))
+        :: (Id -> Either (Error VerifyError) SentenceSort)
         -> Sort
         -> Either (Error VerifyError) ()
     worker findSort (SortActualSort SortActual { sortActualName }) = do

kore/src/Kore/IndexedModule/IndexedModule.hs

@@ -96,7 +96,7 @@ import Kore.Syntax
 import Kore.Syntax.Definition
 import qualified Kore.Verified as Verified
 
-type SortDescription = SentenceSort (Pattern VariableName Attribute.Null)
+type SortDescription = SentenceSort
 
 data IndexModuleError
 
@@ -121,9 +121,9 @@ data IndexedModule pat declAtts axiomAtts =
     , indexedModuleAliasSentences
         :: !(Map.Map Id (declAtts, SentenceAlias pat))
     , indexedModuleSymbolSentences
-        :: !(Map.Map Id (declAtts, SentenceSymbol pat))
+        :: !(Map.Map Id (declAtts, SentenceSymbol))
     , indexedModuleSortDescriptions
-        :: !(Map.Map Id (Attribute.Sort, SentenceSort pat))
+        :: !(Map.Map Id (Attribute.Sort, SentenceSort))
     , indexedModuleAxioms :: ![(axiomAtts, SentenceAxiom pat)]
     , indexedModuleClaims :: ![(axiomAtts, SentenceClaim pat)]
     , indexedModuleAttributes :: !(declAtts, Attributes)
@@ -150,14 +150,14 @@ data IndexedModule pat declAtts axiomAtts =
 recursiveIndexedModuleSortDescriptions
     :: forall pat declAtts axiomAtts
     .  IndexedModule pat declAtts axiomAtts
-    -> Map.Map Id (Attribute.Sort, SentenceSort pat)
+    -> Map.Map Id (Attribute.Sort, SentenceSort)
 recursiveIndexedModuleSortDescriptions =
     recursiveIndexedModuleStuff indexedModuleSortDescriptions
 
 recursiveIndexedModuleSymbolSentences
     :: forall pat axiomAtts
     .  IndexedModule pat Attribute.Symbol axiomAtts
-    -> Map.Map Id (Attribute.Symbol, SentenceSymbol pat)
+    -> Map.Map Id (Attribute.Symbol, SentenceSymbol)
 recursiveIndexedModuleSymbolSentences =
     recursiveIndexedModuleStuff indexedModuleSymbolSentences
 
@@ -273,12 +273,6 @@ erasePatterns indexedModule =
         { indexedModuleAliasSentences =
             Lens.set (Lens.mapped . Lens._2 . Lens.mapped) ()
             $ indexedModuleAliasSentences indexedModule
-        , indexedModuleSymbolSentences =
-            Lens.set (Lens.mapped . Lens._2 . Lens.mapped) ()
-            $ indexedModuleSymbolSentences indexedModule
-        , indexedModuleSortDescriptions =
-            Lens.set (Lens.mapped . Lens._2 . Lens.mapped) ()
-            $ indexedModuleSortDescriptions indexedModule
         , indexedModuleAxioms = []
         , indexedModuleClaims = []
         , indexedModuleImports =
@@ -294,10 +288,6 @@ mapPatterns mapping indexedModule =
     indexedModule
         { indexedModuleAliasSentences =
             (fmap . fmap . fmap) mapping indexedModuleAliasSentences
-        , indexedModuleSymbolSentences =
-            (fmap . fmap . fmap) mapping indexedModuleSymbolSentences
-        , indexedModuleSortDescriptions =
-            (fmap . fmap . fmap) mapping indexedModuleSortDescriptions
         , indexedModuleAxioms =
             (fmap . fmap . fmap) mapping indexedModuleAxioms
         , indexedModuleClaims =
@@ -308,8 +298,6 @@ mapPatterns mapping indexedModule =
         }
   where
     IndexedModule { indexedModuleAliasSentences } = indexedModule
-    IndexedModule { indexedModuleSymbolSentences } = indexedModule
-    IndexedModule { indexedModuleSortDescriptions } = indexedModule
     IndexedModule { indexedModuleAxioms } = indexedModule
     IndexedModule { indexedModuleClaims } = indexedModule
     IndexedModule { indexedModuleImports } = indexedModule
@@ -461,7 +449,7 @@ indexedModuleWithDefaultImports name defaultImport =
  -}
 hookedObjectSymbolSentences
     :: IndexedModule pat declAtts axiomAtts
-    -> Map.Map Id (declAtts, SentenceSymbol pat)
+    -> Map.Map Id (declAtts, SentenceSymbol)
 hookedObjectSymbolSentences
     IndexedModule
         { indexedModuleSymbolSentences

kore/src/Kore/IndexedModule/Resolvers.hs

@@ -78,7 +78,7 @@ import qualified Kore.Syntax.Definition as Syntax
 
 symbolSentencesMap
     :: IndexedModule patternType declAtts axiomAtts
-    -> Map.Map Id (declAtts, SentenceSymbol patternType)
+    -> Map.Map Id (declAtts, SentenceSymbol)
 symbolSentencesMap = indexedModuleSymbolSentences
 
 aliasSentencesMap
@@ -88,7 +88,7 @@ aliasSentencesMap = indexedModuleAliasSentences
 
 sortSentencesMap
     :: IndexedModule patternType declAtts axiomAtts
-    -> Map.Map Id (Attribute.Sort, SentenceSort patternType)
+    -> Map.Map Id (Attribute.Sort, SentenceSort)
 sortSentencesMap = indexedModuleSortDescriptions
 
 -- |Given a KoreIndexedModule and a head, it looks up the 'SentenceSymbol' or
@@ -104,7 +104,7 @@ getHeadApplicationSorts m patternHead =
   where
     sentenceSorts
         :: SentenceSymbolOrAlias sentence
-        => [Sort] -> sentence pat -> ApplicationSorts
+        => [Sort] -> sentence -> ApplicationSorts
     sentenceSorts sortParameters sentence =
         assertRight $ symbolOrAliasSorts sortParameters sentence
 
@@ -191,7 +191,7 @@ resolveSymbol
     :: MonadError (Error e) m
     => IndexedModule patternType declAtts axiomAtts
     -> Id
-    -> m (declAtts, SentenceSymbol patternType)
+    -> m (declAtts, SentenceSymbol)
 resolveSymbol m headId =
     case resolveThing symbolSentencesMap m headId of
         Nothing ->
@@ -245,7 +245,7 @@ resolveSort
     :: MonadError (Error e) m
     => IndexedModule patternType declAtts axiomAtts
     -> Id
-    -> m (Attribute.Sort, SentenceSort patternType)
+    -> m (Attribute.Sort, SentenceSort)
 resolveSort m sortId =
     case resolveThing sortSentencesMap m sortId of
         Nothing ->
@@ -318,7 +318,7 @@ findIndexedSort
     -- ^ indexed module
     -> Id
     -- ^ sort identifier
-    -> error (SentenceSort patternType)
+    -> error SentenceSort
 findIndexedSort indexedModule sort =
     fmap getIndexedSentence (resolveSort indexedModule sort)
 
@@ -331,7 +331,7 @@ findIndexedSort indexedModule sort =
 applyToHeadSentence
     :: (forall sentence.  SentenceSymbolOrAlias sentence
        => [Sort]
-       -> sentence pat
+       -> sentence
        -> result)
     -> IndexedModule pat declAtts axiomAtts
     -> SymbolOrAlias
@@ -343,7 +343,7 @@ applyToResolution
     :: HasCallStack
     => (forall sentence.  SentenceSymbolOrAlias sentence
         => [Sort]
-        -> (declAtts, sentence pat)
+        -> (declAtts, sentence)
         -> result)
     -> IndexedModule pat declAtts axiomAtts
     -> SymbolOrAlias

kore/src/Kore/Internal/ApplicationSorts.hs

@@ -48,7 +48,7 @@ pattern from the given sort parameters.
 symbolOrAliasSorts
     :: (SentenceSymbolOrAlias sentence, MonadError (Error e) m)
     => [Sort]
-    -> sentence pat
+    -> sentence
     -> m ApplicationSorts
 symbolOrAliasSorts params sentence = do
     variableToSort <-