Function gen_expr

crates/kernel/src/subst.rs:1369–1407

Generate a bounded-depth `KExpr ` with de Bruijn indices in `0..=max_var`. Leaf distribution is biased toward concrete data (Var/Sort/Const) to produce meaningful expressions.

(
    env: &mut InternTable<Anon>,
    rng: &mut Prng,
    depth: u32,
    max_var: u64,
  )

    let expected_closed = AE::app(AE::var(0, ()), AE::var(1, ()));
    assert_eq!(closed, expected_closed);
  }

  #[test]
  fn simul_subst_basic() {
    let mut env = InternTable::<Anon>::new();
    let v0 = AE::var(0, ());
    let v1 = AE::var(1, ());
    let app = AE::app(v1, v0); // App(Var(1), Var(0))

    let a = AE::nat(Nat::from(1u64), mk_addr("a"));
    let b = AE::nat(Nat::from(2u64), mk_addr("b"));

    // simul_subst([a, b], depth=0):
    //   Var(0) → substs[0] = a
    //   Var(1) → substs[1] = b
    let result = simul_subst(&mut env, &app, &[a.clone(), b.clone()], 0);
    let expected = AE::app(b, a);
    assert_eq!(result, expected);
  }

  #[test]
  fn simul_subst_shift() {
    let mut env = InternTable::<Anon>::new();
    let v2 = AE::var(2, ());

    let a = AE::nat(Nat::from(1u64), mk_addr("a"));
    let b = AE::nat(Nat::from(2u64), mk_addr("b"));

    // Var(2) >= depth+2 → shifted to Var(0)
    let result = simul_subst(&mut env, &v2, &[a, b], 0);
    assert_eq!(result, AE::var(0, ()));
  }

  #[test]
  fn intern_dedup() {
    let mut env = InternTable::<Anon>::new();
    let _v0 = AE::var(0, ());
    let v2 = AE::var(2, ());
    let arg = AE::nat(Nat::from(3u64), mk_addr("3"));

    // Two substitutions producing the same result should be pointer-equal after interning
    let r1 = subst(&mut env, &v2, &arg, 0);