diff options
author | Nadrieril | 2019-05-04 14:58:18 +0200 |
---|---|---|
committer | Nadrieril | 2019-05-04 14:58:18 +0200 |
commit | 1b1c34b90bb4bf3859b05b1da6db2dcb374996bb (patch) | |
tree | a344a360f8735a3f33d05c04568d9449efa7ba4c /dhall | |
parent | b6f57069b75febf1d312a98efcd6544c9db2fe59 (diff) |
Move `Note`s into the spine of the AST
Diffstat (limited to 'dhall')
-rw-r--r-- | dhall/src/normalize.rs | 12 | ||||
-rw-r--r-- | dhall/src/typecheck.rs | 2 |
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::*; |