3 files changed, 16 insertions, 24 deletions

diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index 5a0c320..ed63b63 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -13,16 +13,16 @@ enum CtxItem {
 }
 
 #[derive(Debug, Clone)]
-pub(crate) struct TypecheckContext {
+pub(crate) struct TyCtx {
     ctx: Vec<(Label, CtxItem)>,
 }
 
-impl TypecheckContext {
+impl TyCtx {
     pub fn new() -> Self {
-        TypecheckContext { ctx: Vec::new() }
+        TyCtx { ctx: Vec::new() }
     }
     fn with_vec(&self, vec: Vec<(Label, CtxItem)>) -> Self {
-        TypecheckContext { ctx: vec }
+        TyCtx { ctx: vec }
     }
     pub fn insert_type(&self, x: &Label, t: Value) -> Self {
         let mut vec = self.ctx.clone();
@@ -116,7 +116,7 @@ impl Shift for CtxItem {
     }
 }
 
-impl Shift for TypecheckContext {
+impl Shift for TyCtx {
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         self.shift(delta, var)
     }
@@ -134,7 +134,7 @@ impl Subst<Value> for CtxItem {
     }
 }
 
-impl Subst<Value> for TypecheckContext {
+impl Subst<Value> for TyCtx {
     fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         self.subst_shift(var, val)
     }
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 6fa00ac..f06c614 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -3,7 +3,7 @@ use std::collections::HashMap;
 use std::rc::Rc;
 
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::core::context::TypecheckContext;
+use crate::semantics::core::context::TyCtx;
 use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
 use crate::semantics::phase::normalize::{apply_any, normalize_whnf};
 use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value};
@@ -292,9 +292,7 @@ impl ValueInternal {
     fn get_type(&self) -> Result<&Value, TypeError> {
         match &self.ty {
             Some(t) => Ok(t),
-            None => {
-                Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
-            }
+            None => Err(TypeError::new(&TyCtx::new(), TypeMessage::Sort)),
         }
     }
 }
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 3960146..16eabea 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -3,7 +3,7 @@ use std::cmp::max;
 use std::collections::HashMap;
 
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::core::context::TypecheckContext;
+use crate::semantics::core::context::TyCtx;
 use crate::semantics::core::value::Value;
 use crate::semantics::core::value::ValueKind;
 use crate::semantics::core::var::{Shift, Subst};
@@ -16,7 +16,7 @@ use crate::syntax::{
 };
 
 fn tck_pi_type(
-    ctx: &TypecheckContext,
+    ctx: &TyCtx,
     x: Label,
     tx: Value,
     te: Value,
@@ -48,7 +48,7 @@ fn tck_pi_type(
 }
 
 fn tck_record_type(
-    ctx: &TypecheckContext,
+    ctx: &TyCtx,
     kts: impl IntoIterator<Item = Result<(Label, Value), TypeError>>,
 ) -> Result<Value, TypeError> {
     use std::collections::hash_map::Entry;
@@ -79,10 +79,7 @@ fn tck_record_type(
     ))
 }
 
-fn tck_union_type<Iter>(
-    ctx: &TypecheckContext,
-    kts: Iter,
-) -> Result<Value, TypeError>
+fn tck_union_type<Iter>(ctx: &TyCtx, kts: Iter) -> Result<Value, TypeError>
 where
     Iter: IntoIterator<Item = Result<(Label, Option<Value>), TypeError>>,
 {
@@ -294,7 +291,7 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
 }
 
 pub(crate) fn builtin_to_value(b: Builtin) -> Value {
-    let ctx = TypecheckContext::new();
+    let ctx = TyCtx::new();
     Value::from_kind_and_type(
         ValueKind::from_builtin(b),
         type_with(&ctx, type_of_builtin(b)).unwrap(),
@@ -305,10 +302,7 @@ pub(crate) fn builtin_to_value(b: Builtin) -> Value {
 /// succeeded, or an error if type-checking failed.
 /// Some normalization is done while typechecking, so the returned expression might be partially
 /// normalized as well.
-fn type_with(
-    ctx: &TypecheckContext,
-    e: Expr<Normalized>,
-) -> Result<Value, TypeError> {
+fn type_with(ctx: &TyCtx, e: Expr<Normalized>) -> Result<Value, TypeError> {
     use syntax::ExprKind::{Annot, Embed, Lam, Let, Pi, Var};
     let span = e.span();
 
@@ -364,7 +358,7 @@ fn type_with(
 /// When all sub-expressions have been typed, check the remaining toplevel
 /// layer.
 fn type_last_layer(
-    ctx: &TypecheckContext,
+    ctx: &TyCtx,
     e: ExprKind<Value, Normalized>,
     span: Span,
 ) -> Result<Value, TypeError> {
@@ -827,7 +821,7 @@ fn type_last_layer(
 /// expression must be closed (i.e. no free variables), otherwise type-checking
 /// will fail.
 pub(crate) fn typecheck(e: Expr<Normalized>) -> Result<Value, TypeError> {
-    type_with(&TypecheckContext::new(), e)
+    type_with(&TyCtx::new(), e)
 }
 
 pub(crate) fn typecheck_with(