summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/nze/normalize.rs
diff options
context:
space:
mode:
authorNadrieril2020-02-09 11:53:55 +0000
committerNadrieril2020-02-09 20:13:23 +0000
commit6c90d356c9a4a5bbeb88f25ad0ab499ba1503eae (patch)
treeb2262fc5468eb4d65ceef713991e51b5dc66b044 /dhall/src/semantics/nze/normalize.rs
parent27031b3739ff9f2043e64130a4c5699d0f9233e8 (diff)
Remove most TyExpr from normalization
Diffstat (limited to 'dhall/src/semantics/nze/normalize.rs')
-rw-r--r--dhall/src/semantics/nze/normalize.rs21
1 files changed, 10 insertions, 11 deletions
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index b5949f5..acb2e51 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -3,8 +3,7 @@ use std::collections::HashMap;
use crate::semantics::NzEnv;
use crate::semantics::{
- Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, TyExpr, TyExprKind,
- Value, ValueKind,
+ Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, Value, ValueKind,
};
use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents};
use crate::Normalized;
@@ -460,11 +459,11 @@ pub(crate) fn normalize_one_layer(
}
}
-/// Normalize a TyExpr into WHNF
-pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
- match tye.kind() {
- TyExprKind::Var(var) => env.lookup_val(var),
- TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => {
+/// Normalize Hir into WHNF
+pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind {
+ match hir.kind() {
+ HirKind::Var(var) => env.lookup_val(var),
+ HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
let annot = annot.eval(env);
ValueKind::LamClosure {
binder: Binder::new(binder.clone()),
@@ -472,7 +471,7 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
closure: Closure::new(env, body.clone()),
}
}
- TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => {
+ HirKind::Expr(ExprKind::Pi(binder, annot, body)) => {
let annot = annot.eval(env);
ValueKind::PiClosure {
binder: Binder::new(binder.clone()),
@@ -480,12 +479,12 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
closure: Closure::new(env, body.clone()),
}
}
- TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => {
+ HirKind::Expr(ExprKind::Let(_, None, val, body)) => {
let val = val.eval(env);
body.eval(&env.insert_value_noty(val)).kind().clone()
}
- TyExprKind::Expr(e) => {
- let e = e.map_ref(|tye| tye.eval(env));
+ HirKind::Expr(e) => {
+ let e = e.map_ref(|hir| hir.eval(env));
normalize_one_layer(e, env)
}
}