oxilean_kernel/simp/
functions.rs

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

oxilean_kernel/simp/
functions.rs
