Skip to content

Commit a390ba7

Browse files
ttuegelttuegel
committed
Remove ProofState type family
The ProofState associated type family is always instantiated at the concrete ProofState type, so this was a meaningless layer of indirection.
1 parent 46db90a commit a390ba7

File tree

3 files changed

+55
-101
lines changed

3 files changed

+55
-101
lines changed

‎kore/src/Kore/Strategies/Goal.hs

Lines changed: 48 additions & 88 deletions
Original file line numberDiff line numberDiff line change
@@ -60,9 +60,6 @@ import Data.Generics.Product
6060
import Data.Generics.Wrapped
6161
( _Unwrapped
6262
)
63-
import Data.Kind
64-
( Type
65-
)
6663
import Data.List.Extra
6764
( groupSortOn
6865
, sortOn
@@ -162,7 +159,6 @@ import Kore.Step.Transition
162159
import qualified Kore.Step.Transition as Transition
163160
import Kore.Strategies.ProofState hiding
164161
( Prim
165-
, ProofState
166162
, proofState
167163
)
168164
import qualified Kore.Strategies.ProofState as ProofState
@@ -190,8 +186,7 @@ See also: 'Strategy.pickFinal', 'extractUnproven'
190186
-}
191187
unprovenNodes
192188
:: forall goal a
193-
. ProofState.ProofState a ~ ProofState goal a
194-
=> Strategy.ExecutionGraph (ProofState goal a) (Rule goal)
189+
. Strategy.ExecutionGraph (ProofState a) (Rule goal)
195190
-> MultiOr.MultiOr a
196191
unprovenNodes executionGraph =
197192
MultiOr.MultiOr
@@ -202,14 +197,12 @@ unprovenNodes executionGraph =
202197
-}
203198
proven
204199
:: forall goal a
205-
. ProofState.ProofState a ~ ProofState goal a
206-
=> Strategy.ExecutionGraph (ProofState goal a) (Rule goal)
200+
. Strategy.ExecutionGraph (ProofState a) (Rule goal)
207201
-> Bool
208202
proven = Foldable.null . unprovenNodes
209203

210204
class Goal goal where
211205
type Prim goal
212-
type ProofState goal :: Type -> Type
213206

214207
goalToRule :: goal -> Rule goal
215208
default goalToRule
@@ -220,8 +213,8 @@ class Goal goal where
220213
transitionRule
221214
:: (MonadCatch m, MonadSimplify m)
222215
=> Prim goal
223-
-> ProofState goal goal
224-
-> Strategy.TransitionT (Rule goal) m (ProofState goal goal)
216+
-> ProofState goal
217+
-> Strategy.TransitionT (Rule goal) m (ProofState goal)
225218

226219
strategy
227220
:: goal
@@ -286,7 +279,6 @@ Things to note when implementing your own:
286279

287280
instance Goal OnePathRule where
288281
type Prim OnePathRule = ProofState.Prim (Rule OnePathRule)
289-
type ProofState OnePathRule = ProofState.ProofState
290282

291283
goalToRule =
292284
OnePathRewriteRule
@@ -321,7 +313,7 @@ deriveParOnePath
321313
=> [Rule OnePathRule]
322314
-> OnePathRule
323315
-> Strategy.TransitionT (Rule OnePathRule) simplifier
324-
(ProofState OnePathRule OnePathRule)
316+
(ProofState OnePathRule)
325317
deriveParOnePath rules =
326318
derivePar _Unwrapped OnePathRewriteRule rewrites
327319
where
@@ -332,7 +324,7 @@ deriveSeqOnePath
332324
=> [Rule OnePathRule]
333325
-> OnePathRule
334326
-> Strategy.TransitionT (Rule OnePathRule) simplifier
335-
(ProofState OnePathRule OnePathRule)
327+
(ProofState OnePathRule)
336328
deriveSeqOnePath rules =
337329
deriveSeq _Unwrapped OnePathRewriteRule rewrites
338330
where
@@ -346,7 +338,6 @@ instance ClaimExtractor OnePathRule where
346338

347339
instance Goal AllPathRule where
348340
type Prim AllPathRule = ProofState.Prim (Rule AllPathRule)
349-
type ProofState AllPathRule = ProofState.ProofState
350341

