From 9e9b556ee2212540ba43d85249df8c763aa6da2b Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 Jan 2020 21:32:48 +0000 Subject: Postpone fixing Foo/build builtins --- dhall/build.rs | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'dhall/build.rs') diff --git a/dhall/build.rs b/dhall/build.rs index c95a26d..ed8d98b 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -276,6 +276,13 @@ fn generate_tests() -> std::io::Result<()> { // TODO: record completion || path == "simple/completion" || path == "unit/Completion" + // TODO: fix variables in Foo/build + || path == "unit/ListBuildFoldFusion" + || path == "unit/ListBuildImplementation" + || path == "unit/NaturalBuildFoldFusion" + || path == "unit/NaturalBuildImplementation" + || path == "unit/OptionalBuildFoldFusion" + || path == "unit/OptionalBuildImplementation" }), input_type: FileType::Text, output_type: Some(FileType::Text), -- cgit v1.3.1 From 084e81956e99bc759012be7c171f4095c2e59d22 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 Jan 2020 19:34:11 +0000 Subject: Thread env through nztion to fix Foo/build closures --- dhall/build.rs | 7 ---- dhall/src/semantics/core/value.rs | 21 +++++++--- dhall/src/semantics/core/visitor.rs | 9 +++-- dhall/src/semantics/nze/nzexpr.rs | 5 +++ dhall/src/semantics/phase/normalize.rs | 70 ++++++++++++++++++++++------------ dhall/src/semantics/phase/typecheck.rs | 20 ++++++---- dhall/src/semantics/tck/typecheck.rs | 14 +++++-- 7 files changed, 95 insertions(+), 51 deletions(-) (limited to 'dhall/build.rs') diff --git a/dhall/build.rs b/dhall/build.rs index ed8d98b..c95a26d 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -276,13 +276,6 @@ fn generate_tests() -> std::io::Result<()> { // TODO: record completion || path == "simple/completion" || path == "unit/Completion" - // TODO: fix variables in Foo/build - || path == "unit/ListBuildFoldFusion" - || path == "unit/ListBuildImplementation" - || path == "unit/NaturalBuildFoldFusion" - || path == "unit/NaturalBuildImplementation" - || path == "unit/OptionalBuildFoldFusion" - || path == "unit/OptionalBuildImplementation" }), input_type: FileType::Text, output_type: Some(FileType::Text), diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 42da653..71c5c65 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -6,7 +6,9 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::var::{AlphaVar, Binder}; use crate::semantics::nze::{NzVar, QuoteEnv}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf, NzEnv}; -use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; +use crate::semantics::phase::typecheck::{ + builtin_to_value, builtin_to_value_env, const_to_value, +}; use crate::semantics::phase::{ Normalized, NormalizedExpr, ToExprOptions, Typed, }; @@ -77,7 +79,8 @@ pub(crate) enum ValueKind { }, // Invariant: in whnf, the evaluation must not be able to progress further. // Keep types around to be able to recover the types of partial applications. - AppliedBuiltin(Builtin, Vec, Vec), + // Keep env around to construct Foo/build closures; hopefully temporary. + AppliedBuiltin(Builtin, Vec, Vec, NzEnv), Var(AlphaVar, NzVar), Const(Const), @@ -144,7 +147,10 @@ impl Value { const_to_value(c) } pub(crate) fn from_builtin(b: Builtin) -> Self { - builtin_to_value(b) + Self::from_builtin_env(b, &NzEnv::new()) + } + pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self { + builtin_to_value_env(b, env) } pub(crate) fn with_span(self, span: Span) -> Self { self.as_internal_mut().span = span; @@ -318,7 +324,7 @@ impl Value { .apply_var(NzVar::new(qenv.size())) .to_tyexpr(qenv.insert()), )), - ValueKind::AppliedBuiltin(b, args, types) => { + ValueKind::AppliedBuiltin(b, args, types, _) => { TyExprKind::Expr(args.into_iter().zip(types.into_iter()).fold( ExprKind::Builtin(*b), |acc, (v, ty)| { @@ -561,7 +567,7 @@ impl ValueKind { | ValueKind::PiClosure { annot, .. } => { annot.normalize_mut(); } - ValueKind::AppliedBuiltin(_, args, _) => { + ValueKind::AppliedBuiltin(_, args, _, _) => { for x in args.iter_mut() { x.normalize_mut(); } @@ -609,7 +615,10 @@ impl ValueKind { } pub(crate) fn from_builtin(b: Builtin) -> ValueKind { - ValueKind::AppliedBuiltin(b, vec![], vec![]) + ValueKind::from_builtin_env(b, NzEnv::new()) + } + pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind { + ValueKind::AppliedBuiltin(b, vec![], vec![], env) } fn shift(&self, delta: isize, var: &AlphaVar) -> Option { diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs index 64250b0..61a7d0b 100644 --- a/dhall/src/semantics/core/visitor.rs +++ b/dhall/src/semantics/core/visitor.rs @@ -98,9 +98,12 @@ where annot: v.visit_val(annot)?, closure: closure.clone(), }, - AppliedBuiltin(b, xs, types) => { - AppliedBuiltin(*b, v.visit_vec(xs)?, v.visit_vec(types)?) - } + AppliedBuiltin(b, xs, types, env) => AppliedBuiltin( + *b, + v.visit_vec(xs)?, + v.visit_vec(types)?, + env.clone(), + ), Var(v, w) => Var(v.clone(), *w), Const(k) => Const(*k), BoolLit(b) => BoolLit(*b), diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs index 6559082..92ba8fd 100644 --- a/dhall/src/semantics/nze/nzexpr.rs +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -141,6 +141,11 @@ impl NameEnv { pub fn new() -> Self { NameEnv { names: Vec::new() } } + pub fn from_binders(names: impl Iterator) -> Self { + NameEnv { + names: names.collect(), + } + } pub fn as_quoteenv(&self) -> QuoteEnv { QuoteEnv { size: self.names.len(), diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 5fc72fc..a11cb75 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -4,9 +4,11 @@ use std::convert::TryInto; use crate::semantics::nze::{NzVar, QuoteEnv}; use crate::semantics::phase::typecheck::{ - builtin_to_value, const_to_value, rc, typecheck, + builtin_to_value_env, const_to_value, rc, }; use crate::semantics::phase::Normalized; +use crate::semantics::tck::typecheck::type_with; +use crate::semantics::tck::typecheck::TyEnv; use crate::semantics::{ AlphaVar, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind, }; @@ -73,6 +75,7 @@ pub(crate) fn apply_builtin( args: Vec, ty: &Value, types: Vec, + env: NzEnv, ) -> ValueKind { use syntax::Builtin::*; use ValueKind::*; @@ -86,6 +89,11 @@ pub(crate) fn apply_builtin( ValueWithRemainingArgs(&'a [Value], Value), DoneAsIs, } + let make_closure = |e| { + type_with(&env.to_alpha_tyenv(), &e) + .unwrap() + .normalize_whnf(&env) + }; let ret = match (b, args.as_slice()) { (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())), @@ -272,13 +280,12 @@ pub(crate) fn apply_builtin( Ret::Value( f.app(list_t.clone()) .app( - typecheck(make_closure!( + make_closure(make_closure!( λ(T : Type) -> λ(a : var(T)) -> λ(as : List var(T)) -> [ var(a) ] # var(as) )) - .unwrap() .app(t.clone()), ) .app(EmptyListLit(t.clone()).into_value_with_type(list_t)), @@ -300,12 +307,11 @@ pub(crate) fn apply_builtin( Ret::Value( f.app(optional_t.clone()) .app( - typecheck(make_closure!( + make_closure(make_closure!( λ(T : Type) -> λ(a : var(T)) -> Some(var(a)) )) - .unwrap() .app(t.clone()), ) .app( @@ -326,13 +332,10 @@ pub(crate) fn apply_builtin( }, (NaturalBuild, [f]) => Ret::Value( f.app(Value::from_builtin(Natural)) - .app( - typecheck(make_closure!( - λ(x : Natural) -> - 1 + var(x) - )) - .unwrap(), - ) + .app(make_closure(make_closure!( + λ(x : Natural) -> + 1 + var(x) + ))) .app( NaturalLit(0) .into_value_with_type(Value::from_builtin(Natural)), @@ -366,7 +369,7 @@ pub(crate) fn apply_builtin( } v.to_whnf_check_type(ty) } - Ret::DoneAsIs => AppliedBuiltin(b, args, types), + Ret::DoneAsIs => AppliedBuiltin(b, args, types, env), } } @@ -379,7 +382,7 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { ValueKind::LamClosure { closure, .. } => { closure.apply(a).to_whnf_check_type(ty) } - ValueKind::AppliedBuiltin(b, args, types) => { + ValueKind::AppliedBuiltin(b, args, types, env) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); let types = types @@ -387,7 +390,7 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { .cloned() .chain(once(f.get_type().unwrap())) .collect(); - apply_builtin(*b, args, ty, types) + apply_builtin(*b, args, ty, types, env.clone()) } ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( l.clone(), @@ -625,6 +628,7 @@ fn apply_binop<'a>( pub(crate) fn normalize_one_layer( expr: ExprKind, ty: &Value, + env: &NzEnv, ) -> ValueKind { use ValueKind::{ BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit, @@ -649,7 +653,7 @@ pub(crate) fn normalize_one_layer( } ExprKind::Annot(x, _) => Ret::Value(x), ExprKind::Const(c) => Ret::Value(const_to_value(c)), - ExprKind::Builtin(b) => Ret::Value(builtin_to_value(b)), + ExprKind::Builtin(b) => Ret::Value(builtin_to_value_env(b, env)), ExprKind::Assert(_) => Ret::Expr(expr), ExprKind::App(v, a) => Ret::Value(v.app(a)), ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)), @@ -659,11 +663,12 @@ pub(crate) fn normalize_one_layer( ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { let arg = match &*t.as_whnf() { - ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _) - if args.len() == 1 => - { - args[0].clone() - } + ValueKind::AppliedBuiltin( + syntax::Builtin::List, + args, + _, + _, + ) if args.len() == 1 => args[0].clone(), _ => panic!("internal type error"), }; Ret::ValueKind(ValueKind::EmptyListLit(arg)) @@ -827,10 +832,10 @@ pub(crate) fn normalize_whnf( ty: &Value, ) -> ValueKind { match v { - ValueKind::AppliedBuiltin(b, args, types) => { - apply_builtin(b, args, ty, types) + ValueKind::AppliedBuiltin(b, args, types, env) => { + apply_builtin(b, args, ty, types, env) } - ValueKind::PartialExpr(e) => normalize_one_layer(e, ty), + ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()), ValueKind::TextLit(elts) => { ValueKind::TextLit(squash_textlit(elts.into_iter())) } @@ -862,6 +867,9 @@ impl NzEnv { pub fn as_quoteenv(&self) -> QuoteEnv { QuoteEnv::construct(self.items.len()) } + pub fn to_alpha_tyenv(&self) -> TyEnv { + TyEnv::from_nzenv_alpha(self) + } pub fn insert_type(&self, t: Value) -> Self { let mut env = self.clone(); @@ -890,6 +898,10 @@ impl NzEnv { NzEnvItem::Replaced(x) => x.clone(), } } + + pub fn size(&self) -> usize { + self.items.len() + } } /// Normalize a TyExpr into WHNF @@ -924,10 +936,18 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { } TyExprKind::Expr(e) => { let e = e.map_ref(|tye| tye.normalize_whnf(env)); - normalize_one_layer(e, &ty) + normalize_one_layer(e, &ty, env) } }; // dbg!(tye.kind(), env, &kind); Value::from_kind_and_type_whnf(kind, ty) } + +/// Ignore NzEnv when comparing +impl std::cmp::PartialEq for NzEnv { + fn eq(&self, _other: &Self) -> bool { + true + } +} +impl std::cmp::Eq for NzEnv {} diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 18e70e4..f559323 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -5,6 +5,7 @@ use std::collections::HashMap; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TyCtx; use crate::semantics::phase::normalize::merge_maps; +use crate::semantics::phase::normalize::NzEnv; use crate::semantics::phase::Normalized; use crate::semantics::{AlphaVar, Binder, Value, ValueKind}; use crate::syntax; @@ -278,8 +279,11 @@ pub(crate) fn type_of_builtin(b: Builtin) -> Expr { } pub(crate) fn builtin_to_value(b: Builtin) -> Value { + builtin_to_value_env(b, &NzEnv::new()) +} +pub(crate) fn builtin_to_value_env(b: Builtin, env: &NzEnv) -> Value { Value::from_kind_and_type( - ValueKind::from_builtin(b), + ValueKind::from_builtin_env(b, env.clone()), crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b)) .unwrap() .normalize_whnf_noenv(), @@ -433,11 +437,12 @@ fn type_last_layer( } ExprKind::EmptyListLit(t) => { let arg = match &*t.as_whnf() { - ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _) - if args.len() == 1 => - { - args[0].clone() - } + ValueKind::AppliedBuiltin( + syntax::Builtin::List, + args, + _, + _, + ) if args.len() == 1 => args[0].clone(), _ => return mkerr("InvalidListType"), }; RetWhole(Value::from_kind_and_type( @@ -596,7 +601,7 @@ fn type_last_layer( } ExprKind::BinOp(ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { - ValueKind::AppliedBuiltin(List, _, _) => {} + ValueKind::AppliedBuiltin(List, _, _, _) => {} _ => return mkerr("BinOpTypeMismatch"), } @@ -666,6 +671,7 @@ fn type_last_layer( syntax::Builtin::Optional, args, _, + _, ) if args.len() == 1 => { let ty = &args[0]; let mut kts = HashMap::new(); diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 4ca5d4d..e2619b5 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -35,6 +35,14 @@ impl TyEnv { items: NzEnv::new(), } } + pub fn from_nzenv_alpha(items: &NzEnv) -> Self { + TyEnv { + names: NameEnv::from_binders( + std::iter::repeat("_".into()).take(items.size()), + ), + items: items.clone(), + } + } pub fn as_quoteenv(&self) -> QuoteEnv { self.names.as_quoteenv() } @@ -147,7 +155,7 @@ fn type_one_layer( ExprKind::EmptyListLit(t) => { let t = t.normalize_whnf(env.as_nzenv()); match &*t.as_whnf() { - ValueKind::AppliedBuiltin(Builtin::List, args, _) + ValueKind::AppliedBuiltin(Builtin::List, args, _, _) if args.len() == 1 => {} _ => return mkerr("InvalidListType"), }; @@ -404,7 +412,7 @@ fn type_one_layer( ExprKind::BinOp(BinOp::ListAppend, l, r) => { let l_ty = l.get_type()?; match &*l_ty.as_whnf() { - ValueKind::AppliedBuiltin(Builtin::List, _, _) => {} + ValueKind::AppliedBuiltin(Builtin::List, _, _, _) => {} _ => return mkerr("BinOpTypeMismatch"), } @@ -572,7 +580,7 @@ fn type_one_layer( /// 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( +pub(crate) fn type_with( env: &TyEnv, expr: &Expr, ) -> Result { -- 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 'dhall/build.rs') 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 From 0a60a4a891cd8c527ecc3caf6502bd614118d59a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 17:11:16 +0000 Subject: Move parser files to syntax/ --- dhall/build.rs | 4 +- dhall/src/dhall.abnf | 1 - dhall/src/dhall.pest.visibility | 189 ---------------------------- dhall/src/syntax/text/dhall.abnf | 1 + dhall/src/syntax/text/dhall.pest.visibility | 189 ++++++++++++++++++++++++++++ 5 files changed, 192 insertions(+), 192 deletions(-) delete mode 120000 dhall/src/dhall.abnf delete mode 100644 dhall/src/dhall.pest.visibility create mode 120000 dhall/src/syntax/text/dhall.abnf create mode 100644 dhall/src/syntax/text/dhall.pest.visibility (limited to 'dhall/build.rs') diff --git a/dhall/build.rs b/dhall/build.rs index cc94f5e..8992f22 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -387,8 +387,8 @@ fn generate_tests() -> std::io::Result<()> { fn convert_abnf_to_pest() -> std::io::Result<()> { let out_dir = env::var("OUT_DIR").unwrap(); - let abnf_path = "src/dhall.abnf"; - let visibility_path = "src/dhall.pest.visibility"; + let abnf_path = "src/syntax/text/dhall.abnf"; + let visibility_path = "src/syntax/text/dhall.pest.visibility"; let grammar_path = Path::new(&out_dir).join("dhall.pest"); println!("cargo:rerun-if-changed={}", abnf_path); println!("cargo:rerun-if-changed={}", visibility_path); diff --git a/dhall/src/dhall.abnf b/dhall/src/dhall.abnf deleted file mode 120000 index ce13b8e..0000000 --- a/dhall/src/dhall.abnf +++ /dev/null @@ -1 +0,0 @@ -../../dhall-lang/standard/dhall.abnf \ No newline at end of file diff --git a/dhall/src/dhall.pest.visibility b/dhall/src/dhall.pest.visibility deleted file mode 100644 index 03a000b..0000000 --- a/dhall/src/dhall.pest.visibility +++ /dev/null @@ -1,189 +0,0 @@ -# end_of_line -# valid_non_ascii -# tab -# block_comment -# block_comment_char -# block_comment_continue -# not_end_of_line -# line_comment -# whitespace_chunk -# whsp -# whsp1 -# ALPHA -# DIGIT -# ALPHANUM -# HEXDIG -# simple_label_first_char -# simple_label_next_char -simple_label -# quoted_label_char -quoted_label -# label -# nonreserved_label -# any_label -any_label_or_some -double_quote_chunk -double_quote_escaped -# unicode_escape -# unicode_suffix -# unbraced_escape -# braced_codepoint -# braced_escape -double_quote_char -double_quote_literal -single_quote_continue -escaped_quote_pair -escaped_interpolation -single_quote_char -single_quote_literal -# interpolation -# text_literal -if_ -# then -# else_ -# let_ -# in_ -# as_ -# using -merge -missing -# Infinity -NaN -Some_ -toMap -assert -# keyword -builtin -# Optional -Text -# List -Location -# Bool -# True -# False -# None_ -# Natural -# Integer -# Double -# Type -# Kind -# Sort -# Natural_fold -# Natural_build -# Natural_isZero -# Natural_even -# Natural_odd -# Natural_toInteger -# Natural_show -# Integer_toDouble -# Integer_show -# Natural_subtract -# Double_show -# List_build -# List_fold -# List_length -# List_head -# List_last -# List_indexed -# List_reverse -# Optional_fold -# Optional_build -# Text_show -combine -combine_types -equivalent -prefer -lambda -forall -arrow -# complete -# exponent -numeric_double_literal -minus_infinity_literal -plus_infinity_literal -# double_literal -natural_literal -integer_literal -identifier -variable -# path_character -# quoted_path_character -unquoted_path_component -quoted_path_component -# path_component -path -local -parent_path -here_path -home_path -absolute_path -scheme -http_raw -authority -# userinfo -# host -# port -# IP_literal -# IPvFuture -# IPv6address -# h16 -# ls32 -# IPv4address -# dec_octet -# domain -# domainlabel -# pchar -query -# pct_encoded -# unreserved -# sub_delims -http -env -bash_environment_variable -posix_environment_variable -posix_environment_variable_character -# import_type -hash -import_hashed -import -expression -# annotated_expression -let_binding -empty_list_literal -operator_expression -import_alt_expression -or_expression -plus_expression -text_append_expression -list_append_expression -and_expression -combine_expression -prefer_expression -combine_types_expression -times_expression -equal_expression -not_equal_expression -equivalent_expression -application_expression -first_application_expression -# import_expression -completion_expression -selector_expression -selector -labels -# type_selector -primitive_expression -# record_type_or_literal -empty_record_literal -empty_record_type -non_empty_record_type_or_literal -non_empty_record_type -record_type_entry -non_empty_record_literal -record_literal_entry -union_type -empty_union_type -# non_empty_union_type -union_type_entry -non_empty_list_literal -# complete_expression diff --git a/dhall/src/syntax/text/dhall.abnf b/dhall/src/syntax/text/dhall.abnf new file mode 120000 index 0000000..4a95034 --- /dev/null +++ b/dhall/src/syntax/text/dhall.abnf @@ -0,0 +1 @@ +../../../../dhall-lang/standard/dhall.abnf \ No newline at end of file diff --git a/dhall/src/syntax/text/dhall.pest.visibility b/dhall/src/syntax/text/dhall.pest.visibility new file mode 100644 index 0000000..03a000b --- /dev/null +++ b/dhall/src/syntax/text/dhall.pest.visibility @@ -0,0 +1,189 @@ +# end_of_line +# valid_non_ascii +# tab +# block_comment +# block_comment_char +# block_comment_continue +# not_end_of_line +# line_comment +# whitespace_chunk +# whsp +# whsp1 +# ALPHA +# DIGIT +# ALPHANUM +# HEXDIG +# simple_label_first_char +# simple_label_next_char +simple_label +# quoted_label_char +quoted_label +# label +# nonreserved_label +# any_label +any_label_or_some +double_quote_chunk +double_quote_escaped +# unicode_escape +# unicode_suffix +# unbraced_escape +# braced_codepoint +# braced_escape +double_quote_char +double_quote_literal +single_quote_continue +escaped_quote_pair +escaped_interpolation +single_quote_char +single_quote_literal +# interpolation +# text_literal +if_ +# then +# else_ +# let_ +# in_ +# as_ +# using +merge +missing +# Infinity +NaN +Some_ +toMap +assert +# keyword +builtin +# Optional +Text +# List +Location +# Bool +# True +# False +# None_ +# Natural +# Integer +# Double +# Type +# Kind +# Sort +# Natural_fold +# Natural_build +# Natural_isZero +# Natural_even +# Natural_odd +# Natural_toInteger +# Natural_show +# Integer_toDouble +# Integer_show +# Natural_subtract +# Double_show +# List_build +# List_fold +# List_length +# List_head +# List_last +# List_indexed +# List_reverse +# Optional_fold +# Optional_build +# Text_show +combine +combine_types +equivalent +prefer +lambda +forall +arrow +# complete +# exponent +numeric_double_literal +minus_infinity_literal +plus_infinity_literal +# double_literal +natural_literal +integer_literal +identifier +variable +# path_character +# quoted_path_character +unquoted_path_component +quoted_path_component +# path_component +path +local +parent_path +here_path +home_path +absolute_path +scheme +http_raw +authority +# userinfo +# host +# port +# IP_literal +# IPvFuture +# IPv6address +# h16 +# ls32 +# IPv4address +# dec_octet +# domain +# domainlabel +# pchar +query +# pct_encoded +# unreserved +# sub_delims +http +env +bash_environment_variable +posix_environment_variable +posix_environment_variable_character +# import_type +hash +import_hashed +import +expression +# annotated_expression +let_binding +empty_list_literal +operator_expression +import_alt_expression +or_expression +plus_expression +text_append_expression +list_append_expression +and_expression +combine_expression +prefer_expression +combine_types_expression +times_expression +equal_expression +not_equal_expression +equivalent_expression +application_expression +first_application_expression +# import_expression +completion_expression +selector_expression +selector +labels +# type_selector +primitive_expression +# record_type_or_literal +empty_record_literal +empty_record_type +non_empty_record_type_or_literal +non_empty_record_type +record_type_entry +non_empty_record_literal +record_literal_entry +union_type +empty_union_type +# non_empty_union_type +union_type_entry +non_empty_list_literal +# complete_expression -- cgit v1.3.1