summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs5
-rw-r--r--dhall/src/semantics/tck/typecheck.rs30
2 files changed, 8 insertions, 27 deletions
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index e4108ad..abb6fa8 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,4 +1,3 @@
-#![allow(dead_code)]
use crate::error::{TypeError, TypeMessage};
use crate::semantics::core::var::AlphaVar;
use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv};
@@ -58,10 +57,6 @@ impl TyExpr {
let mut env = env.iter().collect();
tyexpr_to_expr(self, opts, &mut env)
}
- // TODO: temporary hack
- pub fn to_value(&self) -> Value {
- todo!()
- }
pub fn normalize_whnf(&self, env: &NzEnv) -> Value {
normalize_tyexpr_whnf(self, env)
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index abb36e1..99eb31f 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -1,12 +1,8 @@
-#![allow(dead_code)]
-#![allow(unreachable_code)]
-#![allow(unused_imports)]
use std::borrow::Cow;
use std::cmp::max;
use std::collections::HashMap;
use crate::error::{TypeError, TypeMessage};
-use crate::semantics::core::context::TyCtx;
use crate::semantics::nze::{NameEnv, NzVar, QuoteEnv};
use crate::semantics::phase::normalize::{merge_maps, NzEnv};
use crate::semantics::phase::typecheck::{
@@ -14,12 +10,12 @@ use crate::semantics::phase::typecheck::{
};
use crate::semantics::phase::Normalized;
use crate::semantics::{
- AlphaVar, Binder, Closure, TyExpr, TyExprKind, Type, Value, ValueKind,
+ Binder, Closure, TyExpr, TyExprKind, Type, Value, ValueKind,
};
use crate::syntax;
use crate::syntax::{
BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label,
- Span, UnspannedExpr, V,
+ Span, V,
};
#[derive(Debug, Clone)]
@@ -111,6 +107,8 @@ fn mkerr<T>(x: impl ToString) -> Result<T, TypeError> {
Err(TypeError::new(TypeMessage::Custom(x.to_string())))
}
+/// When all sub-expressions have been typed, check the remaining toplevel
+/// layer.
fn type_one_layer(
env: &TyEnv,
kind: &ExprKind<TyExpr, Normalized>,
@@ -503,20 +501,6 @@ fn type_one_layer(
Some(Some(variant_type)) => {
let handler_type_borrow = handler_type.as_whnf();
match &*handler_type_borrow {
- ValueKind::Pi(_, tx, tb) => {
- if variant_type != tx {
- return mkerr("MergeHandlerTypeMismatch");
- }
-
- // Extract `tb` from under the binder. Fails if the variable was used
- // in `tb`.
- match tb.over_binder() {
- Some(x) => x,
- None => return mkerr(
- "MergeHandlerReturnTypeMustNotBeDependent",
- ),
- }
- }
ValueKind::PiClosure { closure, annot, .. } => {
if variant_type != annot {
// return mkerr("MergeHandlerTypeMismatch");
@@ -609,8 +593,7 @@ fn type_one_layer(
})
}
-/// Type-check an expression and return the expression alongside its type if type-checking
-/// succeeded, or an error if type-checking failed.
+/// `type_with` typechecks an expressio in the provided environment.
pub(crate) fn type_with(
env: &TyEnv,
expr: &Expr<Normalized>,
@@ -689,10 +672,13 @@ pub(crate) fn type_with(
Ok(TyExpr::new(tyekind, ty, expr.span()))
}
+/// Typecheck an expression and return the expression annotated with types if type-checking
+/// succeeded, or an error if type-checking failed.
pub(crate) fn typecheck(e: &Expr<Normalized>) -> Result<TyExpr, TypeError> {
type_with(&TyEnv::new(), e)
}
+/// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
pub(crate) fn typecheck_with(
expr: &Expr<Normalized>,
ty: Expr<Normalized>,