diff options
author | Nadrieril | 2020-01-25 10:15:17 +0000 |
---|---|---|
committer | Nadrieril | 2020-01-25 10:15:17 +0000 |
commit | 70e6e3a06c05cfe7d8ca3d6f072e7182639c147f (patch) | |
tree | 91c8bcfe35b3e99a5332458531a45b58ecfb8be7 /dhall/src/semantics/phase/typecheck.rs | |
parent | b72f0968ac19058b9cc513ab0ed1785133232a3d (diff) |
Typecheck more cases
Diffstat (limited to '')
-rw-r--r-- | dhall/src/semantics/phase/typecheck.rs | 11 |
1 files changed, 9 insertions, 2 deletions
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) { |