Move some stuff around

crates/flux-infer/src/fixpoint_encoding.rs

@@ -19,6 +19,7 @@ use flux_middle::{
     global_env::GlobalEnv,
     queries::QueryResult,
     rty::{self, BoundVariableKind, ESpan, Lambda, List},
+    MaybeExternId,
 };
 use itertools::Itertools;
 use liquid_fixpoint::FixpointResult;
@@ -320,7 +321,7 @@ pub struct FixpointCtxt<'genv, 'tcx, T: Eq + Hash> {
     tags_inv: UnordMap<T, TagIdx>,
     /// [`DefId`] of the item being checked. This can be a function/method or an adt when checking
     /// invariants.
-    def_id: LocalDefId,
+    def_id: MaybeExternId,
 }
 
 pub type FixQueryCache = QueryCache<FixpointResult<TagIdx>>;
@@ -329,7 +330,7 @@ impl<'genv, 'tcx, Tag> FixpointCtxt<'genv, 'tcx, Tag>
 where
     Tag: std::hash::Hash + Eq + Copy,
 {
-    pub fn new(genv: GlobalEnv<'genv, 'tcx>, def_id: LocalDefId, kvars: KVarGen) -> Self {
+    pub fn new(genv: GlobalEnv<'genv, 'tcx>, def_id: MaybeExternId, kvars: KVarGen) -> Self {
         let def_span = genv.tcx().def_span(def_id);
         Self {
             comments: vec![],
@@ -361,7 +362,9 @@ where
 
         let constraint = self.ecx.assume_const_values(constraint);
 
-        let qualifiers = self.ecx.qualifiers_for(self.def_id, &mut self.scx)?;
+        let qualifiers = self
+            .ecx
+            .qualifiers_for(self.def_id.local_id(), &mut self.scx)?;
 
         let mut constants = self
             .ecx
@@ -397,7 +400,7 @@ where
             data_decls: self.scx.into_data_decls(),
         };
         if config::dump_constraint() {
-            dbg::dump_item_info(self.genv.tcx(), self.def_id, "smt2", &task).unwrap();
+            dbg::dump_item_info(self.genv.tcx(), self.def_id.resolved_id(), "smt2", &task).unwrap();
         }
 
         let task_key = self.genv.tcx().def_path_str(self.def_id);

crates/flux-infer/src/refine_tree.rs

@@ -14,8 +14,8 @@ use flux_middle::{
         canonicalize::{Hoister, HoisterDelegate},
         evars::EVarSol,
         fold::{TypeFoldable, TypeSuperVisitable, TypeVisitable, TypeVisitor},
-        BaseTy, EarlyBinder, EarlyReftParam, Expr, GenericArgs, Name, Sort, Ty, TyCtor, TyKind,
-        Var,
+        BaseTy, EarlyBinder, EarlyReftParam, Expr, GenericArgs, Name, Sort, SpecFuncDefns, Ty,
+        TyCtor, TyKind, Var,
     },
 };
 use itertools::Itertools;
@@ -234,8 +234,8 @@ impl RefineTree {
         Ok(RefineTree { root })
     }
 
-    pub fn simplify(&mut self, genv: GlobalEnv) -> QueryResult {
-        self.root.borrow_mut().simplify(genv)
+    pub fn simplify(&mut self, defns: &SpecFuncDefns) {
+        self.root.borrow_mut().simplify(defns)
     }
 
     pub fn into_fixpoint(self, cx: &mut FixpointCtxt<Tag>) -> QueryResult<fixpoint::Constraint> {
@@ -415,14 +415,14 @@ impl std::ops::Deref for NodePtr {
 }
 
 impl Node {
-    fn simplify(&mut self, genv: GlobalEnv) -> QueryResult {
+    fn simplify(&mut self, defns: &SpecFuncDefns) {
         for child in &self.children {
-            child.borrow_mut().simplify(genv)?;
+            child.borrow_mut().simplify(defns);
         }
 
         match &mut self.kind {
             NodeKind::Head(pred, tag) => {
-                let pred = pred.normalize(genv.spec_func_defns()?).simplify();
+                let pred = pred.normalize(defns).simplify();
                 if pred.is_trivially_true() {
                     self.kind = NodeKind::True;
                 } else {
@@ -431,7 +431,7 @@ impl Node {
             }
             NodeKind::True => {}
             NodeKind::Assumption(pred) => {
-                *pred = pred.normalize(genv.spec_func_defns()?).simplify();
+                *pred = pred.normalize(defns).simplify();
                 self.children
                     .extract_if(|child| {
                         matches!(child.borrow().kind, NodeKind::True)
@@ -448,7 +448,6 @@ impl Node {
         if !self.is_leaf() && self.children.is_empty() {
             self.kind = NodeKind::True;
         }
-        Ok(())
     }
 
     fn is_leaf(&self) -> bool {

crates/flux-middle/src/rty/expr.rs

@@ -119,7 +119,9 @@ impl ESpan {
     }
 }
 
-#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeFoldable, TypeVisitable)]
+#[derive(
+    Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeFoldable, TypeVisitable,
+)]
 pub enum BinOp {
     Iff,
     Imp,
@@ -1144,6 +1146,7 @@ mod pretty {
                 }
             }
             let e = if cx.simplify_exprs { self.simplify() } else { self.clone() };
+            // w!("{:?}@(", ^e.span())?;
             match e.kind() {
                 ExprKind::Var(var) => w!("{:?}", var),
                 ExprKind::Local(local) => w!("{:?}", ^local),
@@ -1221,8 +1224,8 @@ mod pretty {
                     }
                 }
                 ExprKind::App(func, args) => {
-                    w!("({:?})({})",
-                        func,
+                    w!("{:?}({})",
+                        parens!(func, !func.is_atom()),
                         ^args
                             .iter()
                             .format_with(", ", |arg, f| f(&format_args_cx!("{:?}", arg)))
@@ -1253,7 +1256,9 @@ mod pretty {
                         w!("{:?}", expr.as_ref().skip_binder())
                     })
                 }
-            }
+            }?;
+            // w!(")")
+            Ok(())
         }
     }
 

crates/flux-refineck/src/checker.rs

@@ -1950,7 +1950,7 @@ pub(crate) mod errors {
             Self { kind: CheckerErrKind::OpaqueStruct(def_id), span }
         }
 
-        pub fn emit_err(self, genv: &GlobalEnv, fn_def_id: MaybeExternId) -> ErrorGuaranteed {
+        pub fn emit(self, genv: GlobalEnv, fn_def_id: MaybeExternId) -> ErrorGuaranteed {
             let dcx = genv.sess().dcx().handle();
             match self.kind {
                 CheckerErrKind::Inference => {

crates/flux-refineck/src/invariants.rs

@@ -1,5 +1,4 @@
-use flux_common::{dbg, iter::IterExt, result::ResultExt};
-use flux_config as config;
+use flux_common::{cache::QueryCache, iter::IterExt, result::ResultExt};
 use flux_errors::ErrorGuaranteed;
 use flux_infer::{
     fixpoint_encoding::{FixQueryCache, FixpointCtxt, KVarGen},
@@ -9,7 +8,7 @@ use flux_infer::{
 use flux_middle::{fhir, global_env::GlobalEnv, rty, MaybeExternId};
 use rustc_span::{Span, DUMMY_SP};
 
-use crate::CheckerConfig;
+use crate::{invoke_fixpoint, CheckerConfig};
 
 pub fn check_invariants(
     genv: GlobalEnv,
@@ -57,16 +56,17 @@ fn check_invariant(
         let pred = invariant.apply(&variant.idx);
         rcx.check_pred(&pred, Tag::new(ConstrReason::Other, DUMMY_SP));
     }
-    let mut fcx = FixpointCtxt::new(genv, def_id.local_id(), KVarGen::dummy());
-    if config::dump_constraint() {
-        dbg::dump_item_info(genv.tcx(), def_id.local_id(), "fluxc", &refine_tree).unwrap();
-    }
-    refine_tree.simplify(genv).emit(&genv)?;
+    let errors = invoke_fixpoint(
+        genv,
+        cache,
+        def_id,
+        refine_tree,
+        KVarGen::dummy(),
+        checker_config,
+        "fluxc",
+    )
+    .emit(&genv)?;
 
-    let cstr = refine_tree.into_fixpoint(&mut fcx).emit(&genv)?;
-    let errors = fcx
-        .check(cache, cstr, checker_config.scrape_quals)
-        .emit(&genv)?;
     if errors.is_empty() {
         Ok(())
     } else {

crates/flux-refineck/src/lib.rs

@@ -80,24 +80,24 @@ fn report_fixpoint_errors(
 fn invoke_fixpoint(
     genv: GlobalEnv,
     cache: &mut FixQueryCache,
-    local_id: LocalDefId,
+    def_id: MaybeExternId,
     mut refine_tree: RefineTree,
     kvars: KVarGen,
     config: CheckerConfig,
     ext: &str,
-) -> Result<Vec<Tag>, ErrorGuaranteed> {
+) -> QueryResult<Vec<Tag>> {
     if config::dump_constraint() {
-        dbg::dump_item_info(genv.tcx(), local_id, ext, &refine_tree).unwrap();
+        dbg::dump_item_info(genv.tcx(), def_id.resolved_id(), ext, &refine_tree).unwrap();
     }
-    refine_tree.simplify(genv).emit(&genv)?;
+    refine_tree.simplify(genv.spec_func_defns()?);
     let simp_ext = format!("simp.{}", ext);
     if config::dump_constraint() {
-        dbg::dump_item_info(genv.tcx(), local_id, simp_ext, &refine_tree).unwrap();
+        dbg::dump_item_info(genv.tcx(), def_id.resolved_id(), simp_ext, &refine_tree).unwrap();
     }
 
-    let mut fcx = FixpointCtxt::new(genv, local_id, kvars);
-    let cstr = refine_tree.into_fixpoint(&mut fcx).emit(&genv)?;
-    fcx.check(cache, cstr, config.scrape_quals).emit(&genv)
+    let mut fcx = FixpointCtxt::new(genv, def_id, kvars);
+    let cstr = refine_tree.into_fixpoint(&mut fcx)?;
+    fcx.check(cache, cstr, config.scrape_quals)
 }
 
 pub fn check_fn(
@@ -147,34 +147,34 @@ pub fn check_fn(
     dbg::check_fn_span!(genv.tcx(), local_id).in_scope(|| {
         let ghost_stmts = compute_ghost_statements(genv, local_id)
             .with_span(span)
-            .map_err(|err| err.emit_err(&genv, def_id))?;
+            .map_err(|err| err.emit(genv, def_id))?;
 
         // PHASE 1: infer shape of `TypeEnv` at the entry of join points
         let shape_result = Checker::run_in_shape_mode(genv, local_id, &ghost_stmts, config)
-            // Augment the possible CheckError with the functions span so we can report
-            // helpful error messages for opaque struct field accesses
-            .map_err(|err| err.emit_err(&genv, def_id))?;
+            .map_err(|err| err.emit(genv, def_id))?;
         tracing::info!("check_fn::shape");
 
         // PHASE 2: generate refinement tree constraint
         let (refine_tree, kvars) =
             Checker::run_in_refine_mode(genv, local_id, &ghost_stmts, shape_result, config)
-                .map_err(|err| err.emit_err(&genv, def_id))?;
+                .map_err(|err| err.emit(genv, def_id))?;
         tracing::info!("check_fn::refine");
 
         // PHASE 3: invoke fixpoint on the constraint
-        let errors = invoke_fixpoint(genv, cache, local_id, refine_tree, kvars, config, "fluxc")?;
+        let errors = invoke_fixpoint(genv, cache, def_id, refine_tree, kvars, config, "fluxc")
+            .emit(&genv)?;
         tracing::info!("check_fn::fixpoint");
         report_fixpoint_errors(genv, local_id, errors)?;
 
         // PHASE 4: subtyping check for trait-method implementations
         if let Some((refine_tree, kvars)) =
             trait_impl_subtyping(genv, local_id, config.check_overflow, span)
-                .map_err(|err| err.emit_err(&genv, def_id))?
+                .map_err(|err| err.emit(genv, def_id))?
         {
             tracing::info!("check_fn::refine-subtyping");
             let errors =
-                invoke_fixpoint(genv, cache, local_id, refine_tree, kvars, config, "sub.fluxc")?;
+                invoke_fixpoint(genv, cache, def_id, refine_tree, kvars, config, "sub.fluxc")
+                    .emit(&genv)?;
             tracing::info!("check_fn::fixpoint-subtyping");
             report_fixpoint_errors(genv, local_id, errors)?;
         }

tests/tests/neg/error_messages/localize02.rs

@@ -9,7 +9,7 @@
     }
 
     fn inc1(x: int) -> int {
-        x + 1   //~ NOTE this is the condition
+        x + 1
     }
 }]
 
@@ -21,7 +21,7 @@ fn test() {
                  //~| NOTE a precondition cannot be proved
 }
 
-#[flux::sig(fn() -> i32[inc1(0)])] //~ NOTE inside this call
+#[flux::sig(fn() -> i32[inc1(0)])] //~ NOTE this is the condition
 fn moo() -> i32 {
     2 //~ ERROR refinement type
       //~| NOTE a postcondition cannot be proved