summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
authorNadrieril2020-02-14 18:55:27 +0000
committerNadrieril2020-02-14 18:55:27 +0000
commit51cf6a28fa56031dbeae0ff378f0ef84eff7fd3e (patch)
treeff452de7a7b4c15b18b1aa43b05a5afafdd5ef58 /dhall/src/semantics/tck
parent350d1cf7d9c114b1334b2743071b0b99ea64c1ec (diff)
Oops
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs12
-rw-r--r--dhall/src/semantics/tck/typecheck.rs18
2 files changed, 14 insertions, 16 deletions
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index ac15ac5..c7b8009 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,3 +1,4 @@
+use crate::error::TypeError;
use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value};
use crate::syntax::{Const, Span};
use crate::{NormalizedExpr, ToExprOptions};
@@ -25,16 +26,13 @@ impl TyExpr {
pub fn ty(&self) -> &Type {
&self.ty
}
- pub fn get_type_tyexpr(&self, env: &TyEnv) -> TyExpr {
- self.ty()
- .to_hir(env.as_varenv())
- .typecheck(env)
- .expect("Internal type error")
+ pub fn get_type_tyexpr(&self, env: &TyEnv) -> Result<TyExpr, TypeError> {
+ Ok(self.ty().to_hir(env.as_varenv()).typecheck(env)?)
}
/// Get the kind (the type of the type) of this value
// TODO: avoid recomputing so much
- pub fn get_kind(&self, env: &TyEnv) -> Option<Const> {
- self.get_type_tyexpr(env).ty().as_const()
+ pub fn get_kind(&self, env: &TyEnv) -> Result<Option<Const>, TypeError> {
+ Ok(self.get_type_tyexpr(env)?.ty().as_const())
}
pub fn to_hir(&self) -> Hir {
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index b3c9353..377b97e 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -53,7 +53,7 @@ fn type_one_layer(
ExprKind::Lam(binder, annot, body) => {
let body_ty = body.get_type_tyexpr(
&env.insert_type(&binder.clone(), annot.eval(env)),
- );
+ )?;
let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty);
type_one_layer(env, pi_ekind, None, Span::Artificial)?.eval(env)
}
@@ -139,7 +139,7 @@ fn type_one_layer(
return span_err("InvalidListElement");
}
}
- if x.get_kind(env) != Some(Const::Type) {
+ if x.get_kind(env)? != Some(Const::Type) {
return span_err("InvalidListType");
}
@@ -147,7 +147,7 @@ fn type_one_layer(
Value::from_builtin(Builtin::List).app(t)
}
ExprKind::SomeLit(x) => {
- if x.get_kind(env) != Some(Const::Type) {
+ if x.get_kind(env)? != Some(Const::Type) {
return span_err("InvalidOptionalType");
}
@@ -167,7 +167,7 @@ fn type_one_layer(
};
// Check that the fields have a valid kind
- match v.get_kind(env) {
+ match v.get_kind(env)? {
Some(_) => {}
None => return span_err("InvalidFieldType"),
}
@@ -315,7 +315,7 @@ fn type_one_layer(
if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) {
return span_err("InvalidPredicate");
}
- if y.get_kind(env) != Some(Const::Type) {
+ if y.get_kind(env)? != Some(Const::Type) {
return span_err("IfBranchMustBeTerm");
}
if y.ty() != z.ty() {
@@ -350,8 +350,8 @@ fn type_one_layer(
ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
let ekind = ExprKind::BinOp(
BinOp::RecursiveRecordTypeMerge,
- x.get_type_tyexpr(env),
- y.get_type_tyexpr(env),
+ x.get_type_tyexpr(env)?,
+ y.get_type_tyexpr(env)?,
);
type_one_layer(env, ekind, None, span.clone())?.eval(env)
}
@@ -413,7 +413,7 @@ fn type_one_layer(
if l.ty() != r.ty() {
return span_err("EquivalenceTypeMismatch");
}
- if l.get_kind(env) != Some(Const::Type) {
+ if l.get_kind(env)? != Some(Const::Type) {
return span_err("EquivalenceArgumentsMustBeTerms");
}
@@ -582,7 +582,7 @@ fn type_one_layer(
}
}
ExprKind::ToMap(record, annot) => {
- if record.get_kind(env) != Some(Const::Type) {
+ if record.get_kind(env)? != Some(Const::Type) {
return span_err("`toMap` only accepts records of type `Type`");
}
let record_t = record.ty();