summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r--dhall/src/semantics/tck/env.rs14
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs4
2 files changed, 9 insertions, 9 deletions
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index ba7fb73..7990059 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, NzEnv, NzVar, Type, Value};
+use crate::semantics::{AlphaVar, NzEnv, NzVar, Type, ValEnv, Value};
use crate::syntax::{Label, V};
/// Environment for indexing variables.
@@ -17,7 +17,7 @@ pub(crate) struct NameEnv {
#[derive(Debug, Clone)]
pub(crate) struct TyEnv {
names: NameEnv,
- items: NzEnv,
+ items: ValEnv<Type>,
}
impl VarEnv {
@@ -91,14 +91,14 @@ impl TyEnv {
pub fn new() -> Self {
TyEnv {
names: NameEnv::new(),
- items: NzEnv::new(),
+ items: ValEnv::new(),
}
}
pub fn as_varenv(&self) -> VarEnv {
self.names.as_varenv()
}
- pub fn as_nzenv(&self) -> &NzEnv {
- &self.items
+ pub fn to_nzenv(&self) -> NzEnv {
+ self.items.discard_types()
}
pub fn as_nameenv(&self) -> &NameEnv {
&self.names
@@ -121,8 +121,8 @@ impl TyEnv {
}
}
-impl<'a> From<&'a TyEnv> for &'a NzEnv {
+impl<'a> From<&'a TyEnv> for NzEnv {
fn from(x: &'a TyEnv) -> Self {
- x.as_nzenv()
+ x.to_nzenv()
}
}
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index edba477..a1666a4 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -56,13 +56,13 @@ impl TyExpr {
}
/// Eval the TyExpr. It will actually get evaluated only as needed on demand.
- pub fn eval<'e>(&self, env: impl Into<&'e NzEnv>) -> Value {
+ pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
Value::new_thunk(env.into(), self.to_hir())
}
/// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
/// needed on demand.
pub fn eval_closed_expr(&self) -> Value {
- self.eval(&NzEnv::new())
+ self.eval(NzEnv::new())
}
/// Eval a closed TyExpr fully and recursively;
pub fn rec_eval_closed_expr(&self) -> Value {