12 use rustc::hir::def_id::DefId;
13 use rustc_target::spec::abi;
14 use crate::lowering::Lower;
15 use crate::generic_types;
18 crate fn wf_clause_for_raw_ptr<'tcx>(
19 tcx: ty::TyCtxt<'_, '_, 'tcx>,
20 mutbl: hir::Mutability
22 let ptr_ty = generic_types::raw_ptr(tcx, mutbl);
24 let wf_clause = ProgramClause {
25 goal: DomainGoal::WellFormed(WellFormed::Ty(ptr_ty)),
26 hypotheses: ty::List::empty(),
27 category: ProgramClauseCategory::WellFormed,
29 let wf_clause = Clause::Implies(wf_clause);
31 // `forall<T> { WellFormed(*const T). }`
32 tcx.mk_clauses(iter::once(wf_clause))
35 crate fn wf_clause_for_fn_ptr<'tcx>(
36 tcx: ty::TyCtxt<'_, '_, 'tcx>,
37 arity_and_output: usize,
39 unsafety: hir::Unsafety,
42 let fn_ptr = generic_types::fn_ptr(tcx, arity_and_output, variadic, unsafety, abi);
44 let wf_clause = ProgramClause {
45 goal: DomainGoal::WellFormed(WellFormed::Ty(fn_ptr)),
46 hypotheses: ty::List::empty(),
47 category: ProgramClauseCategory::WellFormed,
49 let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
51 // `forall <T1, ..., Tn+1> { WellFormed(for<> fn(T1, ..., Tn) -> Tn+1). }`
52 // where `n + 1` == `arity_and_output`
53 tcx.mk_clauses(iter::once(wf_clause))
56 crate fn wf_clause_for_slice<'tcx>(tcx: ty::TyCtxt<'_, '_, 'tcx>) -> Clauses<'tcx> {
57 let ty = generic_types::bound(tcx, 0);
58 let slice_ty = tcx.mk_slice(ty);
60 let sized_trait = match tcx.lang_items().sized_trait() {
61 Some(def_id) => def_id,
62 None => return ty::List::empty(),
64 let sized_implemented = ty::TraitRef {
66 substs: tcx.mk_substs_trait(ty, ty::List::empty()),
68 let sized_implemented: DomainGoal<'_> = ty::TraitPredicate {
69 trait_ref: sized_implemented
72 let wf_clause = ProgramClause {
73 goal: DomainGoal::WellFormed(WellFormed::Ty(slice_ty)),
74 hypotheses: tcx.mk_goals(
75 iter::once(tcx.mk_goal(GoalKind::DomainGoal(sized_implemented)))
77 category: ProgramClauseCategory::WellFormed,
79 let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
81 // `forall<T> { WellFormed([T]) :- Implemented(T: Sized). }`
82 tcx.mk_clauses(iter::once(wf_clause))
85 crate fn wf_clause_for_array<'tcx>(
86 tcx: ty::TyCtxt<'_, '_, 'tcx>,
87 length: &'tcx ty::Const<'tcx>
89 let ty = generic_types::bound(tcx, 0);
90 let array_ty = tcx.mk_ty(ty::Array(ty, length));
92 let sized_trait = match tcx.lang_items().sized_trait() {
93 Some(def_id) => def_id,
94 None => return ty::List::empty(),
96 let sized_implemented = ty::TraitRef {
98 substs: tcx.mk_substs_trait(ty, ty::List::empty()),
100 let sized_implemented: DomainGoal<'_> = ty::TraitPredicate {
101 trait_ref: sized_implemented
104 let wf_clause = ProgramClause {
105 goal: DomainGoal::WellFormed(WellFormed::Ty(array_ty)),
106 hypotheses: tcx.mk_goals(
107 iter::once(tcx.mk_goal(GoalKind::DomainGoal(sized_implemented)))
109 category: ProgramClauseCategory::WellFormed,
111 let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
113 // `forall<T> { WellFormed([T; length]) :- Implemented(T: Sized). }`
114 tcx.mk_clauses(iter::once(wf_clause))
117 crate fn wf_clause_for_tuple<'tcx>(
118 tcx: ty::TyCtxt<'_, '_, 'tcx>,
121 let type_list = generic_types::type_list(tcx, arity);
122 let tuple_ty = tcx.mk_ty(ty::Tuple(type_list));
124 let sized_trait = match tcx.lang_items().sized_trait() {
125 Some(def_id) => def_id,
126 None => return ty::List::empty(),
129 // If `arity == 0` (i.e. the unit type) or `arity == 1`, this list of
130 // hypotheses is actually empty.
131 let sized_implemented = type_list[0 .. std::cmp::max(arity, 1) - 1].iter()
132 .map(|ty| ty::TraitRef {
134 substs: tcx.mk_substs_trait(*ty, ty::List::empty()),
136 .map(|trait_ref| ty::TraitPredicate { trait_ref })
137 .map(|predicate| predicate.lower());
139 let wf_clause = ProgramClause {
140 goal: DomainGoal::WellFormed(WellFormed::Ty(tuple_ty)),
141 hypotheses: tcx.mk_goals(
142 sized_implemented.map(|domain_goal| {
143 tcx.mk_goal(GoalKind::DomainGoal(domain_goal))
146 category: ProgramClauseCategory::WellFormed,
148 let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
151 // forall<T1, ..., Tn-1, Tn> {
152 // WellFormed((T1, ..., Tn)) :-
153 // Implemented(T1: Sized),
155 // Implemented(Tn-1: Sized).
158 tcx.mk_clauses(iter::once(wf_clause))
161 crate fn wf_clause_for_ref<'tcx>(
162 tcx: ty::TyCtxt<'_, '_, 'tcx>,
163 mutbl: hir::Mutability
165 let region = tcx.mk_region(
166 ty::ReLateBound(ty::INNERMOST, ty::BoundRegion::BrAnon(0))
168 let ty = generic_types::bound(tcx, 1);
169 let ref_ty = tcx.mk_ref(region, ty::TypeAndMut {
174 let outlives: DomainGoal<'_> = ty::OutlivesPredicate(ty, region).lower();
175 let wf_clause = ProgramClause {
176 goal: DomainGoal::WellFormed(WellFormed::Ty(ref_ty)),
177 hypotheses: tcx.mk_goals(
178 iter::once(tcx.mk_goal(outlives.into_goal()))
180 category: ProgramClauseCategory::WellFormed,
182 let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
184 // `forall<'a, T> { WellFormed(&'a T) :- Outlives(T: 'a). }`
185 tcx.mk_clauses(iter::once(wf_clause))
188 crate fn wf_clause_for_fn_def<'tcx>(
189 tcx: ty::TyCtxt<'_, '_, 'tcx>,
192 let fn_def = generic_types::fn_def(tcx, def_id);
194 let wf_clause = ProgramClause {
195 goal: DomainGoal::WellFormed(WellFormed::Ty(fn_def)),
196 hypotheses: ty::List::empty(),
197 category: ProgramClauseCategory::WellFormed,
199 let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
201 // `forall <T1, ..., Tn+1> { WellFormed(fn some_fn(T1, ..., Tn) -> Tn+1). }`
202 // where `def_id` maps to the `some_fn` function definition
203 tcx.mk_clauses(iter::once(wf_clause))