OCaml implementation of PubGrub
anil.recoil.org
1(* Implementation of the PubGrub algorithm in OCaml *)
2
3(* Core Types *)
4module type PACKAGE_ID = sig
5 type t
6 val compare : t -> t -> int
7 val to_string : t -> string
8end
9
10module type VERSION = sig
11 type t
12 val compare : t -> t -> int
13 val to_string : t -> string
14end
15
16module type VERSION_SET = sig
17 type t
18 type version
19 val empty : t
20 val any : t
21 val singleton : version -> t
22 val union : t -> t -> t
23 val intersection : t -> t -> t
24 val complement : t -> t
25 val is_empty : t -> bool
26 val contains : version -> t -> bool
27 val subset_of : t -> t -> bool
28 val is_disjoint : t -> t -> bool
29 val to_string : t -> string
30end
31
32(* Terms and Constraints *)
33type ('v, 'vs) term =
34 | Positive of 'vs (* The package version must be in this set *)
35 | Negative of 'vs (* The package version must not be in this set *)
36
37module Term = struct
38 type ('v, 'vs) t = ('v, 'vs) term
39
40 let any (vs : 'vs) : ('v, 'vs) t = Positive vs
41 let empty (vs : 'vs) : ('v, 'vs) t = Negative vs
42 let exact (v : 'v) (mk_singleton : 'v -> 'vs) : ('v, 'vs) t =
43 Positive (mk_singleton v)
44
45 let negate = function
46 | Positive vs -> Negative vs
47 | Negative vs -> Positive vs
48
49 let contains (v : 'v) (vs_contains : 'v -> 'vs -> bool) term =
50 match term with
51 | Positive vs -> vs_contains v vs
52 | Negative vs -> not (vs_contains v vs)
53
54 let intersect_positive_positive vs_intersect vs1 vs2 =
55 Positive (vs_intersect vs1 vs2)
56
57 let intersect_negative_negative vs_intersect vs_complement vs1 vs2 =
58 Negative (vs_intersect (vs_complement vs1) (vs_complement vs2))
59
60 let intersect_positive_negative vs_intersect vs_complement vs1 vs2 =
61 let intersection = vs_intersect vs1 (vs_complement vs2) in
62 Positive intersection
63
64 let intersect_negative_positive vs_intersect vs_complement vs1 vs2 =
65 let intersection = vs_intersect (vs_complement vs1) vs2 in
66 Positive intersection
67
68 let intersection vs_intersect vs_complement t1 t2 =
69 match t1, t2 with
70 | Positive vs1, Positive vs2 ->
71 intersect_positive_positive vs_intersect vs1 vs2
72 | Negative vs1, Negative vs2 ->
73 intersect_negative_negative vs_intersect vs_complement vs1 vs2
74 | Positive vs1, Negative vs2 ->
75 intersect_positive_negative vs_intersect vs_complement vs1 vs2
76 | Negative vs1, Positive vs2 ->
77 intersect_negative_positive vs_intersect vs_complement vs1 vs2
78
79 let union_positive_positive vs_union vs1 vs2 =
80 Positive (vs_union vs1 vs2)
81
82 let union_negative_negative vs_intersect vs1 vs2 =
83 Negative (vs_intersect vs1 vs2)
84
85 let union_positive_negative vs_intersect vs_complement vs_is_empty vs1 vs2 =
86 let diff = vs_intersect vs1 (vs_complement vs2) in
87 if vs_is_empty diff then Negative vs2 else Positive diff
88
89 let union_negative_positive vs_intersect vs_complement vs_is_empty vs1 vs2 =
90 let diff = vs_intersect (vs_complement vs1) vs2 in
91 if vs_is_empty diff then Negative vs1 else Positive diff
92
93 let union vs_union vs_intersect vs_complement vs_is_empty t1 t2 =
94 match t1, t2 with
95 | Positive vs1, Positive vs2 ->
96 union_positive_positive vs_union vs1 vs2
97 | Negative vs1, Negative vs2 ->
98 union_negative_negative vs_intersect vs1 vs2
99 | Positive vs1, Negative vs2 ->
100 union_positive_negative vs_intersect vs_complement vs_is_empty vs1 vs2
101 | Negative vs1, Positive vs2 ->
102 union_negative_positive vs_intersect vs_complement vs_is_empty vs1 vs2
103
104 let is_positive = function
105 | Positive _ -> true
106 | Negative _ -> false
107
108 let to_string (_ : 'v -> string) (vs_to_str : 'vs -> string) term =
109 match term with
110 | Positive vs -> vs_to_str vs
111 | Negative vs -> "not " ^ vs_to_str vs
112end
113
114(* Incompatibilities *)
115type ('p, 'v, 'vs, 'meta) incompatibility = {
116 terms : (('p * ('v, 'vs) term) list);
117 cause : ('p, 'v, 'vs, 'meta) incompatibility_cause;
118}
119and ('p, 'v, 'vs, 'meta) incompatibility_cause =
120 | Root of 'p * 'v
121 | NoVersions of 'p * 'vs
122 | Dependency of 'p * 'vs * 'p * 'vs
123 | Derived of int * int
124 | External of 'p * 'vs * 'meta
125
126module Incompatibility = struct
127 type ('p, 'v, 'vs, 'meta) t = ('p, 'v, 'vs, 'meta) incompatibility
128
129 let not_root pkg ver vs_singleton =
130 { terms = [(pkg, Negative (vs_singleton ver))];
131 cause = Root (pkg, ver) }
132
133 let no_versions pkg term =
134 match term with
135 | Positive vs ->
136 { terms = [(pkg, term)];
137 cause = NoVersions (pkg, vs) }
138 | _ ->
139 failwith "Expected positive term"
140
141 let from_dependency pkg_from vs_from pkg_to vs_to =
142 { terms = [(pkg_from, Positive vs_from); (pkg_to, Negative vs_to)];
143 cause = Dependency (pkg_from, vs_from, pkg_to, vs_to) }
144
145 let from_derivation incomp1 incomp2 =
146 { terms = []; (* This will be populated during conflict resolution *)
147 cause = Derived (incomp1, incomp2) }
148end
149
150(* Partial Solutions *)
151type ('p, 'v, 'vs) partial_solution = {
152 decision_level : int;
153 decisions : ('p * 'v) list;
154 assignments : ('p * ('v, 'vs) term * int * bool) list;
155}
156
157module PartialSolution = struct
158 type ('p, 'v, 'vs) t = ('p, 'v, 'vs) partial_solution
159
160 let empty = {
161 decision_level = 0;
162 decisions = [];
163 assignments = [];
164 }
165
166 let current_decision_level solution = solution.decision_level
167
168 let add_decision solution package version vs_singleton =
169 let decision_level = solution.decision_level + 1 in
170 let new_assignment = (package, Positive (vs_singleton version), decision_level, true) in
171 {
172 decision_level;
173 decisions = (package, version) :: solution.decisions;
174 assignments = new_assignment :: solution.assignments;
175 }
176
177 let add_derivation solution package term cause_incompat decision_level =
178 let new_assignment = (package, term, decision_level, false) in
179 { solution with
180 assignments = new_assignment :: solution.assignments;
181 }
182
183 let check_assignment p_compare pkg term (assign_pkg, assign_term, _, _) =
184 if p_compare assign_pkg pkg = 0 then
185 match assign_term, term with
186 | Positive _, Positive _ -> true
187 | Negative _, Negative _ -> true
188 | _ -> false
189 else
190 false
191
192 let relation solution p_compare incompatibility =
193 let rec check_terms satisfied unsatisfied_term = function
194 | [] ->
195 if satisfied then `Satisfied else `AlmostSatisfied unsatisfied_term
196 | (pkg, term) :: rest ->
197 let pkg_satisfies =
198 List.exists (fun a -> check_assignment p_compare pkg term a) solution.assignments in
199 if pkg_satisfies then
200 check_terms satisfied unsatisfied_term rest
201 else
202 check_terms false (pkg, term) rest
203 in
204 check_terms true (List.hd incompatibility.terms) incompatibility.terms
205
206 let extract_solution solution =
207 solution.decisions |> List.rev
208
209 let backtrack solution level =
210 let new_assignments =
211 List.filter (fun (_, _, assignment_level, _) -> assignment_level <= level) solution.assignments in
212 let new_decisions =
213 List.filter (fun (_, _) -> level <= solution.decision_level) solution.decisions in
214 { decision_level = level; assignments = new_assignments; decisions = new_decisions }
215end
216
217(* Dependency Provider *)
218module type DEPENDENCY_PROVIDER = sig
219 type package_id
220 type version
221 type version_set
222 type error
223
224 val get_root_package : unit -> package_id
225 val get_root_version : unit -> version
226 val available_versions : package_id -> version list
227 val get_dependencies : package_id -> version -> ((package_id * version_set) list, error) result
228 val choose_version : package_id -> version_set -> version option
229end
230
231(* Solver Configuration *)
232type 'a config = {
233 max_iterations : int option;
234}
235
236let default_config = {
237 max_iterations = None;
238}
239
240(* Main Solver Interface *)
241module type SOLVER = sig
242 type package_id
243 type version
244 type version_set
245 type metadata
246
247 type error =
248 | Unsatisfiable of {
249 explanation : string;
250 }
251 | DependencyProviderError of {
252 package : package_id;
253 version : version;
254 message : string;
255 }
256 | MaxIterationsExceeded
257
258 type solution = (package_id * version) list
259
260 val solve :
261 (module DEPENDENCY_PROVIDER with
262 type package_id = package_id and
263 type version = version and
264 type version_set = version_set and
265 type error = string) ->
266 'a config ->
267 (solution, error) result
268
269 val explain_error : error -> string
270end
271
272(* Functor Implementation *)
273module Make
274 (P : PACKAGE_ID)
275 (V : VERSION)
276 (VS : VERSION_SET with type version = V.t) = struct
277
278 type package_id = P.t
279 type version = V.t
280 type version_set = VS.t
281 type metadata = string
282
283 type error =
284 | Unsatisfiable of {
285 explanation : string;
286 }
287 | DependencyProviderError of {
288 package : package_id;
289 version : version;
290 message : string;
291 }
292 | MaxIterationsExceeded
293
294 type solution = (package_id * version) list
295
296 (* Helper functions for the PubGrub algorithm *)
297
298 let add_incompatibility_from_dependencies package version deps =
299 List.map (fun (dep_pkg, dep_vs) ->
300 Incompatibility.from_dependency package (VS.singleton version) dep_pkg dep_vs
301 ) deps
302
303 let check_max_iterations config iterations =
304 match config.max_iterations with
305 | Some max when iterations >= max -> Error MaxIterationsExceeded
306 | _ -> Ok ()
307
308 let process_unit_propagation solution incompatibility =
309 match PartialSolution.relation solution P.compare incompatibility with
310 | `Satisfied ->
311 Error (`Conflict incompatibility)
312 | `AlmostSatisfied (pkg, term) ->
313 (* Add derived assignment *)
314 let new_solution =
315 PartialSolution.add_derivation
316 solution pkg (Term.negate term) incompatibility solution.decision_level in
317 Ok new_solution
318 | `Unsatisfied ->
319 Ok solution
320
321 let unit_propagation solution incompatibilities package =
322 let relevant_incompats =
323 List.filter (fun incomp ->
324 List.exists (fun (pkg, _) -> P.compare pkg package = 0) incomp.terms
325 ) incompatibilities in
326
327 let rec process_incompats solution = function
328 | [] -> Ok solution
329 | incomp :: rest ->
330 match process_unit_propagation solution incomp with
331 | Ok new_solution -> process_incompats new_solution rest
332 | Error e -> Error e
333 in
334 process_incompats solution relevant_incompats
335
336 let propagate_all solution incompatibilities pending_packages =
337 let rec propagate solution = function
338 | [] -> Ok solution
339 | pkg :: rest ->
340 match unit_propagation solution incompatibilities pkg with
341 | Ok new_solution -> propagate new_solution rest
342 | Error (`Conflict incomp) ->
343 (* Simple conflict handling for now - just fails with explanation *)
344 let explanation =
345 Printf.sprintf "Conflict found for package %s" (P.to_string pkg) in
346 Error (Unsatisfiable { explanation })
347 in
348 propagate solution pending_packages
349
350 let get_packages_with_constraints solution =
351 List.fold_left (fun acc (package, _, _, _) ->
352 if List.exists (fun (p, _) -> P.compare p package = 0) solution.decisions then
353 acc
354 else
355 package :: acc
356 ) [] solution.assignments
357 |> List.sort_uniq P.compare
358
359 let get_package_constraints solution package =
360 List.fold_left (fun acc (pkg, term, _, _) ->
361 if P.compare pkg package = 0 then
362 term :: acc
363 else
364 acc
365 ) [] solution.assignments
366
367 let compute_effective_range constraints =
368 let process_constraint range term =
369 match term, range with
370 | Positive vs1, Positive vs2 ->
371 Positive (VS.intersection vs1 vs2)
372 | Negative vs1, Positive vs2 ->
373 let complement = VS.complement vs1 in
374 Positive (VS.intersection vs2 complement)
375 | Positive vs1, Negative vs2 ->
376 let complement = VS.complement vs2 in
377 Positive (VS.intersection vs1 complement)
378 | Negative vs1, Negative vs2 ->
379 Negative (VS.union vs1 vs2)
380 in
381
382 match constraints with
383 | [] -> Positive VS.any
384 | first :: rest ->
385 List.fold_left process_constraint first rest
386
387 let extract_version_set = function
388 | Positive vs -> vs
389 | Negative vs -> VS.complement vs
390
391 (* Main solver implementation *)
392 let solve
393 (module Provider : DEPENDENCY_PROVIDER with
394 type package_id = package_id and
395 type version = version and
396 type version_set = version_set and
397 type error = string)
398 (config : 'a config) =
399
400 let root_pkg = Provider.get_root_package () in
401 let root_version = Provider.get_root_version () in
402
403 let initial_solution = PartialSolution.empty in
404 let initial_incompats = [
405 Incompatibility.not_root root_pkg root_version VS.singleton
406 ] in
407
408 let rec solve_loop solution incompatibilities iterations =
409 match check_max_iterations config iterations with
410 | Error e -> Error e
411 | Ok () ->
412 (* Get all packages that need propagation *)
413 let pending_packages =
414 List.map (fun (package, _, _, _) -> package) solution.assignments in
415
416 (* Run unit propagation on all packages *)
417 match propagate_all solution incompatibilities pending_packages with
418 | Error e -> Error e
419 | Ok propagated_solution ->
420 (* Check if we're done *)
421 if List.length propagated_solution.decisions = 0 then
422 Ok []
423 else if List.exists (fun (pkg, _) -> P.compare pkg root_pkg = 0) propagated_solution.decisions then
424 (* We have a solution *)
425 Ok (PartialSolution.extract_solution propagated_solution)
426 else
427 (* Decision making - pick next package to decide on *)
428 let packages_with_constraints =
429 get_packages_with_constraints propagated_solution in
430
431 match packages_with_constraints with
432 | [] ->
433 (* No more packages to decide on, we're done *)
434 Ok (PartialSolution.extract_solution propagated_solution)
435 | next_pkg :: _ ->
436 (* Find constraints for this package *)
437 let constraints =
438 get_package_constraints propagated_solution next_pkg in
439
440 (* Compute effective range *)
441 let effective_range =
442 compute_effective_range constraints in
443
444 (* Choose version *)
445 let effective_vs = extract_version_set effective_range in
446
447 match Provider.choose_version next_pkg effective_vs with
448 | None ->
449 (* No valid version - add incompatibility and backtrack *)
450 let incomp = Incompatibility.no_versions next_pkg effective_range in
451 solve_loop propagated_solution (incomp :: incompatibilities) (iterations + 1)
452 | Some version ->
453 (* Get dependencies for this version *)
454 match Provider.get_dependencies next_pkg version with
455 | Error msg ->
456 Error (DependencyProviderError {
457 package = next_pkg;
458 version;
459 message = msg;
460 })
461 | Ok deps ->
462 (* Add decision and dependencies as incompatibilities *)
463 let new_solution =
464 PartialSolution.add_decision
465 propagated_solution next_pkg version VS.singleton in
466
467 let new_incompats =
468 add_incompatibility_from_dependencies next_pkg version deps in
469
470 solve_loop
471 new_solution
472 (new_incompats @ incompatibilities)
473 (iterations + 1)
474 in
475
476 match solve_loop initial_solution initial_incompats 0 with
477 | Ok [] ->
478 (* Empty solution - just return the root package *)
479 Ok [(root_pkg, root_version)]
480 | Ok solution -> Ok solution
481 | Error e -> Error e
482
483 (* Format error messages *)
484 let explain_error = function
485 | Unsatisfiable { explanation } ->
486 "Dependency resolution failed: " ^ explanation
487 | DependencyProviderError { package; version; message } ->
488 Printf.sprintf "Error retrieving dependencies for %s %s: %s"
489 (P.to_string package) (V.to_string version) message
490 | MaxIterationsExceeded ->
491 "Dependency resolution exceeded maximum iterations"
492end