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 +--- dhall/src/phase/normalize.rs | 9 ++++----- dhall/src/phase/typecheck.rs | 3 +-- 4 files changed, 9 insertions(+), 15 deletions(-) (limited to 'dhall') 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 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 = + let expr: ExprF = 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), + RetExpr(ExprF), } fn merge_maps( @@ -521,7 +520,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option> { }) } -pub(crate) fn normalize_one_layer(expr: ExprF) -> Value { +pub(crate) fn normalize_one_layer(expr: ExprF) -> 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, + e: &ExprF, ) -> Result { use crate::error::TypeMessage::*; use dhall_syntax::BinOp::*; -- cgit v1.2.3