summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/expr.rs6
-rw-r--r--dhall/src/normalize.rs66
-rw-r--r--dhall/src/typecheck.rs16
3 files changed, 44 insertions, 44 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index 071bb92..7dbbf1c 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -58,7 +58,7 @@ impl std::fmt::Display for Normalized {
mod typed {
use super::{Type, Typed};
- use crate::normalize::{DoubleVar, Thunk, Value};
+ use crate::normalize::{AlphaVar, Thunk, Value};
use crate::typecheck::{
TypeError, TypeInternal, TypeMessage, TypecheckContext,
};
@@ -133,7 +133,7 @@ mod typed {
}
}
- pub(crate) fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
+ pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
match self {
TypedInternal::Value(th, t) => TypedInternal::Value(
th.shift(delta, var),
@@ -143,7 +143,7 @@ mod typed {
}
}
- pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
match self {
TypedInternal::Value(th, t) => TypedInternal::Value(
th.subst_shift(var, val),
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index f950826..35ab45d 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -34,11 +34,11 @@ impl Typed {
Normalized(self.0)
}
- pub(crate) fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
+ pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
Typed(self.0.shift(delta, var))
}
- pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
Typed(self.0.subst_shift(var, val))
}
@@ -54,12 +54,12 @@ impl Typed {
/// Stores a pair of variables: a normal one and if relevant one
/// that corresponds to the alpha-normalized version of the first one.
#[derive(Debug, Clone, Eq)]
-pub(crate) struct DoubleVar {
+pub(crate) struct AlphaVar {
normal: V<Label>,
alpha: Option<V<()>>,
}
-impl DoubleVar {
+impl AlphaVar {
pub(crate) fn to_var(&self, alpha: bool) -> V<Label> {
match (alpha, &self.alpha) {
(true, Some(x)) => V("_".into(), x.1),
@@ -67,13 +67,13 @@ impl DoubleVar {
}
}
pub(crate) fn from_var(normal: V<Label>) -> Self {
- DoubleVar {
+ AlphaVar {
normal,
alpha: None,
}
}
- pub(crate) fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
- DoubleVar {
+ pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+ AlphaVar {
normal: self.normal.shift(delta, &var.normal),
alpha: match (&self.alpha, &var.alpha) {
(Some(x), Some(v)) => Some(x.shift(delta, v)),
@@ -84,7 +84,7 @@ impl DoubleVar {
}
/// Equality is up to alpha-equivalence.
-impl std::cmp::PartialEq for DoubleVar {
+impl std::cmp::PartialEq for AlphaVar {
fn eq(&self, other: &Self) -> bool {
match (&self.alpha, &other.alpha) {
(Some(x), Some(y)) => x == y,
@@ -94,27 +94,27 @@ impl std::cmp::PartialEq for DoubleVar {
}
}
-impl From<Label> for DoubleVar {
- fn from(x: Label) -> DoubleVar {
- DoubleVar {
+impl From<Label> for AlphaVar {
+ fn from(x: Label) -> AlphaVar {
+ AlphaVar {
normal: V(x, 0),
alpha: Some(V((), 0)),
}
}
}
-impl<'a> From<&'a Label> for DoubleVar {
- fn from(x: &'a Label) -> DoubleVar {
+impl<'a> From<&'a Label> for AlphaVar {
+ fn from(x: &'a Label) -> AlphaVar {
x.clone().into()
}
}
-impl From<AlphaLabel> for DoubleVar {
- fn from(x: AlphaLabel) -> DoubleVar {
+impl From<AlphaLabel> for AlphaVar {
+ fn from(x: AlphaLabel) -> AlphaVar {
let l: Label = x.into();
l.into()
}
}
-impl<'a> From<&'a AlphaLabel> for DoubleVar {
- fn from(x: &'a AlphaLabel) -> DoubleVar {
+impl<'a> From<&'a AlphaLabel> for AlphaVar {
+ fn from(x: &'a AlphaLabel) -> AlphaVar {
x.clone().into()
}
}
@@ -157,11 +157,11 @@ impl From<AlphaLabel> for Label {
#[derive(Debug, Clone)]
enum EnvItem {
Thunk(Thunk),
- Skip(DoubleVar),
+ Skip(AlphaVar),
}
impl EnvItem {
- fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
use EnvItem::*;
match self {
Thunk(e) => Thunk(e.shift(delta, var)),
@@ -169,7 +169,7 @@ impl EnvItem {
}
}
- pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
match self {
EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)),
EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.to_thunk()),
@@ -198,7 +198,7 @@ impl NormalizationContext {
Some(EnvItem::Thunk(t)) => t.to_value(),
Some(EnvItem::Skip(newvar)) => Value::Var(newvar.clone()),
// Free variable
- None => Value::Var(DoubleVar::from_var(var.clone())),
+ None => Value::Var(AlphaVar::from_var(var.clone())),
}
}
pub(crate) fn from_typecheck_ctx(
@@ -218,11 +218,11 @@ impl NormalizationContext {
NormalizationContext(Rc::new(ctx))
}
- fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var))))
}
- fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
+ fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
NormalizationContext(Rc::new(
self.0.map(|_, e| e.subst_shift(var, val)),
))
@@ -245,7 +245,7 @@ pub(crate) enum Value {
NaturalSuccClosure,
Pi(AlphaLabel, TypeThunk, TypeThunk),
- Var(DoubleVar),
+ Var(AlphaVar),
Const(Const),
BoolLit(bool),
NaturalLit(Natural),
@@ -521,7 +521,7 @@ impl Value {
Value::AppliedBuiltin(b, vec![])
}
- fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
match self {
Value::Lam(x, t, e) => Value::Lam(
x.clone(),
@@ -618,7 +618,7 @@ impl Value {
}
}
- pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
match self {
// Retry normalizing since substituting may allow progress
Value::AppliedBuiltin(b, args) => apply_builtin(
@@ -731,7 +731,7 @@ impl Value {
mod thunk {
use super::{
- apply_any, normalize_whnf, DoubleVar, InputSubExpr,
+ apply_any, normalize_whnf, AlphaVar, InputSubExpr,
NormalizationContext, OutputSubExpr, Value,
};
use crate::expr::Typed;
@@ -811,7 +811,7 @@ mod thunk {
}
}
- fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
match self {
ThunkInternal::Unnormalized(ctx, e) => {
ThunkInternal::Unnormalized(
@@ -825,7 +825,7 @@ mod thunk {
}
}
- fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
+ fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
match self {
ThunkInternal::Unnormalized(ctx, e) => {
ThunkInternal::Unnormalized(
@@ -930,11 +930,11 @@ mod thunk {
apply_any(self.clone(), th)
}
- pub(crate) fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
+ pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
self.0.borrow().shift(delta, var).into_thunk()
}
- pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
self.0.borrow().subst_shift(var, val).into_thunk()
}
}
@@ -997,14 +997,14 @@ impl TypeThunk {
self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
}
- fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
match self {
TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)),
TypeThunk::Type(t) => TypeThunk::Type(t.shift(delta, var)),
}
}
- pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
match self {
TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)),
TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 2b87bd2..8d6b6eb 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -6,7 +6,7 @@ use std::fmt;
use crate::expr::*;
use crate::normalize::{
- DoubleVar, NormalizationContext, Thunk, TypeThunk, Value,
+ AlphaVar, NormalizationContext, Thunk, TypeThunk, Value,
};
use crate::traits::DynamicType;
use dhall_proc_macros as dhall;
@@ -45,7 +45,7 @@ impl Typed {
}
impl Normalized {
- fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
Normalized(self.0.shift(delta, var))
}
pub(crate) fn to_type(self) -> Type {
@@ -72,10 +72,10 @@ impl Type {
fn internal_whnf(&self) -> Option<Value> {
self.0.whnf()
}
- pub(crate) fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
+ pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
Type(self.0.shift(delta, var))
}
- pub(crate) fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
Type(self.0.subst_shift(var, val))
}
@@ -147,14 +147,14 @@ impl TypeInternal {
_ => None,
}
}
- fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
use TypeInternal::*;
match self {
Typed(e) => Typed(Box::new(e.shift(delta, var))),
Const(c) => Const(*c),
}
}
- fn subst_shift(&self, var: &DoubleVar, val: &Typed) -> Self {
+ fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
use TypeInternal::*;
match self {
Typed(e) => Typed(Box::new(e.subst_shift(var, val))),
@@ -172,12 +172,12 @@ impl PartialEq for TypeInternal {
#[derive(Debug, Clone)]
pub(crate) enum EnvItem {
- Type(DoubleVar, Type),
+ Type(AlphaVar, Type),
Value(Normalized),
}
impl EnvItem {
- fn shift(&self, delta: isize, var: &DoubleVar) -> Self {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
use EnvItem::*;
match self {
Type(v, e) => Type(v.shift(delta, var), e.shift(delta, var)),
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 10:46:03 +0000