pumpkin_checking/
lib.rs

1//! Exposes a common interface used to check inferences.
2//!
3//! The main exposed type is the [`InferenceChecker`], which can be implemented to verify whether
4//! inferences are sound w.r.t. an inference rule.
5
6mod atomic_constraint;
7mod int_ext;
8mod union;
9mod variable;
10mod variable_state;
11
12use std::fmt::Debug;
13
14pub use atomic_constraint::*;
15use dyn_clone::DynClone;
16pub use int_ext::*;
17pub use union::*;
18pub use variable::*;
19pub use variable_state::*;
20
21/// An inference checker tests whether the given state is a conflict under the sematics of an
22/// inference rule.
23pub trait InferenceChecker<Atomic: AtomicConstraint>: Debug + DynClone {
24    /// Returns `true` if `state` is a conflict, and `false` if not.
25    ///
26    /// For the conflict check, all the premises are true in the state and the consequent, if
27    /// present, if false.
28    fn check(
29        &self,
30        state: VariableState<Atomic>,
31        premises: &[Atomic],
32        consequent: Option<&Atomic>,
33    ) -> bool;
34}
35
36/// Wrapper around `Box<dyn InferenceChecker<Atomic>>` that implements [`Clone`].
37#[derive(Debug)]
38pub struct BoxedChecker<Atomic: AtomicConstraint>(Box<dyn InferenceChecker<Atomic>>);
39
40impl<Atomic: AtomicConstraint> Clone for BoxedChecker<Atomic> {
41    fn clone(&self) -> Self {
42        BoxedChecker(dyn_clone::clone_box(&*self.0))
43    }
44}
45
46impl<Atomic: AtomicConstraint> From<Box<dyn InferenceChecker<Atomic>>> for BoxedChecker<Atomic> {
47    fn from(value: Box<dyn InferenceChecker<Atomic>>) -> Self {
48        BoxedChecker(value)
49    }
50}
51
52impl<Atomic: AtomicConstraint> BoxedChecker<Atomic> {
53    /// See [`InferenceChecker::check`].
54    pub fn check(
55        &self,
56        variable_state: VariableState<Atomic>,
57        premises: &[Atomic],
58        consequent: Option<&Atomic>,
59    ) -> bool {
60        self.0.check(variable_state, premises, consequent)
61    }
62}
pumpkin_checking/lib.rs

pumpkin_checking/
lib.rs
