From 62bdfdc1e3399d26a16173d54e4b662ab2fa67f4 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Thu, 5 Dec 2024 14:25:55 -0800 Subject: [PATCH] Delay unfolding --- crates/flux-fhir-analysis/src/lib.rs | 32 +++++--------------------- crates/flux-infer/src/refine_tree.rs | 13 ++++++----- crates/flux-refineck/src/invariants.rs | 1 + crates/flux-refineck/src/lib.rs | 2 +- 4 files changed, 15 insertions(+), 33 deletions(-) diff --git a/crates/flux-fhir-analysis/src/lib.rs b/crates/flux-fhir-analysis/src/lib.rs index 3dedaeb8da..eeeae2af5f 100644 --- a/crates/flux-fhir-analysis/src/lib.rs +++ b/crates/flux-fhir-analysis/src/lib.rs @@ -119,7 +119,8 @@ fn qualifiers(genv: GlobalEnv) -> QueryResult> { .qualifiers() .map(|qualifier| { let wfckresults = wf::check_qualifier(genv, qualifier)?; - normalize(genv, conv::conv_qualifier(genv, qualifier, &wfckresults)?) + Ok(conv::conv_qualifier(genv, qualifier, &wfckresults)? + .normalize(genv.spec_func_defns()?)) }) .try_collect() } @@ -143,16 +144,7 @@ fn invariants_of(genv: GlobalEnv, item: &fhir::Item) -> QueryResult Err(query_bug!(item.owner_id.local_id(), "expected struct or enum"))?, }; let wfckresults = wf::check_invariants(genv, item.owner_id, params, invariants)?; - conv::conv_invariants( - genv, - item.owner_id.map(|it| it.def_id), - params, - invariants, - &wfckresults, - )? - .into_iter() - .map(|invariant| normalize(genv, invariant)) - .collect() + conv::conv_invariants(genv, item.owner_id.map(|it| it.def_id), params, invariants, &wfckresults) } fn predicates_of( @@ -487,23 +479,16 @@ fn variants_of( let wfckresults = genv.check_wf(local_id)?; let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt(); let variants = cx.conv_enum_variants(def_id, enum_def)?; - let variants = struct_compat::variants(genv, &variants, def_id)?; - let variants = variants - .into_iter() - .map(|variant| normalize(genv, variant)) - .try_collect()?; + let variants = rty::List::from_vec(struct_compat::variants(genv, &variants, def_id)?); rty::Opaqueness::Transparent(rty::EarlyBinder(variants)) } fhir::ItemKind::Struct(struct_def) => { let wfckresults = genv.check_wf(local_id)?; let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt(); cx.conv_struct_variant(def_id, struct_def)? - .map(|variant| { + .map(|variant| -> QueryResult<_> { let variants = struct_compat::variants(genv, &[variant], def_id)?; - variants - .into_iter() - .map(|variant| normalize(genv, variant)) - .try_collect() + Ok(rty::List::from_vec(variants)) }) .transpose()? .map(rty::EarlyBinder) @@ -528,7 +513,6 @@ fn fn_sig(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult Result<(), ErrorGuaranteed> { errors.into_result() } -fn normalize(genv: GlobalEnv, t: T) -> QueryResult { - Ok(t.normalize(genv.spec_func_defns()?)) -} - mod errors { use flux_errors::E0999; use flux_macros::Diagnostic; diff --git a/crates/flux-infer/src/refine_tree.rs b/crates/flux-infer/src/refine_tree.rs index a845e4e65a..53c3e14a81 100644 --- a/crates/flux-infer/src/refine_tree.rs +++ b/crates/flux-infer/src/refine_tree.rs @@ -233,8 +233,8 @@ impl RefineTree { Ok(RefineTree { root }) } - pub fn simplify(&mut self) { - self.root.borrow_mut().simplify(); + pub fn simplify(&mut self, genv: GlobalEnv) -> QueryResult { + self.root.borrow_mut().simplify(genv) } pub fn into_fixpoint(self, cx: &mut FixpointCtxt) -> QueryResult { @@ -414,14 +414,14 @@ impl std::ops::Deref for NodePtr { } impl Node { - fn simplify(&mut self) { + fn simplify(&mut self, genv: GlobalEnv) -> QueryResult { for child in &self.children { - child.borrow_mut().simplify(); + child.borrow_mut().simplify(genv)?; } match &mut self.kind { NodeKind::Head(pred, tag) => { - let pred = pred.simplify(); + let pred = pred.normalize(genv.spec_func_defns()?).simplify(); if pred.is_trivially_true() { self.kind = NodeKind::True; } else { @@ -430,7 +430,7 @@ impl Node { } NodeKind::True => {} NodeKind::Assumption(pred) => { - *pred = pred.simplify(); + *pred = pred.normalize(genv.spec_func_defns()?).simplify(); self.children .extract_if(|child| { matches!(child.borrow().kind, NodeKind::True) @@ -447,6 +447,7 @@ impl Node { if !self.is_leaf() && self.children.is_empty() { self.kind = NodeKind::True; } + Ok(()) } fn is_leaf(&self) -> bool { diff --git a/crates/flux-refineck/src/invariants.rs b/crates/flux-refineck/src/invariants.rs index 7e3459c72f..833655f1e5 100644 --- a/crates/flux-refineck/src/invariants.rs +++ b/crates/flux-refineck/src/invariants.rs @@ -61,6 +61,7 @@ fn check_invariant( 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 cstr = refine_tree.into_fixpoint(&mut fcx).emit(&genv)?; let errors = fcx diff --git a/crates/flux-refineck/src/lib.rs b/crates/flux-refineck/src/lib.rs index 1a4bf179b1..aff42abc11 100644 --- a/crates/flux-refineck/src/lib.rs +++ b/crates/flux-refineck/src/lib.rs @@ -89,7 +89,7 @@ fn invoke_fixpoint( if config::dump_constraint() { dbg::dump_item_info(genv.tcx(), local_id, ext, &refine_tree).unwrap(); } - refine_tree.simplify(); + refine_tree.simplify(genv).emit(&genv)?; let simp_ext = format!("simp.{}", ext); if config::dump_constraint() { dbg::dump_item_info(genv.tcx(), local_id, simp_ext, &refine_tree).unwrap();