diff options
author | Nadrieril | 2019-05-09 16:53:48 +0200 |
---|---|---|
committer | Nadrieril | 2019-05-09 16:53:48 +0200 |
commit | 32051979778436ea02cb406551f126fe22ea1636 (patch) | |
tree | bf2610cfc94b39e941a505946d50669b9674789c /dhall | |
parent | 7538e29275720407ac172bb05cdbc028d95ff921 (diff) |
ExprF need not be generic in Label
Diffstat (limited to 'dhall')
-rw-r--r-- | dhall/src/core/thunk.rs | 8 | ||||
-rw-r--r-- | dhall/src/core/value.rs | 4 | ||||
-rw-r--r-- | dhall/src/phase/normalize.rs | 9 | ||||
-rw-r--r-- | dhall/src/phase/typecheck.rs | 3 |
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::*; |