diff options
Diffstat (limited to 'dhall/src/semantics/tck')
| -rw-r--r-- | dhall/src/semantics/tck/tyexpr.rs | 10 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 64 |
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 |