summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2019-05-04 14:58:18 +0200
committerNadrieril2019-05-04 14:58:18 +0200
commit1b1c34b90bb4bf3859b05b1da6db2dcb374996bb (patch)
treea344a360f8735a3f33d05c04568d9449efa7ba4c /dhall
parentb6f57069b75febf1d312a98efcd6544c9db2fe59 (diff)
Move `Note`s into the spine of the AST
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/normalize.rs12
-rw-r--r--dhall/src/typecheck.rs2
2 files changed, 5 insertions, 9 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 4636859..4d87225 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -163,7 +163,7 @@ pub(crate) enum Value {
UnionLit(Label, Thunk, BTreeMap<Label, Option<TypeThunk>>),
TextLit(Vec<InterpolatedTextContents<Thunk>>),
/// Invariant: This must not contain a value captured by one of the variants above.
- PartialExpr(ExprF<Thunk, Label, X, X>),
+ PartialExpr(ExprF<Thunk, Label, X>),
}
impl Value {
@@ -497,7 +497,6 @@ impl Value {
|v| v.shift(delta, var),
|x, v| v.shift(delta, &var.shift(1, &x.into())),
X::clone,
- X::clone,
Label::clone,
))
}
@@ -607,7 +606,6 @@ impl Value {
)
},
X::clone,
- X::clone,
Label::clone,
))
}
@@ -1125,11 +1123,10 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
}
// Thunk subexpressions
- let expr: ExprF<Thunk, Label, X, X> =
+ let expr: ExprF<Thunk, Label, 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()),
- X::clone,
|_| unreachable!(),
Label::clone,
);
@@ -1137,7 +1134,7 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
normalize_one_layer(expr)
}
-fn normalize_one_layer(expr: ExprF<Thunk, Label, X, X>) -> Value {
+fn normalize_one_layer(expr: ExprF<Thunk, Label, X>) -> Value {
use Value::{
BoolLit, EmptyListLit, EmptyOptionalLit, Lam, NEListLit, NEOptionalLit,
NaturalLit, Pi, RecordLit, RecordType, TextLit, UnionConstructor,
@@ -1149,7 +1146,7 @@ fn normalize_one_layer(expr: ExprF<Thunk, Label, X, X>) -> Value {
RetValue(Value),
RetThunk(Thunk),
RetThunkRef(&'a Thunk),
- RetExpr(ExprF<Thunk, Label, X, X>),
+ RetExpr(ExprF<Thunk, Label, X>),
}
use Ret::{RetExpr, RetThunk, RetThunkRef, RetValue};
@@ -1157,7 +1154,6 @@ fn normalize_one_layer(expr: ExprF<Thunk, Label, X, X>) -> Value {
ExprF::Embed(_) => unreachable!(),
ExprF::Var(_) => unreachable!(),
ExprF::Annot(x, _) => RetThunk(x),
- ExprF::Note(_, e) => RetThunk(e),
ExprF::Lam(x, t, e) => RetValue(Lam(x, t, e)),
ExprF::Pi(x, t, e) => {
RetValue(Pi(x, TypeThunk::from_thunk(t), TypeThunk::from_thunk(e)))
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 74de59b..ce4ca96 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -719,7 +719,7 @@ fn type_with(
/// layer.
fn type_last_layer(
ctx: &TypecheckContext,
- e: ExprF<Typed, Label, X, Normalized>,
+ e: ExprF<Typed, Label, Normalized>,
) -> Result<Ret, TypeError> {
use dhall_syntax::BinOp::*;
use dhall_syntax::Builtin::*;