lemma-engine 0.8.19

A language that means business.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109

use crate::evaluation::operations::{OperationResult, VetoType};
use crate::planning::semantics::{LiteralValue, MathematicalComputation, ValueKind};

pub fn mathematical_computation_preserves_quantity_magnitude(op: &MathematicalComputation) -> bool {
    matches!(
        op,
        MathematicalComputation::Abs
            | MathematicalComputation::Ceil
            | MathematicalComputation::Floor
            | MathematicalComputation::Round
    )
}

fn apply_decimal_magnitude_op(
    op: &MathematicalComputation,
    magnitude: rust_decimal::Decimal,
) -> rust_decimal::Decimal {
    match op {
        MathematicalComputation::Abs => magnitude.abs(),
        MathematicalComputation::Floor => magnitude.floor(),
        MathematicalComputation::Ceil => magnitude.ceil(),
        MathematicalComputation::Round => magnitude.round(),
        _ => unreachable!("BUG: non-magnitude-preserving op passed to apply_decimal_magnitude_op"),
    }
}

pub fn quantity_magnitude_math(
    op: &MathematicalComputation,
    value: &LiteralValue,
) -> OperationResult {
    debug_assert!(mathematical_computation_preserves_quantity_magnitude(op));

    let ValueKind::Quantity(canonical_magnitude, signature) = &value.value else {
        unreachable!("BUG: quantity_magnitude_math called with non-quantity value");
    };

    if signature.len() != 1 || signature[0].1 != 1 {
        return OperationResult::Veto(VetoType::computation(format!(
            "Cannot apply '{op}' to quantity with compound unit; convert with `as <unit>` first"
        )));
    }
    let unit_name = signature[0].0.clone();

    let unit_factor = value.lemma_type.quantity_unit_factor(&unit_name);
    let magnitude_in_unit =
        match crate::computation::rational::checked_div(canonical_magnitude, unit_factor) {
            Ok(magnitude) => magnitude,
            Err(failure) => {
                return OperationResult::Veto(VetoType::computation(failure.to_string()));
            }
        };

    let magnitude_decimal =
        match crate::computation::rational::commit_rational_to_decimal(&magnitude_in_unit) {
            Ok(decimal) => decimal,
            Err(_) => {
                return OperationResult::Veto(VetoType::computation(
                    "Mathematical operation requires a decimal-representable input",
                ));
            }
        };

    let rounded_decimal = apply_decimal_magnitude_op(op, magnitude_decimal);

    let rounded_rational = match crate::computation::rational::decimal_to_rational(rounded_decimal)
    {
        Ok(rational) => rational,
        Err(failure) => {
            return OperationResult::Veto(VetoType::computation(failure.to_string()));
        }
    };

    let new_canonical =
        match crate::computation::rational::checked_mul(&rounded_rational, unit_factor) {
            Ok(canonical) => canonical,
            Err(failure) => {
                return OperationResult::Veto(VetoType::computation(failure.to_string()));
            }
        };

    OperationResult::Value(LiteralValue::quantity_with_type(
        new_canonical,
        unit_name,
        value.lemma_type.clone(),
    ))
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::computation::rational::rational_new;
    use crate::planning::semantics::anonymous_quantity_type;
    use std::sync::Arc;

    #[test]
    fn compound_signature_vetoes() {
        let value = LiteralValue::quantity_with_signature(
            rational_new(100, 1),
            vec![("meter".to_string(), 1), ("second".to_string(), -1)],
            Arc::new(anonymous_quantity_type()),
        );
        let result = quantity_magnitude_math(&MathematicalComputation::Ceil, &value);
        assert!(
            result.vetoed(),
            "compound signature must veto, got {:?}",
            result
        );
    }
}