Skip to content

Commit 1247793

Browse files
committed
it's quite unsightly and maybe it would be better to use directly Clauses instead of Predicates (from rustc_middle::ty), Also, it might be the reason the translation is a bit shuffled, so, maybe it would be better to change those modifications
1 parent 159d0c6 commit 1247793

File tree

3 files changed

+23
-7
lines changed

3 files changed

+23
-7
lines changed

creusot/src/ctx.rs

Lines changed: 14 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,10 @@ use rustc_infer::traits::{Obligation, ObligationCause};
2929
use rustc_middle::{
3030
mir::{Body, Promoted},
3131
thir,
32-
ty::{subst::InternalSubsts, GenericArg, ParamEnv, SubstsRef, Ty, TyCtxt, Visibility},
32+
ty::{
33+
subst::InternalSubsts, Clause, GenericArg, ParamEnv, Predicate, SubstsRef, Ty, TyCtxt,
34+
Visibility,
35+
},
3336
};
3437
use rustc_span::{RealFileName, Span, Symbol, DUMMY_SP};
3538
use rustc_trait_selection::traits::SelectionContext;
@@ -354,9 +357,17 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
354357
}
355358
}
356359

357-
additional_predicates.extend(base_env.caller_bounds());
360+
additional_predicates.extend::<Vec<Predicate>>(
361+
base_env.caller_bounds().into_iter().map(Clause::as_predicate).collect(),
362+
);
358363
ParamEnv::new(
359-
self.mk_predicates(&additional_predicates),
364+
self.mk_clauses(
365+
&(additional_predicates
366+
.into_iter()
367+
.map(Predicate::expect_clause)
368+
.collect::<Vec<Clause>>()
369+
.as_slice()),
370+
),
360371
rustc_infer::traits::Reveal::UserFacing,
361372
rustc_hir::Constness::NotConst,
362373
)

creusot/src/translation/external.rs

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ use rustc_middle::{
1010
thir::{self, visit::Visitor, Expr, ExprKind, Thir},
1111
ty::{
1212
subst::{GenericArgKind, InternalSubsts, SubstsRef},
13-
EarlyBinder, Predicate, TyCtxt, TyKind,
13+
Clause, EarlyBinder, Predicate, TyCtxt, TyKind,
1414
},
1515
};
1616
use rustc_span::Symbol;
@@ -131,8 +131,13 @@ pub(crate) fn extract_extern_specs_from_item<'tcx>(
131131

132132
let contract = crate::specification::contract_clauses_of(ctx, def_id.to_def_id()).unwrap();
133133

134-
let additional_predicates =
135-
ctx.predicates_of(def_id).instantiate(ctx.tcx, subst).predicates.into_iter().collect();
134+
let additional_predicates = ctx
135+
.predicates_of(def_id)
136+
.instantiate(ctx.tcx, subst)
137+
.predicates
138+
.into_iter()
139+
.map(Clause::as_predicate)
140+
.collect();
136141

137142
let arg_subst = ctx
138143
.fn_arg_names(def_id)

creusot/src/translation/traits.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -305,7 +305,7 @@ pub(crate) fn resolve_assoc_item_opt<'tcx>(
305305
Some((leaf_def.item.def_id, leaf_substs))
306306
}
307307
ImplSource::Param(_, _) => Some((def_id, substs)),
308-
ImplSource::Builtin(impl_data) => match *substs.type_at(0).kind() {
308+
ImplSource::Builtin(_) => match *substs.type_at(0).kind() {
309309
rustc_middle::ty::Closure(closure_def_id, closure_substs) => {
310310
Some((closure_def_id, closure_substs))
311311
}

0 commit comments

Comments
 (0)