| 4838 | let head = Name::str(head, "below".to_string()); |
| 4839 | let head_addr = Address::hash(b"A.below"); |
| 4840 | stt.name_to_addr.insert(head.clone(), head_addr); |
| 4841 | |
| 4842 | stt.below_call_site_plans.insert( |
| 4843 | head.clone(), |
| 4844 | surgery::BRecOnCallSitePlan { |
| 4845 | n_params: 0, |
| 4846 | n_source_motives: 4, |
| 4847 | n_indices: 0, |
| 4848 | motive_keep: vec![true, true, true, true], |
| 4849 | source_to_canon_motive: vec![0, 3, 1, 2], |
| 4850 | }, |
| 4851 | ); |
| 4852 | |
| 4853 | let mut expr = LeanExpr::cnst(head.clone(), vec![]); |
| 4854 | for i in 10..=14u64 { |
| 4855 | expr = LeanExpr::app(expr, LeanExpr::bvar(Nat::from(i))); |
| 4856 | } |
| 4857 | |
| 4858 | let mut cache = BlockCache { |
| 4859 | compiling: Some(Name::str(Name::anon(), "caller".to_string())), |
| 4860 | ..BlockCache::default() |
| 4861 | }; |
| 4862 | let result = |
| 4863 | compile_expr(&expr, &[], &MutCtx::default(), &mut cache, &stt).unwrap(); |
| 4864 | |
| 4865 | fn app_args(e: &Arc<Expr>) -> Vec<u64> { |
| 4866 | let mut cur = e.clone(); |
| 4867 | let mut args = Vec::new(); |
| 4868 | while let Expr::App(f, a) = cur.as_ref() { |
| 4869 | match a.as_ref() { |
| 4870 | Expr::Var(i) => args.push(*i), |
| 4871 | other => panic!("expected Var arg, got {other:?}"), |
| 4872 | } |
| 4873 | cur = f.clone(); |
| 4874 | } |
| 4875 | match cur.as_ref() { |
| 4876 | Expr::Ref(0, lvls) => assert!(lvls.is_empty()), |
| 4877 | other => panic!("expected Ref head, got {other:?}"), |
| 4878 | } |
| 4879 | args.reverse(); |
| 4880 | args |
| 4881 | } |
| 4882 | |
| 4883 | assert_eq!(app_args(&result), vec![10, 12, 13, 11, 14]); |
| 4884 | } |