From d7d96b175d04a97e080b860aeef72ba39f0ad16a Mon Sep 17 00:00:00 2001
From: belazy <aarthuur01@gmail.com>
Date: Sat, 22 Oct 2022 14:53:10 +0200
Subject: [PATCH] =?UTF-8?q?Resolve=20"Type-checker=20doesn't=20use=20the?=
=?UTF-8?q?=20global=20context"=20=E2=9C=A8=EF=B8=8F=20Closes=20#17=20?=
=?UTF-8?q?=F0=9F=90=94=EF=B8=8F=F0=9F=91=8D=EF=B8=8F=20Approved-by:=20bel?=
=?UTF-8?q?azy=20<aarthuur01@gmail.com>=20Approved-by:=20loutr=20<loutr@cr?=
=?UTF-8?q?ans.org>=20Approved-by:=20aalbert=20<augustin.albert@bleu-azure?=
=?UTF-8?q?.fr>?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
🦀ï¸ðŸ°ðŸ¦€ï¸ðŸ°ðŸ¦€ï¸ðŸ°
* chore: misc
* chore : add test coverage
* chore(kernel): Reduce code complexity
* fix(kernel): Made Context mutable
* fix(kernel): Made type_checker.rs full of reference
* fix(kernel): Made term.rs full of reference
* fix(kernel): Use of reference
* Apply 1 suggestion(s) to 1 file(s)
* Fix : refer to #19
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Fix : remove unused trait
* Fix : apply suggestion
* Fix : use Self in impl
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Apply 1 suggestion(s) to 1 file(s)
* Chore: use `Environment::new()` instead of `Default::default()`
* Chore : add documentation
* Chore : expand tests coverage
* Revert "Feat : parse Constants"
This reverts commit 0618fd79d710791c9d5e0a0470a1489b8ae7ee11.
* Feat : move `Environment` to respective file
* Feat : add test for Env use during typechecking
* Feat : parse Constants
* Feat : use `Environment` during type-checking/inference
* Feat : add `GlobalContext`
---
.gitlab-ci.yml | 4 +-
kernel/src/environment.rs | 43 ++++++
kernel/src/lib.rs | 3 +
kernel/src/term.rs | 110 ++++++++-----
kernel/src/type_checker.rs | 307 ++++++++++++++++++++++---------------
5 files changed, 303 insertions(+), 164 deletions(-)
create mode 100644 kernel/src/environment.rs
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 254aa93a..07eed1f6 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -39,13 +39,13 @@ tests:
stage: tests
variables:
CARGO_INCREMENTAL: 0
- EXCLUDE_REGEXP: "unreachable!()|#\\["
+ EXCLUDE_REGEXP: "//!|///|#\\[|unreachable!()|use"
RUSTDOCFLAGS: "-Cpanic=abort"
RUSTFLAGS: "-Zprofile -Ccodegen-units=1 -Copt-level=0 -Clink-dead-code -Coverflow-checks=off -Zpanic_abort_tests -Cpanic=abort"
script:
- cargo test
- - grcov . -s . --binary-path ./target/debug/ -t cobertura --branch --ignore "*cargo*" --ignore-not-existing --excl-line ${EXCLUDE_REGEXP} --excl-br-line ${EXCLUDE_REGEXP} -o coverage.xml
+ - grcov . -s . --binary-path ./target/debug/ -t cobertura --branch --ignore "*cargo*" --ignore-not-existing --excl-line ${EXCLUDE_REGEXP} --excl-br-line ${EXCLUDE_REGEXP} -o coverage.xml
- sed -n '3p' coverage.xml | grep -oE '[a-z-]+="[0-9](.[0-9]+)?"' | sed -r 's/(branch-rate|line-rate)="(0|(1)).([0-9]{2})([0-9]{2})[0-9]*"/\1="\3\4.\5%"/'
- find target \( -name "*.gcda" -or -name "*.gcno" \) -delete
diff --git a/kernel/src/environment.rs b/kernel/src/environment.rs
new file mode 100644
index 00000000..a58bbc0a
--- /dev/null
+++ b/kernel/src/environment.rs
@@ -0,0 +1,43 @@
+use crate::term::Term;
+use derive_more::From;
+use std::collections::HashMap;
+
+/// Global Environment, contains the term and type of every definitions, denoted by their strings.
+#[derive(Clone, Default, From)]
+pub struct Environment(HashMap<String, (Term, Term)>);
+
+// TODO #19
+#[derive(Debug, Clone)]
+pub enum EnvError {
+ AlreadyDefined(String),
+}
+
+impl Environment {
+ /// Creates an empty environment.
+ pub fn new() -> Self {
+ Self::default()
+ }
+
+ /// Creates a new environment binding s with (t,ty)
+ pub fn insert(self, s: String, t: Term, ty: Term) -> Result<Self, EnvError> {
+ match self.0.clone().get(&s) {
+ Some(_) => Err(EnvError::AlreadyDefined(s)),
+ None => {
+ let mut res = self.0;
+
+ res.insert(s, (t, ty));
+ Ok(res.into())
+ }
+ }
+ }
+
+ /// Returns the term linked to a definition in a given environment.
+ pub fn get_term(&self, s: &String) -> Option<Term> {
+ self.0.get(s).map(|(t, _)| t.clone())
+ }
+
+ /// Returns the type linked to a definition in a given environment.
+ pub fn get_type(&self, s: &String) -> Option<Term> {
+ self.0.get(s).map(|(_, t)| t.clone())
+ }
+}
diff --git a/kernel/src/lib.rs b/kernel/src/lib.rs
index 76a6013f..38565866 100644
--- a/kernel/src/lib.rs
+++ b/kernel/src/lib.rs
@@ -1,7 +1,10 @@
+//! TODO: Make a documentation (#15)
+
#![feature(box_patterns)]
#![feature(box_syntax)]
mod command;
+mod environment;
mod term;
mod type_checker;
diff --git a/kernel/src/term.rs b/kernel/src/term.rs
index bb437fa8..05a0ae23 100644
--- a/kernel/src/term.rs
+++ b/kernel/src/term.rs
@@ -1,12 +1,13 @@
+use crate::environment::Environment;
use derive_more::{Add, Display, From, Into, Sub};
use num_bigint::BigUint;
#[derive(
- Add, Copy, Clone, Debug, Default, Display, Eq, Into, From, Sub, PartialEq, PartialOrd, Ord,
+ Add, Copy, Clone, Debug, Default, Display, Eq, PartialEq, From, Into, Sub, PartialOrd, Ord,
)]
pub struct DeBruijnIndex(usize);
-#[derive(Add, Clone, Debug, Display, Eq, From, Sub, PartialEq, PartialOrd, Ord)]
+#[derive(Add, Clone, Debug, Default, Display, Eq, From, Sub, PartialEq, PartialOrd, Ord)]
pub struct UniverseLevel(BigUint);
#[derive(Clone, Debug, Display, Eq, PartialEq)]
@@ -14,6 +15,9 @@ pub enum Term {
#[display(fmt = "{}", _0)]
Var(DeBruijnIndex),
+ #[display(fmt = "{}", _0)]
+ Const(String),
+
#[display(fmt = "\u{02119}")]
Prop,
@@ -34,60 +38,67 @@ use Term::*;
impl Term {
/// Apply one step of β-reduction, using leftmost outermost evaluation strategy.
- pub fn beta_reduction(self) -> Term {
+ pub fn beta_reduction(&self, env: &Environment) -> Term {
match self {
App(box Abs(_, box t1), box t2) => t1.substitute(t2, 1),
- App(box t1, box t2) => App(box t1.beta_reduction(), box t2),
- Abs(x, box t) => Abs(x, box t.beta_reduction()),
- _ => self,
+ App(box t1, box t2) => App(box t1.beta_reduction(env), box t2.clone()),
+ Abs(x, box t) => Abs(x.clone(), box t.beta_reduction(env)),
+ Const(s) => match env.get_term(s) {
+ Some(t) => t,
+ None => unreachable!(),
+ },
+ _ => self.clone(),
}
}
- fn shift(self, offset: usize, depth: usize) -> Term {
+ fn shift(&self, offset: usize, depth: usize) -> Term {
match self {
- Var(i) if i > depth.into() => Var(i + offset.into()),
+ Var(i) if *i > depth.into() => Var(*i + offset.into()),
App(box t1, box t2) => App(box t1.shift(offset, depth), box t2.shift(offset, depth)),
- Abs(t1, box t2) => Abs(t1, box t2.shift(offset, depth + 1)),
- Prod(t1, box t2) => Prod(t1, box t2.shift(offset, depth + 1)),
- _ => self,
+ Abs(t1, box t2) => Abs(t1.clone(), box t2.shift(offset, depth + 1)),
+ Prod(t1, box t2) => Prod(t1.clone(), box t2.shift(offset, depth + 1)),
+ _ => self.clone(),
}
}
- pub(crate) fn substitute(self, rhs: Term, depth: usize) -> Term {
+ pub(crate) fn substitute(&self, rhs: &Term, depth: usize) -> Term {
match self {
- Var(i) if i == depth.into() => rhs.shift(depth - 1, 0),
- Var(i) if i > depth.into() => Var(i - 1.into()),
+ Var(i) if *i == depth.into() => rhs.shift(depth - 1, 0),
+ Var(i) if *i > depth.into() => Var(*i - 1.into()),
- App(l, r) => App(
- box l.substitute(rhs.clone(), depth),
- box r.substitute(rhs, depth),
- ),
- Abs(t, term) => Abs(t, box term.substitute(rhs, depth + 1)),
- Prod(t, term) => Prod(t, box term.substitute(rhs, depth + 1)),
- _ => self,
+ App(l, r) => App(box l.substitute(rhs, depth), box r.substitute(rhs, depth)),
+ Abs(t, term) => Abs(t.clone(), box term.substitute(rhs, depth + 1)),
+ Prod(t, term) => Prod(t.clone(), box term.substitute(rhs, depth + 1)),
+ _ => self.clone(),
}
}
/// Returns the normal form of a term in a given environment.
///
/// This function is computationally expensive and should only be used for Reduce/Eval commands, not when type-checking.
- pub fn normal_form(self) -> Term {
- let mut res = self.clone().beta_reduction();
+ pub fn normal_form(self, env: &Environment) -> Term {
+ let mut res = self.beta_reduction(env);
let mut temp = self;
+
while res != temp {
temp = res.clone();
- res = res.beta_reduction()
+ res = res.beta_reduction(env)
}
res
}
+
/// Returns the weak-head normal form of a term in a given environment.
- pub fn whnf(self) -> Term {
- match self.clone() {
- App(box t, t2) => match t.whnf() {
- whnf @ Abs(_, _) => App(box whnf, t2).beta_reduction().whnf(),
- _ => self,
+ pub fn whnf(&self, env: &Environment) -> Term {
+ match self {
+ App(box t, t2) => match t.whnf(env) {
+ whnf @ Abs(_, _) => App(box whnf, t2.clone()).beta_reduction(env).whnf(env),
+ _ => self.clone(),
},
- _ => self,
+ Const(s) => match env.get_term(s) {
+ Some(t) => t,
+ None => unreachable!(),
+ },
+ _ => self.clone(),
}
}
}
@@ -96,6 +107,7 @@ impl Term {
mod tests {
// /!\ most of these tests are on ill-typed terms and should not be used for further testings
use super::Term::*;
+ use crate::term::Environment;
#[test]
fn simple_subst() {
@@ -111,7 +123,7 @@ mod tests {
// λx.x x
let reduced = Abs(box Prop, box App(box Var(1.into()), box Var(1.into())));
- assert_eq!(term.beta_reduction(), reduced);
+ assert_eq!(term.beta_reduction(&Environment::new()), reduced);
}
#[test]
@@ -272,13 +284,33 @@ mod tests {
// λa.λb.b
let term_step_7 = Abs(box Prop, box Abs(box Prop, box Var(1.into())));
- assert_eq!(term.beta_reduction(), term_step_1);
- assert_eq!(term_step_1.beta_reduction(), term_step_2);
- assert_eq!(term_step_2.beta_reduction(), term_step_3);
- assert_eq!(term_step_3.beta_reduction(), term_step_4);
- assert_eq!(term_step_4.beta_reduction(), term_step_5);
- assert_eq!(term_step_5.beta_reduction(), term_step_6);
- assert_eq!(term_step_6.beta_reduction(), term_step_7);
- assert_eq!(term_step_7.clone().beta_reduction(), term_step_7);
+ let env = Environment::new();
+
+ assert_eq!(term.beta_reduction(&env), term_step_1);
+ assert_eq!(term_step_1.beta_reduction(&env), term_step_2);
+ assert_eq!(term_step_2.beta_reduction(&env), term_step_3);
+ assert_eq!(term_step_3.beta_reduction(&env), term_step_4);
+ assert_eq!(term_step_4.beta_reduction(&env), term_step_5);
+ assert_eq!(term_step_5.beta_reduction(&env), term_step_6);
+ assert_eq!(term_step_6.beta_reduction(&env), term_step_7);
+ assert_eq!(term_step_7.beta_reduction(&env), term_step_7);
+ }
+
+ #[test]
+ fn shift_prod() {
+ let t1 = Prod(box Var(1.into()), box Var(1.into()));
+ let t2 = App(box Abs(box Prop, box t1.clone()), box Prop);
+
+ assert_eq!(t2.beta_reduction(&Environment::new()), t1)
+ }
+
+ #[test]
+ fn beta_red_const() {
+ let id_prop = Prod(box Prop, box Prod(box Var(1.into()), box Var(1.into())));
+ let env = Environment::new()
+ .insert("foo".into(), id_prop.clone(), Prop)
+ .unwrap();
+
+ assert_eq!(Const("foo".into()).beta_reduction(&env), id_prop);
}
}
diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs
index c8fc05b0..9b5a79ec 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -1,4 +1,5 @@
-use crate::term::*;
+use crate::environment::Environment;
+use crate::term::{DeBruijnIndex, Term};
use num_bigint::BigUint;
use std::cmp::max;
use std::ops::Index;
@@ -7,19 +8,21 @@ use Term::*;
impl Index<DeBruijnIndex> for Vec<Term> {
type Output = Term;
- fn index(&self, i: DeBruijnIndex) -> &Self::Output {
- &self[usize::from(i)]
+ fn index(&self, idx: DeBruijnIndex) -> &Self::Output {
+ &self[usize::from(idx)]
}
}
+
+// TODO #19
/// Type representing kernel errors, is used by the toplevel to pretty-print errors.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum TypeCheckingError {
+ /// Constant s has not been found in the current context
+ ConstNotFound(String),
+
/// t is not a universe
NotUniverse(Term),
- /// t is not a type
- NotType(Term),
-
/// t1 and t2 are not definitionally equal
NotDefEq(Term, Term),
@@ -34,14 +37,14 @@ pub enum TypeCheckingError {
}
use TypeCheckingError::*;
-// The context, which is supposed to contain other definitions in the environment, is not implemented for now.
-// TODO use context for type-checking (#17)
-// Type of lists of tuples representing the respective types of each variables
+/// Type of lists of tuples representing the respective types of each variables
type Types = Vec<Term>;
-/// Structure containing a context used for typechecking. It serves to store the types of variables in the following way :
-/// in a given context {types,lvl}, the type of `Var(i)` is in `types[lvl-i]`.
+/// Structure containing a context used for typechecking.
+///
+/// It serves to store the types of variables in the following way:
+/// In a given context {types, lvl}, the type of `Var(i)` is in `types[lvl - i]`.
#[derive(Clone, Debug, Default)]
struct Context {
types: Types,
@@ -49,50 +52,51 @@ struct Context {
}
impl Context {
+ /// Creates a new empty `Context`.
fn new() -> Self {
- Default::default()
+ Self::default()
}
- /// Extend Context with a bound variable of type ty.
- fn bind(self, ty: Term) -> Context {
- let mut new_types = self.types;
- new_types.push(ty);
- Context {
- types: new_types,
- lvl: self.lvl + 1.into(),
- }
+ /// Extends the actual context with a bound variable of type `ty`.
+ fn bind(&mut self, ty: &Term) -> &mut Self {
+ self.types.push(ty.clone());
+ self.lvl = self.lvl + 1.into();
+ self
}
}
impl Term {
- /// Conversion function, checks whether two values are definitionally equal.
+ /// Conversion function, checks whether two terms are definitionally equal.
///
/// 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.
- pub fn conversion(self, rhs: Term, l: DeBruijnIndex) -> bool {
- match (self.whnf(), rhs.whnf()) {
+ 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,
(Var(i), Var(j)) => i == j,
- (Prod(a1, b1), Prod(box a2, b2)) => {
- a1.conversion(a2, l)
- && b1
- .substitute(Var(l), l.into())
- .conversion(b2.substitute(Var(l), l.into()), l + 1.into())
+ (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())
}
// Since we assume that both vals already have the same type,
// checking conversion over the argument type is useless.
// However, this doesn't mean we can simply remove the arg type
// from the type constructor in the enum, it is needed to quote back to terms.
- (Abs(_, t), Abs(_, u)) => t
- .substitute(Var(l), l.into())
- .conversion(u.substitute(Var(l), l.into()), l + 1.into()),
+ (Abs(_, t), Abs(_, u)) => {
+ let t = t.substitute(&Var(lvl), lvl.into());
+ let u = u.substitute(&Var(lvl), lvl.into());
+
+ t.conversion(&u, env, lvl + 1.into())
+ }
(App(box t1, box u1), App(box t2, box u2)) => {
- t1.conversion(t2, l) && u1.conversion(u2, l)
+ t1.conversion(&t2, env, lvl) && u1.conversion(&u2, env, lvl)
}
_ => false,
@@ -100,21 +104,15 @@ impl Term {
}
/// Checks whether two terms are definitionally equal.
- pub fn is_def_eq(self, rhs: Term) -> Result<(), TypeCheckingError> {
- if !self.clone().conversion(rhs.clone(), 1.into()) {
- Err(NotDefEq(self, rhs))
- } else {
- Ok(())
- }
- }
-
- fn is_universe(&self) -> bool {
- matches!(*self, Prop | Type(_))
+ pub fn is_def_eq(&self, rhs: &Term, env: &Environment) -> Result<(), TypeCheckingError> {
+ self.conversion(rhs, env, 1.into())
+ .then_some(())
+ .ok_or_else(|| NotDefEq(self.clone(), rhs.clone()))
}
/// Computes universe the universe in which `(x : A) -> B` lives when `A : u1` and `B : u2`.
- fn imax(self, u2: Term) -> Result<Term, TypeCheckingError> {
- match u2 {
+ fn imax(&self, rhs: &Term) -> Result<Term, TypeCheckingError> {
+ match rhs {
// Because Prop is impredicative, if B : Prop, then (x : A) -> b : Prop
Prop => Ok(Prop),
@@ -122,73 +120,74 @@ impl Term {
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))),
+ Type(j) => Ok(Type(max(i.clone(), j.clone()))),
- _ => Err(NotUniverse(u2.clone())),
+ _ => Err(NotUniverse(rhs.clone())),
},
- _ => Err(NotUniverse(self)),
+ _ => Err(NotUniverse(self.clone())),
}
}
- fn _infer(self, ctx: &Context) -> Result<Term, TypeCheckingError> {
+ fn _infer(&self, env: &Environment, ctx: &mut Context) -> Result<Term, TypeCheckingError> {
match self {
Prop => Ok(Type(BigUint::from(0_u64).into())),
- Type(i) => Ok(Type(i + BigUint::from(1_u64).into())),
- Var(i) => Ok(ctx.types[ctx.lvl - i].clone()),
- Prod(box a, c) => {
- let ua = a.clone()._infer(ctx)?;
- if !ua.is_universe() {
- Err(NotType(ua))
- } else {
- let ctx2 = ctx.clone().bind(a);
- let ub = c._infer(&ctx2)?;
- if !ub.is_universe() {
- Err(NotType(ub))
- } else {
- ua.imax(ub)
- }
- }
+ Type(i) => Ok(Type(i.clone() + BigUint::from(1_u64).into())),
+ Var(i) => Ok(ctx.types[ctx.lvl - *i].clone()),
+
+ Const(s) => match env.get_type(s) {
+ Some(ty) => Ok(ty),
+ None => Err(ConstNotFound(s.clone())),
+ },
+
+ Prod(box t, u) => {
+ let univ_t = t._infer(env, ctx)?;
+ let univ_u = u._infer(env, ctx.clone().bind(t))?;
+
+ univ_t.imax(&univ_u)
}
- Abs(box t1, c) => {
- let ctx2 = ctx.clone().bind(t1.clone());
- Ok(Prod(box t1, box (*c)._infer(&ctx2)?))
+
+ Abs(box t, u) => {
+ let u = u._infer(env, ctx.clone().bind(t))?;
+
+ Ok(Prod(box t.clone(), box u))
}
- App(box a, box b) => {
- let type_a = a.clone()._infer(ctx)?;
- if let Prod(box t1, cls) = type_a {
- let t1_ = b.clone()._infer(ctx)?;
- if !t1.clone().conversion(t1_.clone(), ctx.types.len().into()) {
- return Err(WrongArgumentType(a, t1, b, t1_));
- };
- Ok(*cls)
- } else {
- Err(NotAFunction(a, type_a, b))
+
+ App(box t, box u) => match t._infer(env, ctx)? {
+ Prod(box typ_lhs, cls) => {
+ let typ_rhs = u._infer(env, ctx)?;
+
+ typ_lhs
+ .conversion(&typ_rhs, env, ctx.types.len().into())
+ .then_some(*cls)
+ .ok_or_else(|| WrongArgumentType(t.clone(), typ_lhs, u.clone(), typ_rhs))
}
- }
+
+ x => Err(NotAFunction(t.clone(), x, u.clone())),
+ },
}
}
/// Infers the type of a `Term` in a given context.
- pub fn infer(self) -> Result<Term, TypeCheckingError> {
- self._infer(&Context::new())
- }
- fn _check(self, ctx: &Context, ty: Term) -> Result<(), TypeCheckingError> {
- let tty = self._infer(ctx)?;
- if !tty.clone().conversion(ty.clone(), ctx.types.len().into()) {
- return Err(TypeMismatch(ty, tty));
- };
- Ok(())
+ pub fn infer(&self, env: &Environment) -> Result<Term, TypeCheckingError> {
+ self._infer(env, &mut Context::new())
}
+
/// Checks whether a given term is of type `ty` in a given context.
- pub fn check(self, ty: Term) -> Result<(), TypeCheckingError> {
- self._check(&Context::new(), ty)
+ pub fn check(&self, ty: &Term, env: &Environment) -> Result<(), TypeCheckingError> {
+ let ctx = &mut Context::new();
+ let tty = self._infer(env, ctx)?;
+
+ tty.conversion(ty, env, ctx.types.len().into())
+ .then_some(())
+ .ok_or_else(|| TypeMismatch(ty.clone(), tty))
}
}
#[cfg(test)]
mod tests {
use crate::type_checker::*;
+
fn id(l: usize) -> Box<Term> {
box Abs(box Prop, box Var(l.into()))
}
@@ -200,8 +199,9 @@ mod tests {
box Abs(box Prop, box Abs(box Prop, box Var(1.into()))),
id(1),
);
+
let nf = Abs(box Prop, box Var(1.into()));
- assert_eq!(t.normal_form(), nf)
+ assert_eq!(t.normal_form(&Environment::new()), nf)
}
#[test]
@@ -210,23 +210,27 @@ mod tests {
box Abs(box Prop, box Abs(box Prop, box Var(2.into()))),
id(1),
);
+
let nf = Abs(box Prop, id(1));
- assert_eq!(t.normal_form(), nf)
+ assert_eq!(t.normal_form(&Environment::new()), nf)
}
+
#[test]
fn simple() {
let t1 = App(
box Abs(box Type(BigUint::from(0_u64).into()), box Var(1.into())),
box Prop,
);
+
let t2 = Prop;
- assert!(t1.clone().conversion(t2, 0.into()));
- let ty = t1._infer(&Context::new());
+ assert!(t1.conversion(&t2, &Environment::new(), 0.into()));
+
+ let ty = t1.infer(&Environment::new());
assert_eq!(ty, Ok(Type(BigUint::from(0_u64).into())));
}
#[test]
- fn simple_substitute() -> Result<(), TypeCheckingError> {
+ fn simple_substitute() {
// λ (x : P -> P).(λ (y :P).x y) x
//λ P -> P.(λ P.2 1) 1
let term = Abs(
@@ -239,10 +243,8 @@ mod tests {
// λx.x x
let reduced = Abs(box Prop, box App(box Var(1.into()), box Var(1.into())));
- assert_eq!(term.clone().is_def_eq(reduced), Ok(()));
- let _ty = term.infer();
- assert!(matches!(_ty, Err(WrongArgumentType(_, _, _, _))));
- Ok(())
+ assert!(term.is_def_eq(&reduced, &Environment::new()).is_ok());
+ assert!(term.infer(&Environment::new()).is_err());
}
#[test]
@@ -312,10 +314,11 @@ mod tests {
),
),
);
+
// λa : P.λb : P .b
let reduced = Abs(box Prop, box Abs(box Prop, box Var(1.into())));
- assert_eq!(term.clone().is_def_eq(reduced), Ok(()));
- assert!(matches!(term.infer(), Ok(_)))
+ assert!(term.is_def_eq(&reduced, &Environment::new()).is_ok());
+ assert!(term.infer(&Environment::new()).is_ok())
}
//(λ ℙ → λ ℙ → λ ℙ → (0 (λ ℙ → λ ℙ → ((4 1) 3) λ ℙ → 3)) (λ ℙ → λ ℙ → (0 1) (λ ℙ → 0 λ ℙ → 0)))
@@ -323,9 +326,10 @@ mod tests {
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)));
- let nff = reduced.clone().normal_form();
+
+ let nff = reduced.clone().normal_form(&Environment::new());
assert_eq!(reduced, nff);
- assert_eq!(reduced.is_def_eq(nff), Ok(()));
+ assert!(reduced.is_def_eq(&nff, &Environment::new()).is_ok());
}
#[test]
@@ -334,40 +338,97 @@ mod tests {
box Type(BigUint::from(0_u64).into()),
box Abs(box Var(1.into()), box Var(1.into())),
);
- assert!(matches!(id.infer(), Ok(_)))
+
+ assert!(id.infer(&Environment::new()).is_ok());
}
+
#[test]
fn type_type() {
- assert!(matches!(
- Type(BigUint::from(0_u64).into()).check(Type(BigUint::from(1_u64).into())),
- Ok(_)
- ))
+ assert!(Type(BigUint::from(0_u64).into())
+ .check(&Type(BigUint::from(1_u64).into()), &Environment::new())
+ .is_ok());
}
#[test]
fn not_function() {
let t = App(box Prop, box Prop);
- assert!(matches!(t.infer(), Err(NotAFunction(..))))
+ assert!(t.infer(&Environment::new()).is_err())
}
#[test]
fn not_type_prod() {
- let t1 = Prod(box Abs(box Prop, box Var(1.into())), box Prop);
- assert!(matches!(t1.infer(), Err(NotType(..))));
- let t2 = Prod(box Prop, box Abs(box Prop, box Prop));
- assert!(matches!(t2.infer(), Err(NotType(..))));
- let wf_prod1 = Prod(box Prop, box Prop);
- assert!(matches!(
- wf_prod1.check(Type(BigUint::from(0_u64).into())),
- Ok(())
- ));
- let wf_prod2 = Prod(box Prop, box Var(1.into()));
- assert!(matches!(wf_prod2.check(Prop), Ok(())));
+ 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_prod3 = Prod(box Prop, box Prop);
- assert!(matches!(
- wf_prod3.check(Type(BigUint::from(0_u64).into())),
- Ok(())
- ));
+ let wf_prod = Prod(box Prop, box Prop);
+ assert!(wf_prod
+ .check(&Type(BigUint::from(0_u64).into()), &Environment::new())
+ .is_ok());
+ }
+
+ #[test]
+ fn poly_test2() {
+ let t = Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box Abs(
+ box Prod(box Prop, box Prod(box Prop, box Prop)),
+ box App(
+ box App(box Var(1.into()), box Var(3.into())),
+ box Var(2.into()),
+ ),
+ ),
+ ),
+ );
+
+ assert!(t.infer(&Environment::new()).is_ok());
+ }
+
+ #[test]
+ fn env_test() {
+ let id_prop = Prod(box Prop, box Prod(box Var(1.into()), box Var(1.into())));
+ let t = Abs(box Prop, box Abs(box Var(1.into()), box Var(1.into())));
+ let env = Environment::new()
+ .insert("foo".into(), id_prop.clone(), Prop)
+ .unwrap();
+
+ assert!(t.check(&Const("foo".into()), &env).is_ok());
+ assert!(id_prop.is_def_eq(&Const("foo".into()), &env).is_ok());
+ }
+
+ #[test]
+ fn check_bad() {
+ assert!(Prop.check(&Prop, &Environment::new()).is_err());
+ }
+
+ #[test]
+ fn not_def_eq() {
+ assert!(Prop
+ .is_def_eq(&Type(BigUint::from(0_u64).into()), &Environment::new())
+ .is_err());
+ }
+
+ #[test]
+ fn infer_const() {
+ let id_prop = Prod(box Prop, box Prod(box Var(1.into()), box Var(1.into())));
+ let env = Environment::new()
+ .insert("foo".into(), id_prop, Prop)
+ .unwrap();
+
+ assert!(Const("foo".into()).infer(&env).is_ok());
+ assert!(Const("foo".into()).infer(&Environment::new()).is_err());
}
}
--
GitLab