diff --git a/kernel/src/command.rs b/kernel/src/command.rs
index 14788a47a4edbbc93e3e66536d2f4796056761e0..7b3c01dc8e3ce37aa869588887036addb09da362 100644
--- a/kernel/src/command.rs
+++ b/kernel/src/command.rs
@@ -1,4 +1,6 @@
-use crate::{Environment, KernelError, Term};
+use crate::environment::Environment;
+use crate::error::Result;
+use crate::term::Term;
#[derive(Debug, Eq, PartialEq)]
pub enum Command {
@@ -11,7 +13,7 @@ pub enum Command {
impl Command {
// TODO (#19)
- pub fn process(self, env: &mut Environment) -> Result<Option<Term>, KernelError> {
+ pub fn process(self, env: &mut Environment) -> Result<Option<Term>> {
match self {
Command::Define(s, None, term) => term
.infer(env)
@@ -30,7 +32,8 @@ impl Command {
#[cfg(test)]
mod tests {
- use crate::{num_bigint::BigUint, Command, Environment, Term};
+ use super::*;
+ use num_bigint::BigUint;
fn simple_env() -> Environment {
Environment::new()
diff --git a/kernel/src/environment.rs b/kernel/src/environment.rs
index a83244ac1a5e06d51cf65120cbb6072a126a99ba..b93dbdd1a92f92a1f708a1c8d22d2cbaef54190c 100644
--- a/kernel/src/environment.rs
+++ b/kernel/src/environment.rs
@@ -1,4 +1,4 @@
-use crate::error::KernelError;
+use crate::error::{KernelError, Result};
use crate::term::Term;
use derive_more::From;
use std::collections::{hash_map, HashMap};
@@ -14,7 +14,7 @@ impl Environment {
}
/// Creates a new environment binding s with (t1,t2)
- pub fn insert(&mut self, s: String, t1: Term, t2: Term) -> Result<&Self, KernelError> {
+ pub fn insert(&mut self, s: String, t1: Term, t2: Term) -> Result<&Self> {
if let hash_map::Entry::Vacant(e) = self.0.entry(s.clone()) {
e.insert((t1, t2));
Ok(self)
diff --git a/kernel/src/error.rs b/kernel/src/error.rs
index e98be68d91f44ff647c50070b9951e8377ae6502..868e4410c709d5e1d93d71c63fe1690fb365729e 100644
--- a/kernel/src/error.rs
+++ b/kernel/src/error.rs
@@ -1,7 +1,7 @@
use crate::{term::Term, Location};
use derive_more::Display;
+use std::error::Error;
-// TODO #19
/// Type representing kernel errors, is used by the toplevel to pretty-print errors.
#[derive(Clone, Debug, Display, PartialEq, Eq)]
pub enum KernelError {
@@ -46,3 +46,7 @@ pub enum KernelError {
#[display(fmt = "expected {}, found {}", _0, _1)]
TypeMismatch(Term, Term),
}
+
+impl Error for KernelError {}
+
+pub type Result<T> = std::result::Result<T, KernelError>;
diff --git a/kernel/src/location.rs b/kernel/src/location.rs
index 43f6d3df725f2eb2b5f1d8605941945b05a13345..7f671d639681aa903abc89d9208b909f07d39f56 100644
--- a/kernel/src/location.rs
+++ b/kernel/src/location.rs
@@ -1,15 +1,21 @@
+// TODO: Waiting for #15
use derive_more::{Constructor, Display, From};
-#[derive(Clone, Constructor, Debug, Default, Display, Eq, PartialEq, From)]
+/// Line and column position.
+#[derive(Clone, Constructor, Debug, Default, Display, Eq, PartialEq, From, Ord, PartialOrd)]
#[display(fmt = "{}:{}", line, column)]
pub struct Position {
pub line: usize,
pub column: usize,
}
-#[derive(Clone, Constructor, Debug, Default, Display, Eq, PartialEq, From)]
+/// Span of position.
+#[derive(Clone, Constructor, Debug, Default, Display, Eq, PartialEq, From, Ord, PartialOrd)]
#[display(fmt = "{}-{}", start, end)]
pub struct Location {
+ #[from(forward)]
pub start: Position,
+
+ #[from(forward)]
pub end: Position,
}
diff --git a/kernel/src/term.rs b/kernel/src/term.rs
index a840deaa697ceca3f0186b86b39bbc8d7ff9d193..e1d934b8be89ebf36f8eabf39cb3667c41ef4b56 100644
--- a/kernel/src/term.rs
+++ b/kernel/src/term.rs
@@ -106,8 +106,7 @@ impl Term {
#[cfg(test)]
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;
+ use super::*;
#[test]
fn simple_subst() {
diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs
index ca4c8cb50e981e24fd99a7e4bbdc99c6e78d4dbc..e81659cdb1a066f3172ad550f3967403ae6683ca 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;
+use crate::error::{KernelError, Result};
use crate::term::{DeBruijnIndex, Term};
use num_bigint::BigUint;
use std::cmp::max;
@@ -84,14 +84,14 @@ impl Term {
}
/// Checks whether two terms are definitionally equal.
- pub fn is_def_eq(&self, rhs: &Term, env: &Environment) -> Result<(), KernelError> {
+ 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()))
}
/// Computes universe the universe in which `(x : A) -> B` lives when `A : u1` and `B : u2`.
- fn imax(&self, rhs: &Term) -> Result<Term, KernelError> {
+ fn imax(&self, rhs: &Term) -> Result<Term> {
match rhs {
// Because Prop is impredicative, if B : Prop, then (x : A) -> b : Prop
Prop => Ok(Prop),
@@ -109,7 +109,7 @@ impl Term {
}
}
- fn _infer(&self, env: &Environment, ctx: &mut Context) -> Result<Term, KernelError> {
+ fn _infer(&self, env: &Environment, ctx: &mut Context) -> Result<Term> {
match self {
Prop => Ok(Type(BigUint::from(0_u64).into())),
Type(i) => Ok(Type(i.clone() + BigUint::from(1_u64).into())),
@@ -151,12 +151,12 @@ impl Term {
}
/// Infers the type of a `Term` in a given context.
- pub fn infer(&self, env: &Environment) -> Result<Term, KernelError> {
+ pub fn infer(&self, env: &Environment) -> Result<Term> {
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, env: &Environment) -> Result<(), KernelError> {
+ pub fn check(&self, ty: &Term, env: &Environment) -> Result<()> {
let ctx = &mut Context::new();
let tty = self._infer(env, ctx)?;
@@ -168,7 +168,7 @@ impl Term {
#[cfg(test)]
mod tests {
- use crate::type_checker::*;
+ use super::*;
fn id(l: usize) -> Box<Term> {
box Abs(box Prop, box Var(l.into()))