summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/core/thunk.rs12
-rw-r--r--dhall/src/core/value.rs10
-rw-r--r--dhall/src/phase/mod.rs4
-rw-r--r--dhall/src/phase/normalize.rs21
-rw-r--r--dhall/src/phase/typecheck.rs11
-rw-r--r--dhall_syntax/src/core/context.rs2
-rw-r--r--dhall_syntax/src/core/expr.rs16
-rw-r--r--dhall_syntax/src/core/visitor.rs15
-rw-r--r--dhall_syntax/src/printer.rs6
9 files changed, 32 insertions, 65 deletions
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index c18014e..4d193f9 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -2,7 +2,7 @@ use std::borrow::Cow;
use std::cell::{Ref, RefCell};
use std::rc::Rc;
-use dhall_syntax::{Const, ExprF, X};
+use dhall_syntax::{Const, ExprF};
use crate::core::context::{NormalizationContext, TypecheckContext};
use crate::core::value::Value;
@@ -12,7 +12,7 @@ use crate::phase::normalize::{
apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr,
};
use crate::phase::typecheck::type_of_const;
-use crate::phase::{NormalizedSubExpr, Type, Typed};
+use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed};
#[derive(Debug, Clone, Copy)]
enum Marker {
@@ -30,7 +30,7 @@ enum ThunkInternal {
/// 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.
- PartialExpr(ExprF<Thunk, X>),
+ PartialExpr(ExprF<Thunk, Normalized>),
/// Partially normalized value.
/// Invariant: if the marker is `NF`, the value must be fully normalized
Value(Marker, Value),
@@ -123,7 +123,7 @@ impl Thunk {
ThunkInternal::Value(WHNF, v).into_thunk()
}
- pub fn from_partial_expr(e: ExprF<Thunk, X>) -> Thunk {
+ pub fn from_partial_expr(e: ExprF<Thunk, Normalized>) -> Thunk {
ThunkInternal::PartialExpr(e).into_thunk()
}
@@ -309,7 +309,7 @@ impl Shift for ThunkInternal {
e.traverse_ref_with_special_handling_of_binders(
|v| Ok(v.shift(delta, var)?),
|x, v| Ok(v.shift(delta, &var.under_binder(x))?),
- |x| Ok(X::clone(x)),
+ |x| Ok(Normalized::clone(x)),
)?,
),
ThunkInternal::Value(m, v) => {
@@ -356,7 +356,7 @@ impl Subst<Typed> for ThunkInternal {
&val.under_binder(x),
)
},
- X::clone,
+ Normalized::clone,
),
),
ThunkInternal::Value(_, v) => {
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 8486d6e..88d7a20 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -2,7 +2,7 @@ use std::collections::HashMap;
use dhall_syntax::{
rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
- NaiveDouble, Natural, X,
+ NaiveDouble, Natural,
};
use crate::core::thunk::{Thunk, TypedThunk};
@@ -10,7 +10,7 @@ use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
use crate::phase::normalize::{
apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr,
};
-use crate::phase::Typed;
+use crate::phase::{Normalized, Typed};
/// A semantic value. The invariants ensure this value represents a Weak-Head
/// Normal Form (WHNF). This means that this first constructor is the first constructor of the
@@ -59,7 +59,7 @@ pub enum Value {
TextLit(Vec<InterpolatedTextContents<Thunk>>),
Equivalence(TypedThunk, TypedThunk),
// Invariant: this must not contain a value captured by one of the variants above.
- PartialExpr(ExprF<Thunk, X>),
+ PartialExpr(ExprF<Thunk, Normalized>),
}
impl Value {
@@ -475,7 +475,7 @@ impl Shift for Value {
e.traverse_ref_with_special_handling_of_binders(
|v| Ok(v.shift(delta, var)?),
|x, v| Ok(v.shift(delta, &var.under_binder(x))?),
- |x| Ok(X::clone(x)),
+ |x| Ok(Normalized::clone(x)),
)?,
),
})
@@ -500,7 +500,7 @@ impl Subst<Typed> for Value {
&val.under_binder(x),
)
},
- X::clone,
+ Normalized::clone,
))
}
// Retry normalizing since substituting may allow progress
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index 8c93889..7364949 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -2,7 +2,7 @@ use std::borrow::Cow;
use std::fmt::Display;
use std::path::Path;
-use dhall_syntax::{Const, Import, SubExpr, X};
+use dhall_syntax::{Const, Import, SubExpr};
use crate::core::thunk::{Thunk, TypedThunk};
use crate::core::value::Value;
@@ -20,7 +20,7 @@ pub(crate) mod typecheck;
pub type ParsedSubExpr = SubExpr<Import>;
pub type DecodedSubExpr = SubExpr<Import>;
pub type ResolvedSubExpr = SubExpr<Normalized>;
-pub type NormalizedSubExpr = SubExpr<X>;
+pub type NormalizedSubExpr = SubExpr<Normalized>;
#[derive(Debug, Clone)]
pub struct Parsed(ParsedSubExpr, ImportRoot);
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 644f98c..f1045a5 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -2,14 +2,14 @@ use std::collections::HashMap;
use dhall_syntax::{
BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents,
- NaiveDouble, X,
+ NaiveDouble,
};
use crate::core::context::NormalizationContext;
use crate::core::thunk::{Thunk, TypedThunk};
use crate::core::value::Value;
use crate::core::var::Subst;
-use crate::phase::{NormalizedSubExpr, ResolvedSubExpr, Typed};
+use crate::phase::{Normalized, NormalizedSubExpr, ResolvedSubExpr, Typed};
pub type InputSubExpr = ResolvedSubExpr;
pub type OutputSubExpr = NormalizedSubExpr;
@@ -86,7 +86,7 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
// Empty string literal.
[] => {
// Printing InterpolatedText takes care of all the escaping
- let txt: InterpolatedText<X> =
+ let txt: InterpolatedText<Normalized> =
std::iter::empty().collect();
let s = txt.to_string();
Ok((
@@ -98,10 +98,11 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
// interpolations, there is a single Text item) in the literal.
[InterpolatedTextContents::Text(s)] => {
// Printing InterpolatedText takes care of all the escaping
- let txt: InterpolatedText<X> = std::iter::once(
- InterpolatedTextContents::Text(s.clone()),
- )
- .collect();
+ let txt: InterpolatedText<Normalized> =
+ std::iter::once(InterpolatedTextContents::Text(
+ s.clone(),
+ ))
+ .collect();
let s = txt.to_string();
Ok((
r,
@@ -376,7 +377,7 @@ pub fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
}
// Thunk subexpressions
- let expr: ExprF<Thunk, X> =
+ let expr: ExprF<Thunk, Normalized> =
expr.as_ref().map_ref_with_special_handling_of_binders(
|e| Thunk::new(ctx.clone(), e.clone()),
|x, e| Thunk::new(ctx.skip(x), e.clone()),
@@ -391,7 +392,7 @@ enum Ret<'a> {
Value(Value),
Thunk(Thunk),
ThunkRef(&'a Thunk),
- Expr(ExprF<Thunk, X>),
+ Expr(ExprF<Thunk, Normalized>),
}
/// Performs an intersection of two HashMaps.
@@ -636,7 +637,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
})
}
-pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
+pub fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
use Value::{
AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam,
NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index ecf9793..96ff246 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -2,7 +2,6 @@ use std::collections::HashMap;
use dhall_syntax::{
rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, SubExpr,
- X,
};
use crate::core::context::{NormalizationContext, TypecheckContext};
@@ -214,7 +213,7 @@ macro_rules! make_type {
};
}
-fn type_of_builtin(b: Builtin) -> Expr<X> {
+fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
use dhall_syntax::Builtin::*;
match b {
Bool | Natural | Integer | Double | Text => make_type!(Type),
@@ -398,7 +397,7 @@ fn type_with(
/// layer.
fn type_last_layer(
ctx: &TypecheckContext,
- e: &ExprF<Typed, X>,
+ e: &ExprF<Typed, Normalized>,
) -> Result<Ret, TypeError> {
use crate::error::TypeMessage::*;
use dhall_syntax::BinOp::*;
@@ -598,9 +597,7 @@ fn type_last_layer(
}
}
Const(c) => Ok(RetWhole(Typed::from_const(*c))),
- Builtin(b) => {
- Ok(RetTypeOnly(mktype(ctx, rc(type_of_builtin(*b)).absurd())?))
- }
+ Builtin(b) => Ok(RetTypeOnly(mktype(ctx, rc(type_of_builtin(*b)))?)),
BoolLit(_) => Ok(RetTypeOnly(builtin_to_type(Bool)?)),
NaturalLit(_) => Ok(RetTypeOnly(builtin_to_type(Natural)?)),
IntegerLit(_) => Ok(RetTypeOnly(builtin_to_type(Integer)?)),
@@ -1016,7 +1013,7 @@ pub fn typecheck(e: Resolved) -> Result<Typed, TypeError> {
pub fn typecheck_with(e: Resolved, ty: &Type) -> Result<Typed, TypeError> {
let expr: SubExpr<_> = e.0;
- let ty: SubExpr<_> = ty.to_expr().absurd();
+ let ty: SubExpr<_> = ty.to_expr();
type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
}
pub fn skip_typecheck(e: Resolved) -> Typed {
diff --git a/dhall_syntax/src/core/context.rs b/dhall_syntax/src/core/context.rs
index eeec121..6844baa 100644
--- a/dhall_syntax/src/core/context.rs
+++ b/dhall_syntax/src/core/context.rs
@@ -4,7 +4,7 @@ use std::hash::Hash;
/// A `(Context a)` associates `Text` labels with values of type `a`
///
-/// The `Context` is used for type-checking when `(a = Expr X)`
+/// The `Context` is used for type-checking when `(a = Expr)`
///
/// * You create a `Context` using `empty` and `insert`
/// * You transform a `Context` using `fmap`
diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs
index 0cbece3..e08d816 100644
--- a/dhall_syntax/src/core/expr.rs
+++ b/dhall_syntax/src/core/expr.rs
@@ -10,9 +10,9 @@ pub type Double = NaiveDouble;
/// An empty type
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
-pub enum X {}
+pub enum Void {}
-pub fn trivial_result<T>(x: Result<T, X>) -> T {
+pub fn trivial_result<T>(x: Result<T, Void>) -> T {
match x {
Ok(x) => x,
Err(e) => match e {},
@@ -351,12 +351,6 @@ impl<E> Expr<E> {
}
}
-impl Expr<X> {
- pub fn absurd<E>(&self) -> Expr<E> {
- self.visit(&mut visitor::AbsurdVisitor)
- }
-}
-
impl<E> SubExpr<E> {
pub fn as_ref(&self) -> &Expr<E> {
&self.0.as_ref().0
@@ -416,12 +410,6 @@ impl<E> SubExpr<E> {
}
}
-impl SubExpr<X> {
- pub fn absurd<T>(&self) -> SubExpr<T> {
- SubExpr::from_expr_no_span(self.as_ref().absurd())
- }
-}
-
impl<E> Clone for SubExpr<E> {
fn clone(&self) -> Self {
SubExpr(Rc::clone(&self.0))
diff --git a/dhall_syntax/src/core/visitor.rs b/dhall_syntax/src/core/visitor.rs
index 50ec68a..e39e95b 100644
--- a/dhall_syntax/src/core/visitor.rs
+++ b/dhall_syntax/src/core/visitor.rs
@@ -243,7 +243,7 @@ impl<'a, T, SE1, SE2, E1, E2> ExprFFallibleVisitor<'a, SE1, SE2, E1, E2>
where
T: ExprFInFallibleVisitor<'a, SE1, SE2, E1, E2>,
{
- type Error = X;
+ type Error = Void;
fn visit_subexpr(&mut self, subexpr: &'a SE1) -> Result<SE2, Self::Error> {
Ok(self.0.visit_subexpr(subexpr))
@@ -379,16 +379,3 @@ where
(self.0)(embed)
}
}
-
-pub struct AbsurdVisitor;
-
-impl<'a, 'b, E> ExprFInFallibleVisitor<'a, SubExpr<X>, SubExpr<E>, X, E>
- for &'b mut AbsurdVisitor
-{
- fn visit_subexpr(&mut self, subexpr: &'a SubExpr<X>) -> SubExpr<E> {
- SubExpr::from_expr_no_span(subexpr.as_ref().visit(&mut **self))
- }
- fn visit_embed(self, embed: &'a X) -> E {
- match *embed {}
- }
-}
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index 95eafe5..25d4ca8 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -491,9 +491,3 @@ impl<Label: Display> Display for V<Label> {
Ok(())
}
}
-
-impl Display for X {
- fn fmt(&self, _: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- match *self {}
- }
-}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 21:20:28 +0000