summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/phase
diff options
context:
space:
mode:
authorNadrieril2019-12-27 15:31:06 +0000
committerNadrieril2020-01-17 10:06:00 +0000
commit5542797c77a9dfcdffec539f1a82341a450291a2 (patch)
treee11cf53df0d6c06d67da2f148ca9eaf0fa1af620 /dhall/src/semantics/phase
parente97e0c8e9905582aef826504b59a1844c8f67613 (diff)
s/TypecheckContext/TyCtx/
Diffstat (limited to 'dhall/src/semantics/phase')
-rw-r--r--dhall/src/semantics/phase/typecheck.rs22
1 files changed, 8 insertions, 14 deletions
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(