From b7d847cc812e6a7ce52354b15a9ed6b41ffeb3b4 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 17 Jan 2020 18:57:52 +0000
Subject: Simplify

---
 dhall/src/semantics/phase/normalize.rs |  9 ++++-----
 dhall/src/semantics/phase/typecheck.rs | 22 +++++++++++-----------
 2 files changed, 15 insertions(+), 16 deletions(-)

(limited to 'dhall/src/semantics/phase')

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,
-- 
cgit v1.2.3