diff options
| -rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 68 |
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) } |