oxilean_kernel/reduce/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::declaration::{QuotKind, RecursorVal};
6use crate::expr_util::{get_app_args, get_app_fn, mk_app};
7use crate::instantiate::instantiate_type_lparams;
8use crate::subst::instantiate;
9use crate::{Environment, Expr, Literal, Name};
10use std::collections::HashMap;
11
12use super::types::{
13    ConfigNode, DecisionNode, Either2, FlatSubstitution, FocusStack, LabelSet, NonEmptyVec,
14    PathBuf, Reducer, ReducerStats, ReducibilityHint, ReductionRule, ReductionTrace, RewriteRule,
15    RewriteRuleSet, SimpleDag, SlidingSum, SmallMap, SparseVec, StackCalc, StatSummary, Stopwatch,
16    StringPool, TokenBucket, TransformStat, TransitiveClosure, TransparencyMode, VersionedRecord,
17    WindowIterator, WriteOnce,
18};
19
20/// Instantiate the RHS of a recursor rule.
21///
22/// The RHS has bound variables that need to be substituted with:
23/// - Parameters from the recursor application
24/// - The motive
25/// - Minor premises
26/// - Constructor fields
27/// - Recursive results
28pub(super) fn instantiate_recursor_rhs(
29    rhs: &Expr,
30    rec_val: &RecursorVal,
31    rec_levels: &[crate::Level],
32    rec_args: &[Expr],
33    ctor_args: &[Expr],
34) -> Expr {
35    let mut subst = Vec::new();
36    let np = rec_val.num_params as usize;
37    for item in rec_args.iter().take(np) {
38        subst.push(item.clone());
39    }
40    let nm = rec_val.num_motives as usize;
41    let motive_start = np;
42    for i in 0..nm {
43        if motive_start + i < rec_args.len() {
44            subst.push(rec_args[motive_start + i].clone());
45        }
46    }
47    let nminor = rec_val.num_minors as usize;
48    let minor_start = motive_start + nm;
49    for i in 0..nminor {
50        if minor_start + i < rec_args.len() {
51            subst.push(rec_args[minor_start + i].clone());
52        }
53    }
54    for item in ctor_args.iter().skip(np) {
55        subst.push(item.clone());
56    }
57    let rhs_inst = if rec_val.common.level_params.is_empty() || rec_levels.is_empty() {
58        rhs.clone()
59    } else {
60        instantiate_type_lparams(rhs, &rec_val.common.level_params, rec_levels)
61    };
62    crate::instantiate::instantiate_rev(&rhs_inst, &subst)
63}
64/// Try to reduce a nat literal operation in application form.
65pub(super) fn try_reduce_nat_app(head: &Expr, args: &[Expr]) -> Option<Expr> {
66    if let Expr::Const(name, _) = head {
67        let name_str = name.to_string();
68        match name_str.as_str() {
69            "Nat.zero" => {
70                return Some(Expr::Lit(Literal::Nat(0)));
71            }
72            "Nat.succ" if !args.is_empty() => {
73                if let Expr::Lit(Literal::Nat(n)) = &args[0] {
74                    return Some(Expr::Lit(Literal::Nat(n + 1)));
75                }
76            }
77            "Nat.pred" if !args.is_empty() => {
78                if let Expr::Lit(Literal::Nat(n)) = &args[0] {
79                    return Some(Expr::Lit(Literal::Nat(n.saturating_sub(1))));
80                }
81            }
82            "Nat.add" if args.len() >= 2 => {
83                if let (Expr::Lit(Literal::Nat(m)), Expr::Lit(Literal::Nat(n))) =
84                    (&args[0], &args[1])
85                {
86                    return Some(Expr::Lit(Literal::Nat(m + n)));
87                }
88            }
89            "Nat.mul" if args.len() >= 2 => {
90                if let (Expr::Lit(Literal::Nat(m)), Expr::Lit(Literal::Nat(n))) =
91                    (&args[0], &args[1])
92                {
93                    return Some(Expr::Lit(Literal::Nat(m * n)));
94                }
95            }
96            "Nat.sub" if args.len() >= 2 => {
97                if let (Expr::Lit(Literal::Nat(m)), Expr::Lit(Literal::Nat(n))) =
98                    (&args[0], &args[1])
99                {
100                    return Some(Expr::Lit(Literal::Nat(m.saturating_sub(*n))));
101                }
102            }
103            "Nat.div" if args.len() >= 2 => {
104                if let (Expr::Lit(Literal::Nat(m)), Expr::Lit(Literal::Nat(n))) =
105                    (&args[0], &args[1])
106                {
107                    if *n != 0 {
108                        return Some(Expr::Lit(Literal::Nat(m / n)));
109                    }
110                    return Some(Expr::Lit(Literal::Nat(0)));
111                }
112            }
113            "Nat.mod" if args.len() >= 2 => {
114                if let (Expr::Lit(Literal::Nat(m)), Expr::Lit(Literal::Nat(n))) =
115                    (&args[0], &args[1])
116                {
117                    if *n != 0 {
118                        return Some(Expr::Lit(Literal::Nat(m % n)));
119                    }
120                    return Some(Expr::Lit(Literal::Nat(*m)));
121                }
122            }
123            "Nat.pow" if args.len() >= 2 => {
124                if let (Expr::Lit(Literal::Nat(m)), Expr::Lit(Literal::Nat(n))) =
125                    (&args[0], &args[1])
126                {
127                    return Some(Expr::Lit(Literal::Nat(m.pow(*n as u32))));
128                }
129            }
130            "Nat.beq" if args.len() >= 2 => {
131                if let (Expr::Lit(Literal::Nat(m)), Expr::Lit(Literal::Nat(n))) =
132                    (&args[0], &args[1])
133                {
134                    return Some(nat_bool_result(m == n));
135                }
136            }
137            "Nat.ble" if args.len() >= 2 => {
138                if let (Expr::Lit(Literal::Nat(m)), Expr::Lit(Literal::Nat(n))) =
139                    (&args[0], &args[1])
140                {
141                    return Some(nat_bool_result(m <= n));
142                }
143            }
144            "Nat.blt" if args.len() >= 2 => {
145                if let (Expr::Lit(Literal::Nat(m)), Expr::Lit(Literal::Nat(n))) =
146                    (&args[0], &args[1])
147                {
148                    return Some(nat_bool_result(m < n));
149                }
150            }
151            "Nat.gcd" if args.len() >= 2 => {
152                if let (Expr::Lit(Literal::Nat(m)), Expr::Lit(Literal::Nat(n))) =
153                    (&args[0], &args[1])
154                {
155                    return Some(Expr::Lit(Literal::Nat(gcd(*m, *n))));
156                }
157            }
158            "Nat.land" if args.len() >= 2 => {
159                if let (Expr::Lit(Literal::Nat(m)), Expr::Lit(Literal::Nat(n))) =
160                    (&args[0], &args[1])
161                {
162                    return Some(Expr::Lit(Literal::Nat(m & n)));
163                }
164            }
165            "Nat.lor" if args.len() >= 2 => {
166                if let (Expr::Lit(Literal::Nat(m)), Expr::Lit(Literal::Nat(n))) =
167                    (&args[0], &args[1])
168                {
169                    return Some(Expr::Lit(Literal::Nat(m | n)));
170                }
171            }
172            "Nat.xor" if args.len() >= 2 => {
173                if let (Expr::Lit(Literal::Nat(m)), Expr::Lit(Literal::Nat(n))) =
174                    (&args[0], &args[1])
175                {
176                    return Some(Expr::Lit(Literal::Nat(m ^ n)));
177                }
178            }
179            "Nat.shiftLeft" if args.len() >= 2 => {
180                if let (Expr::Lit(Literal::Nat(m)), Expr::Lit(Literal::Nat(n))) =
181                    (&args[0], &args[1])
182                {
183                    if *n < 64 {
184                        return Some(Expr::Lit(Literal::Nat(m << n)));
185                    }
186                }
187            }
188            "Nat.shiftRight" if args.len() >= 2 => {
189                if let (Expr::Lit(Literal::Nat(m)), Expr::Lit(Literal::Nat(n))) =
190                    (&args[0], &args[1])
191                {
192                    if *n < 64 {
193                        return Some(Expr::Lit(Literal::Nat(m >> n)));
194                    }
195                    return Some(Expr::Lit(Literal::Nat(0)));
196                }
197            }
198            "String.length" if !args.is_empty() => {
199                if let Expr::Lit(Literal::Str(s)) = &args[0] {
200                    return Some(Expr::Lit(Literal::Nat(s.len() as u64)));
201                }
202            }
203            "String.append" if args.len() >= 2 => {
204                if let (Expr::Lit(Literal::Str(s1)), Expr::Lit(Literal::Str(s2))) =
205                    (&args[0], &args[1])
206                {
207                    let mut result = s1.clone();
208                    result.push_str(s2);
209                    return Some(Expr::Lit(Literal::Str(result)));
210                }
211            }
212            "String.beq" if args.len() >= 2 => {
213                if let (Expr::Lit(Literal::Str(s1)), Expr::Lit(Literal::Str(s2))) =
214                    (&args[0], &args[1])
215                {
216                    return Some(nat_bool_result(s1 == s2));
217                }
218            }
219            _ => {}
220        }
221    }
222    None
223}
224/// GCD for nat literals.
225pub(super) fn gcd(mut a: u64, mut b: u64) -> u64 {
226    while b != 0 {
227        let t = b;
228        b = a % b;
229        a = t;
230    }
231    a
232}
233/// Create a Bool result from a comparison.
234pub(super) fn nat_bool_result(b: bool) -> Expr {
235    if b {
236        Expr::Const(Name::str("Bool").append_str("true"), vec![])
237    } else {
238        Expr::Const(Name::str("Bool").append_str("false"), vec![])
239    }
240}
241/// Try to reduce a structure projection.
242///
243/// `S.idx struct_val` reduces when `struct_val` is a constructor application.
244pub(super) fn try_reduce_proj(
245    struct_name: &Name,
246    field_idx: u32,
247    struct_whnf: &Expr,
248    env: &Environment,
249) -> Option<Expr> {
250    let ctor_fn = get_app_fn(struct_whnf);
251    let ctor_name = if let Expr::Const(name, _) = ctor_fn {
252        name
253    } else {
254        return None;
255    };
256    let ctor_val = env.get_constructor_val(ctor_name)?;
257    if &ctor_val.induct != struct_name {
258        return None;
259    }
260    let ctor_args: Vec<&Expr> = get_app_args(struct_whnf);
261    let param_count = ctor_val.num_params as usize;
262    let field_pos = param_count + field_idx as usize;
263    if field_pos < ctor_args.len() {
264        Some(ctor_args[field_pos].clone())
265    } else {
266        None
267    }
268}
269/// Try to reduce a quotient operation.
270pub(super) fn try_reduce_quot(name: &Name, args: &[Expr], env: &Environment) -> Option<Expr> {
271    let qv = env.get_quotient_val(name)?;
272    match qv.kind {
273        QuotKind::Lift => {
274            if args.len() < 6 {
275                return None;
276            }
277            let quot_val = &args[5];
278            let quot_head = get_app_fn(quot_val);
279            if let Expr::Const(mk_name, _) = quot_head {
280                if let Some(mk_qv) = env.get_quotient_val(mk_name) {
281                    if mk_qv.kind == QuotKind::Mk {
282                        let mk_args: Vec<&Expr> = get_app_args(quot_val);
283                        if mk_args.len() >= 3 {
284                            let a = mk_args[2];
285                            let f = &args[3];
286                            return Some(Expr::App(Box::new(f.clone()), Box::new(a.clone())));
287                        }
288                    }
289                }
290            }
291            None
292        }
293        QuotKind::Ind => {
294            if args.len() < 6 {
295                return None;
296            }
297            let quot_val = &args[5];
298            let quot_head = get_app_fn(quot_val);
299            if let Expr::Const(mk_name, _) = quot_head {
300                if let Some(mk_qv) = env.get_quotient_val(mk_name) {
301                    if mk_qv.kind == QuotKind::Mk {
302                        let mk_args: Vec<&Expr> = get_app_args(quot_val);
303                        if mk_args.len() >= 3 {
304                            let a = mk_args[2];
305                            let h = &args[4];
306                            return Some(Expr::App(Box::new(h.clone()), Box::new(a.clone())));
307                        }
308                    }
309                }
310            }
311            None
312        }
313        _ => None,
314    }
315}
316/// Nat literal arithmetic reduction (legacy API).
317pub fn reduce_nat_op(op: &str, args: &[Expr]) -> Option<Expr> {
318    match (op, args) {
319        ("Nat.succ", [Expr::Lit(Literal::Nat(n))]) => Some(Expr::Lit(Literal::Nat(n + 1))),
320        ("Nat.add", [Expr::Lit(Literal::Nat(m)), Expr::Lit(Literal::Nat(n))]) => {
321            Some(Expr::Lit(Literal::Nat(m + n)))
322        }
323        ("Nat.mul", [Expr::Lit(Literal::Nat(m)), Expr::Lit(Literal::Nat(n))]) => {
324            Some(Expr::Lit(Literal::Nat(m * n)))
325        }
326        ("Nat.sub", [Expr::Lit(Literal::Nat(m)), Expr::Lit(Literal::Nat(n))]) => {
327            Some(Expr::Lit(Literal::Nat(m.saturating_sub(*n))))
328        }
329        _ => None,
330    }
331}
332#[cfg(test)]
333mod tests {
334    use super::*;
335    use crate::{BinderInfo, FVarId, Level};
336    #[test]
337    fn test_beta_reduction() {
338        let mut reducer = Reducer::new();
339        let nat_ty = Expr::Sort(Level::zero());
340        let body = Expr::BVar(0);
341        let lam = Expr::Lam(
342            BinderInfo::Default,
343            Name::str("x"),
344            Box::new(nat_ty),
345            Box::new(body),
346        );
347        let arg = Expr::Lit(Literal::Nat(42));
348        let app = Expr::App(Box::new(lam), Box::new(arg.clone()));
349        let result = reducer.whnf(&app);
350        assert_eq!(result, arg);
351    }
352    #[test]
353    fn test_beta_reduction_nested() {
354        let mut reducer = Reducer::new();
355        let ty = Expr::Sort(Level::zero());
356        let inner_body = Expr::BVar(1);
357        let inner_lam = Expr::Lam(
358            BinderInfo::Default,
359            Name::str("y"),
360            Box::new(ty.clone()),
361            Box::new(inner_body),
362        );
363        let outer_lam = Expr::Lam(
364            BinderInfo::Default,
365            Name::str("x"),
366            Box::new(ty),
367            Box::new(inner_lam),
368        );
369        let arg_a = Expr::FVar(FVarId(1));
370        let arg_b = Expr::FVar(FVarId(2));
371        let app1 = Expr::App(Box::new(outer_lam), Box::new(arg_a.clone()));
372        let app2 = Expr::App(Box::new(app1), Box::new(arg_b));
373        let result = reducer.whnf(&app2);
374        assert_eq!(result, arg_a);
375    }
376    #[test]
377    fn test_zeta_reduction() {
378        let mut reducer = Reducer::new();
379        let nat_ty = Expr::Sort(Level::zero());
380        let val = Expr::Lit(Literal::Nat(42));
381        let body = Expr::BVar(0);
382        let let_expr = Expr::Let(
383            Name::str("x"),
384            Box::new(nat_ty),
385            Box::new(val.clone()),
386            Box::new(body),
387        );
388        let result = reducer.whnf(&let_expr);
389        assert_eq!(result, val);
390    }
391    #[test]
392    fn test_whnf_already_normal() {
393        let mut reducer = Reducer::new();
394        let lambda = Expr::Lam(
395            BinderInfo::Default,
396            Name::str("x"),
397            Box::new(Expr::Sort(Level::zero())),
398            Box::new(Expr::BVar(0)),
399        );
400        let result = reducer.whnf(&lambda);
401        assert_eq!(result, lambda);
402    }
403    #[test]
404    fn test_nat_arithmetic() {
405        let args = vec![Expr::Lit(Literal::Nat(3)), Expr::Lit(Literal::Nat(4))];
406        let result = reduce_nat_op("Nat.add", &args);
407        assert_eq!(result, Some(Expr::Lit(Literal::Nat(7))));
408        let args = vec![Expr::Lit(Literal::Nat(6)), Expr::Lit(Literal::Nat(7))];
409        let result = reduce_nat_op("Nat.mul", &args);
410        assert_eq!(result, Some(Expr::Lit(Literal::Nat(42))));
411    }
412    #[test]
413    fn test_cache_hit() {
414        let mut reducer = Reducer::new();
415        let expr = Expr::Lit(Literal::Nat(42));
416        let result1 = reducer.whnf(&expr);
417        let result2 = reducer.whnf(&expr);
418        assert_eq!(result1, result2);
419        assert_eq!(reducer.cache.len(), 1);
420    }
421    #[test]
422    fn test_nat_extended_ops() {
423        let head = Expr::Const(Name::str("Nat.div"), vec![]);
424        let args = vec![Expr::Lit(Literal::Nat(10)), Expr::Lit(Literal::Nat(3))];
425        assert_eq!(
426            try_reduce_nat_app(&head, &args),
427            Some(Expr::Lit(Literal::Nat(3)))
428        );
429        let head = Expr::Const(Name::str("Nat.mod"), vec![]);
430        let args = vec![Expr::Lit(Literal::Nat(10)), Expr::Lit(Literal::Nat(3))];
431        assert_eq!(
432            try_reduce_nat_app(&head, &args),
433            Some(Expr::Lit(Literal::Nat(1)))
434        );
435        let head = Expr::Const(Name::str("Nat.gcd"), vec![]);
436        let args = vec![Expr::Lit(Literal::Nat(12)), Expr::Lit(Literal::Nat(8))];
437        assert_eq!(
438            try_reduce_nat_app(&head, &args),
439            Some(Expr::Lit(Literal::Nat(4)))
440        );
441    }
442    #[test]
443    fn test_nat_bitwise_ops() {
444        let head = Expr::Const(Name::str("Nat.land"), vec![]);
445        let args = vec![
446            Expr::Lit(Literal::Nat(0b1100)),
447            Expr::Lit(Literal::Nat(0b1010)),
448        ];
449        assert_eq!(
450            try_reduce_nat_app(&head, &args),
451            Some(Expr::Lit(Literal::Nat(0b1000)))
452        );
453        let head = Expr::Const(Name::str("Nat.lor"), vec![]);
454        let args = vec![
455            Expr::Lit(Literal::Nat(0b1100)),
456            Expr::Lit(Literal::Nat(0b1010)),
457        ];
458        assert_eq!(
459            try_reduce_nat_app(&head, &args),
460            Some(Expr::Lit(Literal::Nat(0b1110)))
461        );
462        let head = Expr::Const(Name::str("Nat.xor"), vec![]);
463        let args = vec![
464            Expr::Lit(Literal::Nat(0b1100)),
465            Expr::Lit(Literal::Nat(0b1010)),
466        ];
467        assert_eq!(
468            try_reduce_nat_app(&head, &args),
469            Some(Expr::Lit(Literal::Nat(0b0110)))
470        );
471    }
472    #[test]
473    fn test_string_ops() {
474        let head = Expr::Const(Name::str("String.length"), vec![]);
475        let args = vec![Expr::Lit(Literal::Str("hello".to_string()))];
476        assert_eq!(
477            try_reduce_nat_app(&head, &args),
478            Some(Expr::Lit(Literal::Nat(5)))
479        );
480        let head = Expr::Const(Name::str("String.append"), vec![]);
481        let args = vec![
482            Expr::Lit(Literal::Str("hello".to_string())),
483            Expr::Lit(Literal::Str(" world".to_string())),
484        ];
485        assert_eq!(
486            try_reduce_nat_app(&head, &args),
487            Some(Expr::Lit(Literal::Str("hello world".to_string())))
488        );
489    }
490    #[test]
491    fn test_transparency_modes() {
492        let mut reducer = Reducer::new();
493        assert!(reducer.should_unfold_hint(ReducibilityHint::Abbrev));
494        assert!(reducer.should_unfold_hint(ReducibilityHint::Regular(1)));
495        assert!(!reducer.should_unfold_hint(ReducibilityHint::Opaque));
496        reducer.set_transparency(TransparencyMode::Reducible);
497        assert!(reducer.should_unfold_hint(ReducibilityHint::Abbrev));
498        assert!(!reducer.should_unfold_hint(ReducibilityHint::Regular(1)));
499        reducer.set_transparency(TransparencyMode::None);
500        assert!(!reducer.should_unfold_hint(ReducibilityHint::Abbrev));
501    }
502}
503/// Evaluate a pure binary Nat operation given its name and two literal arguments.
504/// Returns `None` if not recognized or arguments are not literals.
505#[allow(dead_code)]
506pub fn eval_nat_binop(op: &str, lhs: u64, rhs: u64) -> Option<u64> {
507    match op {
508        "Nat.add" => Some(lhs + rhs),
509        "Nat.sub" => Some(lhs.saturating_sub(rhs)),
510        "Nat.mul" => Some(lhs * rhs),
511        "Nat.div" => Some(lhs.checked_div(rhs).unwrap_or(0)),
512        "Nat.mod" => {
513            if rhs == 0 {
514                Some(lhs)
515            } else {
516                Some(lhs % rhs)
517            }
518        }
519        "Nat.pow" => Some(lhs.saturating_pow(rhs as u32)),
520        "Nat.gcd" => {
521            let mut a = lhs;
522            let mut b = rhs;
523            while b != 0 {
524                let t = b;
525                b = a % b;
526                a = t;
527            }
528            Some(a)
529        }
530        "Nat.lcm" => {
531            if lhs == 0 || rhs == 0 {
532                Some(0)
533            } else {
534                let mut a = lhs;
535                let mut b = rhs;
536                while b != 0 {
537                    let t = b;
538                    b = a % b;
539                    a = t;
540                }
541                Some(lhs / a * rhs)
542            }
543        }
544        "Nat.land" => Some(lhs & rhs),
545        "Nat.lor" => Some(lhs | rhs),
546        "Nat.xor" => Some(lhs ^ rhs),
547        "Nat.shiftLeft" => Some(lhs.checked_shl(rhs as u32).unwrap_or(0)),
548        "Nat.shiftRight" => Some(lhs.checked_shr(rhs as u32).unwrap_or(0)),
549        "Nat.min" => Some(lhs.min(rhs)),
550        "Nat.max" => Some(lhs.max(rhs)),
551        _ => None,
552    }
553}
554/// Evaluate a Nat comparison, returning a Bool literal constant name.
555#[allow(dead_code)]
556pub fn eval_nat_cmp(op: &str, lhs: u64, rhs: u64) -> Option<&'static str> {
557    match op {
558        "Nat.beq" | "Nat.decEq" => Some(if lhs == rhs { "true" } else { "false" }),
559        "Nat.bne" => Some(if lhs != rhs { "true" } else { "false" }),
560        "Nat.ble" => Some(if lhs <= rhs { "true" } else { "false" }),
561        "Nat.blt" => Some(if lhs < rhs { "true" } else { "false" }),
562        _ => None,
563    }
564}
565/// Check whether the expression is already in weak-head normal form
566/// without performing any reduction.
567///
568/// An expression is in WHNF if:
569/// - It is a Sort, Lit, FVar, or Const that is not a defined definition.
570/// - It is a Lambda (since we only reduce applications, not under binders).
571/// - It is a Pi type.
572/// - It is a stuck application (the head is not a lambda/const-with-def).
573#[allow(dead_code)]
574pub fn is_whnf(expr: &Expr) -> bool {
575    match expr {
576        Expr::Sort(_)
577        | Expr::Lit(_)
578        | Expr::FVar(_)
579        | Expr::Lam(_, _, _, _)
580        | Expr::Pi(_, _, _, _)
581        | Expr::Let(_, _, _, _) => true,
582        Expr::Const(_, _) => true,
583        Expr::BVar(_) => true,
584        Expr::App(f, _) => match f.as_ref() {
585            Expr::Lam(_, _, _, _) => false,
586            _ => is_whnf(f),
587        },
588        Expr::Proj(_, _, _) => false,
589    }
590}
591/// Compute the "head" of an expression after stripping all App layers.
592#[allow(dead_code)]
593pub fn head_of(expr: &Expr) -> &Expr {
594    match expr {
595        Expr::App(f, _) => head_of(f),
596        _ => expr,
597    }
598}
599/// Count how many arguments are applied in an App chain.
600#[allow(dead_code)]
601pub fn app_arity(expr: &Expr) -> usize {
602    match expr {
603        Expr::App(f, _) => 1 + app_arity(f),
604        _ => 0,
605    }
606}
607#[cfg(test)]
608mod extra_reduce_tests {
609    use super::*;
610    use crate::{BinderInfo, Level};
611    #[test]
612    fn test_reduction_rule_display() {
613        assert_eq!(ReductionRule::Beta.to_string(), "beta");
614        assert_eq!(ReductionRule::Delta.to_string(), "delta");
615        assert_eq!(ReductionRule::Iota.to_string(), "iota");
616        assert_eq!(ReductionRule::None.to_string(), "none");
617    }
618    #[test]
619    fn test_reduction_trace_enabled() {
620        let mut trace = ReductionTrace::enabled();
621        let before = Expr::Lit(Literal::Nat(1));
622        let after = Expr::Lit(Literal::Nat(2));
623        trace.record(ReductionRule::Beta, before.clone(), after.clone());
624        assert_eq!(trace.step_count(), 1);
625        assert_eq!(trace.count_rule(&ReductionRule::Beta), 1);
626        assert_eq!(trace.count_rule(&ReductionRule::Delta), 0);
627    }
628    #[test]
629    fn test_reduction_trace_disabled() {
630        let mut trace = ReductionTrace::disabled();
631        let e = Expr::Lit(Literal::Nat(1));
632        trace.record(ReductionRule::Beta, e.clone(), e.clone());
633        assert_eq!(trace.step_count(), 0);
634    }
635    #[test]
636    fn test_reducer_stats_total() {
637        let stats = ReducerStats {
638            whnf_calls: 10,
639            cache_hits: 3,
640            beta_count: 4,
641            delta_count: 2,
642            iota_count: 1,
643            zeta_count: 1,
644            nat_lit_count: 2,
645        };
646        assert_eq!(stats.total_reductions(), 10);
647    }
648    #[test]
649    fn test_reducer_stats_cache_hit_rate() {
650        let stats = ReducerStats {
651            whnf_calls: 10,
652            cache_hits: 5,
653            ..Default::default()
654        };
655        assert!((stats.cache_hit_rate() - 0.5).abs() < 1e-10);
656    }
657    #[test]
658    fn test_eval_nat_binop_add() {
659        assert_eq!(eval_nat_binop("Nat.add", 3, 4), Some(7));
660    }
661    #[test]
662    fn test_eval_nat_binop_sub_saturating() {
663        assert_eq!(eval_nat_binop("Nat.sub", 3, 10), Some(0));
664    }
665    #[test]
666    fn test_eval_nat_binop_div_zero() {
667        assert_eq!(eval_nat_binop("Nat.div", 7, 0), Some(0));
668    }
669    #[test]
670    fn test_eval_nat_binop_gcd() {
671        assert_eq!(eval_nat_binop("Nat.gcd", 12, 8), Some(4));
672    }
673    #[test]
674    fn test_eval_nat_binop_lcm() {
675        assert_eq!(eval_nat_binop("Nat.lcm", 4, 6), Some(12));
676    }
677    #[test]
678    fn test_eval_nat_binop_land() {
679        assert_eq!(eval_nat_binop("Nat.land", 0b1100, 0b1010), Some(0b1000));
680    }
681    #[test]
682    fn test_eval_nat_cmp_beq_true() {
683        assert_eq!(eval_nat_cmp("Nat.beq", 5, 5), Some("true"));
684    }
685    #[test]
686    fn test_eval_nat_cmp_beq_false() {
687        assert_eq!(eval_nat_cmp("Nat.beq", 5, 6), Some("false"));
688    }
689    #[test]
690    fn test_eval_nat_cmp_ble() {
691        assert_eq!(eval_nat_cmp("Nat.ble", 3, 5), Some("true"));
692        assert_eq!(eval_nat_cmp("Nat.ble", 5, 3), Some("false"));
693    }
694    #[test]
695    fn test_is_whnf_sort() {
696        assert!(is_whnf(&Expr::Sort(Level::zero())));
697    }
698    #[test]
699    fn test_is_whnf_lit() {
700        assert!(is_whnf(&Expr::Lit(Literal::Nat(42))));
701    }
702    #[test]
703    fn test_is_whnf_lam() {
704        let lam = Expr::Lam(
705            BinderInfo::Default,
706            Name::str("x"),
707            Box::new(Expr::Sort(Level::zero())),
708            Box::new(Expr::BVar(0)),
709        );
710        assert!(is_whnf(&lam));
711    }
712    #[test]
713    fn test_is_whnf_redex() {
714        let lam = Expr::Lam(
715            BinderInfo::Default,
716            Name::str("x"),
717            Box::new(Expr::Sort(Level::zero())),
718            Box::new(Expr::BVar(0)),
719        );
720        let redex = Expr::App(Box::new(lam), Box::new(Expr::Lit(Literal::Nat(1))));
721        assert!(!is_whnf(&redex));
722    }
723    #[test]
724    fn test_head_of_nested_app() {
725        let f = Expr::Const(Name::str("f"), vec![]);
726        let app1 = Expr::App(Box::new(f.clone()), Box::new(Expr::Lit(Literal::Nat(1))));
727        let app2 = Expr::App(Box::new(app1), Box::new(Expr::Lit(Literal::Nat(2))));
728        assert_eq!(*head_of(&app2), f);
729    }
730    #[test]
731    fn test_app_arity() {
732        let f = Expr::Const(Name::str("f"), vec![]);
733        let app1 = Expr::App(Box::new(f.clone()), Box::new(Expr::Lit(Literal::Nat(1))));
734        let app2 = Expr::App(Box::new(app1), Box::new(Expr::Lit(Literal::Nat(2))));
735        assert_eq!(app_arity(&app2), 2);
736        assert_eq!(app_arity(&f), 0);
737    }
738    #[test]
739    fn test_trace_clear() {
740        let mut trace = ReductionTrace::enabled();
741        let e = Expr::Lit(Literal::Nat(0));
742        trace.record(ReductionRule::Beta, e.clone(), e.clone());
743        assert_eq!(trace.step_count(), 1);
744        trace.clear();
745        assert_eq!(trace.step_count(), 0);
746    }
747    #[test]
748    fn test_reducer_stats_display() {
749        let stats = ReducerStats::default();
750        let s = stats.display();
751        assert!(s.contains("whnf:0"));
752    }
753}
754#[cfg(test)]
755mod tests_padding_infra {
756    use super::*;
757    #[test]
758    fn test_stat_summary() {
759        let mut ss = StatSummary::new();
760        ss.record(10.0);
761        ss.record(20.0);
762        ss.record(30.0);
763        assert_eq!(ss.count(), 3);
764        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
765        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
766        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
767    }
768    #[test]
769    fn test_transform_stat() {
770        let mut ts = TransformStat::new();
771        ts.record_before(100.0);
772        ts.record_after(80.0);
773        let ratio = ts.mean_ratio().expect("ratio should be present");
774        assert!((ratio - 0.8).abs() < 1e-9);
775    }
776    #[test]
777    fn test_small_map() {
778        let mut m: SmallMap<u32, &str> = SmallMap::new();
779        m.insert(3, "three");
780        m.insert(1, "one");
781        m.insert(2, "two");
782        assert_eq!(m.get(&2), Some(&"two"));
783        assert_eq!(m.len(), 3);
784        let keys = m.keys();
785        assert_eq!(*keys[0], 1);
786        assert_eq!(*keys[2], 3);
787    }
788    #[test]
789    fn test_label_set() {
790        let mut ls = LabelSet::new();
791        ls.add("foo");
792        ls.add("bar");
793        ls.add("foo");
794        assert_eq!(ls.count(), 2);
795        assert!(ls.has("bar"));
796        assert!(!ls.has("baz"));
797    }
798    #[test]
799    fn test_config_node() {
800        let mut root = ConfigNode::section("root");
801        let child = ConfigNode::leaf("key", "value");
802        root.add_child(child);
803        assert_eq!(root.num_children(), 1);
804    }
805    #[test]
806    fn test_versioned_record() {
807        let mut vr = VersionedRecord::new(0u32);
808        vr.update(1);
809        vr.update(2);
810        assert_eq!(*vr.current(), 2);
811        assert_eq!(vr.version(), 2);
812        assert!(vr.has_history());
813        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
814    }
815    #[test]
816    fn test_simple_dag() {
817        let mut dag = SimpleDag::new(4);
818        dag.add_edge(0, 1);
819        dag.add_edge(1, 2);
820        dag.add_edge(2, 3);
821        assert!(dag.can_reach(0, 3));
822        assert!(!dag.can_reach(3, 0));
823        let order = dag.topological_sort().expect("order should be present");
824        assert_eq!(order, vec![0, 1, 2, 3]);
825    }
826    #[test]
827    fn test_focus_stack() {
828        let mut fs: FocusStack<&str> = FocusStack::new();
829        fs.focus("a");
830        fs.focus("b");
831        assert_eq!(fs.current(), Some(&"b"));
832        assert_eq!(fs.depth(), 2);
833        fs.blur();
834        assert_eq!(fs.current(), Some(&"a"));
835    }
836}
837#[cfg(test)]
838mod tests_extra_iterators {
839    use super::*;
840    #[test]
841    fn test_window_iterator() {
842        let data = vec![1u32, 2, 3, 4, 5];
843        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
844        assert_eq!(windows.len(), 3);
845        assert_eq!(windows[0], &[1, 2, 3]);
846        assert_eq!(windows[2], &[3, 4, 5]);
847    }
848    #[test]
849    fn test_non_empty_vec() {
850        let mut nev = NonEmptyVec::singleton(10u32);
851        nev.push(20);
852        nev.push(30);
853        assert_eq!(nev.len(), 3);
854        assert_eq!(*nev.first(), 10);
855        assert_eq!(*nev.last(), 30);
856    }
857}
858#[cfg(test)]
859mod tests_padding2 {
860    use super::*;
861    #[test]
862    fn test_sliding_sum() {
863        let mut ss = SlidingSum::new(3);
864        ss.push(1.0);
865        ss.push(2.0);
866        ss.push(3.0);
867        assert!((ss.sum() - 6.0).abs() < 1e-9);
868        ss.push(4.0);
869        assert!((ss.sum() - 9.0).abs() < 1e-9);
870        assert_eq!(ss.count(), 3);
871    }
872    #[test]
873    fn test_path_buf() {
874        let mut pb = PathBuf::new();
875        pb.push("src");
876        pb.push("main");
877        assert_eq!(pb.as_str(), "src/main");
878        assert_eq!(pb.depth(), 2);
879        pb.pop();
880        assert_eq!(pb.as_str(), "src");
881    }
882    #[test]
883    fn test_string_pool() {
884        let mut pool = StringPool::new();
885        let s = pool.take();
886        assert!(s.is_empty());
887        pool.give("hello".to_string());
888        let s2 = pool.take();
889        assert!(s2.is_empty());
890        assert_eq!(pool.free_count(), 0);
891    }
892    #[test]
893    fn test_transitive_closure() {
894        let mut tc = TransitiveClosure::new(4);
895        tc.add_edge(0, 1);
896        tc.add_edge(1, 2);
897        tc.add_edge(2, 3);
898        assert!(tc.can_reach(0, 3));
899        assert!(!tc.can_reach(3, 0));
900        let r = tc.reachable_from(0);
901        assert_eq!(r.len(), 4);
902    }
903    #[test]
904    fn test_token_bucket() {
905        let mut tb = TokenBucket::new(100, 10);
906        assert_eq!(tb.available(), 100);
907        assert!(tb.try_consume(50));
908        assert_eq!(tb.available(), 50);
909        assert!(!tb.try_consume(60));
910        assert_eq!(tb.capacity(), 100);
911    }
912    #[test]
913    fn test_rewrite_rule_set() {
914        let mut rrs = RewriteRuleSet::new();
915        rrs.add(RewriteRule::unconditional(
916            "beta",
917            "App(Lam(x, b), v)",
918            "b[x:=v]",
919        ));
920        rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
921        assert_eq!(rrs.len(), 2);
922        assert_eq!(rrs.unconditional_rules().len(), 1);
923        assert_eq!(rrs.conditional_rules().len(), 1);
924        assert!(rrs.get("beta").is_some());
925        let disp = rrs
926            .get("beta")
927            .expect("element at \'beta\' should exist")
928            .display();
929        assert!(disp.contains("→"));
930    }
931}
932#[cfg(test)]
933mod tests_padding3 {
934    use super::*;
935    #[test]
936    fn test_decision_node() {
937        let tree = DecisionNode::Branch {
938            key: "x".into(),
939            val: "1".into(),
940            yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
941            no_branch: Box::new(DecisionNode::Leaf("no".into())),
942        };
943        let mut ctx = std::collections::HashMap::new();
944        ctx.insert("x".into(), "1".into());
945        assert_eq!(tree.evaluate(&ctx), "yes");
946        ctx.insert("x".into(), "2".into());
947        assert_eq!(tree.evaluate(&ctx), "no");
948        assert_eq!(tree.depth(), 1);
949    }
950    #[test]
951    fn test_flat_substitution() {
952        let mut sub = FlatSubstitution::new();
953        sub.add("foo", "bar");
954        sub.add("baz", "qux");
955        assert_eq!(sub.apply("foo and baz"), "bar and qux");
956        assert_eq!(sub.len(), 2);
957    }
958    #[test]
959    fn test_stopwatch() {
960        let mut sw = Stopwatch::start();
961        sw.split();
962        sw.split();
963        assert_eq!(sw.num_splits(), 2);
964        assert!(sw.elapsed_ms() >= 0.0);
965        for &s in sw.splits() {
966            assert!(s >= 0.0);
967        }
968    }
969    #[test]
970    fn test_either2() {
971        let e: Either2<i32, &str> = Either2::First(42);
972        assert!(e.is_first());
973        let mapped = e.map_first(|x| x * 2);
974        assert_eq!(mapped.first(), Some(84));
975        let e2: Either2<i32, &str> = Either2::Second("hello");
976        assert!(e2.is_second());
977        assert_eq!(e2.second(), Some("hello"));
978    }
979    #[test]
980    fn test_write_once() {
981        let wo: WriteOnce<u32> = WriteOnce::new();
982        assert!(!wo.is_written());
983        assert!(wo.write(42));
984        assert!(!wo.write(99));
985        assert_eq!(wo.read(), Some(42));
986    }
987    #[test]
988    fn test_sparse_vec() {
989        let mut sv: SparseVec<i32> = SparseVec::new(100);
990        sv.set(5, 10);
991        sv.set(50, 20);
992        assert_eq!(*sv.get(5), 10);
993        assert_eq!(*sv.get(50), 20);
994        assert_eq!(*sv.get(0), 0);
995        assert_eq!(sv.nnz(), 2);
996        sv.set(5, 0);
997        assert_eq!(sv.nnz(), 1);
998    }
999    #[test]
1000    fn test_stack_calc() {
1001        let mut calc = StackCalc::new();
1002        calc.push(3);
1003        calc.push(4);
1004        calc.add();
1005        assert_eq!(calc.peek(), Some(7));
1006        calc.push(2);
1007        calc.mul();
1008        assert_eq!(calc.peek(), Some(14));
1009    }
1010}
oxilean_kernel/reduce/functions.rs

oxilean_kernel/reduce/
functions.rs
