summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/semantics/core/context.rs10
-rw-r--r--dhall/src/semantics/core/value.rs40
-rw-r--r--dhall/src/semantics/core/visitor.rs2
-rw-r--r--dhall/src/semantics/nze/mod.rs2
-rw-r--r--dhall/src/semantics/nze/nzexpr.rs14
5 files changed, 49 insertions, 19 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index 8c64c26..7972a20 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -2,6 +2,7 @@ use crate::error::TypeError;
use crate::semantics::core::value::Value;
use crate::semantics::core::value::ValueKind;
use crate::semantics::core::var::{AlphaVar, Binder};
+use crate::semantics::nze::NzVar;
use crate::syntax::{Label, V};
#[derive(Debug, Clone)]
@@ -42,7 +43,6 @@ impl TyCtx {
let mut var = var.clone();
let mut shift_delta: isize = 0;
let mut rev_ctx = self.ctx.iter().rev().map(|(b, i)| (b.to_label(), i));
-
let found_item = loop {
if let Some((label, item)) = rev_ctx.next() {
var = match var.over_binder(&label) {
@@ -57,10 +57,16 @@ impl TyCtx {
return None;
}
};
+ let var_idx = rev_ctx
+ .filter(|(_, i)| match i {
+ CtxItem::Kept(_) => true,
+ CtxItem::Replaced(_) => false,
+ })
+ .count();
let v = match found_item {
CtxItem::Kept(t) => Value::from_kind_and_type(
- ValueKind::Var(AlphaVar::default()),
+ ValueKind::Var(AlphaVar::default(), NzVar::new(var_idx)),
t.clone(),
),
CtxItem::Replaced(v) => v.clone(),
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index dc6a116..a7c207d 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -4,6 +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::phase::normalize::{apply_any, normalize_whnf};
use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value};
use crate::semantics::phase::{
@@ -60,7 +61,7 @@ pub(crate) enum ValueKind<Value> {
// Invariant: in whnf, the evaluation must not be able to progress further.
AppliedBuiltin(Builtin, Vec<Value>),
- Var(AlphaVar),
+ Var(AlphaVar, NzVar),
Const(Const),
BoolLit(bool),
NaturalLit(Natural),
@@ -167,7 +168,7 @@ impl Value {
self.normalize_nf();
}
- self.to_tyexpr().to_expr(opts)
+ self.to_tyexpr(QuoteEnv::new()).to_expr(opts)
}
pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind<Value> {
self.as_whnf().clone()
@@ -257,7 +258,7 @@ impl Value {
match &*self.as_kind() {
// If the var matches, we can just reuse the provided value instead of copying it.
// We also check that the types match, if in debug mode.
- ValueKind::Var(v) if v == var => {
+ ValueKind::Var(v, _) if v == var => {
if let Ok(self_ty) = self.get_type() {
val.check_type(&self_ty.subst_shift(var, val));
}
@@ -288,18 +289,27 @@ impl Value {
// }
// }
- pub fn to_tyexpr(&self) -> TyExpr {
+ pub fn to_tyexpr(&self, qenv: QuoteEnv) -> TyExpr {
let self_kind = self.as_kind();
let self_ty = self.as_internal().ty.clone();
let self_span = self.as_internal().span.clone();
- if let ValueKind::Var(v) = &*self_kind {
- return TyExpr::new(TyExprKind::Var(*v), self_ty, self_span);
+ if let ValueKind::Var(v, _w) = &*self_kind {
+ return TyExpr::new(
+ // TODO: Only works when we don't normalize under lambdas
+ // TyExprKind::Var(qenv.lookup(w)),
+ TyExprKind::Var(*v),
+ self_ty,
+ self_span,
+ );
}
// TODO: properly recover intermediate types; `None` is a time-bomb here.
- let self_kind = self_kind.map_ref(|v| v.to_tyexpr());
+ let self_kind = self_kind.map_ref_with_special_handling_of_binders(
+ |v| v.to_tyexpr(qenv),
+ |_, _, v| v.to_tyexpr(qenv.insert()),
+ );
let expr = match self_kind {
- ValueKind::Var(_) => unreachable!(),
+ ValueKind::Var(..) => unreachable!(),
ValueKind::Lam(x, t, e) => ExprKind::Lam(x.to_label(), t, e),
ValueKind::Pi(x, t, e) => ExprKind::Pi(x.to_label(), t, e),
ValueKind::AppliedBuiltin(b, args) => {
@@ -320,13 +330,13 @@ 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(),
+ builtin_to_value(Builtin::OptionalNone).to_tyexpr(qenv),
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(),
+ builtin_to_value(Builtin::List).to_tyexpr(qenv),
n,
)),
Some(const_to_value(Const::Type)),
@@ -470,7 +480,7 @@ impl ValueKind<Value> {
pub(crate) fn normalize_mut(&mut self) {
match self {
- ValueKind::Var(_)
+ ValueKind::Var(..)
| ValueKind::Const(_)
| ValueKind::BoolLit(_)
| ValueKind::NaturalLit(_)
@@ -545,7 +555,7 @@ impl ValueKind<Value> {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(match self {
- ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?),
+ ValueKind::Var(v, w) => ValueKind::Var(v.shift(delta, var)?, *w),
_ => self.traverse_ref_with_special_handling_of_binders(
|x| Ok(x.shift(delta, var)?),
|_, _, x| Ok(x.shift(delta, &var.under_binder())?),
@@ -554,8 +564,10 @@ impl ValueKind<Value> {
}
fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
match self {
- ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(),
- ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()),
+ ValueKind::Var(v, _) if v == var => val.to_whnf_ignore_type(),
+ ValueKind::Var(v, w) => {
+ ValueKind::Var(v.shift(-1, var).unwrap(), *w)
+ }
_ => self.map_ref_with_special_handling_of_binders(
|x| x.subst_shift(var, val),
|_, _, x| {
diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs
index a449f6c..5a04747 100644
--- a/dhall/src/semantics/core/visitor.rs
+++ b/dhall/src/semantics/core/visitor.rs
@@ -81,7 +81,7 @@ where
Pi(l.clone(), t, e)
}
AppliedBuiltin(b, xs) => AppliedBuiltin(*b, v.visit_vec(xs)?),
- Var(v) => Var(v.clone()),
+ Var(v, w) => Var(v.clone(), *w),
Const(k) => Const(*k),
BoolLit(b) => BoolLit(*b),
NaturalLit(n) => NaturalLit(*n),
diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs
index ef8918f..213404c 100644
--- a/dhall/src/semantics/nze/mod.rs
+++ b/dhall/src/semantics/nze/mod.rs
@@ -1,2 +1,2 @@
pub mod nzexpr;
-// pub(crate) use nzexpr::*;
+pub(crate) use nzexpr::*;
diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs
index 3a5a1f9..1256ea0 100644
--- a/dhall/src/semantics/nze/nzexpr.rs
+++ b/dhall/src/semantics/nze/nzexpr.rs
@@ -82,10 +82,16 @@ pub(crate) struct QuoteEnv {
}
// Reverse-debruijn index: counts number of binders from the bottom of the stack.
-#[derive(Debug, Clone, Copy)]
+#[derive(Debug, Clone, Copy, Eq)]
pub(crate) struct NzVar {
idx: usize,
}
+// TODO: temporary hopefully
+impl std::cmp::PartialEq for NzVar {
+ fn eq(&self, _other: &Self) -> bool {
+ true
+ }
+}
impl TyEnv {
pub fn new() -> Self {
@@ -219,6 +225,12 @@ impl QuoteEnv {
}
}
+impl NzVar {
+ pub fn new(idx: usize) -> Self {
+ NzVar { idx }
+ }
+}
+
impl TyExpr {
pub fn new(kind: TyExprKind, ty: Option<Type>) -> Self {
TyExpr {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 09:21:16 +0000