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
47/// What a node of the source graph became.
48#[derive(Clone, Copy)]
49enum Mapped {
50    /// A coordinate, which is only allowed as an operand of a difference.
51    Coord { point: usize, axis: u8 },
52    /// An integer literal.
53    Literal(i64),
54    /// A node of the result.
55    Node(NodeId),
56}
57
58/// Rewrites `graph` over differences of coordinates, checking that every sum
59/// and difference combines nodes of the same degree.
60///
61/// A leaf is a difference of the same coordinate of two different points.
62/// A leaf used twice is one node; `a.x - d.x` and `d.x - a.x` are different
63/// leaves. A negation is `0 - x`, kept as a `Neg` node. The graph is walked
64/// iteratively in node order.
65///
66/// # Errors
67///
68/// Returns an error, at `position` (the name of the predicate), when a
69/// coordinate is used outside a difference, a difference mixes axes or
70/// subtracts a point from itself, a sum or difference combines nodes of
71/// different degree, a degree exceeds `u32::MAX`, or an integer literal
72/// appears other than as the zero of a negation.
73pub fn difference_graph(graph: &Graph, file: &str, position: Position) -> Result<DiffGraph, Error> {
74    let fail = |message: String| Error {
75        file: file.to_string(),
76        line: position.line,
77        column: position.column,
78        message,
79    };
80    let mut out = DiffGraph {
81        nodes: Vec::new(),
82        root: 0,
83        degrees: Vec::new(),
84    };
85    let mut mapped: Vec<Mapped> = Vec::with_capacity(graph.nodes.len());
86    for node in &graph.nodes {
87        let value = match *node {
88            Node::Coord { point, axis } => Mapped::Coord { point, axis },
89            Node::Int(n) => Mapped::Literal(n),
90            Node::Sub(x, y) => match (mapped[x], mapped[y]) {
91                (Mapped::Coord { point: p, axis: i }, Mapped::Coord { point: q, axis: j }) => {
92                    if i != j {
93                        return Err(fail(format!(
94                            "a difference of coordinates must use one axis, found {} and {}",
95                            coordinate(p, i),
96                            coordinate(q, j)
97                        )));
98                    }
99                    if p == q {
100                        return Err(fail(format!(
101                            "a difference of {} with itself is always zero",
102                            coordinate(p, i)
103                        )));
104                    }
105                    Mapped::Node(push(
106                        &mut out,
107                        DiffNode::Leaf {
108                            axis: i,
109                            minuend: p,
110                            subtrahend: q,
111                        },
112                        1,
113                    ))
114                }
115                (Mapped::Literal(0), Mapped::Node(id)) => {
116                    let degree = out.degrees[id];
117                    Mapped::Node(push(&mut out, DiffNode::Neg(id), degree))
118                }
119                (Mapped::Literal(0), operand) => return Err(fail(operand_problem(operand))),
120                (x, y) => combine(&mut out, DiffNode::Sub, x, y, &fail)?,
121            },
122            Node::Add(x, y) => combine(&mut out, DiffNode::Add, mapped[x], mapped[y], &fail)?,
123            Node::Mul(x, y) => combine(&mut out, DiffNode::Mul, mapped[x], mapped[y], &fail)?,
124        };
125        mapped.push(value);
126    }
127    match mapped[graph.root] {
128        Mapped::Node(root) => {
129            out.root = root;
130            Ok(out)
131        }
132        other => Err(fail(operand_problem(other))),
133    }
134}
135
136/// Adds the sum, difference or product of two operands to `out`.
137fn combine(
138    out: &mut DiffGraph,
139    make: fn(NodeId, NodeId) -> DiffNode,
140    x: Mapped,
141    y: Mapped,
142    fail: &dyn Fn(String) -> Error,
143) -> Result<Mapped, Error> {
144    let (Mapped::Node(x), Mapped::Node(y)) = (x, y) else {
145        let bad = if matches!(x, Mapped::Node(_)) { y } else { x };
146        return Err(fail(operand_problem(bad)));
147    };
148    let (gx, gy) = (out.degrees[x], out.degrees[y]);
149    let node = make(x, y);
150    let degree = if matches!(node, DiffNode::Mul(..)) {
151        gx.checked_add(gy).ok_or_else(|| {
152            fail(format!(
153                "a product has a degree in the differences above {}",
154                u32::MAX
155            ))
156        })?
157    } else if gx == gy {
158        gx
159    } else {
160        return Err(fail(format!(
161            "a sum or difference combines terms of degree {gx} and {gy} in the differences"
162        )));
163    };
164    Ok(Mapped::Node(push(out, node, degree)))
165}
166
167fn push(out: &mut DiffGraph, node: DiffNode, degree: u32) -> NodeId {
168    out.nodes.push(node);
169    out.degrees.push(degree);
170    out.nodes.len() - 1
171}
172
173fn operand_problem(bad: Mapped) -> String {
174    match bad {
175        Mapped::Coord { point, axis } => format!(
176            "the coordinate {} is used outside a difference of coordinates",
177            coordinate(point, axis)
178        ),
179        Mapped::Literal(n) => format!(
180            "the integer literal {n} is not allowed in the main form, \
181             except as the zero of a negation"
182        ),
183        Mapped::Node(_) => unreachable!("only coordinates and literals are problems"),
184    }
185}
186
187fn coordinate(point: usize, axis: u8) -> String {
188    format!("`point {point}`.{}", ["x", "y", "z"][usize::from(axis)])
189}