Skip to content
Snippets Groups Projects
Verified Commit 09375b75 authored by v-lafeychine's avatar v-lafeychine
Browse files

chore(error): Add Result type + Improve use

parent 1f7a2554
No related branches found
No related tags found
1 merge request!23Resolve "Kernel errors"
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()
......
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)
......
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>;
// 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,
}
......@@ -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() {
......
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()))
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment