summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2020-01-24 17:07:56 +0000
committerNadrieril2020-01-24 17:07:56 +0000
commit700ff482fbff8960bc0e792fec6fd538c5428d70 (patch)
tree61e28733bcddd1287a7eef64f89d2d04181038df
parentbd1eb36503aa6e03532fefcfd0c4f27eb62c99d2 (diff)
Normalize more expressions
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/core/value.rs6
-rw-r--r--dhall/src/semantics/phase/normalize.rs13
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),