diff --git a/crates/formality-core/src/derive_links.rs b/crates/formality-core/src/derive_links.rs index d56e9ae1e..b6cacb756 100644 --- a/crates/formality-core/src/derive_links.rs +++ b/crates/formality-core/src/derive_links.rs @@ -5,7 +5,6 @@ pub use crate::cast::DowncastTo; pub use crate::cast::UpcastFrom; -pub use crate::fixed_point; pub use crate::fold::Fold; pub use crate::fold::SubstitutionFn; pub use crate::parse; diff --git a/crates/formality-core/src/fixed_point.rs b/crates/formality-core/src/fixed_point.rs deleted file mode 100644 index 2d64687ac..000000000 --- a/crates/formality-core/src/fixed_point.rs +++ /dev/null @@ -1,83 +0,0 @@ -use std::cell::RefCell; -use std::fmt::Debug; -use std::hash::Hash; -use std::thread::LocalKey; - -mod stack; -pub use stack::FixedPointStack; - -pub fn fixed_point( - tracing_span: impl Fn(&Input) -> tracing::Span, - storage: &'static LocalKey>>, - args: Input, - default_value: impl Fn(&Input) -> Output, - next_value: impl FnMut(Input) -> Output, -) -> Output -where - Input: Value, - Output: Value, -{ - stacker::maybe_grow(32 * 1024, 1024 * 1024, || { - FixedPoint { - tracing_span, - storage, - default_value, - next_value, - } - .apply(args) - }) -} - -struct FixedPoint -where - Input: Value, - Output: Value, -{ - tracing_span: TracingSpan, - storage: &'static LocalKey>>, - default_value: DefaultValue, - next_value: NextValue, -} - -pub trait Value: Clone + Eq + Debug + Hash + 'static {} -impl Value for T {} - -impl - FixedPoint -where - Input: Value, - Output: Value, - DefaultValue: Fn(&Input) -> Output, - NextValue: FnMut(Input) -> Output, - TracingSpan: Fn(&Input) -> tracing::Span, -{ - fn apply(&mut self, input: Input) -> Output { - if let Some(r) = self.with_stack(|stack| stack.search(&input)) { - tracing::debug!("recursive call to {:?}, yielding {:?}", input, r); - return r; - } - - self.with_stack(|stack| { - let default_value = (self.default_value)(&input); - stack.push(&input, default_value); - }); - - loop { - let span = (self.tracing_span)(&input); - let _guard = span.enter(); - let output = (self.next_value)(input.clone()); - tracing::debug!(?output); - if !self.with_stack(|stack| stack.update_output(&input, output)) { - break; - } else { - tracing::debug!("output is different from previous iteration, re-executing until fixed point is reached"); - } - } - - self.with_stack(|stack| stack.pop(&input)) - } - - fn with_stack(&self, f: impl FnOnce(&mut FixedPointStack) -> R) -> R { - self.storage.with(|v| f(&mut *v.borrow_mut())) - } -} diff --git a/crates/formality-core/src/fixed_point/stack.rs b/crates/formality-core/src/fixed_point/stack.rs deleted file mode 100644 index 906ebf8ea..000000000 --- a/crates/formality-core/src/fixed_point/stack.rs +++ /dev/null @@ -1,89 +0,0 @@ -use super::Value; - -pub struct FixedPointStack { - entries: Vec>, -} - -impl Default for FixedPointStack { - fn default() -> Self { - Self { - entries: Default::default(), - } - } -} - -struct StackEntry { - /// Input. - input: Input, - - /// Current output, updated during computation as we approach a fixed point. - output: Output, - - /// Initially false; set to true when the outputs of this rule - /// are observed while it is being evaluated. - has_dependents: bool, -} - -impl FixedPointStack -where - Input: Value, - Output: Value, -{ - /// Access the top frame on the stack, which should be for `input`. - fn top_frame(&mut self, input: &Input) -> &mut StackEntry { - let top = self.entries.last_mut().unwrap(); - assert_eq!(top.input, *input); - top - } - - /// Search backwards through the stack, looking for the given input. - /// - /// If it is found, return `Some` with the current outputs, and mark it - /// as needing fixed point iteration. - /// - /// If not, return `None`. - /// - /// The fixed-point mark is returned when the stack is [popped](`Self::pop`) and is used - /// as part of the fixed point algorithm. - pub fn search(&mut self, input: &Input) -> Option { - for entry in &mut self.entries { - if entry.input == *input { - entry.has_dependents = true; - return Some(entry.output.clone()); - } - } - - None - } - - /// Push an entry onto the stack, indicating it is currently being evaluated. - /// There must not already be an entry for `input`. - pub fn push(&mut self, input: &Input, output: Output) { - assert!(self.search(input).is_none()); - - self.entries.push(StackEntry { - input: input.clone(), - output, - has_dependents: false, - }); - } - - /// Add outputs to the top-most stack entry, which must be for `input`. - /// Returns true if another iteration is needed before reaching a fixed point. - pub fn update_output(&mut self, input: &Input, output: Output) -> bool { - let top = self.top_frame(input); - if top.output == output { - return false; - } - - top.output = output; - top.has_dependents - } - - /// Pops the top entry from the stack, returning the saved outputs. - pub fn pop(&mut self, input: &Input) -> Output { - let top = self.entries.pop().unwrap(); - assert_eq!(top.input, *input); - top.output - } -} diff --git a/crates/formality-core/src/judgment.rs b/crates/formality-core/src/judgment.rs index 8b8649a48..e6ca0716f 100644 --- a/crates/formality-core/src/judgment.rs +++ b/crates/formality-core/src/judgment.rs @@ -1,26 +1,31 @@ -use std::cell::RefCell; - -use crate::{fixed_point::FixedPointStack, Fallible, Map}; +use crate::Fallible; mod assertion; pub use assertion::JudgmentAssertion; pub mod coverage; +mod memo; + mod proven_set; pub use proven_set::{ insert_smallest_proof, member_of, CheckProven, EachProof, FailedJudgment, FailedRule, FailureLocation, FailureReason, LeafFailure, ProofTree, Proven, ProvenSet, RuleFailureCause, }; +mod runtime; +#[doc(hidden)] +pub use runtime::{execute_judgment, JudgmentCache}; + mod test_explicit_fail; mod test_fallible; mod test_filtered; +mod test_fixed_point; mod test_for_all; +mod test_memo; +mod test_panic; mod test_reachable; -pub type JudgmentStack = RefCell>>; - /// `judgment_fn!` allows construction of inference rules using a more logic-like notation. /// /// The macro input looks like so: @@ -132,9 +137,9 @@ macro_rules! judgment_fn { let mut failed_rules = $crate::set![]; let input = __JudgmentStruct($($input_name),*); - let output = $crate::fixed_point::fixed_point::< + let output = $crate::judgment::execute_judgment::< __JudgmentStruct, - $crate::Map<$output, $crate::judgment::ProofTree>, + $output, >( // Tracing span: |input| { @@ -145,10 +150,10 @@ macro_rules! judgment_fn { ) }, - // Stack: + // Per-judgment cache: { thread_local! { - static R: $crate::judgment::JudgmentStack<__JudgmentStruct, $output> = Default::default() + static R: $crate::judgment::JudgmentCache<__JudgmentStruct, $output> = Default::default() } &R }, @@ -156,10 +161,7 @@ macro_rules! judgment_fn { // Input: input.clone(), - // Default value: - |_| Default::default(), - - // Next value: + // Execute rules: |input: __JudgmentStruct| { let mut output: $crate::Map<$output, $crate::judgment::ProofTree> = $crate::Map::new(); @@ -333,6 +335,15 @@ macro_rules! push_rules { } }; + // Boolean literals also match an `ident` macro fragment. Handle all + // literals before the identity-pattern arm so `true` is treated as a + // refutable pattern instead of expanding to the invalid `let true = ...`. + (@match $conclusion_name:ident inputs($in0:ident $($inputs:tt)*) patterns($pat0:literal, $($pats:tt)*) args $args:tt) => { + if let Some($pat0) = &$crate::Downcast::downcast($in0) { + $crate::push_rules!(@match $conclusion_name inputs($($inputs)*) patterns($($pats)*) args $args); + } + }; + (@match $conclusion_name:ident inputs($in0:ident $($inputs:tt)*) patterns($pat0:ident, $($pats:tt)*) args $args:tt) => { { let $pat0 = $in0; diff --git a/crates/formality-core/src/judgment/memo.rs b/crates/formality-core/src/judgment/memo.rs new file mode 100644 index 000000000..3663d42d7 --- /dev/null +++ b/crates/formality-core/src/judgment/memo.rs @@ -0,0 +1,594 @@ +//! Root-scoped memoization for completed judgment evaluations. +//! +//! The judgment runtime computes recursive judgments by repeatedly executing +//! their rules until the set of proven output values reaches a fixed point. +//! During that process it distinguishes two kinds of reuse, checked in this +//! order by [`execute_judgment`](super::execute_judgment): +//! +//! 1. An *active recursive call* returns the current approximation from the +//! runtime's execution stack. That cycle-breaking cache lives in +//! [`runtime`](super::runtime), not in this module. +//! 2. An *iteration memo hit* reuses a nested judgment that already completed +//! while all enclosing fixed-point approximations were unchanged. +//! +//! ## Iteration lifetime +//! +//! Every fresh judgment evaluation calls [`IterationGuard::begin`], which +//! pushes an empty [`ErasedTables`] slot onto [`MemoContext::active_iterations`]. +//! Nested judgments accumulate their completed positive results in that slot. +//! If the judgment discovers new output values and must execute its rules +//! again, [`IterationGuard::invalidate`] replaces the slot with an empty table: +//! descendants completed under the old approximation are no longer reusable. +//! +//! Once the judgment reaches a fixed point, [`IterationGuard::complete`] pops +//! its slot. For a nested judgment, the valid descendant entries and the +//! judgment's own positive result are merged into the parent's slot. For a +//! top-level judgment, the slot is discarded. Memoized results therefore live +//! only for the duration of one top-level judgment call and cannot affect a +//! later call or test. +//! +//! [`IterationGuard`] also makes the stack unwind-safe. It remembers the stack +//! depth that it owns and truncates back to that depth if rule execution +//! panics before normal completion. +//! +//! ## What is cached +//! +//! Only positive results are cached. An empty [`ProofMap`] means that no value +//! was proven, but it does not contain the failure diagnostics needed to treat +//! that result as a reusable negative fact. +//! +//! A `judgment_fn!` expansion creates a distinct input type for each judgment. +//! [`ErasedTables`] uses that input type's [`TypeId`] as the judgment identity, +//! allowing one context to hold heterogeneous [`MemoTable`] values without +//! allowing judgments with otherwise identical signatures to collide. The +//! context is thread-local, matching the thread-local judgment execution +//! stacks and avoiding synchronization between independent evaluations. + +use std::{ + any::{Any, TypeId}, + cell::RefCell, + collections::HashMap, + fmt::Debug, + hash::Hash, +}; + +use crate::Map; + +use super::{insert_smallest_proof, ProofTree}; + +/// The proven values and their smallest known proof trees for one judgment input. +type ProofMap = Map; + +/// Common bounds required for values stored in a type-erased memo table. +/// +/// This private trait keeps the erased-table signatures readable; its blanket +/// implementation does not add behavior beyond the listed bounds. +trait MemoValue: Clone + Eq + Debug + Hash + 'static {} +impl MemoValue for T {} + +/// Whether iteration lookups are enabled. +/// +/// Production execution always uses [`MemoMode::Enabled`]. Tests temporarily +/// select [`MemoMode::Disabled`] to compute an uncached reference result. +#[derive(Clone, Copy, Debug, Default, Eq, PartialEq)] +enum MemoMode { + /// Bypass iteration memo lookups. + Disabled, + + /// Reuse valid entries completed during this top-level call. + #[default] + Enabled, +} + +/// All memoization state for the current thread. +/// +/// Keeping the iteration stack and test mode in one `RefCell` gives each lookup +/// or lifecycle transition one scoped mutable borrow. +#[derive(Default)] +struct MemoContext { + /// One provisional table set for every fresh judgment evaluation currently active. + active_iterations: Vec, + + /// Test-controlled switch for comparing memoized and uncached execution. + mode: MemoMode, +} + +thread_local! { + // Judgment evaluation itself is thread-local, so memo entries cannot be + // observed by another thread and require no synchronization. + static MEMO_CONTEXT: RefCell = RefCell::new(MemoContext::default()); +} + +/// Mutably access the current thread's memo context for one short operation. +/// +/// Callers must not recursively enter this helper from `op`, because the +/// `RefCell` remains mutably borrowed until `op` returns. +fn with_context(op: impl FnOnce(&mut MemoContext) -> R) -> R { + MEMO_CONTEXT.with(|context| op(&mut context.borrow_mut())) +} + +/// Look up a positive result completed in the current chain of valid iterations. +/// +/// The search proceeds from the innermost active iteration to the outermost. +/// This favors the entry established in the most local evaluation while still +/// allowing a nested call to reuse work already completed by an ancestor. At a +/// given depth, entries remain valid until that depth is invalidated; completing +/// the guard may transfer them into its still-valid parent. +/// +/// Returns `None` when memoization is disabled, when no matching entry exists, +/// or when the matching judgment previously failed (failures are not cached). +pub(crate) fn lookup_iteration(input: &Input) -> Option> +where + Input: Clone + Eq + Debug + Hash + 'static, + Output: Clone + Eq + Debug + Hash + Ord + 'static, +{ + with_context(|context| { + if context.mode == MemoMode::Disabled { + return None; + } + + context + .active_iterations + .iter() + .rev() + .find_map(|entries| entries.get::(input)) + .cloned() + }) +} + +/// Return the number of provisional iteration-table sets currently on the stack. +/// +/// Panic-safety tests use this to verify that [`IterationGuard::drop`] removed +/// every table owned by an unwound judgment evaluation. +#[cfg(test)] +pub(crate) fn active_iteration_count() -> usize { + with_context(|context| context.active_iterations.len()) +} + +/// Test-only scope that selects memoized or uncached execution for this thread. +/// +/// The mode may change only between top-level judgment calls, when there are no +/// memo tables to preserve or discard. +#[cfg(test)] +pub(crate) struct TestModeGuard { + previous: MemoMode, +} + +#[cfg(test)] +impl TestModeGuard { + /// Select whether completed results may be reused during the next root call. + pub(crate) fn new(enabled: bool) -> Self { + let previous = with_context(|context| { + assert!( + context.active_iterations.is_empty(), + "cannot change memo mode during judgment evaluation", + ); + std::mem::replace( + &mut context.mode, + if enabled { + MemoMode::Enabled + } else { + MemoMode::Disabled + }, + ) + }); + Self { previous } + } +} + +#[cfg(test)] +impl Drop for TestModeGuard { + /// Restore the mode that was active before this test scope. + fn drop(&mut self) { + with_context(|context| { + assert!( + context.active_iterations.is_empty(), + "memo mode scope ended during judgment evaluation", + ); + context.mode = self.previous; + }); + } +} + +/// Owns the provisional memo-table slot for one fresh judgment evaluation. +/// +/// `depth` is both the stack length observed by [`IterationGuard::begin`] and +/// the index of this guard's [`ErasedTables`] slot after it is pushed. It lets +/// every lifecycle operation assert that guards complete in stack order and +/// lets unwinding truncate all state created at or below this evaluation. +/// `active` distinguishes a normally completed guard, whose slot was already +/// popped, from one that must clean up during `Drop`. +pub(crate) struct IterationGuard { + /// Stack length before this guard pushed its slot, and therefore that slot's index. + depth: usize, + + /// Whether `Drop` still owns cleanup of this guard's slot and descendants. + active: bool, +} + +impl IterationGuard { + /// Begin a fresh judgment evaluation with an empty provisional table set. + /// + /// The returned guard must be completed after the fixed-point loop succeeds. + /// If it is dropped first, it treats the evaluation as unwound and removes + /// everything pushed since this call. + pub(crate) fn begin() -> Self { + let depth = with_context(|context| { + let depth = context.active_iterations.len(); + context.active_iterations.push(ErasedTables::default()); + depth + }); + Self { + depth, + active: true, + } + } + + /// Assert that this guard owns the topmost, still-empty iteration table. + /// + /// The runtime checks this at the start of every rule pass. [`Self::begin`] + /// establishes the invariant for the first pass, and [`Self::invalidate`] + /// restores it before each repeated pass. The table may then accumulate only + /// completed descendant executions while that pass evaluates its rules. + pub(crate) fn assert_is_top_and_empty(&self) { + with_context(|context| { + assert_eq!( + context.active_iterations.len(), + self.depth + 1, + "current judgment does not own the top memo iteration", + ); + assert!( + context.active_iterations[self.depth].is_empty(), + "current judgment's memo iteration is not empty before a rule pass", + ); + }); + } + + /// Discard entries completed under an obsolete fixed-point approximation. + /// + /// The runtime calls this whenever the judgment gains proven output values + /// and has recursive dependents, just before executing its rules again. The + /// stack slot itself remains in place so subsequent descendants can repopulate + /// it under the new approximation. + pub(crate) fn invalidate(&self) { + with_context(|context| { + assert_eq!(context.active_iterations.len(), self.depth + 1); + context.active_iterations[self.depth] = ErasedTables::default(); + }); + } + + /// Finish this judgment and transfer all results computed in its valid iteration. + /// + /// The guard's own table contains completed descendants but not the judgment + /// represented by `input`; that result is supplied separately as `output`. + /// If a parent iteration exists, both are merged into its provisional table + /// for possible reuse by later nested calls. Otherwise this was a top-level + /// evaluation, so `completed_descendants` is dropped and no memoized result + /// survives the call. Empty outputs are ignored by [`ErasedTables::insert`]. + pub(crate) fn complete(mut self, input: &Input, output: &ProofMap) + where + Input: Clone + Eq + Debug + Hash + 'static, + Output: Clone + Eq + Debug + Hash + Ord + 'static, + { + let completed_descendants = with_context(|context| { + assert_eq!(context.active_iterations.len(), self.depth + 1); + context.active_iterations.pop().unwrap() + }); + self.active = false; + + with_context(|context| { + if let Some(parent) = context.active_iterations.last_mut() { + parent.merge(completed_descendants); + parent.insert(input.clone(), output.clone()); + } + }); + } +} + +impl Drop for IterationGuard { + /// Remove provisional tables when evaluation exits without calling `complete`. + /// + /// Truncation, rather than a single pop, also removes any descendant state + /// that remains if a panic interrupts nested judgment execution. + fn drop(&mut self) { + if self.active { + with_context(|context| { + assert!(context.active_iterations.len() > self.depth); + context.active_iterations.truncate(self.depth); + }); + } + } +} + +/// A heterogeneous collection containing at most one memo table per judgment. +/// +/// Each `judgment_fn!` expansion creates a unique input type, so its [`TypeId`] +/// identifies the judgment even when another judgment has the same Rust input +/// and output shapes. Values are boxed behind [`ErasedMemoTable`] so a single +/// iteration can contain every judgment encountered by the current root call. +#[derive(Default)] +struct ErasedTables { + /// Concrete [`MemoTable`] values indexed by their generated judgment input type. + by_judgment: HashMap>, +} + +impl ErasedTables { + /// Find the completed positive result for one judgment input. + /// + /// The input type selects the concrete table and the input value selects an + /// entry within it. A table's output type is fixed by its judgment; a failed + /// downcast therefore indicates an internal identity/type mismatch rather + /// than a normal cache miss. + fn get(&self, input: &Input) -> Option<&ProofMap> + where + Input: MemoValue, + Output: MemoValue + Ord, + { + self.by_judgment + .get(&TypeId::of::())? + .as_any() + .downcast_ref::>() + .expect("judgment identity mapped to an unexpected memo-table type") + .entries + .get(input) + } + + /// Insert or merge a completed positive judgment result. + /// + /// Empty proof maps are deliberately excluded because their failure diagnostics are not + /// represented in the map. Treating them as cached negative facts would be unsound. + /// Returns `true` when a positive entry was inserted or merged and `false` + /// when `output` was empty and therefore ignored. + fn insert(&mut self, input: Input, output: ProofMap) -> bool + where + Input: MemoValue, + Output: MemoValue + Ord, + { + if output.is_empty() { + return false; + } + + let identity = TypeId::of::(); + let table = self + .by_judgment + .entry(identity) + .or_insert_with(|| Box::new(MemoTable::::default())); + table + .as_any_mut() + .downcast_mut::>() + .expect("judgment identity mapped to an unexpected memo-table type") + .insert(input, output); + true + } + + /// Transfer every judgment table and entry from `other` into this collection. + /// + /// This is used to bubble a completed descendant set into its parent + /// iteration. + /// Colliding entries are delegated to [`ErasedMemoTable::merge`], which + /// verifies that their proven values agree and combines proof metadata. + fn merge(&mut self, other: ErasedTables) { + for (identity, other_table) in other.by_judgment { + match self.by_judgment.get_mut(&identity) { + Some(table) => table.merge(other_table), + None => { + self.by_judgment.insert(identity, other_table); + } + } + } + } + + /// Report whether this collection contains no concrete tables. + /// + /// Because empty outputs are never inserted, this also means it contains no + /// cached positive entries. + fn is_empty(&self) -> bool { + self.by_judgment.is_empty() + } +} + +/// Object-safe operations needed to store and merge differently typed memo tables. +/// +/// The `Any` accessors recover a concrete [`MemoTable`] after its generated +/// input [`TypeId`] selects the appropriate trait object. `merge` is exposed +/// through the trait because [`ErasedTables`] must perform that operation +/// without knowing the table's type parameters. +trait ErasedMemoTable: Any { + /// Borrow this table as `Any` for a checked shared downcast. + fn as_any(&self) -> &dyn Any; + + /// Borrow this table as `Any` for a checked mutable downcast. + fn as_any_mut(&mut self) -> &mut dyn Any; + + /// Convert an owned erased table into `Any` for an owned downcast. + fn into_any(self: Box) -> Box; + + /// Merge another table selected by the same judgment identity into this one. + fn merge(&mut self, other: Box); +} + +/// Completed positive results for one concrete judgment. +/// +/// `Input` is the unique generated judgment input type as well as the per-entry +/// key. `Output` is the judgment's proven-value type. Each input maps to all +/// proven outputs and the smallest proof tree retained for each output. +struct MemoTable { + /// Positive results indexed by the complete judgment input value. + entries: HashMap>, +} + +impl Default for MemoTable { + /// Create an empty concrete judgment table. + fn default() -> Self { + Self { + entries: HashMap::new(), + } + } +} + +impl MemoTable +where + Input: MemoValue, + Output: MemoValue + Ord, +{ + /// Insert one result, merging proof metadata if the input already exists. + /// + /// Two valid completions of the same judgment input must prove exactly the + /// same output values. [`merge_equivalent_outputs`] asserts that invariant + /// and retains the smaller proof tree for each value. + fn insert(&mut self, input: Input, output: ProofMap) { + match self.entries.entry(input) { + std::collections::hash_map::Entry::Occupied(mut entry) => { + merge_equivalent_outputs(entry.get_mut(), output); + } + std::collections::hash_map::Entry::Vacant(entry) => { + entry.insert(output); + } + } + } +} + +impl ErasedMemoTable for MemoTable +where + Input: MemoValue, + Output: MemoValue + Ord, +{ + /// Expose this concrete table for shared type recovery by [`ErasedTables::get`]. + fn as_any(&self) -> &dyn Any { + self + } + + /// Expose this concrete table for mutable type recovery by [`ErasedTables::insert`]. + fn as_any_mut(&mut self) -> &mut dyn Any { + self + } + + /// Expose this owned table so `merge` can recover its concrete entry map. + fn into_any(self: Box) -> Box { + self + } + + /// Merge all entries from another table with the same generated identity. + /// + /// The enclosing [`ErasedTables`] map matched these objects by input + /// [`TypeId`], so a downcast failure indicates an internal invariant breach. + fn merge(&mut self, other: Box) { + let other = other + .into_any() + .downcast::() + .expect("cannot merge memo tables with different concrete types"); + for (input, output) in other.entries { + self.insert(input, output); + } + } +} + +/// Merge two valid completions of the same judgment input. +/// +/// Memoization must not change the semantic set of proven values, so colliding +/// entries are required to have identical ordered keys. Proof trees are metadata +/// and may differ; for each value, this retains the smallest proof observed. +fn merge_equivalent_outputs( + current: &mut ProofMap, + next: ProofMap, +) { + assert!( + current.keys().eq(next.keys()), + "equivalent memo entries have different proven values", + ); + + for (value, proof) in next { + insert_smallest_proof(current, value, proof); + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[derive(Clone, Debug, Eq, Hash, PartialEq)] + struct InputA(u32); + + #[derive(Clone, Debug, Eq, Hash, PartialEq)] + struct InputB(u32); + + fn small_proof() -> ProofTree { + ProofTree::leaf("small") + } + + fn large_proof() -> ProofTree { + ProofTree::new("large", None, vec![ProofTree::leaf("child")]) + } + + #[test] + fn typed_table_round_trip_and_empty_exclusion() { + let mut tables = ErasedTables::default(); + + assert!(!tables.insert::(InputA(0), Map::new())); + assert!(tables.is_empty()); + + let output = Map::from([(22_u32, small_proof())]); + assert!(tables.insert(InputA(0), output.clone())); + assert_eq!(tables.get::(&InputA(0)), Some(&output)); + } + + #[test] + fn generated_input_type_isolates_judgment_identity() { + let mut tables = ErasedTables::default(); + + tables.insert(InputA(0), Map::from([(22_u32, small_proof())])); + tables.insert(InputB(0), Map::from([(44_u32, small_proof())])); + + assert!(tables + .get::(&InputA(0)) + .is_some_and(|output| output.contains_key(&22))); + assert!(tables + .get::(&InputB(0)) + .is_some_and(|output| output.contains_key(&44))); + } + + #[test] + fn table_merge_retains_the_smallest_proof() { + let mut left = ErasedTables::default(); + left.insert(InputA(0), Map::from([(22_u32, large_proof())])); + + let mut right = ErasedTables::default(); + let small = small_proof(); + right.insert(InputA(0), Map::from([(22_u32, small.clone())])); + + left.merge(right); + + assert_eq!( + left.get::(&InputA(0)) + .and_then(|output| output.get(&22)), + Some(&small), + ); + } + + #[test] + #[should_panic(expected = "equivalent memo entries have different proven values")] + fn table_merge_rejects_semantically_unequal_collision() { + let mut left = ErasedTables::default(); + left.insert(InputA(0), Map::from([(22_u32, small_proof())])); + + let mut right = ErasedTables::default(); + right.insert(InputA(0), Map::from([(44_u32, small_proof())])); + + left.merge(right); + } + + #[test] + fn completing_a_root_discards_all_memoized_entries() { + let _mode = TestModeGuard::new(true); + let root = IterationGuard::begin(); + let child = IterationGuard::begin(); + let child_output = Map::from([(22_u32, small_proof())]); + + child.complete(&InputA(0), &child_output); + assert_eq!(lookup_iteration(&InputA(0)), Some(child_output)); + + root.complete(&InputB(0), &Map::from([(44_u32, small_proof())])); + assert_eq!(active_iteration_count(), 0); + assert_eq!(lookup_iteration::(&InputA(0)), None); + } +} diff --git a/crates/formality-core/src/judgment/runtime.rs b/crates/formality-core/src/judgment/runtime.rs new file mode 100644 index 000000000..9de63345c --- /dev/null +++ b/crates/formality-core/src/judgment/runtime.rs @@ -0,0 +1,469 @@ +//! Fixed-point execution for judgments generated by [`judgment_fn!`](crate::judgment_fn). +//! +//! A generated judgment function packages its arguments into a unique input +//! type and supplies this module with four things: +//! +//! * a tracing-span constructor; +//! * a thread-local [`JudgmentCache`] dedicated to that judgment; +//! * the input value for this call; and +//! * an `execute_rules` closure that evaluates every applicable rule once and +//! returns the values proven in that pass. +//! +//! [`execute_judgment`] turns those single-pass rule evaluations into a +//! recursive least-fixed-point computation. +//! +//! ## Active recursion and convergence +//! +//! Each fresh call pushes a [`StackEntry`] containing an initially empty output +//! approximation. If evaluating its rules recursively requests the same +//! judgment input, [`ExecutionStack::search`] returns that current approximation +//! instead of recursing forever and marks the entry as having dependents. +//! +//! After a rule pass, [`ExecutionStack::update`] merges the newly proven values +//! into the approximation. Judgment outputs must grow monotonically: a later +//! pass may add proven values but may not remove one. Another pass is needed +//! only when the value set grew *and* a recursive dependent observed an earlier +//! approximation. Otherwise the current output is final. +//! +//! Different proof trees for the same proven value do not affect convergence. +//! Proofs are metadata, and [`merge_proven_outputs`] retains the smallest proof +//! observed for each value. +//! +//! ## Completed-result memoization +//! +//! The active execution stack is separate from [`memo`]. The stack stores +//! incomplete approximations used to break recursive cycles; the memo layer +//! stores only completed positive results. Each call therefore checks, in order: +//! +//! 1. the active stack for a recursive cycle; +//! 2. completed results from a still-valid enclosing iteration. +//! +//! A call that misses both paths opens an active stack entry and a +//! [`memo::IterationGuard`]. If its approximation grows, completed descendant +//! memo entries from the obsolete pass are invalidated before rules execute +//! again. At convergence, the final output and valid descendants move into the +//! parent iteration. Completing the top-level judgment discards its table, so +//! no memoized result survives between independent calls. See the [`memo`] +//! module for that lifecycle in detail. +//! +//! ## Cleanup and failures +//! +//! [`ActiveJudgmentGuard`] removes active stack state during unwinding, while +//! [`memo::IterationGuard`] removes provisional memo state. This prevents a +//! panic in a rule body from making later calls appear recursive or memoized. +//! +//! This module returns only proven values and proof trees. The generated +//! judgment function separately accumulates failure diagnostics for a pass and +//! uses them if the final [`ProofMap`] is empty. Empty results are not memoized, +//! because the proof map does not contain enough information to reconstruct +//! those diagnostics. + +use std::{cell::RefCell, fmt::Debug, hash::Hash, thread::LocalKey}; + +use crate::Map; + +use super::{insert_smallest_proof, memo, ProofTree}; + +/// The current proven values and smallest known proof for each value. +type ProofMap = Map; + +/// Per-judgment thread-local state generated by [`judgment_fn!`](crate::judgment_fn). +/// +/// One cache exists for each generated judgment, so `Input` and `Output` are +/// concrete and do not require the type erasure used by the shared memo layer. +/// The `RefCell` permits nested calls on the same thread to inspect and update +/// active approximations dynamically. +/// +/// This type is public only because exported macro expansions must be able to name it. +#[doc(hidden)] +pub struct JudgmentCache { + /// Active calls to this judgment, ordered by recursive call depth. + active: RefCell>>, +} + +impl Default for JudgmentCache { + /// Create a per-judgment cache with no active evaluations. + fn default() -> Self { + Self { + active: RefCell::new(ExecutionStack::default()), + } + } +} + +/// Execute one judgment's rules until its proven output values reach a fixed point. +/// +/// `tracing_span` creates the span used for each rule pass. `cache` is the +/// thread-local active stack generated for this particular judgment. `input` +/// identifies the call, and `execute_rules` performs one complete rule pass for +/// that input. +/// +/// Reentrant calls with the same input receive the approximation accumulated so +/// far. A fresh call returns only after its semantic output stops changing, and +/// the returned map contains the smallest proof observed for each proven value. +/// +/// This function is public only because exported macro expansions must be able to call it. +#[doc(hidden)] +pub fn execute_judgment( + tracing_span: impl Fn(&Input) -> tracing::Span, + cache: &'static LocalKey>, + input: Input, + mut execute_rules: impl FnMut(Input) -> ProofMap, +) -> ProofMap +where + Input: Clone + Eq + Debug + Hash + 'static, + Output: Clone + Eq + Debug + Hash + Ord + 'static, +{ + // Recursive judgment chains can exceed the native stack even when they are + // converging normally. Move this evaluation to a larger stack segment when + // the remaining stack drops below `stacker`'s requested red zone. + stacker::maybe_grow(32 * 1024, 1024 * 1024, || { + // Recursive cycle: this exact judgment input is already being evaluated. + // Return its current approximation to break the cycle. `search` also marks + // the active entry as having a dependent, so newly proven values will make + // the enclosing fixed-point loop run again. + if let Some(output) = cache.with(|cache| cache.active.borrow_mut().search(&input)) { + tracing::debug!("recursive call to {:?}, yielding {:?}", input, output); + return output; + } + + // Completed in this fixed-point iteration: a nested call already proved a + // positive result for this input, and no enclosing approximation has grown + // since then. Reuse it until an iteration invalidation clears the table. + if let Some(output) = memo::lookup_iteration(&input) { + tracing::debug!( + "iteration-memoized call to {:?}, yielding {:?}", + input, + output + ); + return output; + } + + // Execute the rules to compute the value. If executing the rules required recursively + // reading the result of the current rule, then execute until a fixed-point is reached. + // Otherwise (no recursion) just compute a single iteration. + // + // The result will be cached in the memo-table for this iteration and then added into + // the parent's table. Whenever this judgment (or a parent) must run a second iteration, + // it clears the intermediate cached results since they may change because recursive + // calls will yield a new value. + cache.with(|cache| cache.active.borrow_mut().push(&input, Map::new())); + let active_guard = ActiveJudgmentGuard::new(cache, &input); + let iteration_guard = memo::IterationGuard::begin(); + loop { + // The current judgment's provisional memo table is topmost here and + // contains no completed descendants yet. `begin` creates it empty for + // the first pass; `invalidate` clears it before every repeated pass. + // The current judgment's own approximation lives in `active_guard`'s + // execution-stack entry, not in this memo table. + iteration_guard.assert_is_top_and_empty(); + + // Run the user's judgment rules and then trace the output. + let span = tracing_span(&input); + let _guard = span.enter(); + let output = execute_rules(input.clone()); + tracing::debug!(?output); + + // Merge this round's proven values into the active approximation. + // `update` requests another round only when the value set grew and + // a recursive call consumed an earlier approximation. If no such + // dependent exists, the newly computed result is already final. + let repeat = cache.with(|cache| cache.active.borrow_mut().update(&input, output)); + if !repeat { + break; + } + + tracing::debug!("proven values changed, re-executing until a fixed point is reached"); + + // Descendants completed in this round may have depended on the old + // approximation. Clear them before evaluating the rules again so + // they cannot be reused as though they were valid at the new point. + iteration_guard.invalidate(); + } + + // Remove and return the final approximation, then transfer the positive + // entries completed in its last valid iteration into the parent memo + // scope. If this was the top-level judgment, completing its iteration + // instead discards the table so no cache survives the call. + let output = active_guard.pop(); + iteration_guard.complete(&input, &output); + output + }) +} + +/// Common bounds for values stored in a generated judgment's active stack. +/// +/// This private trait is a readability alias; its blanket implementation adds +/// no behavior beyond the listed bounds. +trait RuntimeValue: Clone + Eq + Debug + Hash + 'static {} +impl RuntimeValue for T {} + +/// Owns cleanup of one active [`ExecutionStack`] entry. +/// +/// A fresh evaluation pushes the entry before creating this guard. Normal +/// completion consumes the guard through [`ActiveJudgmentGuard::pop`] and +/// returns the final approximation. If rule evaluation unwinds first, `Drop` +/// removes the entry and discards its incomplete output. +struct ActiveJudgmentGuard +where + Input: RuntimeValue, + Output: RuntimeValue + Ord, +{ + /// The generated judgment's thread-local active stack. + cache: &'static LocalKey>, + + /// The exact input used to verify that this guard pops the correct stack entry. + input: Input, + + /// Whether `Drop` still owns cleanup because normal completion has not popped the entry. + active: bool, +} + +impl ActiveJudgmentGuard +where + Input: RuntimeValue, + Output: RuntimeValue + Ord, +{ + /// Begin guarding the active entry that the caller just pushed for `input`. + fn new(cache: &'static LocalKey>, input: &Input) -> Self { + Self { + cache, + input: input.clone(), + active: true, + } + } + + /// Pop this evaluation normally and return its final output approximation. + /// + /// Marking the guard inactive first prevents its subsequent `Drop` from + /// trying to remove the same entry a second time. + fn pop(mut self) -> ProofMap { + self.active = false; + self.cache + .with(|cache| cache.active.borrow_mut().pop(&self.input)) + } +} + +impl Drop for ActiveJudgmentGuard +where + Input: RuntimeValue, + Output: RuntimeValue + Ord, +{ + /// Remove and discard an incomplete active entry during unwinding. + fn drop(&mut self) { + if self.active { + self.cache + .with(|cache| cache.active.borrow_mut().pop(&self.input)); + } + } +} + +/// Active evaluations of one generated judgment on the current thread. +/// +/// Entries are ordered from the oldest call to the currently executing call. +/// Different inputs may be active simultaneously through recursion, but a +/// repeated input is handled by [`ExecutionStack::search`] and is never pushed +/// twice. This makes the vector both a recursion-detection set and a call stack. +struct ExecutionStack { + /// Active calls and the approximations each recursive caller may observe. + entries: Vec>, +} + +impl Default for ExecutionStack { + /// Create an execution stack with no active judgment calls. + fn default() -> Self { + Self { + entries: Vec::new(), + } + } +} + +/// Runtime state for one active judgment input. +/// +/// `output` is the monotonically growing approximation returned to recursive +/// calls. `has_dependents` records whether any such call has observed it; only +/// then can growth require another rule pass. +struct StackEntry { + /// The complete generated judgment input identifying this active call. + input: Input, + + /// The current output approximation, initially empty for a fresh evaluation. + output: Output, + + /// Whether a recursive call has consumed this entry's approximation. + has_dependents: bool, +} + +impl ExecutionStack +where + Input: RuntimeValue, + Output: RuntimeValue, +{ + /// Detect an active call with the same input and return its approximation. + /// + /// A match is a recursive dependency, so this also sets `has_dependents` on + /// the owning entry. If that approximation later grows, its fixed-point loop + /// must execute the rules again for the dependent to observe the new values. + fn search(&mut self, input: &Input) -> Option { + for entry in &mut self.entries { + if entry.input == *input { + entry.has_dependents = true; + return Some(entry.output.clone()); + } + } + + None + } + + /// Push a fresh active input and its initial output approximation. + /// + /// The uniqueness assertion enforces that repeated inputs take the recursive + /// `search` path instead of creating a second fixed-point computation. + fn push(&mut self, input: &Input, output: Output) { + assert!( + self.entries.iter().all(|entry| entry.input != *input), + "judgment is already active" + ); + self.entries.push(StackEntry { + input: input.clone(), + output, + has_dependents: false, + }); + } + + /// Pop the most recent active call and return its approximation. + /// + /// Judgment evaluations are nested, so normal completion and unwinding must + /// be last-in, first-out. The input assertion catches mismatched guards. + fn pop(&mut self, input: &Input) -> Output { + let top = self.entries.pop().expect("no active judgment to pop"); + assert_eq!(top.input, *input); + top.output + } + + /// Borrow the currently executing entry after verifying its input. + /// + /// Rule-pass results can update only the top entry for this judgment; any + /// older entry is suspended beneath the current recursive call. + fn top(&mut self, input: &Input) -> &mut StackEntry { + let top = self.entries.last_mut().expect("no active judgment"); + assert_eq!(top.input, *input); + top + } +} + +impl ExecutionStack> +where + Input: RuntimeValue, + Output: RuntimeValue + Ord, +{ + /// Merge one rule pass into the active approximation and decide whether to repeat. + /// + /// Semantic growth matters only if a recursive dependent previously consumed + /// the old approximation. Without a dependent, the complete rule pass has + /// already computed the final output and no observer needs to be revisited. + fn update(&mut self, input: &Input, output: ProofMap) -> bool { + let top = self.top(input); + merge_proven_outputs(&mut top.output, output) && top.has_dependents + } +} + +/// Merge a new judgment result into its current approximation. +/// +/// Positive judgment outputs must grow monotonically, so every key in `current` +/// must also occur in `next`. Given that subset invariant, a length change means +/// that the pass proved at least one new value. Proof-only changes do not count +/// as semantic growth, but the smallest proof observed for each value is retained. +/// +/// Returns `true` exactly when the set of proven values grew. +fn merge_proven_outputs( + current: &mut ProofMap, + mut next: ProofMap, +) -> bool { + assert!( + current.keys().all(|value| next.contains_key(value)), + "judgment fixed-point output lost a previously proven value", + ); + + let values_changed = current.len() != next.len(); + for (value, proof) in std::mem::take(current) { + insert_smallest_proof(&mut next, value, proof); + } + *current = next; + values_changed +} + +#[cfg(test)] +mod tests { + use std::cell::Cell; + + use super::*; + + thread_local! { + static CACHE: JudgmentCache<(), u32> = JudgmentCache::default(); + static ITERATIONS: Cell = const { Cell::new(0) }; + } + + fn growing_proof() -> ProofMap { + execute_judgment( + |_| tracing::Span::none(), + &CACHE, + (), + |_| { + let iteration = ITERATIONS.get() + 1; + ITERATIONS.set(iteration); + assert!( + iteration <= 8, + "proof metadata forced unbounded judgment iteration" + ); + + let previous = growing_proof(); + let proof = match previous.get(&0) { + Some(proof) => ProofTree::new("recursive", None, vec![proof.clone()]), + None => ProofTree::leaf("base"), + }; + Map::from([(0, proof)]) + }, + ) + } + + fn large_proof() -> ProofTree { + ProofTree::new("large", None, vec![ProofTree::leaf("child")]) + } + + #[test] + fn proof_metadata_does_not_force_iteration_and_smallest_proof_wins() { + ITERATIONS.set(0); + + let output = growing_proof(); + + assert_eq!(ITERATIONS.get(), 2); + assert_eq!(output[&0].total_nodes(), 1); + } + + #[test] + fn merge_reports_only_new_values_and_keeps_the_smallest_proof() { + let small = ProofTree::leaf("small"); + let mut current = Map::from([(0, small.clone())]); + + assert!(!merge_proven_outputs( + &mut current, + Map::from([(0, large_proof())]), + )); + assert_eq!(current, Map::from([(0, small.clone())])); + + assert!(merge_proven_outputs( + &mut current, + Map::from([(0, large_proof()), (1, ProofTree::leaf("one"))]), + )); + assert_eq!(current.get(&0), Some(&small)); + assert!(current.contains_key(&1)); + } + + #[test] + #[should_panic(expected = "lost a previously proven value")] + fn merge_rejects_non_monotonic_outputs() { + let mut current = Map::from([(0, ProofTree::leaf("zero"))]); + + merge_proven_outputs(&mut current, Map::new()); + } +} diff --git a/crates/formality-core/src/judgment/test_fixed_point.rs b/crates/formality-core/src/judgment/test_fixed_point.rs new file mode 100644 index 000000000..14d4d5f95 --- /dev/null +++ b/crates/formality-core/src/judgment/test_fixed_point.rs @@ -0,0 +1,38 @@ +#![cfg(test)] + +use std::cell::Cell; + +use crate::judgment_fn; + +thread_local! { + static EXECUTIONS: Cell = const { Cell::new(0) }; +} + +judgment_fn! { + fn proof_metadata_cycle() => u32 { + debug() + + ( + (let () = EXECUTIONS.set(EXECUTIONS.get() + 1)) + --- ("base") + (proof_metadata_cycle() => 0) + ) + + ( + (proof_metadata_cycle() => value) + --- ("recursive") + (proof_metadata_cycle() => value) + ) + } +} + +#[test] +fn cyclic_judgment_converges_by_value_and_retains_its_base_proof() { + EXECUTIONS.set(0); + + let (value, proof) = proof_metadata_cycle().into_singleton().unwrap(); + + assert_eq!(value, 0); + assert_eq!(EXECUTIONS.get(), 2); + assert_eq!(proof.rule_name, Some("base")); +} diff --git a/crates/formality-core/src/judgment/test_memo/iteration.rs b/crates/formality-core/src/judgment/test_memo/iteration.rs new file mode 100644 index 000000000..b657a7784 --- /dev/null +++ b/crates/formality-core/src/judgment/test_memo/iteration.rs @@ -0,0 +1,135 @@ +//! Iteration-local memoization tests. +//! +//! Completed child judgments may be reused while an enclosing fixed-point +//! approximation is unchanged. Nested completed tables flow up to their parent +//! iteration, but all such entries become invalid as soon as an outer result +//! grows. Only positive results participate, and the generated judgment type +//!—not merely its input/output signature—identifies a memo table. + +use std::cell::Cell; + +use crate::judgment_fn; + +use super::*; + +thread_local! { + static REUSED_CHILD_EXECUTIONS: Cell = const { Cell::new(0) }; + static GRANDCHILD_EXECUTIONS: Cell = const { Cell::new(0) }; +} + +judgment_fn! { + fn propagated_grandchild() => u32 { + debug() + + ( + (let () = GRANDCHILD_EXECUTIONS.set( + GRANDCHILD_EXECUTIONS.get() + 1, + )) + --- ("value") + (propagated_grandchild() => 22) + ) + } +} + +judgment_fn! { + fn propagated_child() => u32 { + debug() + + ( + (propagated_grandchild() => value) + --- ("grandchild") + (propagated_child() => value) + ) + } +} + +judgment_fn! { + fn calls_child_then_grandchild() => u32 { + debug() + + ( + (propagated_child() => child_value) + (propagated_grandchild() => direct_value) + (if child_value == direct_value) + --- ("both") + (calls_child_then_grandchild() => child_value) + ) + } +} + +judgment_fn! { + fn reused_child(value: u32) => u32 { + debug(value) + + ( + (let () = REUSED_CHILD_EXECUTIONS.set( + REUSED_CHILD_EXECUTIONS.get() + 1, + )) + --- ("value") + (reused_child(value) => value) + ) + } +} + +judgment_fn! { + fn calls_reused_child_twice(value: u32) => u32 { + debug(value) + + ( + (reused_child(value) => result) + (reused_child(value) => _) + --- ("twice") + (calls_reused_child_twice(value) => result) + ) + } +} + +#[test] +fn reuses_a_completed_child_in_one_iteration() { + REUSED_CHILD_EXECUTIONS.set(0); + + assert_eq!(values(calls_reused_child_twice(22)), crate::set![22]); + assert_eq!(REUSED_CHILD_EXECUTIONS.get(), 1); +} + +#[test] +fn propagates_completed_grandchildren_to_the_parent_iteration() { + GRANDCHILD_EXECUTIONS.set(0); + + assert_eq!(values(calls_child_then_grandchild()), crate::set![22]); + assert_eq!(GRANDCHILD_EXECUTIONS.get(), 1); +} + +#[test] +fn invalidates_completed_children_when_outer_approximation_grows() { + INVALIDATED_CHILD_EXECUTIONS.set(0); + + assert_eq!(values(invalidation_a()), crate::set![0, 1, 2]); + assert_eq!(INVALIDATED_CHILD_EXECUTIONS.get(), 3); +} + +#[test] +fn shares_iteration_context_across_cyclic_judgment_output_types() { + CROSS_TYPE_EXECUTIONS.set(0); + + assert_eq!(values(cross_type_a()), crate::set![0, 1]); + assert_eq!(CROSS_TYPE_EXECUTIONS.get(), 3); +} + +#[test] +fn generated_identity_separates_same_signature_judgments() { + IDENTITY_LEFT_EXECUTIONS.set(0); + IDENTITY_RIGHT_EXECUTIONS.set(0); + + assert_eq!(values(calls_same_signature_judgments(21)), crate::set![45]); + assert_eq!(IDENTITY_LEFT_EXECUTIONS.get(), 1); + assert_eq!(IDENTITY_RIGHT_EXECUTIONS.get(), 1); +} + +#[test] +fn does_not_cache_failed_children_as_negative_facts() { + FAILED_CHILD_EXECUTIONS.set(0); + + assert!(calls_failed_child_twice().is_proven()); + assert_eq!(FAILED_CHILD_EXECUTIONS.get(), 2); +} diff --git a/crates/formality-core/src/judgment/test_memo/mod.rs b/crates/formality-core/src/judgment/test_memo/mod.rs new file mode 100644 index 000000000..91874ef43 --- /dev/null +++ b/crates/formality-core/src/judgment/test_memo/mod.rs @@ -0,0 +1,208 @@ +//! Tests for judgment-result memoization. +//! +//! Memoized entries live only within one top-level judgment call: +//! +//! * `iteration` tests entries reused only within the current fixed-point +//! iteration. These entries must be discarded whenever an enclosing +//! approximation grows. +//! * `root_scope` tests that returning from the top-level judgment discards +//! both its own table and all completed descendant entries. +//! * `soundness` compares memoized execution with uncached execution across +//! cyclic graphs, different root orders, and every three-node monotone +//! Boolean system. +//! +//! This module contains the small judgments shared by the focused suites. Each +//! one isolates a particular cache-identity or invalidation case. + +#![cfg(test)] + +use std::cell::Cell; + +use crate::{judgment_fn, ProvenSet, Set}; + +use super::memo; + +mod iteration; +mod root_scope; +mod soundness; + +// These counters are observability probes. A memo hit has the same semantic +// result as ordinary execution, so the tests count judgment-body executions to +// distinguish reuse from recomputation. The memo context clears itself when a +// root returns, so each test only resets the counters it observes. +thread_local! { + static INVALIDATED_CHILD_EXECUTIONS: Cell = const { Cell::new(0) }; + static FAILED_CHILD_EXECUTIONS: Cell = const { Cell::new(0) }; + static CROSS_TYPE_EXECUTIONS: Cell = const { Cell::new(0) }; + static IDENTITY_LEFT_EXECUTIONS: Cell = const { Cell::new(0) }; + static IDENTITY_RIGHT_EXECUTIONS: Cell = const { Cell::new(0) }; +} + +fn values(proven: ProvenSet) -> Set +where + T: Clone + std::fmt::Debug + Ord, +{ + proven.iter().map(|(value, _)| value).collect() +} + +// This mutually recursive pair has different output types. It checks that one +// erased memo context can safely hold entries for both judgments while their +// fixed points grow together. +judgment_fn! { + fn cross_type_a() => u32 { + debug() + + ( + --- ("base") + (cross_type_a() => 0) + ) + + ( + (cross_type_b() => flag) + (cross_type_b() => _) + (if *flag)! + --- ("from b") + (cross_type_a() => 1) + ) + } +} + +judgment_fn! { + fn cross_type_b() => bool { + debug() + + ( + (let () = CROSS_TYPE_EXECUTIONS.set( + CROSS_TYPE_EXECUTIONS.get() + 1, + )) + --- ("base") + (cross_type_b() => false) + ) + + ( + (cross_type_a() => value) + (if *value == 0)! + --- ("from a") + (cross_type_b() => true) + ) + } +} + +// These judgments have identical Rust signatures but different generated +// judgment identities. Their entries must never collide in an erased table. +judgment_fn! { + fn identity_left(value: u32) => u32 { + debug(value) + + ( + (let () = IDENTITY_LEFT_EXECUTIONS.set( + IDENTITY_LEFT_EXECUTIONS.get() + 1, + )) + --- ("left") + (identity_left(value) => *value + 1) + ) + } +} + +judgment_fn! { + fn identity_right(value: u32) => u32 { + debug(value) + + ( + (let () = IDENTITY_RIGHT_EXECUTIONS.set( + IDENTITY_RIGHT_EXECUTIONS.get() + 1, + )) + --- ("right") + (identity_right(value) => *value + 2) + ) + } +} + +judgment_fn! { + fn calls_same_signature_judgments(value: u32) => u32 { + debug(value) + + ( + (identity_left(value) => left) + (identity_left(value) => _) + (identity_right(value) => right) + (identity_right(value) => _) + --- ("both") + (calls_same_signature_judgments(value) => *left + *right) + ) + } +} + +// Failed judgments carry diagnostics that are not represented in a proof map. +// Re-executing this judgment is therefore required: caching its empty result +// would incorrectly turn a contextual failure into a reusable negative fact. +judgment_fn! { + fn failed_child() => () { + debug() + + ( + (let () = FAILED_CHILD_EXECUTIONS.set( + FAILED_CHILD_EXECUTIONS.get() + 1, + )) + (if false) + --- ("failure") + (failed_child() => ()) + ) + } +} + +judgment_fn! { + fn calls_failed_child_twice() => () { + debug() + + ( + (let first = failed_child()) + (let second = failed_child()) + (if !first.is_proven() && !second.is_proven()) + --- ("twice") + (calls_failed_child_twice() => ()) + ) + } +} + +// `invalidation_b` first completes using the initial approximation of `a`. +// When `a` grows, its enclosing iteration is invalidated and `b` must execute +// again rather than reuse the result computed under the older approximation. +judgment_fn! { + fn invalidation_a() => u32 { + debug() + + ( + --- ("base") + (invalidation_a() => 0) + ) + + ( + (invalidation_b() => value) + (invalidation_b() => _) + --- ("from b") + (invalidation_a() => value) + ) + } +} + +judgment_fn! { + fn invalidation_b() => u32 { + debug() + + ( + (let () = INVALIDATED_CHILD_EXECUTIONS.set( + INVALIDATED_CHILD_EXECUTIONS.get() + 1, + )) + --- ("base") + (invalidation_b() => 1) + ) + + ( + (invalidation_a() => value) + (if *value == 0)! + --- ("after a grows") + (invalidation_b() => 2) + ) + } +} diff --git a/crates/formality-core/src/judgment/test_memo/root_scope.rs b/crates/formality-core/src/judgment/test_memo/root_scope.rs new file mode 100644 index 000000000..4a0369858 --- /dev/null +++ b/crates/formality-core/src/judgment/test_memo/root_scope.rs @@ -0,0 +1,87 @@ +//! Root-scoped memoization tests. +//! +//! Completed judgments may be reused by other calls made while the same +//! top-level judgment is active. Once that root returns, its iteration table is +//! discarded: neither the root's result nor any completed descendant can be +//! observed by a later top-level call. + +use std::cell::Cell; + +use crate::judgment_fn; + +use super::*; + +thread_local! { + static ROOT_EXECUTIONS: Cell = const { Cell::new(0) }; + static SHARED_CHILD_EXECUTIONS: Cell = const { Cell::new(0) }; +} + +judgment_fn! { + fn counted_root(value: u32) => u32 { + debug(value) + + ( + (let () = ROOT_EXECUTIONS.set(ROOT_EXECUTIONS.get() + 1)) + --- ("value") + (counted_root(value) => value) + ) + } +} + +judgment_fn! { + fn shared_child() => u32 { + debug() + + ( + (let () = SHARED_CHILD_EXECUTIONS.set( + SHARED_CHILD_EXECUTIONS.get() + 1, + )) + --- ("value") + (shared_child() => 22) + ) + } +} + +judgment_fn! { + fn first_root() => u32 { + debug() + + ( + (shared_child() => value) + --- ("child") + (first_root() => value) + ) + } +} + +judgment_fn! { + fn second_root() => u32 { + debug() + + ( + (shared_child() => value) + --- ("child") + (second_root() => value) + ) + } +} + +#[test] +fn top_level_result_does_not_survive_its_call() { + ROOT_EXECUTIONS.set(0); + + assert_eq!(values(counted_root(22)), crate::set![22]); + assert_eq!(values(counted_root(22)), crate::set![22]); + + assert_eq!(ROOT_EXECUTIONS.get(), 2); +} + +#[test] +fn completed_descendant_does_not_survive_its_root() { + SHARED_CHILD_EXECUTIONS.set(0); + + assert_eq!(values(first_root()), crate::set![22]); + assert_eq!(values(second_root()), crate::set![22]); + + assert_eq!(SHARED_CHILD_EXECUTIONS.get(), 2); +} diff --git a/crates/formality-core/src/judgment/test_memo/soundness.rs b/crates/formality-core/src/judgment/test_memo/soundness.rs new file mode 100644 index 000000000..0eaa64cbf --- /dev/null +++ b/crates/formality-core/src/judgment/test_memo/soundness.rs @@ -0,0 +1,343 @@ +//! End-to-end memoization soundness checks. +//! +//! The focused tests in the sibling modules assert particular cache events. +//! These tests instead use uncached execution as an oracle and check that +//! memoization preserves the result. In addition to cyclic reachability from +//! independent roots, they systematically test small systems of mutually +//! recursive Boolean judgments. +//! +//! For example, one system we want to test could have been written by hand as +//! these three judgment functions: +//! +//! ```text +//! judgment_fn! { +//! fn a() => () { +//! ( +//! (b() => ()) +//! ----------- ("from b") +//! (a() => ()) +//! ) +//! ( +//! (c() => ()) +//! ----------- ("from c") +//! (a() => ()) +//! ) +//! } +//! } +//! +//! judgment_fn! { +//! fn b() => () { +//! ( +//! (a() => ()) +//! (c() => ()) +//! ----------- ("from a and c") +//! (b() => ()) +//! ) +//! } +//! } +//! +//! judgment_fn! { +//! fn c() => () { +//! ( +//! ----------- ("unconditional") +//! (c() => ()) +//! ) +//! } +//! } +//! ``` +//! +//! In other words, `a` is proven if `b || c`, `b` is proven if `a && c`, and +//! `c` is always proven. Starting with no proven judgments, the fixed-point +//! computation first proves `c`, then `a` from `c`, and finally `b` from `a` +//! and `c`. +//! +//! The test represents each handwritten function by a truth table. The input +//! to the table is the set of judgments currently proven: bit 0 means `a`, bit +//! 1 means `b`, and bit 2 means `c`. The eight possible inputs range from +//! `0b000` (nothing proven) through `0b111` (all three proven). The output at +//! each input says whether that function's rules have enough premises to prove +//! its judgment: +//! +//! | Proven judgments | Input and output-bit index | Can `a` be proven? | +//! | ---------------- | -------------------------- | ------------------ | +//! | none | `000` | no | +//! | `a` | `001` | no | +//! | `b` | `010` | yes | +//! | `a, b` | `011` | yes | +//! | `c` | `100` | yes | +//! | `a, c` | `101` | yes | +//! | `b, c` | `110` | yes | +//! | `a, b, c` | `111` | yes | +//! +//! ```text +//! function for a: b || c = 0b1111_1100 +//! function for b: a && c = 0b1010_0000 +//! function for c: true = 0b1111_1111 +//! ``` +//! +//! For example, `a`'s byte has output bit 2 set because input `0b010` means +//! that `b` is proven, which is enough to use `a`'s `"from b"` rule. Its +//! minimal satisfying sets are `{b}` and `{c}`. `MonotoneSystem::clauses` +//! recovers those sets from the byte, and `monotone_node` evaluates each set as +//! the premises of one rule. Thus the parameterized `monotone_node(system, +//! node)` is the data-driven equivalent of the three functions above. +//! +//! There are only 256 possible eight-bit truth tables. `monotone_functions` +//! filters those down to the 20 monotone functions, and `MonotoneSystem` assigns +//! one of those functions independently to each of `a`, `b`, and `c`. The final +//! test can therefore enumerate all `20^3 = 8,000` three-judgment systems and +//! compare memoized execution with the uncached oracle for every starting order. + +use std::sync::Arc; + +use crate::{cast_impl, judgment_fn}; + +use super::{memo, values}; + +#[derive(Clone, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)] +struct FiniteGraph { + edges: Vec<(u32, u32)>, +} + +cast_impl!(FiniteGraph); + +impl FiniteGraph { + fn successors(&self, node: u32) -> Vec { + self.edges + .iter() + .filter_map(|(from, to)| (*from == node).then_some(*to)) + .collect() + } +} + +judgment_fn! { + fn memo_reachable(graph: Arc, from: u32) => u32 { + debug(graph, from) + + ( + (to in graph.successors(*from)) + --- ("edge") + (memo_reachable(graph, from) => to) + ) + + ( + (memo_reachable(graph, from) => intermediate) + (memo_reachable(graph, intermediate) => to) + --- ("transitive") + (memo_reachable(graph, from) => to) + ) + } +} + +const BOOLEAN_NODES: [u8; 3] = [0, 1, 2]; +const BOOLEAN_ROOT_ORDERS: [[u8; 3]; 6] = [ + [0, 1, 2], + [0, 2, 1], + [1, 0, 2], + [1, 2, 0], + [2, 0, 1], + [2, 1, 0], +]; + +/// Three mutually recursive Boolean judgments. +/// +/// Each function is represented by an eight-bit truth table indexed by the set +/// of variables that are true. Only monotone truth tables are used. +#[derive(Clone, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)] +struct MonotoneSystem { + functions: [u8; 3], +} + +cast_impl!(MonotoneSystem); + +impl MonotoneSystem { + /// Return the minimal satisfying sets for `node`'s function. + /// + /// These sets are the clauses in the function's canonical monotone DNF. + /// An empty list is `false`; a list containing an empty clause is `true`. + /// + /// For the system in the module-level example, nodes `0`, `1`, and `2` + /// stand for `a`, `b`, and `c`, respectively. This method recovers the + /// premises of their handwritten rules: + /// + /// ```text + /// clauses(0) = [[1], [2]] // a follows from b, or from c + /// clauses(1) = [[0, 2]] // b follows from a and c + /// clauses(2) = [[]] // c follows without any premises + /// ``` + fn clauses(&self, node: u8) -> Vec> { + let function = self.functions[usize::from(node)]; + + (0_u8..8) + .filter(|&variables| function_holds(function, variables)) + .filter(|&variables| { + !(0_u8..8).any(|subset| { + subset != variables + && subset & !variables == 0 + && function_holds(function, subset) + }) + }) + .map(|variables| { + BOOLEAN_NODES + .into_iter() + .filter(|node| variables & (1_u8 << u32::from(*node)) != 0) + .collect() + }) + .collect() + } +} + +fn function_holds(function: u8, variables: u8) -> bool { + function & (1_u8 << u32::from(variables)) != 0 +} + +fn is_monotone_function(function: u8) -> bool { + (0_u8..8).all(|variables| { + (0_u8..8).all(|more_variables| { + variables & !more_variables != 0 + || !function_holds(function, variables) + || function_holds(function, more_variables) + }) + }) +} + +fn monotone_functions() -> Vec { + (u8::MIN..=u8::MAX) + .filter(|function| is_monotone_function(*function)) + .collect() +} + +fn clauses_hold(clauses: &[Vec], variables: u8) -> bool { + clauses.iter().any(|clause| { + clause + .iter() + .all(|node| variables & (1_u8 << u32::from(*node)) != 0) + }) +} + +// This single parameterized judgment executes the rules recovered by +// `MonotoneSystem::clauses`. For `a` (node 0) in the module-level example, it +// considers clauses `[1]` and `[2]`. Recursively proving every dependency in +// `[1]` executes the handwritten "a from b" rule; doing the same for `[2]` +// executes "a from c". For `b`, its one clause `[0, 2]` requires both `a` and +// `c`. For `c`, the empty clause requires nothing and therefore succeeds +// unconditionally. +judgment_fn! { + fn monotone_node(system: MonotoneSystem, node: u8) => () { + debug(system, node) + + ( + (clause in system.clauses(*node)) + (for_all(dependency in clause) + (monotone_node(system, dependency) => ())) + --- ("minimal satisfying clause") + (monotone_node(system, node) => ()) + ) + } +} + +#[test] +fn independent_roots_match_uncached_evaluation_in_every_order() { + let graph = Arc::new(FiniteGraph { + edges: vec![(0, 1), (0, 2), (1, 3), (2, 3), (3, 1)], + }); + let roots = [0, 1, 2, 3]; + let expected: Vec<_> = roots + .iter() + .map(|root| { + let _mode = memo::TestModeGuard::new(false); + values(memo_reachable(&graph, *root)) + }) + .collect(); + + for order in [roots, [3, 2, 1, 0], [1, 3, 0, 2]] { + let _mode = memo::TestModeGuard::new(true); + for root in order { + assert_eq!( + values(memo_reachable(&graph, root)), + expected[root as usize], + "root={root}, order={order:?}", + ); + } + } +} + +#[test] +fn memoized_positive_graphs_match_uncached_evaluation() { + let graphs = [ + FiniteGraph { + edges: vec![(0, 0)], + }, + FiniteGraph { + edges: vec![(0, 1), (1, 0), (1, 2)], + }, + FiniteGraph { + edges: vec![(0, 1), (0, 2), (1, 3), (2, 3), (3, 1)], + }, + ]; + + for graph in graphs { + let graph = Arc::new(graph); + for root in 0..=3 { + let without_memo = { + let _mode = memo::TestModeGuard::new(false); + values(memo_reachable(&graph, root)) + }; + let with_memo = { + let _mode = memo::TestModeGuard::new(true); + values(memo_reachable(&graph, root)) + }; + assert_eq!(with_memo, without_memo, "graph={graph:?}, root={root}"); + } + } +} + +#[test] +fn all_three_node_monotone_systems_match_in_every_root_order() { + let functions = monotone_functions(); + assert_eq!(functions.len(), 20); + + for &function in &functions { + let system = MonotoneSystem { + functions: [function; 3], + }; + let clauses = system.clauses(0); + for variables in 0_u8..8 { + assert_eq!( + clauses_hold(&clauses, variables), + function_holds(function, variables), + "function={function:08b}, variables={variables:03b}", + ); + } + } + + let mut system_count = 0; + for &function_a in &functions { + for &function_b in &functions { + for &function_c in &functions { + system_count += 1; + let system = MonotoneSystem { + functions: [function_a, function_b, function_c], + }; + + let expected = { + let _mode = memo::TestModeGuard::new(false); + BOOLEAN_NODES.map(|node| monotone_node(&system, node).is_proven()) + }; + + for order in BOOLEAN_ROOT_ORDERS { + let _mode = memo::TestModeGuard::new(true); + for node in order { + assert_eq!( + monotone_node(&system, node).is_proven(), + expected[usize::from(node)], + "system={system:?}, order={order:?}, node={node}", + ); + } + } + } + } + } + + assert_eq!(system_count, 8_000); +} diff --git a/crates/formality-core/src/judgment/test_panic.rs b/crates/formality-core/src/judgment/test_panic.rs new file mode 100644 index 000000000..54fc120a0 --- /dev/null +++ b/crates/formality-core/src/judgment/test_panic.rs @@ -0,0 +1,50 @@ +#![cfg(test)] + +use std::cell::Cell; + +use crate::judgment_fn; + +use super::memo; + +thread_local! { + static PANIC_ON_BASE_CASE: Cell = const { Cell::new(true) }; +} + +// The `true` case opens a recursive judgment and memo iteration, then calls the +// `false` base case. The base case panics only on its first execution. This +// forces both the active-judgment guard and the memo iteration guard to unwind +// through a nested call. Calling the judgment again after catching the panic +// checks that neither guard left stale thread-local state behind. +judgment_fn! { + fn panic_during_recursion(recurse: bool) => () { + debug(recurse) + + ( + (panic_during_recursion(false) => ()) + --- ("recursive") + (panic_during_recursion(true) => ()) + ) + + ( + (let () = PANIC_ON_BASE_CASE.with(|flag| { + assert!(!flag.replace(false), "panic from judgment body"); + })) + --- ("base") + (panic_during_recursion(false) => ()) + ) + } +} + +#[test] +fn panic_does_not_leave_an_active_judgment_behind() { + use std::panic::{catch_unwind, AssertUnwindSafe}; + + PANIC_ON_BASE_CASE.set(true); + + let panic = catch_unwind(AssertUnwindSafe(|| panic_during_recursion(true))); + assert!(panic.is_err()); + assert_eq!(memo::active_iteration_count(), 0); + + let result = panic_during_recursion(true); + assert!(result.is_proven(), "{result}"); +} diff --git a/crates/formality-core/src/lib.rs b/crates/formality-core/src/lib.rs index 40ecf123c..8d17217de 100644 --- a/crates/formality-core/src/lib.rs +++ b/crates/formality-core/src/lib.rs @@ -17,7 +17,7 @@ pub use tracing::instrument; pub use tracing::trace; // Re-export things from formality-macros. -pub use formality_macros::{fixed_point, respan, term, test, Visit}; +pub use formality_macros::{respan, term, test, Visit}; pub type Fallible = anyhow::Result; @@ -27,7 +27,6 @@ pub type Fallible = anyhow::Result; pub mod binder; mod cast; mod collections; -pub mod fixed_point; pub mod fold; pub mod judgment; pub mod language; diff --git a/crates/formality-macros/src/fixed_point.rs b/crates/formality-macros/src/fixed_point.rs deleted file mode 100644 index 286fd8909..000000000 --- a/crates/formality-macros/src/fixed_point.rs +++ /dev/null @@ -1,306 +0,0 @@ -// expected input is something like -// -// #[fixed_point(default = )] -// fn foo(k1: Key1, k2: &Key2) -> R -// -// where: -// -// * parameters may or may not be `&` type; they must be cloneable + ord -// * parameters cannot have complex patterns to make my life easier -// * the return value R must be cloneable + ord -// * the default for the expression `` is `Default::default`, and `E` may reference fn args -// -// generates: -// -// fn foo(k1: Key1, k2: &Key2) -> R { -// thread_local! { static _CACHE: RefCell> = Default::default() } -// fixed_point( -// |(k1, k2)| { -// tracing::debug_span!( -// stringify!(foo), -// ?k1, -// ?k2, -// ) -// }, -// &_CACHE, -// (k1, k2.clone()), -// |(k1, k2)| , -// |(k1, ref k2)| , -// ) -// } - -use quote::quote; - -#[derive(Default)] -pub(crate) struct FixedPointArgs { - default: Option, -} - -impl syn::parse::Parse for FixedPointArgs { - fn parse(input: syn::parse::ParseStream) -> syn::Result { - let mut args: FixedPointArgs = Default::default(); - while !input.is_empty() { - let ident: syn::Ident = input.parse()?; - let _: syn::Token!(=) = input.parse()?; - if ident == "default" { - let expr: syn::Expr = input.parse()?; - args.default = Some(expr); - } else { - return Err(syn::Error::new_spanned( - ident, - "valid arguments: ['default']", - )); - } - - // Parse comma after each argument. - let comma: syn::Result = input.parse(); - if comma.is_err() && !input.is_empty() { - // If no comma, must be end of input. - return Err(syn::Error::new_spanned(ident, "expected `,`")); - } - } - Ok(args) - } -} - -struct Input { - is_ref: bool, - is_mut: Option, - ident: syn::Ident, - ty: syn::Type, -} - -pub(crate) fn fixed_point( - args: FixedPointArgs, - mut item_fn: syn::ItemFn, -) -> syn::Result { - let syn::ItemFn { - attrs: _, - vis: _, - sig, - block, - } = &item_fn; - - let (inputs, output_ty) = validate_fixed_point_sig(sig)?; - - let input_tys: Vec<_> = inputs.iter().map(|i| &i.ty).collect(); - - let thread_local = quote! { - thread_local! { - static __CACHE: - std::cell::RefCell< - formality_core::fixed_point::FixedPointStack< - (#(#input_tys),*), - #output_ty - > - > - = Default::default() - } - }; - - // names like k1, k2 - let input_names: Vec<_> = inputs.iter().map(|input| &input.ident).collect(); - - // |(k1, k2)| tracing::debug_span(...) - let tracing_span_expr = { - let fn_name = &item_fn.sig.ident; - quote!( - |(#(#input_names),*)| { - tracing::debug_span!( - stringify!(#fn_name), - #(?#input_names),* - ) - } - ) - }; - - // (k1, k2.clone()), - let input_expr = { - let input_exprs: Vec<_> = inputs - .iter() - .map(|Input { is_ref, ident, .. }| { - if *is_ref { - quote! {Clone::clone(#ident)} - } else { - quote! {#ident} - } - }) - .collect(); - quote!((#(#input_exprs,)*)) - }; - - // |(k1, k2)| , - let default_expr = { - let default_pattern = quote!((#(#input_names),*)); - let default_body = args - .default - .map(|e| quote!(#e)) - .unwrap_or(quote!(Default::default())); - quote!( - #[allow(unused_variables)] - |#default_pattern| #default_body - ) - }; - - // |(k1, ref k2)| , - let body_expr = { - let input_patterns: Vec<_> = inputs - .iter() - .map( - |Input { - is_ref, - ident, - is_mut, - ty: _, - }| { - if *is_ref { - assert!(is_mut.is_none()); - quote! {ref #ident} - } else { - quote! {#is_mut #ident} - } - }, - ) - .collect(); - quote!(|(#(#input_patterns),*)| #block) - }; - - clear_mut_args(&mut item_fn.sig); - item_fn.block = syn::parse( - quote! { - { - #thread_local - formality_core::fixed_point::fixed_point( - #tracing_span_expr, - &__CACHE, - #input_expr, - #default_expr, - #body_expr, - ) - } - } - .into(), - ) - .unwrap(); - - Ok(item_fn) -} - -fn clear_mut_args(sig: &mut syn::Signature) { - for input in &mut sig.inputs { - match input { - syn::FnArg::Receiver(_) => {} - syn::FnArg::Typed(t) => match &mut *t.pat { - syn::Pat::Ident(i) => i.mutability = None, - _ => panic!("unexpected pattern"), - }, - } - } -} - -fn validate_fixed_point_sig(sig: &syn::Signature) -> syn::Result<(Vec, syn::Type)> { - let mut inputs = vec![]; - for input in &sig.inputs { - match input { - syn::FnArg::Receiver(r) => { - return Err(syn::Error::new_spanned( - r, - "fixed-point methods not yet supported", - )); - } - syn::FnArg::Typed(syn::PatType { pat, ty, .. }) => { - let (ident, is_mut) = validate_arg_pattern(pat)?; - let (is_ref, ty) = validate_arg_ty(ty)?; - - if is_mut.is_some() && is_ref { - return Err(syn::Error::new_spanned( - input, - "variables can be mut or by-ref, but not both", - )); - } - - inputs.push(Input { - is_ref, - is_mut, - ty, - ident, - }); - } - } - } - - let output_ty = match &sig.output { - syn::ReturnType::Default => { - return Err(syn::Error::new_spanned(sig, "return type required")); - } - syn::ReturnType::Type(_, ty) => { - validate_ty(ty)?; - syn::Type::clone(ty) - } - }; - - Ok((inputs, output_ty)) -} - -fn validate_arg_pattern(pat: &syn::Pat) -> syn::Result<(syn::Ident, Option)> { - match pat { - syn::Pat::Ident(ident) => { - if let Some(r) = ident.by_ref { - return Err(syn::Error::new_spanned( - r, - "ref patterns not accepted in fixed-point functions", - )); - } - - Ok((ident.ident.clone(), ident.mutability)) - } - _ => Err(syn::Error::new_spanned( - pat, - "argument patterns not accepted in fixed-point functions", - )), - } -} - -fn validate_arg_ty(ty: &syn::Type) -> syn::Result<(bool, syn::Type)> { - match ty { - syn::Type::Reference(r) => { - if r.mutability.is_some() { - return Err(syn::Error::new_spanned( - ty, - "`&mut` arguments not permitted in fixed-point functions", - )); - } - - if r.lifetime.is_some() { - return Err(syn::Error::new_spanned( - ty, - "named lifetimes not permitted in fixed-point functions", - )); - } - - validate_ty(&r.elem)?; - - Ok((true, Clone::clone(&r.elem))) - } - _ => { - validate_ty(ty)?; - Ok((false, ty.clone())) - } - } -} - -fn validate_ty(ty: &syn::Type) -> syn::Result<()> { - match ty { - syn::Type::ImplTrait(_) => Err(syn::Error::new_spanned( - ty, - "impl Trait types not allowed in fixed-point functions", - )), - - syn::Type::Reference(_) => Err(syn::Error::new_spanned( - ty, - "reference types only allowed at the top-level in fixed-point functions", - )), - - _ => Ok(()), - } -} diff --git a/crates/formality-macros/src/lib.rs b/crates/formality-macros/src/lib.rs index 338c65a5b..0f6600865 100644 --- a/crates/formality-macros/src/lib.rs +++ b/crates/formality-macros/src/lib.rs @@ -11,7 +11,6 @@ mod cast; mod constructors; mod custom; mod debug; -mod fixed_point; mod fold; mod parse; mod precedence; @@ -42,16 +41,6 @@ pub fn term(args: TokenStream, input: TokenStream) -> TokenStream { synstructure::decl_derive!([Visit] => visit::derive_visit); -#[proc_macro_attribute] -pub fn fixed_point(args: TokenStream, input: TokenStream) -> TokenStream { - let args = syn::parse_macro_input!(args as fixed_point::FixedPointArgs); - let input = syn::parse_macro_input!(input as syn::ItemFn); - match fixed_point::fixed_point(args, input) { - Ok(s) => quote!(#s).into(), - Err(e) => e.into_compile_error().into(), - } -} - #[proc_macro_attribute] pub fn test(args: TokenStream, input: TokenStream) -> TokenStream { let input = syn::parse_macro_input!(input as syn::ItemFn);