From 5542797c77a9dfcdffec539f1a82341a450291a2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 15:31:06 +0000 Subject: s/TypecheckContext/TyCtx/ --- dhall/src/error/mod.rs | 9 +++------ dhall/src/semantics/core/context.rs | 12 ++++++------ dhall/src/semantics/core/value.rs | 6 ++---- dhall/src/semantics/phase/typecheck.rs | 22 ++++++++-------------- 4 files changed, 19 insertions(+), 30 deletions(-) (limited to 'dhall') diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 6e7be64..56bc8ab 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -1,6 +1,6 @@ use std::io::Error as IOError; -use crate::semantics::core::context::TypecheckContext; +use crate::semantics::core::context::TyCtx; use crate::semantics::core::value::Value; use crate::semantics::phase::resolve::ImportStack; use crate::semantics::phase::NormalizedExpr; @@ -41,7 +41,7 @@ pub enum EncodeError { #[derive(Debug)] pub struct TypeError { message: TypeMessage, - context: TypecheckContext, + context: TyCtx, } /// The specific type error @@ -88,10 +88,7 @@ pub(crate) enum TypeMessage { } impl TypeError { - pub(crate) fn new( - context: &TypecheckContext, - message: TypeMessage, - ) -> Self { + pub(crate) fn new(context: &TyCtx, message: TypeMessage) -> Self { TypeError { context: context.clone(), message, 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.shift(delta, var) } @@ -134,7 +134,7 @@ impl Subst for CtxItem { } } -impl Subst for TypecheckContext { +impl Subst 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>, ) -> Result { use std::collections::hash_map::Entry; @@ -79,10 +79,7 @@ fn tck_record_type( )) } -fn tck_union_type( - ctx: &TypecheckContext, - kts: Iter, -) -> Result +fn tck_union_type(ctx: &TyCtx, kts: Iter) -> Result where Iter: IntoIterator), TypeError>>, { @@ -294,7 +291,7 @@ fn type_of_builtin(b: Builtin) -> Expr { } 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, -) -> Result { +fn type_with(ctx: &TyCtx, e: Expr) -> Result { 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, span: Span, ) -> Result { @@ -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) -> Result { - type_with(&TypecheckContext::new(), e) + type_with(&TyCtx::new(), e) } pub(crate) fn typecheck_with( -- cgit v1.2.3