summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/semantics/core/var.rs8
-rw-r--r--dhall/src/semantics/nze/nzexpr.rs24
-rw-r--r--dhall/src/semantics/phase/mod.rs5
-rw-r--r--dhall/src/semantics/phase/normalize.rs5
-rw-r--r--dhall/src/semantics/phase/resolve.rs8
-rw-r--r--dhall/src/semantics/phase/typecheck.rs26
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs10
-rw-r--r--dhall/src/semantics/tck/typecheck.rs64
-rw-r--r--dhall/src/tests.rs11
9 files changed, 104 insertions, 57 deletions
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index 0d2c1d4..cf45d5e 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -1,10 +1,16 @@
use crate::syntax::{Label, V};
/// Stores an alpha-normalized variable.
-#[derive(Clone, Copy, PartialEq, Eq)]
+#[derive(Clone, Copy, Eq)]
pub struct AlphaVar {
alpha: V<()>,
}
+// TODO: temporary hopefully
+impl std::cmp::PartialEq for AlphaVar {
+ fn eq(&self, _other: &Self) -> bool {
+ true
+ }
+}
// Exactly like a Label, but equality returns always true.
// This is so that ValueKind equality is exactly alpha-equivalence.
diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs
index 49aa704..33fdde3 100644
--- a/dhall/src/semantics/nze/nzexpr.rs
+++ b/dhall/src/semantics/nze/nzexpr.rs
@@ -82,16 +82,16 @@ pub(crate) struct QuoteEnv {
}
// Reverse-debruijn index: counts number of binders from the bottom of the stack.
-#[derive(Debug, Clone, Copy, Eq)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub(crate) struct NzVar {
idx: usize,
}
// TODO: temporary hopefully
-impl std::cmp::PartialEq for NzVar {
- fn eq(&self, _other: &Self) -> bool {
- true
- }
-}
+// impl std::cmp::PartialEq for NzVar {
+// fn eq(&self, _other: &Self) -> bool {
+// true
+// }
+// }
impl TyEnv {
pub fn new() -> Self {
@@ -144,6 +144,9 @@ impl NameEnv {
size: self.names.len(),
}
}
+ pub fn names(&self) -> &[Binder] {
+ &self.names
+ }
pub fn insert(&self, x: &Binder) -> Self {
let mut env = self.clone();
@@ -220,13 +223,20 @@ impl QuoteEnv {
pub fn construct(size: usize) -> Self {
QuoteEnv { size }
}
+ pub fn size(&self) -> usize {
+ self.size
+ }
pub fn insert(&self) -> Self {
QuoteEnv {
size: self.size + 1,
}
}
pub fn lookup(&self, var: &NzVar) -> AlphaVar {
- AlphaVar::new(V((), self.size - var.idx - 1))
+ self.lookup_fallible(var).unwrap()
+ }
+ pub fn lookup_fallible(&self, var: &NzVar) -> Option<AlphaVar> {
+ let idx = self.size.checked_sub(var.idx + 1)?;
+ Some(AlphaVar::new(V((), idx)))
}
}
diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs
index 4dc91e7..67cdc91 100644
--- a/dhall/src/semantics/phase/mod.rs
+++ b/dhall/src/semantics/phase/mod.rs
@@ -89,6 +89,11 @@ impl Resolved {
pub fn to_expr(&self) -> ResolvedExpr {
self.0.clone()
}
+ pub fn tck_and_normalize_new_flow(&self) -> Result<Normalized, TypeError> {
+ let val = crate::semantics::tck::typecheck::typecheck(&self.0)?
+ .normalize_whnf_noenv();
+ Ok(Normalized(Typed(val)))
+ }
}
impl Typed {
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 33e1f2b..5fc72fc 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -2,7 +2,7 @@
use std::collections::HashMap;
use std::convert::TryInto;
-use crate::semantics::nze::NzVar;
+use crate::semantics::nze::{NzVar, QuoteEnv};
use crate::semantics::phase::typecheck::{
builtin_to_value, const_to_value, rc, typecheck,
};
@@ -859,6 +859,9 @@ impl NzEnv {
pub fn construct(items: Vec<NzEnvItem>) -> Self {
NzEnv { items }
}
+ pub fn as_quoteenv(&self) -> QuoteEnv {
+ QuoteEnv::construct(self.items.len())
+ }
pub fn insert_type(&self, t: Value) -> Self {
let mut env = self.clone();
diff --git a/dhall/src/semantics/phase/resolve.rs b/dhall/src/semantics/phase/resolve.rs
index cc4a024..64106aa 100644
--- a/dhall/src/semantics/phase/resolve.rs
+++ b/dhall/src/semantics/phase/resolve.rs
@@ -52,10 +52,14 @@ fn load_import(
import_cache: &mut ImportCache,
import_stack: &ImportStack,
) -> Result<Normalized, Error> {
+ // Ok(
+ // do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)?
+ // .typecheck()?
+ // .normalize(),
+ // )
Ok(
do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)?
- .typecheck()?
- .normalize(),
+ .tck_and_normalize_new_flow()?,
)
}
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 1aab736..18e70e4 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -280,7 +280,9 @@ pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
pub(crate) fn builtin_to_value(b: Builtin) -> Value {
Value::from_kind_and_type(
ValueKind::from_builtin(b),
- typecheck(type_of_builtin(b)).unwrap(),
+ crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b))
+ .unwrap()
+ .normalize_whnf_noenv(),
)
}
@@ -380,17 +382,21 @@ fn type_last_layer(
ExprKind::App(f, a) => {
let tf = f.get_type()?;
let tf_borrow = tf.as_whnf();
- let (tx, tb) = match &*tf_borrow {
- ValueKind::Pi(_, tx, tb) => (tx, tb),
+ match &*tf_borrow {
+ ValueKind::Pi(_, tx, tb) => {
+ if &a.get_type()? != tx {
+ return mkerr("TypeMismatch");
+ }
+
+ let ret = tb.subst_shift(&AlphaVar::default(), a);
+ ret.normalize_nf();
+ RetTypeOnly(ret)
+ }
+ ValueKind::PiClosure { closure, .. } => {
+ RetTypeOnly(closure.apply(a.clone()))
+ }
_ => return mkerr("NotAFunction"),
- };
- if &a.get_type()? != tx {
- return mkerr("TypeMismatch");
}
-
- let ret = tb.subst_shift(&AlphaVar::default(), a);
- ret.normalize_nf();
- RetTypeOnly(ret)
}
ExprKind::Annot(x, t) => {
if &x.get_type()? != t {
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index c8be3a3..a42265d 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -5,6 +5,7 @@ use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv};
use crate::semantics::phase::typecheck::rc;
use crate::semantics::phase::Normalized;
use crate::semantics::phase::{NormalizedExpr, ToExprOptions};
+use crate::semantics::tck::typecheck::TyEnv;
use crate::semantics::Value;
use crate::syntax::{ExprKind, Label, Span, V};
@@ -48,6 +49,15 @@ impl TyExpr {
pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
tyexpr_to_expr(self, opts, &mut Vec::new())
}
+ pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
+ let opts = ToExprOptions {
+ normalize: true,
+ alpha: false,
+ };
+ let env = env.as_nameenv().names();
+ let mut env = env.iter().collect();
+ tyexpr_to_expr(self, opts, &mut env)
+ }
// TODO: temporary hack
pub fn to_value(&self) -> Value {
todo!()
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 1b64d28..4ca5d4d 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -275,10 +275,22 @@ fn type_one_layer(
}
ExprKind::Annot(x, t) => {
let t = t.normalize_whnf(env.as_nzenv());
- if x.get_type()? != t {
- return mkerr("annot mismatch");
+ let x_ty = x.get_type()?;
+ if x_ty != t {
+ return mkerr(format!(
+ "annot mismatch: ({} : {}) : {}",
+ x.to_expr_tyenv(env),
+ x_ty.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env),
+ t.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env)
+ ));
+ // return mkerr(format!(
+ // "annot mismatch: {} != {}",
+ // x_ty.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env),
+ // t.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env)
+ // ));
+ // return mkerr(format!("annot mismatch: {:#?} : {:#?}", x, t,));
}
- t
+ x_ty
}
ExprKind::App(f, arg) => {
let tf = f.get_type()?;
@@ -389,35 +401,29 @@ fn type_one_layer(
let yk = y.get_type()?.as_const().unwrap();
Value::from_const(max(xk, yk))
}
- // ExprKind::BinOp(o @ BinOp::ListAppend, l, r) => {
- // match &*l.get_type()?.as_whnf() {
- // ValueKind::AppliedBuiltin(List, _, _) => {}
- // _ => return mkerr("BinOpTypeMismatch"),
- // }
-
- // if l.get_type()? != r.get_type()? {
- // return mkerr("BinOpTypeMismatch");
- // }
+ ExprKind::BinOp(BinOp::ListAppend, l, r) => {
+ let l_ty = l.get_type()?;
+ match &*l_ty.as_whnf() {
+ ValueKind::AppliedBuiltin(Builtin::List, _, _) => {}
+ _ => return mkerr("BinOpTypeMismatch"),
+ }
- // l.get_type()?
- // }
- // ExprKind::BinOp(BinOp::Equivalence, l, r) => {
- // if l.get_type()?.get_type()?.as_const() != Some(Const::Type) {
- // return mkerr("EquivalenceArgumentMustBeTerm");
- // }
- // if r.get_type()?.get_type()?.as_const() != Some(Const::Type) {
- // return mkerr("EquivalenceArgumentMustBeTerm");
- // }
+ if l_ty != r.get_type()? {
+ return mkerr("BinOpTypeMismatch");
+ }
- // if l.get_type()? != r.get_type()? {
- // return mkerr("EquivalenceTypeMismatch");
- // }
+ l_ty
+ }
+ ExprKind::BinOp(BinOp::Equivalence, l, r) => {
+ if l.get_type()? != r.get_type()? {
+ return mkerr("EquivalenceTypeMismatch");
+ }
+ if l.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+ return mkerr("EquivalenceArgumentsMustBeTerms");
+ }
- // RetWhole(Value::from_kind_and_type(
- // ValueKind::Equivalence(l.clone(), r.clone()),
- // Value::from_const(Type),
- // ))
- // }
+ Value::from_const(Const::Type)
+ }
ExprKind::BinOp(o, l, r) => {
let t = builtin_to_value(match o {
BinOp::BoolAnd
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index f51f6a8..88c09cc 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -232,13 +232,10 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
// 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()?
+ .tck_and_normalize_new_flow()?
+ .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-24 02:05:44 +0000