Skip to content

Commit 46db90a

Browse files
ttuegelttuegel
committed
Rename "remove destination" to "check implication"
We would like to use the same terminology as the domain experts, which is "check implication".
1 parent 8424ed0 commit 46db90a

File tree

4 files changed

+44
-44
lines changed

4 files changed

+44
-44
lines changed

‎kore/src/Kore/Log/InfoReachability.hs

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ License : NCSA
66
module Kore.Log.InfoReachability
77
( InfoReachability (..)
88
, whileSimplify
9-
, whileRemoveDestination
9+
, whileCheckImplication
1010
, whileDeriveSeq
1111
, whileDerivePar
1212
) where
@@ -19,7 +19,7 @@ import qualified Pretty
1919

2020
data InfoReachability
2121
= InfoSimplify !ReachabilityRule
22-
| InfoRemoveDestination !ReachabilityRule
22+
| InfoCheckImplication !ReachabilityRule
2323
| InfoDeriveSeq ![Rule ReachabilityRule] !ReachabilityRule
2424
| InfoDerivePar ![Rule ReachabilityRule] !ReachabilityRule
2525
deriving (Show)
@@ -55,8 +55,8 @@ prettyInfoReachabilityGoalAndRules transition goal rules fromRule =
5555
instance Pretty.Pretty InfoReachability where
5656
pretty (InfoSimplify goal) =
5757
prettyInfoReachabilityGoal "Simplify" goal
58-
pretty (InfoRemoveDestination goal) =
59-
prettyInfoReachabilityGoal "RemoveDestination" goal
58+
pretty (InfoCheckImplication goal) =
59+
prettyInfoReachabilityGoal "CheckImplication" goal
6060
pretty (InfoDeriveSeq rules goal) =
6161
prettyInfoReachabilityGoalAndRules
6262
"DeriveSeq"
@@ -74,7 +74,7 @@ instance Entry InfoReachability where
7474
entrySeverity _ = Info
7575
shortDoc (InfoSimplify _) =
7676
Just "While simplifying the configuration"
77-
shortDoc (InfoRemoveDestination _) =
77+
shortDoc (InfoCheckImplication _) =
7878
Just "While checking implication of the proof goal"
7979
shortDoc (InfoDeriveSeq _ _) =
8080
Just "While applying axioms in sequence"
@@ -89,12 +89,12 @@ whileSimplify
8989
-> log a
9090
whileSimplify goal = logWhile (InfoSimplify goal)
9191

92-
whileRemoveDestination
92+
whileCheckImplication
9393
:: MonadLog log
9494
=> ReachabilityRule
9595
-> log a
9696
-> log a
97-
whileRemoveDestination goal = logWhile (InfoRemoveDestination goal)
97+
whileCheckImplication goal = logWhile (InfoCheckImplication goal)
9898

9999
whileDeriveSeq
100100
:: MonadLog log

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

