Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
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
  • Loading branch information
floriangru committed Jul 6, 2023
1 parent 159d0c6 commit 1247793
Show file tree
Hide file tree
Showing 3 changed files with 23 additions and 7 deletions.
17 changes: 14 additions & 3 deletions creusot/src/ctx.rs
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,10 @@ use rustc_infer::traits::{Obligation, ObligationCause};
use rustc_middle::{
mir::{Body, Promoted},
thir,
ty::{subst::InternalSubsts, GenericArg, ParamEnv, SubstsRef, Ty, TyCtxt, Visibility},
ty::{
subst::InternalSubsts, Clause, GenericArg, ParamEnv, Predicate, SubstsRef, Ty, TyCtxt,
Visibility,
},
};
use rustc_span::{RealFileName, Span, Symbol, DUMMY_SP};
use rustc_trait_selection::traits::SelectionContext;
Expand Down Expand Up @@ -354,9 +357,17 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
}
}

additional_predicates.extend(base_env.caller_bounds());
additional_predicates.extend::<Vec<Predicate>>(
base_env.caller_bounds().into_iter().map(Clause::as_predicate).collect(),
);
ParamEnv::new(
self.mk_predicates(&additional_predicates),
self.mk_clauses(
&(additional_predicates
.into_iter()
.map(Predicate::expect_clause)
.collect::<Vec<Clause>>()
.as_slice()),
),
rustc_infer::traits::Reveal::UserFacing,
rustc_hir::Constness::NotConst,
)
Expand Down
11 changes: 8 additions & 3 deletions creusot/src/translation/external.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ use rustc_middle::{
thir::{self, visit::Visitor, Expr, ExprKind, Thir},
ty::{
subst::{GenericArgKind, InternalSubsts, SubstsRef},
EarlyBinder, Predicate, TyCtxt, TyKind,
Clause, EarlyBinder, Predicate, TyCtxt, TyKind,
},
};
use rustc_span::Symbol;
Expand Down Expand Up @@ -131,8 +131,13 @@ pub(crate) fn extract_extern_specs_from_item<'tcx>(

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

let additional_predicates =
ctx.predicates_of(def_id).instantiate(ctx.tcx, subst).predicates.into_iter().collect();
let additional_predicates = ctx
.predicates_of(def_id)
.instantiate(ctx.tcx, subst)
.predicates
.into_iter()
.map(Clause::as_predicate)
.collect();

let arg_subst = ctx
.fn_arg_names(def_id)
Expand Down
2 changes: 1 addition & 1 deletion creusot/src/translation/traits.rs
Original file line number Diff line number Diff line change
Expand Up @@ -305,7 +305,7 @@ pub(crate) fn resolve_assoc_item_opt<'tcx>(
Some((leaf_def.item.def_id, leaf_substs))
}
ImplSource::Param(_, _) => Some((def_id, substs)),
ImplSource::Builtin(impl_data) => match *substs.type_at(0).kind() {
ImplSource::Builtin(_) => match *substs.type_at(0).kind() {
rustc_middle::ty::Closure(closure_def_id, closure_substs) => {
Some((closure_def_id, closure_substs))
}
Expand Down

0 comments on commit 1247793

Please sign in to comment.