diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -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 + + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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 diff --git a/pubgrub.cabal b/pubgrub.cabal new file mode 100644 --- /dev/null +++ b/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 diff --git a/src/PubGrub.hs b/src/PubGrub.hs new file mode 100644 --- /dev/null +++ b/src/PubGrub.hs @@ -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 diff --git a/src/PubGrub/Cookbook.hs b/src/PubGrub/Cookbook.hs new file mode 100644 --- /dev/null +++ b/src/PubGrub/Cookbook.hs @@ -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 && \ 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])]) +-- @ diff --git a/src/PubGrub/Derivation.hs b/src/PubGrub/Derivation.hs new file mode 100644 --- /dev/null +++ b/src/PubGrub/Derivation.hs @@ -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 diff --git a/src/PubGrub/Incompatibility.hs b/src/PubGrub/Incompatibility.hs new file mode 100644 --- /dev/null +++ b/src/PubGrub/Incompatibility.hs @@ -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 diff --git a/src/PubGrub/PartialSolution.hs b/src/PubGrub/PartialSolution.hs new file mode 100644 --- /dev/null +++ b/src/PubGrub/PartialSolution.hs @@ -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) diff --git a/src/PubGrub/Pretty.hs b/src/PubGrub/Pretty.hs new file mode 100644 --- /dev/null +++ b/src/PubGrub/Pretty.hs @@ -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 "}" diff --git a/src/PubGrub/Provider.hs b/src/PubGrub/Provider.hs new file mode 100644 --- /dev/null +++ b/src/PubGrub/Provider.hs @@ -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. + } diff --git a/src/PubGrub/Relation.hs b/src/PubGrub/Relation.hs new file mode 100644 --- /dev/null +++ b/src/PubGrub/Relation.hs @@ -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 diff --git a/src/PubGrub/Report.hs b/src/PubGrub/Report.hs new file mode 100644 --- /dev/null +++ b/src/PubGrub/Report.hs @@ -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)) diff --git a/src/PubGrub/SetOps.hs b/src/PubGrub/SetOps.hs new file mode 100644 --- /dev/null +++ b/src/PubGrub/SetOps.hs @@ -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 diff --git a/src/PubGrub/Solver.hs b/src/PubGrub/Solver.hs new file mode 100644 --- /dev/null +++ b/src/PubGrub/Solver.hs @@ -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 diff --git a/src/PubGrub/Store.hs b/src/PubGrub/Store.hs new file mode 100644 --- /dev/null +++ b/src/PubGrub/Store.hs @@ -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) diff --git a/src/PubGrub/Term.hs b/src/PubGrub/Term.hs new file mode 100644 --- /dev/null +++ b/src/PubGrub/Term.hs @@ -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 diff --git a/src/PubGrub/Tutorial.hs b/src/PubGrub/Tutorial.hs new file mode 100644 --- /dev/null +++ b/src/PubGrub/Tutorial.hs @@ -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. diff --git a/src/PubGrub/Version.hs b/src/PubGrub/Version.hs new file mode 100644 --- /dev/null +++ b/src/PubGrub/Version.hs @@ -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] diff --git a/src/PubGrub/VersionSet.hs b/src/PubGrub/VersionSet.hs new file mode 100644 --- /dev/null +++ b/src/PubGrub/VersionSet.hs @@ -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 && =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 @=hi@, and the @ 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 diff --git a/test/Cookbook.hs b/test/Cookbook.hs new file mode 100644 --- /dev/null +++ b/test/Cookbook.hs @@ -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] diff --git a/test/CookbookSpec.hs b/test/CookbookSpec.hs new file mode 100644 --- /dev/null +++ b/test/CookbookSpec.hs @@ -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])]) + ] diff --git a/test/DocCode.hs b/test/DocCode.hs new file mode 100644 --- /dev/null +++ b/test/DocCode.hs @@ -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 diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -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]) diff --git a/test/PartialSolutionSpec.hs b/test/PartialSolutionSpec.hs new file mode 100644 --- /dev/null +++ b/test/PartialSolutionSpec.hs @@ -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 + ] diff --git a/test/RelationSpec.hs b/test/RelationSpec.hs new file mode 100644 --- /dev/null +++ b/test/RelationSpec.hs @@ -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 + ] diff --git a/test/StoreInvariantsSpec.hs b/test/StoreInvariantsSpec.hs new file mode 100644 --- /dev/null +++ b/test/StoreInvariantsSpec.hs @@ -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}" + ] diff --git a/test/Toy.hs b/test/Toy.hs new file mode 100644 --- /dev/null +++ b/test/Toy.hs @@ -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) diff --git a/test/ToyDomainSpec.hs b/test/ToyDomainSpec.hs new file mode 100644 --- /dev/null +++ b/test/ToyDomainSpec.hs @@ -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." + ]