diff options
Diffstat (limited to 'dhall/src/semantics/phase')
| -rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 9 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/typecheck.rs | 22 |
2 files changed, 15 insertions, 16 deletions
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 8f9a58a..541a196 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,10 +1,9 @@ use std::collections::HashMap; use std::convert::TryInto; -use crate::semantics::core::value::Value; -use crate::semantics::core::value::ValueKind; use crate::semantics::phase::typecheck::{rc, typecheck}; use crate::semantics::phase::Normalized; +use crate::semantics::{AlphaVar, Value, ValueKind}; use crate::syntax; use crate::syntax::Const::Type; use crate::syntax::{ @@ -367,9 +366,9 @@ pub(crate) fn apply_builtin( pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> { let f_borrow = f.as_whnf(); match &*f_borrow { - ValueKind::Lam(x, _, e) => { - e.subst_shift(&x.into(), &a).to_whnf_check_type(ty) - } + ValueKind::Lam(_, _, e) => e + .subst_shift(&AlphaVar::default(), &a) + .to_whnf_check_type(ty), ValueKind::AppliedBuiltin(b, args) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 852f41b..15025c1 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -6,7 +6,7 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TyCtx; use crate::semantics::phase::normalize::merge_maps; use crate::semantics::phase::Normalized; -use crate::semantics::{Binder, Value, ValueKind}; +use crate::semantics::{AlphaVar, Binder, Value, ValueKind}; use crate::syntax; use crate::syntax::{ Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span, @@ -385,15 +385,15 @@ fn type_last_layer( App(f, a) => { let tf = f.get_type()?; let tf_borrow = tf.as_whnf(); - let (x, tx, tb) = match &*tf_borrow { - ValueKind::Pi(x, tx, tb) => (x, tx, tb), + let (tx, tb) = match &*tf_borrow { + ValueKind::Pi(_, tx, tb) => (tx, tb), _ => return mkerr(NotAFunction(f.clone())), }; if &a.get_type()? != tx { return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone())); } - let ret = tb.subst_shift(&x.into(), a); + let ret = tb.subst_shift(&AlphaVar::default(), a); ret.normalize_nf(); RetTypeOnly(ret) } @@ -500,13 +500,12 @@ fn type_last_layer( ValueKind::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > Some(Some(t)) => { - let x = ctx.new_binder(x); RetTypeOnly( tck_pi_type( ctx, - x.clone(), + ctx.new_binder(x), t.clone(), - r.under_binder(x), + r.under_binder(), )? ) }, @@ -719,8 +718,8 @@ fn type_last_layer( // Union alternative with type Some(Some(variant_type)) => { let handler_type_borrow = handler_type.as_whnf(); - let (x, tx, tb) = match &*handler_type_borrow { - ValueKind::Pi(x, tx, tb) => (x, tx, tb), + let (tx, tb) = match &*handler_type_borrow { + ValueKind::Pi(_, tx, tb) => (tx, tb), _ => { return mkerr(NotAFunction( handler_type.clone(), @@ -736,8 +735,9 @@ fn type_last_layer( )); } - // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`. - match tb.over_binder(x) { + // Extract `tb` from under the binder. Fails if the variable was used + // in `tb`. + match tb.over_binder() { Some(x) => x, None => return mkerr( MergeHandlerReturnTypeMustNotBeDependent, |