Skip to content

Commit 8210f59

Browse files
ttuegelttuegel
authored
Merge pull request #392 from ttuegel/remove-symbol-or-alias-sorts
Remove SymbolOrAliasSorts
2 parents 0bd9dc6 + 4700c69 commit 8210f59

File tree

161 files changed

+6907
-6636
lines changed

Some content is hidden

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

161 files changed

+6907
-6636
lines changed

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

Lines changed: 9 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,6 @@ import Data.Maybe
1313
( fromMaybe )
1414
import Data.Proxy
1515
( Proxy (..) )
16-
import Data.Reflection
17-
( give )
1816
import Data.Semigroup
1917
( (<>) )
2018
import qualified Data.Set as Set
@@ -35,13 +33,12 @@ import System.IO
3533
import Data.Limit
3634
( Limit (..) )
3735
import Kore.AST.Kore
38-
( CommonKorePattern )
36+
( CommonKorePattern, VerifiedKorePattern )
3937
import Kore.AST.Pure
4038
import Kore.AST.PureToKore
4139
( patternKoreToPure )
4240
import Kore.AST.Sentence
43-
import qualified Kore.ASTUtils.SmartConstructors as Pattern
44-
import Kore.ASTUtils.SmartPatterns
41+
import Kore.AST.Valid
4542
import Kore.ASTVerifier.DefinitionVerifier
4643
( AttributesVerification (DoNotVerifyAttributes),
4744
defaultAttributesVerification,
@@ -52,8 +49,6 @@ import Kore.Error
5249
import Kore.Exec
5350
import Kore.IndexedModule.IndexedModule
5451
( IndexedModule (..), VerifiedModule )
55-
import Kore.IndexedModule.MetadataTools
56-
( MetadataTools (..), extractMetadataTools )
5752
import Kore.Parser.Parser
5853
( fromKore, fromKorePattern )
5954
import Kore.Predicate.Predicate
@@ -341,7 +336,7 @@ externalizeFreshVars pat = Recursive.fold renameFreshLocal pat
341336
-> CommonStepPattern level
342337
renameFreshLocal (_ :< VariablePattern v@(Variable {variableName}))
343338
| name `Set.member` freshVarsIds =
344-
Var_ v {
339+
mkVar v {
345340
variableName = variableName
346341
{ getId =
347342
freshPrefix <> Text.filter (/= '_') name
@@ -451,7 +446,7 @@ mainWithOptions
451446
Just specIndexedModule ->
452447
either
453448
(\pat -> (ExitFailure 1, pat))
454-
(\_ -> (ExitSuccess, Pattern.mkTop))
449+
(\_ -> (ExitSuccess, mkTop $ mkSortVariable "R" ))
455450
<$> prove
456451
stepLimit
457452
indexedModule
@@ -502,30 +497,23 @@ mainPatternParseAndVerify
502497
:: VerifiedModule StepperAttributes
503498
-> String
504499
-> IO (CommonStepPattern Object)
505-
mainPatternParseAndVerify indexedModule patternFileName
506-
= do
500+
mainPatternParseAndVerify indexedModule patternFileName = do
507501
parsedPattern <- mainPatternParse patternFileName
508-
mainPatternVerify indexedModule parsedPattern
509-
return (makePurePattern parsedPattern)
502+
makePurePattern <$> mainPatternVerify indexedModule parsedPattern
510503

511504
mainParseSearchPattern
512505
:: VerifiedModule StepperAttributes
513506
-> String
514507
-> IO (CommonExpandedPattern Object)
515-
mainParseSearchPattern indexedModule patternFileName
516-
= do
517-
let
518-
metadataTools :: MetadataTools Object StepperAttributes
519-
metadataTools = extractMetadataTools indexedModule
520-
MetadataTools { symbolOrAliasSorts } = metadataTools
508+
mainParseSearchPattern indexedModule patternFileName = do
521509
purePattern <- mainPatternParseAndVerify indexedModule patternFileName
522510
case purePattern of
523511
And_ _ term predicateTerm -> return
524512
Predicated
525513
{ term
526514
, predicate =
527515
either (error . printError) id
528-
(give symbolOrAliasSorts makePredicate predicateTerm)
516+
(makePredicate predicateTerm)
529517
, substitution = mempty
530518
}
531519
_ -> error "Unexpected non-conjunctive pattern"
@@ -581,7 +569,7 @@ verifyDefinitionWithBase maybeBaseModule willChkAttr definition =
581569
Right indexedDefinition -> return indexedDefinition
582570

583571
makePurePattern
584-
:: CommonKorePattern
572+
:: VerifiedKorePattern
585573
-> CommonStepPattern Object
586574
makePurePattern pat =
587575
case patternKoreToPure Object pat of

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -121,7 +121,8 @@ main = do
121121
when willVerify $ do
122122
indexedModule <-
123123
mainModule (ModuleName mainModuleName) indexedModules
124-
mainPatternVerify indexedModule parsedPattern
124+
_ <- mainPatternVerify indexedModule parsedPattern
125+
return ()
125126
when willPrintPattern $
126127
putStrLn (prettyPrintToString parsedPattern)
127128

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

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -178,15 +178,12 @@ mainPatternVerify
178178
:: VerifiedModule attrs
179179
-- ^ Module containing definitions visible in the pattern
180180
-> CommonKorePattern -- ^ Parsed pattern to check well-formedness
181-
-> IO ()
182-
mainPatternVerify verifiedModule patt =
183-
do
184-
verifyResult <-
181+
-> IO VerifiedKorePattern
182+
mainPatternVerify verifiedModule patt = do
183+
verifyResult <-
185184
clockSomething "Verifying the pattern"
186185
(runPatternVerifier context $ verifyStandalonePattern Nothing patt)
187-
case verifyResult of
188-
Left err1 -> error (printError err1)
189-
Right _ -> return ()
186+
either (error . printError) return verifyResult
190187
where
191188
Builtin.Verifiers { patternVerifier } = Builtin.koreVerifiers
192189
indexedModule =

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

Lines changed: 26 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,9 @@ import Data.Function
88
import Data.Limit
99
( Limit (Unlimited) )
1010
import qualified Data.Map as Map
11+
import qualified Data.Set as Set
1112

13+
import qualified Kore.AST.Kore as Kore
1214
import Kore.AST.Pure
1315
import Kore.AST.PureToKore
1416
( patternKoreToPure )
@@ -17,12 +19,15 @@ import Kore.AST.Sentence
1719
import Kore.ASTVerifier.DefinitionVerifier
1820
( AttributesVerification (DoNotVerifyAttributes),
1921
verifyAndIndexDefinition )
22+
import qualified Kore.ASTVerifier.PatternVerifier as PatternVerifier
23+
import qualified Kore.Attribute.Null as Attribute
2024
import qualified Kore.Builtin as Builtin
2125
import Kore.Error
2226
( printError )
2327
import Kore.Exec
2428
import Kore.IndexedModule.IndexedModule
25-
( IndexedModule (..), VerifiedModule )
29+
( IndexedModule (..), VerifiedModule,
30+
mapIndexedModulePatterns )
2631
import Kore.Parser.Parser
2732
( fromKore, fromKorePattern )
2833
import Kore.Step.Pattern
@@ -125,6 +130,7 @@ execBenchmark root kFile definitionFile mainModuleName test =
125130
envWithCleanup setUp cleanUp $ bench name . nfIO . execution
126131
where
127132
name = takeFileName test
133+
setUp :: IO (VerifiedModule StepperAttributes, CommonStepPattern Object)
128134
setUp = do
129135
kompile
130136
definition <- readFile $ root </> definitionFile
@@ -139,12 +145,30 @@ execBenchmark root kFile definitionFile mainModuleName test =
139145
Just verifiedModule =
140146
fmap constructorFunctions
141147
$ Map.lookup mainModuleName verifiedModules
148+
indexedModule =
149+
mapIndexedModulePatterns
150+
Kore.eraseAnnotations
151+
verifiedModule
142152
pat <- parseProgram
143153
let
144154
parsedPattern = either error id $ fromKorePattern "" pat
155+
verifiedPattern =
156+
either (error . printError) id
157+
$ PatternVerifier.runPatternVerifier context
158+
$ PatternVerifier.verifyStandalonePattern Nothing parsedPattern
159+
where
160+
context =
161+
PatternVerifier.Context
162+
{ builtinPatternVerifier =
163+
Builtin.patternVerifier Builtin.koreVerifiers
164+
, indexedModule = Attribute.Null <$ indexedModule
165+
, declaredSortVariables = Set.empty
166+
, declaredVariables =
167+
PatternVerifier.emptyDeclaredVariables
168+
}
145169
purePattern =
146170
either (error . printError) id
147-
$ patternKoreToPure Object parsedPattern
171+
$ patternKoreToPure Object verifiedPattern
148172
return (verifiedModule, purePattern)
149173
execution
150174
:: (VerifiedModule StepperAttributes, CommonStepPattern Object)

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

Lines changed: 19 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,6 @@ module Kore.AST.Builders
1616
, bottom_ -- TODO: not used yet
1717
, ceilS_ -- TODO: not used yet
1818
, ceil_ -- TODO: not used yet
19-
, parameterizedDomainValue_
2019
, equalsAxiom_
2120
, equalsS_
2221
, equals_
@@ -45,6 +44,7 @@ module Kore.AST.Builders
4544

4645
import Control.Comonad.Trans.Cofree
4746
( CofreeF (..) )
47+
import Data.Functor.Classes
4848
import Data.Proxy
4949
( Proxy (..) )
5050
import Data.Text
@@ -56,7 +56,6 @@ import Kore.AST.BuildersImpl
5656
import Kore.AST.Pure
5757
import Kore.AST.Sentence
5858
import Kore.ASTHelpers
59-
import qualified Kore.Domain.Builtin as Domain
6059
import Kore.Error
6160

6261
{-|'sortParameter' defines a sort parameter that can be used in declarations.
@@ -78,6 +77,7 @@ applyPS
7877
:: ( Functor domain
7978
, SentenceSymbolOrAlias s
8079
, Show level
80+
, Show1 domain
8181
, Show (Pattern level domain Variable child)
8282
, child ~ CommonPurePattern level domain
8383
)
@@ -113,6 +113,7 @@ applyS
113113
:: ( Functor domain
114114
, SentenceSymbolOrAlias s
115115
, Show level
116+
, Show1 domain
116117
, Show (Pattern level domain Variable child)
117118
, child ~ CommonPurePattern level domain
118119
)
@@ -202,7 +203,7 @@ alias_
202203
-> Sort level
203204
-> [Variable level]
204205
-- ^ The left-hand side of the alias: the alias applied to these variables
205-
-> CommonPurePattern level domain
206+
-> PurePattern level domain Variable (Annotation.Null level)
206207
-- ^ The right-hand side of the alias
207208
-> PureSentenceAlias level domain
208209
alias_ name location = parameterizedAlias_ name location []
@@ -217,7 +218,7 @@ parameterizedAlias_
217218
-> Sort level
218219
-> [Variable level]
219220
-- ^ The left-hand side of the alias: the alias applied to these variables
220-
-> CommonPurePattern level domain
221+
-> PurePattern level domain Variable (Annotation.Null level)
221222
-- ^ The right-hand side of the alias
222223
-> PureSentenceAlias level domain
223224
parameterizedAlias_
@@ -270,6 +271,7 @@ equalsS_
270271
:: ( Functor domain
271272
, MetaOrObject level
272273
, Show (CommonPurePattern level domain)
274+
, Show1 domain
273275
)
274276
=> Sort level
275277
-> CommonPurePatternStub level domain
@@ -283,6 +285,7 @@ equals_
283285
:: ( Functor domain
284286
, MetaOrObject level
285287
, Show (CommonPurePattern level domain)
288+
, Show1 domain
286289
)
287290
=> CommonPurePatternStub level domain
288291
-> CommonPurePatternStub level domain
@@ -295,6 +298,7 @@ inS_
295298
:: ( Functor domain
296299
, MetaOrObject level
297300
, Show (CommonPurePattern level domain)
301+
, Show1 domain
298302
)
299303
=> Sort level
300304
-> CommonPurePatternStub level domain
@@ -308,6 +312,7 @@ in_
308312
:: ( Functor domain
309313
, MetaOrObject level
310314
, Show (CommonPurePattern level domain)
315+
, Show1 domain
311316
)
312317
=> CommonPurePatternStub level domain
313318
-> CommonPurePatternStub level domain
@@ -322,6 +327,7 @@ ceilS_
322327
, child ~ CommonPurePattern level domain
323328
, Show child
324329
, Show (Pattern level domain Variable child)
330+
, Show1 domain
325331
)
326332
=> Sort level
327333
-> CommonPurePatternStub level domain
@@ -336,6 +342,7 @@ ceil_
336342
, child ~ CommonPurePattern level domain
337343
, Show child
338344
, Show (Pattern level domain Variable child)
345+
, Show1 domain
339346
)
340347
=> CommonPurePatternStub level domain
341348
-> CommonPurePatternStub level domain
@@ -349,6 +356,7 @@ floorS_
349356
, child ~ CommonPurePattern level domain
350357
, Show child
351358
, Show (Pattern level domain Variable child)
359+
, Show1 domain
352360
)
353361
=> Sort level
354362
-> CommonPurePatternStub level domain
@@ -363,6 +371,7 @@ floor_
363371
, child ~ CommonPurePattern level domain
364372
, Show child
365373
, Show (Pattern level domain Variable child)
374+
, Show1 domain
366375
)
367376
=> CommonPurePatternStub level domain
368377
-> CommonPurePatternStub level domain
@@ -500,25 +509,6 @@ next_ =
500509
}
501510
)
502511

