Function test_compile_simple_def

crates/compile/src/compile.rs:4352–4403

()

    let level = Level::param(name.clone());
    let mut cache = BlockCache::default();
    let univ = compile_univ(&level, &[name], &mut cache).unwrap();
    assert!(matches!(univ.as_ref(), Univ::Var(0)));
  }

  #[test]
  fn test_compile_univ_max() {
    let level = Level::max(Level::zero(), Level::succ(Level::zero()));
    let mut cache = BlockCache::default();
    let univ = compile_univ(&level, &[], &mut cache).unwrap();
    match univ.as_ref() {
      Univ::Max(a, b) => {
        assert!(matches!(a.as_ref(), Univ::Zero));
        match b.as_ref() {
          Univ::Succ(inner) => assert!(matches!(inner.as_ref(), Univ::Zero)),
          _ => panic!("expected Succ"),
        }
      },
      _ => panic!("expected Max"),
    }
  }

  #[test]
  fn test_store_string() {
    let stt = CompileState::default();
    let addr1 = store_string("hello", &stt);
    let addr2 = store_string("hello", &stt);
    // Same content should give same address
    assert_eq!(addr1, addr2);
    // Check we can retrieve it
    let bytes = stt.env.get_blob(&addr1).unwrap();
    assert_eq!(bytes, b"hello");
  }

  #[test]
  fn test_store_nat() {
    let stt = CompileState::default();
    let n = Nat::from(42u64);
    let addr = store_nat(&n, &stt);
    let bytes = stt.env.get_blob(&addr).unwrap();
    let n2 = Nat::from_le_bytes(&bytes);
    assert_eq!(n, n2);
  }

  #[test]
  fn test_compile_name_anon() {
    let stt = CompileState::default();
    let name = Name::anon();
    let addr = compile_name(&name, &stt);
    // Name is stored in env.names, not blobs
    let stored_name = stt.env.names.get(&addr).unwrap();
    assert_eq!(*stored_name, name);
  }

  #[test]
  fn test_compile_name_str() {