conjure_cp_core/ast/
categories.rs

1use std::fmt::Display;
2
3use serde::{Deserialize, Serialize};
4
5/// The *category* of a term describes the kind of symbols it contains.
6///
7/// Categories have a strict order: constant < parameter < quantifying variable < decision
8/// variable.
9#[derive(Copy, Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Serialize, Deserialize, Hash)]
10pub enum Category {
11    /// This term does not have a category in isolation - e.g. a record field declaration
12    Bottom = 0,
13    /// This term contains constants and lettings
14    Constant = 1,
15    /// This term contains parameters / givens
16    Parameter = 2,
17    /// This term contains quantified variables / induction variables
18    Quantified = 3,
19    /// This term contains decision variables
20    Decision = 4,
21}
22
23impl Display for Category {
24    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
25        match self {
26            Category::Bottom => write!(f, "_|_"),
27            Category::Constant => write!(f, "constant"),
28            Category::Parameter => write!(f, "parameter"),
29            Category::Quantified => write!(f, "quantified"),
30            Category::Decision => write!(f, "decision"),
31        }
32    }
33}
34
35/// A type with a [`Category`]
36pub trait CategoryOf {
37    /// Gets the [`Category`] of a term.
38    fn category_of(&self) -> Category;
39}
conjure_cp_core/ast/categories.rs

conjure_cp_core/ast/
categories.rs
