summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/phase
diff options
context:
space:
mode:
authorNadrieril2020-01-25 10:15:17 +0000
committerNadrieril2020-01-25 10:15:17 +0000
commit70e6e3a06c05cfe7d8ca3d6f072e7182639c147f (patch)
tree91c8bcfe35b3e99a5332458531a45b58ecfb8be7 /dhall/src/semantics/phase
parentb72f0968ac19058b9cc513ab0ed1785133232a3d (diff)
Typecheck more cases
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/phase/normalize.rs13
-rw-r--r--dhall/src/semantics/phase/typecheck.rs11
2 files changed, 19 insertions, 5 deletions
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<E>(b: Builtin) -> Expr<E> {
+pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
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<Normalized>) -> Result<Value, TypeError> {
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) {