From 35cc98dc767247f4881866de40c7d8dd82eba8a5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 22:30:32 +0000 Subject: Remove types from NzEnv --- dhall/src/semantics/builtins.rs | 7 ++++-- dhall/src/semantics/hir.rs | 2 +- dhall/src/semantics/nze/env.rs | 42 +++++++++++++++++++++--------------- dhall/src/semantics/nze/normalize.rs | 2 +- dhall/src/semantics/nze/value.rs | 18 ++++++---------- dhall/src/semantics/tck/env.rs | 14 ++++++------ dhall/src/semantics/tck/tyexpr.rs | 4 ++-- 7 files changed, 47 insertions(+), 42 deletions(-) diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index 9d4f8a2..d9a3599 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -265,8 +265,11 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { Value(Value), DoneAsIs, } - let make_closure = - |e| typecheck(&skip_resolve(&e).unwrap()).unwrap().eval(&env); + let make_closure = |e| { + typecheck(&skip_resolve(&e).unwrap()) + .unwrap() + .eval(env.clone()) + }; let ret = match (b, args.as_slice()) { (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())), diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs index 28b38e3..9ad7374 100644 --- a/dhall/src/semantics/hir.rs +++ b/dhall/src/semantics/hir.rs @@ -70,7 +70,7 @@ impl Hir { /// Eval the Hir. It will actually get evaluated only as needed on demand. pub fn eval(&self, env: &NzEnv) -> Value { - Value::new_thunk(env, self.clone()) + Value::new_thunk(env.clone(), self.clone()) } /// Eval a closed Hir (i.e. without free variables). It will actually get evaluated only as /// needed on demand. 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 { // 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, +pub(crate) struct ValEnv { + items: Vec>, } +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 ValEnv { 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(), } 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, } 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) -> 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 { -- cgit v1.2.3