summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs10
-rw-r--r--dhall/src/semantics/tck/typecheck.rs64
2 files changed, 45 insertions, 29 deletions
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index c8be3a3..a42265d 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -5,6 +5,7 @@ use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv};
use crate::semantics::phase::typecheck::rc;
use crate::semantics::phase::Normalized;
use crate::semantics::phase::{NormalizedExpr, ToExprOptions};
+use crate::semantics::tck::typecheck::TyEnv;
use crate::semantics::Value;
use crate::syntax::{ExprKind, Label, Span, V};
@@ -48,6 +49,15 @@ impl TyExpr {
pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
tyexpr_to_expr(self, opts, &mut Vec::new())
}
+ pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
+ let opts = ToExprOptions {
+ normalize: true,
+ alpha: false,
+ };
+ let env = env.as_nameenv().names();
+ let mut env = env.iter().collect();
+ tyexpr_to_expr(self, opts, &mut env)
+ }
// TODO: temporary hack
pub fn to_value(&self) -> Value {
todo!()
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 1b64d28..4ca5d4d 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -275,10 +275,22 @@ fn type_one_layer(
}
ExprKind::Annot(x, t) => {
let t = t.normalize_whnf(env.as_nzenv());
- if x.get_type()? != t {
- return mkerr("annot mismatch");
+ let x_ty = x.get_type()?;
+ if x_ty != t {
+ return mkerr(format!(
+ "annot mismatch: ({} : {}) : {}",
+ x.to_expr_tyenv(env),
+ x_ty.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env),
+ t.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env)
+ ));
+ // return mkerr(format!(
+ // "annot mismatch: {} != {}",
+ // x_ty.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env),
+ // t.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env)
+ // ));
+ // return mkerr(format!("annot mismatch: {:#?} : {:#?}", x, t,));
}
- t
+ x_ty
}
ExprKind::App(f, arg) => {
let tf = f.get_type()?;
@@ -389,35 +401,29 @@ fn type_one_layer(
let yk = y.get_type()?.as_const().unwrap();
Value::from_const(max(xk, yk))
}
- // ExprKind::BinOp(o @ BinOp::ListAppend, l, r) => {
- // match &*l.get_type()?.as_whnf() {
- // ValueKind::AppliedBuiltin(List, _, _) => {}
- // _ => return mkerr("BinOpTypeMismatch"),
- // }
-
- // if l.get_type()? != r.get_type()? {
- // return mkerr("BinOpTypeMismatch");
- // }
+ ExprKind::BinOp(BinOp::ListAppend, l, r) => {
+ let l_ty = l.get_type()?;
+ match &*l_ty.as_whnf() {
+ ValueKind::AppliedBuiltin(Builtin::List, _, _) => {}
+ _ => return mkerr("BinOpTypeMismatch"),
+ }
- // l.get_type()?
- // }
- // ExprKind::BinOp(BinOp::Equivalence, l, r) => {
- // if l.get_type()?.get_type()?.as_const() != Some(Const::Type) {
- // return mkerr("EquivalenceArgumentMustBeTerm");
- // }
- // if r.get_type()?.get_type()?.as_const() != Some(Const::Type) {
- // return mkerr("EquivalenceArgumentMustBeTerm");
- // }
+ if l_ty != r.get_type()? {
+ return mkerr("BinOpTypeMismatch");
+ }
- // if l.get_type()? != r.get_type()? {
- // return mkerr("EquivalenceTypeMismatch");
- // }
+ l_ty
+ }
+ ExprKind::BinOp(BinOp::Equivalence, l, r) => {
+ if l.get_type()? != r.get_type()? {
+ return mkerr("EquivalenceTypeMismatch");
+ }
+ if l.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+ return mkerr("EquivalenceArgumentsMustBeTerms");
+ }
- // RetWhole(Value::from_kind_and_type(
- // ValueKind::Equivalence(l.clone(), r.clone()),
- // Value::from_const(Type),
- // ))
- // }
+ Value::from_const(Const::Type)
+ }
ExprKind::BinOp(o, l, r) => {
let t = builtin_to_value(match o {
BinOp::BoolAnd