rucc_rules/
ast.rs

1//! What a rule is, once it has been read.
2
3use std::fmt;
4
5/// A term: the pattern a rule matches, the replacement it produces, and the two clauses that
6/// constrain it are all one shape.
7#[derive(Debug, Clone, PartialEq, Eq)]
8pub struct Term {
9    /// Which of the three kinds this is.
10    pub kind: TermKind,
11    /// The line it starts on, counted from one.
12    pub line: u32,
13    /// The column it starts at, counted from one.
14    pub column: u32,
15}
16
17/// The three kinds of term.
18#[derive(Debug, Clone, PartialEq, Eq)]
19pub enum TermKind {
20    /// A name standing for whatever the pattern bound it to.
21    Var(String),
22    /// A literal.
23    Int(i128),
24    /// A head applied to arguments, which is every opcode, every constructor and every operator
25    /// in a specification.
26    App {
27        /// The name in head position.
28        head: String,
29        /// What it is applied to, possibly nothing, as in `(result)`.
30        args: Vec<Term>,
31    },
32}
33
34impl Term {
35    /// Walk this term and everything under it, outermost first.
36    ///
37    /// The lifetime is written out so that what the visitor is handed lives as long as the term
38    /// does, which is what lets a caller collect the places it found rather than only count them.
39    pub fn walk<'t>(&'t self, visit: &mut impl FnMut(&'t Term)) {
40        visit(self);
41        if let TermKind::App { args, .. } = &self.kind {
42            for arg in args {
43                arg.walk(visit);
44            }
45        }
46    }
47}
48
49impl fmt::Display for Term {
50    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
51        match &self.kind {
52            TermKind::Var(name) => f.write_str(name),
53            TermKind::Int(value) => write!(f, "{value}"),
54            TermKind::App { head, args } => {
55                write!(f, "({head}")?;
56                for arg in args {
57                    write!(f, " {arg}")?;
58                }
59                f.write_str(")")
60            }
61        }
62    }
63}
64
65/// What a rule rewrites into.
66///
67/// The two kinds are matched by the same trie and verified by the same obligation, and the only
68/// thing that separates them is what the replacement is written in. Keeping them one language
69/// rather than two is the whole reason `spec/09-optimizer.md` section 9.3 and
70/// `spec/10-backend.md` section 10.2 ask for a rule DSL at all, because a rewrite and a
71/// lowering are the same claim about two terms and there is no reason to say it twice.
72#[derive(Debug, Clone, Copy, PartialEq, Eq)]
73pub enum RuleKind {
74    /// IR to IR. The replacement is IR, so a rewrite can be applied over and over and the
75    /// result is still something later rules match. `spec/optimizer/13-rewrite-rules.md`.
76    Simplify,
77    /// IR to machine. The replacement is a machine term, so a lowering is the last thing that
78    /// happens to a value and nothing matches what it produces. `spec/10-backend.md`.
79    Lower,
80}
81
82impl RuleKind {
83    /// The keyword that introduces a rule of this kind.
84    #[must_use]
85    pub const fn as_str(self) -> &'static str {
86        match self {
87            Self::Simplify => "simplify",
88            Self::Lower => "lower",
89        }
90    }
91}
92
93impl fmt::Display for RuleKind {
94    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
95        f.write_str(self.as_str())
96    }
97}
98
99/// One rule: what it matches, what it produces, and what makes that sound.
100#[derive(Debug, Clone, PartialEq, Eq)]
101pub struct Rule {
102    /// Whether the replacement is IR or a machine term.
103    pub kind: RuleKind,
104    /// The term to match, which is IR for a rewrite and IR for a lowering.
105    pub pattern: Term,
106    /// A condition on the match, which is where a rule that only holds for some constants says
107    /// so. It sits between the pattern and the replacement because it is part of deciding
108    /// whether the rule fires, not part of what firing produces.
109    pub guard: Option<Term>,
110    /// What to put in the matched term's place.
111    pub replacement: Term,
112    /// The bitvector claim relating the two, which is what `rucc-verify` discharges. It is not
113    /// optional, because a rule set that lets one rule through without a specification is a rule
114    /// set with an unverified rule in it.
115    pub spec: Term,
116    /// Why a proof at narrower widths is enough for this rule, when there is a reason to think
117    /// the solver will not manage the real one. A rule carrying this is not excused anything:
118    /// it is still asked at its own width first, and the clause only says what a person is
119    /// willing to sign for if the answer comes back as a shrug.
120    pub bounded: Option<String>,
121    /// The line the rule starts on.
122    pub line: u32,
123    /// The column the rule starts at.
124    pub column: u32,
125}
126
127impl fmt::Display for Rule {
128    /// Prints the rule back in the shape `spec/10-backend.md` writes it: one clause to a line,
129    /// with the continuation lines under the pattern.
130    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
131        writeln!(f, "(rule ({} {})", self.kind, self.pattern)?;
132        if let Some(guard) = &self.guard {
133            writeln!(f, "      (if {guard})")?;
134        }
135        writeln!(f, "      {}", self.replacement)?;
136        match &self.bounded {
137            Some(why) => {
138                writeln!(f, "      (spec {})", self.spec)?;
139                write!(f, "      (bounded \"{why}\"))")
140            }
141            None => write!(f, "      (spec {}))", self.spec),
142        }
143    }
144}
rucc_rules/ast.rs

rucc_rules/
ast.rs
