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

oxilean_kernel/simp/
functions.rs
