match_lang/witness.rs
1//! Witnesses: patterns describing values that no arm matches.
2
3use alloc::vec::Vec;
4use core::fmt;
5
6use crate::Model;
7
8/// The constructor at one node of a [`Witness`].
9///
10/// # Examples
11///
12/// ```
13/// use match_lang::Ctor;
14///
15/// let gap = Ctor::Int { lo: 10, hi: 255 };
16/// assert_ne!(gap, Ctor::Wild);
17/// ```
18#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
19#[non_exhaustive]
20pub enum Ctor {
21 /// `_`: any value of the type.
22 Wild,
23 /// A value no pattern can name: an opaque literal that no arm mentions,
24 /// or a [`BigInt`](crate::Signature::BigInt) outside the `i128` range.
25 /// Printed as `_`.
26 Other,
27 /// Variant `index` of a sum type.
28 Variant(u32),
29 /// The constructor of a product type.
30 Product,
31 /// A boolean.
32 Bool(bool),
33 /// Any integer in `lo..=hi`.
34 Int {
35 /// The low end, inclusive.
36 lo: i128,
37 /// The high end, inclusive.
38 hi: i128,
39 },
40 /// Any character in `lo..=hi`.
41 Char {
42 /// The low end, inclusive.
43 lo: char,
44 /// The high end, inclusive.
45 hi: char,
46 },
47 /// An opaque literal, by id.
48 Lit(u64),
49 /// A sequence of exactly `len` elements; the fields are the elements.
50 Slice {
51 /// The number of elements.
52 len: u32,
53 },
54 /// A sequence of at least `prefix + suffix` elements; the fields are the
55 /// first `prefix` and the last `suffix` elements.
56 SliceRest {
57 /// The number of leading elements.
58 prefix: u32,
59 /// The number of trailing elements.
60 suffix: u32,
61 },
62}
63
64/// One node of a witness. Stored with the root last and each node's fields
65/// immediately before it, first field nearest: that is the order the
66/// algorithm produces them in, so building a witness never moves a node.
67#[derive(Clone, Debug, PartialEq, Eq)]
68pub(crate) struct WNode<T> {
69 pub(crate) ctor: Ctor,
70 pub(crate) ty: T,
71 pub(crate) arity: u32,
72 /// Nodes in this subtree, including this one.
73 pub(crate) size: u32,
74}
75
76/// A pattern describing values that no arm matches: proof that a match is
77/// not exhaustive.
78///
79/// Every value matching the witness is matched by no unguarded arm (a
80/// [`Wild`](Ctor::Wild) node stands for any value of its type, an
81/// [`Other`](Ctor::Other) node for any value no pattern names). Every
82/// witness matches at least one value.
83///
84/// A witness is a tree of [`WitnessRef`] nodes, each with a [`Ctor`], the
85/// type of the value at that position, and the fields beneath it. It prints
86/// in a neutral syntax with `Display`, or with the language's variant names
87/// through [`display`](Witness::display).
88///
89/// # Examples
90///
91/// ```
92/// use match_lang::{check, Arm, Ctor, Model, Pat, Signature};
93///
94/// struct Bytes;
95///
96/// impl Model for Bytes {
97/// type Ty = ();
98/// fn signature(&self, _: &()) -> Signature<()> {
99/// Signature::Int { min: 0, max: 255 }
100/// }
101/// fn fields(&self, _: &(), _: u32, _: &mut Vec<()>) {}
102/// }
103///
104/// let arms = [Arm::new(Pat::range(0, 9)), Arm::new(Pat::range(20, 255))];
105/// let report = check(&Bytes, &(), &arms)?;
106/// let witness = &report.missing()[0];
107/// assert_eq!(witness.ctor(), Ctor::Int { lo: 10, hi: 19 });
108/// assert_eq!(witness.to_string(), "10..=19");
109/// # Ok::<(), match_lang::Error>(())
110/// ```
111#[derive(Clone, PartialEq, Eq)]
112pub struct Witness<T> {
113 nodes: Vec<WNode<T>>,
114}
115
116impl<T> Witness<T> {
117 /// Wraps a node sequence holding exactly one subtree.
118 pub(crate) fn from_nodes(nodes: Vec<WNode<T>>) -> Witness<T> {
119 Witness { nodes }
120 }
121
122 /// The root node.
123 ///
124 /// # Examples
125 ///
126 /// ```
127 /// # use match_lang::{check, Arm, Ctor, Model, Pat, Signature};
128 /// # struct Flag;
129 /// # impl Model for Flag {
130 /// # type Ty = ();
131 /// # fn signature(&self, _: &()) -> Signature<()> { Signature::Bool }
132 /// # fn fields(&self, _: &(), _: u32, _: &mut Vec<()>) {}
133 /// # }
134 /// let report = check(&Flag, &(), &[Arm::new(Pat::bool(true))])?;
135 /// assert_eq!(report.missing()[0].root().ctor(), Ctor::Bool(false));
136 /// # Ok::<(), match_lang::Error>(())
137 /// ```
138 #[must_use]
139 pub fn root(&self) -> WitnessRef<'_, T> {
140 WitnessRef {
141 nodes: &self.nodes,
142 pos: self.nodes.len().saturating_sub(1),
143 }
144 }
145
146 /// The root's constructor; shorthand for `root().ctor()`.
147 ///
148 /// # Examples
149 ///
150 /// ```
151 /// # use match_lang::{check, Arm, Ctor, Model, Pat, Signature};
152 /// # struct Flag;
153 /// # impl Model for Flag {
154 /// # type Ty = ();
155 /// # fn signature(&self, _: &()) -> Signature<()> { Signature::Bool }
156 /// # fn fields(&self, _: &(), _: u32, _: &mut Vec<()>) {}
157 /// # }
158 /// let report = check(&Flag, &(), &[Arm::new(Pat::bool(false))])?;
159 /// assert_eq!(report.missing()[0].ctor(), Ctor::Bool(true));
160 /// # Ok::<(), match_lang::Error>(())
161 /// ```
162 #[must_use]
163 pub fn ctor(&self) -> Ctor {
164 self.root().ctor()
165 }
166
167 /// The type of the whole witness: the scrutinee's type.
168 ///
169 /// # Examples
170 ///
171 /// ```
172 /// # use match_lang::{check, Arm, Model, Pat, Signature};
173 /// # struct Flag;
174 /// # impl Model for Flag {
175 /// # type Ty = &'static str;
176 /// # fn signature(&self, _: &&'static str) -> Signature<&'static str> { Signature::Bool }
177 /// # fn fields(&self, _: &&'static str, _: u32, _: &mut Vec<&'static str>) {}
178 /// # }
179 /// let report = check(&Flag, &"bool", &[])?;
180 /// assert_eq!(*report.missing()[0].ty(), "bool");
181 /// # Ok::<(), match_lang::Error>(())
182 /// ```
183 #[must_use]
184 pub fn ty(&self) -> &T {
185 self.root().ty()
186 }
187
188 /// The root's fields; shorthand for `root().fields()`.
189 ///
190 /// # Examples
191 ///
192 /// ```
193 /// # use match_lang::{check, Arm, Ctor, Model, Pat, Signature};
194 /// # struct Pair;
195 /// # impl Model for Pair {
196 /// # type Ty = bool; // true: the pair, false: a bool inside it
197 /// # fn signature(&self, ty: &bool) -> Signature<bool> {
198 /// # if *ty { Signature::Product } else { Signature::Bool }
199 /// # }
200 /// # fn fields(&self, _: &bool, _: u32, out: &mut Vec<bool>) { out.extend([false, false]) }
201 /// # }
202 /// let arms = [Arm::new(Pat::product([Pat::bool(true), Pat::wild()]))];
203 /// let report = check(&Pair, &true, &arms)?;
204 /// let fields: Vec<Ctor> = report.missing()[0].fields().map(|f| f.ctor()).collect();
205 /// assert_eq!(fields, [Ctor::Bool(false), Ctor::Wild]);
206 /// # Ok::<(), match_lang::Error>(())
207 /// ```
208 pub fn fields(&self) -> WitnessFields<'_, T> {
209 self.root().fields()
210 }
211
212 /// Prints the witness with the model's variant names (see
213 /// [`Model::variant_name`]).
214 ///
215 /// # Examples
216 ///
217 /// ```
218 /// use match_lang::{check, Arm, Model, Pat, Signature};
219 ///
220 /// struct Opt;
221 ///
222 /// impl Model for Opt {
223 /// type Ty = u8; // 0: Option<bool>, 1: bool
224 /// fn signature(&self, ty: &u8) -> Signature<u8> {
225 /// if *ty == 0 { Signature::Sum { count: 2 } } else { Signature::Bool }
226 /// }
227 /// fn fields(&self, _: &u8, variant: u32, out: &mut Vec<u8>) {
228 /// if variant == 1 {
229 /// out.push(1);
230 /// }
231 /// }
232 /// fn variant_name(&self, _: &u8, variant: u32) -> Option<&str> {
233 /// Some(if variant == 0 { "None" } else { "Some" })
234 /// }
235 /// }
236 ///
237 /// let arms = [Arm::new(Pat::variant(0, [])), Arm::new(Pat::variant(1, [Pat::bool(true)]))];
238 /// let report = check(&Opt, &0, &arms)?;
239 /// assert_eq!(report.missing()[0].to_string(), "#1(false)");
240 /// assert_eq!(report.missing()[0].display(&Opt).to_string(), "Some(false)");
241 /// # Ok::<(), match_lang::Error>(())
242 /// ```
243 pub fn display<'a, M: Model<Ty = T>>(&'a self, model: &'a M) -> WitnessDisplay<'a, M> {
244 WitnessDisplay {
245 witness: self.root(),
246 model,
247 }
248 }
249}
250
251impl<T> fmt::Display for Witness<T> {
252 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
253 self.root().fmt(f)
254 }
255}
256
257impl<T> fmt::Debug for Witness<T> {
258 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
259 write!(f, "Witness({})", self.root())
260 }
261}
262
263/// A node of a [`Witness`]: its constructor, its type, and its fields.
264///
265/// # Examples
266///
267/// ```
268/// # use match_lang::{check, Arm, Ctor, Model, Pat, Signature};
269/// # struct Pair;
270/// # impl Model for Pair {
271/// # type Ty = bool;
272/// # fn signature(&self, ty: &bool) -> Signature<bool> {
273/// # if *ty { Signature::Product } else { Signature::Bool }
274/// # }
275/// # fn fields(&self, _: &bool, _: u32, out: &mut Vec<bool>) { out.extend([false, false]) }
276/// # }
277/// let arms = [Arm::new(Pat::product([Pat::wild(), Pat::bool(true)]))];
278/// let report = check(&Pair, &true, &arms)?;
279/// let root = report.missing()[0].root();
280/// assert_eq!(root.ctor(), Ctor::Product);
281/// assert_eq!(root.arity(), 2);
282/// let second = root.fields().nth(1).unwrap();
283/// assert_eq!((second.ctor(), *second.ty()), (Ctor::Bool(false), false));
284/// # Ok::<(), match_lang::Error>(())
285/// ```
286pub struct WitnessRef<'a, T> {
287 nodes: &'a [WNode<T>],
288 pos: usize,
289}
290
291impl<T> Clone for WitnessRef<'_, T> {
292 fn clone(&self) -> Self {
293 *self
294 }
295}
296
297impl<T> Copy for WitnessRef<'_, T> {}
298
299impl<'a, T> WitnessRef<'a, T> {
300 fn node(&self) -> Option<&'a WNode<T>> {
301 self.nodes.get(self.pos)
302 }
303
304 /// The constructor at this node.
305 ///
306 /// # Examples
307 ///
308 /// ```
309 /// # use match_lang::{check, Arm, Ctor, Model, Pat, Signature};
310 /// # struct Flag;
311 /// # impl Model for Flag {
312 /// # type Ty = ();
313 /// # fn signature(&self, _: &()) -> Signature<()> { Signature::Bool }
314 /// # fn fields(&self, _: &(), _: u32, _: &mut Vec<()>) {}
315 /// # }
316 /// let report = check(&Flag, &(), &[Arm::new(Pat::bool(true))])?;
317 /// assert_eq!(report.missing()[0].root().ctor(), Ctor::Bool(false));
318 /// # Ok::<(), match_lang::Error>(())
319 /// ```
320 #[must_use]
321 pub fn ctor(&self) -> Ctor {
322 self.node().map_or(Ctor::Wild, |n| n.ctor)
323 }
324
325 /// The type of the value at this node.
326 ///
327 /// # Examples
328 ///
329 /// ```
330 /// # use match_lang::{check, Arm, Model, Pat, Signature};
331 /// # struct Flag;
332 /// # impl Model for Flag {
333 /// # type Ty = u8;
334 /// # fn signature(&self, _: &u8) -> Signature<u8> { Signature::Bool }
335 /// # fn fields(&self, _: &u8, _: u32, _: &mut Vec<u8>) {}
336 /// # }
337 /// let report = check(&Flag, &7, &[])?;
338 /// assert_eq!(*report.missing()[0].root().ty(), 7);
339 /// # Ok::<(), match_lang::Error>(())
340 /// ```
341 #[must_use]
342 pub fn ty(&self) -> &'a T {
343 // A `WitnessRef` is only made for positions inside its witness, and a
344 // witness always has a root, so the fallback is never taken.
345 match self.nodes.get(self.pos) {
346 Some(node) => &node.ty,
347 None => &self.nodes[0].ty,
348 }
349 }
350
351 /// The number of fields under this node.
352 ///
353 /// # Examples
354 ///
355 /// ```
356 /// # use match_lang::{check, Arm, Model, Pat, Signature};
357 /// # struct Flag;
358 /// # impl Model for Flag {
359 /// # type Ty = ();
360 /// # fn signature(&self, _: &()) -> Signature<()> { Signature::Bool }
361 /// # fn fields(&self, _: &(), _: u32, _: &mut Vec<()>) {}
362 /// # }
363 /// let report = check(&Flag, &(), &[])?;
364 /// assert_eq!(report.missing()[0].root().arity(), 0);
365 /// # Ok::<(), match_lang::Error>(())
366 /// ```
367 #[must_use]
368 pub fn arity(&self) -> usize {
369 self.node().map_or(0, |n| n.arity as usize)
370 }
371
372 /// The fields under this node, in order.
373 ///
374 /// # Examples
375 ///
376 /// ```
377 /// # use match_lang::{check, Arm, Ctor, Model, Pat, Signature};
378 /// # struct Pair;
379 /// # impl Model for Pair {
380 /// # type Ty = bool;
381 /// # fn signature(&self, ty: &bool) -> Signature<bool> {
382 /// # if *ty { Signature::Product } else { Signature::Bool }
383 /// # }
384 /// # fn fields(&self, _: &bool, _: u32, out: &mut Vec<bool>) { out.extend([false, false]) }
385 /// # }
386 /// let arms = [Arm::new(Pat::product([Pat::bool(false), Pat::bool(false)]))];
387 /// let report = check(&Pair, &true, &arms)?;
388 /// let first = report.missing()[0].root().fields().next().unwrap();
389 /// assert_eq!(first.ctor(), Ctor::Bool(true));
390 /// # Ok::<(), match_lang::Error>(())
391 /// ```
392 #[must_use]
393 pub fn fields(&self) -> WitnessFields<'a, T> {
394 WitnessFields {
395 nodes: self.nodes,
396 next: self.pos.checked_sub(1),
397 remaining: self.arity(),
398 }
399 }
400
401 /// Prints this node with the model's variant names.
402 ///
403 /// # Examples
404 ///
405 /// ```
406 /// # use match_lang::{check, Arm, Model, Pat, Signature};
407 /// # struct Opt;
408 /// # impl Model for Opt {
409 /// # type Ty = u8;
410 /// # fn signature(&self, ty: &u8) -> Signature<u8> {
411 /// # if *ty == 0 { Signature::Sum { count: 2 } } else { Signature::Bool }
412 /// # }
413 /// # fn fields(&self, _: &u8, v: u32, out: &mut Vec<u8>) { if v == 1 { out.push(1) } }
414 /// # fn variant_name(&self, _: &u8, v: u32) -> Option<&str> {
415 /// # Some(if v == 0 { "None" } else { "Some" })
416 /// # }
417 /// # }
418 /// let report = check(&Opt, &0, &[Arm::new(Pat::variant(1, [Pat::wild()]))])?;
419 /// assert_eq!(report.missing()[0].root().display(&Opt).to_string(), "None");
420 /// # Ok::<(), match_lang::Error>(())
421 /// ```
422 pub fn display<M: Model<Ty = T>>(self, model: &'a M) -> WitnessDisplay<'a, M> {
423 WitnessDisplay {
424 witness: self,
425 model,
426 }
427 }
428
429 /// Writes the subtree, asking `name` for variant and product names.
430 fn write_with<'n>(
431 &self,
432 f: &mut fmt::Formatter<'_>,
433 name: impl Fn(&T, u32) -> Option<&'n str>,
434 ) -> fmt::Result {
435 enum Step<'a, T> {
436 Node(WitnessRef<'a, T>),
437 Text(&'static str),
438 }
439 let mut stack = Vec::new();
440 stack.push(Step::Node(*self));
441 let mut fields = Vec::new();
442 while let Some(step) = stack.pop() {
443 let node = match step {
444 Step::Text(text) => {
445 f.write_str(text)?;
446 continue;
447 }
448 Step::Node(node) => node,
449 };
450 let (open, close) = match node.ctor() {
451 Ctor::Wild | Ctor::Other => {
452 f.write_str("_")?;
453 continue;
454 }
455 Ctor::Bool(b) => {
456 write!(f, "{b}")?;
457 continue;
458 }
459 Ctor::Int { lo, hi } if lo == hi => {
460 write!(f, "{lo}")?;
461 continue;
462 }
463 Ctor::Int { lo, hi } => {
464 write!(f, "{lo}..={hi}")?;
465 continue;
466 }
467 Ctor::Char { lo, hi } if lo == hi => {
468 write!(f, "{lo:?}")?;
469 continue;
470 }
471 Ctor::Char { lo, hi } => {
472 write!(f, "{lo:?}..={hi:?}")?;
473 continue;
474 }
475 Ctor::Lit(id) => {
476 write!(f, "lit#{id}")?;
477 continue;
478 }
479 Ctor::Variant(index) => {
480 match name(node.ty(), index) {
481 Some(n) => f.write_str(n)?,
482 None => write!(f, "#{index}")?,
483 }
484 if node.arity() == 0 {
485 continue;
486 }
487 ("(", ")")
488 }
489 Ctor::Product => match name(node.ty(), 0) {
490 Some(n) => {
491 f.write_str(n)?;
492 if node.arity() == 0 {
493 continue;
494 }
495 ("(", ")")
496 }
497 None if node.arity() == 1 => ("(", ",)"),
498 None => ("(", ")"),
499 },
500 Ctor::Slice { .. } => ("[", "]"),
501 Ctor::SliceRest { prefix, .. } => {
502 f.write_str("[")?;
503 stack.push(Step::Text("]"));
504 fields.clear();
505 fields.extend(node.fields());
506 let split = (prefix as usize).min(fields.len());
507 let (pre, post) = fields.split_at(split);
508 for (i, field) in post.iter().enumerate().rev() {
509 stack.push(Step::Node(*field));
510 if i > 0 {
511 stack.push(Step::Text(", "));
512 }
513 }
514 stack.push(Step::Text(match (pre.is_empty(), post.is_empty()) {
515 (true, true) => "..",
516 (true, false) => ".., ",
517 (false, true) => ", ..",
518 (false, false) => ", .., ",
519 }));
520 for (i, field) in pre.iter().enumerate().rev() {
521 stack.push(Step::Node(*field));
522 if i > 0 {
523 stack.push(Step::Text(", "));
524 }
525 }
526 continue;
527 }
528 };
529 f.write_str(open)?;
530 stack.push(Step::Text(close));
531 fields.clear();
532 fields.extend(node.fields());
533 for (i, field) in fields.iter().enumerate().rev() {
534 stack.push(Step::Node(*field));
535 if i > 0 {
536 stack.push(Step::Text(", "));
537 }
538 }
539 }
540 Ok(())
541 }
542}
543
544impl<T> fmt::Display for WitnessRef<'_, T> {
545 /// Prints the subtree in a neutral syntax: `#i(..)` for variants, tuples
546 /// for products, `_` for wildcards and unnamed values.
547 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
548 self.write_with(f, |_, _| None)
549 }
550}
551
552impl<T> fmt::Debug for WitnessRef<'_, T> {
553 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
554 write!(f, "WitnessRef({self})")
555 }
556}
557
558/// The fields of a [`WitnessRef`], in order. Returned by
559/// [`WitnessRef::fields`].
560///
561/// # Examples
562///
563/// ```
564/// # use match_lang::{check, Arm, Model, Pat, Signature};
565/// # struct Pair;
566/// # impl Model for Pair {
567/// # type Ty = bool;
568/// # fn signature(&self, ty: &bool) -> Signature<bool> {
569/// # if *ty { Signature::Product } else { Signature::Bool }
570/// # }
571/// # fn fields(&self, _: &bool, _: u32, out: &mut Vec<bool>) { out.extend([false, false]) }
572/// # }
573/// let report = check(&Pair, &true, &[])?;
574/// assert_eq!(report.missing()[0].fields().len(), 2);
575/// # Ok::<(), match_lang::Error>(())
576/// ```
577pub struct WitnessFields<'a, T> {
578 nodes: &'a [WNode<T>],
579 /// Where the next field's subtree ends (its root).
580 next: Option<usize>,
581 remaining: usize,
582}
583
584impl<'a, T> Iterator for WitnessFields<'a, T> {
585 type Item = WitnessRef<'a, T>;
586
587 fn next(&mut self) -> Option<WitnessRef<'a, T>> {
588 if self.remaining == 0 {
589 return None;
590 }
591 let pos = self.next?;
592 let node = self.nodes.get(pos)?;
593 self.remaining -= 1;
594 // The next field's subtree ends just before this one starts.
595 self.next = pos.checked_sub(node.size as usize);
596 Some(WitnessRef {
597 nodes: self.nodes,
598 pos,
599 })
600 }
601
602 fn size_hint(&self) -> (usize, Option<usize>) {
603 (self.remaining, Some(self.remaining))
604 }
605}
606
607impl<T> ExactSizeIterator for WitnessFields<'_, T> {}
608
609impl<T> fmt::Debug for WitnessFields<'_, T> {
610 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
611 f.debug_struct("WitnessFields")
612 .field("remaining", &self.remaining)
613 .finish()
614 }
615}
616
617/// A witness printed with the model's variant names. Returned by
618/// [`Witness::display`] and [`WitnessRef::display`].
619///
620/// # Examples
621///
622/// ```
623/// # use match_lang::{check, Arm, Model, Pat, Signature};
624/// # struct Opt;
625/// # impl Model for Opt {
626/// # type Ty = u8;
627/// # fn signature(&self, ty: &u8) -> Signature<u8> {
628/// # if *ty == 0 { Signature::Sum { count: 2 } } else { Signature::Bool }
629/// # }
630/// # fn fields(&self, _: &u8, v: u32, out: &mut Vec<u8>) { if v == 1 { out.push(1) } }
631/// # fn variant_name(&self, _: &u8, v: u32) -> Option<&str> {
632/// # Some(if v == 0 { "None" } else { "Some" })
633/// # }
634/// # }
635/// let report = check(&Opt, &0, &[Arm::new(Pat::variant(0, []))])?;
636/// assert_eq!(format!("{}", report.missing()[0].display(&Opt)), "Some(_)");
637/// # Ok::<(), match_lang::Error>(())
638/// ```
639pub struct WitnessDisplay<'a, M: Model> {
640 witness: WitnessRef<'a, M::Ty>,
641 model: &'a M,
642}
643
644impl<M: Model> fmt::Display for WitnessDisplay<'_, M> {
645 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
646 self.witness
647 .write_with(f, |ty, variant| self.model.variant_name(ty, variant))
648 }
649}
650
651impl<M: Model> fmt::Debug for WitnessDisplay<'_, M> {
652 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
653 fmt::Display::fmt(self, f)
654 }
655}