1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
use crate::infer::InferenceTable;
use chalk_ir::fold::Fold;
use chalk_ir::interner::{HasInterner, Interner};
use chalk_ir::*;
pub trait CanonicalExt<T: HasInterner, I: Interner> {
fn map<OP, U>(self, interner: &I, op: OP) -> Canonical<U::Result>
where
OP: FnOnce(T::Result) -> U,
T: Fold<I>,
U: Fold<I>,
U::Result: HasInterner<Interner = I>;
}
impl<T, I> CanonicalExt<T, I> for Canonical<T>
where
T: HasInterner<Interner = I>,
I: Interner,
{
fn map<OP, U>(self, interner: &I, op: OP) -> Canonical<U::Result>
where
OP: FnOnce(T::Result) -> U,
T: Fold<I>,
U: Fold<I>,
U::Result: HasInterner<Interner = I>,
{
let mut infer = InferenceTable::new();
let snapshot = infer.snapshot();
let instantiated_value = infer.instantiate_canonical(interner, &self);
let mapped_value = op(instantiated_value);
let result = infer.canonicalize(interner, &mapped_value);
infer.rollback_to(snapshot);
result.quantified
}
}
pub trait GoalExt<I: Interner> {
fn into_peeled_goal(self, interner: &I) -> UCanonical<InEnvironment<Goal<I>>>;
fn into_closed_goal(self, interner: &I) -> UCanonical<InEnvironment<Goal<I>>>;
}
impl<I: Interner> GoalExt<I> for Goal<I> {
fn into_peeled_goal(self, interner: &I) -> UCanonical<InEnvironment<Goal<I>>> {
let mut infer = InferenceTable::new();
let peeled_goal = {
let mut env_goal = InEnvironment::new(&Environment::new(interner), self);
loop {
let InEnvironment { environment, goal } = env_goal;
match goal.data(interner) {
GoalData::Quantified(QuantifierKind::ForAll, subgoal) => {
let subgoal = infer.instantiate_binders_universally(interner, subgoal);
env_goal = InEnvironment::new(&environment, subgoal);
}
GoalData::Quantified(QuantifierKind::Exists, subgoal) => {
let subgoal = infer.instantiate_binders_existentially(interner, subgoal);
env_goal = InEnvironment::new(&environment, subgoal);
}
GoalData::Implies(wc, subgoal) => {
let new_environment =
environment.add_clauses(interner, wc.iter(interner).cloned());
env_goal = InEnvironment::new(&new_environment, Goal::clone(subgoal));
}
_ => break InEnvironment::new(&environment, goal),
}
}
};
let canonical = infer.canonicalize(interner, &peeled_goal).quantified;
infer.u_canonicalize(interner, &canonical).quantified
}
fn into_closed_goal(self, interner: &I) -> UCanonical<InEnvironment<Goal<I>>> {
let mut infer = InferenceTable::new();
let env_goal = InEnvironment::new(&Environment::new(interner), self);
let canonical_goal = infer.canonicalize(interner, &env_goal).quantified;
infer.u_canonicalize(interner, &canonical_goal).quantified
}
}