Commit 1df47e71 authored by Franz Thoma's avatar Franz Thoma
Browse files

Update documentation

parent e83ba105
......@@ -24,6 +24,8 @@ type Log m a = Progress m (ConflictSet QPN, ConflictMap) a
messages :: Progress step fail done -> [step]
messages = foldProgress (:) (const []) (const [])
data Exhaustive = Exhaustive | NotExhaustive
-- | Postprocesses a log file. Takes as an argument a limit on allowed backjumps.
-- If the limit is 'Nothing', then infinitely many backjumps are allowed. If the
-- limit is 'Just 0', backtracking is completely disabled.
......@@ -38,26 +40,27 @@ logToProgress mbj l = let
-- messages until the maximum number of backjumps has been reached. It filters out
-- and ignores repeated backjumps. If proc reaches the backjump limit, it truncates
-- the 'Progress' and ends it with the last conflict set. Otherwise, it leaves the
-- original success result or replaces the original failure with 'Nothing'.
proc :: Maybe Int -> Log Message b -> Progress Message (Bool, ConflictSet QPN, ConflictMap) b
-- original result.
proc :: Maybe Int -> Log Message b -> Progress Message (Exhaustive, ConflictSet QPN, ConflictMap) b
proc _ (Done x) = Done x
proc _ (Fail (cs, cm)) = Fail (True, cs, cm)
proc _ (Fail (cs, cm)) = Fail (Exhaustive, cs, cm)
proc mbj' (Step x@(Failure cs Backjump) xs@(Step Leave (Step (Failure cs' Backjump) _)))
| cs == cs' = Step x (proc mbj' xs) -- repeated backjumps count as one
proc (Just 0) (Step (Failure cs Backjump) _) = Fail (False, cs, mempty)
proc (Just 0) (Step (Failure cs Backjump) _) = Fail (NotExhaustive, cs, mempty) -- No final conflict map available
proc (Just n) (Step x@(Failure _ Backjump) xs) = Step x (proc (Just (n - 1)) xs)
proc mbj' (Step x xs) = Step x (proc mbj' xs)
-- Sets the conflict set from the first backjump as the final error, and records
-- whether the search was exhaustive.
useFirstError :: Progress Message (Bool, ConflictSet QPN, ConflictMap) b
-> Progress Message (Bool, ConflictSet QPN, ConflictMap) b
-- Sets the conflict set from the first backjump as the final error in case of a
-- non-exhaustive search.
useFirstError :: Progress Message (Exhaustive, ConflictSet QPN, ConflictMap) b
-> Progress Message (Exhaustive, ConflictSet QPN, ConflictMap) b
useFirstError = replace Nothing
where
replace _ (Done x) = Done x
replace cs' (Fail (exh, cs, cm)) = -- 'Nothing' means backjump limit not reached.
replace _ (Fail (Exhaustive, cs, cm)) = Fail (Exhaustive, cs, cm)
replace cs' (Fail (NotExhaustive, cs, cm)) = -- Backjump limit not reached.
-- Prefer first error over later error.
Fail (exh, if exh then cs else fromMaybe cs cs', cm)
Fail (NotExhaustive, fromMaybe cs cs', cm)
replace Nothing (Step x@(Failure cs Backjump) xs) = Step x $ replace (Just cs) xs
replace cs' (Step x xs) = Step x $ replace cs' xs
......@@ -71,16 +74,19 @@ logToProgress mbj l = let
-- exhaustiveness and first conflict set.
go :: Progress Message a b
-> Progress Message a b
-> Progress String (Bool, ConflictSet QPN, ConflictMap) b
-> Progress String (Exhaustive, ConflictSet QPN, ConflictMap) b
-> Progress String String b
go ms (Step _ ns) (Step x xs) = Step x (go ms ns xs)
go ms r (Step x xs) = Step x (go ms r xs)
go ms _ (Fail (exh, cs, cm)) = Fail $ "Could not resolve dependencies:\n" ++ if exh
then "Dependency tree exhaustively searched.\n" ++
"Final conflict set is: " ++ CS.showCSWithFrequency cm cs
else unlines (messages $ showMessages (L.foldr (\ v _ -> v `CS.member` cs) True) False ms) ++
"Backjump limit reached (" ++ currlimit mbj ++
"change with --max-backjumps or try to run with --reorder-goals).\n"
where currlimit (Just n) = "currently " ++ show n ++ ", "
currlimit Nothing = ""
go ms _ (Fail (exh, cs, cm)) = Fail $
"Could not resolve dependencies:\n" ++ case exh of
Exhaustive ->
"Dependency tree exhaustively searched.\n" ++
"Final conflict set is: " ++ CS.showCSWithFrequency cm cs
NotExhaustive ->
unlines (messages $ showMessages (L.foldr (\ v _ -> v `CS.member` cs) True) False ms) ++
"Backjump limit reached (" ++ currlimit mbj ++
"change with --max-backjumps or try to run with --reorder-goals).\n"
where currlimit (Just n) = "currently " ++ show n ++ ", "
currlimit Nothing = ""
go _ _ (Done s) = Done s
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment