diff options
author | Nadrieril | 2020-02-09 11:53:55 +0000 |
---|---|---|
committer | Nadrieril | 2020-02-09 20:13:23 +0000 |
commit | 6c90d356c9a4a5bbeb88f25ad0ab499ba1503eae (patch) | |
tree | b2262fc5468eb4d65ceef713991e51b5dc66b044 /dhall/src/semantics/nze/normalize.rs | |
parent | 27031b3739ff9f2043e64130a4c5699d0f9233e8 (diff) |
Remove most TyExpr from normalization
Diffstat (limited to 'dhall/src/semantics/nze/normalize.rs')
-rw-r--r-- | dhall/src/semantics/nze/normalize.rs | 21 |
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) } } |