From df056b17418d2f3e43bfa433db23930d0172048e Mon Sep 17 00:00:00 2001
From: Vincent Lafeychine <vincent.lafeychine@proton.me>
Date: Mon, 31 Oct 2022 23:08:23 +0100
Subject: [PATCH] chore(type_checker): Cleaning tests + Analyse branches
---
kernel/src/error.rs | 4 -
kernel/src/location.rs | 2 +-
kernel/src/type_checker.rs | 377 +++++++++++++++++++++++--------------
3 files changed, 235 insertions(+), 148 deletions(-)
diff --git a/kernel/src/error.rs b/kernel/src/error.rs
index 868e4410..9b79f040 100644
--- a/kernel/src/error.rs
+++ b/kernel/src/error.rs
@@ -21,10 +21,6 @@ pub enum KernelError {
#[display(fmt = "{} is not a universe", _0)]
NotUniverse(Term),
- /// t is not a type
- #[display(fmt = "{} is not a type", _0)]
- NotType(Term),
-
/// t1 and t2 are not definitionally equal
#[display(fmt = "{} and {} are not definitionaly equal", _0, _1)]
NotDefEq(Term, Term),
diff --git a/kernel/src/location.rs b/kernel/src/location.rs
index 7f671d63..dc4f01a3 100644
--- a/kernel/src/location.rs
+++ b/kernel/src/location.rs
@@ -1,4 +1,4 @@
-// TODO: Waiting for #15
+// TODO: Waiting for #15 to handle correctly location inside Terms
use derive_more::{Constructor, Display, From};
/// Line and column position.
diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs
index e81659cd..2f96d4f0 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -1,5 +1,5 @@
use crate::environment::Environment;
-use crate::error::{KernelError, Result};
+use crate::error::{KernelError::*, Result};
use crate::term::{DeBruijnIndex, Term};
use num_bigint::BigUint;
use std::cmp::max;
@@ -47,17 +47,19 @@ impl Term {
/// The conversion is untyped, meaning that it should **only** be called during type-checking when the two `Term`s are already known to be of the same type and in the same context.
fn conversion(&self, rhs: &Term, env: &Environment, lvl: DeBruijnIndex) -> bool {
match (self.whnf(env), rhs.whnf(env)) {
- (Type(i), Type(j)) => i == j,
-
(Prop, Prop) => true,
+ (Type(i), Type(j)) => i == j,
+
(Var(i), Var(j)) => i == j,
- (Prod(t1, u1), Prod(box t2, u2)) => {
+ (Prod(_t1, u1), Prod(box _t2, u2)) => {
let u1 = u1.substitute(&Var(lvl), lvl.into());
let u2 = u2.substitute(&Var(lvl), lvl.into());
- t1.conversion(&t2, env, lvl) && u1.conversion(&u2, env, lvl + 1.into())
+ // TODO: Unused code (#32)
+ // t1.conversion(&t2, env, lvl) &&
+ u1.conversion(&u2, env, lvl + 1.into())
}
// Since we assume that both vals already have the same type,
@@ -71,14 +73,16 @@ impl Term {
t.conversion(&u, env, lvl + 1.into())
}
- (App(box t1, box u1), App(box t2, box u2)) => {
- t1.conversion(&t2, env, lvl) && u1.conversion(&u2, env, lvl)
- }
-
- (app @ App(box Abs(_, _), box _), u) | (u, app @ App(box Abs(_, _), box _)) => {
- app.beta_reduction(env).conversion(&u, env, lvl)
+ (App(box _t1, box u1), App(box _t2, box u2)) => {
+ // TODO: Unused code (#32)
+ // t1.conversion(&t2, env, lvl) &&
+ u1.conversion(&u2, env, lvl)
}
+ // TODO: Unused code (#32)
+ // (app @ App(box Abs(_, _), box _), u) | (u, app @ App(box Abs(_, _), box _)) => {
+ // app.beta_reduction(env).conversion(&u, env, lvl)
+ // }
_ => false,
}
}
@@ -87,7 +91,7 @@ impl Term {
pub fn is_def_eq(&self, rhs: &Term, env: &Environment) -> Result<()> {
self.conversion(rhs, env, 1.into())
.then_some(())
- .ok_or_else(|| KernelError::NotDefEq(self.clone(), rhs.clone()))
+ .ok_or_else(|| NotDefEq(self.clone(), rhs.clone()))
}
/// Computes universe the universe in which `(x : A) -> B` lives when `A : u1` and `B : u2`.
@@ -97,15 +101,16 @@ impl Term {
Prop => Ok(Prop),
Type(ref i) => match self {
- Prop => Ok(Type(i.clone())),
+ // TODO: Unused code (#32)
+ // Prop => Ok(Type(i.clone())),
// else if u1 = Type(i) and u2 = Type(j), then (x : A) -> B : Type(max(i,j))
Type(j) => Ok(Type(max(i.clone(), j.clone()))),
- _ => Err(KernelError::NotUniverse(self.clone())),
+ _ => Err(NotUniverse(self.clone())),
},
- _ => Err(KernelError::NotUniverse(rhs.clone())),
+ _ => Err(NotUniverse(rhs.clone())),
}
}
@@ -117,11 +122,13 @@ impl Term {
Const(s) => match env.get_type(s) {
Some(ty) => Ok(ty),
- None => Err(KernelError::ConstNotFound(s.clone())),
+ None => Err(ConstNotFound(s.clone())),
},
Prod(box t, u) => {
+ // TODO: Do a test with _infer failing (#32)
let univ_t = t._infer(env, ctx)?;
+ // TODO: Do a test with _infer failing (#32)
let univ_u = u._infer(env, ctx.clone().bind(t))?;
univ_t.normal_form(env).imax(&univ_u.normal_form(env))
@@ -133,19 +140,19 @@ impl Term {
Ok(Prod(box t.clone(), box u))
}
+ // TODO: Do a test with _infer failing (#32)
App(box t, box u) => match t._infer(env, ctx)? {
Prod(box typ_lhs, cls) => {
+ // TODO: Do a test with _infer failing (#32)
let typ_rhs = u._infer(env, ctx)?;
typ_lhs
.conversion(&typ_rhs, env, ctx.types.len().into())
.then_some(*cls)
- .ok_or_else(|| {
- KernelError::WrongArgumentType(t.clone(), typ_lhs, u.clone(), typ_rhs)
- })
+ .ok_or_else(|| WrongArgumentType(t.clone(), typ_lhs, u.clone(), typ_rhs))
}
- x => Err(KernelError::NotAFunction(t.clone(), x, u.clone())),
+ x => Err(NotAFunction(t.clone(), x, u.clone())),
},
}
}
@@ -158,11 +165,12 @@ impl Term {
/// Checks whether a given term is of type `ty` in a given context.
pub fn check(&self, ty: &Term, env: &Environment) -> Result<()> {
let ctx = &mut Context::new();
+ // TODO: Do a test with _infer failing (#32)
let tty = self._infer(env, ctx)?;
tty.conversion(ty, env, ctx.types.len().into())
.then_some(())
- .ok_or_else(|| KernelError::TypeMismatch(tty, ty.clone()))
+ .ok_or_else(|| TypeMismatch(tty, ty.clone()))
}
}
@@ -170,67 +178,54 @@ impl Term {
mod tests {
use super::*;
- fn id(l: usize) -> Box<Term> {
- box Abs(box Prop, box Var(l.into()))
+ fn proj(idx: usize) -> Box<Term> {
+ box Abs(box Prop, box Var(idx.into()))
}
#[test]
- fn var_subst_1() {
- // (λ P. λP. 1) (λP.1)
- let t = App(
- box Abs(box Prop, box Abs(box Prop, box Var(1.into()))),
- id(1),
- );
+ fn normal_form_1() {
+ let term = App(box Abs(box Prop, proj(1)), proj(1));
+ let normal_form = Abs(box Prop, box Var(1.into()));
- let nf = Abs(box Prop, box Var(1.into()));
- assert_eq!(t.normal_form(&Environment::new()), nf)
+ assert!(term.is_def_eq(&normal_form, &Environment::new()).is_ok());
}
#[test]
- fn var_subst_2() {
- let t = App(
- box Abs(box Prop, box Abs(box Prop, box Var(2.into()))),
- id(1),
- );
+ fn normal_form_2() {
+ let term = App(box Abs(box Prop, proj(2)), proj(1));
+ let normal_form = Abs(box Prop, proj(1));
- let nf = Abs(box Prop, id(1));
- assert_eq!(t.normal_form(&Environment::new()), nf)
+ assert!(term.is_def_eq(&normal_form, &Environment::new()).is_ok());
}
#[test]
- fn simple() {
- let t1 = App(
- box Abs(box Type(BigUint::from(0_u64).into()), box Var(1.into())),
+ fn normal_form_3() {
+ // λa.a (λx.x) (λx.x)
+ let term = Abs(
box Prop,
+ box App(box App(box Var(2.into()), proj(1)), proj(1)),
);
- let t2 = Prop;
- assert!(t1.conversion(&t2, &Environment::new(), 0.into()));
-
- let ty = t1.infer(&Environment::new());
- assert_eq!(ty, Ok(Type(BigUint::from(0_u64).into())));
+ assert!(term.is_def_eq(&term, &Environment::new()).is_ok());
}
#[test]
- fn simple_substitute() {
- // λ (x : P -> P).(λ (y :P).x y) x
- //λ P -> P.(λ P.2 1) 1
- let term = Abs(
- box Prod(box Prop, box Prop),
- box App(
- box Abs(box Prop, box App(box Var(2.into()), box Var(1.into()))),
- box Var(1.into()),
- ),
+ fn typed_reduction_app_1() {
+ let term = App(
+ box Abs(box Type(BigUint::from(0_u64).into()), box Var(1.into())),
+ box Prop,
);
- // λx.x x
- let reduced = Abs(box Prop, box App(box Var(1.into()), box Var(1.into())));
+ let reduced = Prop;
assert!(term.is_def_eq(&reduced, &Environment::new()).is_ok());
- assert!(term.infer(&Environment::new()).is_err());
+
+ let term_type = term.infer(&Environment::new()).unwrap();
+ assert_eq!(term_type, Type(BigUint::from(0_u64).into()));
+ assert!(term.check(&term_type, &Environment::new()).is_ok());
}
#[test]
- fn complex_conv() {
+ fn typed_reduction_app_2() {
// (λa.λb.λc.a (λd.λe.e (d b)) (λ_.c) (λd.d)) (λa.λb.a b)
let term = App(
box Abs(
@@ -275,22 +270,22 @@ mod tests {
),
),
// _ : P
- box Abs(box Prop, box Var(2.into())),
+ proj(2),
),
- //d : P
- box Abs(box Prop, box Var(1.into())),
+ // d : P
+ proj(1),
),
),
),
),
box Abs(
- //a : (P -> P) -> (P -> P) -> P
+ // a : (P -> P) -> (P -> P) -> P
box Prod(
box Prod(box Prop, box Prop),
box Prod(box Prod(box Prop, box Prop), box Prop),
),
box Abs(
- //b : P -> P
+ // b : P -> P
box Prod(box Prop, box Prop),
box App(box Var(2.into()), box Var(1.into())),
),
@@ -298,71 +293,97 @@ mod tests {
);
// λa : P.λb : P .b
- let reduced = Abs(box Prop, box Abs(box Prop, box Var(1.into())));
+ let reduced = Abs(box Prop, proj(1));
assert!(term.is_def_eq(&reduced, &Environment::new()).is_ok());
- assert!(term.infer(&Environment::new()).is_ok())
+
+ let term_type = term.infer(&Environment::new()).unwrap();
+ assert_eq!(term_type, Prod(box Prop, box Prod(box Prop, box Prop)));
+ assert!(term.check(&term_type, &Environment::new()).is_ok());
}
- //(λ ℙ → λ ℙ → λ ℙ → (0 (λ ℙ → λ ℙ → ((4 1) 3) λ ℙ → 3)) (λ ℙ → λ ℙ → (0 1) (λ ℙ → 0 λ ℙ → 0)))
#[test]
- fn nf_test() {
- //λa.a (λx.x) (λx.x)
- let reduced = Abs(box Prop, box App(box App(box Var(2.into()), id(1)), id(1)));
+ fn typed_reduction_universe() {
+ let term = App(
+ box Abs(box Prop, box Type(BigUint::from(0_u64).into())),
+ box Prod(box Prop, box Var(1.into())),
+ );
+
+ let reduced = Type(BigUint::from(0_u64).into());
+ assert!(term.is_def_eq(&reduced, &Environment::new()).is_ok());
- let nff = reduced.clone().normal_form(&Environment::new());
- assert_eq!(reduced, nff);
- assert!(reduced.is_def_eq(&nff, &Environment::new()).is_ok());
+ let term_type = term.infer(&Environment::new()).unwrap();
+ assert_eq!(term_type, Type(BigUint::from(1_u64).into()));
+ assert!(term.check(&term_type, &Environment::new()).is_ok());
}
#[test]
- fn polymorphism() {
- let id = Abs(
- box Type(BigUint::from(0_u64).into()),
- box Abs(box Var(1.into()), box Var(1.into())),
+ fn illtyped_reduction() {
+ // λ (x : P -> P).(λ (y :P).x y) x
+ // λ P -> P.(λ P.2 1) 1
+ let term = Abs(
+ box Prod(box Prop, box Prop),
+ box App(
+ box Abs(box Prop, box App(box Var(2.into()), box Var(1.into()))),
+ box Var(1.into()),
+ ),
);
- assert!(id.infer(&Environment::new()).is_ok());
+ // λx.x x
+ let reduced = Abs(box Prop, box App(box Var(1.into()), box Var(1.into())));
+ assert!(term.is_def_eq(&reduced, &Environment::new()).is_ok());
}
#[test]
- fn type_type() {
- assert!(Type(BigUint::from(0_u64).into())
- .check(&Type(BigUint::from(1_u64).into()), &Environment::new())
- .is_ok());
+ fn typed_prod_1() {
+ let term = Prod(box Prop, box Prop);
+ let term_type = term.infer(&Environment::new()).unwrap();
+
+ assert_eq!(term_type, Type(BigUint::from(0_u64).into()));
+ assert!(term.check(&term_type, &Environment::new()).is_ok());
}
#[test]
- fn not_function() {
- let t = App(box Prop, box Prop);
- assert!(t.infer(&Environment::new()).is_err())
+ fn typed_prod_2() {
+ let term = Prod(box Prop, box Var(1.into()));
+ let term_type = term.infer(&Environment::new()).unwrap();
+
+ assert_eq!(term_type, Prop);
+ assert!(term.check(&term_type, &Environment::new()).is_ok());
}
#[test]
- fn not_type_prod() {
- let t = Prod(box Abs(box Prop, box Var(1.into())), box Prop);
- assert!(t.infer(&Environment::new()).is_err());
-
- let t = Prod(box Prop, box Abs(box Prop, box Prop));
- assert!(t.infer(&Environment::new()).is_err());
-
- let wf_prod = Prod(box Prop, box Prop);
- assert!(wf_prod
- .check(&Type(BigUint::from(0_u64).into()), &Environment::new())
- .is_ok());
-
- let wf_prod = Prod(box Prop, box Var(1.into()));
- assert!(wf_prod.check(&Prop, &Environment::new()).is_ok());
-
- // Type0 -> (A : Prop) ->
- let wf_prod = Prod(box Prop, box Prop);
- assert!(wf_prod
- .check(&Type(BigUint::from(0_u64).into()), &Environment::new())
- .is_ok());
+ fn typed_prod_3() {
+ let term = Abs(box Prop, box Abs(box Var(1.into()), box Var(1.into())));
+ let term_type = term.infer(&Environment::new()).unwrap();
+
+ assert_eq!(
+ term_type,
+ Prod(box Prop, box Prod(box Var(1.into()), box Var(2.into())))
+ );
+ assert!(term.check(&term_type, &Environment::new()).is_ok());
+ }
+
+ #[test]
+ fn typed_polymorphism() {
+ let identity = Abs(
+ box Type(BigUint::from(0_u64).into()),
+ box Abs(box Var(1.into()), box Var(1.into())),
+ );
+ let identity_type = identity.infer(&Environment::new()).unwrap();
+
+ assert_eq!(
+ identity_type,
+ Prod(
+ box Type(BigUint::from(0_u64).into()),
+ box Prod(box Var(1.into()), box Var(2.into()))
+ )
+ );
+ assert!(identity.check(&identity_type, &Environment::new()).is_ok());
}
#[test]
- fn poly_test2() {
- let t = Abs(
+ fn typed_polymorphism_2() {
+ let term = Abs(
box Prop,
box Abs(
box Prop,
@@ -375,60 +396,130 @@ mod tests {
),
),
);
+ let term_type = term.infer(&Environment::new()).unwrap();
- assert!(t.infer(&Environment::new()).is_ok());
+ assert_eq!(
+ term_type,
+ Prod(
+ box Prop,
+ box Prod(
+ box Prop,
+ box Prod(box Prod(box Prop, box Prod(box Prop, box Prop)), box Prop)
+ )
+ )
+ );
+ assert!(term.check(&term_type, &Environment::new()).is_ok());
}
#[test]
- fn env_test() {
- let id_prop = Prod(box Prop, box Prod(box Var(1.into()), box Var(2.into())));
- let t = Abs(box Prop, box Abs(box Var(1.into()), box Var(1.into())));
- let mut env = Environment::new();
- env.insert("foo".into(), id_prop.clone(), Prop).unwrap();
+ fn type_hierarchy_prop() {
+ let term = Prop;
+ let term_type = term.infer(&Environment::new()).unwrap();
- assert!(t.check(&Const("foo".into()), &env).is_ok());
- assert!(id_prop.is_def_eq(&Const("foo".into()), &env).is_ok());
+ assert_eq!(term_type, Type(BigUint::from(0_u64).into()));
+ assert!(term.check(&term_type, &Environment::new()).is_ok());
}
#[test]
- fn check_bad() {
- assert!(Prop.check(&Prop, &Environment::new()).is_err());
+ fn type_hierarchy_type() {
+ let term = Type(BigUint::from(0_u64).into());
+ let term_type = term.infer(&Environment::new()).unwrap();
+
+ assert_eq!(term_type, Type(BigUint::from(1_u64).into()));
+ assert!(term.check(&term_type, &Environment::new()).is_ok());
}
#[test]
- fn not_def_eq() {
- assert!(Prop
- .is_def_eq(&Type(BigUint::from(0_u64).into()), &Environment::new())
- .is_err());
+ fn failed_def_equal() {
+ assert_eq!(
+ Prop.is_def_eq(&Type(BigUint::from(0_u64).into()), &Environment::new()),
+ Err(NotDefEq(Prop, Type(BigUint::from(0_u64).into())))
+ );
}
#[test]
- fn infer_const() {
- let id_prop = Prod(box Prop, box Prod(box Var(1.into()), box Var(1.into())));
+ fn environment() {
+ let term = Abs(box Prop, box Abs(box Var(1.into()), box Var(1.into())));
+ let term_type = term.infer(&Environment::new()).unwrap();
+
+ let context = Prod(box Prop, box Prod(box Var(1.into()), box Var(2.into())));
let mut env = Environment::new();
- env.insert("foo".into(), id_prop, Prop).unwrap();
+ env.insert("foo".into(), context, Prop).unwrap();
- assert!(Const("foo".into()).infer(&env).is_ok());
- assert!(Const("foo".into()).infer(&Environment::new()).is_err());
+ assert_eq!(
+ term_type,
+ Prod(box Prop, box Prod(box Var(1.into()), box Var(2.into())))
+ );
+ assert!(term.check(&Const("foo".into()), &env).is_ok());
}
- #[test]
- fn prod_var() {
- let ty = Prod(box Prop, box Prod(box Var(1.into()), box Var(2.into())));
- let t = Abs(box Prop, box Abs(box Var(1.into()), box Var(1.into())));
- assert!(t.check(&ty, &Environment::new()).is_ok())
- }
+ mod failed_type_inference {
+ use super::*;
- #[test]
- fn univ_reduc() {
- let ty = App(
- box Abs(box Prop, box Type(BigUint::from(0_u64).into())),
- box Prod(box Prop, box Var(1.into())),
- );
- assert!(ty.conversion(
- &Type(BigUint::from(0_u64).into()),
- &Environment::new(),
- 0.into()
- ))
+ #[test]
+ fn not_function() {
+ let term = App(box Prop, box Prop);
+
+ assert_eq!(
+ term.infer(&Environment::new()),
+ Err(NotAFunction(Prop, Type(BigUint::from(0_u64).into()), Prop))
+ );
+ }
+
+ #[test]
+ fn wrong_argument_type() {
+ // λ (x : P -> P).(λ (y :P).x y) x
+ // λ P -> P.(λ P.2 1) 1
+ let term = Abs(
+ box Prod(box Prop, box Prop),
+ box App(
+ box Abs(box Prop, box App(box Var(2.into()), box Var(1.into()))),
+ box Var(1.into()),
+ ),
+ );
+
+ assert_eq!(
+ term.infer(&Environment::new()),
+ Err(WrongArgumentType(
+ Abs(box Prop, box App(box Var(2.into()), box Var(1.into()))),
+ Prop,
+ Var(1.into()),
+ Prod(box Prop, box Prop)
+ ))
+ );
+ }
+
+ #[test]
+ fn not_universe_1() {
+ let term = Prod(proj(1), box Prop);
+
+ assert_eq!(
+ term.infer(&Environment::new()),
+ Err(NotUniverse(Prod(box Prop, box Prop)))
+ );
+ }
+
+ #[test]
+ fn not_universe_2() {
+ let term = Prod(box Prop, box Abs(box Prop, box Prop));
+
+ assert_eq!(
+ term.infer(&Environment::new()),
+ Err(NotUniverse(Prod(
+ box Prop,
+ box Type(BigUint::from(0_u64).into())
+ )))
+ );
+ }
+
+ #[test]
+ fn const_not_found() {
+ let term = Const("foo".to_string());
+
+ assert_eq!(
+ term.infer(&Environment::new()),
+ Err(ConstNotFound("foo".to_string()))
+ );
+ }
}
}
--
GitLab