summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r--dhall/src/semantics/core/context.rs12
-rw-r--r--dhall/src/semantics/core/value.rs6
-rw-r--r--dhall/src/semantics/phase/typecheck.rs22
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(