From 09375b7597f1efeb3cab918df4833e02494eb1dc Mon Sep 17 00:00:00 2001 From: Vincent Lafeychine <vincent.lafeychine@proton.me> Date: Sun, 30 Oct 2022 18:14:01 +0100 Subject: [PATCH] chore(error): Add Result type + Improve use --- kernel/src/command.rs | 9 ++++++--- kernel/src/environment.rs | 4 ++-- kernel/src/error.rs | 6 +++++- kernel/src/location.rs | 10 ++++++++-- kernel/src/term.rs | 3 +-- kernel/src/type_checker.rs | 14 +++++++------- 6 files changed, 29 insertions(+), 17 deletions(-) diff --git a/kernel/src/command.rs b/kernel/src/command.rs index 14788a47..7b3c01dc 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 a83244ac..b93dbdd1 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 e98be68d..868e4410 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 43f6d3df..7f671d63 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 a840deaa..e1d934b8 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 ca4c8cb5..e81659cd 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())) -- GitLab