summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
authorNadrieril2020-01-21 17:43:44 +0000
committerNadrieril2020-01-21 17:43:44 +0000
commit015b24b04128cbf5a60fbc8ac3f526306ca27378 (patch)
tree0af03dcc6f7b60812992f4b5001d325b1e786a01 /dhall/src/semantics
parent476ef4594c9e8c7121bd8fc303e74ef8207a88f4 (diff)
Simplify type error type
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r--dhall/src/semantics/core/value.rs3
-rw-r--r--dhall/src/semantics/phase/typecheck.rs42
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs3
3 files changed, 14 insertions, 34 deletions
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<Value, TypeError> {
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<Item = Result<(Label, Value), TypeError>>,
) -> Result<Value, TypeError> {
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<Iter>(ctx: &TyCtx, kts: Iter) -> Result<Value, TypeError>
+fn tck_union_type<Iter>(kts: Iter) -> Result<Value, TypeError>
where
Iter: IntoIterator<Item = Result<(Label, Option<Value>), 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<Normalized>) -> Result<Value, TypeError> {
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<Normalized>) -> Result<Value, TypeError> {
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<Normalized>) -> Result<Value, TypeError> {
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<Type, TypeError> {
match &self.ty {
Some(t) => Ok(t.clone()),
- None => Err(TypeError::new(&TyCtx::new(), TypeMessage::Sort)),
+ None => Err(TypeError::new(TypeMessage::Sort)),
}
}