summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
authorNadrieril2020-01-24 21:33:21 +0000
committerNadrieril2020-01-24 21:33:21 +0000
commitb72f0968ac19058b9cc513ab0ed1785133232a3d (patch)
tree07647b0f0e3e0f9583d06b4fb1210e6c702d535f /dhall/src/semantics
parent9e9b556ee2212540ba43d85249df8c763aa6da2b (diff)
Implement basic typecheck with new approach
Diffstat (limited to 'dhall/src/semantics')
-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
3 files changed, 150 insertions, 3 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)
+}