summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2019-05-09 16:53:48 +0200
committerNadrieril2019-05-09 16:53:48 +0200
commit32051979778436ea02cb406551f126fe22ea1636 (patch)
treebf2610cfc94b39e941a505946d50669b9674789c /dhall
parent7538e29275720407ac172bb05cdbc028d95ff921 (diff)
ExprF need not be generic in Label
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/core/thunk.rs8
-rw-r--r--dhall/src/core/value.rs4
-rw-r--r--dhall/src/phase/normalize.rs9
-rw-r--r--dhall/src/phase/typecheck.rs3
4 files changed, 9 insertions, 15 deletions
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index 51922e1..eed8685 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -1,7 +1,7 @@
use std::cell::{Ref, RefCell};
use std::rc::Rc;
-use dhall_syntax::{ExprF, Label, X};
+use dhall_syntax::{ExprF, X};
use crate::core::context::NormalizationContext;
use crate::core::context::TypecheckContext;
@@ -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, Label, X>),
+ PartialExpr(ExprF<Thunk, X>),
/// Partially normalized value.
/// Invariant: if the marker is `NF`, the value must be fully normalized
Value(Marker, Value),
@@ -121,7 +121,7 @@ impl Thunk {
Thunk::new(NormalizationContext::new(), e.absurd())
}
- pub(crate) fn from_partial_expr(e: ExprF<Thunk, Label, X>) -> Thunk {
+ pub(crate) fn from_partial_expr(e: ExprF<Thunk, X>) -> Thunk {
ThunkInternal::PartialExpr(e).into_thunk()
}
@@ -280,7 +280,6 @@ impl Shift for ThunkInternal {
|v| Ok(v.shift(delta, var)?),
|x, v| Ok(v.shift(delta, &var.under_binder(x))?),
|x| Ok(X::clone(x)),
- |l| Ok(Label::clone(l)),
)?,
),
ThunkInternal::Value(m, v) => {
@@ -322,7 +321,6 @@ impl Subst<Typed> for ThunkInternal {
)
},
X::clone,
- Label::clone,
),
),
ThunkInternal::Value(_, v) => {
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index e91b6bc..799cfac 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -58,7 +58,7 @@ pub(crate) enum Value {
// contiguous text values must be merged.
TextLit(Vec<InterpolatedTextContents<Thunk>>),
// Invariant: this must not contain a value captured by one of the variants above.
- PartialExpr(ExprF<Thunk, Label, X>),
+ PartialExpr(ExprF<Thunk, X>),
}
impl Value {
@@ -433,7 +433,6 @@ impl Shift for Value {
|v| Ok(v.shift(delta, var)?),
|x, v| Ok(v.shift(delta, &var.under_binder(x))?),
|x| Ok(X::clone(x)),
- |l| Ok(Label::clone(l)),
)?,
),
})
@@ -459,7 +458,6 @@ impl Subst<Typed> for Value {
)
},
X::clone,
- Label::clone,
))
}
// Retry normalizing since substituting may allow progress
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 52c1666..64de2a7 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -1,7 +1,7 @@
use std::collections::HashMap;
use dhall_syntax::{
- BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label,
+ BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents,
NaiveDouble, X,
};
@@ -356,12 +356,11 @@ pub(crate) fn normalize_whnf(
}
// Thunk subexpressions
- let expr: ExprF<Thunk, Label, X> =
+ let expr: ExprF<Thunk, X> =
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()),
|_| unreachable!(),
- Label::clone,
);
normalize_one_layer(expr)
@@ -372,7 +371,7 @@ enum Ret<'a> {
RetValue(Value),
RetThunk(Thunk),
RetThunkRef(&'a Thunk),
- RetExpr(ExprF<Thunk, Label, X>),
+ RetExpr(ExprF<Thunk, X>),
}
fn merge_maps<K, V>(
@@ -521,7 +520,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
})
}
-pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Label, X>) -> Value {
+pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
use Ret::{RetExpr, RetThunk, RetThunkRef, RetValue};
use Value::{
BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit, Lam,
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 497a703..2dc97bb 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -421,7 +421,6 @@ fn type_with(
|e| type_with(ctx, e.clone()),
|_, _| unreachable!(),
|_| unreachable!(),
- |l| Ok(Label::clone(l)),
)?;
let ret = type_last_layer(ctx, &expr)?;
let ret = match ret {
@@ -449,7 +448,7 @@ fn type_with(
/// layer.
fn type_last_layer(
ctx: &TypecheckContext,
- e: &ExprF<Typed, Label, X>,
+ e: &ExprF<Typed, X>,
) -> Result<Ret, TypeError> {
use crate::error::TypeMessage::*;
use dhall_syntax::BinOp::*;