From 015b24b04128cbf5a60fbc8ac3f526306ca27378 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 21 Jan 2020 17:43:44 +0000 Subject: Simplify type error type --- dhall/src/error/mod.rs | 13 ++++------- dhall/src/semantics/core/value.rs | 3 +-- dhall/src/semantics/phase/typecheck.rs | 42 ++++++++++------------------------ dhall/src/semantics/tck/tyexpr.rs | 3 +-- dhall/src/tests.rs | 26 ++++++++++----------- 5 files changed, 31 insertions(+), 56 deletions(-) (limited to 'dhall') diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 844a3e4..5595c53 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -1,6 +1,5 @@ use std::io::Error as IOError; -use crate::semantics::core::context::TyCtx; use crate::semantics::core::value::Value; use crate::semantics::phase::resolve::ImportStack; use crate::semantics::phase::NormalizedExpr; @@ -37,11 +36,10 @@ pub enum EncodeError { CBORError(serde_cbor::error::Error), } -/// A structured type error that includes context +/// A structured type error #[derive(Debug)] pub struct TypeError { message: TypeMessage, - context: TyCtx, } /// The specific type error @@ -88,11 +86,8 @@ pub(crate) enum TypeMessage { } impl TypeError { - pub(crate) fn new(context: &TyCtx, message: TypeMessage) -> Self { - TypeError { - context: context.clone(), - message, - } + pub(crate) fn new(message: TypeMessage) -> Self { + TypeError { message } } } @@ -100,7 +95,7 @@ impl std::fmt::Display for TypeError { fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { use TypeMessage::*; let msg = match &self.message { - UnboundVariable(span) => span.error("Type error: Unbound variable"), + UnboundVariable(var) => var.error("Type error: Unbound variable"), InvalidInputType(v) => { v.span().error("Type error: Invalid function input") } diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index f470019..dc6a116 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -3,7 +3,6 @@ use std::collections::HashMap; use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; -use crate::semantics::core::context::TyCtx; use crate::semantics::core::var::{AlphaVar, Binder}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; @@ -438,7 +437,7 @@ impl ValueInternal { fn get_type(&self) -> Result<&Value, TypeError> { match &self.ty { Some(t) => Ok(t), - None => Err(TypeError::new(&TyCtx::new(), TypeMessage::Sort)), + None => Err(TypeError::new(TypeMessage::Sort)), } } diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 15025c1..9e41f1e 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -14,27 +14,20 @@ use crate::syntax::{ }; fn tck_pi_type( - ctx: &TyCtx, binder: Binder, tx: Value, te: Value, ) -> Result { use TypeMessage::*; - let ctx2 = ctx.insert_type(&binder, tx.clone()); let ka = match tx.get_type()?.as_const() { Some(k) => k, - _ => return Err(TypeError::new(ctx, InvalidInputType(tx))), + _ => return Err(TypeError::new(InvalidInputType(tx))), }; let kb = match te.get_type()?.as_const() { Some(k) => k, - _ => { - return Err(TypeError::new( - &ctx2, - InvalidOutputType(te.get_type()?), - )) - } + _ => return Err(TypeError::new(InvalidOutputType(te.get_type()?))), }; let k = function_check(ka, kb); @@ -46,7 +39,6 @@ fn tck_pi_type( } fn tck_record_type( - ctx: &TyCtx, kts: impl IntoIterator>, ) -> Result { use std::collections::hash_map::Entry; @@ -59,13 +51,13 @@ fn tck_record_type( // Construct the union of the contained `Const`s match t.get_type()?.as_const() { Some(k2) => k = max(k, k2), - None => return Err(TypeError::new(ctx, InvalidFieldType(x, t))), + None => return Err(TypeError::new(InvalidFieldType(x, t))), } // Check for duplicated entries let entry = new_kts.entry(x); match &entry { Entry::Occupied(_) => { - return Err(TypeError::new(ctx, RecordTypeDuplicateField)) + return Err(TypeError::new(RecordTypeDuplicateField)) } Entry::Vacant(_) => entry.or_insert_with(|| t), }; @@ -77,7 +69,7 @@ fn tck_record_type( )) } -fn tck_union_type(ctx: &TyCtx, kts: Iter) -> Result +fn tck_union_type(kts: Iter) -> Result where Iter: IntoIterator), TypeError>>, { @@ -93,17 +85,14 @@ where (None, Some(k2)) => k = Some(k2), (Some(k1), Some(k2)) if k1 == k2 => {} _ => { - return Err(TypeError::new( - ctx, - InvalidFieldType(x, t.clone()), - )) + return Err(TypeError::new(InvalidFieldType(x, t.clone()))) } } } let entry = new_kts.entry(x); match &entry { Entry::Occupied(_) => { - return Err(TypeError::new(ctx, UnionTypeDuplicateField)) + return Err(TypeError::new(UnionTypeDuplicateField)) } Entry::Vacant(_) => entry.or_insert_with(|| t), }; @@ -313,7 +302,7 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { let body_type = body.get_type()?; Ok(Value::from_kind_and_type( ValueKind::Lam(binder.clone(), annot.clone(), body), - tck_pi_type(ctx, binder, annot, body_type)?, + tck_pi_type(binder, annot, body_type)?, )) } Pi(x, ta, tb) => { @@ -321,7 +310,7 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { let ta = type_with(ctx, ta.clone())?; let ctx2 = ctx.insert_type(&binder, ta.clone()); let tb = type_with(&ctx2, tb.clone())?; - tck_pi_type(ctx, binder, ta, tb) + tck_pi_type(binder, ta, tb) } Let(x, t, v, e) => { let v = if let Some(t) = t { @@ -337,9 +326,7 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { Embed(p) => Ok(p.clone().into_typed().into_value()), Var(var) => match ctx.lookup(&var) { Some(typed) => Ok(typed.clone()), - None => { - Err(TypeError::new(ctx, TypeMessage::UnboundVariable(span))) - } + None => Err(TypeError::new(TypeMessage::UnboundVariable(span))), }, e => { // Typecheck recursively all subexpressions @@ -364,7 +351,7 @@ fn type_last_layer( use syntax::Const::Type; use syntax::ExprKind::*; use TypeMessage::*; - let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg)); + let mkerr = |msg: TypeMessage| Err(TypeError::new(msg)); /// Intermediary return type enum Ret { @@ -474,15 +461,12 @@ fn type_last_layer( RetTypeOnly(Value::from_builtin(syntax::Builtin::Optional).app(t)) } RecordType(kts) => RetWhole(tck_record_type( - ctx, kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), )?), UnionType(kts) => RetWhole(tck_union_type( - ctx, kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), )?), RecordLit(kvs) => RetTypeOnly(tck_record_type( - ctx, kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))), )?), Field(r, x) => { @@ -502,7 +486,6 @@ fn type_last_layer( Some(Some(t)) => { RetTypeOnly( tck_pi_type( - ctx, ctx.new_binder(x), t.clone(), r.under_binder(), @@ -577,7 +560,6 @@ fn type_last_layer( // Construct the final record type from the union RetTypeOnly(tck_record_type( - ctx, kts.into_iter().map(|(x, v)| Ok((x.clone(), v))), )?) } @@ -627,7 +609,7 @@ fn type_last_layer( }, )?; - RetWhole(tck_record_type(ctx, kts.into_iter().map(Ok))?) + RetWhole(tck_record_type(kts.into_iter().map(Ok))?) } BinOp(o @ ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 72f5b1d..983f3f8 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,6 +1,5 @@ #![allow(dead_code)] use crate::error::{TypeError, TypeMessage}; -use crate::semantics::core::context::TyCtx; use crate::semantics::core::var::AlphaVar; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::Normalized; @@ -40,7 +39,7 @@ impl TyExpr { pub fn get_type(&self) -> Result { match &self.ty { Some(t) => Ok(t.clone()), - None => Err(TypeError::new(&TyCtx::new(), TypeMessage::Sort)), + None => Err(TypeError::new(TypeMessage::Sort)), } } diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index d86574a..7795d17 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -158,12 +158,12 @@ pub fn run_test(test: Test<'_>) -> Result<()> { parse_file_str(&file_path)?.resolve().unwrap_err(); } TypeInferenceSuccess(expr_file_path, expected_file_path) => { - // let expr = - // parse_file_str(&expr_file_path)?.resolve()?.typecheck()?; - // let ty = expr.get_type()?.to_expr(); - let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?; - let ty = tyexpr.get_type()?.to_expr(); + let expr = + parse_file_str(&expr_file_path)?.resolve()?.typecheck()?; + let ty = expr.get_type()?.to_expr(); + // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + // let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?; + // let ty = tyexpr.get_type()?.to_expr(); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(ty, expected); } @@ -206,15 +206,15 @@ pub fn run_test(test: Test<'_>) -> Result<()> { } } Normalization(expr_file_path, expected_file_path) => { - // let expr = parse_file_str(&expr_file_path)? - // .resolve()? - // .typecheck()? - // .normalize() - // .to_expr(); - let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - let expr = crate::semantics::nze::nzexpr::typecheck(expr)? + let expr = parse_file_str(&expr_file_path)? + .resolve()? + .typecheck()? .normalize() .to_expr(); + // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + // let expr = crate::semantics::nze::nzexpr::typecheck(expr)? + // .normalize() + // .to_expr(); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(expr, expected); -- cgit v1.2.3