From 5a835d9db35bf76858e178e1bd66e60128879629 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 Jan 2020 18:45:09 +0000 Subject: Fix a bunch of bugs and more tck --- dhall/src/semantics/core/var.rs | 8 ++++- dhall/src/semantics/nze/nzexpr.rs | 24 +++++++++---- dhall/src/semantics/phase/mod.rs | 5 +++ dhall/src/semantics/phase/normalize.rs | 5 ++- dhall/src/semantics/phase/resolve.rs | 8 +++-- dhall/src/semantics/phase/typecheck.rs | 26 ++++++++------ dhall/src/semantics/tck/tyexpr.rs | 10 ++++++ dhall/src/semantics/tck/typecheck.rs | 64 +++++++++++++++++++--------------- dhall/src/tests.rs | 11 +++--- 9 files changed, 104 insertions(+), 57 deletions(-) (limited to 'dhall') 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 { + 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 { + 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) -> 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 { + // 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(b: Builtin) -> Expr { 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); -- cgit v1.2.3