]>
Commit | Line | Data |
---|---|---|
f035d41b XL |
1 | use super::lib::Solution; |
2 | use tracing::debug; | |
3 | ||
4 | use chalk_ir::interner::Interner; | |
5 | use chalk_ir::{ClausePriority, DomainGoal, Fallible, GenericArg, Goal, GoalData}; | |
6 | ||
7 | pub(super) fn with_priorities_for_goal<I: Interner>( | |
8 | interner: &I, | |
9 | goal: &Goal<I>, | |
10 | a: Fallible<Solution<I>>, | |
11 | prio_a: ClausePriority, | |
12 | b: Fallible<Solution<I>>, | |
13 | prio_b: ClausePriority, | |
14 | ) -> (Fallible<Solution<I>>, ClausePriority) { | |
15 | let domain_goal = match goal.data(interner) { | |
16 | GoalData::DomainGoal(domain_goal) => domain_goal, | |
17 | _ => { | |
18 | // non-domain goals currently have no priorities, so we always take the new solution here | |
19 | return (b, prio_b); | |
20 | } | |
21 | }; | |
22 | match (a, b) { | |
23 | (Ok(a), Ok(b)) => { | |
24 | let (solution, prio) = with_priorities(interner, domain_goal, a, prio_a, b, prio_b); | |
25 | (Ok(solution), prio) | |
26 | } | |
27 | (Ok(solution), Err(_)) => (Ok(solution), prio_a), | |
28 | (Err(_), Ok(solution)) => (Ok(solution), prio_b), | |
29 | (Err(_), Err(e)) => (Err(e), prio_b), | |
30 | } | |
31 | } | |
32 | ||
33 | pub(super) fn with_priorities<I: Interner>( | |
34 | interner: &I, | |
35 | domain_goal: &DomainGoal<I>, | |
36 | a: Solution<I>, | |
37 | prio_a: ClausePriority, | |
38 | b: Solution<I>, | |
39 | prio_b: ClausePriority, | |
40 | ) -> (Solution<I>, ClausePriority) { | |
41 | match (prio_a, prio_b, a, b) { | |
42 | (ClausePriority::High, ClausePriority::Low, higher, lower) | |
43 | | (ClausePriority::Low, ClausePriority::High, lower, higher) => { | |
44 | // if we have a high-priority solution and a low-priority solution, | |
45 | // the high-priority solution overrides *if* they are both for the | |
46 | // same inputs -- we don't want a more specific high-priority | |
47 | // solution overriding a general low-priority one. Currently inputs | |
48 | // only matter for projections; in a goal like `AliasEq(<?0 as | |
49 | // Trait>::Type = ?1)`, ?0 is the input. | |
50 | let inputs_higher = calculate_inputs(interner, domain_goal, &higher); | |
51 | let inputs_lower = calculate_inputs(interner, domain_goal, &lower); | |
52 | if inputs_higher == inputs_lower { | |
53 | debug!( | |
54 | "preferring solution: {:?} over {:?} because of higher prio", | |
55 | higher, lower | |
56 | ); | |
57 | (higher, ClausePriority::High) | |
58 | } else { | |
59 | (higher.combine(lower, interner), ClausePriority::High) | |
60 | } | |
61 | } | |
62 | (_, _, a, b) => (a.combine(b, interner), prio_a), | |
63 | } | |
64 | } | |
65 | ||
66 | fn calculate_inputs<I: Interner>( | |
67 | interner: &I, | |
68 | domain_goal: &DomainGoal<I>, | |
69 | solution: &Solution<I>, | |
70 | ) -> Vec<GenericArg<I>> { | |
71 | if let Some(subst) = solution.constrained_subst() { | |
72 | let subst_goal = subst.value.subst.apply(&domain_goal, interner); | |
73 | subst_goal.inputs(interner) | |
74 | } else { | |
75 | domain_goal.inputs(interner) | |
76 | } | |
77 | } |