summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/core
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/core')
-rw-r--r--dhall/src/semantics/core/context.rs12
-rw-r--r--dhall/src/semantics/core/value.rs6
2 files changed, 8 insertions, 10 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)),
}
}
}