From 32051979778436ea02cb406551f126fe22ea1636 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 9 May 2019 16:53:48 +0200 Subject: ExprF need not be generic in Label --- dhall/src/core/thunk.rs | 8 +++----- dhall/src/core/value.rs | 4 +--- 2 files changed, 4 insertions(+), 8 deletions(-) (limited to 'dhall/src/core') 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), + PartialExpr(ExprF), /// 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 { + pub(crate) fn from_partial_expr(e: ExprF) -> 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 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>), // Invariant: this must not contain a value captured by one of the variants above. - PartialExpr(ExprF), + PartialExpr(ExprF), } 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 for Value { ) }, X::clone, - Label::clone, )) } // Retry normalizing since substituting may allow progress -- cgit v1.2.3