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,
  )

  }

  #[test]
  fn abstract_fvars_position_mapping() {
    let mut env = InternTable::<Anon>::new();
    let fv0 = AE::fvar(FVarId(0), ());
    let fv1 = AE::fvar(FVarId(1), ());
    let app = AE::app(fv0, fv1);
    // [fv0, fv1]: fv0 outermost (Var(1)), fv1 innermost (Var(0))
    let result = abstract_fvars(&mut env, &app, &[FVarId(0), FVarId(1)]);
    let expected = AE::app(AE::var(1, ()), AE::var(0, ()));
    assert_eq!(result, expected);
  }

  #[test]
  fn abstract_fvars_unrelated_pass_through() {
    let mut env = InternTable::<Anon>::new();
    let fv0 = AE::fvar(FVarId(0), ());
    let fv2 = AE::fvar(FVarId(2), ());
    // fv2 is not in the abstraction list → unchanged
    let result = abstract_fvars(&mut env, &fv2, &[FVarId(0), FVarId(1)]);
    assert!(result.ptr_eq(&fv2));
    let _ = fv0; // silence unused
  }

  #[test]
  fn abstract_fvars_lifts_loose_bvars() {
    let mut env = InternTable::<Anon>::new();
    let fv0 = AE::fvar(FVarId(0), ());
    let v0 = AE::var(0, ());
    let app = AE::app(fv0, v0);
    // Wrap one new binder around `app`; fv0 → Var(0); existing Var(0)
    // (loose) shifts up to Var(1).
    let result = abstract_fvars(&mut env, &app, &[FVarId(0)]);
    let expected = AE::app(AE::var(0, ()), AE::var(1, ()));
    assert_eq!(result, expected);
  }

  #[test]
  fn instantiate_rev_then_abstract_roundtrip() {
    let mut env = InternTable::<Anon>::new();
    // Body: λ. App(#0, #1) — under one extra binder; Var(0) is the inner
    // peeled binder, Var(1) is the outer one.
    let nat = AE::cnst(KId::new(mk_addr("Nat"), ()), Box::new([]));