summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/semantics/core/value.rs36
-rw-r--r--dhall/src/semantics/nze/nzexpr.rs13
-rw-r--r--dhall/src/semantics/tck/typecheck.rs34
3 files changed, 40 insertions, 43 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 30c4116..df1382b 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
use crate::error::{TypeError, TypeMessage};
use crate::semantics::core::var::{AlphaVar, Binder};
-use crate::semantics::nze::{NzVar, QuoteEnv};
+use crate::semantics::nze::{NzVar, VarEnv};
use crate::semantics::phase::normalize::{apply_any, normalize_whnf, NzEnv};
use crate::semantics::phase::typecheck::{
builtin_to_value, builtin_to_value_env, const_to_value,
@@ -277,21 +277,21 @@ impl Value {
}
}
- pub fn to_tyexpr(&self, qenv: QuoteEnv) -> TyExpr {
+ pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
let tye = match &*self.as_kind() {
// ValueKind::Var(v, _w) => TyExprKind::Var(*v),
// TODO: Only works when we don't normalize under lambdas
- ValueKind::Var(_v, w) => TyExprKind::Var(qenv.lookup(w)),
+ ValueKind::Var(_v, w) => TyExprKind::Var(venv.lookup(w)),
ValueKind::LamClosure {
binder,
annot,
closure,
} => TyExprKind::Expr(ExprKind::Lam(
binder.to_label(),
- annot.to_tyexpr(qenv),
+ annot.to_tyexpr(venv),
closure
- .apply_var(NzVar::new(qenv.size()))
- .to_tyexpr(qenv.insert()),
+ .apply_var(NzVar::new(venv.size()))
+ .to_tyexpr(venv.insert()),
)),
ValueKind::PiClosure {
binder,
@@ -299,10 +299,10 @@ impl Value {
closure,
} => TyExprKind::Expr(ExprKind::Pi(
binder.to_label(),
- annot.to_tyexpr(qenv),
+ annot.to_tyexpr(venv),
closure
- .apply_var(NzVar::new(qenv.size()))
- .to_tyexpr(qenv.insert()),
+ .apply_var(NzVar::new(venv.size()))
+ .to_tyexpr(venv.insert()),
)),
ValueKind::AppliedBuiltin(b, args, types, _) => {
TyExprKind::Expr(args.into_iter().zip(types.into_iter()).fold(
@@ -314,7 +314,7 @@ impl Value {
Some(ty.clone()),
Span::Artificial,
),
- v.to_tyexpr(qenv),
+ v.to_tyexpr(venv),
)
},
))
@@ -327,7 +327,7 @@ impl Value {
.map(|(k, v)| {
(
k.clone(),
- v.as_ref().map(|v| v.to_tyexpr(qenv)),
+ v.as_ref().map(|v| v.to_tyexpr(venv)),
)
})
.collect(),
@@ -349,7 +349,7 @@ impl Value {
(
k.clone(),
v.as_ref()
- .map(|v| v.to_tyexpr(qenv)),
+ .map(|v| v.to_tyexpr(venv)),
)
})
.collect(),
@@ -362,14 +362,14 @@ impl Value {
Some(ctort.clone()),
Span::Artificial,
),
- v.to_tyexpr(qenv),
+ v.to_tyexpr(venv),
))
}
self_kind => {
let self_kind = self_kind
.map_ref_with_special_handling_of_binders(
- |v| v.to_tyexpr(qenv),
- |_, _, v| v.to_tyexpr(qenv.insert()),
+ |v| v.to_tyexpr(venv),
+ |_, _, v| v.to_tyexpr(venv.insert()),
);
let expr = match self_kind {
ValueKind::Var(..)
@@ -384,14 +384,14 @@ impl Value {
ValueKind::IntegerLit(n) => ExprKind::IntegerLit(n),
ValueKind::DoubleLit(n) => ExprKind::DoubleLit(n),
ValueKind::EmptyOptionalLit(n) => ExprKind::App(
- builtin_to_value(Builtin::OptionalNone).to_tyexpr(qenv),
+ builtin_to_value(Builtin::OptionalNone).to_tyexpr(venv),
n,
),
ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n),
ValueKind::EmptyListLit(n) => {
ExprKind::EmptyListLit(TyExpr::new(
TyExprKind::Expr(ExprKind::App(
- builtin_to_value(Builtin::List).to_tyexpr(qenv),
+ builtin_to_value(Builtin::List).to_tyexpr(venv),
n,
)),
Some(const_to_value(Const::Type)),
@@ -425,7 +425,7 @@ impl Value {
TyExpr::new(tye, self_ty, self_span)
}
pub fn to_tyexpr_noenv(&self) -> TyExpr {
- self.to_tyexpr(QuoteEnv::new())
+ self.to_tyexpr(VarEnv::new())
}
}
diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs
index 7263cac..87d0269 100644
--- a/dhall/src/semantics/nze/nzexpr.rs
+++ b/dhall/src/semantics/nze/nzexpr.rs
@@ -9,7 +9,7 @@ pub(crate) struct NameEnv {
}
#[derive(Debug, Clone, Copy)]
-pub(crate) struct QuoteEnv {
+pub(crate) struct VarEnv {
size: usize,
}
@@ -30,8 +30,8 @@ impl NameEnv {
names: names.collect(),
}
}
- pub fn as_quoteenv(&self) -> QuoteEnv {
- QuoteEnv {
+ pub fn as_varenv(&self) -> VarEnv {
+ VarEnv {
size: self.names.len(),
}
}
@@ -72,16 +72,15 @@ impl NameEnv {
}
}
-// TODO: rename to VarEnv
-impl QuoteEnv {
+impl VarEnv {
pub fn new() -> Self {
- QuoteEnv { size: 0 }
+ VarEnv { size: 0 }
}
pub fn size(&self) -> usize {
self.size
}
pub fn insert(&self) -> Self {
- QuoteEnv {
+ VarEnv {
size: self.size + 1,
}
}
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 99eb31f..7a225f7 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -3,7 +3,7 @@ use std::cmp::max;
use std::collections::HashMap;
use crate::error::{TypeError, TypeMessage};
-use crate::semantics::nze::{NameEnv, NzVar, QuoteEnv};
+use crate::semantics::nze::{NameEnv, NzVar, VarEnv};
use crate::semantics::phase::normalize::{merge_maps, NzEnv};
use crate::semantics::phase::typecheck::{
builtin_to_value, const_to_value, type_of_builtin,
@@ -39,8 +39,8 @@ impl TyEnv {
items: items.clone(),
}
}
- pub fn as_quoteenv(&self) -> QuoteEnv {
- self.names.as_quoteenv()
+ pub fn as_varenv(&self) -> VarEnv {
+ self.names.as_varenv()
}
pub fn as_nzenv(&self) -> &NzEnv {
&self.items
@@ -194,7 +194,7 @@ fn type_one_layer(
let ty = type_of_recordtype(
kts.iter()
- .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_quoteenv()))),
+ .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
)?;
Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
}
@@ -282,13 +282,13 @@ fn type_one_layer(
return mkerr(format!(
"annot mismatch: ({} : {}) : {}",
x.to_expr_tyenv(env),
- x_ty.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env),
- t.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env)
+ x_ty.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
+ t.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
));
// return mkerr(format!(
// "annot mismatch: {} != {}",
- // x_ty.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env),
- // t.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env)
+ // x_ty.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
+ // t.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
// ));
// return mkerr(format!("annot mismatch: {:#?} : {:#?}", x, t,));
}
@@ -314,11 +314,9 @@ fn type_one_layer(
"function annot mismatch: ({} : {}) : {}",
arg.to_expr_tyenv(env),
arg.get_type()?
- .to_tyexpr(env.as_quoteenv())
- .to_expr_tyenv(env),
- annot
- .to_tyexpr(env.as_quoteenv())
+ .to_tyexpr(env.as_varenv())
.to_expr_tyenv(env),
+ annot.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
));
}
@@ -373,15 +371,15 @@ fn type_one_layer(
// Construct the final record type
let ty = type_of_recordtype(
kts.iter()
- .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_quoteenv()))),
+ .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
)?;
Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
}
ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
let ekind = ExprKind::BinOp(
BinOp::RecursiveRecordTypeMerge,
- x.get_type()?.to_tyexpr(env.as_quoteenv()),
- y.get_type()?.to_tyexpr(env.as_quoteenv()),
+ x.get_type()?.to_tyexpr(env.as_varenv()),
+ y.get_type()?.to_tyexpr(env.as_varenv()),
);
let ty = type_one_layer(env, &ekind)?;
TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial)
@@ -406,8 +404,8 @@ fn type_one_layer(
env,
&ExprKind::BinOp(
BinOp::RecursiveRecordTypeMerge,
- tx.to_tyexpr(env.as_quoteenv()),
- ty.to_tyexpr(env.as_quoteenv()),
+ tx.to_tyexpr(env.as_varenv()),
+ ty.to_tyexpr(env.as_varenv()),
),
)?;
}
@@ -613,7 +611,7 @@ pub(crate) fn type_with(
TyExprKind::Expr(ExprKind::Pi(
binder.clone(),
annot.clone(),
- body_ty.to_tyexpr(body_env.as_quoteenv()),
+ body_ty.to_tyexpr(body_env.as_varenv()),
)),
Some(type_of_function(annot.get_type()?, body_ty.get_type()?)?),
Span::Artificial,
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 17:21:52 +0000