Build env with a nested inductive: Tree with a field `List Tree`. Tree : Sort 1 Tree.leaf : Tree Tree.node : List Tree → Tree This should create a flat block [Tree, List] with Tree nesting into List.
()
| 5069 | // Skip the recursor constant for now. |
| 5070 | |
| 5071 | env.blocks.insert( |
| 5072 | block, |
| 5073 | vec![mk_id("List"), mk_id("List.nil"), mk_id("List.cons")], |
| 5074 | ); |
| 5075 | env |
| 5076 | } |
| 5077 | |
| 5078 | #[test] |
| 5079 | fn check_list_inductive() { |
| 5080 | let mut env = list_env(); |
| 5081 | let mut tc = TypeChecker::new(&mut env); |
| 5082 | assert!(tc.check_const(&mk_id("List")).is_ok()); |
| 5083 | // Verify recursor was generated with the right structure |
| 5084 | let block = mk_id("List"); |
| 5085 | let generated = |
| 5086 | tc.env.recursor_cache.get(&block).expect("recursor should be cached"); |
| 5087 | assert_eq!(generated.len(), 1, "should generate 1 recursor for List"); |
| 5088 | assert_eq!(generated[0].ind_addr, mk_addr("List")); |
| 5089 | |
| 5090 | // Count binders in generated rec type |
| 5091 | let mut n = 0; |
| 5092 | let mut cur = generated[0].ty.clone(); |
| 5093 | while let ExprData::All(_, _, _, body, _) = cur.data() { |
| 5094 | n += 1; |
| 5095 | cur = body.clone(); |
| 5096 | } |
| 5097 | // List.rec should have: 1 param + 1 motive + 2 minors + 0 indices + 1 major = 5 binders |
| 5098 | assert_eq!(n, 5, "List.rec should have 5 binders"); |
| 5099 | } |
| 5100 | |
| 5101 | /// Build env with a nested inductive: Tree with a field `List Tree`. |
| 5102 | /// Tree : Sort 1 |
| 5103 | /// Tree.leaf : Tree |
| 5104 | /// Tree.node : List Tree → Tree |
| 5105 | /// This should create a flat block [Tree, List] with Tree nesting into List. |
| 5106 | fn nested_tree_env() -> KEnv<Anon> { |
| 5107 | let mut env = KEnv::new(); |
| 5108 | let tree_block = mk_id("Tree"); |
| 5109 | let tree = || cnst("Tree", &[]); |
| 5110 | |
| 5111 | // Tree : Sort 1 |
| 5112 | env.insert( |
| 5113 | mk_id("Tree"), |
| 5114 | KConst::Indc { |
| 5115 | name: (), |
| 5116 | level_params: (), |
| 5117 | lvls: 0, |
| 5118 | params: 0, |
| 5119 | indices: 0, |
| 5120 | is_unsafe: false, |
| 5121 | block: tree_block.clone(), |
| 5122 | member_idx: 0, |
| 5123 | ty: sort1(), |
| 5124 | ctors: vec![mk_id("Tree.leaf"), mk_id("Tree.node")], |
| 5125 | lean_all: (), |
| 5126 | }, |
| 5127 | ); |
| 5128 | env.insert( |