pubgrub (empty) → 0.1.0.0

raw patch · 29 files changed

+4684/−0 lines, 29 filesdep +basedep +co-log-coredep +containers

Dependencies added: base, co-log-core, containers, tasty, tasty-hunit, tasty-quickcheck, text

Files

• CHANGELOG.md +17/−0
• LICENSE +26/−0
• README.md +46/−0
• pubgrub.cabal +111/−0
• src/PubGrub.hs +111/−0
• src/PubGrub/Cookbook.hs +403/−0
• src/PubGrub/Derivation.hs +173/−0
• src/PubGrub/Incompatibility.hs +268/−0
• src/PubGrub/PartialSolution.hs +224/−0
• src/PubGrub/Pretty.hs +42/−0
• src/PubGrub/Provider.hs +58/−0
• src/PubGrub/Relation.hs +85/−0
• src/PubGrub/Report.hs +327/−0
• src/PubGrub/SetOps.hs +85/−0
• src/PubGrub/Solver.hs +482/−0
• src/PubGrub/Store.hs +250/−0
• src/PubGrub/Term.hs +181/−0
• src/PubGrub/Tutorial.hs +312/−0
• src/PubGrub/Version.hs +66/−0
• src/PubGrub/VersionSet.hs +411/−0
• test/Cookbook.hs +171/−0
• test/CookbookSpec.hs +67/−0
• test/DocCode.hs +50/−0
• test/Main.hs +11/−0
• test/PartialSolutionSpec.hs +265/−0
• test/RelationSpec.hs +27/−0
• test/StoreInvariantsSpec.hs +176/−0
• test/Toy.hs +90/−0
• test/ToyDomainSpec.hs +149/−0

@@ -0,0 +1,17 @@+# Changelog++All notable changes to this project will be documented in this file.++The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/),+and versions follow the [Haskell PVP](https://pvp.haskell.org/), as described in+[CONTRIBUTING.md](https://github.com/tweag/pubgrub-hs/blob/main/CONTRIBUTING.md).+Every package of the repository has the version of the release; a package's own+changelog lists the changes under its directory.++## [0.1.0.0] - 2026-11-06++First release.++[0.1.0.0]: https://github.com/tweag/pubgrub-hs/releases/tag/v0.1.0.0++<!-- generated by git-cliff -->

@@ -0,0 +1,26 @@+Copyright 2026 Tweag I/O by Modus Create++Redistribution and use in source and binary forms, with or without modification,+are permitted provided that the following conditions are met:++1. Redistributions of source code must retain the above copyright notice, this+list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright notice,+this list of conditions and the following disclaimer in the documentation and/or+other materials provided with the distribution.++3. Neither the name of the copyright holder nor the names of its contributors+may be used to endorse or promote products derived from this software without+specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS “AS IS”+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,46 @@+# pubgrub++[PubGrub][] is a version-solving algorithm. Given a request and a way to read+what each version of each package needs, it finds a version for every package+the request needs, or proves that there is none, and the proof can be written+out for a person to read:++```+1. Because lib 1 depends on util 1 and util has no version 1, lib 1 is forbidden.++Because util has no version 2 and lib 2 depends on util 2, lib 2 is forbidden.+And because lib 1 is forbidden (1), lib 1 or 2 is forbidden.+So, because app 1 depends on lib 1 or 2 and app 1 is requested, version solving failed.+```++This package implements it in Haskell, once, for any domain: the things being+solved for need not be packages, and their values need not be versions. You+describe the domain with a type class, answer the solver's questions with a+callback, and choose the words its explanations use.++## Using it++Add `pubgrub` to your package's `build-depends`, and `import PubGrub`.++## Documentation++The documentation is in the package's modules:++- **[`PubGrub.Tutorial`][tutorial]** — start here. It builds a small domain,+  solves in it, breaks it, and explains the failure. The proof above is its+  output.+- **[`PubGrub.Cookbook`][cookbook]** — how-to guides: versions and ranges,+  requests and constraints, a provider over an index of releases, merging+  facts that say the same thing, explanations in your own words, watching the+  search, releasing a lock.+- **[`PubGrub`][front]** — how the solver sees a problem, and the reference+  for everything the library exports.++The domain of Haskell packages, over Cabal's package descriptions, is the+[`pubgrub-cabal`][cabal] package.++[PubGrub]: https://github.com/dart-lang/pub/blob/master/doc/solver.md+[tutorial]: https://hackage.haskell.org/package/pubgrub/docs/PubGrub-Tutorial.html+[cookbook]: https://hackage.haskell.org/package/pubgrub/docs/PubGrub-Cookbook.html+[front]: https://hackage.haskell.org/package/pubgrub/docs/PubGrub.html+[cabal]: https://hackage.haskell.org/package/pubgrub-cabal

@@ -0,0 +1,111 @@+cabal-version:      3.0+name:               pubgrub+version:            0.1.0.0+synopsis:           The PubGrub version solver+description:+    PubGrub is a version-solving algorithm: unit propagation with+    conflict-driven learning, and, when there is no solution, a proof of why+    that can be written out for a person to read.++    This is a Haskell implementation that is generic over the domain. A type class+    says what the variables, values, sets of values and facts are; a callback+    answers the solver's questions one variable at a time; and the explanation+    of a failure is worded by the domain.++    Start with the tutorial in "PubGrub.Tutorial". "PubGrub.Cookbook" has+    how-to guides, and "PubGrub" explains the model and re-exports what a user+    normally needs. The domain of Haskell packages is the @pubgrub-cabal@+    package.+category:           Distribution+license:            BSD-3-Clause+license-file:       LICENSE+author:             Andrea Bedini+maintainer:         andrea.bedini@moduscreate.com+copyright:          (c) 2026 Tweag I/O by Modus Create+homepage:           https://github.com/tweag/pubgrub-hs+bug-reports:        https://github.com/tweag/pubgrub-hs/issues+build-type:         Simple+tested-with:        GHC ==9.10.3 || ==9.12.2 || ==9.14.1+extra-doc-files:+    CHANGELOG.md+    README.md++source-repository head+    type:     git+    location: https://github.com/tweag/pubgrub-hs.git+    subdir:   pubgrub++common warnings+    ghc-options: -Wall++common language+    default-language:   GHC2021+    default-extensions: ImportQualifiedPost++library+    import:          warnings, language+    hs-source-dirs:  src+    exposed-modules:+        PubGrub+        PubGrub.Cookbook+        PubGrub.Derivation+        PubGrub.Incompatibility+        PubGrub.Pretty+        PubGrub.Provider+        PubGrub.Report+        PubGrub.SetOps+        PubGrub.Solver+        PubGrub.Term+        PubGrub.Tutorial+        PubGrub.Version+        PubGrub.VersionSet+    other-modules:+        PubGrub.PartialSolution+        PubGrub.Relation+        PubGrub.Store+    build-depends:+        , base        >=4.20  && <4.23+        , co-log-core >=0.3.2 && <0.4+        , containers  >=0.7   && <0.9+        , text        >=2.1   && <2.2++-- The suite compiles the library's sources itself rather than depending on+-- it, so that it can test the modules the library does not expose.+test-suite pubgrub-test+    import:         warnings, language+    type:           exitcode-stdio-1.0+    hs-source-dirs: src test+    main-is:        Main.hs+    other-modules:+        Cookbook+        CookbookSpec+        DocCode+        PartialSolutionSpec+        PubGrub+        PubGrub.Cookbook+        PubGrub.Derivation+        PubGrub.Incompatibility+        PubGrub.PartialSolution+        PubGrub.Pretty+        PubGrub.Provider+        PubGrub.Relation+        PubGrub.Report+        PubGrub.SetOps+        PubGrub.Solver+        PubGrub.Store+        PubGrub.Term+        PubGrub.Tutorial+        PubGrub.Version+        PubGrub.VersionSet+        RelationSpec+        StoreInvariantsSpec+        Toy+        ToyDomainSpec+    build-depends:+        , base             >=4.20  && <4.23+        , co-log-core      >=0.3.2 && <0.4+        , containers       >=0.7   && <0.9+        , tasty            >=1.5   && <1.6+        , tasty-hunit      >=0.10  && <0.11+        , tasty-quickcheck >=0.11  && <0.12+        , text             >=2.1   && <2.2

