summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r--dhall/src/semantics/core/value.rs10
-rw-r--r--dhall/src/semantics/core/var.rs32
-rw-r--r--dhall/src/semantics/core/visitor.rs2
-rw-r--r--dhall/src/semantics/nze/env.rs2
-rw-r--r--dhall/src/semantics/tck/env.rs10
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs26
6 files changed, 32 insertions, 50 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 7334552..918826b 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -3,7 +3,7 @@ use std::collections::HashMap;
use std::rc::Rc;
use crate::error::{TypeError, TypeMessage};
-use crate::semantics::core::var::{AlphaVar, Binder};
+use crate::semantics::core::var::Binder;
use crate::semantics::phase::normalize::{apply_any, normalize_whnf};
use crate::semantics::phase::typecheck::{
builtin_to_value, builtin_to_value_env, const_to_value,
@@ -83,7 +83,7 @@ pub(crate) enum ValueKind<Value> {
// Keep env around to construct Foo/build closures; hopefully temporary.
AppliedBuiltin(Builtin, Vec<Value>, Vec<Value>, NzEnv),
- Var(AlphaVar, NzVar),
+ Var(NzVar),
Const(Const),
BoolLit(bool),
NaturalLit(Natural),
@@ -258,9 +258,7 @@ impl Value {
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(venv.lookup(w)),
+ ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)),
ValueKind::LamClosure {
binder,
annot,
@@ -618,7 +616,7 @@ impl Closure {
match self {
Closure::Closure { arg_ty, .. } => {
let val = Value::from_kind_and_type(
- ValueKind::Var(AlphaVar::default(), var),
+ ValueKind::Var(var),
arg_ty.clone(),
);
self.apply(val)
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index 3458489..264b81d 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -1,16 +1,4 @@
-use crate::syntax::{Label, V};
-
-/// Stores an alpha-normalized variable.
-#[derive(Clone, Copy, Eq)]
-pub struct AlphaVar {
- alpha: V<()>,
-}
-// TODO: temporary hopefully
-impl std::cmp::PartialEq for AlphaVar {
- fn eq(&self, _other: &Self) -> bool {
- true
- }
-}
+use crate::syntax::Label;
// Exactly like a Label, but equality returns always true.
// This is so that ValueKind equality is exactly alpha-equivalence.
@@ -19,18 +7,6 @@ pub struct Binder {
name: Label,
}
-impl AlphaVar {
- pub(crate) fn new(alpha: V<()>) -> Self {
- AlphaVar { alpha }
- }
- pub(crate) fn default() -> Self {
- AlphaVar { alpha: V((), 0) }
- }
- pub(crate) fn idx(&self) -> usize {
- self.alpha.idx()
- }
-}
-
impl Binder {
pub(crate) fn new(name: Label) -> Self {
Binder { name }
@@ -47,12 +23,6 @@ impl std::cmp::PartialEq for Binder {
}
}
-impl std::fmt::Debug for AlphaVar {
- fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
- write!(f, "AlphaVar({})", self.alpha.1)
- }
-}
-
impl std::fmt::Debug for Binder {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
write!(f, "Binder({})", &self.name)
diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs
index aec66f8..2191ce3 100644
--- a/dhall/src/semantics/core/visitor.rs
+++ b/dhall/src/semantics/core/visitor.rs
@@ -96,7 +96,7 @@ where
v.visit_vec(types)?,
env.clone(),
),
- Var(v, w) => Var(v.clone(), *w),
+ Var(v) => Var(*v),
Const(k) => Const(*k),
BoolLit(b) => BoolLit(*b),
NaturalLit(n) => NaturalLit(*n),
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index 203d99a..3c42ee7 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -66,7 +66,7 @@ impl NzEnv {
let idx = self.items.len() - 1 - var.idx();
match &self.items[idx] {
NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf(
- ValueKind::Var(var.clone(), NzVar::new(idx)),
+ ValueKind::Var(NzVar::new(idx)),
ty.clone(),
),
NzEnvItem::Replaced(x) => x.clone(),
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 32c2f21..1276a48 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -37,7 +37,7 @@ impl VarEnv {
}
pub fn lookup_fallible(&self, var: &NzVar) -> Option<AlphaVar> {
let idx = self.size.checked_sub(var.idx() + 1)?;
- Some(AlphaVar::new(V((), idx)))
+ Some(AlphaVar::new(idx))
}
}
@@ -68,7 +68,7 @@ impl NameEnv {
self.names.pop();
}
- pub fn unlabel_var(&self, var: &V<Label>) -> Option<AlphaVar> {
+ pub fn unlabel_var(&self, var: &V) -> Option<AlphaVar> {
let V(name, idx) = var;
let (idx, _) = self
.names
@@ -77,9 +77,9 @@ impl NameEnv {
.enumerate()
.filter(|(_, n)| *n == name)
.nth(*idx)?;
- Some(AlphaVar::new(V((), idx)))
+ Some(AlphaVar::new(idx))
}
- pub fn label_var(&self, var: &AlphaVar) -> V<Label> {
+ pub fn label_var(&self, var: &AlphaVar) -> V {
let name = &self.names[self.names.len() - 1 - var.idx()];
let idx = self
.names
@@ -129,7 +129,7 @@ impl TyEnv {
items: self.items.insert_value(e),
}
}
- pub fn lookup(&self, var: &V<Label>) -> Option<(TyExprKind, Type)> {
+ pub fn lookup(&self, var: &V) -> Option<(TyExprKind, Type)> {
let var = self.names.unlabel_var(var)?;
let ty = self.items.lookup_val(&var).get_type().unwrap();
Some((TyExprKind::Var(var), ty))
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 262cda6..114bb14 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,5 +1,4 @@
use crate::error::{TypeError, TypeMessage};
-use crate::semantics::core::var::AlphaVar;
use crate::semantics::phase::normalize::normalize_tyexpr_whnf;
use crate::semantics::phase::typecheck::rc;
use crate::semantics::phase::Normalized;
@@ -9,6 +8,19 @@ use crate::syntax::{ExprKind, Span, V};
pub(crate) type Type = Value;
+/// Stores an alpha-normalized variable.
+#[derive(Debug, Clone, Copy)]
+pub struct AlphaVar {
+ idx: usize,
+}
+
+#[derive(Debug, Clone)]
+pub(crate) enum TyExprKind {
+ Var(AlphaVar),
+ // Forbidden ExprKind variants: Var, Import, Embed
+ Expr(ExprKind<TyExpr, Normalized>),
+}
+
// An expression with inferred types at every node and resolved variables.
#[derive(Clone)]
pub(crate) struct TyExpr {
@@ -17,11 +29,13 @@ pub(crate) struct TyExpr {
span: Span,
}
-#[derive(Debug, Clone)]
-pub(crate) enum TyExprKind {
- Var(AlphaVar),
- // Forbidden ExprKind variants: Var, Import, Embed
- Expr(ExprKind<TyExpr, Normalized>),
+impl AlphaVar {
+ pub(crate) fn new(idx: usize) -> Self {
+ AlphaVar { idx }
+ }
+ pub(crate) fn idx(&self) -> usize {
+ self.idx
+ }
}
impl TyExpr {
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-11 16:00:02 +0000