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/semantics/core/value.rs | 3 +-- dhall/src/semantics/phase/typecheck.rs | 42 ++++++++++------------------------ dhall/src/semantics/tck/tyexpr.rs | 3 +-- 3 files changed, 14 insertions(+), 34 deletions(-) (limited to 'dhall/src/semantics') 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)), } } -- cgit v1.2.3