test: add type check tests

This commit is contained in:
Shunsuke Shibayama 2023-02-20 22:29:44 +09:00
parent caae853036
commit d0c53e456e
5 changed files with 92 additions and 1 deletions

View file

@ -12,6 +12,19 @@ use crate::context::instantiate::TyVarCache;
use crate::context::Context;
impl Context {
pub fn assert_var_type(&self, varname: &str, ty: &Type) -> Result<(), ()> {
let Some((_, vi)) = self.get_var_info(varname) else {
panic!("variable not found: {varname}");
};
println!("{varname}: {}", vi.t);
if self.subtype_of(&vi.t, ty) && self.subtype_of(ty, &vi.t) {
Ok(())
} else {
println!("{varname} is not the type of {ty}");
Err(())
}
}
pub fn test_refinement_subtyping(&self) -> Result<(), ()> {
// Nat :> {I: Int | I >= 1} ?
let lhs = Nat;