summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/nze
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/nze')
-rw-r--r--dhall/src/semantics/nze/env.rs42
-rw-r--r--dhall/src/semantics/nze/normalize.rs2
-rw-r--r--dhall/src/semantics/nze/value.rs18
3 files changed, 32 insertions, 30 deletions
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index ff52343..5b036f0 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, Type, Value, ValueKind};
+use crate::semantics::{AlphaVar, Value, ValueKind};
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub(crate) enum NzVar {
@@ -9,7 +9,7 @@ pub(crate) enum NzVar {
}
#[derive(Debug, Clone)]
-enum NzEnvItem {
+enum EnvItem<Type> {
// Variable is bound with given type
Kept(Type),
// Variable has been replaced by corresponding value
@@ -17,10 +17,12 @@ enum NzEnvItem {
}
#[derive(Debug, Clone)]
-pub(crate) struct NzEnv {
- items: Vec<NzEnvItem>,
+pub(crate) struct ValEnv<Type> {
+ items: Vec<EnvItem<Type>>,
}
+pub(crate) type NzEnv = ValEnv<()>;
+
impl NzVar {
pub fn new(idx: usize) -> Self {
NzVar::Bound(idx)
@@ -44,37 +46,43 @@ impl NzVar {
}
}
-impl NzEnv {
+impl<Type: Clone> ValEnv<Type> {
pub fn new() -> Self {
- NzEnv { items: Vec::new() }
+ ValEnv { items: Vec::new() }
+ }
+ pub fn discard_types(&self) -> ValEnv<()> {
+ let items = self
+ .items
+ .iter()
+ .map(|i| match i {
+ EnvItem::Kept(_) => EnvItem::Kept(()),
+ EnvItem::Replaced(val, _) => EnvItem::Replaced(val.clone(), ()),
+ })
+ .collect();
+ ValEnv { items }
}
pub fn insert_type(&self, ty: Type) -> Self {
let mut env = self.clone();
- env.items.push(NzEnvItem::Kept(ty));
+ env.items.push(EnvItem::Kept(ty));
env
}
pub fn insert_value(&self, e: Value, ty: Type) -> Self {
let mut env = self.clone();
- env.items.push(NzEnvItem::Replaced(e, ty));
+ env.items.push(EnvItem::Replaced(e, ty));
env
}
- pub fn insert_value_noty(&self, e: Value) -> Self {
- // TODO
- let ty = Value::const_sort();
- self.insert_value(e, ty)
- }
pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind {
let idx = self.items.len() - 1 - var.idx();
match &self.items[idx] {
- NzEnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)),
- NzEnvItem::Replaced(x, _) => x.kind().clone(),
+ EnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)),
+ EnvItem::Replaced(x, _) => x.kind().clone(),
}
}
- pub fn lookup_ty(&self, var: &AlphaVar) -> Value {
+ pub fn lookup_ty(&self, var: &AlphaVar) -> Type {
let idx = self.items.len() - 1 - var.idx();
match &self.items[idx] {
- NzEnvItem::Kept(ty) | NzEnvItem::Replaced(_, ty) => ty.clone(),
+ EnvItem::Kept(ty) | EnvItem::Replaced(_, ty) => ty.clone(),
}
}
}
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 981d894..d12146a 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -473,7 +473,7 @@ pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind {
}
HirKind::Expr(ExprKind::Let(_, None, val, body)) => {
let val = val.eval(env);
- body.eval(&env.insert_value_noty(val)).kind().clone()
+ body.eval(&env.insert_value(val, ())).kind().clone()
}
HirKind::Expr(e) => {
let e = e.map_ref(|hir| hir.eval(env));
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 5a7b558..a60be9d 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -100,11 +100,8 @@ pub(crate) enum ValueKind {
}
impl Value {
- pub(crate) fn const_sort() -> Value {
- Value::from_const(Const::Sort)
- }
/// Construct a Value from a completely unnormalized expression.
- pub(crate) fn new_thunk(env: &NzEnv, hir: Hir) -> Value {
+ pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Value {
let span = hir.span();
ValueInternal::from_thunk(Thunk::new(env, hir), span).into_value()
}
@@ -158,8 +155,8 @@ impl Value {
self.to_tyexpr_noenv().to_expr(opts)
}
- pub(crate) fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
- self.to_hir(env.as_varenv()).to_expr_tyenv(env)
+ pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
+ self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
}
pub(crate) fn normalize(&self) {
@@ -389,11 +386,8 @@ impl ValueKind {
}
impl Thunk {
- fn new(env: &NzEnv, body: Hir) -> Self {
- Thunk::Thunk {
- env: env.clone(),
- body,
- }
+ fn new(env: NzEnv, body: Hir) -> Self {
+ Thunk::Thunk { env, body }
}
fn from_partial_expr(
env: NzEnv,
@@ -424,7 +418,7 @@ impl Closure {
pub fn apply(&self, val: Value) -> Value {
match self {
Closure::Closure { env, body, .. } => {
- body.eval(&env.insert_value_noty(val))
+ body.eval(&env.insert_value(val, ()))
}
Closure::ConstantClosure { body, .. } => body.clone(),
}