summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--dhall/src/semantics/nze/env.rs16
-rw-r--r--dhall/src/semantics/nze/normalize.rs21
-rw-r--r--dhall/src/semantics/nze/value.rs6
-rw-r--r--dhall/src/semantics/tck/env.rs2
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs5
5 files changed, 25 insertions, 25 deletions
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index 073886e..0b22a8b 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -59,14 +59,18 @@ impl NzEnv {
env.items.push(NzEnvItem::Replaced(e));
env
}
- pub fn lookup_val(&self, var: &AlphaVar) -> Value {
+ pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind {
let idx = self.items.len() - 1 - var.idx();
match &self.items[idx] {
- NzEnvItem::Kept(ty) => Value::from_kind_and_type(
- ValueKind::Var(NzVar::new(idx)),
- ty.clone(),
- ),
- NzEnvItem::Replaced(x) => x.clone(),
+ NzEnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)),
+ NzEnvItem::Replaced(x) => x.kind().clone(),
+ }
+ }
+ pub fn lookup_ty(&self, var: &AlphaVar) -> Value {
+ let idx = self.items.len() - 1 - var.idx();
+ match &self.items[idx] {
+ NzEnvItem::Kept(ty) => ty.clone(),
+ NzEnvItem::Replaced(x) => x.get_type().unwrap(),
}
}
}
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 7632d12..e677f78 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -445,14 +445,9 @@ pub(crate) fn normalize_one_layer(
}
/// Normalize a TyExpr into WHNF
-pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value {
- let ty = match tye.get_type() {
- Ok(ty) => ty,
- Err(_) => return Value::from_const(Const::Sort),
- };
-
- let kind = match tye.kind() {
- TyExprKind::Var(var) => return env.lookup_val(var),
+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)) => {
let annot = annot.eval(env);
ValueKind::LamClosure {
@@ -472,13 +467,15 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value {
}
TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => {
let val = val.eval(env);
- return body.eval(&env.insert_value(val));
+ body.eval(&env.insert_value(val)).kind().clone()
}
TyExprKind::Expr(e) => {
+ let ty = match tye.get_type() {
+ Ok(ty) => ty,
+ Err(_) => return ValueKind::Const(Const::Sort),
+ };
let e = e.map_ref(|tye| tye.eval(env));
normalize_one_layer(e, &ty, env)
}
- };
-
- Value::from_kind_and_type(kind, ty)
+ }
}
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 108dc9c..ff0ca42 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -405,7 +405,7 @@ impl ValueInternal {
use std::mem::replace;
let dummy = Form::PartialExpr(ExprKind::Const(Const::Type));
self.form = match replace(&mut self.form, dummy) {
- Form::Thunk(th) => Form::WHNF(th.eval().kind().clone()),
+ Form::Thunk(th) => Form::WHNF(th.eval()),
Form::PartialExpr(e) => {
Form::WHNF(match &self.ty {
// TODO: env
@@ -516,9 +516,7 @@ impl Thunk {
body,
}
}
-
- // TODO: maybe return a ValueKind ?
- pub fn eval(&self) -> Value {
+ pub fn eval(&self) -> ValueKind {
normalize_tyexpr_whnf(&self.body, &self.env)
}
}
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index d4cc37d..812ca7a 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -118,7 +118,7 @@ impl TyEnv {
}
pub fn lookup(&self, var: &V) -> Option<(TyExprKind, Type)> {
let var = self.names.unlabel_var(var)?;
- let ty = self.items.lookup_val(&var).get_type().unwrap();
+ let ty = self.items.lookup_ty(&var);
Some((TyExprKind::Var(var), ty))
}
}
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 4b88048..1a048f9 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,5 +1,4 @@
use crate::error::{TypeError, TypeMessage};
-use crate::semantics::normalize_tyexpr_whnf;
use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value};
use crate::syntax::{ExprKind, Span, V};
use crate::Normalized;
@@ -83,7 +82,9 @@ impl TyExpr {
}
/// Eval a closed TyExpr fully and recursively;
pub fn rec_eval_closed_expr(&self) -> Value {
- normalize_tyexpr_whnf(self, &NzEnv::new())
+ let mut val = self.eval_closed_expr();
+ val.normalize_mut();
+ val
}
}