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/// One rule: what it matches, what it produces, and what makes that sound.
66#[derive(Debug, Clone, PartialEq, Eq)]
67pub struct Rule {
68    /// The term to match, which is IR for a rewrite and IR for a lowering.
69    pub pattern: Term,
70    /// A condition on the match, which is where a rule that only holds for some constants says
71    /// so. It sits between the pattern and the replacement because it is part of deciding
72    /// whether the rule fires, not part of what firing produces.
73    pub guard: Option<Term>,
74    /// What to put in the matched term's place.
75    pub replacement: Term,
76    /// The bitvector claim relating the two, which is what `rucc-verify` discharges. It is not
77    /// optional, because a rule set that lets one rule through without a specification is a rule
78    /// set with an unverified rule in it.
79    pub spec: Term,
80    /// Why a proof at narrower widths is enough for this rule, when there is a reason to think
81    /// the solver will not manage the real one. A rule carrying this is not excused anything:
82    /// it is still asked at its own width first, and the clause only says what a person is
83    /// willing to sign for if the answer comes back as a shrug.
84    pub bounded: Option<String>,
85    /// The line the rule starts on.
86    pub line: u32,
87    /// The column the rule starts at.
88    pub column: u32,
89}
90
91impl fmt::Display for Rule {
92    /// Prints the rule back in the shape `spec/10-backend.md` writes it: one clause to a line,
93    /// with the continuation lines under the pattern.
94    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
95        writeln!(f, "(rule (lower {})", self.pattern)?;
96        if let Some(guard) = &self.guard {
97            writeln!(f, "      (if {guard})")?;
98        }
99        writeln!(f, "      {}", self.replacement)?;
100        match &self.bounded {
101            Some(why) => {
102                writeln!(f, "      (spec {})", self.spec)?;
103                write!(f, "      (bounded \"{why}\"))")
104            }
105            None => write!(f, "      (spec {}))", self.spec),
106        }
107    }
108}
rucc_rules/ast.rs

rucc_rules/
ast.rs
