oxilean_kernel/simp/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::Node;
6use crate::{Expr, Literal, Name};
7use std::rc::Rc;
8
9use super::types::{
10    ConfigNode, DecisionNode, Either2, Fixture, FlatSubstitution, FocusStack, LabelSet, MinHeap,
11    NonEmptyVec, PathBuf, PrefixCounter, RewriteRule, RewriteRuleSet, SimpDirection, SimpLemma,
12    SimpLemmaSet, SimpResult, SimpleDag, SlidingSum, SmallMap, SparseVec, StackCalc, StatSummary,
13    Stopwatch, StringPool, TokenBucket, TransformStat, TransitiveClosure, VersionedRecord,
14    WindowIterator, WriteOnce,
15};
16
17/// Simplify an expression using basic rewrite rules.
18pub fn simplify(expr: &Expr) -> Expr {
19    match expr {
20        Expr::App(f, a) => {
21            let f_simp = simplify(f);
22            let a_simp = simplify(a);
23            if let Expr::Const(name, _) = &f_simp {
24                if let Some(result) = try_simplify_nat_op(name, &a_simp) {
25                    return result;
26                }
27            }
28            Expr::App(Node::new(f_simp), Node::new(a_simp))
29        }
30        Expr::Lam(bi, name, ty, body) => Expr::Lam(
31            *bi,
32            name.clone(),
33            Node::new(simplify(ty)),
34            Node::new(simplify(body)),
35        ),
36        Expr::Pi(bi, name, ty, body) => Expr::Pi(
37            *bi,
38            name.clone(),
39            Node::new(simplify(ty)),
40            Node::new(simplify(body)),
41        ),
42        Expr::Let(name, ty, val, body) => Expr::Let(
43            name.clone(),
44            Node::new(simplify(ty)),
45            Node::new(simplify(val)),
46            Node::new(simplify(body)),
47        ),
48        _ => expr.clone(),
49    }
50}
51fn try_simplify_nat_op(name: &Name, arg: &Expr) -> Option<Expr> {
52    match name.to_string().as_str() {
53        "Nat.succ" => {
54            if let Expr::Lit(Literal::Nat(n)) = arg {
55                Some(Expr::Lit(Literal::Nat(n.succ())))
56            } else {
57                None
58            }
59        }
60        _ => None,
61    }
62}
63/// Normalize an expression (reduce to normal form).
64pub fn normalize(expr: &Expr) -> Expr {
65    use crate::Reducer;
66    let mut reducer = Reducer::new();
67    let whnf = reducer.whnf(expr);
68    match &whnf {
69        Expr::Lam(bi, name, ty, body) => Expr::Lam(
70            *bi,
71            name.clone(),
72            Node::new(normalize(ty)),
73            Node::new(normalize(body)),
74        ),
75        Expr::Pi(bi, name, ty, body) => Expr::Pi(
76            *bi,
77            name.clone(),
78            Node::new(normalize(ty)),
79            Node::new(normalize(body)),
80        ),
81        Expr::App(f, a) => Expr::App(Node::new(normalize(f)), Node::new(normalize(a))),
82        _ => whnf,
83    }
84}
85/// Check if two expressions are alpha-equivalent (structurally equal).
86pub fn alpha_eq(e1: &Expr, e2: &Expr) -> bool {
87    match (e1, e2) {
88        (Expr::Sort(l1), Expr::Sort(l2)) => l1 == l2,
89        (Expr::BVar(i1), Expr::BVar(i2)) => i1 == i2,
90        (Expr::FVar(f1), Expr::FVar(f2)) => f1 == f2,
91        (Expr::Const(n1, ls1), Expr::Const(n2, ls2)) => n1 == n2 && ls1 == ls2,
92        (Expr::App(f1, a1), Expr::App(f2, a2)) => alpha_eq(f1, f2) && alpha_eq(a1, a2),
93        (Expr::Lam(_, _, ty1, b1), Expr::Lam(_, _, ty2, b2)) => {
94            alpha_eq(ty1, ty2) && alpha_eq(b1, b2)
95        }
96        (Expr::Pi(_, _, ty1, b1), Expr::Pi(_, _, ty2, b2)) => {
97            alpha_eq(ty1, ty2) && alpha_eq(b1, b2)
98        }
99        (Expr::Let(_, ty1, v1, b1), Expr::Let(_, ty2, v2, b2)) => {
100            alpha_eq(ty1, ty2) && alpha_eq(v1, v2) && alpha_eq(b1, b2)
101        }
102        (Expr::Lit(l1), Expr::Lit(l2)) => l1 == l2,
103        (Expr::Proj(n1, i1, e1), Expr::Proj(n2, i2, e2)) => {
104            n1 == n2 && i1 == i2 && alpha_eq(e1, e2)
105        }
106        _ => false,
107    }
108}
109#[cfg(test)]
110mod tests {
111    use super::*;
112    use crate::{BinderInfo, Level, Literal, Name};
113    #[test]
114    fn test_simplify_nat_succ() {
115        let expr = Expr::App(
116            Node::new(Expr::Const(Name::str("Nat.succ"), vec![])),
117            Node::new(Expr::Lit(Literal::nat(5))),
118        );
119        let result = simplify(&expr);
120        assert_eq!(result, Expr::Lit(Literal::nat(6)));
121    }
122    #[test]
123    fn test_alpha_eq_bvar() {
124        let e1 = Expr::BVar(0);
125        let e2 = Expr::BVar(0);
126        assert!(alpha_eq(&e1, &e2));
127    }
128    #[test]
129    fn test_alpha_eq_lambda() {
130        let lam1 = Expr::Lam(
131            BinderInfo::Default,
132            Name::str("x"),
133            Node::new(Expr::Sort(Level::zero())),
134            Node::new(Expr::BVar(0)),
135        );
136        let lam2 = Expr::Lam(
137            BinderInfo::Default,
138            Name::str("y"),
139            Node::new(Expr::Sort(Level::zero())),
140            Node::new(Expr::BVar(0)),
141        );
142        assert!(alpha_eq(&lam1, &lam2));
143    }
144    #[test]
145    fn test_alpha_eq_different() {
146        let e1 = Expr::Lit(Literal::nat(1));
147        let e2 = Expr::Lit(Literal::nat(2));
148        assert!(!alpha_eq(&e1, &e2));
149    }
150}
151/// Check if `expr` is headed by constant `head_name`.
152pub fn is_app_of(expr: &Expr, head_name: &str) -> bool {
153    match expr {
154        Expr::App(f, _) => is_app_of(f, head_name),
155        Expr::Const(n, _) => n.to_string() == head_name,
156        _ => false,
157    }
158}
159/// Collect the arguments of a spine application `f a1 a2 … an`.
160///
161/// Returns `(head, [a1, …, an])`.
162pub fn decompose_app(expr: &Expr) -> (&Expr, Vec<&Expr>) {
163    let mut args = Vec::new();
164    let mut current = expr;
165    while let Expr::App(f, a) = current {
166        args.push(a.as_ref());
167        current = f;
168    }
169    args.reverse();
170    (current, args)
171}
172/// Build an application spine from a head and argument list.
173pub fn mk_app(head: Expr, args: Vec<Expr>) -> Expr {
174    args.into_iter()
175        .fold(head, |f, a| Expr::App(Node::new(f), Node::new(a)))
176}
177/// Evaluate a closed Nat arithmetic expression to a literal, if possible.
178///
179/// Delegates all arithmetic to the single BigNat evaluator
180/// ([`crate::reduce::eval_nat_binop`]) so exactly one implementation of the
181/// Lean literal semantics exists in the kernel (in particular `x % 0 = x`
182/// and exact, non-wrapping `add`/`mul`/`pow`).
183pub fn eval_nat(expr: &Expr) -> Option<crate::bignat::BigNat> {
184    use crate::bignat::BigNat;
185    match expr {
186        Expr::Lit(Literal::Nat(n)) => Some(n.clone()),
187        Expr::Const(name, _) if name.to_string() == "Nat.zero" => Some(BigNat::zero()),
188        Expr::App(f, a) => {
189            if let Expr::Const(name, _) = f.as_ref() {
190                match name.to_string().as_str() {
191                    "Nat.succ" => return eval_nat(a).map(|n| n.succ()),
192                    "Nat.pred" => return eval_nat(a).map(|n| n.pred()),
193                    _ => {}
194                }
195            }
196            if let Expr::App(f2, a2) = f.as_ref() {
197                if let Expr::Const(name, _) = f2.as_ref() {
198                    let name_str = name.to_string();
199                    let lhs = eval_nat(a2)?;
200                    let rhs = eval_nat(a)?;
201                    return match name_str.as_str() {
202                        // Nat.min/Nat.max are simp-only conveniences; both
203                        // reduce to comparisons, so no arithmetic drift.
204                        "Nat.min" => Some(if lhs <= rhs { lhs } else { rhs }),
205                        "Nat.max" => Some(if lhs >= rhs { lhs } else { rhs }),
206                        op => crate::reduce::eval_nat_binop(op, &lhs, &rhs),
207                    };
208                }
209            }
210            None
211        }
212        _ => None,
213    }
214}
215/// Apply `simplify` to all sub-expressions one level deep.
216pub fn simp_congruence(expr: &Expr) -> Expr {
217    match expr {
218        Expr::App(f, a) => Expr::App(Node::new(simplify(f)), Node::new(simplify(a))),
219        Expr::Lam(bi, name, ty, body) => Expr::Lam(
220            *bi,
221            name.clone(),
222            Node::new(simplify(ty)),
223            Node::new(simplify(body)),
224        ),
225        Expr::Pi(bi, name, ty, body) => Expr::Pi(
226            *bi,
227            name.clone(),
228            Node::new(simplify(ty)),
229            Node::new(simplify(body)),
230        ),
231        Expr::Let(name, ty, val, body) => Expr::Let(
232            name.clone(),
233            Node::new(simplify(ty)),
234            Node::new(simplify(val)),
235            Node::new(simplify(body)),
236        ),
237        other => other.clone(),
238    }
239}
240/// Simplify to a maximum depth (prevents looping on large terms).
241pub fn simplify_bounded(expr: &Expr, max_depth: usize) -> Expr {
242    if max_depth == 0 {
243        return expr.clone();
244    }
245    let simp_sub = |e: &Expr| simplify_bounded(e, max_depth - 1);
246    match expr {
247        Expr::App(f, a) => {
248            let f_s = simp_sub(f);
249            let a_s = simp_sub(a);
250            if let Expr::Const(name, _) = &f_s {
251                if let Some(r) = try_simplify_nat_op(name, &a_s) {
252                    return r;
253                }
254            }
255            Expr::App(Node::new(f_s), Node::new(a_s))
256        }
257        Expr::Lam(bi, name, ty, body) => Expr::Lam(
258            *bi,
259            name.clone(),
260            Node::new(simp_sub(ty)),
261            Node::new(simp_sub(body)),
262        ),
263        Expr::Pi(bi, name, ty, body) => Expr::Pi(
264            *bi,
265            name.clone(),
266            Node::new(simp_sub(ty)),
267            Node::new(simp_sub(body)),
268        ),
269        other => other.clone(),
270    }
271}
272/// Remove eta-redexes: `(fun x => f x)` → `f` (when `x` not free in `f`).
273///
274/// This is a best-effort, single-pass eta-reduction.
275pub fn eta_reduce(expr: &Expr) -> Expr {
276    match expr {
277        Expr::Lam(_, _, _, body) => {
278            if let Expr::App(f, a) = body.as_ref() {
279                if matches!(a.as_ref(), Expr::BVar(0)) && !contains_bvar(f, 0) {
280                    return shift_bvars(f, -1, 0);
281                }
282            }
283            expr.clone()
284        }
285        _ => expr.clone(),
286    }
287}
288/// Check if an expression contains the given de Bruijn variable.
289pub fn contains_bvar(expr: &Expr, idx: u32) -> bool {
290    match expr {
291        Expr::BVar(i) => *i == idx,
292        Expr::App(f, a) => contains_bvar(f, idx) || contains_bvar(a, idx),
293        Expr::Lam(_, _, ty, body) => contains_bvar(ty, idx) || contains_bvar(body, idx + 1),
294        Expr::Pi(_, _, ty, body) => contains_bvar(ty, idx) || contains_bvar(body, idx + 1),
295        Expr::Let(_, ty, val, body) => {
296            contains_bvar(ty, idx) || contains_bvar(val, idx) || contains_bvar(body, idx + 1)
297        }
298        _ => false,
299    }
300}
301/// Shift all de Bruijn variables `≥ cutoff` by `shift` (signed).
302fn shift_bvars(expr: &Expr, shift: i32, cutoff: u32) -> Expr {
303    match expr {
304        Expr::BVar(i) => {
305            if *i >= cutoff {
306                let new_i = (*i as i32 + shift).max(0) as u32;
307                Expr::BVar(new_i)
308            } else {
309                expr.clone()
310            }
311        }
312        Expr::App(f, a) => Expr::App(
313            Node::new(shift_bvars(f, shift, cutoff)),
314            Node::new(shift_bvars(a, shift, cutoff)),
315        ),
316        Expr::Lam(bi, name, ty, body) => Expr::Lam(
317            *bi,
318            name.clone(),
319            Node::new(shift_bvars(ty, shift, cutoff)),
320            Node::new(shift_bvars(body, shift, cutoff + 1)),
321        ),
322        Expr::Pi(bi, name, ty, body) => Expr::Pi(
323            *bi,
324            name.clone(),
325            Node::new(shift_bvars(ty, shift, cutoff)),
326            Node::new(shift_bvars(body, shift, cutoff + 1)),
327        ),
328        other => other.clone(),
329    }
330}
331/// Return the AST size (number of nodes) of an expression.
332pub fn expr_size(expr: &Expr) -> usize {
333    match expr {
334        Expr::App(f, a) => 1 + expr_size(f) + expr_size(a),
335        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => 1 + expr_size(ty) + expr_size(body),
336        Expr::Let(_, ty, val, body) => 1 + expr_size(ty) + expr_size(val) + expr_size(body),
337        Expr::Proj(_, _, inner) => 1 + expr_size(inner),
338        _ => 1,
339    }
340}
341/// Return the depth (longest path to leaf) of an expression.
342pub fn expr_depth(expr: &Expr) -> usize {
343    match expr {
344        Expr::App(f, a) => 1 + expr_depth(f).max(expr_depth(a)),
345        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
346            1 + expr_depth(ty).max(expr_depth(body))
347        }
348        Expr::Let(_, ty, val, body) => {
349            1 + expr_depth(ty).max(expr_depth(val)).max(expr_depth(body))
350        }
351        Expr::Proj(_, _, inner) => 1 + expr_depth(inner),
352        _ => 0,
353    }
354}
355#[cfg(test)]
356mod simp_extra_tests {
357    use super::*;
358    use crate::Name;
359    #[test]
360    fn test_is_app_of() {
361        let e = Expr::App(
362            Node::new(Expr::App(
363                Node::new(Expr::Const(Name::str("Nat.add"), vec![])),
364                Node::new(Expr::Lit(Literal::nat(1))),
365            )),
366            Node::new(Expr::Lit(Literal::nat(2))),
367        );
368        assert!(is_app_of(&e, "Nat.add"));
369        assert!(!is_app_of(&e, "Nat.mul"));
370    }
371    #[test]
372    fn test_decompose_app() {
373        let e = Expr::App(
374            Node::new(Expr::App(
375                Node::new(Expr::Const(Name::str("f"), vec![])),
376                Node::new(Expr::Lit(Literal::nat(1))),
377            )),
378            Node::new(Expr::Lit(Literal::nat(2))),
379        );
380        let (head, args) = decompose_app(&e);
381        assert!(matches!(head, Expr::Const(_, _)));
382        assert_eq!(args.len(), 2);
383    }
384    #[test]
385    fn test_eval_nat_literal() {
386        let e = Expr::Lit(Literal::nat(42));
387        assert_eq!(eval_nat(&e), Some(crate::bignat::BigNat::from(42u64)));
388    }
389    #[test]
390    fn test_eval_nat_succ() {
391        let e = Expr::App(
392            Node::new(Expr::Const(Name::str("Nat.succ"), vec![])),
393            Node::new(Expr::Lit(Literal::nat(4))),
394        );
395        assert_eq!(eval_nat(&e), Some(crate::bignat::BigNat::from(5u64)));
396    }
397    #[test]
398    fn test_eval_nat_add() {
399        let e = Expr::App(
400            Node::new(Expr::App(
401                Node::new(Expr::Const(Name::str("Nat.add"), vec![])),
402                Node::new(Expr::Lit(Literal::nat(3))),
403            )),
404            Node::new(Expr::Lit(Literal::nat(7))),
405        );
406        assert_eq!(eval_nat(&e), Some(crate::bignat::BigNat::from(10u64)));
407    }
408    #[test]
409    fn test_eval_nat_pred() {
410        let e = Expr::App(
411            Node::new(Expr::Const(Name::str("Nat.pred"), vec![])),
412            Node::new(Expr::Lit(Literal::nat(5))),
413        );
414        assert_eq!(eval_nat(&e), Some(crate::bignat::BigNat::from(4u64)));
415        let e_zero = Expr::App(
416            Node::new(Expr::Const(Name::str("Nat.pred"), vec![])),
417            Node::new(Expr::Lit(Literal::nat(0))),
418        );
419        assert_eq!(eval_nat(&e_zero), Some(crate::bignat::BigNat::from(0u64)));
420    }
421    #[test]
422    fn test_eval_nat_pow() {
423        let e = Expr::App(
424            Node::new(Expr::App(
425                Node::new(Expr::Const(Name::str("Nat.pow"), vec![])),
426                Node::new(Expr::Lit(Literal::nat(2))),
427            )),
428            Node::new(Expr::Lit(Literal::nat(3))),
429        );
430        assert_eq!(eval_nat(&e), Some(crate::bignat::BigNat::from(8u64)));
431    }
432    #[test]
433    fn test_simplify_nat_succ_chain() {
434        let e = Expr::App(
435            Node::new(Expr::Const(Name::str("Nat.succ"), vec![])),
436            Node::new(Expr::App(
437                Node::new(Expr::Const(Name::str("Nat.succ"), vec![])),
438                Node::new(Expr::Lit(Literal::nat(0))),
439            )),
440        );
441        let result = simplify(&e);
442        assert_eq!(result, Expr::Lit(Literal::nat(2)));
443    }
444    #[test]
445    fn test_contains_bvar() {
446        assert!(contains_bvar(&Expr::BVar(0), 0));
447        assert!(!contains_bvar(&Expr::BVar(1), 0));
448        let app = Expr::App(Node::new(Expr::BVar(0)), Node::new(Expr::BVar(1)));
449        assert!(contains_bvar(&app, 0));
450        assert!(contains_bvar(&app, 1));
451        assert!(!contains_bvar(&app, 2));
452    }
453    #[test]
454    fn test_expr_size() {
455        let lit = Expr::Lit(Literal::nat(1));
456        assert_eq!(expr_size(&lit), 1);
457        let app = Expr::App(Node::new(lit.clone()), Node::new(lit.clone()));
458        assert_eq!(expr_size(&app), 3);
459    }
460    #[test]
461    fn test_expr_depth() {
462        let lit = Expr::Lit(Literal::nat(1));
463        assert_eq!(expr_depth(&lit), 0);
464        let app = Expr::App(Node::new(lit.clone()), Node::new(lit.clone()));
465        assert_eq!(expr_depth(&app), 1);
466    }
467    #[test]
468    fn test_simp_lemma_reversed() {
469        let lhs = Expr::Lit(Literal::nat(1));
470        let rhs = Expr::Lit(Literal::nat(2));
471        let lemma = SimpLemma::forward(Name::str("test"), lhs.clone(), rhs.clone());
472        assert_eq!(lemma.direction, SimpDirection::Forward);
473        let rev = lemma.reversed();
474        assert_eq!(rev.direction, SimpDirection::Backward);
475    }
476    #[test]
477    fn test_mk_app() {
478        let head = Expr::Const(Name::str("f"), vec![]);
479        let args = vec![Expr::Lit(Literal::nat(1)), Expr::Lit(Literal::nat(2))];
480        let e = mk_app(head, args);
481        assert!(matches!(e, Expr::App(_, _)));
482    }
483    #[test]
484    fn test_simplify_bounded_depth_zero() {
485        let e = Expr::App(
486            Node::new(Expr::Const(Name::str("Nat.succ"), vec![])),
487            Node::new(Expr::Lit(Literal::nat(5))),
488        );
489        let result = simplify_bounded(&e, 0);
490        assert_eq!(result, e);
491    }
492    #[test]
493    fn test_alpha_eq_lit() {
494        let e1 = Expr::Lit(Literal::nat(42));
495        let e2 = Expr::Lit(Literal::nat(42));
496        let e3 = Expr::Lit(Literal::nat(43));
497        assert!(alpha_eq(&e1, &e2));
498        assert!(!alpha_eq(&e1, &e3));
499    }
500    #[test]
501    fn test_eta_reduce_no_change() {
502        let e = Expr::Lit(Literal::nat(5));
503        assert_eq!(eta_reduce(&e), e);
504    }
505}
506/// Check whether `expr` is a Nat literal with value `n`.
507pub fn is_nat_lit(expr: &Expr, n: u64) -> bool {
508    matches!(expr, Expr::Lit(Literal::Nat(m)) if * m == n)
509}
510/// Check whether `expr` is `Nat.zero` or the literal `0`.
511pub fn is_zero(expr: &Expr) -> bool {
512    is_nat_lit(expr, 0) || matches!(expr, Expr::Const(name, _) if name.to_string() == "Nat.zero")
513}
514/// Check whether `expr` is `Nat.succ _`.
515pub fn is_succ(expr: &Expr) -> bool {
516    matches!(
517        expr, Expr::App(f, _) if matches!(f.as_ref(), Expr::Const(name, _) if name
518        .to_string() == "Nat.succ")
519    )
520}
521/// Extract the predecessor from a `Nat.succ n` expression.
522pub fn succ_of(expr: &Expr) -> Option<&Expr> {
523    if let Expr::App(f, a) = expr {
524        if matches!(f.as_ref(), Expr::Const(name, _) if name.to_string() == "Nat.succ") {
525            return Some(a);
526        }
527    }
528    None
529}
530/// Apply a single rewrite rule `lhs = rhs` throughout `expr`.
531///
532/// Returns `(new_expr, changed)`.
533pub fn rewrite_once(expr: &Expr, lhs: &Expr, rhs: &Expr) -> (Expr, bool) {
534    if alpha_eq(expr, lhs) {
535        return (rhs.clone(), true);
536    }
537    let mut changed = false;
538    let new_expr = match expr {
539        Expr::App(f, a) => {
540            let (new_f, c1) = rewrite_once(f, lhs, rhs);
541            let (new_a, c2) = rewrite_once(a, lhs, rhs);
542            changed = c1 || c2;
543            Expr::App(Node::new(new_f), Node::new(new_a))
544        }
545        Expr::Lam(bi, name, ty, body) => {
546            let (new_ty, c1) = rewrite_once(ty, lhs, rhs);
547            let (new_body, c2) = rewrite_once(body, lhs, rhs);
548            changed = c1 || c2;
549            Expr::Lam(*bi, name.clone(), Node::new(new_ty), Node::new(new_body))
550        }
551        Expr::Pi(bi, name, ty, body) => {
552            let (new_ty, c1) = rewrite_once(ty, lhs, rhs);
553            let (new_body, c2) = rewrite_once(body, lhs, rhs);
554            changed = c1 || c2;
555            Expr::Pi(*bi, name.clone(), Node::new(new_ty), Node::new(new_body))
556        }
557        other => other.clone(),
558    };
559    (new_expr, changed)
560}
561/// Apply a rewrite rule exhaustively until no more rewrites are possible.
562pub fn rewrite_all(expr: &Expr, lhs: &Expr, rhs: &Expr) -> Expr {
563    let mut current = expr.clone();
564    loop {
565        let (new_expr, changed) = rewrite_once(&current, lhs, rhs);
566        if !changed {
567            return current;
568        }
569        current = new_expr;
570    }
571}
572/// Collect all `FVarId`s appearing in `expr`.
573pub fn free_vars(expr: &Expr) -> Vec<crate::FVarId> {
574    let mut result = Vec::new();
575    free_vars_rec(expr, &mut result);
576    result.sort_by_key(|fv| fv.0);
577    result.dedup_by_key(|fv| fv.0);
578    result
579}
580fn free_vars_rec(expr: &Expr, out: &mut Vec<crate::FVarId>) {
581    match expr {
582        Expr::FVar(fv) => out.push(*fv),
583        Expr::App(f, a) => {
584            free_vars_rec(f, out);
585            free_vars_rec(a, out);
586        }
587        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
588            free_vars_rec(ty, out);
589            free_vars_rec(body, out);
590        }
591        Expr::Let(_, ty, val, body) => {
592            free_vars_rec(ty, out);
593            free_vars_rec(val, out);
594            free_vars_rec(body, out);
595        }
596        Expr::Proj(_, _, inner) => free_vars_rec(inner, out),
597        _ => {}
598    }
599}
600/// Return `true` if `expr` contains no free variables.
601pub fn is_closed(expr: &Expr) -> bool {
602    free_vars(expr).is_empty()
603}
604#[cfg(test)]
605mod simp_extra_tests2 {
606    use super::*;
607    use crate::{FVarId, Name};
608    #[test]
609    fn test_is_nat_lit() {
610        assert!(is_nat_lit(&Expr::Lit(Literal::nat(5)), 5));
611        assert!(!is_nat_lit(&Expr::Lit(Literal::nat(5)), 6));
612    }
613    #[test]
614    fn test_is_zero() {
615        assert!(is_zero(&Expr::Lit(Literal::nat(0))));
616        assert!(is_zero(&Expr::Const(Name::str("Nat.zero"), vec![])));
617        assert!(!is_zero(&Expr::Lit(Literal::nat(1))));
618    }
619    #[test]
620    fn test_is_succ_and_succ_of() {
621        let succ_n = Expr::App(
622            Node::new(Expr::Const(Name::str("Nat.succ"), vec![])),
623            Node::new(Expr::Lit(Literal::nat(3))),
624        );
625        assert!(is_succ(&succ_n));
626        assert!(succ_of(&succ_n).is_some());
627        assert!(!is_succ(&Expr::Lit(Literal::nat(5))));
628        assert!(succ_of(&Expr::Lit(Literal::nat(5))).is_none());
629    }
630    #[test]
631    fn test_rewrite_once() {
632        let lhs = Expr::Lit(Literal::nat(1));
633        let rhs = Expr::Lit(Literal::nat(99));
634        let expr = Expr::App(
635            Node::new(Expr::Const(Name::str("f"), vec![])),
636            Node::new(lhs.clone()),
637        );
638        let (new_expr, changed) = rewrite_once(&expr, &lhs, &rhs);
639        assert!(changed);
640        if let Expr::App(_, a) = &new_expr {
641            assert_eq!(a.as_ref(), &rhs);
642        } else {
643            panic!("expected App");
644        }
645    }
646    #[test]
647    fn test_rewrite_all() {
648        let lhs = Expr::Lit(Literal::nat(0));
649        let rhs = Expr::Lit(Literal::nat(100));
650        let expr = Expr::App(
651            Node::new(Expr::App(
652                Node::new(Expr::Const(Name::str("f"), vec![])),
653                Node::new(lhs.clone()),
654            )),
655            Node::new(lhs.clone()),
656        );
657        let result = rewrite_all(&expr, &lhs, &rhs);
658        let size = expr_size(&result);
659        assert!(size >= 3);
660    }
661    #[test]
662    fn test_free_vars() {
663        let expr = Expr::FVar(FVarId(42));
664        let fvs = free_vars(&expr);
665        assert_eq!(fvs.len(), 1);
666        assert_eq!(fvs[0].0, 42);
667    }
668    #[test]
669    fn test_is_closed() {
670        let lit = Expr::Lit(Literal::nat(5));
671        assert!(is_closed(&lit));
672        let fvar = Expr::FVar(FVarId(1));
673        assert!(!is_closed(&fvar));
674    }
675    #[test]
676    fn test_decompose_app_single() {
677        let e = Expr::Const(Name::str("x"), vec![]);
678        let (head, args) = decompose_app(&e);
679        assert!(matches!(head, Expr::Const(_, _)));
680        assert!(args.is_empty());
681    }
682}
683/// Apply a `SimpLemmaSet` and record which lemmas were used.
684pub fn simp_with_trace(expr: &Expr, set: &SimpLemmaSet) -> SimpResult {
685    let mut current = expr.clone();
686    let mut applied = Vec::new();
687    let mut any_changed = false;
688    loop {
689        let mut pass_changed = false;
690        for lemma in set.iter() {
691            let (new_expr, c) =
692                rewrite_once(&current, lemma.effective_lhs(), lemma.effective_rhs());
693            if c {
694                current = new_expr;
695                applied.push(lemma.name.clone());
696                pass_changed = true;
697                any_changed = true;
698            }
699        }
700        if !pass_changed {
701            break;
702        }
703    }
704    if any_changed {
705        SimpResult::simplified(current, applied)
706    } else {
707        SimpResult::unchanged(current)
708    }
709}
710/// Check if `expr` is the constant `True`.
711pub fn is_true(expr: &Expr) -> bool {
712    matches!(expr, Expr::Const(name, _) if name.to_string() == "True")
713}
714/// Check if `expr` is the constant `False`.
715pub fn is_false_expr(expr: &Expr) -> bool {
716    matches!(expr, Expr::Const(name, _) if name.to_string() == "False")
717}
718/// Check if `expr` is `Prop` (Sort 0).
719pub fn is_prop(expr: &Expr) -> bool {
720    matches!(expr, Expr::Sort(l) if l.is_zero())
721}
722/// Fold constant Nat arithmetic in an expression (recursive).
723///
724/// Eagerly evaluates `Nat.add`, `Nat.mul`, `Nat.sub`, `Nat.succ`
725/// wherever both operands are literals.
726pub fn fold_nat_constants(expr: &Expr) -> Expr {
727    match expr {
728        Expr::App(f, a) => {
729            let f2 = fold_nat_constants(f);
730            let a2 = fold_nat_constants(a);
731            if let Some(n) = eval_nat(&Expr::App(Node::new(f2.clone()), Node::new(a2.clone()))) {
732                Expr::Lit(Literal::Nat(n))
733            } else {
734                Expr::App(Node::new(f2), Node::new(a2))
735            }
736        }
737        Expr::Lam(bi, n, ty, body) => Expr::Lam(
738            *bi,
739            n.clone(),
740            Node::new(fold_nat_constants(ty)),
741            Node::new(fold_nat_constants(body)),
742        ),
743        Expr::Pi(bi, n, ty, body) => Expr::Pi(
744            *bi,
745            n.clone(),
746            Node::new(fold_nat_constants(ty)),
747            Node::new(fold_nat_constants(body)),
748        ),
749        other => other.clone(),
750    }
751}
752#[cfg(test)]
753mod simp_set_tests {
754    use super::*;
755    use crate::Name;
756    fn mk_lit(n: u64) -> Expr {
757        Expr::Lit(Literal::nat(n))
758    }
759    fn mk_c(s: &str) -> Expr {
760        Expr::Const(Name::str(s), vec![])
761    }
762    #[test]
763    fn test_simp_lemma_set_empty() {
764        let set = SimpLemmaSet::new();
765        assert!(set.is_empty());
766        let (result, changed) = set.apply_once(&mk_lit(1));
767        assert!(!changed);
768        assert_eq!(result, mk_lit(1));
769    }
770    #[test]
771    fn test_simp_lemma_set_apply_once() {
772        let mut set = SimpLemmaSet::new();
773        let lhs = mk_lit(0);
774        let rhs = mk_lit(100);
775        set.add(SimpLemma::forward(
776            Name::str("zero_to_hundred"),
777            lhs.clone(),
778            rhs.clone(),
779        ));
780        let (result, changed) = set.apply_once(&lhs);
781        assert!(changed);
782        assert_eq!(result, rhs);
783    }
784    #[test]
785    fn test_simp_lemma_set_apply_all() {
786        let mut set = SimpLemmaSet::new();
787        let a = mk_lit(1);
788        let b = mk_lit(2);
789        let c = mk_lit(3);
790        set.add(SimpLemma::forward(Name::str("r1"), a.clone(), b.clone()));
791        set.add(SimpLemma::forward(Name::str("r2"), b.clone(), c.clone()));
792        let result = set.apply_all(&a);
793        assert_eq!(result, c);
794    }
795    #[test]
796    fn test_simp_lemma_set_find() {
797        let mut set = SimpLemmaSet::new();
798        let lemma = SimpLemma::forward(Name::str("myRule"), mk_lit(0), mk_lit(1));
799        set.add(lemma);
800        assert!(set.find(&Name::str("myRule")).is_some());
801        assert!(set.find(&Name::str("unknownRule")).is_none());
802    }
803    #[test]
804    fn test_simp_with_trace_no_change() {
805        let set = SimpLemmaSet::new();
806        let e = mk_lit(5);
807        let result = simp_with_trace(&e, &set);
808        assert!(!result.changed);
809        assert_eq!(result.expr, e);
810    }
811    #[test]
812    fn test_simp_with_trace_change() {
813        let mut set = SimpLemmaSet::new();
814        let lhs = mk_lit(0);
815        let rhs = mk_lit(99);
816        set.add(SimpLemma::forward(Name::str("r"), lhs.clone(), rhs.clone()));
817        let result = simp_with_trace(&lhs, &set);
818        assert!(result.changed);
819        assert_eq!(result.expr, rhs);
820        assert_eq!(result.applied.len(), 1);
821    }
822    #[test]
823    fn test_is_true() {
824        assert!(is_true(&mk_c("True")));
825        assert!(!is_true(&mk_c("False")));
826        assert!(!is_true(&mk_lit(1)));
827    }
828    #[test]
829    fn test_is_false_expr() {
830        assert!(is_false_expr(&mk_c("False")));
831        assert!(!is_false_expr(&mk_c("True")));
832    }
833    #[test]
834    fn test_is_prop() {
835        use crate::Level;
836        assert!(is_prop(&Expr::Sort(Level::zero())));
837        assert!(!is_prop(&Expr::Sort(Level::succ(Level::zero()))));
838    }
839    #[test]
840    fn test_fold_nat_constants_succ() {
841        let e = Expr::App(
842            Node::new(Expr::Const(Name::str("Nat.succ"), vec![])),
843            Node::new(mk_lit(3)),
844        );
845        let result = fold_nat_constants(&e);
846        assert_eq!(result, mk_lit(4));
847    }
848    #[test]
849    fn test_fold_nat_constants_no_change() {
850        let e = mk_lit(7);
851        let result = fold_nat_constants(&e);
852        assert_eq!(result, e);
853    }
854    #[test]
855    fn test_simp_result_unchanged() {
856        let e = mk_lit(1);
857        let r = SimpResult::unchanged(e.clone());
858        assert!(!r.changed);
859        assert_eq!(r.expr, e);
860    }
861    #[test]
862    fn test_simp_result_simplified() {
863        let e = mk_lit(2);
864        let r = SimpResult::simplified(e.clone(), vec![Name::str("ruleX")]);
865        assert!(r.changed);
866        assert_eq!(r.applied.len(), 1);
867    }
868}
869#[cfg(test)]
870mod tests_padding_infra {
871    use super::*;
872    #[test]
873    fn test_stat_summary() {
874        let mut ss = StatSummary::new();
875        ss.record(10.0);
876        ss.record(20.0);
877        ss.record(30.0);
878        assert_eq!(ss.count(), 3);
879        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
880        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
881        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
882    }
883    #[test]
884    fn test_transform_stat() {
885        let mut ts = TransformStat::new();
886        ts.record_before(100.0);
887        ts.record_after(80.0);
888        let ratio = ts.mean_ratio().expect("ratio should be present");
889        assert!((ratio - 0.8).abs() < 1e-9);
890    }
891    #[test]
892    fn test_small_map() {
893        let mut m: SmallMap<u32, &str> = SmallMap::new();
894        m.insert(3, "three");
895        m.insert(1, "one");
896        m.insert(2, "two");
897        assert_eq!(m.get(&2), Some(&"two"));
898        assert_eq!(m.len(), 3);
899        let keys = m.keys();
900        assert_eq!(*keys[0], 1);
901        assert_eq!(*keys[2], 3);
902    }
903    #[test]
904    fn test_label_set() {
905        let mut ls = LabelSet::new();
906        ls.add("foo");
907        ls.add("bar");
908        ls.add("foo");
909        assert_eq!(ls.count(), 2);
910        assert!(ls.has("bar"));
911        assert!(!ls.has("baz"));
912    }
913    #[test]
914    fn test_config_node() {
915        let mut root = ConfigNode::section("root");
916        let child = ConfigNode::leaf("key", "value");
917        root.add_child(child);
918        assert_eq!(root.num_children(), 1);
919    }
920    #[test]
921    fn test_versioned_record() {
922        let mut vr = VersionedRecord::new(0u32);
923        vr.update(1);
924        vr.update(2);
925        assert_eq!(*vr.current(), 2);
926        assert_eq!(vr.version(), 2);
927        assert!(vr.has_history());
928        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
929    }
930    #[test]
931    fn test_simple_dag() {
932        let mut dag = SimpleDag::new(4);
933        dag.add_edge(0, 1);
934        dag.add_edge(1, 2);
935        dag.add_edge(2, 3);
936        assert!(dag.can_reach(0, 3));
937        assert!(!dag.can_reach(3, 0));
938        let order = dag.topological_sort().expect("order should be present");
939        assert_eq!(order, vec![0, 1, 2, 3]);
940    }
941    #[test]
942    fn test_focus_stack() {
943        let mut fs: FocusStack<&str> = FocusStack::new();
944        fs.focus("a");
945        fs.focus("b");
946        assert_eq!(fs.current(), Some(&"b"));
947        assert_eq!(fs.depth(), 2);
948        fs.blur();
949        assert_eq!(fs.current(), Some(&"a"));
950    }
951}
952#[cfg(test)]
953mod tests_extra_iterators {
954    use super::*;
955    #[test]
956    fn test_window_iterator() {
957        let data = vec![1u32, 2, 3, 4, 5];
958        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
959        assert_eq!(windows.len(), 3);
960        assert_eq!(windows[0], &[1, 2, 3]);
961        assert_eq!(windows[2], &[3, 4, 5]);
962    }
963    #[test]
964    fn test_non_empty_vec() {
965        let mut nev = NonEmptyVec::singleton(10u32);
966        nev.push(20);
967        nev.push(30);
968        assert_eq!(nev.len(), 3);
969        assert_eq!(*nev.first(), 10);
970        assert_eq!(*nev.last(), 30);
971    }
972}
973#[cfg(test)]
974mod tests_padding2 {
975    use super::*;
976    #[test]
977    fn test_sliding_sum() {
978        let mut ss = SlidingSum::new(3);
979        ss.push(1.0);
980        ss.push(2.0);
981        ss.push(3.0);
982        assert!((ss.sum() - 6.0).abs() < 1e-9);
983        ss.push(4.0);
984        assert!((ss.sum() - 9.0).abs() < 1e-9);
985        assert_eq!(ss.count(), 3);
986    }
987    #[test]
988    fn test_path_buf() {
989        let mut pb = PathBuf::new();
990        pb.push("src");
991        pb.push("main");
992        assert_eq!(pb.as_str(), "src/main");
993        assert_eq!(pb.depth(), 2);
994        pb.pop();
995        assert_eq!(pb.as_str(), "src");
996    }
997    #[test]
998    fn test_string_pool() {
999        let mut pool = StringPool::new();
1000        let s = pool.take();
1001        assert!(s.is_empty());
1002        pool.give("hello".to_string());
1003        let s2 = pool.take();
1004        assert!(s2.is_empty());
1005        assert_eq!(pool.free_count(), 0);
1006    }
1007    #[test]
1008    fn test_transitive_closure() {
1009        let mut tc = TransitiveClosure::new(4);
1010        tc.add_edge(0, 1);
1011        tc.add_edge(1, 2);
1012        tc.add_edge(2, 3);
1013        assert!(tc.can_reach(0, 3));
1014        assert!(!tc.can_reach(3, 0));
1015        let r = tc.reachable_from(0);
1016        assert_eq!(r.len(), 4);
1017    }
1018    #[test]
1019    fn test_token_bucket() {
1020        let mut tb = TokenBucket::new(100, 0);
1021        assert_eq!(tb.available(), 100);
1022        assert!(tb.try_consume(50));
1023        assert_eq!(tb.available(), 50);
1024        assert!(!tb.try_consume(60));
1025        assert_eq!(tb.capacity(), 100);
1026    }
1027    #[test]
1028    fn test_rewrite_rule_set() {
1029        let mut rrs = RewriteRuleSet::new();
1030        rrs.add(RewriteRule::unconditional(
1031            "beta",
1032            "App(Lam(x, b), v)",
1033            "b[x:=v]",
1034        ));
1035        rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
1036        assert_eq!(rrs.len(), 2);
1037        assert_eq!(rrs.unconditional_rules().len(), 1);
1038        assert_eq!(rrs.conditional_rules().len(), 1);
1039        assert!(rrs.get("beta").is_some());
1040        let disp = rrs
1041            .get("beta")
1042            .expect("element at \'beta\' should exist")
1043            .display();
1044        assert!(disp.contains("→"));
1045    }
1046}
1047#[cfg(test)]
1048mod tests_padding3 {
1049    use super::*;
1050    #[test]
1051    fn test_decision_node() {
1052        let tree = DecisionNode::Branch {
1053            key: "x".into(),
1054            val: "1".into(),
1055            yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
1056            no_branch: Box::new(DecisionNode::Leaf("no".into())),
1057        };
1058        let mut ctx = std::collections::HashMap::new();
1059        ctx.insert("x".into(), "1".into());
1060        assert_eq!(tree.evaluate(&ctx), "yes");
1061        ctx.insert("x".into(), "2".into());
1062        assert_eq!(tree.evaluate(&ctx), "no");
1063        assert_eq!(tree.depth(), 1);
1064    }
1065    #[test]
1066    fn test_flat_substitution() {
1067        let mut sub = FlatSubstitution::new();
1068        sub.add("foo", "bar");
1069        sub.add("baz", "qux");
1070        assert_eq!(sub.apply("foo and baz"), "bar and qux");
1071        assert_eq!(sub.len(), 2);
1072    }
1073    #[test]
1074    fn test_stopwatch() {
1075        let mut sw = Stopwatch::start();
1076        sw.split();
1077        sw.split();
1078        assert_eq!(sw.num_splits(), 2);
1079        assert!(sw.elapsed_ms() >= 0.0);
1080        for &s in sw.splits() {
1081            assert!(s >= 0.0);
1082        }
1083    }
1084    #[test]
1085    fn test_either2() {
1086        let e: Either2<i32, &str> = Either2::First(42);
1087        assert!(e.is_first());
1088        let mapped = e.map_first(|x| x * 2);
1089        assert_eq!(mapped.first(), Some(84));
1090        let e2: Either2<i32, &str> = Either2::Second("hello");
1091        assert!(e2.is_second());
1092        assert_eq!(e2.second(), Some("hello"));
1093    }
1094    #[test]
1095    fn test_write_once() {
1096        let wo: WriteOnce<u32> = WriteOnce::new();
1097        assert!(!wo.is_written());
1098        assert!(wo.write(42));
1099        assert!(!wo.write(99));
1100        assert_eq!(wo.read(), Some(42));
1101    }
1102    #[test]
1103    fn test_sparse_vec() {
1104        let mut sv: SparseVec<i32> = SparseVec::new(100);
1105        sv.set(5, 10);
1106        sv.set(50, 20);
1107        assert_eq!(*sv.get(5), 10);
1108        assert_eq!(*sv.get(50), 20);
1109        assert_eq!(*sv.get(0), 0);
1110        assert_eq!(sv.nnz(), 2);
1111        sv.set(5, 0);
1112        assert_eq!(sv.nnz(), 1);
1113    }
1114    #[test]
1115    fn test_stack_calc() {
1116        let mut calc = StackCalc::new();
1117        calc.push(3);
1118        calc.push(4);
1119        assert_eq!(calc.add(), Some(7));
1120        assert_eq!(calc.peek(), Some(7));
1121        calc.push(2);
1122        assert_eq!(calc.mul(), Some(14));
1123        assert_eq!(calc.peek(), Some(14));
1124    }
1125}
1126#[cfg(test)]
1127mod tests_final_padding {
1128    use super::*;
1129    #[test]
1130    fn test_min_heap() {
1131        let mut h = MinHeap::new();
1132        h.push(5u32);
1133        h.push(1u32);
1134        h.push(3u32);
1135        assert_eq!(h.peek(), Some(&1));
1136        assert_eq!(h.pop(), Some(1));
1137        assert_eq!(h.pop(), Some(3));
1138        assert_eq!(h.pop(), Some(5));
1139        assert!(h.is_empty());
1140    }
1141    #[test]
1142    fn test_prefix_counter() {
1143        let mut pc = PrefixCounter::new();
1144        pc.record("hello");
1145        pc.record("help");
1146        pc.record("world");
1147        assert_eq!(pc.count_with_prefix("hel"), 2);
1148        assert_eq!(pc.count_with_prefix("wor"), 1);
1149        assert_eq!(pc.count_with_prefix("xyz"), 0);
1150    }
1151    #[test]
1152    fn test_fixture() {
1153        let mut f = Fixture::new();
1154        f.set("key1", "val1");
1155        f.set("key2", "val2");
1156        assert_eq!(f.get("key1"), Some("val1"));
1157        assert_eq!(f.get("key3"), None);
1158        assert_eq!(f.len(), 2);
1159    }
1160}
oxilean_kernel/simp/functions.rs

oxilean_kernel/simp/
functions.rs
