From 2c2ea53dc4052c7718e3e7f1ba131f7d74736a83 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Wed, 3 Jan 2024 09:41:12 -0800 Subject: [PATCH] Remove some unstable dependencies from fixpoint crate --- crates/flux-fixpoint/src/constraint.rs | 3 +-- crates/flux-fixpoint/src/lib.rs | 13 ++++++------- crates/flux-middle/src/queries.rs | 8 ++++---- crates/flux-middle/src/rty/mod.rs | 4 ++-- crates/flux-middle/src/rustc/lowering.rs | 2 +- crates/flux-refineck/src/fixpoint_encoding.rs | 6 ++++-- 6 files changed, 18 insertions(+), 18 deletions(-) diff --git a/crates/flux-fixpoint/src/constraint.rs b/crates/flux-fixpoint/src/constraint.rs index 181d61bbe2..0f25e29713 100644 --- a/crates/flux-fixpoint/src/constraint.rs +++ b/crates/flux-fixpoint/src/constraint.rs @@ -7,7 +7,6 @@ use derive_where::derive_where; use flux_common::format::PadAdapter; use itertools::Itertools; use rustc_macros::{Decodable, Encodable}; -use rustc_span::Symbol; use crate::{big_int::BigInt, StringTypes, Types}; @@ -73,7 +72,7 @@ pub enum Expr { pub enum Func { Var(T::Var), /// interpreted (theory) function - Itf(Symbol), + Itf(String), } #[derive(Clone, Copy, Hash)] diff --git a/crates/flux-fixpoint/src/lib.rs b/crates/flux-fixpoint/src/lib.rs index 46985d2ad5..5b6905c3f4 100644 --- a/crates/flux-fixpoint/src/lib.rs +++ b/crates/flux-fixpoint/src/lib.rs @@ -1,8 +1,7 @@ -#![feature(rustc_private, min_specialization, lazy_cell, box_patterns, let_chains)] +#![feature(rustc_private, lazy_cell, box_patterns)] extern crate rustc_macros; extern crate rustc_serialize; -extern crate rustc_span; pub mod big_int; mod constraint; @@ -73,7 +72,7 @@ impl Types for StringTypes { #[derive_where(Hash)] pub struct ConstInfo { pub name: T::Var, - pub orig: rustc_span::Symbol, + pub orig: String, pub sort: Sort, } @@ -154,10 +153,10 @@ impl Task { let result = self.check(); - if config::is_cache_enabled() - && let Ok(FixpointResult::Safe(_)) = result - { - cache.insert(key, hash); + if config::is_cache_enabled() { + if let Ok(FixpointResult::Safe(_)) = result { + cache.insert(key, hash); + } } result } diff --git a/crates/flux-middle/src/queries.rs b/crates/flux-middle/src/queries.rs index 9f128067b5..8d7bed6e7e 100644 --- a/crates/flux-middle/src/queries.rs +++ b/crates/flux-middle/src/queries.rs @@ -128,7 +128,7 @@ impl<'tcx> Queries<'tcx> { run_with_cache(&self.lower_generics_of, def_id, || { let generics = genv.tcx.generics_of(def_id); lowering::lower_generics(generics) - .map_err(UnsupportedReason::to_err) + .map_err(UnsupportedReason::into_err) .map_err(|err| QueryErr::unsupported(genv.tcx, def_id, err)) }) } @@ -154,7 +154,7 @@ impl<'tcx> Queries<'tcx> { let ty = genv.tcx.type_of(def_id).instantiate_identity(); Ok(ty::EarlyBinder( lowering::lower_ty(genv.tcx, ty) - .map_err(UnsupportedReason::to_err) + .map_err(UnsupportedReason::into_err) .map_err(|err| QueryErr::unsupported(genv.tcx, def_id, err))?, )) }) @@ -176,7 +176,7 @@ impl<'tcx> Queries<'tcx> { .normalize(fn_sig.instantiate_identity()); Ok(ty::EarlyBinder( lowering::lower_fn_sig(genv.tcx, result.value) - .map_err(UnsupportedReason::to_err) + .map_err(UnsupportedReason::into_err) .map_err(|err| QueryErr::unsupported(genv.tcx, def_id, err))?, )) }) @@ -375,7 +375,7 @@ impl<'tcx> Queries<'tcx> { let hir_id = genv.hir().local_def_id_to_hir_id(def_id); let bound_vars = genv.tcx.late_bound_vars(hir_id); lowering::lower_bound_vars(bound_vars) - .map_err(UnsupportedReason::to_err) + .map_err(UnsupportedReason::into_err) .map_err(|err| QueryErr::unsupported(genv.tcx, def_id.to_def_id(), err)) }) } diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 5a99184ae3..31d9599004 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -143,7 +143,7 @@ pub struct GeneratorObligPredicate { pub output: Ty, } -#[derive(Copy, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] +#[derive(Copy, Clone, PartialEq, Eq, Hash, Encodable, Decodable)] pub enum SortCtor { Set, Map, @@ -153,7 +153,7 @@ pub enum SortCtor { /// [SortVar] are used for polymorphic sorts (Set, Map etc.) and they should occur /// "bound" under a PolyFuncSort; i.e. should be < than the number of params in the /// PolyFuncSort. -#[derive(Clone, PartialEq, Eq, Debug, Hash, TyEncodable, TyDecodable)] +#[derive(Clone, PartialEq, Eq, Debug, Hash, Encodable, Decodable)] pub struct SortVar { pub index: usize, } diff --git a/crates/flux-middle/src/rustc/lowering.rs b/crates/flux-middle/src/rustc/lowering.rs index 47397838ae..3ab2786d87 100644 --- a/crates/flux-middle/src/rustc/lowering.rs +++ b/crates/flux-middle/src/rustc/lowering.rs @@ -52,7 +52,7 @@ impl UnsupportedReason { UnsupportedReason { descr: reason.to_string() } } - pub(crate) fn to_err(self) -> UnsupportedErr { + pub(crate) fn into_err(self) -> UnsupportedErr { UnsupportedErr { descr: self.descr, span: None } } } diff --git a/crates/flux-refineck/src/fixpoint_encoding.rs b/crates/flux-refineck/src/fixpoint_encoding.rs index 8f8bb2ee69..c01bfa734f 100644 --- a/crates/flux-refineck/src/fixpoint_encoding.rs +++ b/crates/flux-refineck/src/fixpoint_encoding.rs @@ -305,7 +305,7 @@ where .map(|const_info| { fixpoint::ConstInfo { name: fixpoint::Var::Global(const_info.name), - orig: const_info.sym, + orig: const_info.sym.to_string(), sort: const_info.sort, } }) @@ -766,7 +766,9 @@ impl<'a> ExprCtxt<'a> { fn func_to_fixpoint(&self, func: &rty::Expr) -> fixpoint::Func { match func.kind() { rty::ExprKind::Var(var) => fixpoint::Func::Var(self.var_to_fixpoint(var).into()), - rty::ExprKind::GlobalFunc(_, FuncKind::Thy(sym)) => fixpoint::Func::Itf(*sym), + rty::ExprKind::GlobalFunc(_, FuncKind::Thy(sym)) => { + fixpoint::Func::Itf(sym.to_string()) + } rty::ExprKind::GlobalFunc(sym, FuncKind::Uif) => { let cinfo = self.const_map.get(&Key::Uif(*sym)).unwrap_or_else(|| { span_bug!(