diff options
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r-- | dhall/src/semantics/tck/env.rs | 14 | ||||
-rw-r--r-- | dhall/src/semantics/tck/tyexpr.rs | 4 |
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 { |