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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
|
//! Calls `chalk-solve` to solve a `ty::Predicate`
//!
//! In order to call `chalk-solve`, this file must convert a `CanonicalChalkEnvironmentAndGoal` into
//! a Chalk uncanonical goal. It then calls Chalk, and converts the answer back into rustc solution.
pub(crate) mod db;
pub(crate) mod lowering;
use rustc_middle::infer::canonical::{CanonicalTyVarKind, CanonicalVarKind};
use rustc_middle::traits::ChalkRustInterner;
use rustc_middle::ty::query::Providers;
use rustc_middle::ty::{self, TyCtxt, TypeFoldable, TypeVisitable};
use rustc_infer::infer::canonical::{
Canonical, CanonicalVarValues, Certainty, QueryRegionConstraints, QueryResponse,
};
use rustc_infer::traits::{self, CanonicalChalkEnvironmentAndGoal};
use crate::chalk::db::RustIrDatabase as ChalkRustIrDatabase;
use crate::chalk::lowering::LowerInto;
use crate::chalk::lowering::{ParamsSubstitutor, PlaceholdersCollector, ReverseParamsSubstitutor};
use chalk_solve::Solution;
pub(crate) fn provide(p: &mut Providers) {
*p = Providers { evaluate_goal, ..*p };
}
pub(crate) fn evaluate_goal<'tcx>(
tcx: TyCtxt<'tcx>,
obligation: CanonicalChalkEnvironmentAndGoal<'tcx>,
) -> Result<&'tcx Canonical<'tcx, QueryResponse<'tcx, ()>>, traits::query::NoSolution> {
let interner = ChalkRustInterner { tcx };
// Chalk doesn't have a notion of `Params`, so instead we use placeholders.
let mut placeholders_collector = PlaceholdersCollector::new();
obligation.visit_with(&mut placeholders_collector);
let mut params_substitutor =
ParamsSubstitutor::new(tcx, placeholders_collector.next_ty_placeholder);
let obligation = obligation.fold_with(&mut params_substitutor);
let params = params_substitutor.params;
let max_universe = obligation.max_universe.index();
let lowered_goal: chalk_ir::UCanonical<
chalk_ir::InEnvironment<chalk_ir::Goal<ChalkRustInterner<'tcx>>>,
> = chalk_ir::UCanonical {
canonical: chalk_ir::Canonical {
binders: chalk_ir::CanonicalVarKinds::from_iter(
interner,
obligation.variables.iter().map(|v| match v.kind {
CanonicalVarKind::PlaceholderTy(_ty) => unimplemented!(),
CanonicalVarKind::PlaceholderRegion(_ui) => unimplemented!(),
CanonicalVarKind::Ty(ty) => match ty {
CanonicalTyVarKind::General(ui) => chalk_ir::WithKind::new(
chalk_ir::VariableKind::Ty(chalk_ir::TyVariableKind::General),
chalk_ir::UniverseIndex { counter: ui.index() },
),
CanonicalTyVarKind::Int => chalk_ir::WithKind::new(
chalk_ir::VariableKind::Ty(chalk_ir::TyVariableKind::Integer),
chalk_ir::UniverseIndex::root(),
),
CanonicalTyVarKind::Float => chalk_ir::WithKind::new(
chalk_ir::VariableKind::Ty(chalk_ir::TyVariableKind::Float),
chalk_ir::UniverseIndex::root(),
),
},
CanonicalVarKind::Region(ui) => chalk_ir::WithKind::new(
chalk_ir::VariableKind::Lifetime,
chalk_ir::UniverseIndex { counter: ui.index() },
),
CanonicalVarKind::Const(_ui, _ty) => unimplemented!(),
CanonicalVarKind::PlaceholderConst(_pc, _ty) => unimplemented!(),
}),
),
value: obligation.value.lower_into(interner),
},
universes: max_universe + 1,
};
use chalk_solve::Solver;
let mut solver = chalk_engine::solve::SLGSolver::new(32, None);
let db = ChalkRustIrDatabase { interner };
debug!(?lowered_goal);
let solution = solver.solve(&db, &lowered_goal);
debug!(?obligation, ?solution, "evaluate goal");
// Ideally, the code to convert *back* to rustc types would live close to
// the code to convert *from* rustc types. Right now though, we don't
// really need this and so it's really minimal.
// Right now, we also treat a `Unique` solution the same as
// `Ambig(Definite)`. This really isn't right.
let make_solution = |subst: chalk_ir::Substitution<_>,
binders: chalk_ir::CanonicalVarKinds<_>| {
use rustc_middle::infer::canonical::CanonicalVarInfo;
let mut reverse_param_substitutor = ReverseParamsSubstitutor::new(tcx, params);
let var_values = tcx.mk_substs_from_iter(
subst
.as_slice(interner)
.iter()
.map(|p| p.lower_into(interner).fold_with(&mut reverse_param_substitutor)),
);
let variables = binders.iter(interner).map(|var| {
let kind = match var.kind {
chalk_ir::VariableKind::Ty(ty_kind) => CanonicalVarKind::Ty(match ty_kind {
chalk_ir::TyVariableKind::General => CanonicalTyVarKind::General(
ty::UniverseIndex::from_usize(var.skip_kind().counter),
),
chalk_ir::TyVariableKind::Integer => CanonicalTyVarKind::Int,
chalk_ir::TyVariableKind::Float => CanonicalTyVarKind::Float,
}),
chalk_ir::VariableKind::Lifetime => {
CanonicalVarKind::Region(ty::UniverseIndex::from_usize(var.skip_kind().counter))
}
// FIXME(compiler-errors): We don't currently have a way of turning
// a Chalk ty back into a rustc ty, right?
chalk_ir::VariableKind::Const(_) => todo!(),
};
CanonicalVarInfo { kind }
});
let max_universe = binders.iter(interner).map(|v| v.skip_kind().counter).max().unwrap_or(0);
let sol = Canonical {
max_universe: ty::UniverseIndex::from_usize(max_universe),
variables: tcx.mk_canonical_var_infos_from_iter(variables),
value: QueryResponse {
var_values: CanonicalVarValues { var_values },
region_constraints: QueryRegionConstraints::default(),
certainty: Certainty::Proven,
opaque_types: vec![],
value: (),
},
};
tcx.arena.alloc(sol)
};
solution
.map(|s| match s {
Solution::Unique(subst) => {
// FIXME(chalk): handle constraints
make_solution(subst.value.subst, subst.binders)
}
Solution::Ambig(guidance) => {
match guidance {
chalk_solve::Guidance::Definite(subst) => {
make_solution(subst.value, subst.binders)
}
chalk_solve::Guidance::Suggested(_) => unimplemented!(),
chalk_solve::Guidance::Unknown => {
// chalk_fulfill doesn't use the var_values here, so
// let's just ignore that
let sol = Canonical {
max_universe: ty::UniverseIndex::from_usize(0),
variables: obligation.variables,
value: QueryResponse {
var_values: CanonicalVarValues::dummy(),
region_constraints: QueryRegionConstraints::default(),
certainty: Certainty::Ambiguous,
opaque_types: vec![],
value: (),
},
};
&*tcx.arena.alloc(sol)
}
}
}
})
.ok_or(traits::query::NoSolution)
}
|
