summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--dhall/src/semantics/phase/normalize.rs68
1 files changed, 41 insertions, 27 deletions
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 7fd76df..75d61d5 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -2,7 +2,9 @@ use std::collections::HashMap;
use std::convert::TryInto;
use crate::semantics::nze::NzVar;
-use crate::semantics::phase::typecheck::{rc, typecheck};
+use crate::semantics::phase::typecheck::{
+ builtin_to_value, const_to_value, rc, typecheck,
+};
use crate::semantics::phase::Normalized;
use crate::semantics::{
AlphaVar, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind,
@@ -372,6 +374,9 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> {
ValueKind::Lam(_, _, e) => e
.subst_shift(&AlphaVar::default(), &a)
.to_whnf_check_type(ty),
+ ValueKind::LamClosure { closure, .. } => {
+ closure.apply(a).to_whnf_check_type(ty)
+ }
ValueKind::AppliedBuiltin(b, args) => {
use std::iter::once;
let args = args.iter().cloned().chain(once(a.clone())).collect();
@@ -597,8 +602,8 @@ pub(crate) fn normalize_one_layer(
) -> ValueKind<Value> {
use ValueKind::{
BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit,
- NEOptionalLit, NaturalLit, RecordLit, TextLit, UnionConstructor,
- UnionLit, UnionType,
+ NEOptionalLit, NaturalLit, RecordLit, RecordType, TextLit,
+ UnionConstructor, UnionLit, UnionType,
};
let ret = match expr {
@@ -611,15 +616,12 @@ pub(crate) fn normalize_one_layer(
| ExprKind::Pi(_, _, _)
| ExprKind::Let(_, _, _, _)
| ExprKind::Embed(_)
- | ExprKind::Const(_)
- | ExprKind::Builtin(_)
| ExprKind::Var(_)
- | ExprKind::Annot(_, _)
- | ExprKind::EmptyListLit(_)
- | ExprKind::RecordType(_)
- | ExprKind::UnionType(_) => {
+ | ExprKind::Annot(_, _) => {
unreachable!("This case should have been handled in typecheck")
}
+ ExprKind::Const(c) => Ret::Value(const_to_value(c)),
+ ExprKind::Builtin(b) => Ret::Value(builtin_to_value(b)),
ExprKind::Assert(_) => Ret::Expr(expr),
ExprKind::App(v, a) => Ret::Value(v.app(a)),
ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)),
@@ -627,12 +629,29 @@ pub(crate) fn normalize_one_layer(
ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)),
ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)),
ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
+ ExprKind::EmptyListLit(t) => {
+ let arg = match &*t.as_whnf() {
+ ValueKind::AppliedBuiltin(syntax::Builtin::List, args)
+ if args.len() == 1 =>
+ {
+ args[0].clone()
+ }
+ _ => panic!("internal type error"),
+ };
+ Ret::ValueKind(ValueKind::EmptyListLit(arg))
+ }
ExprKind::NEListLit(elts) => {
Ret::ValueKind(NEListLit(elts.into_iter().collect()))
}
ExprKind::RecordLit(kvs) => {
Ret::ValueKind(RecordLit(kvs.into_iter().collect()))
}
+ ExprKind::RecordType(kvs) => {
+ Ret::ValueKind(RecordType(kvs.into_iter().collect()))
+ }
+ ExprKind::UnionType(kvs) => {
+ Ret::ValueKind(UnionType(kvs.into_iter().collect()))
+ }
ExprKind::TextLit(elts) => {
use InterpolatedTextContents::Expr;
let elts: Vec<_> = squash_textlit(elts.into_iter());
@@ -665,6 +684,13 @@ pub(crate) fn normalize_one_layer(
}
}
}
+ // ExprKind::BinOp(RecursiveRecordTypeMerge, l, r) => { }
+ // ExprKind::BinOp(Equivalence, l, r) => {
+ // RetWhole(Value::from_kind_and_type(
+ // ValueKind::Equivalence(l.clone(), r.clone()),
+ // Value::from_const(Type),
+ // ))
+ // }
ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
Some(ret) => ret,
None => Ret::Expr(expr),
@@ -831,8 +857,9 @@ impl NzEnv {
}
/// Normalize a TyExpr into WHNF
-pub(crate) fn normalize_tyexpr_whnf(e: &TyExpr, env: &NzEnv) -> Value {
- let kind = match e.kind() {
+pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value {
+ let ty = tye.get_type().unwrap();
+ let kind = match tye.kind() {
TyExprKind::Var(var) => return env.lookup_val(var),
TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => {
ValueKind::LamClosure {
@@ -850,22 +877,9 @@ pub(crate) fn normalize_tyexpr_whnf(e: &TyExpr, env: &NzEnv) -> Value {
}
TyExprKind::Expr(e) => {
let e = e.map_ref(|tye| tye.normalize_whnf(env));
- match e {
- ExprKind::App(f, arg) => {
- let f_borrow = f.as_whnf();
- match &*f_borrow {
- ValueKind::LamClosure { closure, .. } => {
- return closure.apply(arg)
- }
- _ => {
- drop(f_borrow);
- ValueKind::PartialExpr(ExprKind::App(f, arg))
- }
- }
- }
- _ => ValueKind::PartialExpr(e),
- }
+ normalize_one_layer(e, &ty)
}
};
- Value::from_kind_and_type_whnf(kind, e.get_type().unwrap())
+
+ Value::from_kind_and_type_whnf(kind, ty)
}