match_lang/
checker.rs

1//! The configurable, reusable entry point.
2
3use core::fmt;
4
5use crate::{Arm, Error, Model, Report, engine::Engine};
6
7/// The default [step limit](Checker::with_step_limit): about 16.7 million
8/// units of work. Real matches, even with tens of thousands of arms, use a
9/// small fraction of it; a pathological one stops in well under a second.
10pub const DEFAULT_STEP_LIMIT: u64 = 1 << 24;
11
12/// The default [witness limit](Checker::with_witness_limit).
13pub const DEFAULT_WITNESS_LIMIT: usize = 16;
14
15/// Checks matches for exhaustiveness and usefulness, reusing its buffers
16/// from one check to the next.
17///
18/// [`check`](crate::check) is a `Checker` used once with default limits. Keep
19/// a `Checker` around when checking many matches (a whole program's): after
20/// the first few checks it allocates almost nothing. Configure it with:
21///
22/// - [`with_step_limit`](Checker::with_step_limit): how much work one check
23///   may do before giving up with [`Error::StepLimit`].
24/// - [`with_witness_limit`](Checker::with_witness_limit): how many missing
25///   cases one report lists at most.
26///
27/// # Examples
28///
29/// ```
30/// use match_lang::{Arm, Checker, Model, Pat, Signature};
31///
32/// struct Bytes;
33///
34/// impl Model for Bytes {
35///     type Ty = ();
36///     fn signature(&self, _: &()) -> Signature<()> {
37///         Signature::Int { min: 0, max: 255 }
38///     }
39///     fn fields(&self, _: &(), _: u32, _: &mut Vec<()>) {}
40/// }
41///
42/// let mut checker = Checker::new().with_witness_limit(2);
43/// for n in 0..10 {
44///     let arms: Vec<Arm> = (0..n).map(|i| Arm::new(Pat::int(i * 2))).collect();
45///     let report = checker.check(&Bytes, &(), &arms)?;
46///     assert!(!report.is_exhaustive());
47///     assert!(report.missing().len() <= 2);
48/// }
49/// # Ok::<(), match_lang::Error>(())
50/// ```
51pub struct Checker<T> {
52    engine: Engine<T>,
53    step_limit: u64,
54    witness_limit: usize,
55}
56
57impl<T: Clone> Checker<T> {
58    /// A checker with the default limits ([`DEFAULT_STEP_LIMIT`] and
59    /// [`DEFAULT_WITNESS_LIMIT`]).
60    ///
61    /// # Examples
62    ///
63    /// ```
64    /// use match_lang::{Checker, DEFAULT_STEP_LIMIT};
65    ///
66    /// let checker: Checker<()> = Checker::new();
67    /// assert_eq!(checker.step_limit(), DEFAULT_STEP_LIMIT);
68    /// ```
69    #[must_use]
70    pub fn new() -> Checker<T> {
71        Checker {
72            engine: Engine::new(),
73            step_limit: DEFAULT_STEP_LIMIT,
74            witness_limit: DEFAULT_WITNESS_LIMIT,
75        }
76    }
77
78    /// Sets how many units of work one check may do. A unit is roughly one
79    /// matrix row, cell, or witness node built, or one constructor examined;
80    /// [`Report::steps`] tells how many a check used. A check that would
81    /// exceed the limit stops with [`Error::StepLimit`], so time and memory
82    /// per check are bounded by the limit whatever the input.
83    ///
84    /// # Examples
85    ///
86    /// ```
87    /// use match_lang::{Arm, Checker, Error, Model, Pat, Signature};
88    ///
89    /// struct Bytes;
90    ///
91    /// impl Model for Bytes {
92    ///     type Ty = ();
93    ///     fn signature(&self, _: &()) -> Signature<()> {
94    ///         Signature::Int { min: 0, max: 255 }
95    ///     }
96    ///     fn fields(&self, _: &(), _: u32, _: &mut Vec<()>) {}
97    /// }
98    ///
99    /// let arms: Vec<Arm> = (0..100).map(|i| Arm::new(Pat::int(i))).collect();
100    /// let mut tight = Checker::new().with_step_limit(10);
101    /// assert_eq!(tight.check(&Bytes, &(), &arms).unwrap_err(), Error::StepLimit { limit: 10 });
102    /// ```
103    #[must_use]
104    pub fn with_step_limit(mut self, limit: u64) -> Checker<T> {
105        self.step_limit = limit;
106        self
107    }
108
109    /// Sets the most missing cases one report lists. At least one is always
110    /// kept, since the first witness is what proves a match non-exhaustive;
111    /// `0` is treated as `1`.
112    ///
113    /// # Examples
114    ///
115    /// ```
116    /// use match_lang::Checker;
117    ///
118    /// let checker: Checker<()> = Checker::new().with_witness_limit(0);
119    /// assert_eq!(checker.witness_limit(), 1);
120    /// ```
121    #[must_use]
122    pub fn with_witness_limit(mut self, limit: usize) -> Checker<T> {
123        self.witness_limit = limit.max(1);
124        self
125    }
126
127    /// The step limit in effect.
128    ///
129    /// # Examples
130    ///
131    /// ```
132    /// use match_lang::Checker;
133    ///
134    /// assert_eq!(Checker::<()>::new().with_step_limit(99).step_limit(), 99);
135    /// ```
136    #[must_use]
137    pub fn step_limit(&self) -> u64 {
138        self.step_limit
139    }
140
141    /// The witness limit in effect.
142    ///
143    /// # Examples
144    ///
145    /// ```
146    /// use match_lang::{Checker, DEFAULT_WITNESS_LIMIT};
147    ///
148    /// assert_eq!(Checker::<()>::new().witness_limit(), DEFAULT_WITNESS_LIMIT);
149    /// ```
150    #[must_use]
151    pub fn witness_limit(&self) -> usize {
152        self.witness_limit
153    }
154
155    /// Checks `arms`, in order, against values of type `ty`.
156    ///
157    /// # Errors
158    ///
159    /// - [`Error::InvalidPattern`] if a pattern does not fit the type it is
160    ///   matched against (checked before any analysis).
161    /// - [`Error::StepLimit`] if the analysis needs more steps than the limit.
162    /// - [`Error::Model`] if the model answers inconsistently.
163    /// - [`Error::TooLarge`] past `u32::MAX - 1` pattern nodes or matrix
164    ///   entries.
165    ///
166    /// # Examples
167    ///
168    /// ```
169    /// use match_lang::{Arm, Checker, Model, Pat, Signature};
170    ///
171    /// struct Flags;
172    ///
173    /// impl Model for Flags {
174    ///     type Ty = u8; // 0: (bool, bool), 1: bool
175    ///     fn signature(&self, ty: &u8) -> Signature<u8> {
176    ///         if *ty == 0 { Signature::Product } else { Signature::Bool }
177    ///     }
178    ///     fn fields(&self, _: &u8, _: u32, out: &mut Vec<u8>) {
179    ///         out.extend([1, 1]);
180    ///     }
181    /// }
182    ///
183    /// let arms = [
184    ///     Arm::new(Pat::product([Pat::bool(true), Pat::wild()])),
185    ///     Arm::new(Pat::product([Pat::wild(), Pat::bool(true)])),
186    /// ];
187    /// let report = Checker::new().check(&Flags, &0, &arms)?;
188    /// assert_eq!(report.missing()[0].to_string(), "(false, false)");
189    /// # Ok::<(), match_lang::Error>(())
190    /// ```
191    pub fn check<M: Model<Ty = T>>(
192        &mut self,
193        model: &M,
194        ty: &T,
195        arms: &[Arm],
196    ) -> Result<Report<T>, Error> {
197        self.engine
198            .check(model, ty, arms, self.step_limit, self.witness_limit)
199    }
200}
201
202impl<T: Clone> Default for Checker<T> {
203    fn default() -> Checker<T> {
204        Checker::new()
205    }
206}
207
208impl<T> fmt::Debug for Checker<T> {
209    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
210        f.debug_struct("Checker")
211            .field("step_limit", &self.step_limit)
212            .field("witness_limit", &self.witness_limit)
213            .finish_non_exhaustive()
214    }
215}
match_lang/checker.rs

match_lang/
checker.rs
