summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r--dhall/src/semantics/tck/env.rs6
-rw-r--r--dhall/src/semantics/tck/typecheck.rs204
2 files changed, 113 insertions, 97 deletions
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 812ca7a..1fc711c 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, NzEnv, NzVar, TyExprKind, Type, Value};
+use crate::semantics::{AlphaVar, NzEnv, NzVar, Type, Value};
use crate::syntax::{Label, V};
/// Environment for indexing variables.
@@ -116,9 +116,9 @@ impl TyEnv {
items: self.items.insert_value(e),
}
}
- pub fn lookup(&self, var: &V) -> Option<(TyExprKind, Type)> {
+ pub fn lookup(&self, var: &V) -> Option<(AlphaVar, Type)> {
let var = self.names.unlabel_var(var)?;
let ty = self.items.lookup_ty(&var);
- Some((TyExprKind::Var(var), ty))
+ Some((var, ty))
}
}
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index a652663..e642b8f 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -35,19 +35,6 @@ fn function_check(a: Const, b: Const) -> Const {
}
}
-fn type_of_function(src: Type, tgt: Type) -> Result<Type, TypeError> {
- let ks = match src.as_const() {
- Some(k) => k,
- _ => return Err(TypeError::new(TypeMessage::InvalidInputType(src))),
- };
- let kt = match tgt.as_const() {
- Some(k) => k,
- _ => return Err(TypeError::new(TypeMessage::InvalidOutputType(tgt))),
- };
-
- Ok(Value::from_const(function_check(ks, kt)))
-}
-
fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
Err(TypeError::new(TypeMessage::Custom(x.to_string())))
}
@@ -64,12 +51,55 @@ fn type_one_layer(
"There should remain no imports in a resolved expression"
),
ExprKind::Var(..)
- | ExprKind::Lam(..)
- | ExprKind::Pi(..)
- | ExprKind::Let(..)
| ExprKind::Const(Const::Sort)
| ExprKind::Embed(..) => unreachable!(), // Handled in type_with
+ ExprKind::Lam(binder, annot, body) => {
+ let body_ty = body.get_type()?;
+ let body_ty = body_ty.to_tyexpr(env.as_varenv().insert());
+ let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty);
+ let pi_ty = type_one_layer(env, &pi_ekind, Span::Artificial)?;
+ let ty = TyExpr::new(
+ TyExprKind::Expr(pi_ekind),
+ Some(pi_ty),
+ Span::Artificial,
+ );
+ ty.eval(env.as_nzenv())
+ }
+ ExprKind::Pi(_, annot, body) => {
+ let ks = match annot.get_type()?.as_const() {
+ Some(k) => k,
+ _ => {
+ return mkerr(
+ ErrorBuilder::new(format!(
+ "Invalid input type: `{}`",
+ annot.get_type()?.to_expr_tyenv(env),
+ ))
+ .span_err(
+ &annot.span(),
+ format!(
+ "this has type: `{}`",
+ annot.get_type()?.to_expr_tyenv(env)
+ ),
+ )
+ .help(
+ format!(
+ "The input type of a function must have type `Type`, `Kind` or `Sort`",
+ ),
+ )
+ .format(),
+ );
+ }
+ };
+ let kt = match body.get_type()?.as_const() {
+ Some(k) => k,
+ _ => return mkerr("Invalid output type"),
+ };
+
+ Value::from_const(function_check(ks, kt))
+ }
+ ExprKind::Let(_, _, _, body) => body.get_type()?,
+
ExprKind::Const(Const::Type) => Value::from_const(Const::Kind),
ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort),
ExprKind::Builtin(b) => {
@@ -202,10 +232,12 @@ fn type_one_layer(
ValueKind::UnionType(kts) => match kts.get(x) {
// Constructor has type T -> < x: T, ... >
Some(Some(ty)) => {
- let pi_ty = type_of_function(
- ty.get_type()?,
- scrut.get_type()?,
- )?;
+ // Can't fail because uniontypes must have type Const(_).
+ let kt = scrut.get_type()?.as_const().unwrap();
+ // The type of the field must be Const smaller than `kt`, thus the
+ // function type has type `kt`.
+ let pi_ty = Value::from_const(kt);
+
Value::from_kind_and_type(
ValueKind::PiClosure {
binder: Binder::new(x.clone()),
@@ -256,25 +288,27 @@ fn type_one_layer(
ExprKind::App(f, arg) => match f.get_type()?.kind() {
ValueKind::PiClosure { annot, closure, .. } => {
if arg.get_type()? != *annot {
- let mut builder = ErrorBuilder::span_err(
- &span,
- format!("function annot mismatch",),
- );
- builder.annotate_info(
- &f.span(),
- format!(
- "this expects an argument of type: {}",
- annot.to_expr_tyenv(env),
- ),
+ return mkerr(
+ ErrorBuilder::new_span_err(
+ &span,
+ format!("Wrong type of function argument"),
+ )
+ .span_help(
+ &f.span(),
+ format!(
+ "this expects an argument of type: {}",
+ annot.to_expr_tyenv(env),
+ ),
+ )
+ .span_help(
+ &arg.span(),
+ format!(
+ "but this has type: {}",
+ arg.get_type()?.to_expr_tyenv(env),
+ ),
+ )
+ .format(),
);
- builder.annotate_info(
- &arg.span(),
- format!(
- "but this has type: {}",
- arg.get_type()?.to_expr_tyenv(env),
- ),
- );
- return mkerr(builder.format());
}
let arg_nf = arg.eval(env.as_nzenv());
@@ -534,62 +568,15 @@ pub(crate) fn type_with(
) -> Result<TyExpr, TypeError> {
let (tyekind, ty) = match expr.as_ref() {
ExprKind::Var(var) => match env.lookup(&var) {
- Some((k, ty)) => (k, Some(ty)),
- None => return mkerr("unbound variable"),
+ Some((v, ty)) => (TyExprKind::Var(v), Some(ty)),
+ None => {
+ return mkerr(
+ ErrorBuilder::new(format!("unbound variable `{}`", var))
+ .span_err(&expr.span(), "not found in this scope")
+ .format(),
+ )
+ }
},
- ExprKind::Lam(binder, annot, body) => {
- let annot = type_with(env, annot)?;
- let annot_nf = annot.eval(env.as_nzenv());
- let body_env = env.insert_type(&binder, annot_nf.clone());
- let body = type_with(&body_env, body)?;
- let body_ty = body.get_type()?;
- let ty = TyExpr::new(
- TyExprKind::Expr(ExprKind::Pi(
- binder.clone(),
- annot.clone(),
- body_ty.to_tyexpr(body_env.as_varenv()),
- )),
- Some(type_of_function(annot.get_type()?, body_ty.get_type()?)?),
- Span::Artificial,
- );
- let ty = ty.eval(env.as_nzenv());
- (
- TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)),
- Some(ty),
- )
- }
- ExprKind::Pi(binder, annot, body) => {
- let annot = type_with(env, annot)?;
- let annot_nf = annot.eval(env.as_nzenv());
- let body =
- type_with(&env.insert_type(binder, annot_nf.clone()), body)?;
- let ty = type_of_function(annot.get_type()?, body.get_type()?)?;
- (
- TyExprKind::Expr(ExprKind::Pi(binder.clone(), annot, body)),
- Some(ty),
- )
- }
- ExprKind::Let(binder, annot, val, body) => {
- let val = if let Some(t) = annot {
- t.rewrap(ExprKind::Annot(val.clone(), t.clone()))
- } else {
- val.clone()
- };
-
- let val = type_with(env, &val)?;
- let val_nf = val.eval(&env.as_nzenv());
- let body = type_with(&env.insert_value(&binder, val_nf), body)?;
- let body_ty = body.get_type().ok();
- (
- TyExprKind::Expr(ExprKind::Let(
- binder.clone(),
- None,
- val,
- body,
- )),
- body_ty,
- )
- }
ExprKind::Const(Const::Sort) => {
(TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
}
@@ -597,7 +584,36 @@ pub(crate) fn type_with(
return Ok(p.clone().into_value().to_tyexpr_noenv())
}
ekind => {
- let ekind = ekind.traverse_ref(|e| type_with(env, e))?;
+ let ekind = match ekind {
+ ExprKind::Lam(binder, annot, body) => {
+ let annot = type_with(env, annot)?;
+ let annot_nf = annot.eval(env.as_nzenv());
+ let body_env = env.insert_type(binder, annot_nf);
+ let body = type_with(&body_env, body)?;
+ ExprKind::Lam(binder.clone(), annot, body)
+ }
+ ExprKind::Pi(binder, annot, body) => {
+ let annot = type_with(env, annot)?;
+ let annot_nf = annot.eval(env.as_nzenv());
+ let body_env = env.insert_type(binder, annot_nf);
+ let body = type_with(&body_env, body)?;
+ ExprKind::Pi(binder.clone(), annot, body)
+ }
+ ExprKind::Let(binder, annot, val, body) => {
+ let val = if let Some(t) = annot {
+ t.rewrap(ExprKind::Annot(val.clone(), t.clone()))
+ } else {
+ val.clone()
+ };
+ let val = type_with(env, &val)?;
+ let val_nf = val.eval(&env.as_nzenv());
+ let body_env = env.insert_value(&binder, val_nf);
+ let body = type_with(&body_env, body)?;
+ ExprKind::Let(binder.clone(), None, val, body)
+ }
+ _ => ekind.traverse_ref(|e| type_with(env, e))?,
+ };
+
let ty = type_one_layer(env, &ekind, expr.span())?;
(TyExprKind::Expr(ekind), Some(ty))
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 06:27:23 +0000