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" => {
512            if rhs == 0 {
513                Some(0)
514            } else {
515                Some(lhs / rhs)
516            }
517        }
518        "Nat.mod" => {
519            if rhs == 0 {
520                Some(lhs)
521            } else {
522                Some(lhs % rhs)
523            }
524        }
525        "Nat.pow" => Some(lhs.saturating_pow(rhs as u32)),
526        "Nat.gcd" => {
527            let mut a = lhs;
528            let mut b = rhs;
529            while b != 0 {
530                let t = b;
531                b = a % b;
532                a = t;
533            }
534            Some(a)
535        }
536        "Nat.lcm" => {
537            if lhs == 0 || rhs == 0 {
538                Some(0)
539            } else {
540                let mut a = lhs;
541                let mut b = rhs;
542                while b != 0 {
543                    let t = b;
544                    b = a % b;
545                    a = t;
546                }
547                Some(lhs / a * rhs)
548            }
549        }
550        "Nat.land" => Some(lhs & rhs),
551        "Nat.lor" => Some(lhs | rhs),
552        "Nat.xor" => Some(lhs ^ rhs),
553        "Nat.shiftLeft" => Some(lhs.checked_shl(rhs as u32).unwrap_or(0)),
554        "Nat.shiftRight" => Some(lhs.checked_shr(rhs as u32).unwrap_or(0)),
555        "Nat.min" => Some(lhs.min(rhs)),
556        "Nat.max" => Some(lhs.max(rhs)),
557        _ => None,
558    }
559}
560/// Evaluate a Nat comparison, returning a Bool literal constant name.
561#[allow(dead_code)]
562pub fn eval_nat_cmp(op: &str, lhs: u64, rhs: u64) -> Option<&'static str> {
563    match op {
564        "Nat.beq" | "Nat.decEq" => Some(if lhs == rhs { "true" } else { "false" }),
565        "Nat.bne" => Some(if lhs != rhs { "true" } else { "false" }),
566        "Nat.ble" => Some(if lhs <= rhs { "true" } else { "false" }),
567        "Nat.blt" => Some(if lhs < rhs { "true" } else { "false" }),
568        _ => None,
569    }
570}
571/// Check whether the expression is already in weak-head normal form
572/// without performing any reduction.
573///
574/// An expression is in WHNF if:
575/// - It is a Sort, Lit, FVar, or Const that is not a defined definition.
576/// - It is a Lambda (since we only reduce applications, not under binders).
577/// - It is a Pi type.
578/// - It is a stuck application (the head is not a lambda/const-with-def).
579#[allow(dead_code)]
580pub fn is_whnf(expr: &Expr) -> bool {
581    match expr {
582        Expr::Sort(_)
583        | Expr::Lit(_)
584        | Expr::FVar(_)
585        | Expr::Lam(_, _, _, _)
586        | Expr::Pi(_, _, _, _)
587        | Expr::Let(_, _, _, _) => true,
588        Expr::Const(_, _) => true,
589        Expr::BVar(_) => true,
590        Expr::App(f, _) => match f.as_ref() {
591            Expr::Lam(_, _, _, _) => false,
592            _ => is_whnf(f),
593        },
594        Expr::Proj(_, _, _) => false,
595    }
596}
597/// Compute the "head" of an expression after stripping all App layers.
598#[allow(dead_code)]
599pub fn head_of(expr: &Expr) -> &Expr {
600    match expr {
601        Expr::App(f, _) => head_of(f),
602        _ => expr,
603    }
604}
605/// Count how many arguments are applied in an App chain.
606#[allow(dead_code)]
607pub fn app_arity(expr: &Expr) -> usize {
608    match expr {
609        Expr::App(f, _) => 1 + app_arity(f),
610        _ => 0,
611    }
612}
613#[cfg(test)]
614mod extra_reduce_tests {
615    use super::*;
616    use crate::{BinderInfo, Level};
617    #[test]
618    fn test_reduction_rule_display() {
619        assert_eq!(ReductionRule::Beta.to_string(), "beta");
620        assert_eq!(ReductionRule::Delta.to_string(), "delta");
621        assert_eq!(ReductionRule::Iota.to_string(), "iota");
622        assert_eq!(ReductionRule::None.to_string(), "none");
623    }
624    #[test]
625    fn test_reduction_trace_enabled() {
626        let mut trace = ReductionTrace::enabled();
627        let before = Expr::Lit(Literal::Nat(1));
628        let after = Expr::Lit(Literal::Nat(2));
629        trace.record(ReductionRule::Beta, before.clone(), after.clone());
630        assert_eq!(trace.step_count(), 1);
631        assert_eq!(trace.count_rule(&ReductionRule::Beta), 1);
632        assert_eq!(trace.count_rule(&ReductionRule::Delta), 0);
633    }
634    #[test]
635    fn test_reduction_trace_disabled() {
636        let mut trace = ReductionTrace::disabled();
637        let e = Expr::Lit(Literal::Nat(1));
638        trace.record(ReductionRule::Beta, e.clone(), e.clone());
639        assert_eq!(trace.step_count(), 0);
640    }
641    #[test]
642    fn test_reducer_stats_total() {
643        let stats = ReducerStats {
644            whnf_calls: 10,
645            cache_hits: 3,
646            beta_count: 4,
647            delta_count: 2,
648            iota_count: 1,
649            zeta_count: 1,
650            nat_lit_count: 2,
651        };
652        assert_eq!(stats.total_reductions(), 10);
653    }
654    #[test]
655    fn test_reducer_stats_cache_hit_rate() {
656        let stats = ReducerStats {
657            whnf_calls: 10,
658            cache_hits: 5,
659            ..Default::default()
660        };
661        assert!((stats.cache_hit_rate() - 0.5).abs() < 1e-10);
662    }
663    #[test]
664    fn test_eval_nat_binop_add() {
665        assert_eq!(eval_nat_binop("Nat.add", 3, 4), Some(7));
666    }
667    #[test]
668    fn test_eval_nat_binop_sub_saturating() {
669        assert_eq!(eval_nat_binop("Nat.sub", 3, 10), Some(0));
670    }
671    #[test]
672    fn test_eval_nat_binop_div_zero() {
673        assert_eq!(eval_nat_binop("Nat.div", 7, 0), Some(0));
674    }
675    #[test]
676    fn test_eval_nat_binop_gcd() {
677        assert_eq!(eval_nat_binop("Nat.gcd", 12, 8), Some(4));
678    }
679    #[test]
680    fn test_eval_nat_binop_lcm() {
681        assert_eq!(eval_nat_binop("Nat.lcm", 4, 6), Some(12));
682    }
683    #[test]
684    fn test_eval_nat_binop_land() {
685        assert_eq!(eval_nat_binop("Nat.land", 0b1100, 0b1010), Some(0b1000));
686    }
687    #[test]
688    fn test_eval_nat_cmp_beq_true() {
689        assert_eq!(eval_nat_cmp("Nat.beq", 5, 5), Some("true"));
690    }
691    #[test]
692    fn test_eval_nat_cmp_beq_false() {
693        assert_eq!(eval_nat_cmp("Nat.beq", 5, 6), Some("false"));
694    }
695    #[test]
696    fn test_eval_nat_cmp_ble() {
697        assert_eq!(eval_nat_cmp("Nat.ble", 3, 5), Some("true"));
698        assert_eq!(eval_nat_cmp("Nat.ble", 5, 3), Some("false"));
699    }
700    #[test]
701    fn test_is_whnf_sort() {
702        assert!(is_whnf(&Expr::Sort(Level::zero())));
703    }
704    #[test]
705    fn test_is_whnf_lit() {
706        assert!(is_whnf(&Expr::Lit(Literal::Nat(42))));
707    }
708    #[test]
709    fn test_is_whnf_lam() {
710        let lam = Expr::Lam(
711            BinderInfo::Default,
712            Name::str("x"),
713            Box::new(Expr::Sort(Level::zero())),
714            Box::new(Expr::BVar(0)),
715        );
716        assert!(is_whnf(&lam));
717    }
718    #[test]
719    fn test_is_whnf_redex() {
720        let lam = Expr::Lam(
721            BinderInfo::Default,
722            Name::str("x"),
723            Box::new(Expr::Sort(Level::zero())),
724            Box::new(Expr::BVar(0)),
725        );
726        let redex = Expr::App(Box::new(lam), Box::new(Expr::Lit(Literal::Nat(1))));
727        assert!(!is_whnf(&redex));
728    }
729    #[test]
730    fn test_head_of_nested_app() {
731        let f = Expr::Const(Name::str("f"), vec![]);
732        let app1 = Expr::App(Box::new(f.clone()), Box::new(Expr::Lit(Literal::Nat(1))));
733        let app2 = Expr::App(Box::new(app1), Box::new(Expr::Lit(Literal::Nat(2))));
734        assert_eq!(*head_of(&app2), f);
735    }
736    #[test]
737    fn test_app_arity() {
738        let f = Expr::Const(Name::str("f"), vec![]);
739        let app1 = Expr::App(Box::new(f.clone()), Box::new(Expr::Lit(Literal::Nat(1))));
740        let app2 = Expr::App(Box::new(app1), Box::new(Expr::Lit(Literal::Nat(2))));
741        assert_eq!(app_arity(&app2), 2);
742        assert_eq!(app_arity(&f), 0);
743    }
744    #[test]
745    fn test_trace_clear() {
746        let mut trace = ReductionTrace::enabled();
747        let e = Expr::Lit(Literal::Nat(0));
748        trace.record(ReductionRule::Beta, e.clone(), e.clone());
749        assert_eq!(trace.step_count(), 1);
750        trace.clear();
751        assert_eq!(trace.step_count(), 0);
752    }
753    #[test]
754    fn test_reducer_stats_display() {
755        let stats = ReducerStats::default();
756        let s = stats.display();
757        assert!(s.contains("whnf:0"));
758    }
759}
760#[cfg(test)]
761mod tests_padding_infra {
762    use super::*;
763    #[test]
764    fn test_stat_summary() {
765        let mut ss = StatSummary::new();
766        ss.record(10.0);
767        ss.record(20.0);
768        ss.record(30.0);
769        assert_eq!(ss.count(), 3);
770        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
771        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
772        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
773    }
774    #[test]
775    fn test_transform_stat() {
776        let mut ts = TransformStat::new();
777        ts.record_before(100.0);
778        ts.record_after(80.0);
779        let ratio = ts.mean_ratio().expect("ratio should be present");
780        assert!((ratio - 0.8).abs() < 1e-9);
781    }
782    #[test]
783    fn test_small_map() {
784        let mut m: SmallMap<u32, &str> = SmallMap::new();
785        m.insert(3, "three");
786        m.insert(1, "one");
787        m.insert(2, "two");
788        assert_eq!(m.get(&2), Some(&"two"));
789        assert_eq!(m.len(), 3);
790        let keys = m.keys();
791        assert_eq!(*keys[0], 1);
792        assert_eq!(*keys[2], 3);
793    }
794    #[test]
795    fn test_label_set() {
796        let mut ls = LabelSet::new();
797        ls.add("foo");
798        ls.add("bar");
799        ls.add("foo");
800        assert_eq!(ls.count(), 2);
801        assert!(ls.has("bar"));
802        assert!(!ls.has("baz"));
803    }
804    #[test]
805    fn test_config_node() {
806        let mut root = ConfigNode::section("root");
807        let child = ConfigNode::leaf("key", "value");
808        root.add_child(child);
809        assert_eq!(root.num_children(), 1);
810    }
811    #[test]
812    fn test_versioned_record() {
813        let mut vr = VersionedRecord::new(0u32);
814        vr.update(1);
815        vr.update(2);
816        assert_eq!(*vr.current(), 2);
817        assert_eq!(vr.version(), 2);
818        assert!(vr.has_history());
819        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
820    }
821    #[test]
822    fn test_simple_dag() {
823        let mut dag = SimpleDag::new(4);
824        dag.add_edge(0, 1);
825        dag.add_edge(1, 2);
826        dag.add_edge(2, 3);
827        assert!(dag.can_reach(0, 3));
828        assert!(!dag.can_reach(3, 0));
829        let order = dag.topological_sort().expect("order should be present");
830        assert_eq!(order, vec![0, 1, 2, 3]);
831    }
832    #[test]
833    fn test_focus_stack() {
834        let mut fs: FocusStack<&str> = FocusStack::new();
835        fs.focus("a");
836        fs.focus("b");
837        assert_eq!(fs.current(), Some(&"b"));
838        assert_eq!(fs.depth(), 2);
839        fs.blur();
840        assert_eq!(fs.current(), Some(&"a"));
841    }
842}
843#[cfg(test)]
844mod tests_extra_iterators {
845    use super::*;
846    #[test]
847    fn test_window_iterator() {
848        let data = vec![1u32, 2, 3, 4, 5];
849        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
850        assert_eq!(windows.len(), 3);
851        assert_eq!(windows[0], &[1, 2, 3]);
852        assert_eq!(windows[2], &[3, 4, 5]);
853    }
854    #[test]
855    fn test_non_empty_vec() {
856        let mut nev = NonEmptyVec::singleton(10u32);
857        nev.push(20);
858        nev.push(30);
859        assert_eq!(nev.len(), 3);
860        assert_eq!(*nev.first(), 10);
861        assert_eq!(*nev.last(), 30);
862    }
863}
864#[cfg(test)]
865mod tests_padding2 {
866    use super::*;
867    #[test]
868    fn test_sliding_sum() {
869        let mut ss = SlidingSum::new(3);
870        ss.push(1.0);
871        ss.push(2.0);
872        ss.push(3.0);
873        assert!((ss.sum() - 6.0).abs() < 1e-9);
874        ss.push(4.0);
875        assert!((ss.sum() - 9.0).abs() < 1e-9);
876        assert_eq!(ss.count(), 3);
877    }
878    #[test]
879    fn test_path_buf() {
880        let mut pb = PathBuf::new();
881        pb.push("src");
882        pb.push("main");
883        assert_eq!(pb.as_str(), "src/main");
884        assert_eq!(pb.depth(), 2);
885        pb.pop();
886        assert_eq!(pb.as_str(), "src");
887    }
888    #[test]
889    fn test_string_pool() {
890        let mut pool = StringPool::new();
891        let s = pool.take();
892        assert!(s.is_empty());
893        pool.give("hello".to_string());
894        let s2 = pool.take();
895        assert!(s2.is_empty());
896        assert_eq!(pool.free_count(), 0);
897    }
898    #[test]
899    fn test_transitive_closure() {
900        let mut tc = TransitiveClosure::new(4);
901        tc.add_edge(0, 1);
902        tc.add_edge(1, 2);
903        tc.add_edge(2, 3);
904        assert!(tc.can_reach(0, 3));
905        assert!(!tc.can_reach(3, 0));
906        let r = tc.reachable_from(0);
907        assert_eq!(r.len(), 4);
908    }
909    #[test]
910    fn test_token_bucket() {
911        let mut tb = TokenBucket::new(100, 10);
912        assert_eq!(tb.available(), 100);
913        assert!(tb.try_consume(50));
914        assert_eq!(tb.available(), 50);
915        assert!(!tb.try_consume(60));
916        assert_eq!(tb.capacity(), 100);
917    }
918    #[test]
919    fn test_rewrite_rule_set() {
920        let mut rrs = RewriteRuleSet::new();
921        rrs.add(RewriteRule::unconditional(
922            "beta",
923            "App(Lam(x, b), v)",
924            "b[x:=v]",
925        ));
926        rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
927        assert_eq!(rrs.len(), 2);
928        assert_eq!(rrs.unconditional_rules().len(), 1);
929        assert_eq!(rrs.conditional_rules().len(), 1);
930        assert!(rrs.get("beta").is_some());
931        let disp = rrs
932            .get("beta")
933            .expect("element at \'beta\' should exist")
934            .display();
935        assert!(disp.contains("→"));
936    }
937}
938#[cfg(test)]
939mod tests_padding3 {
940    use super::*;
941    #[test]
942    fn test_decision_node() {
943        let tree = DecisionNode::Branch {
944            key: "x".into(),
945            val: "1".into(),
946            yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
947            no_branch: Box::new(DecisionNode::Leaf("no".into())),
948        };
949        let mut ctx = std::collections::HashMap::new();
950        ctx.insert("x".into(), "1".into());
951        assert_eq!(tree.evaluate(&ctx), "yes");
952        ctx.insert("x".into(), "2".into());
953        assert_eq!(tree.evaluate(&ctx), "no");
954        assert_eq!(tree.depth(), 1);
955    }
956    #[test]
957    fn test_flat_substitution() {
958        let mut sub = FlatSubstitution::new();
959        sub.add("foo", "bar");
960        sub.add("baz", "qux");
961        assert_eq!(sub.apply("foo and baz"), "bar and qux");
962        assert_eq!(sub.len(), 2);
963    }
964    #[test]
965    fn test_stopwatch() {
966        let mut sw = Stopwatch::start();
967        sw.split();
968        sw.split();
969        assert_eq!(sw.num_splits(), 2);
970        assert!(sw.elapsed_ms() >= 0.0);
971        for &s in sw.splits() {
972            assert!(s >= 0.0);
973        }
974    }
975    #[test]
976    fn test_either2() {
977        let e: Either2<i32, &str> = Either2::First(42);
978        assert!(e.is_first());
979        let mapped = e.map_first(|x| x * 2);
980        assert_eq!(mapped.first(), Some(84));
981        let e2: Either2<i32, &str> = Either2::Second("hello");
982        assert!(e2.is_second());
983        assert_eq!(e2.second(), Some("hello"));
984    }
985    #[test]
986    fn test_write_once() {
987        let wo: WriteOnce<u32> = WriteOnce::new();
988        assert!(!wo.is_written());
989        assert!(wo.write(42));
990        assert!(!wo.write(99));
991        assert_eq!(wo.read(), Some(42));
992    }
993    #[test]
994    fn test_sparse_vec() {
995        let mut sv: SparseVec<i32> = SparseVec::new(100);
996        sv.set(5, 10);
997        sv.set(50, 20);
998        assert_eq!(*sv.get(5), 10);
999        assert_eq!(*sv.get(50), 20);
1000        assert_eq!(*sv.get(0), 0);
1001        assert_eq!(sv.nnz(), 2);
1002        sv.set(5, 0);
1003        assert_eq!(sv.nnz(), 1);
1004    }
1005    #[test]
1006    fn test_stack_calc() {
1007        let mut calc = StackCalc::new();
1008        calc.push(3);
1009        calc.push(4);
1010        calc.add();
1011        assert_eq!(calc.peek(), Some(7));
1012        calc.push(2);
1013        calc.mul();
1014        assert_eq!(calc.peek(), Some(14));
1015    }
1016}
oxilean_kernel/reduce/functions.rs

oxilean_kernel/reduce/
functions.rs
