summaryrefslogtreecommitdiff
path: root/dhall/src/core
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/core')
-rw-r--r--dhall/src/core/context.rs31
-rw-r--r--dhall/src/core/thunk.rs59
-rw-r--r--dhall/src/core/value.rs5
-rw-r--r--dhall/src/core/var.rs6
4 files changed, 21 insertions, 80 deletions
diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index 9230a2e..3c07c1c 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -19,9 +19,6 @@ enum CtxItem<T> {
struct Context<T>(Rc<Vec<(Label, CtxItem<T>)>>);
#[derive(Debug, Clone)]
-pub(crate) struct NormalizationContext(Context<()>);
-
-#[derive(Debug, Clone)]
pub(crate) struct TypecheckContext(Context<Type>);
impl<T> Context<T> {
@@ -117,22 +114,6 @@ impl<T> Context<T> {
}
}
-impl NormalizationContext {
- pub fn new() -> Self {
- NormalizationContext(Context::new())
- }
- pub fn skip(&self, x: &Label) -> Self {
- NormalizationContext(self.0.insert_kept(x, ()))
- }
- pub fn lookup(&self, var: &V<Label>) -> Value {
- match self.0.lookup(var) {
- Ok(CtxItem::Replaced(t, ())) => t.to_value(),
- Ok(CtxItem::Kept(newvar, ())) => Value::Var(newvar.clone()),
- Err(var) => Value::Var(AlphaVar::from_var(var)),
- }
- }
-}
-
impl TypecheckContext {
pub fn new() -> Self {
TypecheckContext(Context::new())
@@ -180,12 +161,6 @@ impl<T: Clone + Shift> Shift for Context<T> {
}
}
-impl Shift for NormalizationContext {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(NormalizationContext(self.0.shift(delta, var)?))
- }
-}
-
impl<T: Subst<Typed>> Subst<Typed> for CtxItem<T> {
fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
match self {
@@ -209,12 +184,6 @@ impl<T: Clone + Subst<Typed>> Subst<Typed> for Context<T> {
}
}
-impl Subst<Typed> for NormalizationContext {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- NormalizationContext(self.0.subst_shift(var, val))
- }
-}
-
impl PartialEq for TypecheckContext {
fn eq(&self, _: &Self) -> bool {
// don't count contexts when comparing stuff
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index 54a5442..87541d3 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -4,13 +4,11 @@ use std::rc::Rc;
use dhall_syntax::{Const, ExprF};
-use crate::core::context::{NormalizationContext, TypecheckContext};
+use crate::core::context::TypecheckContext;
use crate::core::value::Value;
use crate::core::var::{AlphaVar, Shift, Subst};
use crate::error::{TypeError, TypeMessage};
-use crate::phase::normalize::{
- apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr,
-};
+use crate::phase::normalize::{apply_any, normalize_one_layer, OutputSubExpr};
use crate::phase::typecheck::type_of_const;
use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed};
@@ -25,8 +23,6 @@ use Marker::{NF, WHNF};
#[derive(Debug)]
enum ThunkInternal {
- /// Non-normalized value alongside a normalization context
- Unnormalized(NormalizationContext, InputSubExpr),
/// Partially normalized value whose subexpressions have been thunked (this is returned from
/// typechecking). Note that this is different from `Value::PartialExpr` because there is no
/// requirement of WHNF here.
@@ -63,12 +59,6 @@ impl ThunkInternal {
fn normalize_whnf(&mut self) {
match self {
- ThunkInternal::Unnormalized(ctx, e) => {
- *self = ThunkInternal::Value(
- WHNF,
- normalize_whnf(ctx.clone(), e.clone()),
- )
- }
ThunkInternal::PartialExpr(e) => {
*self =
ThunkInternal::Value(WHNF, normalize_one_layer(e.clone()))
@@ -80,8 +70,7 @@ impl ThunkInternal {
fn normalize_nf(&mut self) {
match self {
- ThunkInternal::Unnormalized(_, _)
- | ThunkInternal::PartialExpr(_) => {
+ ThunkInternal::PartialExpr(_) => {
self.normalize_whnf();
self.normalize_nf();
}
@@ -97,8 +86,7 @@ impl ThunkInternal {
// Always use normalize_whnf before
fn as_whnf(&self) -> &Value {
match self {
- ThunkInternal::Unnormalized(_, _)
- | ThunkInternal::PartialExpr(_) => unreachable!(),
+ ThunkInternal::PartialExpr(_) => unreachable!(),
ThunkInternal::Value(_, v) => v,
}
}
@@ -106,19 +94,15 @@ impl ThunkInternal {
// Always use normalize_nf before
fn as_nf(&self) -> &Value {
match self {
- ThunkInternal::Unnormalized(_, _)
- | ThunkInternal::PartialExpr(_)
- | ThunkInternal::Value(WHNF, _) => unreachable!(),
+ ThunkInternal::PartialExpr(_) | ThunkInternal::Value(WHNF, _) => {
+ unreachable!()
+ }
ThunkInternal::Value(NF, v) => v,
}
}
}
impl Thunk {
- pub(crate) fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk {
- ThunkInternal::Unnormalized(ctx, e).into_thunk()
- }
-
pub(crate) fn from_value(v: Value) -> Thunk {
ThunkInternal::Value(WHNF, v).into_thunk()
}
@@ -141,8 +125,7 @@ impl Thunk {
fn do_normalize_whnf(&self) {
let borrow = self.0.borrow();
match &*borrow {
- ThunkInternal::Unnormalized(_, _)
- | ThunkInternal::PartialExpr(_) => {
+ ThunkInternal::PartialExpr(_) => {
drop(borrow);
self.0.borrow_mut().normalize_whnf();
}
@@ -154,9 +137,7 @@ impl Thunk {
fn do_normalize_nf(&self) {
let borrow = self.0.borrow();
match &*borrow {
- ThunkInternal::Unnormalized(_, _)
- | ThunkInternal::PartialExpr(_)
- | ThunkInternal::Value(WHNF, _) => {
+ ThunkInternal::PartialExpr(_) | ThunkInternal::Value(WHNF, _) => {
drop(borrow);
self.0.borrow_mut().normalize_nf();
}
@@ -183,7 +164,10 @@ impl Thunk {
self.as_value().clone()
}
- pub(crate) fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr {
+ pub(crate) fn normalize_to_expr_maybe_alpha(
+ &self,
+ alpha: bool,
+ ) -> OutputSubExpr {
self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
}
@@ -222,7 +206,10 @@ impl TypedThunk {
self.clone().into_typed()
}
- pub(crate) fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr {
+ pub(crate) fn normalize_to_expr_maybe_alpha(
+ &self,
+ alpha: bool,
+ ) -> OutputSubExpr {
self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
}
@@ -302,9 +289,6 @@ impl Shift for Thunk {
impl Shift for ThunkInternal {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(match self {
- ThunkInternal::Unnormalized(ctx, e) => {
- ThunkInternal::Unnormalized(ctx.shift(delta, var)?, e.clone())
- }
ThunkInternal::PartialExpr(e) => ThunkInternal::PartialExpr(
e.traverse_ref_with_special_handling_of_binders(
|v| Ok(v.shift(delta, var)?),
@@ -342,10 +326,6 @@ impl Subst<Typed> for Thunk {
impl Subst<Typed> for ThunkInternal {
fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
match self {
- ThunkInternal::Unnormalized(ctx, e) => ThunkInternal::Unnormalized(
- ctx.subst_shift(var, val),
- e.clone(),
- ),
ThunkInternal::PartialExpr(e) => ThunkInternal::PartialExpr(
e.map_ref_with_special_handling_of_binders(
|v| v.subst_shift(var, val),
@@ -404,11 +384,6 @@ impl std::fmt::Debug for Thunk {
ThunkInternal::PartialExpr(e) => {
f.debug_tuple("Thunk@PartialExpr").field(e).finish()
}
- ThunkInternal::Unnormalized(ctx, e) => f
- .debug_tuple("Thunk@Unnormalized")
- .field(ctx)
- .field(e)
- .finish(),
}
}
}
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 61a8eea..d3d017d 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -66,7 +66,10 @@ impl Value {
}
/// Convert the value to a fully normalized syntactic expression. Also alpha-normalize
/// if alpha is `true`
- pub(crate) fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr {
+ pub(crate) fn normalize_to_expr_maybe_alpha(
+ &self,
+ alpha: bool,
+ ) -> OutputSubExpr {
match self {
Value::Lam(x, t, e) => rc(ExprF::Lam(
x.to_label_maybe_alpha(alpha),
diff --git a/dhall/src/core/var.rs b/dhall/src/core/var.rs
index 4ef1b93..5e7bf05 100644
--- a/dhall/src/core/var.rs
+++ b/dhall/src/core/var.rs
@@ -61,12 +61,6 @@ impl AlphaVar {
_ => self.normal.clone(),
}
}
- pub(crate) fn from_var(normal: V<Label>) -> Self {
- AlphaVar {
- normal,
- alpha: None,
- }
- }
pub(crate) fn from_var_and_alpha(normal: V<Label>, alpha: usize) -> Self {
AlphaVar {
normal,
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-02 21:50:33 +0000