351342
goalToRule =
352343
AllPathRewriteRule
@@ -381,7 +372,7 @@ deriveParAllPath
381372
=> [Rule AllPathRule]
382373
-> AllPathRule
383374
-> Strategy.TransitionT (Rule AllPathRule) simplifier
384-
(ProofState AllPathRule AllPathRule)
375+
(ProofState AllPathRule)
385376
deriveParAllPath rules =
386377
derivePar _Unwrapped AllPathRewriteRule rewrites
387378
where
@@ -392,7 +383,7 @@ deriveSeqAllPath
392383
=> [Rule AllPathRule]
393384
-> AllPathRule
394385
-> Strategy.TransitionT (Rule AllPathRule) simplifier
395-
(ProofState AllPathRule AllPathRule)
386+
(ProofState AllPathRule)
396387
deriveSeqAllPath rules =
397388
deriveSeq _Unwrapped AllPathRewriteRule rewrites
398389
where
@@ -406,7 +397,6 @@ instance ClaimExtractor AllPathRule where
406397

407398
instance Goal ReachabilityRule where
408399
type Prim ReachabilityRule = ProofState.Prim (Rule ReachabilityRule)
409-
type ProofState ReachabilityRule = ProofState.ProofState
410400

411401
goalToRule (OnePath rule) =
412402
ReachabilityRewriteRule
@@ -420,18 +410,11 @@ instance Goal ReachabilityRule where
420410
$ getAllPathRule rule
421411

422412
transitionRule
423-
:: (MonadCatch m, MonadSimplify m)
424-
=> Prim ReachabilityRule
425-
-> ProofState
426-
ReachabilityRule
427-
ReachabilityRule
428-
-> Strategy.TransitionT
429-
(Rule ReachabilityRule)
430-
m
431-
( ProofState
432-
ReachabilityRule
433-
ReachabilityRule
434-
)
413+
:: (MonadCatch m, MonadSimplify m)
414+
=> Prim ReachabilityRule
415+
-> ProofState ReachabilityRule
416+
-> Strategy.TransitionT (Rule ReachabilityRule) m
417+
(ProofState ReachabilityRule)
435418
transitionRule = logTransitionRule $ \prim proofstate ->
436419
case proofstate of
437420
Goal (OnePath rule) ->
@@ -520,14 +503,10 @@ reachabilityAllPathStrategy strategy' =
520503
ruleAllPathToRuleReachability
521504
strategy'
522505

523-
allPathProofState
524-
:: ProofState AllPathRule AllPathRule
525-
-> ProofState ReachabilityRule ReachabilityRule
506+
allPathProofState :: ProofState AllPathRule -> ProofState ReachabilityRule
526507
allPathProofState = fmap AllPath
527508

528-
onePathProofState
529-
:: ProofState OnePathRule OnePathRule
530-
-> ProofState ReachabilityRule ReachabilityRule
509+
onePathProofState :: ProofState OnePathRule -> ProofState ReachabilityRule
531510
onePathProofState = fmap OnePath
532511

533512
primRuleOnePath
@@ -568,36 +547,35 @@ data TransitionRuleTemplate monad goal =
568547
{ simplifyTemplate
569548
:: goal -> Strategy.TransitionT (Rule goal) monad goal
570549
, checkImplicationTemplate
571-
:: (forall x. x -> ProofState goal x)
550+
:: (forall x. x -> ProofState x)
572551
-> goal
573-
-> Strategy.TransitionT (Rule goal) monad (ProofState goal goal)
552+
-> Strategy.TransitionT (Rule goal) monad (ProofState goal)
574553
, isTriviallyValidTemplate :: goal -> Bool
575554
, deriveParTemplate
576555
:: [Rule goal]
577556
-> goal
578-
-> Strategy.TransitionT (Rule goal) monad (ProofState goal goal)
557+
-> Strategy.TransitionT (Rule goal) monad (ProofState goal)
579558
, deriveSeqTemplate
580559
:: [Rule goal]
581560
-> goal
582-
-> Strategy.TransitionT (Rule goal) monad (ProofState goal goal)
561+
-> Strategy.TransitionT (Rule goal) monad (ProofState goal)
583562
}
584563

