logicaffeine_compile/semantics/
exact.rs

1//! The exact real types in the interpreter's value model: real algebraic numbers, computable reals,
2//! the program's infinitesimal and the hyperreals it generates, infinite integers, ordinals, and
3//! the values a supertask leaves.
4//!
5//! How they mix with the numeric tower and with each other is decided once, in
6//! [`logicaffeine_base::tower`], generic over a value model; this module is where `RuntimeValue`
7//! joins it, so the tree-walker and the VM compute exactly what a compiled program computes.
8
9use std::cell::RefCell;
10use std::rc::Rc;
11use std::sync::Arc;
12
13use logicaffeine_base::algebraic::Algebraic;
14use logicaffeine_base::exact_real::ExactReal;
15use logicaffeine_base::germ::Germ;
16use logicaffeine_base::hypernatural::Hypernatural;
17use logicaffeine_base::hyperreal::Hyperreal;
18use logicaffeine_base::limit_value::{Converging, Depends, LimitRule};
19use logicaffeine_base::numeric::{rational_from_f64_exact, BigInt, Rational};
20use logicaffeine_base::ordinal::Ordinal;
21use logicaffeine_base::tower::{self, ExactRef, Shape, TowerValue, ValueAlgebra};
22
23pub use logicaffeine_base::tower::{Branch, HyperForm, HyperValue, NaturalValue, Op, Rel, Rounding, Scale};
24
25use crate::ast::stmt::BinaryOpKind;
26use crate::interpreter::{ListRepr, RuntimeValue};
27use crate::semantics::builtins::{call_builtin, BuiltinId};
28
29/// A runtime value that depends on the residue of `⌈1/dt⌉`.
30pub type DependsValue = tower::DependsValue<RuntimeValue>;
31
32/// The canonical runtime value of an algebraic number: a rational is an `Int`/`BigInt`/`Rational`.
33pub fn from_algebraic(a: Algebraic) -> RuntimeValue {
34    tower::from_algebraic(a)
35}
36
37/// The canonical runtime value of a computable real: an algebraic one is an algebraic number.
38pub fn from_exact_real(x: ExactReal) -> RuntimeValue {
39    tower::from_exact_real(x)
40}
41
42/// The canonical runtime value of a hyperreal.
43pub fn from_hyper(value: Hyperreal, scale: &Arc<Scale>) -> RuntimeValue {
44    tower::from_hyper(value, scale)
45}
46
47/// The canonical runtime value of a germ.
48pub fn from_germ(g: Germ, scale: &Arc<Scale>) -> RuntimeValue {
49    tower::from_germ(g, scale)
50}
51
52/// The canonical runtime value of an infinite integer.
53pub fn from_natural(value: Hypernatural, scale: &Arc<Scale>) -> RuntimeValue {
54    tower::from_natural(value, scale)
55}
56
57/// The canonical runtime value of a residue-dependent value.
58pub fn from_depends(value: Depends<Branch<RuntimeValue>>, scale: &Arc<Scale>) -> RuntimeValue {
59    tower::from_depends(value, scale)
60}
61
62/// A finite ordinal is a natural number.
63pub fn from_ordinal(o: Ordinal) -> RuntimeValue {
64    tower::from_ordinal(o)
65}
66
67/// True for a value of one of the exact types.
68pub fn is_exact_value(v: &RuntimeValue) -> bool {
69    tower::is_exact_value(v)
70}
71
72/// Apply `op` when either operand is an exact type; `None` when neither is.
73pub fn arith(
74    op: Op,
75    left: &RuntimeValue,
76    right: &RuntimeValue,
77    recurse: &dyn Fn(Op, RuntimeValue, RuntimeValue) -> Result<RuntimeValue, String>,
78) -> Option<Result<RuntimeValue, String>> {
79    tower::arith(op, left, right, recurse)
80}
81
82/// A number as a germ, or `None`.
83pub fn germ_of(v: &RuntimeValue) -> Option<Germ> {
84    tower::germ_of(v)
85}
86
87/// Apply `rel` when either operand is an exact type; `None` when neither is.
88pub fn relation(
89    rel: Rel,
90    left: &RuntimeValue,
91    right: &RuntimeValue,
92    recurse: &dyn Fn(Rel, RuntimeValue, RuntimeValue) -> Result<RuntimeValue, String>,
93) -> Option<Result<RuntimeValue, String>> {
94    tower::relation(rel, left, right, recurse)
95}
96
97/// Structural equality for collections and hashing; `None` when neither value is exact.
98pub fn structurally_equal(left: &RuntimeValue, right: &RuntimeValue) -> Option<bool> {
99    tower::structurally_equal(left, right)
100}
101
102/// How an exact value prints.
103pub fn display(v: &RuntimeValue) -> Option<String> {
104    tower::display(v)
105}
106
107/// The standard part of a limited value.
108pub fn standard_part(v: &RuntimeValue) -> Result<RuntimeValue, String> {
109    tower::standard_part(v)
110}
111
112/// The integer part of an exact value under `mode`; `None` when `v` is not one.
113pub fn integer_part(
114    v: &RuntimeValue,
115    mode: Rounding,
116    recurse: &dyn Fn(RuntimeValue) -> Result<RuntimeValue, String>,
117) -> Option<Result<RuntimeValue, String>> {
118    tower::integer_part(v, mode, recurse)
119}
120
121/// `x ≈ 0`: zero or an infinitesimal.
122pub fn is_infinitesimal(v: &RuntimeValue) -> Result<RuntimeValue, String> {
123    tower::is_infinitesimal(v)
124}
125
126/// Bounded by a standard number.
127pub fn is_limited(v: &RuntimeValue) -> Result<RuntimeValue, String> {
128    tower::is_limited(v)
129}
130
131/// The program's infinitesimal, its reciprocal's residues modulo `modulus` limited to `allowed`.
132pub fn new_infinitesimal(name: &str, modulus: u64, allowed: &[u64]) -> Result<RuntimeValue, String> {
133    tower::new_infinitesimal(name, modulus, allowed)
134}
135
136/// An infinitesimal declared much smaller than `larger` and much larger than `smaller`, each an
137/// infinitesimal or `nothing`.
138pub fn new_ordered_infinitesimal(
139    name: &str,
140    larger: &RuntimeValue,
141    smaller: &RuntimeValue,
142    modulus: u64,
143    allowed: &[u64],
144) -> Result<RuntimeValue, String> {
145    tower::new_ordered_infinitesimal(name, larger, smaller, modulus, allowed)
146}
147
148/// The infinite natural `⌈1/dt⌉` generated by an infinitesimal value.
149pub fn generator_of(v: &RuntimeValue) -> Result<RuntimeValue, String> {
150    tower::generator_of(v)
151}
152
153/// A limit rule by its English name.
154pub fn limit_rule(name: &str) -> Result<LimitRule, String> {
155    tower::limit_rule(name)
156}
157
158/// Resolve a residue-dependent value under a limit rule.
159pub fn apply_limit(v: &RuntimeValue, rule: LimitRule) -> Result<RuntimeValue, String> {
160    tower::apply_limit(v, rule)
161}
162
163/// A provisional answer: the current guess after `steps` cases with `revisions` changes.
164pub fn provisional(value: RuntimeValue, steps: u64, revisions: u64) -> RuntimeValue {
165    tower::provisional(value, steps, revisions)
166}
167
168/// Why a value cannot decide a branch, or `None`.
169pub fn undecided_branch(v: &RuntimeValue) -> Option<String> {
170    tower::undecided_branch(v)
171}
172
173/// `not` lifted over residue branches and through provisional values; `None` for any other value.
174pub fn not(
175    v: &RuntimeValue,
176    recurse: &dyn Fn(RuntimeValue) -> Result<RuntimeValue, String>,
177) -> Option<Result<RuntimeValue, String>> {
178    tower::not(v, recurse)
179}
180
181/// An algebraic number, computable real or ordinal as its kind and canonical bytes.
182pub fn exact_bytes(v: &RuntimeValue) -> Option<(u8, Vec<u8>)> {
183    tower::exact_bytes(v)
184}
185
186/// The value [`exact_bytes`] wrote; `None` for a forged or non-canonical encoding.
187pub fn from_exact_bytes(kind: u8, bytes: &[u8]) -> Option<RuntimeValue> {
188    tower::from_exact_bytes(kind, bytes)
189}
190
191/// The infinitesimal's name and its reciprocal's residue facts.
192pub fn scale_parts(scale: &Scale) -> (String, Vec<u8>) {
193    tower::scale_parts(scale)
194}
195
196/// The scale [`scale_parts`] wrote.
197pub fn scale_from_parts(name: &str, residues: &[u8]) -> Option<Arc<Scale>> {
198    tower::scale_from_parts(name, residues)
199}
200
201/// A hyperreal, infinite integer or germ as its kind, scale and canonical bytes.
202pub fn scaled_bytes(v: &RuntimeValue) -> Option<(u8, String, Vec<u8>, Vec<u8>)> {
203    tower::scaled_bytes(v)
204}
205
206/// The value [`scaled_bytes`] wrote; `None` for a forged or non-canonical encoding.
207pub fn from_scaled_bytes(kind: u8, name: &str, residues: &[u8], bytes: &[u8]) -> Option<RuntimeValue> {
208    tower::from_scaled_bytes(kind, name, residues, bytes)
209}
210
211/// A residue-dependent value rebuilt from its scale, modulus and per-class values.
212pub fn depends_from_parts(
213    name: &str,
214    residues: &[u8],
215    modulus: u64,
216    branches: Vec<Option<RuntimeValue>>,
217) -> Option<RuntimeValue> {
218    tower::depends_from_parts(name, residues, modulus, branches)
219}
220
221impl TowerValue for RuntimeValue {
222    fn exact(&self) -> Option<ExactRef<'_, Self>> {
223        Some(match self {
224            RuntimeValue::Algebraic(a) => ExactRef::Algebraic(a),
225            RuntimeValue::ExactReal(x) => ExactRef::Real(x),
226            RuntimeValue::Hyperreal(h) => ExactRef::Hyper(h),
227            RuntimeValue::Hypernatural(n) => ExactRef::Natural(n),
228            RuntimeValue::Ordinal(o) => ExactRef::Ordinal(o),
229            RuntimeValue::Depends(d) => ExactRef::Depends(d),
230            RuntimeValue::Converging(c) => ExactRef::Converging(c),
231            _ => return None,
232        })
233    }
234
235    fn standard_rational(&self) -> Option<Rational> {
236        match self {
237            RuntimeValue::Int(n) => Some(Rational::from_i64(*n)),
238            RuntimeValue::BigInt(b) => Some(Rational::from_bigint((**b).clone())),
239            RuntimeValue::Rational(r) => Some((**r).clone()),
240            RuntimeValue::Decimal(d) => Some(d.to_rational()),
241            RuntimeValue::Float(f) => rational_from_f64_exact(*f),
242            _ => None,
243        }
244    }
245
246    fn integer(&self) -> Option<BigInt> {
247        match self {
248            RuntimeValue::Int(n) => Some(BigInt::from_i64(*n)),
249            RuntimeValue::BigInt(b) => Some((**b).clone()),
250            _ => None,
251        }
252    }
253
254    fn exact_rational(&self) -> Option<Rational> {
255        match self {
256            RuntimeValue::Int(n) => Some(Rational::from_i64(*n)),
257            RuntimeValue::BigInt(b) => Some(Rational::from_bigint((**b).clone())),
258            RuntimeValue::Rational(r) => Some((**r).clone()),
259            _ => None,
260        }
261    }
262
263    fn is_standard_number(&self) -> bool {
264        matches!(
265            self,
266            RuntimeValue::Int(_)
267                | RuntimeValue::BigInt(_)
268                | RuntimeValue::Rational(_)
269                | RuntimeValue::Decimal(_)
270                | RuntimeValue::Float(_)
271        )
272    }
273
274    fn text(&self) -> Option<&str> {
275        match self {
276            RuntimeValue::Text(t) => Some(t.as_str()),
277            _ => None,
278        }
279    }
280
281    fn type_name(&self) -> String {
282        RuntimeValue::type_name(self).to_string()
283    }
284
285    fn display_string(&self) -> String {
286        self.to_display_string()
287    }
288
289    fn values_equal(&self, other: &Self) -> bool {
290        super::compare::values_equal(self, other)
291    }
292
293    fn is_nothing(&self) -> bool {
294        matches!(self, RuntimeValue::Nothing)
295    }
296
297    fn from_rational(r: Rational) -> Self {
298        RuntimeValue::from_rational(r)
299    }
300
301    fn from_bigint(b: BigInt) -> Self {
302        RuntimeValue::from_bigint(b)
303    }
304
305    fn boolean(b: bool) -> Self {
306        RuntimeValue::Bool(b)
307    }
308
309    fn nothing() -> Self {
310        RuntimeValue::Nothing
311    }
312
313    fn algebraic(a: Algebraic) -> Self {
314        RuntimeValue::Algebraic(Rc::new(a))
315    }
316
317    fn exact_real(x: ExactReal) -> Self {
318        RuntimeValue::ExactReal(Rc::new(x))
319    }
320
321    fn hyper(h: HyperValue) -> Self {
322        RuntimeValue::Hyperreal(Rc::new(h))
323    }
324
325    fn natural(n: NaturalValue) -> Self {
326        RuntimeValue::Hypernatural(Rc::new(n))
327    }
328
329    fn ordinal(o: Ordinal) -> Self {
330        RuntimeValue::Ordinal(Rc::new(o))
331    }
332
333    fn depends(d: DependsValue) -> Self {
334        RuntimeValue::Depends(Rc::new(d))
335    }
336
337    fn converging(c: Converging<Self>) -> Self {
338        RuntimeValue::Converging(Rc::new(c))
339    }
340}
341
342impl ValueAlgebra for RuntimeValue {
343    fn add(a: Self, b: Self) -> Result<Self, String> {
344        super::arith::add(a, b)
345    }
346
347    fn subtract(a: Self, b: Self) -> Result<Self, String> {
348        super::arith::subtract(a, b)
349    }
350
351    fn multiply(a: Self, b: Self) -> Result<Self, String> {
352        super::arith::multiply(a, b)
353    }
354
355    fn exact_divide(a: Self, b: Self) -> Result<Self, String> {
356        super::arith::exact_divide(a, b)
357    }
358
359    fn modulo(a: Self, b: Self) -> Result<Self, String> {
360        super::arith::modulo(a, b)
361    }
362
363    fn power(a: Self, b: Self) -> Result<Self, String> {
364        super::arith::power(a, b)
365    }
366
367    fn holds(rel: Rel, a: &Self, b: &Self) -> Result<bool, String> {
368        let op = match rel {
369            Rel::Lt => BinaryOpKind::Lt,
370            Rel::Gt => BinaryOpKind::Gt,
371            Rel::LtEq => BinaryOpKind::LtEq,
372            Rel::GtEq => BinaryOpKind::GtEq,
373            Rel::Eq => BinaryOpKind::Eq,
374            Rel::NotEq => BinaryOpKind::NotEq,
375        };
376        super::arith::binary_op(op, a.clone(), b.clone())?.decided_truth()
377    }
378
379    fn floor(v: Self) -> Result<Self, String> {
380        call_builtin(BuiltinId::Floor, vec![v])
381    }
382
383    fn ceil(v: Self) -> Result<Self, String> {
384        call_builtin(BuiltinId::Ceil, vec![v])
385    }
386
387    fn list(values: Vec<Self>) -> Self {
388        RuntimeValue::List(Rc::new(RefCell::new(ListRepr::from_values(values))))
389    }
390
391    fn shape(&self) -> Shape<Self> {
392        match self {
393            RuntimeValue::Bool(_) => Shape::Bool,
394            RuntimeValue::Int(n) => Shape::Int(*n),
395            RuntimeValue::Float(_) => Shape::Float,
396            RuntimeValue::BigInt(b) => Shape::BigInt((**b).clone()),
397            RuntimeValue::Rational(r) => Shape::Rational((**r).clone()),
398            RuntimeValue::Decimal(_) => Shape::Decimal,
399            RuntimeValue::Text(t) => Shape::Text(t.len()),
400            RuntimeValue::List(l) => Shape::List(l.borrow().to_values()),
401            RuntimeValue::Tuple(items) => Shape::Tuple(items.to_vec()),
402            _ => Shape::Other,
403        }
404    }
405}
406
407#[cfg(test)]
408#[path = "../../../logicaffeine_tests/unit/logicaffeine_compile/semantics/exact/tests.rs"]
409mod tests;
logicaffeine_compile/semantics/exact.rs

logicaffeine_compile/semantics/
exact.rs
