Polymorphic nested: PTree.{u} : Sort (u+1) → Sort (u+1) Like Tree but with one universe param and one type param. PTree.leaf.{u} : ∀ (α : Sort (u+1)), α → PTree.{u} α PTree.node.{u} : ∀ (α : Sort (u+1)), List.{u+1} (PTree.{u} α) → PTree.{u} α
()
| 5372 | let mut tc = TypeChecker::new(&mut env); |
| 5373 | tc.check_const(&mk_id("Tree")).unwrap(); |
| 5374 | |
| 5375 | let tree_block = mk_id("Tree"); |
| 5376 | let generated = tc.env.recursor_cache.get(&tree_block).unwrap(); |
| 5377 | |
| 5378 | // Count binders in Tree.rec (member 0) |
| 5379 | let count_binders = |e: &AE| -> usize { |
| 5380 | let mut n = 0; |
| 5381 | let mut c = e.clone(); |
| 5382 | while let ExprData::All(_, _, _, b, _) = c.data() { |
| 5383 | n += 1; |
| 5384 | c = b.clone(); |
| 5385 | } |
| 5386 | n |
| 5387 | }; |
| 5388 | |
| 5389 | let tree_rec = &generated[0]; |
| 5390 | // Tree.rec: 0 params + 2 motives + (2 + 2) minors + 0 indices + 1 major = 7 |
| 5391 | // Minors: Tree.leaf (0 fields, 0 IH), Tree.node (1 field + 1 IH = 2) |
| 5392 | // List.nil (0 fields, 0 IH), List.cons (2 fields + 2 IH = 4) |
| 5393 | // Wait — minors for Tree.rec include ALL ctors of ALL flat members. |
| 5394 | // Tree: leaf (0 binders), node (1 field + 1 IH = 2 binders) |
| 5395 | // List(aux): nil (0 binders), cons (2 fields + 2 IH = 4 binders) |
| 5396 | // But minors are individual forall types, not nested. Each minor is ONE forall domain. |
| 5397 | // So: 2 motives + 4 minors + 1 major = 7 binders total (0 params, 0 indices) |
| 5398 | let n = count_binders(&tree_rec.ty); |
| 5399 | assert_eq!( |
| 5400 | n, 7, |
| 5401 | "Tree.rec should have 7 binders (2 motives + 4 minors + 1 major), got {n}" |
| 5402 | ); |
| 5403 | |
| 5404 | // List auxiliary rec (member 1) |
| 5405 | let list_rec = &generated[1]; |
| 5406 | // List aux rec for List Tree: |
| 5407 | // 0 params + 2 motives + 4 minors + 0 indices + 1 major = 7 |
| 5408 | let n = count_binders(&list_rec.ty); |
| 5409 | assert_eq!(n, 7, "List aux rec should have 7 binders, got {n}"); |
| 5410 | } |
| 5411 | |
| 5412 | /// Polymorphic nested: PTree.{u} : Sort (u+1) → Sort (u+1) |
| 5413 | /// Like Tree but with one universe param and one type param. |
| 5414 | /// PTree.leaf.{u} : ∀ (α : Sort (u+1)), α → PTree.{u} α |
| 5415 | /// PTree.node.{u} : ∀ (α : Sort (u+1)), List.{u+1} (PTree.{u} α) → PTree.{u} α |
| 5416 | fn poly_nested_env() -> KEnv<Anon> { |
| 5417 | let mut env = KEnv::new(); |
| 5418 | let block = mk_id("PTree"); |
| 5419 | let su = || AU::succ(param(0)); // u+1 |
| 5420 | |
| 5421 | // PTree.{u} : Sort(u+1) → Sort(u+1) |
| 5422 | let ptree_ty = pi(AE::sort(su()), AE::sort(su())); |
| 5423 | env.insert( |
| 5424 | mk_id("PTree"), |
| 5425 | KConst::Indc { |
| 5426 | name: (), |
| 5427 | level_params: (), |
| 5428 | lvls: 1, |
| 5429 | params: 1, |
| 5430 | indices: 0, |
| 5431 | is_unsafe: false, |