Lines changed: 21 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -298,7 +298,7 @@ instance Goal OnePathRule where
298298
(withDebugProofState . transitionRuleTemplate)
299299
TransitionRuleTemplate
300300
{ simplifyTemplate = simplify _Unwrapped
301-
, removeDestinationTemplate = removeDestination _Unwrapped
301+
, checkImplicationTemplate = checkImplication _Unwrapped
302302
, isTriviallyValidTemplate = isTriviallyValid _Unwrapped
303303
, deriveParTemplate = deriveParOnePath
304304
, deriveSeqTemplate = deriveSeqOnePath
@@ -358,7 +358,7 @@ instance Goal AllPathRule where
358358
(withDebugProofState . transitionRuleTemplate)
359359
TransitionRuleTemplate
360360
{ simplifyTemplate = simplify _Unwrapped
361-
, removeDestinationTemplate = removeDestination _Unwrapped
361+
, checkImplicationTemplate = checkImplication _Unwrapped
362362
, isTriviallyValidTemplate = isTriviallyValid _Unwrapped
363363
, deriveParTemplate = deriveParAllPath
364364
, deriveSeqTemplate = deriveSeqAllPath
@@ -567,7 +567,7 @@ data TransitionRuleTemplate monad goal =
567567
TransitionRuleTemplate
568568
{ simplifyTemplate
569569
:: goal -> Strategy.TransitionT (Rule goal) monad goal
570-
, removeDestinationTemplate
570+
, checkImplicationTemplate
571571
:: (forall x. x -> ProofState goal x)
572572
-> goal
573573
-> Strategy.TransitionT (Rule goal) monad (ProofState goal goal)
@@ -602,8 +602,8 @@ logTransitionRule rule prim proofState = case proofState of
602602
logWith goal = case prim of
603603
Simplify ->
604604
whileSimplify goal $ rule prim proofState
605-
RemoveDestination ->
606-
whileRemoveDestination goal $ rule prim proofState
605+
CheckImplication ->
606+
whileCheckImplication goal $ rule prim proofState
607607
(DeriveSeq rules) ->
608608
whileDeriveSeq rules goal $ rule prim proofState
609609
(DerivePar rules) ->
@@ -623,7 +623,7 @@ transitionRuleTemplate
623623
transitionRuleTemplate
624624
TransitionRuleTemplate
625625
{ simplifyTemplate
626-
, removeDestinationTemplate
626+
, checkImplicationTemplate
627627
, isTriviallyValidTemplate
628628
, deriveParTemplate
629629
, deriveSeqTemplate
@@ -654,12 +654,12 @@ transitionRuleTemplate
654654
Profile.timeStrategy "Goal.SimplifyRemainder"
655655
$ GoalRemainder <$> simplifyTemplate goal
656656

657-
transitionRuleWorker RemoveDestination (Goal goal) =
658-
Profile.timeStrategy "Goal.RemoveDestination"
659-
$ removeDestinationTemplate Goal goal
660-
transitionRuleWorker RemoveDestination (GoalRemainder goal) =
661-
Profile.timeStrategy "Goal.RemoveDestinationRemainder"
662-
$ removeDestinationTemplate GoalRemainder goal
657+
transitionRuleWorker CheckImplication (Goal goal) =
658+
Profile.timeStrategy "Goal.CheckImplication"
659+
$ checkImplicationTemplate Goal goal
660+
transitionRuleWorker CheckImplication (GoalRemainder goal) =
661+
Profile.timeStrategy "Goal.CheckImplicationRemainder"
662+
$ checkImplicationTemplate GoalRemainder goal
663663

664664
transitionRuleWorker TriviallyValid (Goal goal)
665665
| isTriviallyValidTemplate goal =
@@ -712,7 +712,7 @@ onePathFirstStep axioms =
712712
, CheckGoalRemainder
713713
, Simplify
714714
, TriviallyValid
715-
, RemoveDestination
715+
, CheckImplication
716716
, DeriveSeq axioms
717717
, Simplify
718718
, TriviallyValid
@@ -733,7 +733,7 @@ onePathFollowupStep claims axioms =
733733
, CheckGoalRemainder
734734
, Simplify
735735
, TriviallyValid
736-
, RemoveDestination
736+
, CheckImplication
737737
, DeriveSeq claims
738738
, Simplify
739739
, TriviallyValid
@@ -764,7 +764,7 @@ allPathFirstStep axiomGroups =
764764
, CheckGoalRemainder
765765
, Simplify
766766
, TriviallyValid
767-
, RemoveDestination
767+
, CheckImplication
768768
]
769769
<> groupStrategy axiomGroups <>
770770
[ ResetGoal
@@ -783,7 +783,7 @@ allPathFollowupStep claims axiomGroups =
783783
, CheckGoalRemainder
784784
, Simplify
785785
, TriviallyValid
786-
, RemoveDestination
786+
, CheckImplication
787787
, DeriveSeq claims
788788
, Simplify
789789
, TriviallyValid
@@ -795,7 +795,7 @@ allPathFollowupStep claims axiomGroups =
795795
]
796796

797797
-- | Remove the destination of the goal.
798-
removeDestination
798+
checkImplication
799799
:: forall goal m
800800
. MonadSimplify m
801801
=> MonadCatch m
@@ -804,16 +804,16 @@ removeDestination
804804
-> (forall x. x -> ProofState goal x)
805805
-> goal
806806
-> Strategy.TransitionT (Rule goal) m (ProofState goal goal)
807-
removeDestination lensRulePattern mkState goal =
807+
checkImplication lensRulePattern mkState goal =
808808
goal
809-
& Lens.traverseOf lensRulePattern (Compose . removeDestinationWorker)
809+
& Lens.traverseOf lensRulePattern (Compose . checkImplicationWorker)
810810
& getCompose
811811
& lift
812812
where
813-
removeDestinationWorker
813+
checkImplicationWorker
814814
:: RulePattern VariableName
815815
-> m (ProofState goal (RulePattern VariableName))
816-
removeDestinationWorker (snd . Step.refreshRule mempty -> rulePattern) =
816+
checkImplicationWorker (snd . Step.refreshRule mempty -> rulePattern) =
817817
do
818818
removal <- removalPatterns destination configuration existentials
819819
when (isTop removal) (succeed . mkState $ rulePattern)

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ data Prim rule
3737
| ResetGoal
3838
-- ^ Mark all goals rewritten previously as new goals.
3939
| Simplify
40-
| RemoveDestination
40+
| CheckImplication
4141
| TriviallyValid
4242
| DerivePar [rule]
4343
| DeriveSeq [rule]
@@ -49,7 +49,7 @@ instance Filterable Prim where
4949
mapMaybe _ CheckGoalStuck = CheckGoalStuck
5050
mapMaybe _ ResetGoal = ResetGoal
5151
mapMaybe _ Simplify = Simplify
52-
mapMaybe _ RemoveDestination = RemoveDestination
52+
mapMaybe _ CheckImplication = CheckImplication
5353
mapMaybe _ TriviallyValid = TriviallyValid
5454
mapMaybe f (DerivePar rules) = DerivePar (mapMaybe f rules)
5555
mapMaybe f (DeriveSeq rules) = DeriveSeq (mapMaybe f rules)
@@ -60,7 +60,7 @@ instance Unparse goal => Pretty (Prim goal) where
6060
pretty CheckGoalStuck = "Transition CheckGoalStuck."
6161
pretty ResetGoal = "Transition ResetGoal."
6262
pretty Simplify = "Transition Simplify."
63-
pretty RemoveDestination = "Transition RemoveDestination."
63+
pretty CheckImplication = "Transition CheckImplication."
6464
pretty TriviallyValid = "Transition TriviallyValid."
6565
pretty (DerivePar rules) =
6666
Pretty.vsep
@@ -83,7 +83,7 @@ data ProofState goal
8383
| GoalStuck !goal
8484
-- ^ If the terms unify and the condition does not imply
8585
-- the goal, the proof is stuck. This state should be reachable
86-
-- only by applying RemoveDestination.
86+
-- only by applying CheckImplication.
8787
| Proven
8888
-- ^ The parent goal was proven.
8989
deriving (Eq, Show, Ord, Functor, GHC.Generic)

‎kore/test/Test/Kore/Strategies/AllPath/AllPath.hs

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ module Test.Kore.Strategies.AllPath.AllPath
22
( test_unprovenNodes
33
, test_transitionRule_CheckProven
44
, test_transitionRule_CheckGoalRem
5-
, test_transitionRule_RemoveDestination
5+
, test_transitionRule_CheckImplication
66
, test_transitionRule_TriviallyValid
77
, test_transitionRule_DerivePar
88
, test_runStrategy
@@ -147,14 +147,14 @@ test_transitionRule_CheckGoalRem =
147147
done :: HasCallStack => ProofState -> TestTree
148148
done state = run state `satisfies_` Foldable.null
149149

150-
test_transitionRule_RemoveDestination :: [TestTree]
151-
test_transitionRule_RemoveDestination =
150+
test_transitionRule_CheckImplication :: [TestTree]
151+
test_transitionRule_CheckImplication =
152152
[ unmodified ProofState.Proven
153153
, unmodified (ProofState.GoalRemainder (A, B))
154154
, ProofState.Goal (B, B) `becomes` (ProofState.Goal (Bot, B), mempty)
155155
]
156156
where
157-
run = runTransitionRule ProofState.RemoveDestination
157+
run = runTransitionRule ProofState.CheckImplication
158158
unmodified :: HasCallStack => ProofState -> TestTree
159159
unmodified state = run state `equals_` [(state, mempty)]
160160
becomes initial final = run initial `equals_` [final]
@@ -329,7 +329,7 @@ instance Goal.Goal Goal where
329329
(Strategy.sequence . map Strategy.apply)
330330
[ ProofState.CheckProven
331331
, ProofState.CheckGoalRemainder
332-
, ProofState.RemoveDestination
332+
, ProofState.CheckImplication
333333
, ProofState.TriviallyValid
334334
, ProofState.DerivePar axioms
335335
, ProofState.Simplify
@@ -341,14 +341,14 @@ instance Goal.Goal Goal where
341341
(Strategy.sequence . map Strategy.apply)
342342
[ ProofState.CheckProven
343343
, ProofState.CheckGoalRemainder
344-
, ProofState.RemoveDestination
344+
, ProofState.CheckImplication
345345
, ProofState.TriviallyValid
346346
, ProofState.DeriveSeq claims
347-
, ProofState.RemoveDestination
347+
, ProofState.CheckImplication
348348
, ProofState.Simplify
349349
, ProofState.TriviallyValid
350350
, ProofState.DerivePar axioms
351-
, ProofState.RemoveDestination
351+
, ProofState.CheckImplication
352352
, ProofState.Simplify
353353
, ProofState.TriviallyValid
354354
, ProofState.ResetGoal
@@ -362,8 +362,8 @@ instance Goal.Goal Goal where
362362
Goal.TransitionRuleTemplate
363363
{ simplifyTemplate =
364364
simplify
365-
, removeDestinationTemplate =
366-
removeDestination
365+
, checkImplicationTemplate =
366+
checkImplication
367367
, isTriviallyValidTemplate =
368368
isTriviallyValid
369369
, deriveParTemplate =
@@ -381,11 +381,11 @@ instance Debug (Goal.Rule Goal)
381381
instance Diff (Goal.Rule Goal)
382382

383383
-- | The destination-removal rule for our unit test goal.
384-
removeDestination
384+
checkImplication
385385
:: (Goal -> ProofState)
386386
-> Goal
387387
-> Strategy.TransitionT (Goal.Rule Goal) m ProofState
388-
removeDestination constr (src, dst) =
388+
checkImplication constr (src, dst) =
389389
return . constr $ (difference src dst, dst)
390390

391391
-- | The goal is trivially valid when the members are equal.

0 commit comments

Comments
 (0)