Remove some unstable dependencies from fixpoint crate

flux-rs · Jan 3, 2024 · 2c2ea53 · 2c2ea53
1 parent 4e0ae3a
commit 2c2ea53
Show file tree

Hide file tree

Showing 6 changed files with 18 additions and 18 deletions.
diff --git 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<T: Types> {
 pub enum Func<T: Types> {
     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
@@ -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<T: Types> {
     pub name: T::Var,
-    pub orig: rustc_span::Symbol,
+    pub orig: String,
     pub sort: Sort,
 }
 
@@ -154,10 +153,10 @@ impl<T: Types> Task<T> {
 
         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
@@ -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
@@ -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
@@ -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
@@ -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!(