From 70e6e3a06c05cfe7d8ca3d6f072e7182639c147f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 25 Jan 2020 10:15:17 +0000 Subject: Typecheck more cases --- dhall/src/error/mod.rs | 1 + dhall/src/semantics/phase/normalize.rs | 13 ++- dhall/src/semantics/phase/typecheck.rs | 11 +- dhall/src/semantics/tck/typecheck.rs | 187 +++++++++++++++++++++++---------- dhall/src/tests.rs | 15 ++- 5 files changed, 165 insertions(+), 62 deletions(-) diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 5595c53..850a792 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -83,6 +83,7 @@ pub(crate) enum TypeMessage { EquivalenceTypeMismatch(Value, Value), AssertMismatch(Value, Value), AssertMustTakeEquivalence, + Custom(String), } impl TypeError { diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index e848601..066a004 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -625,12 +625,14 @@ pub(crate) fn normalize_one_layer( // `RetWhole`), so they won't appear here. ExprKind::Lam(_, _, _) | ExprKind::Pi(_, _, _) - | ExprKind::Let(_, _, _, _) | ExprKind::Embed(_) - | ExprKind::Var(_) - | ExprKind::Annot(_, _) => { + | ExprKind::Var(_) => { unreachable!("This case should have been handled in typecheck") } + ExprKind::Let(_, _, val, body) => { + Ret::Value(body.subst_shift(&AlphaVar::default(), &val)) + } + ExprKind::Annot(x, _) => Ret::Value(x), ExprKind::Const(c) => Ret::Value(const_to_value(c)), ExprKind::Builtin(b) => Ret::Value(builtin_to_value(b)), ExprKind::Assert(_) => Ret::Expr(expr), @@ -895,11 +897,16 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { closure: Closure::new(env, body.clone()), } } + TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { + let val = val.normalize_whnf(env); + return body.normalize_whnf(&env.insert_value(val)); + } TyExprKind::Expr(e) => { let e = e.map_ref(|tye| tye.normalize_whnf(env)); normalize_one_layer(e, &ty) } }; + // dbg!(tye.kind(), env, &kind); Value::from_kind_and_type_whnf(kind, ty) } diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index f2d1bf2..0f3754e 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -189,7 +189,7 @@ macro_rules! make_type { }; } -fn type_of_builtin(b: Builtin) -> Expr { +pub(crate) fn type_of_builtin(b: Builtin) -> Expr { use syntax::Builtin::*; rc(match b { Bool | Natural | Integer | Double | Text => make_type!(Type), @@ -321,7 +321,14 @@ fn type_with(ctx: &TyCtx, e: Expr) -> Result { let v = type_with(ctx, v)?; let binder = ctx.new_binder(x); - type_with(&ctx.insert_value(&binder, v.clone())?, e.clone()) + let e = + type_with(&ctx.insert_value(&binder, v.clone())?, e.clone())?; + // let e_ty = e.get_type()?; + // Ok(Value::from_kind_and_type( + // ValueKind::PartialExpr(ExprKind::Let(x.clone(), None, v, e)), + // e_ty, + // )) + Ok(e) } Embed(p) => Ok(p.clone().into_typed().into_value()), Var(var) => match ctx.lookup(&var) { diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index aab5f83..046c999 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -10,6 +10,9 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TyCtx; use crate::semantics::nze::{NameEnv, QuoteEnv}; use crate::semantics::phase::normalize::{merge_maps, NzEnv}; +use crate::semantics::phase::typecheck::{ + builtin_to_value, const_to_value, type_of_builtin, +}; use crate::semantics::phase::Normalized; use crate::semantics::{ AlphaVar, Binder, Closure, TyExpr, TyExprKind, Type, Value, ValueKind, @@ -55,93 +58,171 @@ impl TyEnv { items: self.items.insert_value(e), } } - pub fn lookup_var(&self, var: &V