summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/semantics/builtins.rs7
-rw-r--r--dhall/src/semantics/hir.rs2
-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
-rw-r--r--dhall/src/semantics/tck/env.rs14
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs4
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<Value>, 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<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(),
}
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 {
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-01 11:46:53 +0000