logicaffeine_base/
extension.rs

1//! The builtins of the exact extension, read and run once for every value model. A program calls
2//! them by name (`infinitesimal`, `standardPart`, `tripCount`, …), the declarations and the
3//! supertask engine's resolved loops call them too, and the interpreter and a compiled program
4//! both answer through [`call`], so a builtin computes the same value and refuses in the same
5//! words on every tier.
6
7use crate::numeric::BigInt;
8use crate::supertask;
9use crate::tower::{self, ValueAlgebra};
10
11/// A builtin of the exact extension.
12#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
13pub enum Builtin {
14    /// `infinitesimal(name, modulus, allowed…)`: a fresh infinitesimal whose reciprocal's residue
15    /// modulo `modulus` is one of `allowed`.
16    Infinitesimal,
17    /// `standardPart(x[, at])`, `isInfinitesimal(x[, at])`, `isLimited(x[, at])`,
18    /// `infinitelyClose(x, y[, at])`: the standard part and the predicates, relative to the infinitesimal
19    /// `at` when it is given.
20    StandardPart,
21    IsInfinitesimal,
22    IsLimited,
23    InfinitelyClose,
24    /// The infinite integer `1/dt` an infinitesimal generates.
25    GeneratorOf,
26    /// A value read under a named limit rule.
27    LimitOf,
28    /// A search's answer with its evidence: the steps it took and the revisions it made.
29    Provisional,
30    /// The statement `At the limit, take …`: names a rule, answers nothing.
31    AtTheLimit,
32    TripCount,
33    AffinePower,
34    PolynomialFlow,
35    CycleAt,
36    SearchCandidates,
37    StateSize,
38    /// A search over every natural that reached a run unresolved.
39    EveryNatural,
40    /// The exact square root, exponential and natural logarithm, which `sqrt`, `exp` and `ln` are in
41    /// a context that declares an exact type.
42    ExactSqrt,
43    ExactExp,
44    ExactLn,
45    /// π and e exactly, which `pi` and `e` are in a context that declares an exact type.
46    ExactPi,
47    ExactE,
48    /// ω, the first infinite ordinal, which `omega` is in an `Ordinal` context.
49    ExactOmega,
50    /// The end state of a loop whose state flows between jumps.
51    HybridFlow,
52    /// How many passes a loop makes whose guard compares terms linear in a counter it steps.
53    FirstExit,
54    /// `base ** exponent` to an exponent that is an exact number, which `**` and `pow` are when their
55    /// exponent is one: a fraction `p/q` takes the real `q`-th root to the `p`-th power.
56    ExactPower,
57    /// `orderedInfinitesimal(name, larger, smaller, modulus, allowed…)`: a fresh infinitesimal much
58    /// smaller than the infinitesimal `larger` and much larger than `smaller`, either bound `nothing`
59    /// when the declaration does not name it.
60    OrderedInfinitesimal,
61}
62
63impl Builtin {
64    pub const ALL: [Builtin; 26] = [
65        Builtin::Infinitesimal,
66        Builtin::StandardPart,
67        Builtin::IsInfinitesimal,
68        Builtin::IsLimited,
69        Builtin::InfinitelyClose,
70        Builtin::GeneratorOf,
71        Builtin::LimitOf,
72        Builtin::Provisional,
73        Builtin::AtTheLimit,
74        Builtin::TripCount,
75        Builtin::AffinePower,
76        Builtin::PolynomialFlow,
77        Builtin::CycleAt,
78        Builtin::SearchCandidates,
79        Builtin::StateSize,
80        Builtin::EveryNatural,
81        Builtin::ExactSqrt,
82        Builtin::ExactExp,
83        Builtin::ExactLn,
84        Builtin::ExactPi,
85        Builtin::ExactE,
86        Builtin::ExactOmega,
87        Builtin::HybridFlow,
88        Builtin::FirstExit,
89        Builtin::ExactPower,
90        Builtin::OrderedInfinitesimal,
91    ];
92
93    /// The builtin's name as a program calls it.
94    pub fn name(self) -> &'static str {
95        match self {
96            Builtin::Infinitesimal => "infinitesimal",
97            Builtin::StandardPart => "standardPart",
98            Builtin::IsInfinitesimal => "isInfinitesimal",
99            Builtin::IsLimited => "isLimited",
100            Builtin::InfinitelyClose => "infinitelyClose",
101            Builtin::GeneratorOf => "generatorOf",
102            Builtin::LimitOf => "limitOf",
103            Builtin::Provisional => "provisional",
104            Builtin::AtTheLimit => "atTheLimit",
105            Builtin::TripCount => "tripCount",
106            Builtin::AffinePower => "affinePower",
107            Builtin::PolynomialFlow => "polynomialFlow",
108            Builtin::HybridFlow => "hybridFlow",
109            Builtin::FirstExit => "firstExit",
110            Builtin::CycleAt => "cycleAt",
111            Builtin::SearchCandidates => "searchCandidates",
112            Builtin::StateSize => "stateSize",
113            Builtin::EveryNatural => "everyNatural",
114            Builtin::ExactSqrt => "exactSqrt",
115            Builtin::ExactExp => "exactExp",
116            Builtin::ExactLn => "exactLn",
117            Builtin::ExactPi => "exactPi",
118            Builtin::ExactE => "exactE",
119            Builtin::ExactOmega => "exactOmega",
120            Builtin::ExactPower => "exactPower",
121            Builtin::OrderedInfinitesimal => "orderedInfinitesimal",
122        }
123    }
124
125    /// The builtin a program calls by `name`.
126    pub fn named(name: &str) -> Option<Builtin> {
127        Builtin::ALL.into_iter().find(|b| b.name() == name)
128    }
129}
130
131/// `builtin` applied to `args`, which number as many as the builtin takes (the checker refuses a
132/// call with any other count before a program runs).
133pub fn call<V: ValueAlgebra>(builtin: Builtin, args: Vec<V>) -> Result<V, String> {
134    let mut args = args.into_iter();
135    let mut next = || args.next().expect("the checker counted this builtin's arguments");
136    let name_of = |v: V| match v.text() {
137        Some(t) => Ok(t.to_string()),
138        None => Err(format!("an infinitesimal's name is Text, got {}", v.type_name())),
139    };
140    let natural = |v: V| match v.integer().and_then(|b| b.to_i64()) {
141        Some(n) if n >= 0 => Ok(n as u64),
142        _ => Err(format!(
143            "an infinitesimal's residue facts are natural numbers, got {}",
144            v.display_string()
145        )),
146    };
147    match builtin {
148        Builtin::Infinitesimal => {
149            let name = name_of(next())?;
150            let modulus = natural(next())?;
151            let allowed = args.map(natural).collect::<Result<Vec<u64>, String>>()?;
152            tower::new_infinitesimal(&name, modulus, &allowed)
153        }
154        Builtin::OrderedInfinitesimal => {
155            let name = name_of(next())?;
156            let (larger, smaller) = (next(), next());
157            let modulus = natural(next())?;
158            let allowed = args.map(natural).collect::<Result<Vec<u64>, String>>()?;
159            tower::new_ordered_infinitesimal(&name, &larger, &smaller, modulus, &allowed)
160        }
161        Builtin::StandardPart => {
162            let x = next();
163            match args.next() {
164                Some(at) => tower::standard_part_relative(&x, &at),
165                None => tower::standard_part(&x),
166            }
167        }
168        Builtin::IsInfinitesimal => {
169            let x = next();
170            match args.next() {
171                Some(at) => tower::is_infinitesimal_relative(&x, &at),
172                None => tower::is_infinitesimal(&x),
173            }
174        }
175        Builtin::IsLimited => {
176            let x = next();
177            match args.next() {
178                Some(at) => tower::is_limited_relative(&x, &at),
179                None => tower::is_limited(&x),
180            }
181        }
182        Builtin::InfinitelyClose => {
183            let left = next();
184            let right = next();
185            let difference = V::subtract(left, right)?;
186            match args.next() {
187                Some(at) => tower::is_infinitesimal_relative(&difference, &at),
188                None => tower::is_infinitesimal(&difference),
189            }
190        }
191        Builtin::GeneratorOf => tower::generator_of(&next()),
192        Builtin::LimitOf => {
193            let value = next();
194            let rule = rule_named(&next())?;
195            tower::apply_limit(&value, rule)
196        }
197        Builtin::Provisional => {
198            let count = |v: V| match v.integer().and_then(|b| b.to_i64()) {
199                Some(n) if n >= 0 => Ok(n as u64),
200                _ => Err(format!(
201                    "a provisional answer counts with natural numbers, got {}",
202                    v.display_string()
203                )),
204            };
205            let value = next();
206            let steps = count(next())?;
207            let revisions = count(next())?;
208            Ok(tower::provisional(value, steps, revisions))
209        }
210        Builtin::AtTheLimit => {
211            rule_named(&next())?;
212            Ok(V::nothing())
213        }
214        Builtin::TripCount => {
215            let (t0, step, bound, relation) = (next(), next(), next(), next());
216            match relation.text() {
217                Some(rel) => supertask::trip_count(&t0, &step, &bound, rel),
218                None => Err(format!("a clock's relation is named by Text, got {}", relation.type_name())),
219            }
220        }
221        Builtin::AffinePower => {
222            let (matrix, vector, n) = (next(), next(), next());
223            supertask::affine_power(&matrix, &vector, &n)
224        }
225        Builtin::PolynomialFlow => {
226            let (field, vector, n) = (next(), next(), next());
227            supertask::polynomial_flow(&field, &vector, &n)
228        }
229        Builtin::HybridFlow => {
230            let (model, vector, n) = (next(), next(), next());
231            supertask::hybrid_flow(&model, &vector, &n)
232        }
233        Builtin::FirstExit => {
234            let (t0, step, guard) = (next(), next(), next());
235            supertask::first_exit(&t0, &step, &guard)
236        }
237        Builtin::CycleAt => {
238            let (states, repeated, n) = (next(), next(), next());
239            supertask::cycle_at(&states, &repeated, &n)
240        }
241        Builtin::SearchCandidates => {
242            let (atoms, moduli) = (next(), next());
243            supertask::search_candidates(&atoms, &moduli)
244        }
245        Builtin::StateSize => {
246            let bits = supertask::state_size(&next());
247            Ok(V::from_bigint(BigInt::from_i64(i64::try_from(bits).unwrap_or(i64::MAX))))
248        }
249        Builtin::EveryNatural => Err(
250            "a search over every natural number reached the runtime unresolved; the supertask engine resolves every such loop before the program runs"
251                .to_string(),
252        ),
253        Builtin::ExactSqrt => tower::real_fn(tower::RealFn::Sqrt, &next()),
254        Builtin::ExactExp => tower::real_fn(tower::RealFn::Exp, &next()),
255        Builtin::ExactLn => tower::real_fn(tower::RealFn::Ln, &next()),
256        Builtin::ExactPi => Ok(tower::pi()),
257        Builtin::ExactE => Ok(tower::euler()),
258        Builtin::ExactOmega => Ok(tower::omega()),
259        Builtin::ExactPower => {
260            let (base, exponent) = (next(), next());
261            tower::exact_power(&base, &exponent)
262        }
263    }
264}
265
266fn rule_named<V: ValueAlgebra>(rule: &V) -> Result<crate::limit_value::LimitRule, String> {
267    match rule.text() {
268        Some(name) => tower::limit_rule(name),
269        None => Err(format!("a limit rule is named by Text, got {}", rule.type_name())),
270    }
271}
272
273#[cfg(test)]
274#[path = "../../logicaffeine_tests/unit/logicaffeine_base/extension/tests.rs"]
275mod tests;
logicaffeine_base/extension.rs

logicaffeine_base/
extension.rs
