Skip to main content

implicit_predicates_gen/
differences.rs

1//! The difference form of a predicate: a graph whose leaves are differences
2//! of point coordinates.
3
4use crate::error::Error;
5use crate::graph::{Graph, Node, NodeId};
6use crate::parse::Position;
7
8/// One node of a [`DiffGraph`].
9#[derive(Clone, Copy, Debug, PartialEq, Eq)]
10pub enum DiffNode {
11    /// The difference `minuend.axis - subtrahend.axis` of one coordinate of
12    /// two different points, given as parameter indices.
13    Leaf {
14        /// Coordinate: 0, 1 and 2 are x, y and z.
15        axis: u8,
16        /// Index of the parameter whose coordinate is subtracted from.
17        minuend: usize,
18        /// Index of the parameter whose coordinate is subtracted.
19        subtrahend: usize,
20    },
21    /// Negation of a node, with the degree of its operand.
22    Neg(NodeId),
23    /// Sum of two nodes of the same degree.
24    Add(NodeId, NodeId),
25    /// Difference of two nodes of the same degree.
26    Sub(NodeId, NodeId),
27    /// Product of two nodes.
28    Mul(NodeId, NodeId),
29}
30
31/// An expression graph homogeneous in differences of point coordinates.
32///
33/// Children come before their parents. The graph is a faithful image of the
34/// source: `0 - x` becomes `Neg(x)`, and nothing is folded or reordered.
35#[derive(Clone, Debug, PartialEq, Eq)]
36pub struct DiffGraph {
37    /// The nodes, in dependency order.
38    pub nodes: Vec<DiffNode>,
39    /// The node holding the value of the whole expression.
40    pub root: NodeId,
41    /// Degree of each node: 1 for a leaf, the sum for a product, the common
42    /// degree for a sum or difference, and the degree of its operand for a
43    /// negation.
44    pub degrees: Vec<u32>,
45}
46
47impl DiffGraph {
48    /// The degree of the form in the differences of each axis, if the form
49    /// is multihomogeneous: every sum and difference combines nodes of the
50    /// same degree in x, in y and in z, so every term of the result has the
51    /// returned degrees. Returns `None` otherwise, as for a sum of squares
52    /// over the three axes.
53    ///
54    /// The test is on the graph as written: a form whose expansion is
55    /// multihomogeneous but that sums nodes of different degree vectors on
56    /// the way is reported as `None`, which only keeps it on the global
57    /// form of the filter bound.
58    pub fn axis_degrees(&self) -> Option<[u32; 3]> {
59        self.node_axis_degrees()?.get(self.root).copied()
60    }
61
62    /// The degree in each axis of every node, if the form is
63    /// multihomogeneous (see [`DiffGraph::axis_degrees`]).
64    pub(crate) fn node_axis_degrees(&self) -> Option<Vec<[u32; 3]>> {
65        let mut degrees: Vec<[u32; 3]> = Vec::with_capacity(self.nodes.len());
66        for node in &self.nodes {
67            let g = match *node {
68                DiffNode::Leaf { axis, .. } => {
69                    let mut g = [0; 3];
70                    *g.get_mut(usize::from(axis))? = 1;
71                    g
72                }
73                DiffNode::Neg(x) => *degrees.get(x)?,
74                DiffNode::Add(x, y) | DiffNode::Sub(x, y) => {
75                    let (gx, gy) = (*degrees.get(x)?, *degrees.get(y)?);
76                    if gx != gy {
77                        return None;
78                    }
79                    gx
80                }
81                DiffNode::Mul(x, y) => {
82                    let (gx, gy) = (*degrees.get(x)?, *degrees.get(y)?);
83                    // Each component is at most the total degree, which
84                    // `difference_graph` keeps within `u32`.
85                    [0, 1, 2].map(|k| gx[k].saturating_add(gy[k]))
86                }
87            };
88            degrees.push(g);
89        }
90        Some(degrees)
91    }
92}
93
94/// What a node of the source graph became.
95#[derive(Clone, Copy)]
96enum Mapped {
97    /// A coordinate, which is only allowed as an operand of a difference.
98    Coord { point: usize, axis: u8 },
99    /// An integer literal.
100    Literal(i64),
101    /// A node of the result.
102    Node(NodeId),
103}
104
105/// Rewrites `graph` over differences of coordinates, checking that every sum
106/// and difference combines nodes of the same degree.
107///
108/// A leaf is a difference of the same coordinate of two different points.
109/// A leaf used twice is one node; `a.x - d.x` and `d.x - a.x` are different
110/// leaves. A negation is `0 - x`, kept as a `Neg` node. The graph is walked
111/// iteratively in node order.
112///
113/// # Errors
114///
115/// Returns an error, at `position` (the name of the predicate), when a
116/// coordinate is used outside a difference, a difference mixes axes or
117/// subtracts a point from itself, a sum or difference combines nodes of
118/// different degree, a degree exceeds `u32::MAX`, or an integer literal
119/// appears other than as the zero of a negation.
120pub fn difference_graph(graph: &Graph, file: &str, position: Position) -> Result<DiffGraph, Error> {
121    let fail = |message: String| Error {
122        file: file.to_string(),
123        line: position.line,
124        column: position.column,
125        message,
126    };
127    let mut out = DiffGraph {
128        nodes: Vec::new(),
129        root: 0,
130        degrees: Vec::new(),
131    };
132    let mut mapped: Vec<Mapped> = Vec::with_capacity(graph.nodes.len());
133    for node in &graph.nodes {
134        let value = match *node {
135            Node::Coord { point, axis } => Mapped::Coord { point, axis },
136            Node::Int(n) => Mapped::Literal(n),
137            Node::Sub(x, y) => match (mapped[x], mapped[y]) {
138                (Mapped::Coord { point: p, axis: i }, Mapped::Coord { point: q, axis: j }) => {
139                    if i != j {
140                        return Err(fail(format!(
141                            "a difference of coordinates must use one axis, found {} and {}",
142                            coordinate(p, i),
143                            coordinate(q, j)
144                        )));
145                    }
146                    if p == q {
147                        return Err(fail(format!(
148                            "a difference of {} with itself is always zero",
149                            coordinate(p, i)
150                        )));
151                    }
152                    Mapped::Node(push(
153                        &mut out,
154                        DiffNode::Leaf {
155                            axis: i,
156                            minuend: p,
157                            subtrahend: q,
158                        },
159                        1,
160                    ))
161                }
162                (Mapped::Literal(0), Mapped::Node(id)) => {
163                    let degree = out.degrees[id];
164                    Mapped::Node(push(&mut out, DiffNode::Neg(id), degree))
165                }
166                (Mapped::Literal(0), operand) => return Err(fail(operand_problem(operand))),
167                (x, y) => combine(&mut out, DiffNode::Sub, x, y, &fail)?,
168            },
169            Node::Add(x, y) => combine(&mut out, DiffNode::Add, mapped[x], mapped[y], &fail)?,
170            Node::Mul(x, y) => combine(&mut out, DiffNode::Mul, mapped[x], mapped[y], &fail)?,
171        };
172        mapped.push(value);
173    }
174    match mapped[graph.root] {
175        Mapped::Node(root) => {
176            out.root = root;
177            Ok(out)
178        }
179        other => Err(fail(operand_problem(other))),
180    }
181}
182
183/// Adds the sum, difference or product of two operands to `out`.
184fn combine(
185    out: &mut DiffGraph,
186    make: fn(NodeId, NodeId) -> DiffNode,
187    x: Mapped,
188    y: Mapped,
189    fail: &dyn Fn(String) -> Error,
190) -> Result<Mapped, Error> {
191    let (Mapped::Node(x), Mapped::Node(y)) = (x, y) else {
192        let bad = if matches!(x, Mapped::Node(_)) { y } else { x };
193        return Err(fail(operand_problem(bad)));
194    };
195    let (gx, gy) = (out.degrees[x], out.degrees[y]);
196    let node = make(x, y);
197    let degree = if matches!(node, DiffNode::Mul(..)) {
198        gx.checked_add(gy).ok_or_else(|| {
199            fail(format!(
200                "a product has a degree in the differences above {}",
201                u32::MAX
202            ))
203        })?
204    } else if gx == gy {
205        gx
206    } else {
207        return Err(fail(format!(
208            "a sum or difference combines terms of degree {gx} and {gy} in the differences"
209        )));
210    };
211    Ok(Mapped::Node(push(out, node, degree)))
212}
213
214fn push(out: &mut DiffGraph, node: DiffNode, degree: u32) -> NodeId {
215    out.nodes.push(node);
216    out.degrees.push(degree);
217    out.nodes.len() - 1
218}
219
220fn operand_problem(bad: Mapped) -> String {
221    match bad {
222        Mapped::Coord { point, axis } => format!(
223            "the coordinate {} is used outside a difference of coordinates",
224            coordinate(point, axis)
225        ),
226        Mapped::Literal(n) => format!(
227            "the integer literal {n} is not allowed in the main form, \
228             except as the zero of a negation"
229        ),
230        Mapped::Node(_) => unreachable!("only coordinates and literals are problems"),
231    }
232}
233
234fn coordinate(point: usize, axis: u8) -> String {
235    format!("`point {point}`.{}", ["x", "y", "z"][usize::from(axis)])
236}