From 763a810358f15a8bac6973ac4b273f517729cc84 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 17 Jan 2020 10:06:22 +0000 Subject: Oops, this endeavour is doomed --- tests_buffer | 1 + 1 file changed, 1 insertion(+) (limited to 'tests_buffer') diff --git a/tests_buffer b/tests_buffer index 1c4cde5..225fc98 100644 --- a/tests_buffer +++ b/tests_buffer @@ -36,6 +36,7 @@ variables across import boundaries TextLitNested3 "${"${""}"}${x}" regression/ NaturalFoldExtraArg Natural/fold 0 (Bool -> Bool) (λ(_ : (Bool -> Bool)) → λ(_ : Bool) → True) (λ(_ : Bool) → False) True + let T = Natural let ap = λ(f : T → List T) -> λ(x : T) -> f x in ap (λ(x : T) -> ap (λ(y : T) -> [x, y]) 1) 0 typecheck: something that involves destructuring a recordtype after merge -- cgit v1.3.1 From 8ced62a2cdde95c4d67298289756c12f53656df0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 Jan 2020 18:41:20 +0000 Subject: Fix all sorts of variable shenanigans --- dhall/src/semantics/core/value.rs | 118 ++++---------------------------------- dhall/src/semantics/nze/nzexpr.rs | 34 ++++++++--- dhall/src/semantics/tck/tyexpr.rs | 15 ++++- dhall/src/tests.rs | 18 ++++++ tests_buffer | 1 + 5 files changed, 69 insertions(+), 117 deletions(-) (limited to 'tests_buffer') diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 35913cf..42da653 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -303,7 +303,9 @@ impl Value { } => TyExprKind::Expr(ExprKind::Lam( binder.to_label(), annot.to_tyexpr(qenv), - closure.normalize().to_tyexpr(qenv.insert()), + closure + .apply_var(NzVar::new(qenv.size())) + .to_tyexpr(qenv.insert()), )), ValueKind::PiClosure { binder, @@ -312,7 +314,9 @@ impl Value { } => TyExprKind::Expr(ExprKind::Pi( binder.to_label(), annot.to_tyexpr(qenv), - closure.normalize().to_tyexpr(qenv.insert()), + closure + .apply_var(NzVar::new(qenv.size())) + .to_tyexpr(qenv.insert()), )), ValueKind::AppliedBuiltin(b, args, types) => { TyExprKind::Expr(args.into_iter().zip(types.into_iter()).fold( @@ -692,119 +696,16 @@ impl Closure { pub fn apply(&self, val: Value) -> Value { self.body.normalize_whnf(&self.env.insert_value(val)) } - pub fn apply_fresh(&self, env: QuoteEnv) -> Value { + pub fn apply_var(&self, var: NzVar) -> Value { let val = Value::from_kind_and_type( - ValueKind::Var(AlphaVar::default(), NzVar::new(env.size())), + ValueKind::Var(AlphaVar::default(), var), self.arg_ty.clone(), ); self.apply(val) } - pub fn normalize(&self) -> Value { - self.body - .normalize_whnf(&self.env.insert_type(self.arg_ty.clone())) - } } /// Compare two values for equality modulo alpha/beta-equivalence. -// TODO: use Rc comparison to shortcut on identical pointers -fn equiv(val1: &Value, val2: &Value) -> bool { - struct ValueWithEnv<'v> { - val: &'v Value, - env: QuoteEnv, - } - impl<'v> PartialEq for ValueWithEnv<'v> { - fn eq(&self, other: &ValueWithEnv<'v>) -> bool { - equiv_with_env(self.env, self.val, other.env, other.val) - } - } - // Push the given context into every subnode of the ValueKind. That way, normal equality of the - // resulting value will take into account the context. - fn push_context<'v>( - env: QuoteEnv, - kind: &'v ValueKind, - ) -> ValueKind> { - kind.map_ref_with_special_handling_of_binders( - |val| ValueWithEnv { val, env }, - |_, _, val| ValueWithEnv { - val, - env: env.insert(), - }, - ) - } - - fn equiv_with_env<'v>( - env1: QuoteEnv, - val1: &'v Value, - env2: QuoteEnv, - val2: &'v Value, - ) -> bool { - use ValueKind::Var; - let kind1 = val1.as_whnf(); - let kind2 = val2.as_whnf(); - match (&*kind1, &*kind2) { - (Var(_, v1), Var(_, v2)) => { - v1 == v2 - // match (env1.lookup(v1), env2.lookup(v2)) { - // // Both vars were found in the environment, check they point to the same - // // binder. - // // Does that even make any sense with an incomplete environment ? - // // I have no clue what I'm doing anymore. - // (Some(i), Some(j)) => i == j, - // // Both vars point to outside the environment ???? - // // (None, None) => v1 == v2, - // _ => false, - // } - } - // (Var(_, v1), Var(_, v2)) => env1.lookup(v1) == env2.lookup(v2), - ( - ValueKind::LamClosure { - annot: a1, - closure: cl1, - .. - }, - ValueKind::LamClosure { - annot: a2, - closure: cl2, - .. - }, - ) => { - equiv_with_env(env1, a1, env2, a2) - && equiv_with_env( - env1.insert(), - &cl1.apply_fresh(env1), - env2.insert(), - &cl2.apply_fresh(env2), - ) - } - ( - ValueKind::PiClosure { - annot: a1, - closure: cl1, - .. - }, - ValueKind::PiClosure { - annot: a2, - closure: cl2, - .. - }, - ) => { - equiv_with_env(env1, a1, env2, a2) - && equiv_with_env( - env1.insert(), - &cl1.apply_fresh(env1), - env2.insert(), - &cl2.apply_fresh(env2), - ) - } - (k1, k2) => push_context(env1, k1) == push_context(env2, k2), - } - } - - // TODO: need to use ambiant env instead of creating new one - // Might be possible to generate free variables differently to avoid this - equiv_with_env(QuoteEnv::new(), val1, QuoteEnv::new(), val2) -} - // TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { @@ -815,7 +716,8 @@ impl std::cmp::Eq for Value {} impl std::cmp::PartialEq for Closure { fn eq(&self, other: &Self) -> bool { - self.normalize() == other.normalize() + let v = NzVar::fresh(); + self.apply_var(v) == other.apply_var(v) } } impl std::cmp::Eq for Closure {} diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs index 33fdde3..6559082 100644 --- a/dhall/src/semantics/nze/nzexpr.rs +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -81,10 +81,12 @@ pub(crate) struct QuoteEnv { size: usize, } -// Reverse-debruijn index: counts number of binders from the bottom of the stack. #[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub(crate) struct NzVar { - idx: usize, +pub(crate) enum NzVar { + /// Reverse-debruijn index: counts number of binders from the bottom of the stack. + Bound(usize), + /// Fake fresh variable generated for expression equality checking. + Fresh(usize), } // TODO: temporary hopefully // impl std::cmp::PartialEq for NzVar { @@ -207,7 +209,9 @@ impl NzEnv { let idx = self.items.len() - 1 - var.idx(); match &self.items[idx] { NzEnvItem::Kept(ty) => NzExpr::new( - NzExprKind::Var { var: NzVar { idx } }, + NzExprKind::Var { + var: NzVar::new(idx), + }, Some(ty.clone()), ), NzEnvItem::Replaced(x) => x.clone(), @@ -235,18 +239,32 @@ impl QuoteEnv { self.lookup_fallible(var).unwrap() } pub fn lookup_fallible(&self, var: &NzVar) -> Option { - let idx = self.size.checked_sub(var.idx + 1)?; + let idx = self.size.checked_sub(var.idx() + 1)?; Some(AlphaVar::new(V((), idx))) } } impl NzVar { pub fn new(idx: usize) -> Self { - NzVar { idx } + NzVar::Bound(idx) + } + pub fn fresh() -> Self { + use std::sync::atomic::{AtomicUsize, Ordering}; + // Global counter to ensure uniqueness of the generated id. + static FRESH_VAR_COUNTER: AtomicUsize = AtomicUsize::new(0); + let id = FRESH_VAR_COUNTER.fetch_add(1, Ordering::SeqCst); + NzVar::Fresh(id) } pub fn shift(&self, delta: isize) -> Self { - NzVar { - idx: (self.idx as isize + delta) as usize, + NzVar::new((self.idx() as isize + delta) as usize) + } + // Panics on a fresh variable. + pub fn idx(&self) -> usize { + match self { + NzVar::Bound(i) => *i, + NzVar::Fresh(_) => panic!( + "Trying to use a fresh variable outside of equality checking" + ), } } } diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index a42265d..9e8dc47 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -12,7 +12,7 @@ use crate::syntax::{ExprKind, Label, Span, V}; pub(crate) type Type = Value; // An expression with inferred types at every node and resolved variables. -#[derive(Debug, Clone)] +#[derive(Clone)] pub(crate) struct TyExpr { kind: Box, ty: Option, @@ -114,3 +114,16 @@ fn tyexpr_to_expr<'a>( } }) } + +impl std::fmt::Debug for TyExpr { + fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let mut x = fmt.debug_struct("TyExpr"); + x.field("kind", self.kind()); + if let Some(ty) = self.ty.as_ref() { + x.field("type", &ty); + } else { + x.field("type", &None::<()>); + } + x.finish() + } +} diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 88c09cc..971c48d 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -164,6 +164,7 @@ pub fn run_test(test: Test<'_>) -> Result<()> { // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); // let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?; // let ty = tyexpr.get_type()?.to_expr(); + // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); let ty = crate::semantics::tck::typecheck::typecheck(&expr)? .get_type()? @@ -173,6 +174,23 @@ pub fn run_test(test: Test<'_>) -> Result<()> { }); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(ty, expected); + // + // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + // let ty = crate::semantics::tck::typecheck::typecheck(&expr)? + // .get_type()?; + // let expected = parse_file_str(&expected_file_path)?.to_expr(); + // let expected = crate::semantics::tck::typecheck::typecheck(&expected)? + // .normalize_whnf_noenv(); + // // if ty != expected { + // // assert_eq_display!(ty.to_expr(crate::semantics::phase::ToExprOptions { + // // alpha: false, + // // normalize: true, + // // }), expected.to_expr(crate::semantics::phase::ToExprOptions { + // // alpha: false, + // // normalize: true, + // // })) + // // } + // assert_eq_pretty!(ty, expected); } TypeInferenceFailure(file_path) => { let mut res = diff --git a/tests_buffer b/tests_buffer index 225fc98..a872503 100644 --- a/tests_buffer +++ b/tests_buffer @@ -47,6 +47,7 @@ success/ somehow test that ({ x = { z = 1 } } ∧ { x = { y = 2 } }).x has a type somehow test that the recordtype from List/indexed has a type in both empty and nonempty cases somehow test types added to the Foo/build closures + λ(x : ∀(a : Type) → a) → x failure/ merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True) merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y > -- cgit v1.3.1 From 7683b0d762cf0df489ad4bc006e8db2358e81cf4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 Jan 2020 21:50:04 +0000 Subject: Implement assert & merge and fix more bugs --- dhall/src/semantics/core/value.rs | 47 ++++++-- dhall/src/semantics/phase/normalize.rs | 20 +++- dhall/src/semantics/tck/typecheck.rs | 208 +++++++++++++++++++-------------- tests_buffer | 1 + 4 files changed, 172 insertions(+), 104 deletions(-) (limited to 'tests_buffer') diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 71c5c65..3dcbd38 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -56,10 +56,15 @@ pub(crate) enum Form { } #[derive(Debug, Clone)] -pub(crate) struct Closure { - arg_ty: Value, - env: NzEnv, - body: TyExpr, +pub(crate) enum Closure { + /// Normal closure + Closure { + arg_ty: Value, + env: NzEnv, + body: TyExpr, + }, + /// Closure that ignores the argument passed + ConstantClosure { env: NzEnv, body: TyExpr }, } #[derive(Debug, Clone, PartialEq, Eq)] @@ -696,21 +701,41 @@ impl ValueKind { impl Closure { pub fn new(arg_ty: Value, env: &NzEnv, body: TyExpr) -> Self { - Closure { + Closure::Closure { arg_ty, env: env.clone(), body, } } + pub fn new_constant(env: &NzEnv, body: TyExpr) -> Self { + Closure::ConstantClosure { + env: env.clone(), + body, + } + } pub fn apply(&self, val: Value) -> Value { - self.body.normalize_whnf(&self.env.insert_value(val)) + match self { + Closure::Closure { env, body, .. } => { + body.normalize_whnf(&env.insert_value(val)) + } + Closure::ConstantClosure { env, body, .. } => { + body.normalize_whnf(env) + } + } } pub fn apply_var(&self, var: NzVar) -> Value { - let val = Value::from_kind_and_type( - ValueKind::Var(AlphaVar::default(), var), - self.arg_ty.clone(), - ); - self.apply(val) + match self { + Closure::Closure { arg_ty, .. } => { + let val = Value::from_kind_and_type( + ValueKind::Var(AlphaVar::default(), var), + arg_ty.clone(), + ); + self.apply(val) + } + Closure::ConstantClosure { env, body, .. } => { + body.normalize_whnf(env) + } + } } } diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index a11cb75..532dae3 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -855,17 +855,30 @@ pub(crate) enum NzEnvItem { #[derive(Debug, Clone)] pub(crate) struct NzEnv { items: Vec, + vars: QuoteEnv, } impl NzEnv { pub fn new() -> Self { - NzEnv { items: Vec::new() } + NzEnv { + items: Vec::new(), + vars: QuoteEnv::new(), + } } pub fn construct(items: Vec) -> Self { - NzEnv { items } + let vars = QuoteEnv::construct( + items + .iter() + .filter(|i| match i { + NzEnvItem::Kept(_) => true, + NzEnvItem::Replaced(_) => false, + }) + .count(), + ); + NzEnv { items, vars } } pub fn as_quoteenv(&self) -> QuoteEnv { - QuoteEnv::construct(self.items.len()) + self.vars } pub fn to_alpha_tyenv(&self) -> TyEnv { TyEnv::from_nzenv_alpha(self) @@ -874,6 +887,7 @@ impl NzEnv { pub fn insert_type(&self, t: Value) -> Self { let mut env = self.clone(); env.items.push(NzEnvItem::Kept(t)); + env.vars = env.vars.insert(); env } pub fn insert_value(&self, e: Value) -> Self { diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index e2619b5..1b8f261 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -7,7 +7,7 @@ use std::collections::HashMap; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TyCtx; -use crate::semantics::nze::{NameEnv, QuoteEnv}; +use crate::semantics::nze::{NameEnv, NzVar, QuoteEnv}; use crate::semantics::phase::normalize::{merge_maps, NzEnv}; use crate::semantics::phase::typecheck::{ builtin_to_value, const_to_value, type_of_builtin, @@ -44,7 +44,7 @@ impl TyEnv { } } pub fn as_quoteenv(&self) -> QuoteEnv { - self.names.as_quoteenv() + self.items.as_quoteenv() } pub fn as_nzenv(&self) -> &NzEnv { &self.items @@ -262,8 +262,7 @@ fn type_one_layer( ValueKind::PiClosure { binder: Binder::new(x.clone()), annot: ty.clone(), - closure: Closure::new( - ty.clone(), + closure: Closure::new_constant( env.as_nzenv(), scrut.clone(), ), @@ -300,6 +299,15 @@ fn type_one_layer( } x_ty } + ExprKind::Assert(t) => { + let t = t.normalize_whnf(env.as_nzenv()); + match &*t.as_whnf() { + ValueKind::Equivalence(x, y) if x == y => {} + ValueKind::Equivalence(..) => return mkerr("AssertMismatch"), + _ => return mkerr("AssertMustTakeEquivalence"), + } + t + } ExprKind::App(f, arg) => { let tf = f.get_type()?; let tf_borrow = tf.as_whnf(); @@ -458,88 +466,109 @@ fn type_one_layer( t } - // ExprKind::Merge(record, union, type_annot) => { - // let record_type = record.get_type()?; - // let record_borrow = record_type.as_whnf(); - // let handlers = match &*record_borrow { - // ValueKind::RecordType(kts) => kts, - // _ => return mkerr("Merge1ArgMustBeRecord"), - // }; - - // let union_type = union.get_type()?; - // let union_borrow = union_type.as_whnf(); - // let variants = match &*union_borrow { - // ValueKind::UnionType(kts) => Cow::Borrowed(kts), - // ValueKind::AppliedBuiltin( - // syntax::Builtin::Optional, - // args, - // _, - // ) if args.len() == 1 => { - // let ty = &args[0]; - // let mut kts = HashMap::new(); - // kts.insert("None".into(), None); - // kts.insert("Some".into(), Some(ty.clone())); - // Cow::Owned(kts) - // } - // _ => return mkerr("Merge2ArgMustBeUnionOrOptional"), - // }; - - // let mut inferred_type = None; - // for (x, handler_type) in handlers { - // let handler_return_type = - // match variants.get(x) { - // // Union alternative with type - // Some(Some(variant_type)) => { - // let handler_type_borrow = handler_type.as_whnf(); - // let (tx, tb) = match &*handler_type_borrow { - // ValueKind::Pi(_, tx, tb) => (tx, tb), - // _ => return mkerr("NotAFunction"), - // }; - - // if variant_type != tx { - // return mkerr("TypeMismatch"); - // } - - // // Extract `tb` from under the binder. Fails if the variable was used - // // in `tb`. - // match tb.over_binder() { - // Some(x) => x, - // None => return mkerr( - // "MergeHandlerReturnTypeMustNotBeDependent", - // ), - // } - // } - // // Union alternative without type - // Some(None) => handler_type.clone(), - // None => return mkerr("MergeHandlerMissingVariant"), - // }; - // match &inferred_type { - // None => inferred_type = Some(handler_return_type), - // Some(t) => { - // if t != &handler_return_type { - // return mkerr("MergeHandlerTypeMismatch"); - // } - // } - // } - // } - // for x in variants.keys() { - // if !handlers.contains_key(x) { - // return mkerr("MergeVariantMissingHandler"); - // } - // } - - // match (inferred_type, type_annot.as_ref()) { - // (Some(t1), Some(t2)) => { - // if &t1 != t2 { - // return mkerr("MergeAnnotMismatch"); - // } - // RetTypeOnly(t1) - // } - // (Some(t), None) => RetTypeOnly(t), - // (None, Some(t)) => RetTypeOnly(t.clone()), - // (None, None) => return mkerr("MergeEmptyNeedsAnnotation"), - // } - // } + ExprKind::Merge(record, union, type_annot) => { + let record_type = record.get_type()?; + let record_borrow = record_type.as_whnf(); + let handlers = match &*record_borrow { + ValueKind::RecordType(kts) => kts, + _ => return mkerr("Merge1ArgMustBeRecord"), + }; + + let union_type = union.get_type()?; + let union_borrow = union_type.as_whnf(); + let variants = match &*union_borrow { + ValueKind::UnionType(kts) => Cow::Borrowed(kts), + ValueKind::AppliedBuiltin( + syntax::Builtin::Optional, + args, + _, + _, + ) if args.len() == 1 => { + let ty = &args[0]; + let mut kts = HashMap::new(); + kts.insert("None".into(), None); + kts.insert("Some".into(), Some(ty.clone())); + Cow::Owned(kts) + } + _ => return mkerr("Merge2ArgMustBeUnionOrOptional"), + }; + + let mut inferred_type = None; + for (x, handler_type) in handlers { + let handler_return_type = match variants.get(x) { + // Union alternative with type + Some(Some(variant_type)) => { + let handler_type_borrow = handler_type.as_whnf(); + match &*handler_type_borrow { + ValueKind::Pi(_, tx, tb) => { + if variant_type != tx { + return mkerr("MergeHandlerTypeMismatch"); + } + + // Extract `tb` from under the binder. Fails if the variable was used + // in `tb`. + match tb.over_binder() { + Some(x) => x, + None => return mkerr( + "MergeHandlerReturnTypeMustNotBeDependent", + ), + } + } + ValueKind::PiClosure { closure, annot, .. } => { + if variant_type != annot { + // return mkerr("MergeHandlerTypeMismatch"); + return mkerr(format!( + "MergeHandlerTypeMismatch: {:#?} != {:#?}", + variant_type, + annot + )); + } + + let v = NzVar::fresh(); + // TODO: handle case where variable is used in closure + closure.apply_var(v) + } + _ => return mkerr("NotAFunction"), + } + } + // Union alternative without type + Some(None) => handler_type.clone(), + None => return mkerr("MergeHandlerMissingVariant"), + }; + match &inferred_type { + None => inferred_type = Some(handler_return_type), + Some(t) => { + if t != &handler_return_type { + // return mkerr("MergeHandlerTypeMismatch"); + return mkerr(format!( + "MergeHandlerTypeMismatch: {:#?} != {:#?}", + t, handler_return_type, + )); + } + } + } + } + for x in variants.keys() { + if !handlers.contains_key(x) { + return mkerr("MergeVariantMissingHandler"); + } + } + + let type_annot = type_annot + .as_ref() + .map(|t| t.normalize_whnf(env.as_nzenv())); + match (inferred_type, type_annot) { + (Some(t1), Some(t2)) => { + if t1 != t2 { + return mkerr("MergeAnnotMismatch"); + } + t1 + } + (Some(t), None) => t, + (None, Some(t)) => t, + (None, None) => return mkerr("MergeEmptyNeedsAnnotation"), + } + } ExprKind::ToMap(_, _) => unimplemented!("toMap"), ExprKind::Projection(record, labels) => { let record_type = record.get_type()?; @@ -574,7 +603,6 @@ fn type_one_layer( unimplemented!("selection by expression") } ExprKind::Completion(_, _) => unimplemented!("record completion"), - _ => Value::from_const(Const::Type), // TODO }) } @@ -592,14 +620,14 @@ pub(crate) fn type_with( ExprKind::Lam(binder, annot, body) => { let annot = type_with(env, annot)?; let annot_nf = annot.normalize_whnf(env.as_nzenv()); - let body = - type_with(&env.insert_type(&binder, annot_nf.clone()), body)?; + let body_env = env.insert_type(&binder, annot_nf.clone()); + let body = type_with(&body_env, body)?; let body_ty = body.get_type()?; let ty = TyExpr::new( TyExprKind::Expr(ExprKind::Pi( binder.clone(), annot.clone(), - body_ty.to_tyexpr(env.as_quoteenv().insert()), + body_ty.to_tyexpr(body_env.as_quoteenv()), )), Some(type_of_function(annot.get_type()?, body_ty.get_type()?)?), Span::Artificial, diff --git a/tests_buffer b/tests_buffer index a872503..e5e1705 100644 --- a/tests_buffer +++ b/tests_buffer @@ -48,6 +48,7 @@ success/ somehow test that the recordtype from List/indexed has a type in both empty and nonempty cases somehow test types added to the Foo/build closures λ(x : ∀(a : Type) → a) → x + let X = 0 in λ(T : Type) → λ(x : T) → 1 failure/ merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True) merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y > -- cgit v1.3.1 From f31ccaa40df77b1ca8b37db46a819460c831006e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 18:17:12 +0000 Subject: Fix more bugs --- dhall/build.rs | 4 ++ dhall/src/semantics/phase/normalize.rs | 32 ++-------------- dhall/src/semantics/tck/typecheck.rs | 69 ++++++++++++++++++---------------- dhall/src/tests.rs | 18 +++++++-- tests_buffer | 1 + 5 files changed, 59 insertions(+), 65 deletions(-) (limited to 'tests_buffer') diff --git a/dhall/build.rs b/dhall/build.rs index c95a26d..cc94f5e 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -339,6 +339,8 @@ fn generate_tests() -> std::io::Result<()> { || path == "unit/CompletionWithWrongDefaultType" || path == "unit/CompletionWithWrongFieldName" || path == "unit/CompletionWithWrongOverridenType" + // TODO: enable free variable checking + || path == "unit/MergeHandlerFreeVar" }), input_type: FileType::Text, output_type: None, @@ -367,6 +369,8 @@ fn generate_tests() -> std::io::Result<()> { || path == "unit/CompletionWithWrongDefaultType" || path == "unit/CompletionWithWrongFieldName" || path == "unit/CompletionWithWrongOverridenType" + // TODO: enable free variable checking + || path == "unit/MergeHandlerFreeVar" }), input_type: FileType::Text, output_type: None, diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 532dae3..f4e4099 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, QuoteEnv}; +use crate::semantics::nze::NzVar; use crate::semantics::phase::typecheck::{ builtin_to_value_env, const_to_value, rc, }; @@ -855,30 +855,14 @@ pub(crate) enum NzEnvItem { #[derive(Debug, Clone)] pub(crate) struct NzEnv { items: Vec, - vars: QuoteEnv, } impl NzEnv { pub fn new() -> Self { - NzEnv { - items: Vec::new(), - vars: QuoteEnv::new(), - } + NzEnv { items: Vec::new() } } pub fn construct(items: Vec) -> Self { - let vars = QuoteEnv::construct( - items - .iter() - .filter(|i| match i { - NzEnvItem::Kept(_) => true, - NzEnvItem::Replaced(_) => false, - }) - .count(), - ); - NzEnv { items, vars } - } - pub fn as_quoteenv(&self) -> QuoteEnv { - self.vars + NzEnv { items } } pub fn to_alpha_tyenv(&self) -> TyEnv { TyEnv::from_nzenv_alpha(self) @@ -887,7 +871,6 @@ impl NzEnv { pub fn insert_type(&self, t: Value) -> Self { let mut env = self.clone(); env.items.push(NzEnvItem::Kept(t)); - env.vars = env.vars.insert(); env } pub fn insert_value(&self, e: Value) -> Self { @@ -897,16 +880,9 @@ impl NzEnv { } pub fn lookup_val(&self, var: &AlphaVar) -> Value { let idx = self.items.len() - 1 - var.idx(); - let var_idx = self.items[..idx] - .iter() - .filter(|i| match i { - NzEnvItem::Kept(_) => true, - NzEnvItem::Replaced(_) => false, - }) - .count(); match &self.items[idx] { NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf( - ValueKind::Var(var.clone(), NzVar::new(var_idx)), + ValueKind::Var(var.clone(), NzVar::new(idx)), ty.clone(), ), NzEnvItem::Replaced(x) => x.clone(), diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 1b8f261..a83f175 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -44,7 +44,7 @@ impl TyEnv { } } pub fn as_quoteenv(&self) -> QuoteEnv { - self.items.as_quoteenv() + self.names.as_quoteenv() } pub fn as_nzenv(&self) -> &NzEnv { &self.items @@ -70,9 +70,6 @@ impl TyEnv { let ty = self.items.lookup_val(&var).get_type().unwrap(); Some((TyExprKind::Var(var), ty)) } - pub fn size(&self) -> usize { - self.names.size() - } } fn type_of_recordtype<'a>( @@ -312,33 +309,24 @@ fn type_one_layer( let tf = f.get_type()?; let tf_borrow = tf.as_whnf(); match &*tf_borrow { - // ValueKind::PiClosure { annot, closure, .. } => (annot, closure), - ValueKind::PiClosure { - annot: _expected_arg_ty, - closure: ty_closure, - .. - } => { - // if arg.get_type()? != *expected_arg_ty { - // return mkerr(format!( - // "function annot mismatch: {:?}, {:?}", - // arg.get_type()?, - // expected_arg_ty - // )); - // } + ValueKind::PiClosure { annot, closure, .. } => { + if arg.get_type()? != *annot { + // return mkerr(format!("function annot mismatch")); + return mkerr(format!( + "function annot mismatch: ({} : {}) : {}", + arg.to_expr_tyenv(env), + arg.get_type()? + .to_tyexpr(env.as_quoteenv()) + .to_expr_tyenv(env), + annot + .to_tyexpr(env.as_quoteenv()) + .to_expr_tyenv(env), + )); + } let arg_nf = arg.normalize_whnf(env.as_nzenv()); - ty_closure.apply(arg_nf) + closure.apply(arg_nf) } - // ValueKind::Pi(_, _expected_arg_ty, body) => { - // // if arg.get_type()? != *tx { - // // return mkerr("TypeMismatch"); - // // } - - // let arg_nf = arg.normalize_whnf(env.as_nzenv()); - // let ret = body.subst_shift(&AlphaVar::default(), &arg_nf); - // ret.normalize_nf(); - // ret - // } _ => return mkerr(format!("apply to not Pi: {:?}", tf_borrow)), } } @@ -404,14 +392,29 @@ fn type_one_layer( ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { let x_val = x.normalize_whnf(env.as_nzenv()); let y_val = y.normalize_whnf(env.as_nzenv()); - match &*x_val.as_whnf() { - ValueKind::RecordType(_) => {} + let x_val_borrow = x_val.as_whnf(); + let y_val_borrow = y_val.as_whnf(); + let kts_x = match &*x_val_borrow { + ValueKind::RecordType(kts) => kts, _ => return mkerr("RecordTypeMergeRequiresRecordType"), - } - match &*y_val.as_whnf() { - ValueKind::RecordType(_) => {} + }; + let kts_y = match &*y_val_borrow { + ValueKind::RecordType(kts) => kts, _ => return mkerr("RecordTypeMergeRequiresRecordType"), + }; + for (k, tx) in kts_x { + if let Some(ty) = kts_y.get(k) { + type_one_layer( + env, + &ExprKind::BinOp( + BinOp::RecursiveRecordTypeMerge, + tx.to_tyexpr(env.as_quoteenv()), + ty.to_tyexpr(env.as_quoteenv()), + ), + )?; + } } + // A RecordType's type is always a const let xk = x.get_type()?.as_const().unwrap(); let yk = y.get_type()?.as_const().unwrap(); diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 971c48d..1c687f6 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -193,13 +193,23 @@ pub fn run_test(test: Test<'_>) -> Result<()> { // assert_eq_pretty!(ty, expected); } TypeInferenceFailure(file_path) => { - let mut res = - parse_file_str(&file_path)?.skip_resolve()?.typecheck(); + // let mut res = + // parse_file_str(&file_path)?.skip_resolve()?.typecheck(); + // if let Ok(e) = &res { + // // If e did typecheck, check that get_type fails + // res = e.get_type(); + // } + // res.unwrap_err(); + + let res = crate::semantics::tck::typecheck::typecheck( + &parse_file_str(&file_path)?.skip_resolve()?.to_expr(), + ); if let Ok(e) = &res { // If e did typecheck, check that get_type fails - res = e.get_type(); + e.get_type().unwrap_err(); + } else { + res.unwrap_err(); } - res.unwrap_err(); } // Checks the output of the type error against a text file. If the text file doesn't exist, // we instead write to it the output we got. This makes it easy to update those files: just diff --git a/tests_buffer b/tests_buffer index e5e1705..34210a9 100644 --- a/tests_buffer +++ b/tests_buffer @@ -49,6 +49,7 @@ success/ somehow test types added to the Foo/build closures λ(x : ∀(a : Type) → a) → x let X = 0 in λ(T : Type) → λ(x : T) → 1 + (λ(T : Type) → let foo = 0 in λ(x : T) → x) : ∀(T : Type) → ∀(x : T) → T failure/ merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True) merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y > -- cgit v1.3.1