summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/core/context.rs5
-rw-r--r--dhall/src/semantics/phase/normalize.rs1
-rw-r--r--dhall/src/semantics/tck/typecheck.rs147
-rw-r--r--dhall/src/tests.rs25
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);
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 07:45:18 +0000