| 4404 | |
| 4405 | #[test] |
| 4406 | fn test_compile_name_str() { |
| 4407 | let stt = CompileState::default(); |
| 4408 | let name = Name::str(Name::anon(), "foo".to_string()); |
| 4409 | let addr = compile_name(&name, &stt); |
| 4410 | // Name is stored in env.names |
| 4411 | let stored_name = stt.env.names.get(&addr).unwrap(); |
| 4412 | assert_eq!(*stored_name, name); |
| 4413 | // String component should be in blobs |
| 4414 | let foo_bytes = "foo".as_bytes(); |
| 4415 | let foo_addr = Address::hash(foo_bytes); |
| 4416 | assert!(stt.env.blobs.contains_key(&foo_addr)); |
| 4417 | } |
| 4418 | |
| 4419 | #[test] |
| 4420 | fn test_compile_expr_bvar() { |
| 4421 | let stt = CompileState::default(); |
| 4422 | let mut cache = BlockCache::default(); |
| 4423 | let expr = LeanExpr::bvar(Nat::from(3u64)); |
| 4424 | let result = |
| 4425 | compile_expr(&expr, &[], &MutCtx::default(), &mut cache, &stt).unwrap(); |
| 4426 | assert!(matches!(result.as_ref(), Expr::Var(3))); |
| 4427 | } |
| 4428 | |
| 4429 | #[test] |
| 4430 | fn test_compile_expr_sort() { |
| 4431 | let stt = CompileState::default(); |
| 4432 | let mut cache = BlockCache::default(); |
| 4433 | let expr = LeanExpr::sort(Level::zero()); |
| 4434 | let result = |
| 4435 | compile_expr(&expr, &[], &MutCtx::default(), &mut cache, &stt).unwrap(); |
| 4436 | match result.as_ref() { |
| 4437 | Expr::Sort(idx) => { |
| 4438 | assert_eq!(*idx, 0); |
| 4439 | assert!(matches!( |
| 4440 | cache.univs.get_index(0).unwrap().as_ref(), |
| 4441 | Univ::Zero |
| 4442 | )); |
| 4443 | }, |
| 4444 | _ => panic!("expected Sort"), |
| 4445 | } |
| 4446 | } |
| 4447 | |
| 4448 | #[test] |
| 4449 | fn test_compile_expr_app() { |
| 4450 | let stt = CompileState::default(); |
| 4451 | let mut cache = BlockCache::default(); |
| 4452 | let f = LeanExpr::bvar(Nat::from(0u64)); |
| 4453 | let a = LeanExpr::bvar(Nat::from(1u64)); |
| 4454 | let expr = LeanExpr::app(f, a); |
| 4455 | let result = |
| 4456 | compile_expr(&expr, &[], &MutCtx::default(), &mut cache, &stt).unwrap(); |
| 4457 | match result.as_ref() { |
| 4458 | Expr::App(f, a) => { |
| 4459 | assert!(matches!(f.as_ref(), Expr::Var(0))); |
| 4460 | assert!(matches!(a.as_ref(), Expr::Var(1))); |
| 4461 | }, |
| 4462 | _ => panic!("expected App"), |
| 4463 | } |