Skip to content

Commit 7579c77

Browse files
ttuegelttuegel
authored
Parse left- and right-assoc (#2252)
1 parent b1de2cf commit 7579c77

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

46 files changed

+1599
-1640
lines changed

‎kore/app/share/GlobalMain.hs

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -108,6 +108,7 @@ import System.Clock
108108
, getTime
109109
)
110110
import qualified System.Environment as Env
111+
import qualified Text.Megaparsec as Parser
111112

112113
import Kore.ASTVerifier.DefinitionVerifier
113114
( sortModuleClaims
@@ -132,12 +133,9 @@ import Kore.Parser
132133
( ParsedPattern
133134
, parseKoreDefinition
134135
)
135-
import Kore.Parser.Lexeme
136-
( moduleNameIdParser
137-
)
136+
import qualified Kore.Parser.Lexer as Lexer
138137
import Kore.Parser.ParserUtils
139-
( endOfInput
140-
, parseOnly
138+
( parseOnly
141139
)
142140
import Kore.Step.Strategy
143141
( GraphSearchOrder (..)
@@ -184,7 +182,7 @@ parseModuleName metaName longName helpMsg =
184182
readModuleName :: Options.ReadM ModuleName
185183
readModuleName = do
186184
opt <- str
187-
case parseOnly (moduleNameIdParser <* endOfInput) "<command-line>" opt of
185+
case parseOnly (Lexer.parseModuleName <* Parser.eof) "<command-line>" opt of
188186
Left err -> readerError err
189187
Right something -> pure something
190188

‎kore/package.yaml

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,6 @@ category: Language
1111
extra-source-files:
1212
- README.md
1313
- CHANGELOG.md
14-
- test/resources/*.kore
15-
- test/resources/*.kore.golden
1614

1715
data-dir: data
1816

‎kore/src/Kore/AST/Error.hs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -89,7 +89,7 @@ withLocationAndContext location message =
8989
-}
9090
withSentenceSymbolContext
9191
:: MonadError (Error e) error
92-
=> SentenceSymbol patternType
92+
=> SentenceSymbol
9393
-> error a
9494
-> error a
9595
withSentenceSymbolContext
@@ -133,7 +133,7 @@ withSentenceClaimContext _ = withContext "claim declaration"
133133
-}
134134
withSentenceSortContext
135135
:: MonadError (Error e) error
136-
=> SentenceSort patternType
136+
=> SentenceSort
137137
-> error a
138138
-> error a
139139
withSentenceSortContext SentenceSort { sentenceSortName } =
@@ -144,7 +144,7 @@ withSentenceSortContext SentenceSort { sentenceSortName } =
144144
-}
145145
withSentenceHookContext
146146
:: MonadError (Error e) error
147-
=> SentenceHook patternType
147+
=> SentenceHook
148148
-> error a
149149
-> error a
150150
withSentenceHookContext =
@@ -167,7 +167,7 @@ withSentenceHookContext =
167167
{- | Locate the given import declaration in the error context.
168168
-}
169169
withSentenceImportContext
170-
:: SentenceImport patternType
170+
:: SentenceImport
171171
-> error a
172172
-> error a
173173
withSentenceImportContext _ = id

‎kore/src/Kore/ASTVerifier/ModuleVerifier.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -134,7 +134,7 @@ The named modules are verified and imported into the current 'VerifiedModule'.
134134
verifyImports :: [ParsedSentence] -> SentenceVerifier ()
135135
verifyImports = traverse_ verifyImport . mapMaybe projectSentenceImport
136136

137-
verifyImport :: SentenceImport ParsedPattern -> SentenceVerifier ()
137+
verifyImport :: SentenceImport -> SentenceVerifier ()
138138
verifyImport sentence =
139139
withSentenceImportContext sentence $ do
140140
let SentenceImport { sentenceImportAttributes = attrs0 } = sentence

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -275,7 +275,7 @@ withDeclaredVariables declaredVariables' =
275275
applicationSortsFromSymbolOrAliasSentence
276276
:: SentenceSymbolOrAlias sentence
277277
=> SymbolOrAlias
278-
-> sentence pat
278+
-> sentence
279279
-> PatternVerifier ApplicationSorts
280280
applicationSortsFromSymbolOrAliasSentence symbolOrAlias sentence = do
281281
Context { declaredSortVariables } <- Reader.ask

‎kore/src/Kore/ASTVerifier/SentenceVerifier.hs

Lines changed: 11 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -152,7 +152,7 @@ type SentenceVerifier = StateT VerifiedModule' Verifier
152152

153153
{- | Look up a sort declaration.
154154
-}
155-
findSort :: Id -> SentenceVerifier (SentenceSort Verified.Pattern)
155+
findSort :: Id -> SentenceVerifier SentenceSort
156156
findSort identifier = do
157157
verifiedModule <- State.get
158158
findIndexedSort verifiedModule identifier
@@ -197,7 +197,7 @@ verifyHookedSorts =
197197
traverse_ verifyHookedSortSentence
198198
. mapMaybe projectSentenceHookedSort
199199

200-
verifyHookedSortSentence :: SentenceSort ParsedPattern -> SentenceVerifier ()
200+
verifyHookedSortSentence :: SentenceSort -> SentenceVerifier ()
201201
verifyHookedSortSentence sentence =
202202
withSentenceHookContext (SentenceHookedSort sentence) $ do
203203
let SentenceSort { sentenceSortAttributes } = sentence
@@ -224,9 +224,7 @@ verifyHookedSymbols =
224224
traverse_ verifyHookedSymbolSentence
225225
. mapMaybe projectSentenceHookedSymbol
226226

227-
verifyHookedSymbolSentence
228-
:: SentenceSymbol ParsedPattern
229-
-> SentenceVerifier ()
227+
verifyHookedSymbolSentence :: SentenceSymbol -> SentenceVerifier ()
230228
verifyHookedSymbolSentence sentence =
231229
withSentenceHookContext (SentenceHookedSymbol sentence) $ do
232230
let SentenceSymbol { sentenceSymbolAttributes } = sentence
@@ -262,7 +260,7 @@ verifySymbols = traverse_ verifySymbolSentence . mapMaybe project
262260
projectSentenceSymbol sentence <|> projectSentenceHookedSymbol sentence
263261

264262
verifySymbolSentence
265-
:: SentenceSymbol ParsedPattern
263+
:: SentenceSymbol
266264
-> SentenceVerifier Verified.SentenceSymbol
267265
verifySymbolSentence sentence =
268266
withSentenceSymbolContext sentence $ do
@@ -272,15 +270,14 @@ verifySymbolSentence sentence =
272270
mapM_ (verifySort findSort variables) sorts
273271
let resultSort = sentenceSymbolResultSort sentence
274272
verifySort findSort variables resultSort
275-
verified <- traverse verifyNoPatterns sentence
276273
attrs <- parseAttributes' $ sentenceSymbolAttributes sentence
277274
let isConstructor =
278275
Attribute.Symbol.isConstructor
279276
. Attribute.Symbol.constructor
280277
$ attrs
281-
when isConstructor (verifyConstructor verified)
282-
State.modify' $ addSymbol verified attrs
283-
return verified
278+
when isConstructor (verifyConstructor sentence)
279+
State.modify' $ addSymbol sentence attrs
280+
return sentence
284281
where
285282
addSymbol verified attrs =
286283
Lens.over
@@ -425,15 +422,14 @@ verifySorts = traverse_ verifySortSentence . mapMaybe project
425422
projectSentenceSort sentence <|> projectSentenceHookedSort sentence
426423

427424
verifySortSentence
428-
:: SentenceSort ParsedPattern
425+
:: SentenceSort
429426
-> SentenceVerifier Verified.SentenceSort
430427
verifySortSentence sentence =
431428
withSentenceSortContext sentence $ do
432429
_ <- buildDeclaredSortVariables $ sentenceSortParameters sentence
433-
verified <- traverse verifyNoPatterns sentence
434-
attrs <- parseAttributes' $ sentenceSortAttributes verified
435-
State.modify' $ addSort verified attrs
436-
return verified
430+
attrs <- parseAttributes' $ sentenceSortAttributes sentence
431+
State.modify' $ addSort sentence attrs
432+
return sentence
437433
where
438434
addSort verified attrs =
439435
Lens.over

‎kore/src/Kore/ASTVerifier/SortVerifier.hs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ import Kore.Syntax.Definition
2222
{-|'verifySort' verifies the welformedness of a Kore 'Sort'. -}
2323
verifySort
2424
:: MonadError (Error VerifyError) m
25-
=> (Id -> m (SentenceSort patternType))
25+
=> (Id -> m SentenceSort)
2626
-- ^ Provides a sortMetaSorts description.
2727
-> Set.Set SortVariable
2828
-- ^ Sort variables visible here.
@@ -64,10 +64,10 @@ verifySort findSortDescription declaredSortVariables (SortActualSort sort)
6464

6565
verifySortMatchesDeclaration
6666
:: MonadError (Error VerifyError) m
67-
=> (Id -> m (SentenceSort patternType))
67+
=> (Id -> m SentenceSort)
6868
-> Set.Set SortVariable
6969
-> SortActual
70-
-> SentenceSort patternType'
70+
-> SentenceSort
7171
-> m VerifySuccess
7272
verifySortMatchesDeclaration
7373
findSortDescription declaredSortVariables sort sortDescription

‎kore/src/Kore/Builtin/Verifiers.hs

Lines changed: 4 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -124,8 +124,7 @@ type SortDeclVerifier =
124124
newtype SortVerifier =
125125
SortVerifier
126126
{ runSortVerifier
127-
:: forall patternType
128-
. (Id -> Either (Error VerifyError) (SentenceSort patternType))
127+
:: (Id -> Either (Error VerifyError) SentenceSort)
129128
-> Sort
130129
-> Either (Error VerifyError) ()
131130
}
@@ -136,8 +135,7 @@ type SortDeclVerifiers = HashMap Text SortDeclVerifier
136135
newtype SymbolVerifier =
137136
SymbolVerifier
138137
{ runSymbolVerifier
139-
:: forall patternType
140-
. (Id -> Either (Error VerifyError) (SentenceSort patternType))
138+
:: (Id -> Either (Error VerifyError) SentenceSort)
141139
-> ParsedSentenceSymbol
142140
-> Either (Error VerifyError) ()
143141
}
@@ -435,8 +433,7 @@ verifySort builtinName =
435433
SortVerifier worker
436434
where
437435
worker
438-
:: forall patternType
439-
. (Id -> Either (Error VerifyError) (SentenceSort patternType))
436+
:: (Id -> Either (Error VerifyError) SentenceSort)
440437
-> Sort
441438
-> Either (Error VerifyError) ()
442439
worker findSort (SortActualSort SortActual { sortActualName }) = do
@@ -457,8 +454,7 @@ verifySortHasDomainValues :: SortVerifier
457454
verifySortHasDomainValues = SortVerifier worker
458455
where
459456
worker
460-
:: forall patternType
461-
. (Id -> Either (Error VerifyError) (SentenceSort patternType))
457+
:: (Id -> Either (Error VerifyError) SentenceSort)
462458
-> Sort
463459
-> Either (Error VerifyError) ()
464460
worker findSort (SortActualSort SortActual { sortActualName }) = do

‎kore/src/Kore/IndexedModule/IndexedModule.hs

Lines changed: 6 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,7 @@ import Kore.Syntax
9696
import Kore.Syntax.Definition
9797
import qualified Kore.Verified as Verified
9898

99-
type SortDescription = SentenceSort (Pattern VariableName Attribute.Null)
99+
type SortDescription = SentenceSort
100100

101101
data IndexModuleError
102102

@@ -121,9 +121,9 @@ data IndexedModule pat declAtts axiomAtts =
121121
, indexedModuleAliasSentences
122122
:: !(Map.Map Id (declAtts, SentenceAlias pat))
123123
, indexedModuleSymbolSentences
124-
:: !(Map.Map Id (declAtts, SentenceSymbol pat))
124+
:: !(Map.Map Id (declAtts, SentenceSymbol))
125125
, indexedModuleSortDescriptions
126-
:: !(Map.Map Id (Attribute.Sort, SentenceSort pat))
126+
:: !(Map.Map Id (Attribute.Sort, SentenceSort))
127127
, indexedModuleAxioms :: ![(axiomAtts, SentenceAxiom pat)]
128128
, indexedModuleClaims :: ![(axiomAtts, SentenceClaim pat)]
129129
, indexedModuleAttributes :: !(declAtts, Attributes)
@@ -150,14 +150,14 @@ data IndexedModule pat declAtts axiomAtts =
150150
recursiveIndexedModuleSortDescriptions
151151
:: forall pat declAtts axiomAtts
152152
. IndexedModule pat declAtts axiomAtts
153-
-> Map.Map Id (Attribute.Sort, SentenceSort pat)
153+
-> Map.Map Id (Attribute.Sort, SentenceSort)
154154
recursiveIndexedModuleSortDescriptions =
155155
recursiveIndexedModuleStuff indexedModuleSortDescriptions
156156

157157
recursiveIndexedModuleSymbolSentences
158158
:: forall pat axiomAtts
159159
. IndexedModule pat Attribute.Symbol axiomAtts
160-
-> Map.Map Id (Attribute.Symbol, SentenceSymbol pat)
160+
-> Map.Map Id (Attribute.Symbol, SentenceSymbol)
161161
recursiveIndexedModuleSymbolSentences =
162162
recursiveIndexedModuleStuff indexedModuleSymbolSentences
163163

@@ -273,12 +273,6 @@ erasePatterns indexedModule =
273273
{ indexedModuleAliasSentences =
274274
Lens.set (Lens.mapped . Lens._2 . Lens.mapped) ()
275275
$ indexedModuleAliasSentences indexedModule
276-
, indexedModuleSymbolSentences =
277-
Lens.set (Lens.mapped . Lens._2 . Lens.mapped) ()
278-
$ indexedModuleSymbolSentences indexedModule
279-
, indexedModuleSortDescriptions =
280-
Lens.set (Lens.mapped . Lens._2 . Lens.mapped) ()
281-
$ indexedModuleSortDescriptions indexedModule
282276
, indexedModuleAxioms = []
283277
, indexedModuleClaims = []
284278
, indexedModuleImports =
@@ -294,10 +288,6 @@ mapPatterns mapping indexedModule =
294288
indexedModule
295289
{ indexedModuleAliasSentences =
296290
(fmap . fmap . fmap) mapping indexedModuleAliasSentences
297-
, indexedModuleSymbolSentences =
298-
(fmap . fmap . fmap) mapping indexedModuleSymbolSentences
299-
, indexedModuleSortDescriptions =
300-
(fmap . fmap . fmap) mapping indexedModuleSortDescriptions
301291
, indexedModuleAxioms =
302292
(fmap . fmap . fmap) mapping indexedModuleAxioms
303293
, indexedModuleClaims =
@@ -308,8 +298,6 @@ mapPatterns mapping indexedModule =
308298
}
309299
where
310300
IndexedModule { indexedModuleAliasSentences } = indexedModule
311-
IndexedModule { indexedModuleSymbolSentences } = indexedModule
312-
IndexedModule { indexedModuleSortDescriptions } = indexedModule
313301
IndexedModule { indexedModuleAxioms } = indexedModule
314302
IndexedModule { indexedModuleClaims } = indexedModule
315303
IndexedModule { indexedModuleImports } = indexedModule
@@ -461,7 +449,7 @@ indexedModuleWithDefaultImports name defaultImport =
461449
-}
462450
hookedObjectSymbolSentences
463451
:: IndexedModule pat declAtts axiomAtts
464-
-> Map.Map Id (declAtts, SentenceSymbol pat)
452+
-> Map.Map Id (declAtts, SentenceSymbol)
465453
hookedObjectSymbolSentences
466454
IndexedModule
467455
{ indexedModuleSymbolSentences

‎kore/src/Kore/IndexedModule/Resolvers.hs

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ import qualified Kore.Syntax.Definition as Syntax
7878

7979
symbolSentencesMap
8080
:: IndexedModule patternType declAtts axiomAtts
81-
-> Map.Map Id (declAtts, SentenceSymbol patternType)
81+
-> Map.Map Id (declAtts, SentenceSymbol)
8282
symbolSentencesMap = indexedModuleSymbolSentences
8383

8484
aliasSentencesMap
@@ -88,7 +88,7 @@ aliasSentencesMap = indexedModuleAliasSentences
8888

8989
sortSentencesMap
9090
:: IndexedModule patternType declAtts axiomAtts
91-
-> Map.Map Id (Attribute.Sort, SentenceSort patternType)
91+
-> Map.Map Id (Attribute.Sort, SentenceSort)
9292
sortSentencesMap = indexedModuleSortDescriptions
9393

9494
-- |Given a KoreIndexedModule and a head, it looks up the 'SentenceSymbol' or
@@ -104,7 +104,7 @@ getHeadApplicationSorts m patternHead =
104104
where
105105
sentenceSorts
106106
:: SentenceSymbolOrAlias sentence
107-
=> [Sort] -> sentence pat -> ApplicationSorts
107+
=> [Sort] -> sentence -> ApplicationSorts
108108
sentenceSorts sortParameters sentence =
109109
assertRight $ symbolOrAliasSorts sortParameters sentence
110110

@@ -191,7 +191,7 @@ resolveSymbol
191191
:: MonadError (Error e) m
192192
=> IndexedModule patternType declAtts axiomAtts
193193
-> Id
194-
-> m (declAtts, SentenceSymbol patternType)
194+
-> m (declAtts, SentenceSymbol)
195195
resolveSymbol m headId =
196196
case resolveThing symbolSentencesMap m headId of
197197
Nothing ->
@@ -245,7 +245,7 @@ resolveSort
245245
:: MonadError (Error e) m
246246
=> IndexedModule patternType declAtts axiomAtts
247247
-> Id
248-
-> m (Attribute.Sort, SentenceSort patternType)
248+
-> m (Attribute.Sort, SentenceSort)
249249
resolveSort m sortId =
250250
case resolveThing sortSentencesMap m sortId of
251251
Nothing ->
@@ -318,7 +318,7 @@ findIndexedSort
318318
-- ^ indexed module
319319
-> Id
320320
-- ^ sort identifier
321-
-> error (SentenceSort patternType)
321+
-> error SentenceSort
322322
findIndexedSort indexedModule sort =
323323
fmap getIndexedSentence (resolveSort indexedModule sort)
324324

@@ -331,7 +331,7 @@ findIndexedSort indexedModule sort =
331331
applyToHeadSentence
332332
:: (forall sentence. SentenceSymbolOrAlias sentence
333333
=> [Sort]
334-
-> sentence pat
334+
-> sentence
335335
-> result)
336336
-> IndexedModule pat declAtts axiomAtts
337337
-> SymbolOrAlias
@@ -343,7 +343,7 @@ applyToResolution
343343
:: HasCallStack
344344
=> (forall sentence. SentenceSymbolOrAlias sentence
345345
=> [Sort]
346-
-> (declAtts, sentence pat)
346+
-> (declAtts, sentence)
347347
-> result)
348348
-> IndexedModule pat declAtts axiomAtts
349349
-> SymbolOrAlias

‎kore/src/Kore/Internal/ApplicationSorts.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ pattern from the given sort parameters.
4848
symbolOrAliasSorts
4949
:: (SentenceSymbolOrAlias sentence, MonadError (Error e) m)
5050
=> [Sort]
51-
-> sentence pat
51+
-> sentence
5252
-> m ApplicationSorts
5353
symbolOrAliasSorts params sentence = do
5454
variableToSort <-

0 commit comments

Comments
 (0)