You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
-- The stack 'v' represents variables that are currently assigned by the
44
+
-- solver. 'go' pushes a variable for a recursive call when it encounters
45
+
-- 'TryP', 'TryF', or 'TryS' and pops a variable when it encounters 'Leave'.
46
+
-- When 'go' processes a package goal, or a package goal followed by a
47
+
-- 'Failure', it calls 'atLevel' with the goal variable at the head of the
48
+
-- stack so that the predicate can also select messages relating to package
49
+
-- goal choices.
43
50
go:: [VarQPN] ->Int-> [Message] -> [String]
44
51
go _ _ []=[]
45
52
-- complex patterns
46
53
go v l (TryP qpn i :Enter:Failure c fr :Leave: ms) = goPReject v l qpn [i] c fr ms
47
54
go v l (TryF qfn b :Enter:Failure c fr :Leave: ms) = (atLevel (add (F qfn) v) l $"rejecting: "++ showQFNBool qfn b ++ showFR c fr) (go v l ms)
48
55
go v l (TryS qsn b :Enter:Failure c fr :Leave: ms) = (atLevel (add (S qsn) v) l $"rejecting: "++ showQSNBool qsn b ++ showFR c fr) (go v l ms)
49
56
go v l (Next (Goal (P qpn) gr) :TryP qpn' i : ms@(Enter:Next _ : _)) = (atLevel (add (P qpn) v) l $"trying: "++ showQPNPOpt qpn' i ++ showGRs gr) (go (add (P qpn) v) l ms)
57
+
go v l (Next (Goal (P qpn) gr) :Failure c fr : ms) =
58
+
let v' = add (P qpn) v
59
+
in (atLevel v' l $ showPackageGoal qpn gr) $ (atLevel v' l $ showFailure c fr) (go v l ms)
50
60
go v l (Failure c Backjump: ms@(Leave:Failure c' Backjump: _)) | c == c' = go v l ms
51
61
-- standard display
52
62
go v l (Enter: ms) = go v (l+1) ms
53
63
go v l (Leave: ms) = go (drop1 v) (l-1) ms
54
64
go v l (TryP qpn i : ms) = (atLevel (add (P qpn) v) l $"trying: "++ showQPNPOpt qpn i) (go (add (P qpn) v) l ms)
55
65
go v l (TryF qfn b : ms) = (atLevel (add (F qfn) v) l $"trying: "++ showQFNBool qfn b) (go (add (F qfn) v) l ms)
56
66
go v l (TryS qsn b : ms) = (atLevel (add (S qsn) v) l $"trying: "++ showQSNBool qsn b) (go (add (S qsn) v) l ms)
57
-
go v l (Next (Goal (P qpn) gr) : ms) = (atLevel (add (P qpn) v) l $"next goal: "++ showQPN qpn++ showGRs gr) (go v l ms)
67
+
go v l (Next (Goal (P qpn) gr) : ms) = (atLevel (add (P qpn) v) l $showPackageGoal qpn gr) (go v l ms)
58
68
go v l (Next _ : ms) = go v l ms -- ignore flag goals in the log
59
69
go v l (Success: ms) = (atLevel v l $"done") (go v l ms)
60
-
go v l (Failure c fr : ms) = (atLevel v l $"fail"++ showFR c fr) (go v l ms)
70
+
go v l (Failure c fr : ms) = (atLevel v l $ showFailure c fr) (go v l ms)
71
+
72
+
showPackageGoal::QPN->QGoalReasonChain->String
73
+
showPackageGoal qpn gr ="next goal: "++ showQPN qpn ++ showGRs gr
74
+
75
+
showFailure::ConflictSetQPN->FailReason->String
76
+
showFailure c fr ="fail"++ showFR c fr
61
77
62
78
add::VarQPN-> [VarQPN] -> [VarQPN]
63
79
add v vs = simplifyVar v : vs
@@ -68,6 +84,7 @@ showMessages p sl = go [] 0
68
84
goPReject v l qpn is c fr ms = (atLevel (P qpn : v) l $"rejecting: "++L.intercalate ", " (map (showQPNPOpt qpn) (reverse is)) ++ showFR c fr) (go v l ms)
69
85
70
86
-- write a message, but only if it's relevant; we can also enable or disable the display of the current level
0 commit comments