@@ -0,0 +1,111 @@+-- | PubGrub is a version-solving algorithm. Given a set of requests, it finds+-- a value for every variable they need or explains why there is no such choice.+-- This module re-exports what a user of the library normally needs.+--+-- = Where to start+--+-- * To learn the library by building something with it, follow+--   "PubGrub.Tutorial".+-- * For a task in hand (versions and ranges, requests and constraints, a+--   provider over an index, merging facts, explanations in a domain's words,+--   watching the search, releasing a lock), see the recipes in+--   "PubGrub.Cookbook".+-- * For what each name means, read on: the sections below are the reference,+--   and the modules they come from say more.+--+-- = How the solver sees a problem+--+-- A /domain/ says what the solver is solving over ('Domain'): the variables,+-- the values each can take, sets of values, and the facts it can be told. In a+-- package manager the variables are packages and the values their versions,+-- but nothing in the solver depends on that.+--+-- All the solver knows is a collection of /incompatibilities/: sets of+-- /terms/, one per variable, that cannot all be true. A term says something+-- about one variable's value: @'Positive' s@, it has a value in the set @s@;+-- @'Negative' s@, it has none in @s@, or no value at all. A request, a+-- dependency and a conflict are all incompatibilities ("PubGrub.Incompatibility"+-- lists their shapes).+--+-- A solve starts from the request, a list of incompatibilities marked as+-- seeds, and repeats two steps. /Propagation/ derives from the+-- incompatibilities what each variable must or must not be. When it has+-- nothing more to derive, a /decision/ takes a variable that must have a value+-- and has none, and asks the provider for one ('expand'); it answers with a+-- value and with the incompatibilities that value brings, its dependencies+-- for instance, and the search goes on. The world is read one variable at a+-- time, only as far as the search reaches.+--+-- When the incompatibilities rule out what has been decided, there is a+-- /conflict/. The solver does not just undo the last decision: by resolving+-- incompatibilities against each other it derives a new one that says why the+-- conflict happened, keeps it, and goes back to the point where the new+-- incompatibility forces a different choice. What it learned is never+-- forgotten, so the search does not walk into the same conflict twice.+--+-- Every derived incompatibility remembers the two it came from. When a+-- conflict rests on the seeds alone, no decision can be undone to avoid it, and+-- the solve fails. The incompatibility it ends with is the root of a tree of+-- reasoning whose leaves are the facts the solver was given or found: the proof+-- that there is no solution. "PubGrub.Derivation" reads that tree, and+-- "PubGrub.Report" writes it out as sentences that the domain words.+--+-- = Modules+--+-- * "PubGrub.Incompatibility": the domain, incompatibilities and their causes.+-- * "PubGrub.Term" and "PubGrub.SetOps": terms, and the set operations a+--   domain's sets provide. The class is re-exported here and its methods are+--   not, since @empty@, @union@ and @intersect@ are names every other set+--   library uses too: code that writes an instance or combines sets imports+--   "PubGrub.SetOps" for them.+-- * "PubGrub.Provider": the provider and its contract.+-- * "PubGrub.Solver": 'solve'.+-- * "PubGrub.Derivation" and "PubGrub.Report": reading a failure, and writing+--   it out.+-- * "PubGrub.Version", "PubGrub.VersionSet" and "PubGrub.Pretty": values and+--   sets for a domain whose values are versions, and their rendering.+--+-- The domain of Haskell packages is the @pubgrub-cabal@ package.+module PubGrub+    ( -- * The domain+      Domain (..)+    , MergeRule (..)+    , noMerging+      -- * Terms and incompatibilities+    , SetOps+    , module PubGrub.Term+    , Incompatibility (..)+    , Cause (..)+    , incompGet+    , noValues+    , isSeed+    , incompatibility+    , seed+    , fact+      -- * The provider+    , Provider (..)+      -- * Solving+    , solve+    , SolveError (..)+    , SolverMsg (..)+      -- * Reading a failure+    , module PubGrub.Derivation+    , module PubGrub.Report+      -- * Rendering+    , Pretty (..)+      -- * Versions+    , module PubGrub.Version+    , module PubGrub.VersionSet+    ) where++import           PubGrub.Derivation+import           PubGrub.Incompatibility+import           PubGrub.Pretty+import           PubGrub.Provider+import           PubGrub.Report+import           PubGrub.SetOps          (SetOps)+import           PubGrub.Solver          (SolveError (..), SolverMsg (..),+                                          solve)+import           PubGrub.Term+import           PubGrub.Version+import           PubGrub.VersionSet

@@ -0,0 +1,403 @@+{-# OPTIONS_GHC -Wno-unused-imports #-}++-- | How-to guides: recipes for the tasks a user of the library meets. They+-- assume the terms of "PubGrub.Tutorial"; "PubGrub" explains the model, and+-- each module documents its names.+--+-- The recipes share one example: a domain of packages with versions and+-- ranges, an index of releases, and a provider over it. Their code is one+-- module, @Cookbook.hs@, which the recipes build up in order: each uses only+-- what the recipes before it added, so the module compiles after every one of+-- them, and a GHCi session at the end of a recipe runs on what there is so+-- far. It needs @pubgrub@, @containers@, @text@ and @co-log-core@, and starts+-- with every import the recipes will use:+--+-- > {-# LANGUAGE OverloadedStrings #-}+-- > {-# LANGUAGE TypeFamilies      #-}+-- >+-- > module Cookbook where+-- >+-- > import           Colog.Core            (LogAction (..))+-- > import           Control.Monad         (guard)+-- > import           Data.Functor.Identity (Identity (..))+-- > import           Data.List             (find, sortOn)+-- > import           Data.Map.Strict       (Map)+-- > import qualified Data.Map.Strict       as Map+-- > import           Data.Maybe            (isJust)+-- > import           Data.Ord              (Down (..))+-- > import           Data.Semigroup        (First (..))+-- > import qualified Data.Set              as Set+-- > import           Data.Text             (Text)+-- > import qualified Data.Text             as T+-- > import           PubGrub+-- > import           PubGrub.SetOps        (isSubsetOf)+module PubGrub.Cookbook+    ( -- * How to give a domain versions and ranges+      -- $versions++      -- * How to request a package, or constrain one without requesting it+      -- $requests++      -- * How to write a provider over an index of releases+      -- $provider++      -- * How to merge facts that say the same thing+      -- $merging++      -- * How to explain a failure in your domain's words+      -- $explaining++      -- * How to watch the search+      -- $watching++      -- * How to find what to release from a lock after a failure+      -- $unlocking+    ) where++import           PubGrub++-- $versions+--+-- When a variable's values are versions, use 'Version' for the values and+-- 'VersionSet' for the sets: ranges of versions, built from bounds. Make the+-- variable type an instance of 'Domain', naming the types of its values, sets+-- and facts, and give 'singleton':+--+-- > newtype Name = Name Text+-- >     deriving (Eq, Ord, Show)+-- >+-- > data Said+-- >     = Requested Name VersionSet+-- >     | Constrained Name VersionSet+-- >     | DependsOn Name VersionSet Name VersionSet+-- >     | Unusable Name VersionSet Text+-- >+-- >+-- > instance Domain Name where+-- >     type ValueOf Name = Version+-- >     type SetOf Name = VersionSet+-- >     type FactOf Name = Said+-- >     singleton _ = singletonVersionSet+--+-- The fact type is what explanations are made from: give it one constructor+-- per kind of fact the request and the provider state, carrying what a sentence+-- about it needs. The four constructors here are the four kinds of fact the+-- recipes state. A domain can also say which facts merge, which is one more line+-- in this instance; [How to merge facts that say the same thing](#g:4) adds it.+--+-- Build ranges from their bounds. @'halfOpenVersionSet' lo ('Just' hi)@ is+-- @>=lo && \<hi@, and 'aboveVersionSet', 'belowVersionSet',+-- 'singletonVersionSet' and the 'SetOps' operations make the rest. The recipes+-- write their ranges with this:+--+-- > range :: [Int] -> [Int] -> VersionSet+-- > range lo hi = halfOpenVersionSet (mkVersion lo) (Just (mkVersion hi))+--+-- A set built from a range someone wrote can keep their spelling for+-- explanations: 'declare' tags it, and 'pretty' prints the tag rather than+-- the canonical form.++-- $requests+--+-- The request is a list of seeds: incompatibilities of one term, built with+-- 'seed' from what the request said. To require a package to have a version+-- in a set, state that its having none there is impossible, with a 'Negative'+-- term:+--+-- > request :: Name -> VersionSet -> Incompatibility Name+-- > request p s = seed (Requested p s) p (Negative s)+--+-- To constrain a package without requiring it, so that /if/ it is in the plan+-- its version is in a range, forbid the versions outside the range with a+-- 'Positive' term. Sets need not have a complement, so a constraint is stated+-- through what it forbids; a version set has one, 'complementVersionSet':+--+-- > constrain :: Name -> VersionSet -> Incompatibility Name+-- > constrain p allowed = seed (Constrained p allowed) p (Positive (complementVersionSet allowed))+--+-- Give both to 'solve' in one list. A constraint narrows the choice for a+-- package the plan needs, and does not bring into the plan a package nothing+-- requires. A conflict among the seeds alone ends the solve, and the+-- explanation ends with the requests and constraints it rests on. The next+-- recipe solves with both.++-- $provider+--+-- A provider is asked about one package at a time: here are the versions it may+-- still have, pick one and say what it needs. Over an index of releases,+-- describe each release by what it needs and whether it can be used:+--+-- > data Release = Release+-- >     { needs  :: [(Name, VersionSet)]+-- >     , broken :: Maybe Text+-- >     }+-- >+-- > type Index = Map Name [(Version, Release)]+--+-- State each dependency over the release's /slot/ rather than over its version+-- alone: the range from its version up to the next release in the index, and+-- for the first release everything up to the next one, since nothing is+-- published below it. A slot holds the same releases as the version, but the+-- slots of neighbouring releases touch, so facts over them can merge into one+-- (the next recipe), and a proof says @lib \<2@ rather than+-- @lib >=1 && \<2@ of a first release:+--+-- > slot :: [Version] -> Version -> VersionSet+-- > slot versions x+-- >     | all (>= x) versions = belowVersionSet next+-- >     | otherwise = halfOpenVersionSet x next+-- >   where+-- >     next = find (> x) versions+-- >+-- > dependsOn :: Name -> VersionSet -> Name -> VersionSet -> Incompatibility Name+-- > dependsOn p ps q qs = fact (DependsOn p ps q qs) [(p, Positive ps), (q, Negative qs)]+--+-- Pick the newest release the offered set admits; the answer must be in the+-- set. When releases are passed over because they cannot be used, say why, with+-- a fact over each one's slot: the solver keeps the facts, and an explanation+-- then names the reason rather than saying that no version exists. If no+-- release is left, answer 'Nothing', still with the reasons:+--+-- > provider :: Index -> Provider Name Identity+-- > provider index = Provider $ \p offered ->+-- >     let releases = Map.findWithDefault [] p index+-- >         versions = map fst releases+-- >         newestFirst = sortOn (Down . fst) [r | r@(x, _) <- releases, offered `contains` x]+-- >         (unusable, usable) = span (isJust . broken . snd) newestFirst+-- >         reasons =+-- >             [ fact (Unusable p (slot versions x) reason) [(p, Positive (slot versions x))]+-- >             | (x, Release{broken = Just reason}) <- unusable+-- >             ]+-- >      in Identity $ case usable of+-- >             (x, release) : _ -> (Just x, reasons ++ [dependsOn p (slot versions x) q qs | (q, qs) <- needs release])+-- >             []               -> (Nothing, reasons)+--+-- An example index, and a function that solves over one:+--+-- > app, lib, util, extra :: Name+-- > app = Name "app"+-- > lib = Name "lib"+-- > util = Name "util"+-- > extra = Name "extra"+-- >+-- > example :: Index+-- > example =+-- >     Map.fromList+-- >         [ (app, [(mkVersion [1], Release [(lib, range [1] [2, 1])] Nothing)])+-- >         , ( lib+-- >           , [ (mkVersion [1], Release [(util, range [1] [3])] Nothing)+-- >             , (mkVersion [2], Release [(util, range [1] [3])] Nothing)+-- >             , (mkVersion [2, 1], Release [] (Just "it does not build here"))+-- >             ]+-- >           )+-- >         , (util, [(mkVersion [1], Release [] Nothing), (mkVersion [2], Release [] Nothing)])+-- >         , (extra, [(mkVersion [1], Release [] Nothing), (mkVersion [2], Release [] Nothing)])+-- >         ]+-- >+-- > plan :: Index -> [Incompatibility Name] -> Maybe (Map Name Version)+-- > plan index seeds = case runIdentity (solve mempty (provider index) seeds) of+-- >     Right solution -> Just solution+-- >     Left _         -> Nothing+--+-- A request alone, then with a constraint on a package the plan needs, then+-- with one on a package nothing requires:+--+-- @+-- ghci> plan example [request app fullVersionSet]+-- Just (fromList [(Name \"app\",mkVersion [1]),(Name \"lib\",mkVersion [2]),(Name \"util\",mkVersion [2])])+-- ghci> plan example [request app fullVersionSet, constrain util (range [1] [2])]+-- Just (fromList [(Name \"app\",mkVersion [1]),(Name \"lib\",mkVersion [2]),(Name \"util\",mkVersion [1])])+-- ghci> plan example [request app fullVersionSet, constrain extra (range [2] [3])]+-- Just (fromList [(Name \"app\",mkVersion [1]),(Name \"lib\",mkVersion [2]),(Name \"util\",mkVersion [2])])+-- @+--+-- This provider runs in 'Data.Functor.Identity.Identity'. One that reads its+-- index from disk runs in 'IO', and so does 'solve' then.++-- $merging+--+-- A provider that states the same dependency for each of several releases gives+-- the solver several facts where one would do. A t'MergeRule' tells the solver+-- which incompatibilities can be stated as one: it splits each into a key and a+-- part, and those with the same key are merged as they arrive, their parts+-- combined with @<>@, which for a 'VersionSet' is union. Here, two dependencies+-- with the same depender and the same dependee range merge into one over both+-- depender ranges:+--+-- > sameDependency :: MergeRule Name+-- > sameDependency =+-- >     MergeRule+-- >         { mergeParts = \i -> case incompCause i of+-- >             Fact (DependsOn p ps q qs) -> Just ((p, q, qs), ps)+-- >             _                          -> Nothing+-- >         , mergeBuild = \(p, q, qs) ps -> dependsOn p ps q qs+-- >         }+--+-- Name the rule in the domain's instance, as 'mergeRule': add this line to the+-- @instance Domain Name@ of the first recipe, after 'singleton':+--+-- >     mergeRule = sameDependency+--+-- Check one thing. The merged fact replaces both, so it must say exactly what+-- the two said together; a union of depender ranges does, since \"@lib@ in @a@+-- or @b@ needs @util@ in @r@\" is both \"@lib@ in @a@ needs @util@ in @r@\" and+-- \"@lib@ in @b@ needs @util@ in @r@\".+--+-- The dependencies of @lib@ 1 and @lib@ 2 on @util@ are stated over their+-- slots, which touch, so the merged fact is one range:+--+-- @+-- ghci> let slotOf = slot (map fst (example Map.! lib))+-- ghci> pretty (slotOf (mkVersion [1]) <> slotOf (mkVersion [2]))+-- \"\<2.1\"+-- @+--+-- The plans of the previous recipe are the same with the rule as without it;+-- what it buys is a shorter search and, in the next recipe, a proof that+-- states the dependency once.+--+-- A domain whose facts do not merge still has a reason to name a rule. When the+-- solver backtracks and decides a variable again, the provider states that+-- value's facts again, and with no rule each is one more incompatibility to+-- judge. On a search that backtracks far and often, that can cost more than the+-- rest of the search: a synthetic problem took more than ten times as long. A+-- rule that keeps one incompatibility per set of terms stops it:+--+-- > sameTerms :: (Domain v, Ord (SetOf v)) => MergeRule v+-- > sameTerms =+-- >     MergeRule+-- >         { mergeParts = \i -> case incompCause i of+-- >             Fact _ -> Just (incompTerms i, First i)+-- >             _      -> Nothing+-- >         , mergeBuild = \_ (First i) -> i+-- >         }+--+-- It needs 'Ord' on the domain's sets. Two facts with the same terms forbid the+-- same thing, so keeping the first says all that both said. A rule like+-- @sameDependency@ already does this for the facts it merges, since a repeated+-- dependency merges with itself.++-- $explaining+--+-- When there is no plan, 'solve' answers with the incompatibility the proof+-- ends with, and 'reportConflict' writes the proof out in the sentences a+-- t'Formatter' gives it. 'mkFormatter' builds one from the domain's three+-- sentences: one for each kind of fact, one for the solver's finding that a+-- package has no version in a set, and how to name a package with a set of+-- versions, from which 'summaryWith' makes the conclusions. Its other fields+-- hold rules of your own, set by record update ("PubGrub.Report" describes+-- them). This domain sets 'clauseRules', below:+--+-- > name :: Name -> VersionSet -> Text+-- > name (Name p) s = p <> " " <> pretty s+-- >+-- > formatter :: Formatter Name+-- > formatter = (mkFormatter says hole name){clauseRules = [whichDependsOn]}+-- >   where+-- >     says said _ = case said of+-- >         Requested p s       -> name p s <> " is requested"+-- >         Constrained p s     -> name p s <> " is required by a constraint"+-- >         DependsOn p ps q qs -> name p ps <> " depends on " <> name q qs+-- >         Unusable p s reason -> name p s <> " cannot be used: " <> reason+-- >     hole p s = "no version of " <> name p s <> " exists"+--+-- A sentence is a fragment: no capital letter, no full stop, and no leading+-- \"because\" or \"and\", since the proof adds its own connectives. The second+-- argument of @says@, ignored here, is the incompatibility the fact is the+-- cause of, for a sentence that depends on which of its terms survived.+--+-- A clause rule says two facts as one premise where that reads better. This one+-- writes \"a depends on b which depends on c\" rather than naming @b@ twice. It+-- fires only when the second fact covers every version of @b@ the first one+-- names, so the sentence stays true. 'Rule', 'symmetric' and 'asFact' come from+-- "PubGrub.Derivation":+--+-- > whichDependsOn :: Rule (Incompatibility Name, Incompatibility Name) Text+-- > whichDependsOn = symmetric $ \(first, second) -> do+-- >     DependsOn p ps q qs <- asFact first+-- >     DependsOn q' qs' r rs <- asFact second+-- >     guard (q == q' && qs `isSubsetOf` qs')+-- >     pure (name p ps <> " depends on " <> name q qs <> " which depends on " <> name r rs)+--+-- Then render a failure. Any 'Left' other than 'NoSolution' is a bug, in the+-- seeds, in the provider or in the solver, not a verdict on the index:+--+-- > why :: Index -> [Incompatibility Name] -> Text+-- > why index seeds = case runIdentity (solve mempty (provider index) seeds) of+-- >     Right _                -> "There is a plan."+-- >     Left (NoSolution root) -> reportConflict formatter root+-- >     Left _                 -> "The solver failed unexpectedly."+--+-- @+-- ghci> import qualified Data.Text.IO as T+-- ghci> T.putStrLn (why example [request app fullVersionSet, constrain util (range [3] [4])])+-- Because app >=0 depends on lib >=1 && \<2.1 which depends on util >=1 && \<3, app >=0 requires util >=1 && \<3.+-- So, because app >=0 is requested and util >=3 && \<4 is required by a constraint, version solving failed.+-- ghci> T.putStrLn (why example [request lib (singletonVersionSet (mkVersion [2, 1]))])+-- So, because lib >=2.1 cannot be used: it does not build here and lib ==2.1 is requested, version solving failed.+-- @+--+-- The first proof names the dependency of @lib@ on @util@ once: the merged+-- fact of the previous recipe covers @lib@ 1 and @lib@ 2 together, and the+-- clause rule joins it to @app@'s dependency on @lib@.++-- $watching+--+-- 'solve' sends a 'SolverMsg' for each step of the search to the @LogAction@ it+-- is given, from co-log-core, and the provider runs in the same monad. To print+-- the steps, solve in 'IO' with @LogAction (mapM_ T.putStrLn . describe)@. To+-- collect them, solve in a monad that can, such as a pair with a list, and lift+-- the provider into it:+--+-- > searchLog :: Index -> [Incompatibility Name] -> [Text]+-- > searchLog index seeds = fst (solve logger (Provider expandLogged) seeds)+-- >   where+-- >     logger = LogAction $ \msg -> (describe msg, ())+-- >     expandLogged p s = ([], runIdentity (expand (provider index) p s))+-- >+-- > describe :: SolverMsg Name -> [Text]+-- > describe msg = case msg of+-- >     Chose (Name p) x            -> [p <> " " <> pretty x]+-- >     NoVersionFor (Name p) s     -> ["no " <> p <> " in " <> pretty s]+-- >     Learned i                   -> ["learned: " <> sayTerms formatter (incompTerms i)]+-- >     Backtracked level           -> ["back to level " <> T.pack (show level)]+-- >     _                           -> []+--+-- @+-- ghci> mapM_ T.putStrLn (searchLog example [request app fullVersionSet, constrain util (range [3] [4])])+-- app 1+-- lib 2+-- learned: lib >=2 && \<2.1 requires util >=1 && \<3+-- back to level 1+-- lib 1+-- @+--+-- Each @learned@ line is an incompatibility the solver derived from a conflict+-- and keeps; each @back to@ line is the backtrack that followed it.++-- $unlocking+--+-- A planner that holds packages at the versions a lock file names states each as+-- a constraint. When the solve fails, 'conflictSet' gives every package that took+-- part in the failure. A held package outside it played no part, and stays held;+-- release the held packages inside it, and solve again:+--+-- > solveWithLock :: Index -> Map Name Version -> [Incompatibility Name] -> Either (SolveError Name) (Map Name Version)+-- > solveWithLock index lock requests = case attempt lock of+-- >     Left (NoSolution root)+-- >         | let involved = Map.keysSet lock `Set.intersection` conflictSet root+-- >         , not (Set.null involved) ->+-- >             attempt (Map.withoutKeys lock involved)+-- >     result -> result+-- >   where+-- >     attempt held =+-- >         runIdentity . solve mempty (provider index) $+-- >             requests ++ [constrain p (singletonVersionSet x) | (p, x) <- Map.toList held]+--+-- Here the lock holds @util@ and @extra@ at 1, and the request now asks for+-- @util >=2 && \<3@. @util@ is released and @extra@ stays at 1:+--+-- @+-- ghci> either (const Nothing) Just (solveWithLock example (Map.fromList [(util, mkVersion [1]), (extra, mkVersion [1])]) [request app fullVersionSet, request util (range [2] [3]), request extra fullVersionSet])+-- Just (fromList [(Name \"app\",mkVersion [1]),(Name \"extra\",mkVersion [1]),(Name \"lib\",mkVersion [2]),(Name \"util\",mkVersion [2])])+-- @

@@ -0,0 +1,173 @@+-- | Reading a derivation: views of the tree a failed solve hands back, over+-- any 'Domain'.+--+-- The incompatibility a failed solve ends with carries the derivation that+-- produced it ('PubGrub.Incompatibility.Cause'): a tree whose leaves are+-- external facts and whose nodes each follow from their two children.+-- Everything here reads that shape and nothing inside a fact; what a leaf+-- /says/ is the domain's business.+--+-- The views are 'Rule's, functions that may decline, so that they compose in+-- one @do@ block in 'Maybe' with a renderer's own rules ("PubGrub.Report"): a+-- line reads a view, states a guard, and says a sentence.+module PubGrub.Derivation+    ( -- * Rules+      Rule+    , firstOf+    , symmetric+      -- * Views of a node+    , isDerived+    , derivedFrom+    , bothExternal+    , bothDerived+    , chainStep+      -- * Views of a leaf+    , asFact+    , asSeed+    , asNoValues+      -- * Walks+    , externals+    , everywhere+    , nearestRoot+    , runWhile+    , conflictSet+    ) where++import           Control.Applicative     ((<|>))+import           Control.Monad           (guard)+import           Data.Foldable           (asum)+import           Data.List               (minimumBy)+import qualified Data.Map.Strict         as Map+import           Data.Ord                (comparing)+import           Data.Set                (Set)+import qualified Data.Set                as Set+import           PubGrub.Incompatibility (Cause (..), Domain (..),+                                          Incompatibility (..))++-- | A rule reads an @a@ and either fires with a @b@ or declines.+type Rule a b = a -> Maybe b++-- | The first rule of the table that fires.+firstOf :: [Rule a b] -> Rule a b+firstOf rules x = asum [rule x | rule <- rules]++-- | A rule over a pair, tried both ways round: as given first.+symmetric :: Rule (a, a) b -> Rule (a, a) b+symmetric rule (x, y) = rule (x, y) <|> rule (y, x)++-- --------------------------------------------------------------------------+-- Views of a node+-- --------------------------------------------------------------------------++-- | Was this derived by the solver, rather than stated?+isDerived :: Incompatibility v -> Bool+isDerived c = case incompCause c of+    Derived _ _ -> True+    _           -> False++-- | The two causes of a derived step, in the order the solver joined them.+derivedFrom :: Rule (Incompatibility v) (Incompatibility v, Incompatibility v)+derivedFrom inc = case incompCause inc of+    Derived a b -> Just (a, b)+    _           -> Nothing++-- | A step whose causes are both external facts: the only kind of step that+-- opens a line of derivation.+bothExternal :: Rule (Incompatibility v) (Incompatibility v, Incompatibility v)+bothExternal inc = do+    (a, b) <- derivedFrom inc+    guard (not (isDerived a) && not (isDerived b))+    pure (a, b)++-- | A step whose causes are both derived: where the derivation branches.+bothDerived :: Rule (Incompatibility v) (Incompatibility v, Incompatibility v)+bothDerived inc = do+    (a, b) <- derivedFrom inc+    guard (isDerived a && isDerived b)+    pure (a, b)++-- | A step with one derived cause and one external fact, the derived cause+-- first: the step a linear chain is made of and the step every run walks.+chainStep :: Rule (Incompatibility v) (Incompatibility v, Incompatibility v)+chainStep inc = do+    (a, b) <- derivedFrom inc+    case (isDerived a, isDerived b) of+        (True, False) -> Just (a, b)+        (False, True) -> Just (b, a)+        _             -> Nothing++-- --------------------------------------------------------------------------+-- Views of a leaf+-- --------------------------------------------------------------------------++-- | The domain's fact at a leaf, whether it was a seed or stated by the+-- provider.+asFact :: Rule (Incompatibility v) (FactOf v)+asFact c = case incompCause c of+    Seed f -> Just f+    Fact f -> Just f+    _      -> Nothing++-- | A seed: what the solve was asked for.+asSeed :: Rule (Incompatibility v) (FactOf v)+asSeed c = case incompCause c of+    Seed f -> Just f+    _      -> Nothing++-- | A hole: a set of a variable's values the solver found nothing in.+asNoValues :: Rule (Incompatibility v) (v, SetOf v)+asNoValues c = case incompCause c of+    NoValues v s -> Just (v, s)+    _            -> Nothing++-- --------------------------------------------------------------------------+-- Walks+-- --------------------------------------------------------------------------++-- | The external facts at the leaves, in proof order.+externals :: Incompatibility v -> [Incompatibility v]+externals inc = case derivedFrom inc of+    Just (a, b) -> externals a ++ externals b+    Nothing     -> [inc]++-- | Every node of the tree the rule fires on, with its depth below the root, in+-- proof order.+everywhere :: Rule (Incompatibility v) a -> Incompatibility v -> [(Int, a)]+everywhere rule = go 0+  where+    go depth n =+        [(depth, a) | Just a <- [rule n]] ++ case derivedFrom n of+            Just (a, b) -> go (depth + 1) a ++ go (depth + 1) b+            Nothing     -> []++-- | Of some nodes with their depth, the one nearest the root; the first in proof+-- order on a tie.+nearestRoot :: [(Int, a)] -> Maybe a+nearestRoot [] = Nothing+nearestRoot cs = Just (snd (minimumBy (comparing fst) cs))++-- | Walk down the spine of chain steps while the rule fires on each step's+-- external fact. Answers with the node where the walk stopped (the input+-- itself when there was no run, and otherwise a derived node, since the walk+-- only descends into a chain step's derived cause) and what the rule read off+-- each fact, deepest first. An empty list means there was no run.+runWhile :: Rule (Incompatibility v) a -> Incompatibility v -> (Incompatibility v, [a])+runWhile rule = go []+  where+    go acc node = case chainStep node of+        Just (d, e) | Just a <- rule e -> go (a : acc) d+        _                              -> (node, acc)++-- | Every variable a failed solve's derivation mentions: the terminal+-- incompatibility's own terms, and the terms of every incompatibility it was+-- derived from, down to the external facts at the leaves.+--+-- This is the __conflict set__: the variables on the path to the conflict as+-- well as those in it. A caller that solved with some variables held at+-- earlier values (a lock file, say) reads it to decide which to release before+-- solving again. A held variable that is not in the set took no part in the+-- failure, and releasing it cannot help.+conflictSet :: Domain v => Incompatibility v -> Set (v)+conflictSet inc = Map.keysSet (incompTerms inc) <> case incompCause inc of+    Derived a b -> conflictSet a <> conflictSet b+    _           -> Set.empty

@@ -0,0 +1,268 @@+{-# LANGUAGE DerivingStrategies   #-}+{-# LANGUAGE StandaloneDeriving   #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Incompatibilities, the solver's only kind of knowledge, and the 'Domain'+-- they are stated in.+--+-- The solver is written once, over a domain it knows only through 'Domain':+-- what a variable is, what its values and sets of values are, and what an+-- external fact says. Everything it is told, by the request and by the+-- provider, and everything it learns, is an t'Incompatibility'.+module PubGrub.Incompatibility+    ( -- * The domain+      Domain (..)+    , MergeRule (..)+    , noMerging+      -- * Incompatibilities+    , Incompatibility (..)+    , Cause (..)+    , incompGet+    , noValues+    , isSeed+      -- * Building one+    , incompatibility+    , seed+    , fact+      -- * Resolution+      -- | The step conflict resolution derives a new incompatibility with. A+      -- formatter's tests can build a derivation by hand with 'priorCause', and+      -- a formatter rule that says several steps in one line can check that it+      -- is sound by replaying them with 'priorCauseTerms'.+    , priorCause+    , priorCauseTerms+    ) where++import           Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import           Data.Void       (Void, absurd)+import           PubGrub.SetOps  (SetOps (..))+import           PubGrub.Term    (Term (..), anyTerm, intersectTerm, isTopTerm,+                                  unionTerm)++-- Specialised in the client, with the solver ("PubGrub.Solver" says why).+{-# INLINABLE incompGet #-}+{-# INLINABLE noValues #-}+{-# INLINABLE priorCause #-}+{-# INLINABLE priorCauseTerms #-}++-- --------------------------------------------------------------------------+-- Domain+-- --------------------------------------------------------------------------++-- | A problem domain: everything the solver needs to know about what it is+-- solving over, and nothing it does not. The solver compares variables with+-- 'Ord' and combines sets with 'SetOps'; what a variable, a value or a fact+-- /is/ never reaches it.+--+-- The instance is on the type of the /variables/, the things the solver+-- assigns values to, and that type names the domain everywhere: an+-- @t'Incompatibility' v@ is one over the domain whose variables are @v@. The+-- associated types say what a variable's values, its sets of values and the+-- facts about it are.+class (Ord v, SetOps (SetOf v)) => Domain v where+    -- | The values a variable takes.+    type ValueOf v+    -- | A set of values of one variable: what a 'Term' ranges over.+    type SetOf v+    -- | An external fact: what the domain knows about the world, recorded as+    -- the 'Cause' of the incompatibility that states it. The solver never reads+    -- it; it is what a failure is explained from.+    type FactOf v++    -- | The set holding exactly one value of the variable. The solver states+    -- a decision with it.+    singleton :: v -> ValueOf v -> SetOf v++    -- | Which incompatibilities can be stated as one, and the one that states+    -- them. The solver applies it as incompatibilities arrive. The default+    -- merges nothing.+    mergeRule :: MergeRule v+    mergeRule = noMerging++-- | A merge rule: it splits an incompatibility into a key and a part. Two with+-- the same key are one piece of knowledge in two parts, the parts combine with+-- @<>@, and 'mergeBuild' makes the one incompatibility that states the result.+-- The solver keeps at most one incompatibility per key: one that arrives with a+-- key already taken is merged into the one that has it, which keeps its place in+-- the order the solver judges them in. The two types are the rule's own.+--+-- Merging pays where a provider states a dependency once per release. If two+-- releases of @p@ both need @q@ in @r@, the solver is given one incompatibility+-- for each. Merged, they can propagate where neither part can: knowing only that+-- @p@ is one of the two releases, without knowing which, is enough to conclude+-- that @q@ is in @r@. A proof then states the dependency once.+--+-- __The law.__ The merged incompatibility replaces both, so it must say exactly+-- what the two say together: whenever @mergeParts a == Just (k, x)@ and+-- @mergeParts b == Just (k, y)@, @mergeBuild k (x <> y)@ forbids exactly what @a@+-- and @b@ forbid between them. 'Semigroup' cannot check this. Merging+-- @{p: Positive a, q: Negative r}@ with @{p: Positive b, q: Negative r}@ into+-- @{p: Positive (a ∪ b), q: Negative r}@ keeps it, because "@p@ in @a ∪ b@" is+-- "@p@ in @a@ or @p@ in @b@", so the key is @(p, q, r)@ and the part is the set+-- under union. Nothing else is required: a merge may change which variables the+-- incompatibility mentions.+data MergeRule v = forall k s. (Ord k, Semigroup s) => MergeRule+    { mergeParts :: Incompatibility v -> Maybe (k, s)+      -- ^ the key and the part of an incompatibility that may be merged, or+      -- 'Nothing' for one that is never merged+    , mergeBuild :: k -> s -> Incompatibility v+      -- ^ the incompatibility that states a key and a part: the key the first+      -- of them arrived with, and the @<>@ of their parts in the order they+      -- arrived+    }++-- | No two clauses merge, so a fact the provider states again, when the solver+-- decides a variable a second time, is a second clause. "PubGrub.Cookbook" has a+-- rule that stops that.+noMerging :: MergeRule v+noMerging = MergeRule{mergeParts = const (Nothing :: Maybe (Void, ())), mergeBuild = \k _ -> absurd k}++-- --------------------------------------------------------------------------+-- Incompatibility+-- --------------------------------------------------------------------------++-- | A set of terms, at most one per variable, that cannot /all/ be true in a+-- solution. Every fact the solver is given or learns has this shape:+--+-- @+-- {p: t, q: u}   means   not (t is true of p and u is true of q)+-- @+--+-- Read as an implication, it states the familiar facts. With @'Positive' s@+-- read as "has a value in @s@" and @'Negative' s@ as "has no value, or one+-- outside @s@":+--+--   * @{p: Negative s}@: @p@ must have a value, in @s@. A request, with+--     cause 'Seed'.+--   * @{p: Positive f}@: @p@ may not take a value in @f@. A constraint on the+--     request, with cause 'Seed', or the solver's own finding ('noValues').+--   * @{p: Positive s, q: Negative r}@: if @p@ has a value in @s@, then @q@+--     has a value in @r@. A dependency, with cause 'Fact'.+--   * @{p: Positive s, q: Positive r}@: @p@ in @s@ and @q@ in @r@ cannot both+--     be. A conflict, with cause 'Fact'.+--+-- A term that is always true ('PubGrub.Term.isTopTerm') says nothing, and is+-- left out. An incompatibility with a term that is never true+-- ('PubGrub.Term.isBottomTerm') can never be violated, and is not worth+-- stating. An incompatibility with no terms is always violated: it is what a+-- failed solve ends with.+--+-- Every incompatibility records why it holds, its 'Cause', which is what a+-- failure is explained from. The cause never changes what an incompatibility+-- means.+--+-- Build one with 'seed', 'fact' or 'incompatibility', which keep that shape;+-- the constructor is for taking one apart.+data Incompatibility v = Incompatibility+    { incompTerms :: Map (v) (Term (SetOf v))+    , incompCause :: Cause v+    }++-- | Why an incompatibility holds. It is either /external/, a fact the solver+-- was given or found, or /derived/ by the solver from two others. A failed+-- solve ends with an incompatibility whose causes form a tree: derived nodes,+-- with external facts at the leaves. That tree is the explanation of the+-- failure ("PubGrub.Derivation" reads it, "PubGrub.Report" writes it out), and+-- the domain supplies only what a leaf says ('FactOf').+--+-- A seed is kept apart from other facts because the solver treats it+-- specially: a conflict that rests on the seeds alone ends the search, since+-- no decision can be undone to avoid it.+data Cause v+    = Seed (FactOf v)+      -- ^ part of the request: what the solve was asked for, or a constraint+      -- on it+    | Fact (FactOf v)+      -- ^ a fact about the world, stated by the provider+    | NoValues (v) (SetOf v)+      -- ^ the solver's own fact: the provider had nothing to offer in this+      -- set of the variable's values ('noValues')+    | Derived (Incompatibility v) (Incompatibility v)+      -- ^ the resolvent of two incompatibilities, in the order 'priorCause'+      -- took them++-- The instances are structural, over the whole cause tree: two derived+-- incompatibilities are equal when their terms and their derivations are, and+-- 'show' prints the tree. They are what a test asserts with and what GHCi+-- prints; a report of a failure is "PubGrub.Report".+deriving stock instance (Eq (v), Eq (SetOf v), Eq (FactOf v)) => Eq (Incompatibility v)+deriving stock instance (Eq (v), Eq (SetOf v), Eq (FactOf v)) => Eq (Cause v)+deriving stock instance (Show (v), Show (SetOf v), Show (FactOf v)) => Show (Incompatibility v)+deriving stock instance (Show (v), Show (SetOf v), Show (FactOf v)) => Show (Cause v)++-- | The term an incompatibility states about @v@, if any.+incompGet :: Domain v => v -> Incompatibility v -> Maybe (Term (SetOf v))+incompGet v (Incompatibility m _) = Map.lookup v m++-- | @{v: Positive s}@, caused by 'NoValues': the variable takes no value in+-- @s@. The solver states it when the provider has no value to offer in @s@.+noValues :: Domain v => v -> SetOf v -> Incompatibility v+noValues v s = Incompatibility (Map.singleton v (Positive s)) (NoValues v s)++-- | Is this part of the request: is its cause a 'Seed'?+isSeed :: Incompatibility v -> Bool+isSeed i = case incompCause i of+    Seed _ -> True+    _      -> False++-- | An incompatibility from its cause and terms, in the shape the solver+-- expects: a variable named twice gets the intersection of its terms, and a+-- term that is always true is left out.+incompatibility :: Domain v => Cause v -> [(v, Term (SetOf v))] -> Incompatibility v+incompatibility cause terms =+    Incompatibility (Map.filter (not . isTopTerm) (Map.fromListWith intersectTerm terms)) cause++-- | A seed: one term about one variable, with what the request said as its+-- fact. @'Negative' s@ asks for the variable to have a value in @s@, and+-- @'Positive' f@ forbids it the values in @f@. 'PubGrub.Solver.solve' takes a+-- list of these, and a seed built here is always one it accepts.+seed :: FactOf v -> v -> Term (SetOf v) -> Incompatibility v+seed f v t = Incompatibility (Map.singleton v t) (Seed f)++-- | A fact the provider states, from what it says and its terms, in the shape+-- 'incompatibility' keeps.+fact :: Domain v => FactOf v -> [(v, Term (SetOf v))] -> Incompatibility v+fact f = incompatibility (Fact f)++-- | The rule of resolution: from two incompatibilities that both mention the+-- pivot variable, the one that follows from both. Its terms are+-- 'priorCauseTerms', and its cause is 'Derived' from the two, in this order.+priorCause+    :: Domain v+    => Incompatibility v+    -- ^ the incompatibility being resolved+    -> Incompatibility v+    -- ^ the incompatibility it is resolved with+    -> v+    -- ^ the pivot, which both mention+    -> Incompatibility v+priorCause current@(Incompatibility cur _) satCause@(Incompatibility sat _) pivot =+    Incompatibility (priorCauseTerms pivot cur sat) (Derived current satCause)++-- | The terms 'priorCause' arrives at: the union of the pivot's two terms,+-- the intersection of every other variable's, and no term for the pivot where+-- the union is always true.+priorCauseTerms+    :: Domain v+    => v+    -- ^ the pivot+    -> Map (v) (Term (SetOf v))+    -- ^ the terms of the incompatibility being resolved+    -> Map (v) (Term (SetOf v))+    -- ^ the terms of the one it is resolved with+    -> Map (v) (Term (SetOf v))+priorCauseTerms pivot cur sat = finalTerms+  where+    merged =+        Map.unionWith+            intersectTerm+            (Map.delete pivot cur)+            (Map.delete pivot sat)+    t1 = Map.findWithDefault anyTerm pivot cur+    t2 = Map.findWithDefault anyTerm pivot sat+    unioned = unionTerm t1 t2+    finalTerms+        | isTopTerm unioned = merged+        | otherwise = Map.insert pivot unioned merged

@@ -0,0 +1,224 @@+-- | The partial solution: every assignment the search has made, indexed by+-- variable so that each of the algorithm's questions about one variable is a+-- lookup rather than a scan.+module PubGrub.PartialSolution+    ( Assignment (..)+    , AssignmentKind (..)+    , assignmentTerm+    , decidedValue+    , VarAssignments (..)+    , PartialSolution (..)+    , emptyPS+    , addDecision+    , addDerivation+    , backtrack+    , termIntersectionFor+    , psRelation+    , extractSolution+    , undecidedPositive+    , varHistory+    ) where++import           Control.Applicative     ((<|>))+import           Data.Foldable           (Foldable (..))+import           Data.List               (sortOn)+import           Data.Map.Strict         (Map)+import qualified Data.Map.Strict         as Map+import           Data.Maybe              (mapMaybe)+import           Data.Sequence           (Seq)+import qualified Data.Sequence           as Seq+import           PubGrub.Incompatibility (Domain (..), Incompatibility (..),+                                          incompGet)+import           PubGrub.Relation        (IncompatRelation, incompRelation)+import           PubGrub.Term            (Term (..), anyTerm, intersectTerm,+                                          negateTerm)++-- Specialised in the client, with the solver ("PubGrub.Solver" says why).+{-# INLINABLE assignmentTerm #-}+{-# INLINABLE extendVar #-}+{-# INLINABLE fromHistory #-}+{-# INLINABLE recordAssignment #-}+{-# INLINABLE addDecision #-}+{-# INLINABLE addDerivation #-}+{-# INLINABLE backtrack #-}+{-# INLINABLE termIntersectionFor #-}+{-# INLINABLE psRelation #-}+{-# INLINABLE varHistory #-}++-- --------------------------------------------------------------------------+-- Partial solution+-- --------------------------------------------------------------------------++-- | A single entry in the partial solution: one variable, at one decision+-- level, with the reason it is there.+data Assignment v = Assignment+    { aIndex :: !Int+    , aLevel :: !Int+    , aVar   :: v+    , aKind  :: AssignmentKind v+    }++-- | Why an assignment is in the partial solution, and what it asserts: a+-- decision (a freely chosen singleton instance) or a derivation (a term forced+-- by unit propagation, with the incompatibility that forced it).+--+-- The two shapes are a sum /inside/ the record rather than two constructors of+-- it because they carry different payloads: sharing @aIndex@, @aLevel@ and+-- @aVar@ across two constructors is what would make the payload fields+-- partial selectors, and a partial selector is a crash waiting for the wrong+-- constructor.+data AssignmentKind v+    = Decision (ValueOf v)+    | Derivation (Term (SetOf v)) (Incompatibility v)++-- | The term contributed by an assignment; for a decision, @Positive@ of the+-- singleton.+assignmentTerm :: Domain v => Assignment v -> Term (SetOf v)+assignmentTerm a = case aKind a of+    Decision i     -> Positive (singleton (aVar a) i)+    Derivation t _ -> t++-- | The value a decision decides; 'Nothing' for a derivation.+decidedValue :: Assignment v -> Maybe (ValueOf v)+decidedValue a = case aKind a of+    Decision i   -> Just i+    Derivation{} -> Nothing++-- | Everything recorded about one variable: its own assignments oldest-first,+-- the intersection of their terms, and the value it was decided to be if it+-- has been decided.+--+-- @vaTerm@ is a cache of @foldl1 intersectTerm (assignmentTerm <$> vaHistory)@+-- and @vaDecision@ a cache of the (at most one) decision in @vaHistory@;+-- keeping them is what lets propagation ask about a variable without scanning+-- the partial solution. Invariant: a record exists only for a variable with a+-- non-empty history.+data VarAssignments v = VarAssignments+    { vaHistory  :: Seq (Assignment v)+    , vaTerm     :: Term (SetOf v)+    , vaDecision :: Maybe (ValueOf v)+    }++-- | Assignments are indexed by variable, and within a variable stored+-- oldest-first (chronological), so the satisfier search reads them in order+-- without reversing; @psLevel@ is the current decision level; @psNextIndex@ is+-- a monotone counter giving chronological order /across/ variables.+data PartialSolution v = PartialSolution+    { psVariables :: Map (v) (VarAssignments v)+    , psLevel     :: !Int+    , psNextIndex :: !Int+    }++emptyPS :: PartialSolution v+emptyPS = PartialSolution{psVariables = Map.empty, psLevel = 0, psNextIndex = 0}++-- | Add one assignment to a variable's record, creating the record if this is+-- the variable's first assignment. The caches move with it: the term folds in+-- by intersection, the decision is remembered.+extendVar :: Domain v => Assignment v -> Maybe (VarAssignments v) -> VarAssignments v+extendVar a Nothing =+    VarAssignments+        { vaHistory = Seq.singleton a+        , vaTerm = assignmentTerm a+        , vaDecision = decidedValue a+        }+extendVar a (Just pa) =+    pa+        { vaHistory = vaHistory pa Seq.|> a+        , vaTerm = intersectTerm (vaTerm pa) (assignmentTerm a)+        , vaDecision = decidedValue a <|> vaDecision pa+        }++-- | Rebuild a record from a history, recomputing both caches. 'Nothing' for an+-- empty history, which has no record.+fromHistory :: Domain v => Seq (Assignment v) -> Maybe (VarAssignments v)+fromHistory = foldl' (\acc a -> Just (extendVar a acc)) Nothing++-- | File an assignment under its variable and consume its index.+recordAssignment :: Domain v => Assignment v -> PartialSolution v -> PartialSolution v+recordAssignment a ps@PartialSolution{psVariables, psNextIndex} =+    ps+        { psVariables = Map.alter (Just . extendVar a) (aVar a) psVariables+        , psNextIndex = psNextIndex + 1+        }++-- | Record a decision (a guess); increments the decision level.+addDecision :: Domain v => v -> ValueOf v -> PartialSolution v -> PartialSolution v+addDecision p i ps@PartialSolution{psLevel, psNextIndex} =+    recordAssignment+        (Assignment psNextIndex (psLevel + 1) p (Decision i))+        ps{psLevel = psLevel + 1}++-- | Record a derivation: the negation of @cause@'s term for @p@, at the+-- current level.+addDerivation :: Domain v => v -> Incompatibility v -> PartialSolution v -> PartialSolution v+addDerivation p cause ps@PartialSolution{psLevel, psNextIndex} =+    let term = maybe anyTerm negateTerm (incompGet p cause)+     in recordAssignment (Assignment psNextIndex psLevel p (Derivation term cause)) ps++-- | Backtrack: drop every assignment strictly above the target level. Answers+-- with the variables that lost an assignment, whose accumulated terms are the+-- only ones that changed, and the solution after.+--+-- Levels are non-decreasing along a history (a derivation takes the current+-- level, a decision the next, and backtracking only lowers it), so what is+-- dropped is always a suffix — which is why this splits the history from the+-- right instead of filtering it: a variable that drops nothing keeps its history+-- as it stands, rather than paying to rebuild an identical one. For the same+-- reason a variable moved exactly when its newest assignment is above the+-- level, which is one lookup.+--+-- A variable that does lose assignments must have both its caches rebuilt from+-- the survivors — @intersectTerm@ cannot be undone, so the accumulated term is+-- recomputed, and a dropped decision must stop being remembered. A variable that+-- loses all of them loses its record.+backtrack :: Domain v => Int -> PartialSolution v -> ([v], PartialSolution v)+backtrack level ps@PartialSolution{psVariables} =+    ( [v | (v, pa) <- Map.toList psVariables, moved pa]+    , ps+        { psVariables = Map.mapMaybe prune psVariables+        , psLevel = level+        }+    )+  where+    moved pa = case vaHistory pa of+        _ Seq.:|> a -> aLevel a > level+        Seq.Empty   -> False+    prune pa = case Seq.spanr ((> level) . aLevel) (vaHistory pa) of+        (dropped, kept)+            | Seq.null dropped -> Just pa+            | otherwise -> fromHistory kept++-- | Intersection of all terms recorded for a variable ('Nothing' if the+-- variable is unmentioned, which judges as 'anyTerm' = ⊤).+termIntersectionFor :: Domain v => PartialSolution v -> v -> Maybe (Term (SetOf v))+termIntersectionFor PartialSolution{psVariables} p =+    vaTerm <$> Map.lookup p psVariables++-- | Relation of the whole partial solution to an incompatibility.+psRelation :: Domain v => PartialSolution v -> Incompatibility v -> IncompatRelation v+psRelation ps = incompRelation (termIntersectionFor ps)++-- | The decisions, as a solution map.+extractSolution :: PartialSolution v -> Map (v) (ValueOf v)+extractSolution PartialSolution{psVariables} = Map.mapMaybe vaDecision psVariables++-- | Variables that have a positive accumulated term but no decision yet, with+-- that positive set. Ordered by first mention (oldest first) for+-- determinism.+undecidedPositive :: PartialSolution v -> [(v, SetOf v)]+undecidedPositive PartialSolution{psVariables} =+    map snd (sortOn fst (mapMaybe candidate (Map.toList psVariables)))+  where+    candidate (p, pa) = case (vaDecision pa, vaTerm pa) of+        (Nothing, Positive r) -> Just (firstIndex pa, (p, r))+        _                     -> Nothing+    -- The variable's first mention, which is what the order is keyed on. A+    -- record always has a non-empty history, so the fallback is unreachable.+    firstIndex pa = maybe maxBound aIndex (Seq.lookup 0 (vaHistory pa))++-- | All assignments for a variable, oldest first. The satisfier search walks+-- this list.+varHistory :: Domain v => PartialSolution v -> v -> [Assignment v]+varHistory PartialSolution{psVariables} p =+    maybe [] (toList . vaHistory) (Map.lookup p psVariables)

@@ -0,0 +1,42 @@+-- | Compact rendering to 'Text', for messages and explanations: version sets+-- as ranges, finite sets in braces, negative terms as @¬(…)@.+--+-- It is separate from 'Show' on purpose. 'Show' stays derived and shows the+-- constructors as they are, which is what debugging wants; 'pretty' is what a+-- person reads.+module PubGrub.Pretty (Pretty (..), AsPretty (..)) where++import           Data.Maybe         (fromMaybe)+import           Data.Set           (Set)+import qualified Data.Set           as Set+import           Data.Text          (Text)+import qualified Data.Text          as T+import           PubGrub.Term       (Term (..))+import           PubGrub.Version    (Version, versionNumbers)+import           PubGrub.VersionSet (VersionSet, declared, renderVersionSet)++-- | Types with a compact rendering.+class Pretty a where+    -- | The rendering.+    pretty :: a -> Text++-- | Shows a value through 'pretty', for GHCi and examples.+newtype AsPretty a = AsPretty {getAsPretty :: a}++instance Pretty a => Show (AsPretty a) where+    show = T.unpack . pretty . getAsPretty++instance Pretty Version where+    pretty = T.intercalate (T.pack ".") . map (T.pack . show) . versionNumbers++-- | The declared spelling where there is one, and the canonical intervals+-- otherwise ('PubGrub.VersionSet.renderVersionSet').+instance Pretty VersionSet where+    pretty vs = fromMaybe (renderVersionSet vs) (declared vs)++instance Pretty a => Pretty (Term a) where+    pretty (Positive s) = pretty s+    pretty (Negative s) = T.pack "¬(" <> pretty s <> T.pack ")"++instance Pretty a => Pretty (Set a) where+    pretty s = T.pack "{" <> T.intercalate (T.pack ",") (map pretty (Set.toList s)) <> T.pack "}"

@@ -0,0 +1,58 @@+-- | The provider: how the solver learns about the world, one variable at a+-- time.+module PubGrub.Provider+    ( Provider (..)+    ) where++import           PubGrub.Incompatibility (Domain (..), Incompatibility)+++-- | What the solver asks of the world. It never sees the world itself, only+-- variables, sets of values and incompatibilities, and it asks about one+-- variable when it needs to: there is no problem description handed over up+-- front, so a provider reads only what the search reaches.+--+-- The question is always the same: here is a variable, and the set of values+-- it may still take; commit to one of them, and say what that choice entails.+-- The set may be symbolic, a range rather than a list, so the provider is not+-- asked to enumerate it: it picks a value the set admits, by whatever+-- preference it has (the newest version, an installed one, a default).+--+-- @m@ is the provider's own monad: 'Data.Functor.Identity.Identity' for a world+-- held in memory, 'IO' for one read from disk.+newtype Provider v m = Provider+    { expand :: v -> SetOf v -> m (Maybe (ValueOf v), [Incompatibility v])+      -- ^ Pick a value of the variable from the set, and state what is known+      -- on the way: typically the chosen value's dependencies.+      --+      -- __The value must be in the set.__ The set is everything the solver+      -- has derived about the variable, and the solver records the value as a+      -- decision at once, so a value outside it contradicts what the solver+      -- already knows. The solver checks, and stops the solve with+      -- 'PubGrub.Solver.BadValue' rather than go on. A value in the set that+      -- turns out wrong is not an error: on a later conflict the solver+      -- backtracks and asks again with a smaller set.+      --+      -- Answer 'Nothing' when no value in the set can be chosen. The solver+      -- then states that the variable takes no value in the set, so the same+      -- set is never offered twice.+      --+      -- __The incompatibilities are facts.__ The solver adds them to what it+      -- knows without examining them, and each must be true of every solution,+      -- whatever has been decided so far. They need not mention the chosen+      -- value. So a provider that passes over values on the way to its answer+      -- may say why it passed them over, and those facts prune the search and+      -- explain a failure like any other. A fact should have a positive term,+      -- or a single negative one: a fact of two or more negative terms and+      -- nothing else says that one of several variables must have a value+      -- without saying which, and the search never acts on it.+      --+      -- This matters most when the answer is 'Nothing'. If every value in the+      -- set was rejected for a reason (it cannot be built here, it needs+      -- something missing), state the reasons: the solver uses them, and+      -- states \"no value\" only for what they do not cover. A failure is then+      -- explained by what was wrong with the values, not by their absence.+      -- Only a fact about the variable alone covers its values. A reason that+      -- names another variable rules the values out only while its other terms+      -- hold, so the solver states \"no value\" for them as well.+    }

@@ -0,0 +1,85 @@+module PubGrub.Relation+    ( Relation (..)+    , relation+    , IncompatRelation (..)+    , incompRelation+    ) where++import qualified Data.Map.Strict         as Map+import           PubGrub.Incompatibility (Domain (..), Incompatibility (..))+import           PubGrub.SetOps          (SetOps (..))+import           PubGrub.Term            (Term (..))++-- Specialised in the client, with the solver ("PubGrub.Solver" says why).+{-# INLINABLE relation #-}+{-# INLINABLE incompRelation #-}+++-- | How a term stands relative to a reference term (both about the same+-- package). This is the primitive unit propagation reads off the partial+-- solution.+data Relation+    = -- | @subject ⊆ reference@: the reference already holds.+      Satisfied+    | -- | @subject ∩ reference = ∅@: they cannot both hold.+      Contradicted+    | -- | neither — the reference is still open.+      Inconclusive+    deriving (Eq, Show)++-- | Relation of @subject@ (typically what the partial solution has derived so+-- far for a package) to @reference@ (a term from an incompatibility). Both+-- tests are emptiness tests, so no equality on payloads is needed — and no+-- reliance on canonical representations either. Against a negative reference,+-- an exact subject either avoids the set or lands in it; a negative subject is+-- never satisfied by a positive reference, because the /absent/ state always+-- escapes it.+relation :: SetOps a => Term a -> Term a -> Relation+relation subject reference+    | subject `isSubsetOf` reference = Satisfied+    | subject `isDisjoint` reference = Contradicted+    | otherwise = Inconclusive++-- --------------------------------------------------------------------------+-- Judging a whole incompatibility+-- --------------------------------------------------------------------------++-- | Relation of a partial solution (seen as a term lookup) to a whole+-- incompatibility.+data IncompatRelation v+    = ISatisfied+    | IContradicted v+    | -- | all terms satisfied but one (the named variable): the unit case+      IAlmostSatisfied v+    | IInconclusive+    deriving (Eq, Show)++-- | Judge an incompatibility against the partial solution. @lookupTerm v@ is+-- the accumulated term the partial solution holds for @v@, or 'Nothing' if+-- @v@ is unmentioned (equivalent to ⊤, and always inconclusive).+incompRelation+    :: Domain v+    => (v -> Maybe (Term (SetOf v)))+    -> Incompatibility v+    -> IncompatRelation v+incompRelation lookupTerm (Incompatibility m _) = Map.foldlWithKey' step ISatisfied m+  where+    -- A strict fold over the map rather than a walk over 'Map.toList': this runs+    -- for every clause on every visit, and the list cost a tenth of a large+    -- solve's allocation. A clause has a handful of terms, so once the answer is+    -- final the remaining terms are skipped by the first two equations rather+    -- than by stopping. Terms are judged in key order, which decides the+    -- variable a contradiction or an open term is reported on.+    step acc@(IContradicted _) _ _ = acc+    step IInconclusive _ _ = IInconclusive+    step acc v it =+        case lookupTerm v of+            Just term ->+                case relation term it of+                    Satisfied    -> acc+                    Contradicted -> IContradicted v+                    Inconclusive -> almost v acc+            Nothing -> almost v acc+    -- absent or inconclusive term: at most one allowed for AlmostSatisfied+    almost v ISatisfied = IAlmostSatisfied v+    almost _ _          = IInconclusive

@@ -0,0 +1,327 @@+{-# LANGUAGE OverloadedStrings #-}++-- | Rendering a failed resolution as a human-readable proof, over any 'Domain'.+--+-- A terminal t'Incompatibility' carries the 'Cause' tree that produced it, which+-- is all this module needs: 'reportConflict' replays that tree as PubGrub's+-- argument for why no solution exists, one line per step it keeps, ending+-- \"So, because …, version solving failed\".+--+-- == What is fixed and what is the domain's+--+-- The wording is the domain's; the /shape/ of the argument is fixed: which+-- steps get a line, which are skipped, where a line number is minted and where+-- a blank line falls. The shape is here, written once. The words come from a+-- t'Formatter' the domain supplies (what a fact says, what a /hole/, a set of+-- values in which the provider had nothing, says, and what a set of terms+-- concludes), together with any rules of its own that say a step in fewer+-- lines than the standard cases would, and a pass over the tree before the walk+-- begins.+--+-- == How the proof is made+--+-- The walker visits each derived step and writes one line for it: a+-- connective, a __premise__, and what the step concludes. The premise is what+-- varies, and it is chosen by a __rule__ — the first of the line rules to fire.+-- A rule is a @do@ block in 'Maybe', written in the vocabulary of+-- "PubGrub.Derivation": each line reads a view of the tree or states a guard,+-- and the last says the premise and names the sub-derivation, if any, the line+-- continues (@Line@). Two facts named together in one premise are joined by a+-- second table, the clause rules, in the same language.+--+-- Two rules keep the proof short, and both are PubGrub's own. Neither is+-- cosmetic: a proof is only useful if it is read to the end, and the naive+-- replay of the derivation tree — one line per derived incompatibility, each+-- naming one external fact — is too long for that.+--+--  * __A chain of two external facts is one sentence__: a domain's clause rules.+--    Where a dependency's dependee is the depender of the next, the proof writes+--    \"@foo@ depends on @bar@ /which depends on/ @baz@\" rather than naming+--    @bar@ twice, and where two facts share a depender it writes \"depends on+--    /both/ X and Y\". What a dependency is, the core does not know, so these+--    rules belong to the domain's t'Formatter'.+--+--  * __Every other derived step is skipped__. Where a step's derived cause has+--    a single derived cause of its own, that intermediate /conclusion/ is left+--    out and both external facts are named in one line. Most derivation graphs+--    are linear chains, so this halves them without losing anything a reader+--    needs.+--+-- == Line numbers are for joins only+--+-- A line is numbered only if a later line refers back to it, and in a linear+-- chain none does. A number is given only at a step with two derived causes,+-- so a proof that never branches carries no numbers at all.+--+-- A sub-derivation that two steps share is explained twice rather than+-- referred to: an t'Incompatibility' has no identity to recognise it by.+module PubGrub.Report+    ( -- * The domain's words+      Formatter (..)+    , mkFormatter+    , Line (..)+    , leaf+    , summaryWith+    , listing+    , anyOf+      -- * The proof+    , reportConflict+    ) where++import           Data.List               (unsnoc)+import           Data.Map.Strict         (Map)+import qualified Data.Map.Strict         as Map+import           Data.Maybe              (fromMaybe)+import           Data.Text               (Text)+import qualified Data.Text               as T+import           PubGrub.Derivation      (Rule, bothDerived, bothExternal,+                                          chainStep, firstOf, isDerived)+import           PubGrub.Incompatibility (Cause (..), Domain (..),+                                          Incompatibility (..))+import           PubGrub.Term            (Term (..))++-- --------------------------------------------------------------------------+-- The domain's words+-- --------------------------------------------------------------------------++-- | What a domain says, and the rules of its own it adds to the standard ones.+--+-- Every field that says something answers with a fragment: no connective in+-- front of it and no full stop after it, because the walker puts its own+-- \"Because\" before a fragment and ends every line as a sentence. A fragment+-- must therefore never open with \"because\" or \"and\".+data Formatter v = Formatter+    { sayFact     :: FactOf v -> Incompatibility v -> Text+      -- ^ a leaf that states a fact, a seed's or the provider's; the+      -- incompatibility it is the cause of comes with it, for a fact whose+      -- sentence depends on which of its terms survived+    , sayNoValues :: v -> SetOf v -> Text+      -- ^ the solver's own leaf: nothing to offer in this set+    , sayTerms    :: Map (v) (Term (SetOf v)) -> Text+      -- ^ what a set of terms concludes; 'summaryWith' is the standard sentences+    , prepare     :: Incompatibility v -> Incompatibility v+      -- ^ a pass over the tree before the walk; 'id' for none+    , lineRules   :: [Rule (Incompatibility v) (Line v)]+      -- ^ the domain's own ways of saying a step that is not a branch, tried+      -- before the standard rules for a chain of steps; a rule must keep the+      -- proof sound on its own, and can check that it does by replaying the+      -- steps it covers with 'PubGrub.Incompatibility.priorCauseTerms'+    , clauseRules :: [Rule (Incompatibility v, Incompatibility v) Text]+      -- ^ the domain's ways of saying two external facts as one premise, tried+      -- in order; the fallback names them side by side+    }++-- | A formatter from the domain's three sentences, with no rules of its own:+-- what a fact says, what the solver's own finding that a variable has no+-- value in a set says, and how to name a variable with a set of its values,+-- from which 'summaryWith' makes the conclusions. The three other fields add+-- nothing ('prepare' is 'id', and there are no rules); set them by record+-- update, as in+-- @(mkFormatter says hole name){clauseRules = [rule]}@.+mkFormatter+    :: (FactOf v -> Incompatibility v -> Text)+    -> (v -> SetOf v -> Text)+    -> (v -> SetOf v -> Text)+    -> Formatter v+mkFormatter says hole name =+    Formatter+        { sayFact = says+        , sayNoValues = hole+        , sayTerms = summaryWith name name+        , prepare = id+        , lineRules = []+        , clauseRules = []+        }++-- | What a rule proposes for one line of the proof.+data Line v+    = Line+        Text+        -- ^ the premise, which goes after the connective+        (Maybe (Incompatibility v))+        -- ^ the sub-derivation the line continues, explained before it; a line+        -- that continues nothing opens a line of derivation++-- | An external fact at a leaf of the proof, in the domain's words; a derived+-- node, which is not a leaf, reads as what its terms conclude.+leaf :: Formatter v -> Incompatibility v -> Text+leaf fmt c = case incompCause c of+    Seed f       -> sayFact fmt f c+    Fact f       -> sayFact fmt f c+    NoValues v s -> sayNoValues fmt v s+    Derived _ _  -> sayTerms fmt (incompTerms c)++-- | What an incompatibility says, in PubGrub's standard sentences, given how+-- the domain names a variable with its set: @named@ where the sentence calls+-- for the full form (\"every version of foo\") and @bare@ where it does not. A+-- negative term is never written as \"not …\": it says the variable /must/ be+-- in that set, and the sentence carries the negation — \"foo requires bar >=2\",+-- \"if foo and bar then baz <3\", \"either foo <2 or bar <3\". The empty+-- incompatibility is failure by name: \"version solving failed\".+summaryWith+    :: (v -> SetOf v -> Text)+    -> (v -> SetOf v -> Text)+    -> Map (v) (Term (SetOf v))+    -> Text+summaryWith named bare ts = case Map.toList ts of+    [] -> "version solving failed"+    [(p, Positive r)] -> bare p r <> " is forbidden"+    [(p, Negative r)] -> bare p r <> " is required"+    [(p1, Positive r1), (p2, Negative r2)] -> requires p1 r1 p2 r2+    [(p2, Negative r2), (p1, Positive r1)] -> requires p1 r1 p2 r2+    [(p1, Positive r1), (p2, Positive r2)] -> bare p1 r1 <> " is incompatible with " <> bare p2 r2+    [(p1, Negative r1), (p2, Negative r2)] -> "either " <> bare p1 r1 <> " or " <> bare p2 r2+    terms ->+        let positives = [(p, r) | (p, Positive r) <- terms]+            negatives = [bare p r | (p, Negative r) <- terms]+         in case (positives, negatives) of+                ([(p, r)], _ : _) -> named p r <> " requires " <> anyOf negatives+                (_ : _, _ : _) ->+                    "if " <> T.intercalate " and " (map (uncurry bare) positives)+                        <> " then " <> anyOf negatives+                (_, []) -> "one of " <> anyOf (map (uncurry bare) positives) <> " must be false"+                ([], _) -> "one of " <> anyOf negatives <> " must be true"+  where+    -- A /derived/ two-term incompatibility. The spec says \"requires\" here and+    -- keeps \"depends on\" for the external fact (@references\/pubgrub.md:1005@,+    -- both in one line): a dependency is declared, a requirement is what the+    -- solver worked out.+    requires p1 r1 p2 r2 = named p1 r1 <> " requires " <> bare p2 r2++-- | \"a, b and c\"+listing :: [Text] -> Text+listing xs = case unsnoc xs of+    Just (front@(_ : _), l) -> T.intercalate ", " front <> " and " <> l+    _                       -> T.intercalate ", " xs++-- | \"a or b or c\"+anyOf :: [Text] -> Text+anyOf = T.intercalate " or "++-- --------------------------------------------------------------------------+-- The proof+-- --------------------------------------------------------------------------++-- | Render an incompatibility and its derivation as a human-readable proof.+reportConflict :: Domain v => Formatter v -> Incompatibility v -> Text+reportConflict fmt root0+    | isDerived root = render (reverse (outLines (derived fmt True root (Out [] 1))))+    -- The terminal incompatibility is itself an external fact: nothing was+    -- derived, so the fact is the whole explanation.+    | otherwise = leaf fmt root+  where+    root = prepare fmt root0++    -- Every line is a sentence and ends as one. A blank line between two+    -- branches of a derivation (references/pubgrub.md:632) stays blank.+    render ls = T.intercalate "\n" [line n t | (n, t) <- ls]+    line _ "" = ""+    line n t  = prefix n <> t <> "."+    prefix Nothing  = ""+    prefix (Just n) = T.pack (show n) <> ". "++-- --------------------------------------------------------------------------+-- The walker+-- --------------------------------------------------------------------------++-- | The proof under construction: its lines __newest first__, and the next free+-- line number.+data Out = Out+    { outLines :: [(Maybe Int, Text)]+    , outNext  :: !Int+    }++emit :: Text -> Out -> Out+emit t out = out{outLines = (Nothing, t) : outLines out}++-- | Give the line just emitted a number, so a later line can cite it. Numbers+-- are minted here and nowhere else.+numberLast :: Out -> (Int, Out)+numberLast out = case outLines out of+    ((Just n, t) : rest) -> (n, out{outLines = (Just n, t) : rest})+    ((Nothing, t) : rest) ->+        ( outNext out+        , out{outLines = (Just (outNext out), t) : rest, outNext = outNext out + 1}+        )+    -- Unreachable: every branch emits at least one line before this is called.+    -- Answering with the unused number keeps the proof well-formed if it ever is.+    [] -> (outNext out, out)++-- | Explain one derived incompatibility, ending with the line that concludes it.+-- @final@ marks the last line of the whole proof, which reads \"So, …\" and+-- concludes failure by name.+derived :: Domain v => Formatter v -> Bool -> Incompatibility v -> Out -> Out+derived fmt final inc out = case bothDerived inc of+    -- Case 1 (references/pubgrub.md:595): both causes derived — the derivation+    -- branches, and this is the only place a line number is wanted. Explain the+    -- first branch, number the line it ends on, then explain the second and close+    -- by referring back. The blank line between the two branches is the spec's+    -- (:632): it marks that a new line of derivation starts. No rule chooses+    -- this: it is the structure of the proof, not a way of saying a step.+    Just (c1, c2) ->+        let (n, out') = numberLast (derived fmt False c1 out)+         in emit+                (opening (Just c2) <> summary c1 <> " (" <> T.pack (show n) <> "), " <> says inc)+                (derived fmt False c2 (emit "" out'))+    Nothing -> case firstOf rules inc of+        Just (Line premise below) ->+            emit+                (opening below <> premise <> ", " <> says inc)+                (maybe out (\d -> derived fmt False d out) below)+        -- Not reached: a derived step either branches, chains or joins two+        -- facts, and the last two rules of the table fire on any such step.+        Nothing -> emit (leaf fmt inc) out+  where+    -- The domain's rules go between the spec's case 3 and its case 2: a run+    -- rule collapses what the ordinary skip would print two facts at a time,+    -- and the spec's 2.iii fires on any chain step, so the table is total over+    -- chain steps. Case 3 fires only on a step both of whose causes are+    -- external, which no chain rule reads, so its place in the table is free.+    rules = twoFacts fmt : lineRules fmt ++ [everyOtherStep fmt, oneFact fmt]++    summary c = sayTerms fmt (incompTerms c)++    -- "So," marks the conclusion (references/pubgrub.md:1027); "Because" opens a+    -- line of derivation, which only a step with nothing below it does; "And+    -- because" continues one.+    opening below+        | final = "So, because "+        | Just _ <- below = "And because "+        | otherwise = "Because "+    says c+        | final = "version solving failed"+        | otherwise = summary c++-- --------------------------------------------------------------------------+-- The spec's cases+-- --------------------------------------------------------------------------++-- | Both causes are external. One line, and the only case that opens a line+-- of derivation rather than continuing one.+twoFacts :: Formatter v -> Rule (Incompatibility v) (Line v)+twoFacts fmt step = do+    (c1, c2) <- bothExternal step+    pure (Line (clause fmt c1 c2) Nothing)++-- | One cause is derived, from a derived cause and an external fact of its+-- own: the every-other-step skip. The derived cause's own conclusion is left+-- unsaid and the two external facts are named together here, which is where a+-- long linear chain loses half its lines.+everyOtherStep :: Formatter v -> Rule (Incompatibility v) (Line v)+everyOtherStep fmt step = do+    (d, e) <- chainStep step+    (dd, de) <- chainStep d+    pure (Line (clause fmt de e) (Just dd))++-- | One cause is derived and one external, and the derived cause branches or+-- bottoms out, so it gets its own lines and this one closes with the external+-- fact alone.+oneFact :: Formatter v -> Rule (Incompatibility v) (Line v)+oneFact fmt step = do+    (d, e) <- chainStep step+    pure (Line (leaf fmt e) (Just d))++-- | Two external facts, as one clause: the first of the domain's clause rules+-- to fire, or the two facts side by side.+clause :: Formatter v -> Incompatibility v -> Incompatibility v -> Text+clause fmt c1 c2 = fromMaybe (leaf fmt c1 <> " and " <> leaf fmt c2) (firstOf (clauseRules fmt) (c1, c2))

@@ -0,0 +1,85 @@+-- | Sets of values: what a term ranges over.+--+-- A domain's set type ('PubGrub.Incompatibility.SetOf') is an instance of+-- 'SetOps'. 'Set' is one, for values that can be listed, and+-- "PubGrub.VersionSet" is one for ranges of versions.+module PubGrub.SetOps+    ( SetOps (..)+    , equivalent+    ) where++import           Data.Set (Set)+import qualified Data.Set as Set++-- $setup+-- >>> import qualified Data.Set as Set++-- ---------------------------------------------------------------------------+-- SetOps+-- ---------------------------------------------------------------------------++-- | The operations the solver needs from a set of values: the empty set,+-- intersection, union, difference and an emptiness test. Each must mean what+-- it says of the values a set holds.+--+-- There is no complement, so a set type needs no universe of all values. The+-- solver negates terms, not sets: 'PubGrub.Term.Negative' is the negation of+-- 'PubGrub.Term.Positive' over the same set.+--+-- 'isSubsetOf' and 'isDisjoint' have defaults in terms of the other methods.+-- An instance may override them to answer without building a set, and must+-- then answer exactly as the defaults would.+class SetOps a where+    -- | The set with no values.+    empty       :: a+    -- | The values in both sets.+    intersect   :: a -> a -> a+    -- | The values in either set.+    union       :: a -> a -> a+    -- | The values in the first set and not in the second.+    difference  :: a -> a -> a+    -- | Does the set hold no value?+    isEmpty     :: a -> Bool++    -- The two tests are methods because the solver asks them of every term it+    -- judges. Building the difference or the intersection first, as the+    -- defaults do, measured at a fifth of a large solve's time and two fifths+    -- of its allocation.++    -- | @a ⊆ b@: removing @b@ from @a@ leaves nothing.+    --+    -- >>> Set.fromList [3,4] `isSubsetOf` Set.fromList [1..9]+    -- True+    --+    -- >>> Set.fromList [1..9] `isSubsetOf` Set.fromList [3,4]+    -- False+    isSubsetOf :: a -> a -> Bool+    isSubsetOf a b = isEmpty (a `difference` b)++    -- | @a ∩ b = ∅@: no value is in both.+    --+    -- >>> Set.fromList [1,2] `isDisjoint` Set.fromList [3,4]+    -- True+    --+    -- >>> Set.fromList [1,2,3] `isDisjoint` Set.fromList [3,4]+    -- False+    isDisjoint :: a -> a -> Bool+    isDisjoint xs ys = isEmpty (xs `intersect` ys)++-- | Do two sets hold the same values? Two subset tests, so it needs neither+-- 'Eq' nor a canonical form.+--+-- >>> equivalent (Set.fromList [1,2]) (Set.fromList [2,1])+-- True+equivalent :: SetOps s => s -> s -> Bool+equivalent x y = x `isSubsetOf` y && y `isSubsetOf` x++-- | Sets whose values can be listed.+instance Ord a => SetOps (Set a) where+    empty = Set.empty+    intersect = Set.intersection+    union = Set.union+    difference = Set.difference+    isEmpty = Set.null+    isSubsetOf = Set.isSubsetOf+    isDisjoint = Set.disjoint

@@ -0,0 +1,482 @@+{-# LANGUAGE DerivingStrategies   #-}+{-# LANGUAGE LambdaCase           #-}+{-# LANGUAGE StandaloneDeriving   #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Solving: 'solve' runs PubGrub over a t'PubGrub.Provider.Provider' and the+-- incompatibilities it is asked to satisfy, and answers with a value for every+-- variable it decided, or with the incompatibility that proves there is none.+module PubGrub.Solver+    ( solve+    , SolveError (..)+    , SolverMsg (..)+    ) where++import           Colog.Core              (LogAction, (<&))+import           Control.Monad           (foldM)+import           Data.Bifunctor          (first)+import           Data.IntSet             (IntSet)+import qualified Data.IntSet             as IntSet+import           Data.List.NonEmpty      (nonEmpty)+import qualified Data.List.NonEmpty      as NE+import           Data.Map.Strict         (Map)+import qualified Data.Map.Strict         as Map+import           Data.Maybe              (fromMaybe)+import           PubGrub.Incompatibility (Domain (..), Incompatibility (..),+                                          incompGet, isSeed, noValues,+                                          priorCause)+import           PubGrub.PartialSolution (Assignment (..), AssignmentKind (..),+                                          PartialSolution (..), addDecision,+                                          addDerivation, assignmentTerm,+                                          backtrack, emptyPS, extractSolution,+                                          psRelation, undecidedPositive,+                                          varHistory)+import           PubGrub.Provider        (Provider (..))+import           PubGrub.Relation        (IncompatRelation (..), incompRelation)+import           PubGrub.SetOps          (SetOps (..))+import           PubGrub.Store           (Store, allClauses, clauseAt,+                                          clausesOf, emptyStore, insertClause,+                                          insertClauses, storeSize)+import           PubGrub.Term            (Term (..), anyTerm, intersectTerm,+                                          negateTerm)++-- The solver is polymorphic in the domain and the monad, and a client calls it+-- from another package, where GHC specialises an imported function only if it+-- has an unfolding to specialise. These pragmas, and the ones in the modules+-- the solver calls, give every function that takes a dictionary one, so that+-- a client's solve runs over its own variable and set types rather than+-- through the dictionaries. Measured on synthetic problems over a Set Int+-- domain, with every count identical: a fifth of the time and a tenth of+-- the allocation.+{-# INLINABLE satisfierOf #-}+{-# INLINABLE maximumOn #-}+{-# INLINABLE satisfierSearch #-}+{-# INLINABLE seedAssignments #-}+{-# INLINABLE satisfiedBySeeds #-}+{-# INLINABLE closeWithSeeds #-}+{-# INLINABLE unitPropagation #-}+{-# INLINABLE conflictResolution #-}+{-# INLINABLE solve #-}++-- --------------------------------------------------------------------------+-- The algorithm+-- --------------------------------------------------------------------------++-- | Result of searching for the satisfier of a conflict incompatibility.+data SatisfierSearch v+    = DifferentDecisionLevels !Int+      -- ^ backtrack to this level+    | SameDecisionLevels (Incompatibility v)+      -- ^ satisfier's cause++-- | Earliest assignment of @p@ whose running accumulated term becomes disjoint+-- from @startTerm@, or 'Nothing' if none does.+satisfierOf+    :: Domain v+    => PartialSolution v+    -> v+    -> Term (SetOf v)+    -> Maybe (Assignment v)+satisfierOf ps p startTerm = go anyTerm (varHistory ps p)+  where+    go _ [] = Nothing+    go acc (a : as)+        | isEmpty (intersectTerm acc' startTerm) = Just a+        | otherwise = go acc' as+      where+        acc' = intersect acc (assignmentTerm a)++-- | 'Data.List.maximumBy' on a key, total. Ties keep the earlier element, which never+-- arises here: the key is @aIndex@, and indices are unique.+maximumOn :: Ord b => (a -> b) -> [a] -> Maybe a+maximumOn f = foldl' pick Nothing+  where+    pick Nothing x = Just x+    pick (Just best) x+        | f x > f best = Just x+        | otherwise = Just best++-- | The satisfier of an incompatibility is the latest of its terms' satisfiers.+-- When the satisfier is a derivation and the previous satisfier sits at its+-- level, resolution continues with the satisfier's cause; otherwise it+-- backtracks to the previous satisfier's level.+--+-- Every term of a satisfied incompatibility has a satisfier, so 'satisfierOf'+-- returning 'Nothing' means the partial solution and 'psRelation' disagree.+-- That is reported as a 'NoSatisfier' failure rather than thrown, so a bug+-- there is something the caller can print, not a crash inside a pure fold.+satisfierSearch+    :: Domain v+    => PartialSolution v+    -> Incompatibility v+    -> Either (SolveError v) (v, SatisfierSearch v)+satisfierSearch ps i = do+    satMap <- traverse satisfierForTerm (Map.toList (incompTerms i))+    (satVar, satAssign) <- latestSatisfier satMap+    let satLevel = aLevel satAssign+        it_s = fromMaybe anyTerm (incompGet satVar i)+        startTerm' = intersect (assignmentTerm satAssign) (negateTerm it_s)+    prevForSat <- require satVar (satisfierOf ps satVar startTerm')+    let satMap' = [(p, if p == satVar then prevForSat else a) | (p, a) <- satMap]+    (_, prevAssign) <- latestSatisfier satMap'+    -- No floor. The requests are derivations at level 0, so the first decision+    -- at level 1 is an ordinary one that a conflict may have to undo. The spec+    -- stops at level 1 (@references\/pubgrub.md:398@), where its root package+    -- was selected, and notes that level 0 is safe (:401).+    let prevLevel = aLevel prevAssign+    pure $ case aKind satAssign of+        Derivation _ cause+            | prevLevel >= satLevel -> (satVar, SameDecisionLevels cause)+        _ -> (satVar, DifferentDecisionLevels prevLevel)+  where+    satisfierForTerm (p, it) = (,) p <$> require p (satisfierOf ps p (negateTerm it))+    require p = maybe (Left (NoSatisfier p i)) Right+    -- An incompatibility with no terms is the empty clause: unsatisfiable+    -- outright, hence a terminal failure. 'satisfiedBySeeds' catches it before+    -- conflict resolution ever gets here, so this is the same verdict by+    -- another route, not a second opinion.+    latestSatisfier = maybe (Left (NoSolution i)) Right . maximumOn (aIndex . snd)++-- | The assignments the seeds made: the level-0 derivations whose cause is a+-- seed ('isSeed'). They are the oldest assignments of all, and they are never+-- backtracked.+seedAssignments :: Domain v => PartialSolution v -> v -> [Assignment v]+seedAssignments ps p = [a | a <- varHistory ps p, fromSeed a]+  where+    fromSeed a = case aKind a of+        Derivation _ cause -> isSeed cause+        Decision _         -> False++-- | Is the incompatibility satisfied by the seeds' own derivations alone? Then+-- no decision took part in the conflict, so nothing can be backtracked and+-- version solving has failed. This is PubGrub's terminal test stated over the+-- seeds. The published algorithm starts from a single root package, so its+-- only level-0 derivation is the root's, and it stops on an incompatibility+-- that is empty or names the root alone; here the level-0 derivations are+-- whatever the seeds derived. An empty incompatibility is satisfied by+-- anything, and one whose every term is subsumed by a seed's derivation is+-- satisfied before anything is decided.+--+-- Checked before the satisfier search, which is what keeps a seed from ever being+-- a satisfier's cause: the seeds are the oldest assignments, so a seed derivation+-- is the latest satisfier only when it is the only one.+satisfiedBySeeds :: Domain v => PartialSolution v -> Incompatibility v -> Bool+satisfiedBySeeds ps inc = incompRelation seedTerm inc == ISatisfied+  where+    seedTerm p = foldr1 intersectTerm . NE.map assignmentTerm <$> nonEmpty (seedAssignments ps p)++-- | Resolve a terminal incompatibility against the seeds it rests on, one+-- 'priorCause' per seed, so that the incompatibility handed to the report is the+-- empty one and its derivation ends with the request: a proof's last line names+-- the request and concludes "version solving failed". Here the request is the+-- seeds, and the last step is taken explicitly.+--+-- Each step is a genuine resolution: 'satisfiedBySeeds' holds, so every term is+-- subsumed by its seed's derivation and the union over the pivot is ⊤. The+-- emptiness test that drops it is the one 'PubGrub.Relation.relation' answered+-- "satisfied" with, so the two agree. A term that nonetheless survives is left+-- as it is: the verdict is decided, and the report prints the closing line as+-- failure whatever the terms say.+closeWithSeeds+    :: (Domain v, Monad m)+    => LogAction m (SolverMsg v) -> PartialSolution v -> Incompatibility v -> m (Incompatibility v)+closeWithSeeds logA ps = go+  where+    -- One pass over the seeds of every variable named, which is enough: a seed+    -- has a single term, so resolving with one never adds a variable, and two+    -- seeds on one variable are both applied in the pass, one after the other.+    go inc =+        foldM step inc [(p, cause) | p <- Map.keys (incompTerms inc), a <- seedAssignments ps p, Derivation _ cause <- [aKind a]]+    step inc (p, cause)+        | Map.member p (incompTerms inc) = do+            let next = priorCause inc cause p+            logA <& Resolving p next+            pure next+        | otherwise = pure inc++-- | Propagate the incompatibilities to a fixpoint: judge each with+-- 'psRelation'; on @IAlmostSatisfied p@ derive (¬ its term for @p@) via+-- 'addDerivation'; on @ISatisfied@ hand off to 'conflictResolution'. Returns+-- the terminal incompatibility on unsolvable input, or the (possibly grown)+-- store and updated solution.+--+-- The clause acted on is the __newest__ clause that is satisfied or almost+-- satisfied — the first one a scan of the store from the front would find — and+-- a learned clause goes back through 'insertClause' rather than being consed+-- on, which is what gives dependency facts about one pair of packages the chance+-- to merge ('PubGrub.Store').+--+-- Which clauses are judged is a worklist, not the store. A clause's relation+-- depends only on the accumulated terms of the variables it mentions, and a+-- call starts from a fixpoint — nothing was actionable when the last one+-- returned — so the only clauses whose relation can have changed are the ones+-- the caller names: the ones inserted or merged into since then, and the ones+-- mentioning a variable it decided. Within the call, after a derivation on @q@+-- they are the clauses that mention @q@ ('clausesOf'). After a backtrack they+-- are the clauses of the variables that lost an assignment, the clause learned,+-- and the clauses of the variable the learned clause then derives. Those are+-- re-judged and the set of actionable clauses kept up to date; everything else+-- keeps the judgement it had. The clause chosen is therefore the one a full+-- scan would choose, every time: the search does not depend on the worklist,+-- and the number of judgements is proportional to what changed.+unitPropagation+    :: forall v m. (Domain v, Monad m)+    => LogAction m (SolverMsg v)+    -> IntSet+    -- ^ the clauses whose relation may have changed since the last fixpoint+    -> Store v+    -> PartialSolution v+    -> m (Either (SolveError v) (Store v, PartialSolution v))+unitPropagation logA pending store0 ps0 = settle pending IntSet.empty store0 ps0+  where+    -- Judge the dirty clauses, then act on the newest actionable one.+    settle dirty actionable store ps = do+        logA <& (Judged (IntSet.size dirty) :: SolverMsg v)+        let actionable' = IntSet.foldl' (judge store ps) actionable dirty+        case IntSet.maxView actionable' of+            Nothing        -> pure (Right (store, ps))+            Just (c, rest) -> act c rest store ps++    judge store ps acc c = case clauseAt store c of+        Just i | actionableRelation (psRelation ps i) -> IntSet.insert c acc+        _                                             -> IntSet.delete c acc++    actionableRelation ISatisfied           = True+    actionableRelation (IAlmostSatisfied _) = True+    actionableRelation _                    = False++    act c actionable store ps = case clauseAt store c of+        Nothing -> settle IntSet.empty actionable store ps+        Just i -> case psRelation ps i of+            ISatisfied -> do+                -- 'conflictResolution' is pure, so both of its events are logged+                -- from here: the conflict before it runs, and the level it landed+                -- on after. A terminal conflict logs the first and not the second,+                -- which is the right shape — nothing was backtracked to.+                logA <& Conflict i+                conflictResolution logA i ps >>= \case+                    Left err ->+                        pure (Left err)+                    Right (almostVar, rootCause, (moved, ps')) -> do+                        logA <& Learned rootCause+                        -- 'Backtracked' carries only a level, which does not+                        -- determine @d@, so the message's type is annotated.+                        logA <& (Backtracked (psLevel ps') :: SolverMsg v)+                        -- Only the clauses of the variables the backtrack+                        -- moved, the learned clause (which is the conflict's+                        -- clause too, where the rule merged them) and the+                        -- clauses of the variable it derives can have changed+                        -- relation; every other clause keeps its judgement,+                        -- actionable or not. How that set is collected is a+                        -- matter of cost alone, and both ways judge the same+                        -- clauses. When the moved variables are mentioned by+                        -- fewer clauses than the store holds, it is their+                        -- ids read off the index: a shallow backjump touches+                        -- a few clauses of a store that the full re-judge made+                        -- quadratic in the number of conflicts. Otherwise it+                        -- is the whole store, which costs one pass: a far+                        -- backjump's variables mention most of it, with+                        -- repeats, and listing their ids cost more than the+                        -- judging it saved. Counting the mentions allocates+                        -- nothing, and a union per variable is never built:+                        -- the ids interleave, so each union rebuilt its+                        -- accumulator.+                        let (learned, store') = insertClause rootCause store+                            changed = almostVar : moved+                            mentions = sum [IntSet.size (clausesOf v store') | v <- changed]+                            dirty+                                | mentions >= storeSize store' = allClauses store'+                                | otherwise = IntSet.fromList (c : learned : concatMap (IntSet.toList . (`clausesOf` store')) changed)+                        settle dirty actionable store' (addDerivation almostVar rootCause ps')+            IAlmostSatisfied q ->+                settle (clausesOf q store) actionable store (addDerivation q i ps)+            -- Not actionable after all: unreachable while the actionable set is+            -- kept right, and harmless if it is not — the clause is dropped from+            -- the set and the next newest is tried.+            _ -> settle IntSet.empty actionable store ps+++-- | Conflict resolution: satisfier search over 'varHistory', 'priorCause'+-- while satisfier and previous satisfier share a decision level, then+-- 'backtrack'. Returns the failure (no solution, or a violated invariant), or+-- the pivot variable, the learned root cause, and what 'backtrack' answered:+-- the variables it moved and the backtracked solution.+-- It is monadic only to log 'Resolving': the outcome depends on the partial+-- solution alone.+conflictResolution+    :: (Domain v, Monad m)+    => LogAction m (SolverMsg v)+    -> Incompatibility v+    -> PartialSolution v+    -> m (Either (SolveError v) (v, Incompatibility v, ([v], PartialSolution v)))+conflictResolution logA = loop+  where+    loop current ps+        | satisfiedBySeeds ps current = Left . NoSolution <$> closeWithSeeds logA ps current+        | otherwise =+            case satisfierSearch ps current of+                Left err -> pure (Left err)+                Right (satVar, DifferentDecisionLevels prevLevel) ->+                    pure (Right (satVar, current, backtrack prevLevel ps))+                Right (satVar, SameDecisionLevels satCause) -> do+                    let next = priorCause current satCause satVar+                    logA <& Resolving satVar next+                    loop next ps+++-- | Why 'solve' found no solution. Only 'NoSolution' is a verdict on the+-- problem; the others say the solve was given something it cannot work with.+data SolveError v+    = -- | There is none. The incompatibility is the end of the proof: normally+      -- one with no terms, which can never be satisfied, derived from the seeds+      -- and from facts the provider stated. Its 'PubGrub.Incompatibility.Cause'+      -- tree is the argument for why; "PubGrub.Report" writes it out and+      -- "PubGrub.Derivation" reads it.+      NoSolution (Incompatibility v)+    | -- | This seed is not a request or a constraint: its cause is not+      -- 'PubGrub.Incompatibility.Seed', or it has more or fewer than one term;+      -- one built with 'PubGrub.Incompatibility.seed' never is.+      -- The solve is refused before it starts. A seed with two negative terms,+      -- say, asks for one of two variables to have a value without saying+      -- which, and the search would never decide either: the answer would be a+      -- plan that violates the seed.+      BadSeed (Incompatibility v)+    | -- | The provider chose a value outside the set it was offered: the+      -- variable, the value, and the set. The solver stops at once, because+      -- recording such a decision contradicts what it had already derived and+      -- the search would never end. This is a bug in the provider.+      BadValue (v) (ValueOf v) (SetOf v)+    | -- | The solver broke an invariant of its own: conflict resolution found a+      -- term of a violated incompatibility that nothing it had recorded about+      -- the variable accounts for. This is a bug in the solver, returned as a+      -- value so that a caller can report it.+      NoSatisfier (v) (Incompatibility v)++deriving stock instance (Eq (v), Eq (ValueOf v), Eq (SetOf v), Eq (FactOf v)) => Eq (SolveError v)+deriving stock instance (Show (v), Show (ValueOf v), Show (SetOf v), Show (FactOf v)) => Show (SolveError v)++-- | What the solver is doing: one message per step of the search, and 'Judged'+-- per round of propagation. 'solve' sends them to the log action it is given.+data SolverMsg v+    = -- | About to ask the provider for a value of the variable in the set.+      Deciding (v) (SetOf v)+    | -- | The provider chose this value, and the solver decided it.+      Chose (v) (ValueOf v)+    | -- | The provider had no value in the set. A conflict follows.+      NoVersionFor (v) (SetOf v)+    | -- | This incompatibility is violated by what has been decided: a+      -- conflict, which conflict resolution starts from.+      Conflict (Incompatibility v)+    | -- | One step of conflict resolution: the variable it resolved on, and+      -- the incompatibility it derived. The number of these between a+      -- 'Conflict' and its 'Backtracked' is how deep that resolution went.+      Resolving (v) (Incompatibility v)+    | -- | The incompatibility conflict resolution learned, which the solver now+      -- keeps. The 'Conflict' that started it was already known; this is new.+      Learned (Incompatibility v)+    | -- | The solver undid every decision above this level. A level is the+      -- number of decisions in force.+      Backtracked Int+    | -- | One round of propagation judged this many incompatibilities, the ones+      -- that may have changed since the last. The round right after a+      -- 'Backtracked' judges again what the backtrack undid. This measures the+      -- solver's work and is not a step of the search: another release may+      -- change these counts without changing what the solver decides.+      Judged Int++deriving stock instance (Eq (v), Eq (ValueOf v), Eq (SetOf v), Eq (FactOf v)) => Eq (SolverMsg v)+deriving stock instance (Show (v), Show (ValueOf v), Show (SetOf v), Show (FactOf v)) => Show (SolverMsg v)++-- | Solve: find a value for every variable the request needs, or prove that+-- there is none.+--+-- The seeds are the request, incompatibilities whose cause is+-- 'PubGrub.Incompatibility.Seed': @{p: Negative s}@ asks for @p@ to have a+-- value in @s@, and @{p: Positive f}@ forbids @p@ the values in @f@ (see+-- t'Incompatibility'). Those are the only two shapes: a seed with any other+-- cause, or with more or fewer than one term, is answered with 'BadSeed'+-- before the search starts. The solver alternates two steps. It derives+-- everything that what it knows implies about each variable; then, of the+-- variables that must have a value and have none yet, it takes the one the+-- search reached first, and asks the provider for a value+-- ('PubGrub.Provider.expand'). The requested variables come first, in the+-- order of the seeds. When no variable is left without a value, the solve is+-- done; when a conflict rests on the seeds alone, there is no solution.+--+-- The answer maps each variable the solver decided to its value: those the+-- request requires, directly or through what the provider stated. A variable+-- nothing requires is not in it.+--+-- The first argument receives a 'SolverMsg' at each step, a @LogAction@ from+-- co-log-core; 'mempty' discards them.+solve+    :: (Domain v, Monad m)+    => LogAction m (SolverMsg v)+    -> Provider v m+    -> [Incompatibility v]+    -> m (Either (SolveError v) (Map (v) (ValueOf v)))+solve logA provider seeds+    | (bad : _) <- filter (not . wellFormedSeed) seeds = pure (Left (BadSeed bad))+    | otherwise = uncurry go (insertClauses seeds emptyStore) emptyPS+    where+        -- A request or a constraint: one term, marked as a seed.+        wellFormedSeed i = isSeed i && Map.size (incompTerms i) == 1++        go pending incompats ps =+            unitPropagation logA pending incompats ps >>= \case+                Left err -> pure (Left err)+                Right (incompats', ps') ->+                    case undecidedPositive ps' of+                        [] -> pure (Right (extractSolution ps'))+                        ((p, range) : _) -> do+                            logA <& Deciding p range+                            expand provider p range >>= \case+                                -- The provider's contract, checked: a decision+                                -- outside the offered set would contradict the+                                -- derivation that offered it, and the search+                                -- would not terminate.+                                (Just i, _)+                                    | not (singleton p i `isSubsetOf` range) ->+                                        pure (Left (BadValue p i range))+                                (Just i, incs) -> do+                                    logA <& Chose p i+                                    let (inserted, store) = insertClauses incs incompats'+                                    go (inserted <> clausesOf p store) store (addDecision p i ps')+                                (Nothing, facts) -> do+                                    logA <& NoVersionFor p range+                                    let (banned, store) = banRest p range facts incompats'+                                        (inserted, store') = insertClauses facts store+                                    go (banned <> inserted) store' ps'++        -- The provider has nothing to offer in @range@, and may have said why:+        -- clauses banning the releases it rejected on the way+        -- (@references\/pubgrub.md:475@). Those are a better explanation than+        -- "no version for p in range" — they name the reason rather than the+        -- symptom — but they are not necessarily a complete one, so what is left+        -- of the range gets the weaker statement it deserves and no more.+        --+        -- __Progress does not depend on the provider being thorough.__ Whatever it+        -- says, this bans all of @range@ between them: the facts cover part, the+        -- @noValues@ clause covers the remainder. So @p@ cannot be offered the+        -- same set twice, which is the property termination rests on. Only a fact+        -- about @p@ alone covers anything: one with a term about another variable+        -- rules its values out only while that term holds, and @p@ would be+        -- offered the same set again whenever it does not.+        banRest p range facts+            -- Said nothing: the range itself, untouched. A @difference@ against the+            -- empty set would give an equivalent but differently shaped set, and so+            -- change the search for every provider that states no facts.+            | [] <- stated = landed (noValues p range)+            | isEmpty leftover = (,) IntSet.empty+            | otherwise = landed (noValues p leftover)+          where+            leftover = case stated of+                []       -> range+                (s : ss) -> range `difference` foldr union s ss+            stated =+                [ s+                | inc <- facts+                , Map.size (incompTerms inc) == 1+                , Just (Positive s) <- [incompGet p inc]+                ]+            landed inc = first IntSet.singleton . insertClause inc

@@ -0,0 +1,250 @@+-- | The incompatibility store: what the solver has learned, in the order+-- propagation scans it, with facts that can be stated as one __merged as they+-- arrive__. Which facts those are is the domain's 'mergeRule'; for cabal,+-- dependency facts about the same pair of packages under the same guard, flag+-- declarations of the same flag, and unbuildable facts about the same package+-- for the same reasons ('PubGrub.Cabal').+--+-- == Why this is not just a list+--+-- PubGrub states identical dependencies of /adjacent versions of the depender/+-- as one incompatibility — @{foo >=1.0 && <1.3, not bar >=1.0 && <2}@ rather+-- than one fact per version of @foo@. There are two places to do that. When a+-- fact is generated, a provider can walk out from the release it was asked+-- about and read its neighbours to learn whether they carry the same+-- dependency; that costs a read per neighbour.+--+-- This module is the other place. The provider emits one fact per+-- release __slot__ — the half-open range up to the next release in the index —+-- so adjacent slots /touch/, and this module unions the depender terms of two+-- facts that agree about the dependee. @unionVersionSet@ then coalesces the+-- touching ranges into one contiguous interval. No neighbour is read /here/,+-- because the only releases that merge are ones the solver expanded anyway.+--+-- The rule is weaker than reading the neighbours: it collapses the releases+-- the solver expanded, not every release that carries the dependency. But+-- those are the only ones whose clauses exist, so for both things collapsing+-- is for — clauses to propagate, and lines in a proof — it is nearly as good.+--+-- == Why merging is sound+--+-- Two incompatibilities that state the same term about @q@:+--+-- @+-- ¬(p ∈ A ∧ q ∉ R)   and   ¬(p ∈ B ∧ q ∉ R)+-- @+--+-- together give @¬(p ∈ A∪B ∧ q ∉ R)@, since @p ∈ A∪B@ is @p ∈ A ∨ p ∈ B@ and the+-- conjunction distributes. Each half was established separately, so the union+-- claims nothing new — it is the /same/ knowledge in one clause instead of two,+-- which is exactly what makes it a stronger clause to propagate: a wider positive+-- term is satisfied by more of the partial solutions that can arise.+--+-- == The merged clause is a leaf, and that is the point for reports+--+-- It is rebuilt with its own constructor — 'PubGrub.Cabal.fromDependency',+-- 'PubGrub.Cabal.declaresFlag' or 'PubGrub.Cabal.unbuildable' — so its cause+-- stays a leaf cause with the unioned term. The alternative — letting conflict+-- resolution reach the same range by resolving the narrow facts against each+-- other — produces derived nodes, and those derived nodes /are/ the proof+-- lines this exists to remove: a proof that merges facts pairwise runs to+-- hundreds of lines. Merging at insert does not shorten those lines; it stops+-- them existing.+--+-- == Scan position is preserved, deliberately+--+-- The scan order decides /which/ clause propagation acts on when more than one+-- could fire, and through it which derivation is recorded first, which satisfier+-- a conflict finds, and so the shape of a proof. New knowledge goes to the front,+-- and a merge replaces the existing clause __where it already sits__ rather than+-- removing it and adding the result at the front, so learning that two facts were+-- one does not reorder anything the search has already settled on.+--+-- == What propagation reads+--+-- A clause's relation to the partial solution depends only on the accumulated+-- terms of the variables it mentions. So after an assignment to @v@ only the+-- clauses that mention @v@ can change their relation, and after a merge only the+-- merged clause can. The store keeps the index that turns that into a worklist,+-- which clauses mention each variable ('clausesOf'), and an insert answers with+-- the id the clause landed at, new or merged into. Which clauses are still to+-- be judged is propagation's business, not the store's ("PubGrub.Solver").+--+-- == What the store assumes of its rule, and what it does not+--+-- The store's invariants hold for any t'MergeRule'. It holds each key with its+-- part and never takes a merged clause apart again, so it assumes nothing about+-- what the rule builds; the rule's law is what makes a merge sound, and the store+-- does not depend on it. A merge may change which variables a clause mentions,+-- and the index follows it, dropping a variable no clause mentions any more.+-- 'valid' states every invariant the store keeps.+module PubGrub.Store+    ( Store+    , ClauseId+    , emptyStore+    , emptyStoreWith+    , storeClauses+    , insertClause+    , insertClauses+    , clauseAt+    , clausesOf+    , allClauses+    , storeSize+    , valid+    ) where++import           Data.IntMap.Strict      (IntMap)+import qualified Data.IntMap.Strict      as IntMap+import           Data.IntSet             (IntSet)+import qualified Data.IntSet             as IntSet+import           Data.Map.Strict         (Map)+import qualified Data.Map.Strict         as Map+import           PubGrub.Incompatibility (Domain (..), Incompatibility (..),+                                          MergeRule (..))++-- Specialised in the client, with the solver ("PubGrub.Solver" says why).+{-# INLINABLE emptyStore #-}+{-# INLINABLE insertClause #-}+{-# INLINABLE insertClauses #-}+{-# INLINABLE clausesOf #-}+{-# INLINABLE index #-}+{-# INLINABLE unindex #-}+{-# INLINABLE reindex #-}++-- | A clause's place in the scan order: higher is newer. A merge keeps the id of+-- the clause it merged into.+type ClauseId = Int++-- | The clauses by id, the index from a variable to the clauses that mention it,+-- and the merge rule with the clause each of its keys names.+data Store v = Store+    { stClauses :: !(IntMap (Incompatibility v))+    , stIndex   :: !(Map (v) IntSet)+    , stMerging :: !(MergeIndex v)+    , stNext    :: !ClauseId+    }++-- | The clause a key names, the key it first arrived with, and the part it has+-- grown to. Keys that compare equal may still differ, in how a range is spelled+-- for one, and a merged clause says what the first one said.+data Target k s = Target !ClauseId !k !s++-- | The rule's key for each clause that has one, mapped to that clause's id and+-- part, with the rule itself. The two types are the rule's own and existential,+-- as in t'MergeRule', and only here.+data MergeIndex v = forall k s. (Ord k, Semigroup s) => MergeIndex+    { miTargets :: !(Map k (Target k s))+    , miParts   :: Incompatibility v -> Maybe (k, s)+    , miBuild   :: k -> s -> Incompatibility v+    }++-- | The empty store, under the domain's 'mergeRule'.+emptyStore :: Domain v => Store v+emptyStore = emptyStoreWith mergeRule++-- | The empty store, under the given rule.+emptyStoreWith :: MergeRule v -> Store v+emptyStoreWith MergeRule{mergeParts, mergeBuild} =+    Store+        { stClauses = IntMap.empty+        , stIndex = Map.empty+        , stMerging = MergeIndex{miTargets = Map.empty, miParts = mergeParts, miBuild = mergeBuild}+        , stNext = 0+        }++-- | Where an arriving clause goes: the id it lands at, the clause that is there+-- afterwards, and the index with the clause's part added. A clause whose key is+-- free lands at the given id as it arrived; one whose key is taken lands at that+-- clause's id, as what the rule builds; one without a key leaves the index as it+-- was.+place :: ClauseId -> Incompatibility v -> MergeIndex v -> (ClauseId, Incompatibility v, MergeIndex v)+place c i mi@(MergeIndex targets parts build) = case parts i of+    Nothing -> (c, i, mi)+    Just (k, s) ->+        let slot Nothing = ((c, i), Just (Target c k s))+            slot (Just (Target t first old)) =+                let merged = old <> s+                 in ((t, build first merged), Just (Target t first merged))+            ((landed, clause), targets') = Map.alterF slot k targets+         in (landed, clause, MergeIndex targets' parts build)++-- | The clauses in scan order, newest first.+storeClauses :: Store v -> [Incompatibility v]+storeClauses Store{stClauses} = IntMap.foldl (flip (:)) [] stClauses++-- | Add a clause: merge it into the fact it agrees with, or put it at the front.+-- Either way, the id of the clause that results: the one merged into, or a new+-- one.+insertClause :: Domain v => Incompatibility v -> Store v -> (ClauseId, Store v)+insertClause i Store{stClauses, stIndex, stMerging, stNext} =+    case place stNext i stMerging of+        -- A merge lands on a clause that is there, in place: the id, and so the+        -- scan position, is the one it had, and the index moves only the+        -- variables the merge added or dropped.+        (c, landed, merging) ->+            ( c+            , Store+                { stClauses = IntMap.insert c landed stClauses+                , stIndex = case IntMap.lookup c stClauses of+                    Nothing       -> index c (incompTerms landed) stIndex+                    Just existing -> reindex c (incompTerms existing) (incompTerms landed) stIndex+                , stMerging = merging+                , stNext = if c == stNext then stNext + 1 else stNext+                }+            )++-- | Insert several clauses, preserving their order at the front: @insertClauses+-- [a,b,c]@ leaves the store scanning @a@, @b@, @c@, then what was there before,+-- except that a clause merged into an older one keeps that one's place. Answers+-- with the ids they landed at.+insertClauses :: Domain v => [Incompatibility v] -> Store v -> (IntSet, Store v)+insertClauses is store = foldr step (IntSet.empty, store) is+  where+    step i (!ids, !s) = case insertClause i s of+        (c, s') -> (IntSet.insert c ids, s')++-- | The clause with this id, if there is one.+clauseAt :: Store v -> ClauseId -> Maybe (Incompatibility v)+clauseAt Store{stClauses} c = IntMap.lookup c stClauses++-- | The clauses that mention a variable.+clausesOf :: Domain v => v -> Store v -> IntSet+clausesOf v Store{stIndex} = Map.findWithDefault IntSet.empty v stIndex++-- | Every clause.+allClauses :: Store v -> IntSet+allClauses Store{stClauses} = IntMap.keysSet stClauses++-- | How many clauses there are. A pass over them, allocating nothing.+storeSize :: Store v -> Int+storeSize Store{stClauses} = IntMap.size stClauses++-- | Every invariant the store keeps, for the tests:+--+-- * the index is exactly the variables the clauses mention, each mapped to the+--   clauses that mention it, so no variable maps to no clause;+-- * every key names a clause that is there, and no two keys name the same one;+-- * every id is below the next one.+valid :: Domain v => Store v -> Bool+valid Store{stClauses, stIndex, stMerging = MergeIndex{miTargets}, stNext} =+    stIndex == mentions+        && all (`IntMap.member` stClauses) targets+        && IntSet.size (IntSet.fromList targets) == length targets+        && maybe True ((< stNext) . fst) (IntMap.lookupMax stClauses)+  where+    clauses = IntMap.toList stClauses+    mentions = Map.fromListWith IntSet.union [(v, IntSet.singleton c) | (c, i) <- clauses, v <- Map.keys (incompTerms i)]+    targets = [t | Target t _ _ <- Map.elems miTargets]++-- | File a clause under each variable it mentions, and the inverse. 'unindex'+-- drops a variable that no clause mentions any more.+index, unindex :: Ord v => ClauseId -> Map v a -> Map v IntSet -> Map v IntSet+index c terms ix = Map.foldlWithKey' (\acc v _ -> Map.insertWith IntSet.union v (IntSet.singleton c) acc) ix terms+unindex c terms ix = Map.foldlWithKey' (\acc v _ -> Map.update without v acc) ix terms+  where+    without cs = let cs' = IntSet.delete c cs in if IntSet.null cs' then Nothing else Just cs'++-- | Move a clause's filing from its old terms to its new ones: only the+-- variables it stopped or started mentioning change.+reindex :: Ord v => ClauseId -> Map v a -> Map v a -> Map v IntSet -> Map v IntSet+reindex c old new = index c (Map.difference new old) . unindex c (Map.difference old new)

@@ -0,0 +1,181 @@+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE TypeFamilies       #-}++-- | Terms: statements about the value of one variable, and the Boolean+-- operations on them. 'Term' says what the two kinds of term mean.+module PubGrub.Term+    ( Term (..)+    , negateTerm+    , anyTerm+    , isTopTerm+    , isBottomTerm+      -- * The operations, by name+      -- | The same as the 'SetOps' methods of @'Term' s@, for use where the+      -- class is not wanted.+    , intersectTerm+    , unionTerm+    , differenceTerm+    , isEmptyTerm+    ) where++import           PubGrub.SetOps++-- $setup+-- >>> import qualified Data.Set as Set+-- >>> import Data.Set (Set)+-- >>> import PubGrub.SetOps++-- Specialised in the client, with the solver ("PubGrub.Solver" says why).+{-# INLINABLE intersectTerm #-}+{-# INLINABLE unionTerm #-}+{-# INLINABLE differenceTerm #-}+{-# INLINABLE isEmptyTerm #-}+{-# INLINABLE anyTerm #-}+{-# INLINABLE isTopTerm #-}+{-# INLINABLE isBottomTerm #-}++-- ---------------------------------------------------------------------------+-- Term+-- ---------------------------------------------------------------------------++-- | A statement about the value of one variable in a solution, given a set+-- @s@ of its values.+--+--   * @Positive s@: the variable has a value, and it is in @s@.+--   * @Negative s@: the variable has no value, or its value is not in @s@.+--+-- A variable a solution leaves out has no value, and only a negative term is+-- true of it. @Negative s@ is exactly the negation of @Positive s@; it is not+-- @Positive@ of the values outside @s@, which would still require a value.+--+-- So a term stands for a set of /states/ of the variable: each of its values,+-- plus one more, /absent/. A positive term is a set of states without absent,+-- a negative term one with it, and every set of states has exactly one term.+-- Absent is what separates the two: every positive term is a subset of+-- @Negative ∅@, the term that is always true, but no negative term is a subset+-- of a positive one.+--+-- >>> Positive (Set.fromList [1,2]) `isSubsetOf` (Negative Set.empty :: Term (Set Int))+-- True+--+-- >>> (Negative Set.empty :: Term (Set Int)) `isSubsetOf` Positive (Set.fromList [1,2])+-- False+data Term a+    = Positive a+    | Negative a+    deriving (Eq, Ord, Show)++-- | Negation: the other polarity over the same set.+negateTerm :: Term a -> Term a+negateTerm (Positive s) = Negative s+negateTerm (Negative s) = Positive s++-- | The states both terms allow.+intersectTerm :: SetOps s => Term s -> Term s -> Term s+intersectTerm (Positive x) (Positive y) = Positive (x `intersect` y)+intersectTerm (Positive x) (Negative y) = Positive (x `difference` y)+intersectTerm (Negative x) (Positive y) = Positive (y `difference` x)+intersectTerm (Negative x) (Negative y) = Negative (x `union` y)++-- | The states either term allows.+unionTerm :: SetOps s => Term s -> Term s -> Term s+unionTerm (Positive x) (Positive y) = Positive (x `union` y)+unionTerm (Positive x) (Negative y) = Negative (y `difference` x)+unionTerm (Negative x) (Positive y) = Negative (x `difference` y)+unionTerm (Negative x) (Negative y) = Negative (x `intersect` y)++-- | The states the first term allows and the second does not.+differenceTerm :: SetOps s => Term s -> Term s -> Term s+differenceTerm x y =+    x `intersectTerm` negateTerm y++-- | Does the term allow no state? Only a positive term over an empty set.+isEmptyTerm :: SetOps s => Term s -> Bool+isEmptyTerm (Positive s) = isEmpty s+isEmptyTerm (Negative _) = False+++-- | The Boolean algebra on sets of states. It needs only 'intersect', 'union'+-- and 'difference' of the sets, never a complement: each case follows from+-- whether absent is in or out.+--+-- >>> Positive (Set.fromList [2,3,4]) `intersect` Negative (Set.fromList [4,5])+-- Positive (fromList [2,3])+--+-- >>> Negative (Set.fromList [2]) `intersect` Negative (Set.fromList [4])+-- Negative (fromList [2,4])+--+-- A union of prohibitions only forbids what both prohibit:+--+-- >>> Negative (Set.fromList [5,6]) `union` Negative (Set.fromList [6,7])+-- Negative (fromList [6])+--+-- Subtracting a negative term removes absent, so the result is positive:+--+-- >>> Negative (Set.fromList [1]) `difference` Negative (Set.fromList [0,1,2])+-- Positive (fromList [0,2])+--+-- Only a positive term over the empty set is empty; a negative term always+-- allows absent:+--+-- >>> isEmpty (Negative Set.empty :: Term (Set Int))+-- False+instance SetOps a => SetOps (Term a) where+    {-# INLINABLE intersect #-}+    {-# INLINABLE union #-}+    {-# INLINABLE difference #-}+    {-# INLINABLE isEmpty #-}+    {-# INLINABLE isSubsetOf #-}+    {-# INLINABLE isDisjoint #-}+    empty = Positive empty+    intersect = intersectTerm+    union = unionTerm+    difference = differenceTerm+    isEmpty = isEmptyTerm++    -- The two tests by cases on polarity, so that neither builds a term. Each+    -- case is the default definition evaluated by hand: P x ⊆ N y is+    -- isEmpty (P (x ∩ y)), N x ⊆ N y is isEmpty (P (y \ x)), and a negative+    -- term is never empty, which is why N x ⊆ P y is False and two negative+    -- terms are never disjoint.++    isSubsetOf (Positive x) (Positive y) = x `isSubsetOf` y+    isSubsetOf (Positive x) (Negative y) = x `isDisjoint` y+    isSubsetOf (Negative _) (Positive _) = False+    isSubsetOf (Negative x) (Negative y) = y `isSubsetOf` x++    isDisjoint (Positive x) (Positive y) = x `isDisjoint` y+    isDisjoint (Positive x) (Negative y) = x `isSubsetOf` y+    isDisjoint (Negative x) (Positive y) = y `isSubsetOf` x+    isDisjoint (Negative _) (Negative _) = False++-- | The term that is always true, ⊤: \"absent, or any value\". An+-- incompatibility never holds it, since it says nothing, and a variable an+-- incompatibility does not mention stands for it.+--+-- >>> isTopTerm (anyTerm :: Term (Set Int))+-- True+anyTerm :: SetOps a => Term a+anyTerm = Negative empty++-- | Is this the term that is always true?+--+-- >>> isTopTerm (Negative Set.empty :: Term (Set Int))+-- True+isTopTerm :: SetOps a => Term a -> Bool+isTopTerm (Negative s) = isEmpty s+isTopTerm (Positive _) = False++-- | Is this the term that is never true, ⊥: \"a value, in ∅\"? Only a positive+-- term can be, because a negative term is true of absent. In particular+-- @Negative@ of all of a variable's values, \"the variable has no value\", can+-- be true and is not ⊥.+--+-- >>> isBottomTerm (Positive Set.empty :: Term (Set Int))+-- True+--+-- >>> isBottomTerm (Negative (Set.fromList [1,2]) :: Term (Set Int))+-- False+isBottomTerm :: SetOps a => Term a -> Bool+isBottomTerm (Positive s) = isEmpty s+isBottomTerm (Negative _) = False

@@ -0,0 +1,312 @@+{-# OPTIONS_GHC -Wno-unused-imports #-}++-- | A first solve: from an empty file to a plan, and from a broken world to an+-- explanation of why it has no plan.+--+-- PubGrub is a version solver. Given packages, their versions and what each+-- version needs, it chooses versions that fit together, which we call a /plan/,+-- or, when no such choice exists, it explains why.+--+-- In this tutorial we will describe a small world of three packages to the+-- solver, ask it for a plan, and then break the world so that no plan exists+-- and have the solver say why. Along the way we will meet the four things a use+-- of the library involves: a /domain/, the /incompatibilities/ stated in it,+-- a /provider/ that answers the solver's questions, and a /formatter/ that puts+-- a failure into words.+--+-- Everything we write goes into one file, @Toy.hs@, built up a piece at a time.+-- Each piece goes at the end of the file. The packages here are not Haskell+-- packages: they are names with numbered versions, and that is all the solver+-- needs.+module PubGrub.Tutorial+    ( -- * Setting up+      -- $settingUp++      -- * Describing the domain+      -- $domain++      -- * Stating what is known+      -- $facts++      -- * Describing a world+      -- $world++      -- * Answering the solver's questions+      -- $provider++      -- * Solving+      -- $solving++      -- * Breaking the world+      -- $breaking++      -- * Explaining the failure+      -- $explaining++      -- * Where to go from here+      -- $next+    ) where++import           PubGrub++-- $settingUp+--+-- Make a new directory with two files in it. The first is @toy.cabal@:+--+-- @+-- cabal-version: 3.0+-- name:          toy+-- version:       0+--+-- library+--     exposed-modules:  Toy+--     build-depends:    base, containers, pubgrub, text+--     default-language: GHC2021+-- @+--+-- The second is @Toy.hs@, which starts with the extensions, the module name and+-- the imports we will need:+--+-- > {-# LANGUAGE OverloadedStrings #-}+-- > {-# LANGUAGE TypeFamilies      #-}+-- >+-- > module Toy where+-- >+-- > import           Data.Functor.Identity (Identity, runIdentity)+-- > import           Data.List             (maximumBy)+-- > import           Data.Map.Strict       (Map)+-- > import qualified Data.Map.Strict       as Map+-- > import           Data.Ord              (comparing)+-- > import           Data.Set              (Set)+-- > import qualified Data.Set              as Set+-- > import           Data.Text             (Text)+-- > import qualified Data.Text             as T+-- > import qualified Data.Text.IO          as T+-- > import           PubGrub+--+-- Start a session in that directory with @cabal repl@. After cabal has built+-- the dependencies, GHCi says @Ok, one module loaded.@ and gives you a @ghci>@+-- prompt. Keep this session open. Each time you add to @Toy.hs@, type @:reload@+-- and check that it says @Ok, one module reloaded.@++-- $domain+--+-- The solver does not know what it is solving for. We tell it, by making the+-- type of the /variables/ (here, a package) an instance of 'Domain' that names+-- three more types: what a /value/ is (a version), what a /set of values/ is,+-- and what a /fact/ about the world is. The solver does not interpret a fact:+-- facts are what explanations are made from, and we will use them at the end.+--+-- Add to @Toy.hs@:+--+-- > newtype Pkg = Pkg String+-- >     deriving (Eq, Ord, Show)+-- >+-- > data ToyFact+-- >     = Wants Pkg (Set Int)+-- >     | Needs Pkg Int Pkg (Set Int)+-- >+-- > instance Domain Pkg where+-- >     type ValueOf Pkg = Int+-- >     type SetOf Pkg = Set Int+-- >     type FactOf Pkg = ToyFact+-- >     singleton _ v = Set.singleton v+--+-- The variable type names the domain: the library's types that belong to a+-- domain take it as a parameter, so an @Incompatibility Pkg@ is one about these+-- packages. @Pkg@ is a newtype rather than @String@ so that the instance is+-- ours. 'singleton' is the one function the domain has to supply: the set+-- that holds exactly one value.+--+-- A @ToyFact@ is either a request (/we want @app@ at one of these versions/) or a+-- dependency (/@lib@ version 1 needs @util@ at one of these versions/).++-- $facts+--+-- Everything the solver knows is an t'Incompatibility': a set of terms, one per+-- variable, that cannot /all/ be true at once. A term is either+-- 'Positive', \"the package is picked, at a version in this set\", or+-- 'Negative', \"the package is not picked at a version in this set\". Each+-- incompatibility also records why it holds: the fact it comes from, which+-- is either something we ask for, built with 'seed', or something the world+-- says, built with 'fact'.+--+-- Add two functions that state our two kinds of fact:+--+-- > wants :: Pkg -> [Int] -> Incompatibility Pkg+-- > wants p vs = seed (Wants p (Set.fromList vs)) p (Negative (Set.fromList vs))+-- >+-- > needs :: Pkg -> Int -> Pkg -> [Int] -> Incompatibility Pkg+-- > needs p v q ws =+-- >     fact (Needs p v q (Set.fromList ws)) [(p, Positive (Set.singleton v)), (q, Negative (Set.fromList ws))]+--+-- Reload, and look at what a dependency says:+--+-- @+-- ghci> incompTerms (needs (Pkg \"lib\") 1 (Pkg \"util\") [1])+-- fromList [(Pkg \"lib\",Positive (fromList [1])),(Pkg \"util\",Negative (fromList [1]))]+-- @+--+-- It says that \"@lib@ is picked at 1\" and \"@util@ is not picked at 1\"+-- cannot both be true: if @lib@ is 1, then @util@ is 1. A request has a single+-- negative term, so \"@app@ is not picked at 1\" cannot be true, and @app@ must+-- be picked at 1. A request is a seed and a dependency is a fact, and the+-- solver treats the two differently when it decides that it has failed.++-- $world+--+-- Now some packages. A world lists each package's versions and, for each+-- version, what it needs. Add:+--+-- > type World = Map Pkg [(Int, [(Pkg, [Int])])]+-- >+-- > app, lib, util :: Pkg+-- > app = Pkg "app"+-- > lib = Pkg "lib"+-- > util = Pkg "util"+-- >+-- > world :: World+-- > world =+-- >     Map.fromList+-- >         [ (app, [(1, [(lib, [1, 2])])])+-- >         , (lib, [(1, [(util, [1])]), (2, [(util, [2])])])+-- >         , (util, [(1, [])])+-- >         ]+--+-- So @app@ 1 needs @lib@ 1 or 2, @lib@ 1 needs @util@ 1, @lib@ 2 needs @util@+-- 2, and the only version of @util@ is 1.++-- $provider+--+-- The solver never sees the world. When it needs a package, it asks a+-- t'Provider': here is the package, and here is the set of versions still+-- allowed; pick one, and tell me what that choice entails. Add:+--+-- > provider :: World -> Provider Pkg Identity+-- > provider w = Provider $ \p offered ->+-- >     pure $ case [(v, deps) | (v, deps) <- Map.findWithDefault [] p w, v `Set.member` offered] of+-- >         [] -> (Nothing, [])+-- >         candidates ->+-- >             let (v, deps) = maximumBy (comparing fst) candidates+-- >              in (Just v, [needs p v q ws | (q, ws) <- deps])+--+-- Our provider picks the newest version the set allows, and states that+-- version's dependencies with @needs@. If no version is allowed, it answers+-- 'Nothing'. It runs in 'Data.Functor.Identity.Identity' because it needs no+-- effects; a provider that reads files would run in 'IO'.+--+-- Reload, and ask it the question the solver will ask about @lib@:+--+-- @+-- ghci> fst (runIdentity (expand (provider world) lib (Set.fromList [1, 2])))+-- Just 2+-- @++-- $solving+--+-- To solve, hand 'solve' the provider and the requests. Its first argument+-- receives a message at each step of the search; 'mempty' discards them. Add:+--+-- > plan :: World -> [Incompatibility Pkg] -> Maybe (Map Pkg Int)+-- > plan w seeds = case runIdentity (solve mempty (provider w) seeds) of+-- >     Right solution -> Just solution+-- >     Left _         -> Nothing+--+-- Reload, and ask for @app@ 1:+--+-- @+-- ghci> plan world [wants app [1]]+-- Just (fromList [(Pkg \"app\",1),(Pkg \"lib\",1),(Pkg \"util\",1)])+-- @+--+-- Notice that @lib@ is 1, though the provider prefers 2. The provider did pick+-- @lib@ 2 first. That made the solver ask for @util@ 2, the provider found no+-- such version, and the solver went back and asked for @lib@ again, this time+-- without 2.++-- $breaking+--+-- Replace @util@ 1 with a @util@ 3 that no @lib@ accepts. Add:+--+-- > broken :: World+-- > broken = Map.insert util [(3, [])] world+--+-- @+-- ghci> plan broken [wants app [1]]+-- Nothing+-- @+--+-- There is no plan, and 'Nothing' does not say why.++-- $explaining+--+-- When there is no plan, 'solve' answers @'Left' ('NoSolution' root)@. The+-- incompatibility @root@ carries the whole chain of reasoning that led to the+-- failure, and 'reportConflict' writes it out as a proof. It needs a+-- t'Formatter', which 'mkFormatter' builds from three things: the words for+-- each fact, the words for the solver's own finding that a package has none+-- of a set of versions, and how to name a package with a set of versions,+-- from which the conclusions are made. Any other 'Left' is not a verdict on+-- the world but a bug, in our requests, in our provider or in the solver, and+-- @why@ says only that. Add:+--+-- > versions :: Set Int -> Text+-- > versions vs = T.intercalate " or " (map (T.pack . show) (Set.toList vs))+-- >+-- > name :: Pkg -> Set Int -> Text+-- > name (Pkg p) vs = T.pack p <> " " <> versions vs+-- >+-- > formatter :: Formatter Pkg+-- > formatter = mkFormatter says hole name+-- >   where+-- >     says (Wants p vs) _     = name p vs <> " is requested"+-- >     says (Needs p v q ws) _ = name p (Set.singleton v) <> " depends on " <> name q ws+-- >     hole (Pkg p) vs = T.pack p <> " has no version " <> versions vs+-- >+-- > why :: World -> [Incompatibility Pkg] -> Text+-- > why w seeds = case runIdentity (solve mempty (provider w) seeds) of+-- >     Right _                -> "There is a plan."+-- >     Left (NoSolution root) -> reportConflict formatter root+-- >     Left _                 -> "The solver failed unexpectedly."+-- >+-- > explain :: World -> [Incompatibility Pkg] -> IO ()+-- > explain w seeds = T.putStrLn (why w seeds)+--+-- Reload, and ask why the broken world has no plan:+--+-- @+-- ghci> explain broken [wants app [1]]+-- 1. Because lib 1 depends on util 1 and util has no version 1, lib 1 is forbidden.+--+-- Because util has no version 2 and lib 2 depends on util 2, lib 2 is forbidden.+-- And because lib 1 is forbidden (1), lib 1 or 2 is forbidden.+-- So, because app 1 depends on lib 1 or 2 and app 1 is requested, version solving failed.+-- @+--+-- Each line takes facts, or an earlier conclusion, and draws a new conclusion.+-- The first line is numbered because a later line uses it. The last line rests+-- on the request, @app 1@: everything above it shows that the request cannot be+-- met. What each fact says and how a package is named came from our @formatter@;+-- the connectives, and words such as \"is forbidden\", are the library's.+--+-- The original world still has a plan, and @explain@ says so:+--+-- @+-- ghci> explain world [wants app [1]]+-- There is a plan.+-- @+--+-- We have described a domain to the solver, answered its questions with a+-- provider, found a plan, and turned a failure into an explanation in our own+-- words.++-- $next+--+-- * "PubGrub" is the library's front page, with everything this tutorial used.+-- * "PubGrub.Cookbook" has recipes for what comes next: versions and ranges, a+--   provider over an index of releases, explanations in a domain's own words.+-- * "PubGrub.Provider" states what a provider must and may do.+-- * "PubGrub.Report" describes the rest of t'Formatter', for wording proofs in a+--   domain's own terms.+-- * "PubGrub.Version" and "PubGrub.VersionSet" are ready-made values and sets+--   for a domain whose values are versions with ranges.

@@ -0,0 +1,66 @@+-- | Versions: a list of numbers, such as @1.2.0@, ordered component by+-- component, for a domain whose values are versions. "PubGrub.VersionSet" is+-- the matching set type.+--+-- __Trailing zeros are insignificant__: @1.2@, @1.2.0@ and @1.2.0.0@ are one+-- version, equal under 'Eq' and 'Ord'. Each keeps its spelling for display+-- ('versionNumbers'), and the comparisons read the 'normalForm', the spelling+-- with its trailing zeros dropped.+--+-- An order in which @1.2 < 1.2.0@ would put room between two spellings of one+-- version, where no version can ever be, and every set would have to carry+-- it: @>=1.2 && <1.2.0@ would be a range that looks open and holds nothing,+-- which a search can only discover by asking. With trailing zeros+-- insignificant there is no such range, and a bound @>=1.8.0@ admits the+-- version spelled @1.8@, as its author means. Two values that spell one version+-- differently are one value here, so a domain that has both has to keep one.+module PubGrub.Version+    ( Version+    , mkVersion+    , versionNumbers+    , normalForm+    , version0+    ) where++import           Data.Ord (comparing)++-- | A version: its spelling, and its normal form. Build one with 'mkVersion'.+data Version = Version+    { versionNumbers :: ![Int]+    -- ^ the components as spelled — @[1,2,0,0]@ for @1.2.0.0@, not the normal+    -- form+    , normalForm     :: ![Int]+    -- ^ the spelling with trailing zeros dropped, keeping at least one+    -- component. What 'Eq' and 'Ord' compare.+    }++-- The normal form is a field, computed once by 'mkVersion', because 'Eq' and+-- 'Ord' read it on every comparison and a solve compares versions far more+-- often than it makes them. Deriving it on each comparison cost a fifth of a+-- large solve's time and a third of its allocation.++instance Eq Version where+    a == b = normalForm a == normalForm b++instance Ord Version where+    compare = comparing normalForm++-- | As the expression that makes it: @mkVersion [1,2,0]@.+instance Show Version where+    showsPrec d v =+        showParen (d > 10) (showString "mkVersion " . showsPrec 11 (versionNumbers v))++-- | A version from its components, as spelled. An empty list is the version+-- @0@, and a negative component is taken as @0@.+mkVersion :: [Int] -> Version+mkVersion [] = version0+mkVersion ns = Version spelled normal+  where+    spelled = map (max 0) ns+    normal = case reverse (dropWhile (== 0) (reverse spelled)) of+        [] -> [0]+        ms -> ms++-- | The version @0@, the lowest there is. Every version set starts here.+version0 :: Version+version0 = Version [0] [0]

@@ -0,0 +1,411 @@+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE OverloadedStrings  #-}+{-# LANGUAGE TypeFamilies       #-}++-- | A version set: a canonical, sorted, disjoint, non-adjacent collection of+-- version intervals over 'PubGrub.Version.Version', each interval a pair of+-- bound positions (@Cut@). 'Eq' compares the intervals alone, so structural+-- equality coincides with semantic equality.+--+-- Beside the intervals, a set remembers the __declared spelling__ it was built+-- from, when it was built from one. That tag is a display hint and nothing more:+-- only 'declare' sets it, every operation below drops it, 'Eq' and 'Ord' cannot+-- see it, and 'PubGrub.Pretty.Pretty' hands it back so a report quotes a range the way its+-- author wrote it — @^>=4.13.0.0@ rather than @>=4.13.0.0 && <4.14@: the same+-- intervals as a plain range, plus the knowledge of how it was spelled. A+-- derived term has no author, and prints canonically ('renderVersionSet').+--+-- Union, intersection and complement are computed /directly on the intervals/,+-- as one pass of comparisons between bound positions, and the result is+-- canonical by construction. Parsing range syntax is a domain's business: a+-- domain builds a set from a declared range with the constructors and+-- operations below, and tags it with 'declare'.+--+-- Versions compare with trailing zeros insignificant ("PubGrub.Version"), so+-- @>=4.13 && <4.14 || >=4.14.0.0 && <4.15@ is __one__ interval, and+-- @>=0.3 && <0.3.0.0@ is empty.+module PubGrub.VersionSet (+    -- The constructor is hidden, so that every 'VersionSet' stays canonical.+    VersionSet,+    Cut (..),+    Side (..),+    emptyVersionSet,+    fullVersionSet,+    singletonVersionSet,+    halfOpenVersionSet,+    aboveVersionSet,+    belowVersionSet,+    snapToVersions,+    fillGaps,+    declare,+    declared,+    renderVersionSet,+    complementVersionSet,+    unionVersionSet,+    intersectionVersionSet,+    contains,+    intervals,+) where++import           Data.List       (intercalate)+import           Data.Maybe      (mapMaybe)+import           Data.Ord        (Down (..), comparing)+import           Data.Set        (Set)+import qualified Data.Set        as Set+import           Data.Text       (Text)+import qualified Data.Text       as T+import           PubGrub.SetOps  (SetOps (..))+import           PubGrub.Version (Version, version0, versionNumbers)+++-- | A position on the version line, fine enough to tell "up to but not+-- including @v@" from "up to and including @v@". Every interval bound is one of+-- these, and every operation below is comparisons between them.+--+-- 'Unbounded' is deliberately the /last/ constructor, so the derived 'Ord' puts+-- it above every position: a set with no upper bound reaches higher than any+-- bounded one.+data Cut+    = Cut Version Side+    | Unbounded+    deriving stock (Eq, Ord, Show)++-- | Which side of its version a cut falls on. An interval /starting/ at+-- @Before v@ contains @v@; one /ending/ there does not. @After v@ is the mirror+-- image. This is the whole trick: inclusive and exclusive bounds become two+-- neighbouring positions, so "does this interval touch that one" is @<=@.+data Side = Before | After+    deriving stock (Eq, Ord, Show)++-- | The later of two positions, and the earlier. At the __same__ position — two+-- spellings of one version, since 'Eq' on 'Version' ignores trailing zeros — the+-- shorter spelling is kept. Either denotes the set; the shorter one is what a+-- declared @>=2.0@ was written as, where the release's slot says @2.0.0.0@, and it+-- is what a derived term should print.+laterCut, earlierCut :: Cut -> Cut -> Cut+laterCut a b = case compare a b of+    LT -> b+    GT -> a+    EQ -> shorterCut a b+earlierCut a b = case compare a b of+    LT -> a+    GT -> b+    EQ -> shorterCut a b++shorterCut :: Cut -> Cut -> Cut+shorterCut a@(Cut v _) b@(Cut w _)+    | length (versionNumbers w) < length (versionNumbers v) = b+    | otherwise = a+shorterCut a _ = a++-- | A set as the cut pairs bounding its intervals: sorted, disjoint, and+-- separated by at least one position (that last part is what "non-adjacent"+-- means here, and what every operation below has to preserve).+cutsOf :: VersionSet -> [(Cut, Cut)]+cutsOf = intervals++-- | Back from cut pairs, dropping the empty ones — which is where @>=2 && <2@+-- and friends disappear. An interval is empty exactly when its bounds are the+-- same position or crossed, so canonicalisation is a comparison. The input must+-- already be sorted and non-adjacent; every caller below arranges that.+fromCuts :: [(Cut, Cut)] -> VersionSet+fromCuts cs = VersionSet (filter nonEmpty cs) Nothing+  where+    nonEmpty (Unbounded, _) = False -- a lower bound above every version: empty+    nonEmpty (lo, hi)       = lo < hi++-- | A set of versions: a list of intervals, and the spelling it was declared+-- with, if any. Build one with the functions below; it is canonical, so 'Eq'+-- is equality of sets.+data VersionSet = VersionSet+    { intervals :: [(Cut, Cut)]+    -- ^ The intervals, in order, each as its lower and upper bound.+    , declared  :: Maybe Text+    -- ^ The spelling this set was built from by 'declare', if it was, and+    -- 'Nothing' for anything an operation produced. It always denotes exactly+    -- 'intervals'. Equality and order ignore it.+    }+    deriving stock (Show)++instance Eq VersionSet where+    a == b = intervals a == intervals b++-- | Order by how high the set reaches, then by how wide it is, then by the+-- full cut list — the third coordinate is arbitrary and exists only to+-- keep the order total and consistent with 'Eq' (two distinct sets+-- can share a reach and a start: @[1,2) ∪ [3,4)@ and @[1,4)@).+--+-- The empty set has neither reach nor start; @Nothing@ sorts below every+-- @Just@, so it is the minimum.+instance Ord VersionSet where+    compare = comparing sortKey+      where+        sortKey vs =+            ( reachOf vs+            , Down (startOf vs)               -- wider (lower start) ranks higher+            , cutsOf vs+            )++        reachOf vs = case reverse (cutsOf vs) of+            (_, hi) : _ -> Just hi+            []          -> Nothing++        startOf vs = case cutsOf vs of+            (lo, _) : _ -> Just lo+            []          -> Nothing++-- | Tag a set with the spelling it was built from. This is the one place the+-- tag is set: a range that arrives here was written by someone, and that+-- spelling is what a report should quote back. The caller vouches that the+-- spelling denotes exactly the set.+declare :: Text -> VersionSet -> VersionSet+declare spelling vs = vs{declared = Just spelling}++-- | The intervals as text: @>=a && <b@ pieces joined by @||@, a one-version+-- interval as @==v@, a lower bound at @0@ left out, every version as @>=0@ and+-- none as @<0@. The 'PubGrub.Pretty.Pretty' instance prefers the 'declared'+-- spelling where there is one, so a range is quoted the way its author wrote+-- it, and uses this otherwise.+renderVersionSet :: VersionSet -> Text+renderVersionSet vs = case map interval (cutsOf vs) of+    [] -> "<0"+    rs -> T.intercalate " || " rs+  where+    interval (Cut v Before, Cut w After) | v == w = "==" <> spell v+    interval (lo, hi) = case (lower lo, upper hi) of+        (Nothing, Nothing) -> ">=0"+        (Just l, Nothing)  -> l+        (Nothing, Just u)  -> u+        (Just l, Just u)   -> l <> " && " <> u++    lower (Cut v Before)+        | v == version0 = Nothing+        | otherwise = Just (">=" <> spell v)+    lower (Cut v After) = Just (">" <> spell v)+    lower Unbounded = Nothing -- unreachable: 'fromCuts' drops such an interval++    upper Unbounded      = Nothing+    upper (Cut w Before) = Just ("<" <> spell w)+    upper (Cut w After)  = Just ("<=" <> spell w)++    spell = T.pack . intercalate "." . map show . versionNumbers++-- | No versions.+emptyVersionSet :: VersionSet+emptyVersionSet = VersionSet [] Nothing++-- | Every version.+fullVersionSet :: VersionSet+fullVersionSet = fromCuts [(Cut version0 Before, Unbounded)]++-- | The set containing exactly one version.+singletonVersionSet :: Version -> VersionSet+singletonVersionSet v = fromCuts [(Cut v Before, Cut v After)]++-- | The half-open interval @[lo, hi)@, unbounded above when there is no @hi@.+-- Empty if @hi <= lo@.+--+-- This is the shape to reach for when naming /one release/ out of an index whose+-- version list you know: pass the release and the next existing release above it.+-- The interval then contains exactly that one real release, so it denotes the same+-- instances as @'singletonVersionSet' lo@ over anything that can actually be+-- offered — but unlike the singleton it __touches its neighbour__, and touching+-- intervals coalesce (see 'unionVersionSet'). So @[v1,v2)@ and @[v2,v3)@ join into+-- @[v1,v3)@ on their own, where @{v1}@ and @{v2}@ stay two pieces, and removing+-- @[v1,v2)@ leaves no empty @(v1,v2)@ behind for the solver to learn about+-- separately. A fact stated over such slots for each of several neighbouring+-- releases therefore merges into one fact over a single range.+halfOpenVersionSet :: Version -> Maybe Version -> VersionSet+halfOpenVersionSet lo hi = fromCuts [(Cut lo Before, maybe Unbounded (`Cut` Before) hi)]++-- | Everything strictly above @lo@: the set @>lo@.+aboveVersionSet :: Version -> VersionSet+aboveVersionSet lo = fromCuts [(Cut lo After, Unbounded)]++-- | Everything below @hi@, or everything when there is no @hi@: the slot of a+-- package's __first__ release, which has no lower bound: a proof says+-- @foo <1.1@, not @foo >=1.0 && <1.1@. Nothing is published below the first+-- release, so the set denotes the same instances as the half-open slot would —+-- but its complement is @>=hi@ and not @<lo || >=hi@, and the @<lo@ piece is a+-- hole the solver would otherwise have to learn is empty, one @no version for@+-- at a time.+belowVersionSet :: Maybe Version -> VersionSet+belowVersionSet hi = fromCuts [(Cut version0 Before, maybe Unbounded (`Cut` Before) hi)]++-- | Narrow every interval to the versions in @universe@ that it actually+-- contains: each becomes the closed range from its lowest such version to its+-- highest, and intervals holding none are dropped.+--+-- The result is a __subset__ of the input denoting the __same__ versions of+-- @universe@ — it only ever removes version space nothing occupies. That is what+-- makes it safe to apply to a declared dependency range once the index's version+-- list is known: @>=0.2@ against a package whose oldest release is @0.5.1.0@+-- becomes @>=0.5.1.0@, so banning that release empties the set instead of leaving+-- a live-looking @>=0.2 && <0.5.1.0@ for the solver to refute separately.+--+-- Narrowing, never widening, is deliberate. The dual operation (widening each+-- interval out to the next existing version, as 'halfOpenVersionSet' does for a+-- release's slot) denotes the same versions just as soundly, but it would report+-- a declared @<5@ back to its author as @<=4.21.0.0@. A subset cannot overstate+-- what was declared.+--+-- Takes the universe as a 'Set' so each interval costs two ordered lookups rather+-- than a pass over every version of the package.+--+-- __Not for declared ranges.__ Applied to them, it rewrites every quoted range+-- in a closed form nobody wrote: a user's own @lens <4@ comes back as+-- @lens >=0.1 && <=3.10.3@ on the proof's last line. That objection holds+-- whatever it would save. 'fillGaps' is the half of this that does not touch an+-- outer bound.+snapToVersions :: Set Version -> VersionSet -> VersionSet+snapToVersions universe vs = fromCuts (mapMaybe tighten (cutsOf vs))+  where+    tighten (lo, hi) = do+        a <- lowest lo+        b <- highest hi+        if a <= b then Just (Cut a Before, Cut b After) else Nothing++    -- The lowest member of the universe at or above the interval's lower bound.+    -- @Before v@ admits @v@ itself, @After v@ does not — the same distinction the+    -- cut makes.+    lowest (Cut v Before) = Set.lookupGE v universe+    lowest (Cut v After)  = Set.lookupGT v universe+    lowest Unbounded      = Nothing  -- a lower bound above every version: empty++    -- And the highest at or below the upper bound, mirrored: an interval ending+    -- @Before w@ excludes @w@, one ending @After w@ includes it.+    highest (Cut w Before) = Set.lookupLT w universe+    highest (Cut w After)  = Set.lookupLE w universe+    highest Unbounded      = Set.lookupMax universe++-- | Fill every gap between two intervals that no member of @universe@ occupies.+-- The outer bounds are never touched; only interior holes go. The result is a+-- __superset__ of the input denoting the __same__ members of the universe, and+-- it carries no 'declared' spelling, since it is no longer what anyone wrote.+--+-- This is the other half of 'snapToVersions', and the half that is safe to show+-- an author: a declared @>=4.7 && <5@ is left alone, while @>=1.0 && <1.2 ||+-- >=1.3 && <2@ against a package with nothing published in @[1.2, 1.3)@+-- becomes @>=1.0 && <2@.+--+-- A single interval costs nothing here. Each gap costs one ordered lookup.+--+-- It is not meant for declared ranges, because a filled set has to drop its+-- 'declared' spelling, and an explanation should quote the author's own+-- spelling. It suits a __derived__ set, which nobody wrote and which prints+-- canonically anyway.+fillGaps :: Set Version -> VersionSet -> VersionSet+fillGaps universe vs = fromCuts (go (cutsOf vs))+  where+    go ((lo1, hi1) : (lo2, hi2) : rest)+        | occupied hi1 lo2 = (lo1, hi1) : go ((lo2, hi2) : rest)+        | otherwise = go ((lo1, hi2) : rest)+    go is = is++    -- Is some member of the universe strictly between the two cuts? @v@ is, iff+    -- @hi < After v@ and @Before v < lo@; 'above' finds the least @v@ with the+    -- first property, and the second is one comparison.+    occupied hi lo = case above hi of+        Nothing -> False+        Just v  -> Cut v Before < lo+    above (Cut w Before) = Set.lookupGE w universe+    above (Cut w After)  = Set.lookupGT w universe+    above Unbounded      = Nothing++-- | Merge two sorted interval lists, joining any that overlap or touch.+--+-- Touching is the case worth naming: @<2@ and @>=2@ share no version, yet their+-- union is everything, so leaving them as two intervals would break canonicity+-- (and with it the derived 'Eq'). In cut terms both are the position+-- @Before 2@, so the test for "join these" is just @<=@.+unionVersionSet :: VersionSet -> VersionSet -> VersionSet+unionVersionSet a b = fromCuts (coalesce (merge (cutsOf a) (cutsOf b)))+  where+    merge [] ys = ys+    merge xs [] = xs+    merge (x : xs) (y : ys)+        | fst x < fst y = x : merge xs (y : ys)+        | fst y < fst x = y : merge (x : xs) ys+        | otherwise = (shorterCut (fst x) (fst y), snd x) : merge xs (y : ys)++    coalesce ((lo1, hi1) : (lo2, hi2) : rest)+        | lo2 <= hi1 = coalesce ((lo1, laterCut hi1 hi2) : rest)+    coalesce (i : rest) = i : coalesce rest+    coalesce [] = []++-- | Sweep both lists together, taking the overlap of the pair in hand and+-- advancing whichever interval ends first. Empty overlaps are dropped.+intersectionVersionSet :: VersionSet -> VersionSet -> VersionSet+intersectionVersionSet a b = fromCuts (go (cutsOf a) (cutsOf b))+  where+    go [] _ = []+    go _ [] = []+    go xs@((lo1, hi1) : xs') ys@((lo2, hi2) : ys')+        | hi1 <= hi2 = overlap : go xs' ys+        | otherwise = overlap : go xs ys'+      where+        overlap = (laterCut lo1 lo2, earlierCut hi1 hi2)++-- | Complement: the gaps between the intervals, plus the tails at either end.+--+-- Consecutive gaps are separated by the non-empty interval that lies between+-- them, so the result is canonical without any coalescing pass.+complementVersionSet :: VersionSet -> VersionSet+complementVersionSet vs = fromCuts (go (Cut version0 Before) (cutsOf vs))+  where+    go prev []             = [(prev, Unbounded)]+    go prev ((lo, hi) : rest)+        | hi == Unbounded = [(prev, lo)]+        | otherwise = (prev, lo) : go hi rest++-- | Under union.+instance Semigroup VersionSet where+    (<>) = unionVersionSet++-- | Version sets as the solver's sets. 'difference' goes through+-- 'complementVersionSet', which a version set has because versions have a+-- lowest one and no highest.+instance SetOps VersionSet where+    empty = emptyVersionSet+    intersect = intersectionVersionSet+    union = unionVersionSet+    difference a b = intersectionVersionSet a (complementVersionSet b)+    isEmpty = null . intervals+    isSubsetOf = subsetVersionSet+    isDisjoint = disjointVersionSet++-- | @a ⊆ b@: every interval of @a@ lies inside one interval of @b@. One sweep,+-- no set built. Both lists are sorted and their intervals separated by at least+-- one position, so an interval of @b@ that ends at or before the interval of @a@+-- in hand covers none of it and is passed; one that starts after it, or ends+-- before it does, leaves part of it uncovered that no later interval of @b@+-- can reach. The same answer as @isEmpty (a \\ b)@.+subsetVersionSet :: VersionSet -> VersionSet -> Bool+subsetVersionSet a b = go (cutsOf a) (cutsOf b)+  where+    go [] _ = True+    go _ [] = False+    go xs@((lo1, hi1) : xs') ys@((lo2, hi2) : ys')+        | hi2 <= lo1 = go xs ys'+        | lo2 <= lo1 && hi1 <= hi2 = go xs' ys+        | otherwise = False++-- | @a ∩ b = ∅@: no interval of @a@ overlaps one of @b@. Two intervals overlap+-- iff each starts before the other ends, so the sweep drops whichever ends+-- first. The same answer as @isEmpty (a ∩ b)@.+disjointVersionSet :: VersionSet -> VersionSet -> Bool+disjointVersionSet a b = go (cutsOf a) (cutsOf b)+  where+    go [] _ = True+    go _ [] = True+    go xs@((lo1, hi1) : xs') ys@((lo2, hi2) : ys')+        | hi1 <= lo2 = go xs' ys+        | hi2 <= lo1 = go xs ys'+        | otherwise = False++-- | Membership: @v@ lies in an interval iff the interval starts at or before+-- @Before v@ and ends at or after @After v@.+contains :: VersionSet -> Version -> Bool+contains vs v = any inside (cutsOf vs)+  where+    inside (lo, hi) = lo <= Cut v Before && Cut v After <= hi

@@ -0,0 +1,171 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeFamilies      #-}++module Cookbook where++import           Colog.Core            (LogAction (..))+import           Control.Monad         (guard)+import           Data.Functor.Identity (Identity (..))+import           Data.List             (find, sortOn)+import           Data.Map.Strict       (Map)+import qualified Data.Map.Strict       as Map+import           Data.Maybe            (isJust)+import           Data.Ord              (Down (..))+import           Data.Semigroup        (First (..))+import qualified Data.Set              as Set+import           Data.Text             (Text)+import qualified Data.Text             as T+import           PubGrub+import           PubGrub.SetOps        (isSubsetOf)++newtype Name = Name Text+    deriving (Eq, Ord, Show)++data Said+    = Requested Name VersionSet+    | Constrained Name VersionSet+    | DependsOn Name VersionSet Name VersionSet+    | Unusable Name VersionSet Text++instance Domain Name where++    type ValueOf Name = Version+    type SetOf Name = VersionSet+    type FactOf Name = Said+    singleton _ = singletonVersionSet+    mergeRule = sameDependency++range :: [Int] -> [Int] -> VersionSet+range lo hi = halfOpenVersionSet (mkVersion lo) (Just (mkVersion hi))++request :: Name -> VersionSet -> Incompatibility Name+request p s = seed (Requested p s) p (Negative s)++constrain :: Name -> VersionSet -> Incompatibility Name+constrain p allowed = seed (Constrained p allowed) p (Positive (complementVersionSet allowed))++data Release = Release+    { needs  :: [(Name, VersionSet)]+    , broken :: Maybe Text+    }++type Index = Map Name [(Version, Release)]++slot :: [Version] -> Version -> VersionSet+slot versions x+    | all (>= x) versions = belowVersionSet next+    | otherwise = halfOpenVersionSet x next+  where+    next = find (> x) versions++dependsOn :: Name -> VersionSet -> Name -> VersionSet -> Incompatibility Name+dependsOn p ps q qs = fact (DependsOn p ps q qs) [(p, Positive ps), (q, Negative qs)]++provider :: Index -> Provider Name Identity+provider index = Provider $ \p offered ->+    let releases = Map.findWithDefault [] p index+        versions = map fst releases+        newestFirst = sortOn (Down . fst) [r | r@(x, _) <- releases, offered `contains` x]+        (unusable, usable) = span (isJust . broken . snd) newestFirst+        reasons =+            [ fact (Unusable p (slot versions x) reason) [(p, Positive (slot versions x))]+            | (x, Release{broken = Just reason}) <- unusable+            ]+     in Identity $ case usable of+            (x, release) : _ -> (Just x, reasons ++ [dependsOn p (slot versions x) q qs | (q, qs) <- needs release])+            []               -> (Nothing, reasons)++app, lib, util, extra :: Name+app = Name "app"+lib = Name "lib"+util = Name "util"+extra = Name "extra"++example :: Index+example =+    Map.fromList+        [ (app, [(mkVersion [1], Release [(lib, range [1] [2, 1])] Nothing)])+        , ( lib+          , [ (mkVersion [1], Release [(util, range [1] [3])] Nothing)+            , (mkVersion [2], Release [(util, range [1] [3])] Nothing)+            , (mkVersion [2, 1], Release [] (Just "it does not build here"))+            ]+          )+        , (util, [(mkVersion [1], Release [] Nothing), (mkVersion [2], Release [] Nothing)])+        , (extra, [(mkVersion [1], Release [] Nothing), (mkVersion [2], Release [] Nothing)])+        ]++plan :: Index -> [Incompatibility Name] -> Maybe (Map Name Version)+plan index seeds = case runIdentity (solve mempty (provider index) seeds) of+    Right solution -> Just solution+    Left _         -> Nothing++sameDependency :: MergeRule Name+sameDependency =+    MergeRule+        { mergeParts = \i -> case incompCause i of+            Fact (DependsOn p ps q qs) -> Just ((p, q, qs), ps)+            _                          -> Nothing+        , mergeBuild = \(p, q, qs) ps -> dependsOn p ps q qs+        }++sameTerms :: (Domain v, Ord (SetOf v)) => MergeRule v+sameTerms =+    MergeRule+        { mergeParts = \i -> case incompCause i of+            Fact _ -> Just (incompTerms i, First i)+            _      -> Nothing+        , mergeBuild = \_ (First i) -> i+        }++name :: Name -> VersionSet -> Text+name (Name p) s = p <> " " <> pretty s++formatter :: Formatter Name+formatter = (mkFormatter says hole name){clauseRules = [whichDependsOn]}+  where+    says said _ = case said of+        Requested p s       -> name p s <> " is requested"+        Constrained p s     -> name p s <> " is required by a constraint"+        DependsOn p ps q qs -> name p ps <> " depends on " <> name q qs+        Unusable p s reason -> name p s <> " cannot be used: " <> reason+    hole p s = "no version of " <> name p s <> " exists"++whichDependsOn :: Rule (Incompatibility Name, Incompatibility Name) Text+whichDependsOn = symmetric $ \(first, second) -> do+    DependsOn p ps q qs <- asFact first+    DependsOn q' qs' r rs <- asFact second+    guard (q == q' && qs `isSubsetOf` qs')+    pure (name p ps <> " depends on " <> name q qs <> " which depends on " <> name r rs)++why :: Index -> [Incompatibility Name] -> Text+why index seeds = case runIdentity (solve mempty (provider index) seeds) of+    Right _                -> "There is a plan."+    Left (NoSolution root) -> reportConflict formatter root+    Left _                 -> "The solver failed unexpectedly."++searchLog :: Index -> [Incompatibility Name] -> [Text]+searchLog index seeds = fst (solve logger (Provider expandLogged) seeds)+  where+    logger = LogAction $ \msg -> (describe msg, ())+    expandLogged p s = ([], runIdentity (expand (provider index) p s))++describe :: SolverMsg Name -> [Text]+describe msg = case msg of+    Chose (Name p) x            -> [p <> " " <> pretty x]+    NoVersionFor (Name p) s     -> ["no " <> p <> " in " <> pretty s]+    Learned i                   -> ["learned: " <> sayTerms formatter (incompTerms i)]+    Backtracked level           -> ["back to level " <> T.pack (show level)]+    _                           -> []++solveWithLock :: Index -> Map Name Version -> [Incompatibility Name] -> Either (SolveError Name) (Map Name Version)+solveWithLock index lock requests = case attempt lock of+    Left (NoSolution root)+        | let involved = Map.keysSet lock `Set.intersection` conflictSet root+        , not (Set.null involved) ->+            attempt (Map.withoutKeys lock involved)+    result -> result+  where+    attempt held =+        runIdentity . solve mempty (provider index) $+            requests ++ [constrain p (singletonVersionSet x) | (p, x) <- Map.toList held]

@@ -0,0 +1,67 @@+{-# LANGUAGE OverloadedStrings #-}++-- | "PubGrub.Cookbook" against what it shows: its code is "Cookbook", and+-- every result its sessions print is asserted here.+module CookbookSpec (tests) where++import qualified Data.Map.Strict  as Map+import qualified Data.Text        as T+import           DocCode          (codeMatches)+import           PubGrub          (MergeRule, Pretty (..), fullVersionSet,+                                   mkVersion, noMerging, singletonVersionSet)+import           PubGrub.Store    (emptyStoreWith, insertClause, storeClauses)+import           Test.Tasty       (TestTree, testGroup)+import           Test.Tasty.HUnit (testCase, (@?=))++import           Cookbook++tests :: TestTree+tests =+    testGroup+        "the cookbook"+        [ testCase "its code is Cookbook.hs" $+            codeMatches "src/PubGrub/Cookbook.hs" "test/Cookbook.hs"+        , testCase "a plan" $+            plan example [request app fullVersionSet]+                @?= Just (Map.fromList [(app, mkVersion [1]), (lib, mkVersion [2]), (util, mkVersion [2])])+        , testCase "a constraint on a requested package" $+            plan example [request app fullVersionSet, constrain util (range [1] [2])]+                @?= Just (Map.fromList [(app, mkVersion [1]), (lib, mkVersion [2]), (util, mkVersion [1])])+        , testCase "a constraint on a package nothing requests" $+            plan example [request app fullVersionSet, constrain extra (range [2] [3])]+                @?= Just (Map.fromList [(app, mkVersion [1]), (lib, mkVersion [2]), (util, mkVersion [2])])+        , testCase "an explanation in the domain's words" $+            T.lines (why example [request app fullVersionSet, constrain util (range [3] [4])])+                @?= [ "Because app >=0 depends on lib >=1 && <2.1 which depends on util >=1 && <3, app >=0 requires util >=1 && <3."+                    , "So, because app >=0 is requested and util >=3 && <4 is required by a constraint, version solving failed."+                    ]+        , testCase "two dependencies over touching slots merge into one" $+            let slotOf = slot (map fst (example Map.! lib))+             in pretty (slotOf (mkVersion [1]) <> slotOf (mkVersion [2]))+                    @?= "<2.1"+        , testCase "a fact stated twice is one clause under sameTerms, and two with no rule" $+            let clausesUnder :: MergeRule Name -> Int+                clausesUnder rule =+                    length (storeClauses (snd (insertClause dep (snd (insertClause dep (emptyStoreWith rule))))))+                dep = dependsOn lib (slot (map fst (example Map.! lib)) (mkVersion [1])) util (range [1] [3])+             in (clausesUnder sameTerms, clausesUnder noMerging) @?= (1, 2)+        , testCase "a release passed over, with its reason" $+            why example [request lib (singletonVersionSet (mkVersion [2, 1]))]+                @?= "So, because lib >=2.1 cannot be used: it does not build here and lib ==2.1 is requested, version solving failed."+        , testCase "the search, step by step" $+            searchLog example [request app fullVersionSet, constrain util (range [3] [4])]+                @?= [ "app 1"+                    , "lib 2"+                    , "learned: lib >=2 && <2.1 requires util >=1 && <3"+                    , "back to level 1"+                    , "lib 1"+                    ]+        , testCase "a lock released where it took part in a failure" $+            either (const Nothing) Just+                ( solveWithLock+                    example+                    (Map.fromList [(util, mkVersion [1]), (extra, mkVersion [1])])+                    [request app fullVersionSet, request util (range [2] [3]), request extra fullVersionSet]+                )+                @?= Just (Map.fromList [(app, mkVersion [1]), (extra, mkVersion [1]), (lib, mkVersion [2]), (util, mkVersion [2])])+        ]

@@ -0,0 +1,50 @@+-- | Holding a module of documentation to the code it shows: every code block+-- is a run of consecutive lines of a test module, and together the blocks+-- cover the module, so that the code a reader copies is code that compiles+-- and that the tests run.+--+-- The blocks need not come in the module's order, and a block may be a single+-- line: a recipe that adds one line to an instance an earlier recipe declared+-- shows that line alone, where the module has it inside the instance.+module DocCode (codeMatches) where++import           Data.List        (isPrefixOf, stripPrefix, tails)+import           Data.Maybe       (mapMaybe)+import qualified Data.Set         as Set+import           Test.Tasty.HUnit (Assertion, assertFailure)++-- | The code blocks of the documentation module against the test module.+codeMatches :: FilePath -> FilePath -> Assertion+codeMatches doc code = do+    blocks <- codeBlocks <$> readFile doc+    source <- nonBlank . lines <$> readFile code+    let placed = [(block, runOf block source) | block <- blocks]+    case [block | (block, Nothing) <- placed] of+        block : _ -> assertFailure ("not in " ++ code ++ ":\n" ++ unlines block)+        []        -> pure ()+    let covered = Set.fromList (concat [[i .. i + length block - 1] | (block, Just i) <- placed])+    case [l | (i, l) <- zip [0 ..] source, i `Set.notMember` covered] of+        l : _ -> assertFailure ("not shown by " ++ doc ++ ": " ++ l)+        []    -> pure ()++-- | The code blocks of a Haddock comment: each run of bird-track lines, as+-- the lines it holds, blank lines dropped.+codeBlocks :: String -> [[String]]+codeBlocks = go . lines+  where+    go ls = case dropWhile (not . isCode) ls of+        [] -> []+        rest ->+            let (block, after) = span isCode rest+             in nonBlank (mapMaybe (fmap (drop 1) . stripPrefix "-- >") block) : go after+    isCode = ("-- >" `isPrefixOf`)++nonBlank :: [String] -> [String]+nonBlank = filter (not . all (== ' '))++-- | Where a block appears as consecutive lines of the module, if it does.+runOf :: [String] -> [String] -> Maybe Int+runOf block source =+    case [i | (i, rest) <- zip [0 ..] (tails source), block `isPrefixOf` rest] of+        i : _ -> Just i+        []    -> Nothing

@@ -0,0 +1,11 @@+module Main (main) where++import qualified CookbookSpec+import qualified PartialSolutionSpec+import qualified RelationSpec+import qualified StoreInvariantsSpec+import           Test.Tasty          (defaultMain, testGroup)+import qualified ToyDomainSpec++main :: IO ()+main = defaultMain (testGroup "pubgrub" [CookbookSpec.tests, PartialSolutionSpec.tests, RelationSpec.tests, StoreInvariantsSpec.tests, ToyDomainSpec.tests])

@@ -0,0 +1,265 @@+-- | Differential tests for the partial solution's storage layer.+--+-- 'PubGrub.PartialSolution.PartialSolution' indexes assignments by variable and+-- caches, per variable, the intersection of its assignments' terms and the+-- value it was decided to be. The caches are what let unit propagation ask+-- about a variable without scanning; they are also the only thing that can be+-- wrong. Backtracking is where they can be wrong most quietly: @intersectTerm@+-- cannot be undone, so a variable that loses assignments must have its term+-- rebuilt from the survivors, and a dropped decision must stop being+-- remembered.+--+-- The model below is the naive implementation: one flat chronological list,+-- every query a scan. It has no caches to invalidate, so agreement with it is+-- exactly the property at issue.+module PartialSolutionSpec (tests) where++import qualified Data.Map.Strict         as Map+import           Data.Maybe              (mapMaybe)+import           Data.Set                (Set)+import qualified Data.Set                as Set+import           PubGrub.Incompatibility (Incompatibility, incompGet, noValues)+import           PubGrub.PartialSolution (Assignment (..), AssignmentKind (..),+                                          PartialSolution (..), addDecision,+                                          addDerivation, assignmentTerm,+                                          backtrack, decidedValue, emptyPS,+                                          extractSolution, termIntersectionFor,+                                          undecidedPositive, varHistory)+import           PubGrub.SetOps          (equivalent)+import           PubGrub.Term            (Term (..), anyTerm, intersectTerm,+                                          negateTerm)+import           Test.Tasty              (TestTree, testGroup)+import           Test.Tasty.QuickCheck   (Arbitrary (..), Gen, Property,+                                          conjoin, counterexample, elements,+                                          frequency, testProperty)+import           Toy                     (Pkg (..), needs, wants)++-- --------------------------------------------------------------------------+-- The universe the scripts draw from+-- --------------------------------------------------------------------------++-- | Probe packages. Every query is checked for all of them, so keep the list+-- short — and keep it a superset of what the generators use, so that packages+-- which were never mentioned (the @Nothing@ / @⊤@ case) are checked too.+packages :: [Pkg]+packages = map Pkg ["a", "b", "c", "d"]++instances :: [Int]+instances = [1 .. 3]++-- | Range-shaped sets over the versions 1 to 3: at least 2, below 3, exactly 2.+sets :: [Set Int]+sets = map Set.fromList [[2, 3], [1, 2], [2]]++-- | The incompatibilities a derivation can be caused by: unit bans (which+-- derive a negative term), \"no versions\" (positive), and real two-package+-- dependencies — so that deriving for a package the incompatibility does /not/+-- mention (⊤, the term-absent case) is reachable too.+incompatibilities :: [Incompatibility Pkg]+incompatibilities =+    [wants p [i] | p <- packages, i <- instances]+        ++ [noValues p s | p <- packages, s <- sets]+        ++ [ needs p 2 q (Set.toList t)+           | (p, q) <- zip packages (drop 1 packages)+           , t <- sets+           ]++atIndex :: [a] -> Int -> Maybe a+atIndex xs n = case drop (n `mod` max 1 (length xs)) xs of+    x : _ -> Just x+    []    -> Nothing++-- --------------------------------------------------------------------------+-- Op scripts+-- --------------------------------------------------------------------------++-- | One step of a script. Indices are taken modulo the universe's size, and a+-- backtrack level modulo the current level plus one, so every generated script+-- is meaningful without a shrink-hostile precondition.+--+-- Deciding a package twice is allowed on purpose: the solver never does it+-- (a decided package's term is a singleton, which is never inconclusive, so it+-- is never chosen again), but the caches should not depend on that.+data Op+    = OpDecide Int Int+    | OpDerive Int Int+    | OpBacktrack Int+    deriving (Show)++instance Arbitrary Op where+    arbitrary =+        frequency+            [ (3, OpDecide <$> ix <*> ix)+            , (6, OpDerive <$> ix <*> ix)+            , (2, OpBacktrack <$> ix)+            ]+      where+        ix = elements [0 .. 11] :: Gen Int+    shrink (OpDecide a b)  = [OpDecide a' b' | (a', b') <- shrink (a, b)]+    shrink (OpDerive a b)  = [OpDerive a' b' | (a', b') <- shrink (a, b)]+    shrink (OpBacktrack a) = map OpBacktrack (shrink a)++-- | The model: one flat chronological list of assignments.+data Model = Model+    { mAssignments :: [Assignment Pkg]+    , mLevel       :: Int+    , mNextIndex   :: Int+    }++emptyModel :: Model+emptyModel = Model{mAssignments = [], mLevel = 0, mNextIndex = 0}++mDecide :: Pkg -> Int -> Model -> Model+mDecide p i (Model as l n) =+    Model (as ++ [Assignment n (l + 1) p (Decision i)]) (l + 1) (n + 1)++mDerive :: Pkg -> Incompatibility Pkg -> Model -> Model+mDerive p cause (Model as l n) =+    Model (as ++ [Assignment n l p (Derivation term cause)]) l (n + 1)+  where+    term = maybe anyTerm negateTerm (incompGet p cause)++mBacktrack :: Int -> Model -> Model+mBacktrack level (Model as _ n) = Model (filter ((<= level) . aLevel) as) level n++mHistory :: Model -> Pkg -> [Assignment Pkg]+mHistory m p = filter ((== p) . aVar) (mAssignments m)++mTerm :: Model -> Pkg -> Maybe (Term (Set Int))+mTerm m p = case map assignmentTerm (mHistory m p) of+    []     -> Nothing+    t : ts -> Just (foldl intersectTerm t ts)++mSolution :: Model -> Map.Map Pkg Int+mSolution m =+    Map.fromList+        [(aVar a, i) | a <- mAssignments m, Just i <- [decidedValue a]]++mUndecidedPositive :: Model -> [(Pkg, Set Int)]+mUndecidedPositive m =+    mapMaybe positive (filter (`notElem` decided) pkgs)+  where+    decided = [aVar a | a <- mAssignments m, Just _ <- [decidedValue a]]+    pkgs = uniqueOldestFirst [aVar a | a <- mAssignments m]+    positive p = case mTerm m p of+        Just (Positive r) -> Just (p, r)+        _                 -> Nothing+    uniqueOldestFirst = go []+      where+        go seen [] = reverse seen+        go seen (x : xs)+            | x `elem` seen = go seen xs+            | otherwise = go (x : seen) xs++-- | Apply one op to both, so a script drives them in lockstep.+step :: Op -> (PartialSolution Pkg, Model) -> (PartialSolution Pkg, Model)+step op (ps, m) = case op of+    OpDecide pi_ ii -> case (atIndex packages pi_, atIndex instances ii) of+        (Just p, Just i) -> (addDecision p i ps, mDecide p i m)+        _                -> (ps, m)+    OpDerive pi_ ci -> case (atIndex packages pi_, atIndex incompatibilities ci) of+        (Just p, Just c) -> (addDerivation p c ps, mDerive p c m)+        _                -> (ps, m)+    OpBacktrack k ->+        let level = k `mod` (psLevel ps + 1)+         in (snd (backtrack level ps), mBacktrack level m)++-- --------------------------------------------------------------------------+-- Comparisons+-- --------------------------------------------------------------------------++-- | Terms are compared up to set equivalence, which with canonical sets is+-- equality; the semantic form says what is being compared.+termEquiv :: Term (Set Int) -> Term (Set Int) -> Bool+termEquiv (Positive x) (Positive y) = equivalent x y+termEquiv (Negative x) (Negative y) = equivalent x y+termEquiv _ _                       = False++maybeTermEquiv :: Maybe (Term (Set Int)) -> Maybe (Term (Set Int)) -> Bool+maybeTermEquiv Nothing Nothing   = True+maybeTermEquiv (Just x) (Just y) = termEquiv x y+maybeTermEquiv _ _               = False++-- | An assignment's identity, ignoring the term (compared separately, by+-- equivalence).+key :: Assignment Pkg -> (Int, Int, Pkg, Maybe Int)+key a = (aIndex a, aLevel a, aVar a, decidedValue a)++check :: String -> Bool -> Property+check what = counterexample ("mismatch: " ++ what)++-- | Every query, on both, for every probe package.+agree :: PartialSolution Pkg -> Model -> Property+agree ps m =+    conjoin $+        [ check "psLevel" (psLevel ps == mLevel m)+        , check "extractSolution" (extractSolution ps == mSolution m)+        , check+            "undecidedPositive (packages)"+            (map fst (undecidedPositive ps) == map fst (mUndecidedPositive m))+        , check+            "undecidedPositive (sets)"+            ( and+                [ equivalent x y+                | ((_, x), (_, y)) <- zip (undecidedPositive ps) (mUndecidedPositive m)+                ]+            )+        ]+            ++ concatMap perPackage packages+  where+    perPackage p =+        [ check+            ("varHistory " ++ show p)+            (map key (varHistory ps p) == map key (mHistory m p))+        , check+            ("varHistory terms " ++ show p)+            ( and+                [ termEquiv (assignmentTerm x) (assignmentTerm y)+                | (x, y) <- zip (varHistory ps p) (mHistory m p)+                ]+            )+        , check+            ("termIntersectionFor " ++ show p)+            (maybeTermEquiv (termIntersectionFor ps p) (mTerm m p))+        ]++-- | Run a script, checking after every op — so the first divergence is+-- reported at the op that caused it, not at the end of the script.+runScript :: [Op] -> Property+runScript ops =+    conjoin+        [ counterexample ("after " ++ show op) (agree ps m)+        | (op, (ps, m)) <- zip ops (drop 1 (scanl (flip step) (emptyPS, emptyModel) ops))+        ]++-- | Unbiased scripts mostly backtrack to a level near the top, because levels+-- only rise a step at a time; a rebuild needs a backtrack that actually drops+-- something. Sprinkling extra backtracks in is what forces them.+interleaveBacktracks :: [Op] -> [Op]+interleaveBacktracks ops =+    concat+        [ if n `mod` 3 == (2 :: Int) then [op, OpBacktrack n] else [op]+        | (n, op) <- zip [0 ..] ops+        ]++-- | 'backtrack' names exactly the variables whose history it shortened: from+-- every state a script reaches, to every level there is.+movedAreTheShortened :: [Op] -> Property+movedAreTheShortened ops =+    conjoin+        [ counterexample ("backtracking to " ++ show level ++ " after " ++ show n ++ " ops") $+            Set.fromList moved == Set.fromList [p | p <- packages, length (varHistory ps' p) < length (varHistory ps p)]+        | (n, (ps, _)) <- zip [0 :: Int ..] (scanl (flip step) (emptyPS, emptyModel) ops)+        , level <- [0 .. psLevel ps]+        , let (moved, ps') = backtrack level ps+        ]++tests :: TestTree+tests =+    testGroup+        "PartialSolution (indexed vs flat-list model)"+        [ testProperty "every query agrees with the naive model, op by op" runScript+        , testProperty "…on scripts that backtrack heavily" $+            runScript . interleaveBacktracks+        , testProperty "backtrack names exactly the variables it moved" movedAreTheShortened+        ]

@@ -0,0 +1,27 @@+-- | 'PubGrub.Relation.relation', on small sets: how a term the partial+-- solution holds stands to a term of an incompatibility.+module RelationSpec (tests) where++import qualified Data.Set         as Set+import           PubGrub.Relation (Relation (..), relation)+import           PubGrub.Term     (Term (..))+import           Test.Tasty       (TestTree, testGroup)+import           Test.Tasty.HUnit (testCase, (@?=))++tests :: TestTree+tests =+    testGroup+        "relation"+        [ testCase "a subject inside the reference satisfies it" $+            relation (Positive (Set.fromList [3 :: Int])) (Positive (Set.fromList [1 .. 9])) @?= Satisfied+        , testCase "a subject outside the reference contradicts it" $+            relation (Positive (Set.fromList [3 :: Int])) (Positive (Set.fromList [5 .. 9])) @?= Contradicted+        , testCase "a subject wider than the reference leaves it open" $+            relation (Positive (Set.fromList [1 .. 9 :: Int])) (Positive (Set.fromList [3])) @?= Inconclusive+        , testCase "an exact subject that avoids a negative reference satisfies it" $+            relation (Positive (Set.fromList [3 :: Int])) (Negative (Set.fromList [5 .. 9])) @?= Satisfied+        , testCase "an exact subject that lands in a negative reference contradicts it" $+            relation (Positive (Set.fromList [6 :: Int])) (Negative (Set.fromList [5 .. 9])) @?= Contradicted+        , testCase "a negative subject never satisfies a positive reference" $+            relation (Negative (Set.fromList [5, 6 :: Int])) (Positive (Set.fromList [1 .. 4])) @?= Inconclusive+        ]

@@ -0,0 +1,176 @@+{-# LANGUAGE TypeFamilies #-}++-- | 'PubGrub.Store' as a data structure: its invariants ('valid') under any+-- merge rule, not only under cabal's.+--+-- Cabal's rule widens a depender term and never changes which variables a+-- clause mentions. The rules here do what it does not: one replaces a clause by+-- whatever arrived, so a merge can drop variables and add others, and one+-- unions the two clauses' terms, so a merge can only add them. One builds a+-- clause under another key, which the store does not ask about.+module StoreInvariantsSpec (tests) where++import qualified Data.IntSet             as IntSet+import           Data.List               (nub)+import qualified Data.Map.Strict         as Map+import           Data.Semigroup          (First (..), Last (..))+import           Data.Set                (Set)+import qualified Data.Set                as Set+import           PubGrub.Incompatibility (Cause (..), Domain (..),+                                          Incompatibility (..), MergeRule (..),+                                          noMerging)+import           PubGrub.Store           (Store, allClauses, clausesOf,+                                          emptyStoreWith, insertClause,+                                          insertClauses, storeClauses, valid)+import           PubGrub.Term            (Term (..))+import           Test.Tasty              (TestTree, testGroup)+import           Test.Tasty.HUnit        (testCase, (@?=))+import           Test.Tasty.QuickCheck   (Arbitrary (..), Property, choose,+                                          frequency, listOf, sublistOf,+                                          testProperty, vectorOf, (===))++-- --------------------------------------------------------------------------+-- The domain+-- --------------------------------------------------------------------------++newtype V = V Int+    deriving (Eq, Ord, Show)++-- | The domain: variables are small numbers, and a fact is a tag the rules+-- key on.++instance Domain V where++    type ValueOf V = Int+    type SetOf V = Set Int+    type FactOf V = Int+    singleton _ = Set.singleton++-- | A clause, as data a counterexample can print: its tag, whether it carries+-- a key ('Fact') or not ('Seed'), and its terms.+data Spec = Spec+    { spTag   :: Int+    , spKeyed :: Bool+    , spTerms :: [(Int, Bool, [Int])]+    }+    deriving (Show)++clause :: Spec -> Incompatibility V+clause Spec{spTag, spKeyed, spTerms} =+    Incompatibility+        (Map.fromList [(V v, (if pos then Positive else Negative) (Set.fromList vs)) | (v, pos, vs) <- spTerms])+        ((if spKeyed then Fact else Seed) spTag)++instance Arbitrary Spec where+    arbitrary = do+        tag <- choose (0, 4)+        keyed <- frequency [(4, pure True), (1, pure False)]+        n <- choose (0, 3)+        terms <- vectorOf n ((,,) <$> choose (0, 5) <*> arbitrary <*> sublistOf [0 .. 3])+        pure (Spec tag keyed terms)++-- | What a test does to a store.+data Op+    = Insert Spec+    | InsertMany [Spec]+    deriving (Show)++instance Arbitrary Op where+    arbitrary = frequency [(3, Insert <$> arbitrary), (1, InsertMany <$> listOf arbitrary)]++apply :: Store V -> Op -> Store V+apply store op = case op of+    Insert s      -> snd (insertClause (clause s) store)+    InsertMany ss -> snd (insertClauses (map clause ss) store)++-- --------------------------------------------------------------------------+-- The rules+-- --------------------------------------------------------------------------++keyOf :: Incompatibility V -> Maybe Int+keyOf i = case incompCause i of+    Fact t -> Just t+    _      -> Nothing++-- | The key, and the clause's own value of a part.+partsBy :: (Incompatibility V -> s) -> Incompatibility V -> Maybe (Int, s)+partsBy part i = (\k -> (k, part i)) <$> keyOf i++-- | The arriving clause replaces the existing one: a merge may drop any+-- variable and add any other.+replacing :: MergeRule V+replacing = MergeRule{mergeParts = partsBy Last, mergeBuild = const getLast}++-- | The merged clause mentions every variable either half did.+widening :: MergeRule V+widening =+    MergeRule+        { mergeParts = partsBy (\i -> (incompTerms i, First (incompCause i)))+        , mergeBuild = \_ (terms, First cause) -> Incompatibility terms cause+        }++-- | The merged clause has another key.+rekeying :: MergeRule V+rekeying = MergeRule{mergeParts = partsBy Last, mergeBuild = \k (Last new) -> new{incompCause = Fact (100 + k)}}++-- | Every store along the way is valid.+validThroughout :: MergeRule V -> [Op] -> Bool+validThroughout rule ops = all valid (scanl apply (emptyStoreWith rule) ops)++-- | An insert answers with the id of a clause that is in the store afterwards:+-- the one it merged into, or a new one exactly when nothing had its key.+landsWhereItSays :: MergeRule V -> [Spec] -> Spec -> Bool+landsWhereItSays rule before s =+    IntSet.member c (allClauses after) && isNew == not merges+  where+    store = foldl (\st x -> snd (insertClause (clause x) st)) (emptyStoreWith rule) before+    (c, after) = insertClause (clause s) store+    isNew = not (IntSet.member c (allClauses store))+    merges = spKeyed s && any ((== Just (spTag s)) . keyOf) (storeClauses store)++-- | Under a rule that merges by key, a store holds one clause per key and one+-- per clause without a key.+oneClausePerKey :: MergeRule V -> [Spec] -> Property+oneClausePerKey rule specs =+    length (storeClauses (foldl (\st x -> snd (insertClause x st)) (emptyStoreWith rule) (map clause specs)))+        === length (nub [spTag s | s <- specs, spKeyed s]) + length (filter (not . spKeyed) specs)++-- --------------------------------------------------------------------------+-- Tests+-- --------------------------------------------------------------------------++tests :: TestTree+tests =+    testGroup+        "the store under any lawful merge rule"+        [ testProperty "valid throughout, merging nothing" (validThroughout noMerging)+        , testProperty "valid throughout, a merge replacing the clause" (validThroughout replacing)+        , testProperty "valid throughout, a merge widening the clause" (validThroughout widening)+        , testProperty "an insert answers where the clause landed, replacing" (landsWhereItSays replacing)+        , testProperty "an insert answers where the clause landed, widening" (landsWhereItSays widening)+        , testProperty "one clause per key, replacing" (oneClausePerKey replacing)+        , testProperty "one clause per key, widening" (oneClausePerKey widening)+        , testCase "a variable the merged clause stops mentioning leaves the index" $ do+            let store =+                    snd . insertClause (clause (Spec 0 True [(2, True, [1])])) . snd $+                        insertClause (clause (Spec 0 True [(1, True, [1])])) (emptyStoreWith replacing)+            clausesOf (V 1) store @?= IntSet.empty+            clausesOf (V 2) store @?= IntSet.singleton 0+            valid store @?= True+        , testProperty "valid throughout, a merge changing the key" (validThroughout rekeying)+        , testCase "a clause built under another key is still found by its first key" $ do+            let insert s = snd . insertClause (clause s)+                store =+                    insert (Spec 0 True [(1, True, [3])])+                        . insert (Spec 0 True [(1, True, [1])])+                        . insert (Spec 0 True [(1, True, [2])])+                        $ emptyStoreWith rekeying+            length (storeClauses store) @?= 1+            valid store @?= True+        , testCase "a clause compares and shows structurally, cause included" $ do+            let a = clause (Spec 0 True [(1, True, [1]), (2, False, [2])])+                b = clause (Spec 1 True [(1, True, [1]), (2, False, [2])])+            a @?= a+            (a == b) @?= False+            show a @?= "Incompatibility {incompTerms = fromList [(V 1,Positive (fromList [1])),(V 2,Negative (fromList [2]))], incompCause = Fact 0}"+        ]

@@ -0,0 +1,90 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeFamilies      #-}++module Toy where++import           Data.Functor.Identity (Identity, runIdentity)+import           Data.List             (maximumBy)+import           Data.Map.Strict       (Map)+import qualified Data.Map.Strict       as Map+import           Data.Ord              (comparing)+import           Data.Set              (Set)+import qualified Data.Set              as Set+import           Data.Text             (Text)+import qualified Data.Text             as T+import qualified Data.Text.IO          as T+import           PubGrub++newtype Pkg = Pkg String+    deriving (Eq, Ord, Show)++data ToyFact+    = Wants Pkg (Set Int)+    | Needs Pkg Int Pkg (Set Int)++instance Domain Pkg where++    type ValueOf Pkg = Int+    type SetOf Pkg = Set Int+    type FactOf Pkg = ToyFact+    singleton _ v = Set.singleton v++wants :: Pkg -> [Int] -> Incompatibility Pkg+wants p vs = seed (Wants p (Set.fromList vs)) p (Negative (Set.fromList vs))++needs :: Pkg -> Int -> Pkg -> [Int] -> Incompatibility Pkg+needs p v q ws =+    fact (Needs p v q (Set.fromList ws)) [(p, Positive (Set.singleton v)), (q, Negative (Set.fromList ws))]++type World = Map Pkg [(Int, [(Pkg, [Int])])]++app, lib, util :: Pkg+app = Pkg "app"+lib = Pkg "lib"+util = Pkg "util"++world :: World+world =+    Map.fromList+        [ (app, [(1, [(lib, [1, 2])])])+        , (lib, [(1, [(util, [1])]), (2, [(util, [2])])])+        , (util, [(1, [])])+        ]++provider :: World -> Provider Pkg Identity+provider w = Provider $ \p offered ->+    pure $ case [(v, deps) | (v, deps) <- Map.findWithDefault [] p w, v `Set.member` offered] of+        [] -> (Nothing, [])+        candidates ->+            let (v, deps) = maximumBy (comparing fst) candidates+             in (Just v, [needs p v q ws | (q, ws) <- deps])++plan :: World -> [Incompatibility Pkg] -> Maybe (Map Pkg Int)+plan w seeds = case runIdentity (solve mempty (provider w) seeds) of+    Right solution -> Just solution+    Left _         -> Nothing++broken :: World+broken = Map.insert util [(3, [])] world++versions :: Set Int -> Text+versions vs = T.intercalate " or " (map (T.pack . show) (Set.toList vs))++name :: Pkg -> Set Int -> Text+name (Pkg p) vs = T.pack p <> " " <> versions vs++formatter :: Formatter Pkg+formatter = mkFormatter says hole name+  where+    says (Wants p vs) _     = name p vs <> " is requested"+    says (Needs p v q ws) _ = name p (Set.singleton v) <> " depends on " <> name q ws+    hole (Pkg p) vs = T.pack p <> " has no version " <> versions vs++why :: World -> [Incompatibility Pkg] -> Text+why w seeds = case runIdentity (solve mempty (provider w) seeds) of+    Right _                -> "There is a plan."+    Left (NoSolution root) -> reportConflict formatter root+    Left _                 -> "The solver failed unexpectedly."++explain :: World -> [Incompatibility Pkg] -> IO ()+explain w seeds = T.putStrLn (why w seeds)

@@ -0,0 +1,149 @@+{-# LANGUAGE OverloadedStrings #-}++-- | The solver over a domain that is not cabal's.+--+-- 'PubGrub.Incompatibility.Domain' is the whole of what the algorithm asks of+-- a problem, and this module is the proof: the domain is "Toy", where a package+-- is a name, a value is an 'Int', a set of values is a 'Set' and a fact is one+-- of two sentences, and nothing from Cabal-syntax or "PubGrub.Cabal" is+-- imported. If the core leans on the cabal domain, this module stops+-- compiling.+--+-- "Toy" is also the code of "PubGrub.Tutorial", line for line, so the tests+-- here hold the tutorial to what it shows: its code is checked against "Toy",+-- and every result it prints is asserted.+module ToyDomainSpec (tests) where++import           Data.Functor.Identity   (Identity, runIdentity)+import           Data.IORef              (modifyIORef', newIORef, readIORef)+import           Data.List               (sort, tails)+import qualified Data.Map.Strict         as Map+import qualified Data.Set                as Set+import           Data.Text               (Text)+import qualified Data.Text               as T+import           DocCode                 (codeMatches)+import           PubGrub.Derivation      (asFact, asNoValues, conflictSet,+                                          externals)+import           PubGrub.Incompatibility (Cause (..), Incompatibility (..),+                                          incompatibility)+import           PubGrub.Provider        (Provider (..))+import           PubGrub.Solver          (SolveError (..), solve)+import           PubGrub.Term            (Term (..))+import           Test.Tasty              (TestTree, testGroup)+import           Test.Tasty.HUnit        (assertBool, assertFailure, testCase,+                                          (@?=))+import           Toy++tests :: TestTree+tests =+    testGroup+        "a domain that is not cabal's"+        [ testCase "solves, backtracking from lib 2 to lib 1" $+            plan world [wants app [1]] @?= Just (Map.fromList [(app, 1), (lib, 1), (util, 1)])+        , testCase "fails when nothing fits, and the derivation reads back" $+            case runIdentity (solve mempty (provider broken) [wants app [1]]) of+                Right plan' -> assertFailure ("expected no solution, got " ++ show plan')+                Left (NoSatisfier p _) -> assertFailure ("no satisfier for " ++ show p)+                Left (BadSeed _) -> assertFailure "the seed was refused"+                Left (BadValue p v _) -> assertFailure ("bad value " ++ show v ++ " for " ++ show p)+                Left (NoSolution root) -> do+                    -- The root is the empty clause, closed against the seeds.+                    Map.keys (incompTerms root) @?= []+                    -- Every variable the search touched is in the conflict set.+                    conflictSet root @?= Set.fromList [app, lib, util]+                    -- The leaves are the seed, the facts the provider stated,+                    -- and the two holes the solver found: util has no version 1+                    -- and no version 2.+                    let leaves = externals root+                    [p | Just (Wants p vs) <- map asFact leaves, vs == Set.fromList [1]] @?= [app]+                    sort [h | Just h <- map asNoValues leaves] @?= [(util, Set.fromList [1]), (util, Set.fromList [2])]+        , testCase "incompatibility intersects a variable named twice and drops a term that is always true" $+            incompTerms (incompatibility (Fact (Wants app Set.empty)) [(app, Positive (Set.fromList [1, 2])), (app, Positive (Set.fromList [2, 3])), (lib, Negative Set.empty)])+                @?= Map.fromList [(app, Positive (Set.fromList [2]))]+        , testGroup+            "the boundary"+            [ testCase "a seed of two negative terms is refused, not solved to an empty plan" $+                -- "app is 1 or lib is 1": neither variable is ever almost+                -- satisfied, so nothing would be decided and the empty plan+                -- would violate the seed.+                case runIdentity (solve mempty (provider world) [eitherOf app lib]) of+                    Left (BadSeed _) -> pure ()+                    Left _           -> assertFailure "refused for another reason"+                    Right plan'      -> assertFailure ("solved to " ++ show plan')+            , testCase "a request whose cause is not Seed is refused" $+                case runIdentity (solve mempty (provider world) [needs app 1 lib [1]]) of+                    Left (BadSeed _) -> pure ()+                    Left _           -> assertFailure "refused for another reason"+                    Right plan'      -> assertFailure ("solved to " ++ show plan')+            , testCase "a provider that answers outside the offered set stops the solve" $+                case runIdentity (solve mempty outside [wants app [1]]) of+                    Left (BadValue p v s) -> (p, v, s) @?= (app, 99, Set.fromList [1])+                    Left _                -> assertFailure "failed for another reason"+                    Right plan'           -> assertFailure ("solved to " ++ show plan')+            , testCase "a reason that names another variable still bans the set" $ do+                -- lib 1 is passed over because it needs util 1. That reason+                -- rules lib 1 out only while util is outside {1}, so the+                -- solver must also state that lib has no value in {1}, or it+                -- offers lib {1} again, forever. After ten questions the+                -- provider answers outside the set, which stops the solve.+                asked <- newIORef (0 :: Int)+                let reasoned = Provider $ \p _ -> do+                        modifyIORef' asked (+ 1)+                        n <- readIORef asked+                        pure $ if n > 10+                            then (Just 99, [])+                            else (Nothing, [needs lib 1 util [1] | p == lib])+                result <- solve mempty reasoned [wants lib [1]]+                case result of+                    Left (NoSolution _) -> pure ()+                    Left (BadValue p _ s) ->+                        assertFailure ("offered " ++ show (p, s) ++ " again and again")+                    Left _ -> assertFailure "failed for another reason"+                    Right plan' -> assertFailure ("solved to " ++ show plan')+            ]+        , testGroup+            "the tutorial"+            [ testCase "its code is Toy.hs" $+                codeMatches "src/PubGrub/Tutorial.hs" "test/Toy.hs"+            , testCase "a dependency's terms" $+                incompTerms (needs (Pkg "lib") 1 (Pkg "util") [1])+                    @?= Map.fromList [(Pkg "lib", Positive (Set.fromList [1])), (Pkg "util", Negative (Set.fromList [1]))]+            , testCase "the provider picks the newest" $+                fst (runIdentity (expand (provider world) lib (Set.fromList [1, 2]))) @?= Just 2+            , testCase "the broken world has no plan" $+                plan broken [wants app [1]] @?= Nothing+            , testCase "the explanation" $+                T.lines (why broken [wants app [1]]) @?= expectedProof+            , testCase "the README shows its explanation" $ do+                readme <- T.lines . T.pack <$> readFile "README.md"+                assertBool "the README quotes the explanation the tutorial prints" $+                    expectedProof `elem` [take (length expectedProof) rest | rest <- tails readme]+            , testCase "the original world has a plan" $+                why world [wants app [1]] @?= "There is a plan."+            ]+        ]++-- | A seed that says "@p@ is 1 or @q@ is 1": two negative terms, which is not+-- a request.+eitherOf :: Pkg -> Pkg -> Incompatibility Pkg+eitherOf p q =+    Incompatibility+        (Map.fromList [(p, Negative (Set.singleton 1)), (q, Negative (Set.singleton 1))])+        (Seed (Wants p (Set.singleton 1)))++-- | A provider that ignores the set it is offered.+outside :: Provider Pkg Identity+outside = Provider (\_ _ -> pure (Just 99, []))++-- | The proof, as the spec's three cases render the derivation above: the two+-- refutations of @lib@ are two branches (@references\/pubgrub.md:595@), so the+-- first ends on a numbered line and the second refers back to it (@:608@), and+-- the closing line ends in \"version solving failed\" (@:1030@).+expectedProof :: [Text]+expectedProof =+    [ "1. Because lib 1 depends on util 1 and util has no version 1, lib 1 is forbidden."+    , ""+    , "Because util has no version 2 and lib 2 depends on util 2, lib 2 is forbidden."+    , "And because lib 1 is forbidden (1), lib 1 or 2 is forbidden."+    , "So, because app 1 depends on lib 1 or 2 and app 1 is requested, version solving failed."+    ]