diff options
| -rw-r--r-- | dhall/src/semantics/core/value.rs | 6 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 13 |
2 files changed, 10 insertions, 9 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 3798053..3e3bfe1 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -10,7 +10,7 @@ use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; use crate::semantics::phase::{ Normalized, NormalizedExpr, ToExprOptions, Typed, }; -use crate::semantics::{TyExpr, TyExprKind, Type}; +use crate::semantics::{TyExpr, TyExprKind}; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, Span, @@ -235,6 +235,10 @@ impl Value { v.check_type(t); e.subst_shift(&AlphaVar::default(), &v) } + ValueKind::PiClosure { annot, closure, .. } => { + v.check_type(annot); + closure.apply(v.clone()) + } _ => unreachable!("Internal type error"), }; Value::from_kind_and_type_whnf( diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 8f3953d..ac60ce0 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -594,10 +594,14 @@ fn apply_binop<'a>( Ret::ValueKind(RecordLit(kvs)) } - (RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => { + (RecursiveRecordTypeMerge, _, _) => { unreachable!("This case should have been handled in typecheck") } + (Equivalence, _, _) => { + Ret::ValueKind(ValueKind::Equivalence(x.clone(), y.clone())) + } + _ => return None, }) } @@ -690,13 +694,6 @@ 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), |