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/core/context.rs | 12 +++++++----- dhall/src/semantics/core/value.rs | 26 ++++++++++---------------- dhall/src/semantics/core/var.rs | 21 ++------------------- dhall/src/semantics/phase/normalize.rs | 9 ++++----- dhall/src/semantics/phase/typecheck.rs | 22 +++++++++++----------- 5 files changed, 34 insertions(+), 56 deletions(-) diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index 47d2d2d..8c64c26 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -6,7 +6,9 @@ use crate::syntax::{Label, V}; #[derive(Debug, Clone)] enum CtxItem { - Kept(AlphaVar, Value), + // Variable is bound with given type + Kept(Value), + // Variable has been replaced by corresponding value Replaced(Value), } @@ -24,7 +26,7 @@ impl TyCtx { } pub fn insert_type(&self, x: &Binder, t: Value) -> Self { let mut vec = self.ctx.clone(); - vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x)))); + vec.push((x.clone(), CtxItem::Kept(t.under_binder()))); self.with_vec(vec) } pub fn insert_value( @@ -47,7 +49,7 @@ impl TyCtx { Some(newvar) => newvar, None => break item, }; - if let CtxItem::Kept(_, _) = item { + if let CtxItem::Kept(_) = item { shift_delta += 1; } } else { @@ -57,8 +59,8 @@ impl TyCtx { }; let v = match found_item { - CtxItem::Kept(newvar, t) => Value::from_kind_and_type( - ValueKind::Var(newvar.clone()), + CtxItem::Kept(t) => Value::from_kind_and_type( + ValueKind::Var(AlphaVar::default()), t.clone(), ), CtxItem::Replaced(v) => v.clone(), diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 6ae0a90..8b3ada1 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -209,9 +209,9 @@ impl Value { pub(crate) fn app(&self, v: Value) -> Value { let body_t = match &*self.get_type_not_sort().as_whnf() { - ValueKind::Pi(x, t, e) => { + ValueKind::Pi(_, t, e) => { v.check_type(t); - e.subst_shift(&x.into(), &v) + e.subst_shift(&AlphaVar::default(), &v) } _ => unreachable!("Internal type error"), }; @@ -242,18 +242,12 @@ impl Value { pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(self.as_internal().shift(delta, var)?.into_value()) } - pub(crate) fn over_binder(&self, x: T) -> Option - where - T: Into, - { - self.shift(-1, &x.into()) + pub(crate) fn over_binder(&self) -> Option { + self.shift(-1, &AlphaVar::default()) } - pub(crate) fn under_binder(&self, x: T) -> Self - where - T: Into, - { + pub(crate) fn under_binder(&self) -> Self { // Can't fail since delta is positive - self.shift(1, &x.into()).unwrap() + self.shift(1, &AlphaVar::default()).unwrap() } pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { match &*self.as_kind() { @@ -456,18 +450,18 @@ impl ValueKind { ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?), _ => self.traverse_ref_with_special_handling_of_binders( |x| Ok(x.shift(delta, var)?), - |b, _, x| Ok(x.shift(delta, &var.under_binder(b))?), + |_, _, x| Ok(x.shift(delta, &var.under_binder())?), )?, }) } fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { match self { ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(), - ValueKind::Var(v) => ValueKind::Var(v.over_binder(var).unwrap()), + ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()), _ => self.map_ref_with_special_handling_of_binders( |x| x.subst_shift(var, val), - |b, _, x| { - x.subst_shift(&var.under_binder(b), &val.under_binder(b)) + |_, _, x| { + x.subst_shift(&var.under_binder(), &val.under_binder()) }, ), } diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index 93776bf..b336c66 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -26,15 +26,9 @@ impl AlphaVar { alpha: self.alpha.shift(delta, &var.alpha)?, }) } - pub(crate) fn under_binder(&self, x: T) -> Self - where - T: Into, - { + pub(crate) fn under_binder(&self) -> Self { // Can't fail since delta is positive - self.shift(1, &x.into()).unwrap() - } - pub(crate) fn over_binder(&self, x: &AlphaVar) -> Option { - self.shift(-1, x) + self.shift(1, &AlphaVar::default()).unwrap() } } @@ -82,17 +76,6 @@ impl std::fmt::Debug for Binder { } } -impl From for AlphaVar { - fn from(x: Binder) -> AlphaVar { - AlphaVar { alpha: V((), 0) } - } -} -impl<'a> From<&'a Binder> for AlphaVar { - fn from(x: &'a Binder) -> AlphaVar { - AlphaVar { alpha: V((), 0) } - } -} - impl From for Label { fn from(x: Binder) -> Label { x.name 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 { 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