diff options
| -rw-r--r-- | dhall/src/semantics/core/context.rs | 5 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 1 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 147 | ||||
| -rw-r--r-- | dhall/src/tests.rs | 25 |
4 files changed, 166 insertions, 12 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index 0e62fef..9749c50 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -2,8 +2,8 @@ use crate::error::TypeError; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{AlphaVar, Binder}; -use crate::semantics::nze::{NzVar, QuoteEnv}; -use crate::semantics::phase::normalize::{NzEnv, NzEnvItem}; +use crate::semantics::nze::NzVar; +// use crate::semantics::phase::normalize::{NzEnv, NzEnvItem}; use crate::syntax::{Label, V}; #[derive(Debug, Clone)] @@ -71,7 +71,6 @@ impl TyCtx { t.clone(), ), CtxItem::Replaced(v) => v.clone() - // .to_tyexpr(QuoteEnv::construct(var_idx)) // .normalize_whnf(&NzEnv::construct( // self.ctx // .iter() diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 3ddfb84..e848601 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,3 +1,4 @@ +#![allow(dead_code)] use std::collections::HashMap; use std::convert::TryInto; diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs new file mode 100644 index 0000000..aab5f83 --- /dev/null +++ b/dhall/src/semantics/tck/typecheck.rs @@ -0,0 +1,147 @@ +#![allow(dead_code)] +#![allow(unused_variables)] +#![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, QuoteEnv}; +use crate::semantics::phase::normalize::{merge_maps, NzEnv}; +use crate::semantics::phase::Normalized; +use crate::semantics::{ + AlphaVar, Binder, Closure, TyExpr, TyExprKind, Type, Value, ValueKind, +}; +use crate::syntax; +use crate::syntax::{ + Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span, + UnspannedExpr, V, +}; + +#[derive(Debug, Clone)] +pub(crate) struct TyEnv { + names: NameEnv, + items: NzEnv, +} + +impl TyEnv { + pub fn new() -> Self { + TyEnv { + names: NameEnv::new(), + items: NzEnv::new(), + } + } + pub fn as_quoteenv(&self) -> QuoteEnv { + self.names.as_quoteenv() + } + pub fn as_nzenv(&self) -> &NzEnv { + &self.items + } + pub fn as_nameenv(&self) -> &NameEnv { + &self.names + } + + pub fn insert_type(&self, x: &Label, t: Value) -> Self { + TyEnv { + names: self.names.insert(x), + items: self.items.insert_type(t), + } + } + pub fn insert_value(&self, x: &Label, e: Value) -> Self { + TyEnv { + names: self.names.insert(x), + items: self.items.insert_value(e), + } + } + pub fn lookup_var(&self, var: &V<Label>) -> Option<(TyExprKind, Value)> { + let var = self.names.unlabel_var(var)?; + let ty = self.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() + } +} + +/// 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()), + }, + ExprKind::Lam(binder, annot, body) => { + let annot = type_with(env, annot.clone())?; + let annot_nf = annot.normalize_whnf(env.as_nzenv()); + let body = type_with( + &env.insert_type(&binder, annot_nf.clone()), + body.clone(), + )?; + 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()), + ), + }, + 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_nf = annot.normalize_whnf(env.as_nzenv()); + let body = type_with( + &env.insert_type(binder, annot_nf.clone()), + body.clone(), + )?; + Ok(TyExpr::new( + TyExprKind::Expr(ExprKind::Pi(binder.clone(), annot, body)), + None, // TODO: function_check + expr.span(), + )) + } + 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 + }; + + Ok(TyExpr::new(TyExprKind::Expr(kind), Some(ty), expr.span())) + } + } +} + +pub(crate) fn typecheck(e: Expr<Normalized>) -> Result<TyExpr, TypeError> { + type_with(&TyEnv::new(), e) +} diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 4928c51..994a134 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -211,20 +211,27 @@ pub fn run_test(test: Test<'_>) -> Result<()> { // .typecheck()? // .normalize() // .to_expr(); - let expr = parse_file_str(&expr_file_path)? - .resolve()? - .typecheck()? - .to_value() - .to_tyexpr_noenv() + // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + // let expr = crate::semantics::nze::nzexpr::typecheck(expr)? + // .normalize() + // .to_expr(); + // let expr = parse_file_str(&expr_file_path)? + // .resolve()? + // .typecheck()? + // .to_value() + // .to_tyexpr_noenv() + // .normalize_whnf_noenv() + // .to_expr(crate::semantics::phase::ToExprOptions { + // alpha: false, + // normalize: true, + // }); + let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + let expr = crate::semantics::tck::typecheck::typecheck(expr)? .normalize_whnf_noenv() .to_expr(crate::semantics::phase::ToExprOptions { alpha: false, normalize: true, }); - // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - // let expr = crate::semantics::nze::nzexpr::typecheck(expr)? - // .normalize() - // .to_expr(); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(expr, expected); |