564+
type TransitionRule m goal =
565+
Prim goal
566+
-> ProofState goal
567+
-> Strategy.TransitionT (Rule goal) m (ProofState goal)
568+
585569
logTransitionRule
586-
:: forall m goal
570+
:: forall m
587571
. MonadSimplify m
588-
=> goal ~ ReachabilityRule
589-
=> ( Prim goal
590-
-> ProofState goal goal
591-
-> Strategy.TransitionT (Rule goal) m (ProofState goal goal)
592-
)
593-
-> ( Prim goal
594-
-> ProofState goal goal
595-
-> Strategy.TransitionT (Rule goal) m (ProofState goal goal)
596-
)
597-
logTransitionRule rule prim proofState = case proofState of
598-
Goal goal -> logWith goal
599-
GoalRemainder goal -> logWith goal
600-
_ -> rule prim proofState
572+
=> TransitionRule m ReachabilityRule
573+
-> TransitionRule m ReachabilityRule
574+
logTransitionRule rule prim proofState =
575+
case proofState of
576+
Goal goal -> logWith goal
577+
GoalRemainder goal -> logWith goal
578+
_ -> rule prim proofState
601579
where
602580
logWith goal = case prim of
603581
Simplify ->
@@ -614,12 +592,9 @@ logTransitionRule rule prim proofState = case proofState of
614592
transitionRuleTemplate
615593
:: forall m goal
616594
. MonadSimplify m
617-
=> ProofState goal goal ~ ProofState.ProofState goal
618595
=> Prim goal ~ ProofState.Prim (Rule goal)
619596
=> TransitionRuleTemplate m goal
620-
-> Prim goal
621-
-> ProofState goal goal
622-
-> Strategy.TransitionT (Rule goal) m (ProofState goal goal)
597+
-> TransitionRule m goal
623598
transitionRuleTemplate
624599
TransitionRuleTemplate
625600
{ simplifyTemplate
@@ -633,8 +608,8 @@ transitionRuleTemplate
633608
where
634609
transitionRuleWorker
635610
:: Prim goal
636-
-> ProofState goal goal
637-
-> Strategy.TransitionT (Rule goal) m (ProofState goal goal)
611+
-> ProofState goal
612+
-> Strategy.TransitionT (Rule goal) m (ProofState goal)
638613
transitionRuleWorker CheckProven Proven = empty
639614
transitionRuleWorker CheckGoalRemainder (GoalRemainder _) = empty
640615

@@ -799,11 +774,10 @@ checkImplication
799774
:: forall goal m
800775
. MonadSimplify m
801776
=> MonadCatch m
802-
=> ProofState.ProofState goal ~ ProofState goal goal
803777
=> Lens' goal (RulePattern VariableName)
804-
-> (forall x. x -> ProofState goal x)
778+
-> (forall x. x -> ProofState x)
805779
-> goal
806-
-> Strategy.TransitionT (Rule goal) m (ProofState goal goal)
780+
-> Strategy.TransitionT (Rule goal) m (ProofState goal)
807781
checkImplication lensRulePattern mkState goal =
808782
goal
809783
& Lens.traverseOf lensRulePattern (Compose . checkImplicationWorker)
@@ -812,7 +786,7 @@ checkImplication lensRulePattern mkState goal =
812786
where
813787
checkImplicationWorker
814788
:: RulePattern VariableName
815-
-> m (ProofState goal (RulePattern VariableName))
789+
-> m (ProofState (RulePattern VariableName))
816790
checkImplicationWorker (snd . Step.refreshRule mempty -> rulePattern) =
817791
do
818792
removal <- removalPatterns destination configuration existentials
@@ -882,12 +856,11 @@ instance Exception WithConfiguration
882856
derivePar
883857
:: forall m goal
884858
. (MonadCatch m, MonadSimplify m)
885-
=> ProofState.ProofState goal ~ ProofState goal goal
886859
=> Lens' goal (RulePattern VariableName)
887860
-> (RewriteRule RewritingVariableName -> Rule goal)
888861
-> [RewriteRule RewritingVariableName]
889862
-> goal
890-
-> Strategy.TransitionT (Rule goal) m (ProofState goal goal)
863+
-> Strategy.TransitionT (Rule goal) m (ProofState goal)
891864
derivePar lensRulePattern mkRule =
892865
deriveWith lensRulePattern mkRule
893866
$ Step.applyRewriteRulesParallel Unification.unificationProcedure
@@ -901,13 +874,12 @@ type Deriver monad =
901874
deriveWith
902875
:: forall m goal
903876
. MonadCatch m
904-
=> ProofState.ProofState goal ~ ProofState goal goal
905877
=> Lens' goal (RulePattern VariableName)
906878
-> (RewriteRule RewritingVariableName -> Rule goal)
907879
-> Deriver m
908880
-> [RewriteRule RewritingVariableName]
909881
-> goal
910-
-> Strategy.TransitionT (Rule goal) m (ProofState goal goal)
882+
-> Strategy.TransitionT (Rule goal) m (ProofState goal)
911883
deriveWith lensRulePattern mkRule takeStep rewrites goal =
912884
getCompose
913885
$ Lens.forOf lensRulePattern goal
@@ -922,12 +894,11 @@ deriveWith lensRulePattern mkRule takeStep rewrites goal =
922894
deriveSeq
923895
:: forall m goal
924896
. (MonadCatch m, MonadSimplify m)
925-
=> ProofState.ProofState goal ~ ProofState goal goal
926897
=> Lens' goal (RulePattern VariableName)
927898
-> (RewriteRule RewritingVariableName -> Rule goal)
928899
-> [RewriteRule RewritingVariableName]
929900
-> goal
930-
-> Strategy.TransitionT (Rule goal) m (ProofState goal goal)
901+
-> Strategy.TransitionT (Rule goal) m (ProofState goal)
931902
deriveSeq lensRulePattern mkRule =
932903
deriveWith lensRulePattern mkRule . flip
933904
$ Step.applyRewriteRulesSequence Unification.unificationProcedure
@@ -1055,15 +1026,14 @@ debugProofStateBracket
10551026
. MonadLog monad
10561027
=> ToReachabilityRule goal
10571028
=> Coercible (Rule goal) (RewriteRule RewritingVariableName)
1058-
=> ProofState goal goal ~ ProofState.ProofState goal
10591029
=> Prim goal ~ ProofState.Prim (Rule goal)
1060-
=> ProofState goal goal
1030+
=> ProofState goal
10611031
-- ^ current proof state
10621032
-> Prim goal
10631033
-- ^ transition
1064-
-> monad (ProofState goal goal)
1034+
-> monad (ProofState goal)
10651035
-- ^ action to be computed
1066-
-> monad (ProofState goal goal)
1036+
-> monad (ProofState goal)
10671037
debugProofStateBracket
10681038
(fmap toReachabilityRule -> proofState)
10691039
(coerce -> transition)
@@ -1083,13 +1053,12 @@ debugProofStateFinal
10831053
=> MonadLog monad
10841054
=> ToReachabilityRule goal
10851055
=> Coercible (Rule goal) (RewriteRule RewritingVariableName)
1086-
=> ProofState goal goal ~ ProofState.ProofState goal
10871056
=> Prim goal ~ ProofState.Prim (Rule goal)
1088-
=> ProofState goal goal
1057+
=> ProofState goal
10891058
-- ^ current proof state
10901059
-> Prim goal
10911060
-- ^ transition
1092-
-> monad (ProofState goal goal)
1061+
-> monad (ProofState goal)
10931062
debugProofStateFinal
10941063
(fmap toReachabilityRule -> proofState)
10951064
(coerce -> transition)
@@ -1106,18 +1075,9 @@ withDebugProofState
11061075
. MonadLog monad
11071076
=> ToReachabilityRule goal
11081077
=> Coercible (Rule goal) (RewriteRule RewritingVariableName)
1109-
=> ProofState goal goal ~ ProofState.ProofState goal
11101078
=> Prim goal ~ ProofState.Prim (Rule goal)
1111-
=>
1112-
( Prim goal
1113-
-> ProofState goal goal
1114-
-> Strategy.TransitionT (Rule goal) monad (ProofState goal goal)
1115-
)
1116-
->
1117-
( Prim goal
1118-
-> ProofState goal goal
1119-
-> Strategy.TransitionT (Rule goal) monad (ProofState goal goal)
1120-
)
1079+
=> TransitionRule monad goal
1080+
-> TransitionRule monad goal
11211081
withDebugProofState transitionFunc =
11221082
\transition state ->
11231083
Transition.orElse

0 commit comments

Comments
 (0)