503-
-- |Builds a 'PatternStub' representing 'DomainValue' given a 'Sort' and
504-
-- a'String' for its operand.
505-
parameterizedDomainValue_
506-
:: Sort Object
507-
-> String
508-
-> CommonPurePatternStub Object Domain.Builtin
509-
parameterizedDomainValue_ sort str =
510-
SortedPatternStub
511-
SortedPattern
512-
{ sortedPatternSort = sort
513-
, sortedPatternPattern =
514-
DomainValuePattern DomainValue
515-
{ domainValueSort = sort
516-
, domainValueChild =
517-
(Domain.BuiltinPattern . asPurePattern . (mempty :<))
518-
(StringLiteralPattern $ StringLiteral str)
519-
}
520-
}
521-
522512
-- |Builds a 'PatternStub' representing 'Rewrites' given 'PatternStub's for its
523513
-- operands.
524514
rewrites_
@@ -546,6 +536,7 @@ parameterizedAxiom_
546536
, child ~ CommonPurePattern level domain
547537
, Show child
548538
, Show (Pattern level domain Variable child)
539+
, Show1 domain
549540
)
550541
=> [SortVariable level]
551542
-> CommonPurePatternStub level domain
@@ -564,9 +555,10 @@ parameterizedAxiom_
564555
SentenceAxiom
565556
{ sentenceAxiomParameters = parameters
566557
, sentenceAxiomPattern =
567-
quantifyFreeVariables s (asPurePattern $ Annotation.Null :< p)
558+
quantifyFreeVariables s (asPurePattern $ mempty :< p)
568559
, sentenceAxiomAttributes = Attributes []
569560
}
561+
570562
{-|Creates an axiom with no sort parameters from a pattern.
571563
-}
572564
axiom_
@@ -575,6 +567,7 @@ axiom_
575567
, MetaOrObject level
576568
, child ~ CommonPurePattern level domain
577569
, Show child
570+
, Show1 domain
578571
, Show (Pattern level domain Variable child)
579572
)
580573
=> CommonPurePatternStub level domain
@@ -594,6 +587,7 @@ parameterizedEqualsAxiom_
594587
, MetaOrObject level
595588
, child ~ CommonPurePattern level domain
596589
, Show child
590+
, Show1 domain
597591
, Show (Pattern level domain Variable child)
598592
)
599593
=> [SortVariable level]
@@ -618,6 +612,7 @@ equalsAxiom_
618612
, MetaOrObject level
619613
, child ~ CommonPurePattern level domain
620614
, Show child
615+
, Show1 domain
621616
, Show (Pattern level domain Variable child)
622617
)
623618
=> SortVariable level

0 commit comments

Comments
 (0)