summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
authorNadrieril2020-01-25 10:15:17 +0000
committerNadrieril2020-01-25 10:15:17 +0000
commit70e6e3a06c05cfe7d8ca3d6f072e7182639c147f (patch)
tree91c8bcfe35b3e99a5332458531a45b58ecfb8be7 /dhall/src/semantics/tck
parentb72f0968ac19058b9cc513ab0ed1785133232a3d (diff)
Typecheck more cases
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r--dhall/src/semantics/tck/typecheck.rs187
1 files changed, 134 insertions, 53 deletions
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index aab5f83..046c999 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -10,6 +10,9 @@ use crate::error::{TypeError, TypeMessage};
use crate::semantics::core::context::TyCtx;
use crate::semantics::nze::{NameEnv, QuoteEnv};
use crate::semantics::phase::normalize::{merge_maps, NzEnv};
+use crate::semantics::phase::typecheck::{
+ builtin_to_value, const_to_value, type_of_builtin,
+};
use crate::semantics::phase::Normalized;
use crate::semantics::{
AlphaVar, Binder, Closure, TyExpr, TyExprKind, Type, Value, ValueKind,
@@ -55,93 +58,171 @@ impl TyEnv {
items: self.items.insert_value(e),
}
}
- pub fn lookup_var(&self, var: &V<Label>) -> Option<(TyExprKind, Value)> {
+ pub fn lookup(&self, var: &V<Label>) -> Option<(TyExprKind, Value)> {
let var = self.names.unlabel_var(var)?;
- let ty = self.lookup_val(&var).get_type().unwrap();
+ let ty = self.items.lookup_val(&var).get_type().unwrap();
Some((TyExprKind::Var(var), ty))
}
- pub fn lookup_val(&self, var: &AlphaVar) -> Value {
- self.items.lookup_val(var)
- }
pub fn size(&self) -> usize {
self.names.size()
}
}
+fn mkerr<T>(x: impl ToString) -> Result<T, TypeError> {
+ Err(TypeError::new(TypeMessage::Custom(x.to_string())))
+}
+
+fn type_last_layer(
+ env: &TyEnv,
+ kind: &ExprKind<TyExpr, Normalized>,
+) -> Result<Value, TypeError> {
+ Ok(match &kind {
+ ExprKind::Import(..) => unreachable!(
+ "There should remain no imports in a resolved expression"
+ ),
+ ExprKind::Var(..)
+ | ExprKind::Lam(..)
+ | ExprKind::Pi(..)
+ | ExprKind::Let(..)
+ | ExprKind::Const(Const::Sort)
+ | ExprKind::Embed(..) => unreachable!(),
+
+ ExprKind::Const(Const::Type) => const_to_value(Const::Kind),
+ ExprKind::Const(Const::Kind) => const_to_value(Const::Sort),
+ ExprKind::Builtin(b) => {
+ type_with(env, &type_of_builtin(*b))?.normalize_whnf(env.as_nzenv())
+ }
+ ExprKind::BoolLit(_) => builtin_to_value(Builtin::Bool),
+ ExprKind::NaturalLit(_) => builtin_to_value(Builtin::Natural),
+ ExprKind::IntegerLit(_) => builtin_to_value(Builtin::Integer),
+ ExprKind::DoubleLit(_) => builtin_to_value(Builtin::Double),
+
+ ExprKind::Annot(x, t) => {
+ if x.get_type()? != t.normalize_whnf(env.as_nzenv()) {
+ return mkerr("annot mismatch");
+ }
+ x.normalize_whnf(env.as_nzenv())
+ }
+ ExprKind::App(f, arg) => {
+ let tf = f.get_type()?;
+ let tf_borrow = tf.as_whnf();
+ let (expected_arg_ty, ty_closure) = match &*tf_borrow {
+ ValueKind::PiClosure { annot, closure, .. } => (annot, closure),
+ _ => return mkerr(format!("apply to not Pi: {:?}", tf_borrow)),
+ };
+ // if arg.get_type()? != *expected_arg_ty {
+ // return mkerr(format!(
+ // "function annot mismatch: {:?}, {:?}",
+ // arg.get_type()?,
+ // expected_arg_ty
+ // ));
+ // }
+
+ let arg_nf = arg.normalize_whnf(env.as_nzenv());
+ ty_closure.apply(arg_nf)
+ }
+ ExprKind::BoolIf(x, y, z) => {
+ if *x.get_type()?.as_whnf()
+ != ValueKind::from_builtin(Builtin::Bool)
+ {
+ return mkerr("InvalidPredicate");
+ }
+ if y.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+ return mkerr("IfBranchMustBeTerm");
+ }
+ if z.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+ return mkerr("IfBranchMustBeTerm");
+ }
+ if y.get_type()? != z.get_type()? {
+ return mkerr("IfBranchMismatch");
+ }
+
+ y.get_type()?
+ }
+
+ _ => Value::from_const(Const::Type), // TODO
+ })
+}
+
/// Type-check an expression and return the expression alongside its type if type-checking
/// succeeded, or an error if type-checking failed.
-fn type_with(env: &TyEnv, expr: Expr<Normalized>) -> Result<TyExpr, TypeError> {
- let mkerr = || TypeError::new(TypeMessage::Sort);
-
- match expr.as_ref() {
- ExprKind::Var(var) => match env.lookup_var(&var) {
- Some((e, ty)) => Ok(TyExpr::new(e, Some(ty), expr.span())),
- None => Err(mkerr()),
+fn type_with(
+ env: &TyEnv,
+ expr: &Expr<Normalized>,
+) -> 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"),
},
ExprKind::Lam(binder, annot, body) => {
- let annot = type_with(env, annot.clone())?;
+ let annot = type_with(env, annot)?;
let annot_nf = annot.normalize_whnf(env.as_nzenv());
- let body = type_with(
- &env.insert_type(&binder, annot_nf.clone()),
- body.clone(),
- )?;
+ let body =
+ type_with(&env.insert_type(&binder, annot_nf.clone()), body)?;
let ty = Value::from_kind_and_type(
ValueKind::PiClosure {
binder: Binder::new(binder.clone()),
annot: annot_nf,
closure: Closure::new(
env.as_nzenv(),
- body.get_type()?.to_tyexpr(env.as_quoteenv()),
+ body.get_type()?.to_tyexpr(env.as_quoteenv().insert()),
),
},
Value::from_const(Const::Type), // TODO: function_check
);
- Ok(TyExpr::new(
+ (
TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)),
Some(ty),
- expr.span(),
- ))
+ )
}
ExprKind::Pi(binder, annot, body) => {
- let annot = type_with(env, annot.clone())?;
+ let annot = type_with(env, annot)?;
let annot_nf = annot.normalize_whnf(env.as_nzenv());
- let body = type_with(
- &env.insert_type(binder, annot_nf.clone()),
- body.clone(),
- )?;
- Ok(TyExpr::new(
+ let body =
+ type_with(&env.insert_type(binder, annot_nf.clone()), body)?;
+ (
TyExprKind::Expr(ExprKind::Pi(binder.clone(), annot, body)),
- None, // TODO: function_check
- expr.span(),
- ))
+ Some(Value::from_const(Const::Type)), // TODO: function_check
+ )
}
- kind => {
- let kind = kind.traverse_ref(|e| type_with(env, e.clone()))?;
- let ty = match &kind {
- ExprKind::App(f, arg) => {
- let tf = f.get_type()?;
- let tf_borrow = tf.as_whnf();
- let (_expected_arg_ty, ty_closure) = match &*tf_borrow {
- ValueKind::PiClosure { annot, closure, .. } => {
- (annot, closure)
- }
- _ => return Err(mkerr()),
- };
- // if arg.get_type()? != *expected_arg_ty {
- // return Err(mkerr());
- // }
-
- let arg_nf = arg.normalize_whnf(env.as_nzenv());
- ty_closure.apply(arg_nf)
- }
- _ => Value::from_const(Const::Type), // TODO
+ ExprKind::Let(binder, annot, val, body) => {
+ let v = if let Some(t) = annot {
+ t.rewrap(ExprKind::Annot(val.clone(), t.clone()))
+ } else {
+ val.clone()
};
- Ok(TyExpr::new(TyExprKind::Expr(kind), Some(ty), expr.span()))
+ let val = type_with(env, val)?;
+ let val_nf = val.normalize_whnf(&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)
+ }
+ ExprKind::Embed(p) => {
+ return Ok(p.clone().into_typed().into_value().to_tyexpr_noenv())
+ }
+ ekind => {
+ let ekind = ekind.traverse_ref(|e| type_with(env, e))?;
+ let ty = type_last_layer(env, &ekind)?;
+ (TyExprKind::Expr(ekind), Some(ty))
+ }
+ };
+
+ Ok(TyExpr::new(tyekind, ty, expr.span()))
}
-pub(crate) fn typecheck(e: Expr<Normalized>) -> Result<TyExpr, TypeError> {
+pub(crate) fn typecheck(e: &Expr<Normalized>) -> Result<TyExpr, TypeError> {
type_with(&TyEnv::new(), e)
}