From 664c925186ecd587f46577715254b74b6264e4fe Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Aug 2019 12:33:52 +0200 Subject: Avoid capture when typechecking union constructor --- dhall/src/phase/typecheck.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 56fb5ed..2030f21 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -564,13 +564,12 @@ fn type_last_layer( Value::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > Some(Some(t)) => { - // TODO: avoid capture Ok(RetTypeOnly( tck_pi_type( ctx, "_".into(), t.to_type(), - r.clone(), + r.under_binder(Label::from("_")), )?.to_type() )) }, -- cgit v1.2.3 From 51bb1d2da8e5874129d4b5cc5d0c60e23eee9f11 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Aug 2019 12:35:34 +0200 Subject: Typecheck before normalizing in tests --- dhall/src/phase/typecheck.rs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 2030f21..7bbad38 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -1002,10 +1002,7 @@ fn type_last_layer( /// will fail. fn type_of(e: SubExpr) -> Result { let ctx = TypecheckContext::new(); - let e = type_with(&ctx, e)?; - // Ensure `e` has a type (i.e. `e` is not `Sort`) - e.get_type()?; - Ok(e) + type_with(&ctx, e) } pub(crate) fn typecheck(e: Resolved) -> Result { -- cgit v1.2.3 From 5f0d69671b44ba1dff6becb9ebc7f6e74241e3e2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Aug 2019 18:14:55 +0200 Subject: Remove dead code --- dhall/src/phase/typecheck.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 7bbad38..dd6da70 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -4,7 +4,7 @@ use dhall_syntax::{ rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, SubExpr, }; -use crate::core::context::{NormalizationContext, TypecheckContext}; +use crate::core::context::TypecheckContext; use crate::core::thunk::{Thunk, TypedThunk}; use crate::core::value::Value; use crate::core::var::{Shift, Subst}; @@ -1009,11 +1009,11 @@ pub(crate) fn typecheck(e: Resolved) -> Result { type_of(e.0) } -pub(crate) fn typecheck_with(e: Resolved, ty: &Type) -> Result { +pub(crate) fn typecheck_with( + e: Resolved, + ty: &Type, +) -> Result { let expr: SubExpr<_> = e.0; let ty: SubExpr<_> = ty.to_expr(); type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty))) } -pub(crate) fn skip_typecheck(e: Resolved) -> Typed { - Typed::from_thunk_untyped(Thunk::new(NormalizationContext::new(), e.0)) -} -- cgit v1.2.3 From e0f5216215ccb7a4df85d80e11dd265cdb52a44f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Aug 2019 19:47:36 +0200 Subject: s/Value/ValueF/ --- dhall/src/phase/typecheck.rs | 110 ++++++++++++++++++++++--------------------- 1 file changed, 56 insertions(+), 54 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index dd6da70..8d7a3bc 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -6,7 +6,7 @@ use dhall_syntax::{ use crate::core::context::TypecheckContext; use crate::core::thunk::{Thunk, TypedThunk}; -use crate::core::value::Value; +use crate::core::value::ValueF; use crate::core::var::{Shift, Subst}; use crate::error::{TypeError, TypeMessage}; use crate::phase::{Normalized, Resolved, Type, Typed}; @@ -43,7 +43,7 @@ fn tck_pi_type( let k = function_check(ka, kb); Ok(Typed::from_thunk_and_type( - Value::Pi( + ValueF::Pi( x.into(), TypedThunk::from_type(tx), TypedThunk::from_type(te), @@ -88,7 +88,7 @@ fn tck_record_type( let k = k.unwrap_or(dhall_syntax::Const::Type); Ok(Typed::from_thunk_and_type( - Value::RecordType(new_kts).into_thunk(), + ValueF::RecordType(new_kts).into_thunk(), Type::from_const(k), )) } @@ -132,7 +132,7 @@ fn tck_union_type( let k = k.unwrap_or(dhall_syntax::Const::Type); Ok(Typed::from_thunk_and_type( - Value::UnionType(new_kts).into_thunk(), + ValueF::UnionType(new_kts).into_thunk(), Type::from_const(k), )) } @@ -335,14 +335,14 @@ fn type_with( let tx = mktype(ctx, t.clone())?; let ctx2 = ctx.insert_type(x, tx.clone()); let b = type_with(&ctx2, b.clone())?; - let v = Value::Lam( + let v = ValueF::Lam( x.clone().into(), TypedThunk::from_type(tx.clone()), b.to_thunk(), ); let tb = b.get_type()?.into_owned(); let t = tck_pi_type(ctx, x.clone(), tx, tb)?.to_type(); - Typed::from_thunk_and_type(Thunk::from_value(v), t) + Typed::from_thunk_and_type(Thunk::from_valuef(v), t) } Pi(x, ta, tb) => { let ta = mktype(ctx, ta.clone())?; @@ -415,8 +415,10 @@ fn type_last_layer( } App(f, a) => { let tf = f.get_type()?; - let (x, tx, tb) = match &tf.to_value() { - Value::Pi(x, tx, tb) => (x.clone(), tx.to_type(), tb.to_type()), + let (x, tx, tb) = match &tf.to_valuef() { + ValueF::Pi(x, tx, tb) => { + (x.clone(), tx.to_type(), tb.to_type()) + } _ => return Err(mkerr(NotAFunction(f.clone()))), }; if a.get_type()?.as_ref() != &tx { @@ -437,9 +439,9 @@ fn type_last_layer( Ok(RetTypeOnly(x.get_type()?.into_owned())) } Assert(t) => { - match t.to_value() { - Value::Equivalence(ref x, ref y) if x == y => {} - Value::Equivalence(x, y) => { + match t.to_valuef() { + ValueF::Equivalence(ref x, ref y) if x == y => {} + ValueF::Equivalence(x, y) => { return Err(mkerr(AssertMismatch( x.to_typed(), y.to_typed(), @@ -470,8 +472,8 @@ fn type_last_layer( } EmptyListLit(t) => { let t = t.to_type(); - match &t.to_value() { - Value::AppliedBuiltin(dhall_syntax::Builtin::List, args) + match &t.to_valuef() { + ValueF::AppliedBuiltin(dhall_syntax::Builtin::List, args) if args.len() == 1 => {} _ => { return Err(TypeError::new( @@ -504,8 +506,8 @@ fn type_last_layer( Ok(RetTypeOnly( Typed::from_thunk_and_type( - Value::from_builtin(dhall_syntax::Builtin::List) - .app(t.to_value()) + ValueF::from_builtin(dhall_syntax::Builtin::List) + .app(t.to_valuef()) .into_thunk(), Typed::from_const(Type), ) @@ -523,8 +525,8 @@ fn type_last_layer( Ok(RetTypeOnly( Typed::from_thunk_and_type( - Value::from_builtin(dhall_syntax::Builtin::Optional) - .app(t.to_value()) + ValueF::from_builtin(dhall_syntax::Builtin::Optional) + .app(t.to_valuef()) .into_thunk(), Typed::from_const(Type).into_type(), ) @@ -549,8 +551,8 @@ fn type_last_layer( .into_type(), )), Field(r, x) => { - match &r.get_type()?.to_value() { - Value::RecordType(kts) => match kts.get(&x) { + match &r.get_type()?.to_valuef() { + ValueF::RecordType(kts) => match kts.get(&x) { Some(tth) => { Ok(RetTypeOnly(tth.to_type())) }, @@ -560,8 +562,8 @@ fn type_last_layer( // TODO: branch here only when r.get_type() is a Const _ => { let r = r.to_type(); - match &r.to_value() { - Value::UnionType(kts) => match kts.get(&x) { + match &r.to_valuef() { + ValueF::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > Some(Some(t)) => { Ok(RetTypeOnly( @@ -631,14 +633,14 @@ fn type_last_layer( } // Extract the LHS record type - let kts_x = match l_type.to_value() { - Value::RecordType(kts) => kts, + let kts_x = match l_type.to_valuef() { + ValueF::RecordType(kts) => kts, _ => return Err(mkerr(MustCombineRecord(l.clone()))), }; // Extract the RHS record type - let kts_y = match r_type.to_value() { - Value::RecordType(kts) => kts, + let kts_y = match r_type.to_valuef() { + ValueF::RecordType(kts) => kts, _ => return Err(mkerr(MustCombineRecord(r.clone()))), }; @@ -672,10 +674,10 @@ fn type_last_layer( inner_l: &TypedThunk, inner_r: &TypedThunk| -> Result { - match (inner_l.to_value(), inner_r.to_value()) { + match (inner_l.to_valuef(), inner_r.to_valuef()) { ( - Value::RecordType(inner_l_kvs), - Value::RecordType(inner_r_kvs), + ValueF::RecordType(inner_l_kvs), + ValueF::RecordType(inner_r_kvs), ) => { combine_record_types(ctx, inner_l_kvs, inner_r_kvs) } @@ -715,14 +717,14 @@ fn type_last_layer( } // Extract the LHS record type - let kts_x = match l_type.to_value() { - Value::RecordType(kts) => kts, + let kts_x = match l_type.to_valuef() { + ValueF::RecordType(kts) => kts, _ => return Err(mkerr(MustCombineRecord(l.clone()))), }; // Extract the RHS record type - let kts_y = match r_type.to_value() { - Value::RecordType(kts) => kts, + let kts_y = match r_type.to_valuef() { + ValueF::RecordType(kts) => kts, _ => return Err(mkerr(MustCombineRecord(r.clone()))), }; @@ -745,10 +747,10 @@ fn type_last_layer( kts_l_inner: &TypedThunk, kts_r_inner: &TypedThunk| -> Result { - match (kts_l_inner.to_value(), kts_r_inner.to_value()) { + match (kts_l_inner.to_valuef(), kts_r_inner.to_valuef()) { ( - Value::RecordType(kvs_l_inner), - Value::RecordType(kvs_r_inner), + ValueF::RecordType(kvs_l_inner), + ValueF::RecordType(kvs_r_inner), ) => { combine_record_types(ctx, kvs_l_inner, kvs_r_inner) } @@ -774,8 +776,8 @@ fn type_last_layer( }; // Extract the Const of the LHS - let k_l = match l.get_type()?.to_value() { - Value::Const(k) => k, + let k_l = match l.get_type()?.to_valuef() { + ValueF::Const(k) => k, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( l.clone(), @@ -784,8 +786,8 @@ fn type_last_layer( }; // Extract the Const of the RHS - let k_r = match r.get_type()?.to_value() { - Value::Const(k) => k, + let k_r = match r.get_type()?.to_valuef() { + ValueF::Const(k) => k, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( r.clone(), @@ -806,8 +808,8 @@ fn type_last_layer( }; // Extract the LHS record type - let kts_x = match l.to_value() { - Value::RecordType(kts) => kts, + let kts_x = match l.to_valuef() { + ValueF::RecordType(kts) => kts, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( l.clone(), @@ -816,8 +818,8 @@ fn type_last_layer( }; // Extract the RHS record type - let kts_y = match r.to_value() { - Value::RecordType(kts) => kts, + let kts_y = match r.to_valuef() { + ValueF::RecordType(kts) => kts, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( r.clone(), @@ -831,8 +833,8 @@ fn type_last_layer( .and(Ok(RetTypeOnly(Typed::from_const(k)))) } BinOp(o @ ListAppend, l, r) => { - match l.get_type()?.to_value() { - Value::AppliedBuiltin(List, _) => {} + match l.get_type()?.to_valuef() { + ValueF::AppliedBuiltin(List, _) => {} _ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone()))), } @@ -893,13 +895,13 @@ fn type_last_layer( Ok(RetTypeOnly(t)) } Merge(record, union, type_annot) => { - let handlers = match record.get_type()?.to_value() { - Value::RecordType(kts) => kts, + let handlers = match record.get_type()?.to_valuef() { + ValueF::RecordType(kts) => kts, _ => return Err(mkerr(Merge1ArgMustBeRecord(record.clone()))), }; - let variants = match union.get_type()?.to_value() { - Value::UnionType(kts) => kts, + let variants = match union.get_type()?.to_valuef() { + ValueF::UnionType(kts) => kts, _ => return Err(mkerr(Merge2ArgMustBeUnion(union.clone()))), }; @@ -910,8 +912,8 @@ fn type_last_layer( Some(Some(variant_type)) => { let variant_type = variant_type.to_type(); let handler_type = handler.to_type(); - let (x, tx, tb) = match &handler_type.to_value() { - Value::Pi(x, tx, tb) => { + let (x, tx, tb) = match &handler_type.to_valuef() { + ValueF::Pi(x, tx, tb) => { (x.clone(), tx.to_type(), tb.to_type()) } _ => return Err(mkerr(NotAFunction(handler_type))), @@ -973,8 +975,8 @@ fn type_last_layer( } Projection(record, labels) => { let trecord = record.get_type()?; - let kts = match trecord.to_value() { - Value::RecordType(kts) => kts, + let kts = match trecord.to_valuef() { + ValueF::RecordType(kts) => kts, _ => return Err(mkerr(ProjectionMustBeRecord)), }; @@ -988,7 +990,7 @@ fn type_last_layer( Ok(RetTypeOnly( Typed::from_thunk_and_type( - Value::RecordType(new_kts).into_thunk(), + ValueF::RecordType(new_kts).into_thunk(), trecord.get_type()?.into_owned(), ) .to_type(), -- cgit v1.2.3 From 6753a1f97bb674d91dd4d42f2ddb25a8119e070d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 17 Aug 2019 19:00:43 +0200 Subject: s/Thunk/Value/ --- dhall/src/phase/typecheck.rs | 68 ++++++++++++++++++++++---------------------- 1 file changed, 34 insertions(+), 34 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 8d7a3bc..4154afe 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -5,8 +5,8 @@ use dhall_syntax::{ }; use crate::core::context::TypecheckContext; -use crate::core::thunk::{Thunk, TypedThunk}; -use crate::core::value::ValueF; +use crate::core::value::{TypedValue, Value}; +use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; use crate::error::{TypeError, TypeMessage}; use crate::phase::{Normalized, Resolved, Type, Typed}; @@ -42,13 +42,13 @@ fn tck_pi_type( let k = function_check(ka, kb); - Ok(Typed::from_thunk_and_type( + Ok(Typed::from_value_and_type( ValueF::Pi( x.into(), - TypedThunk::from_type(tx), - TypedThunk::from_type(te), + TypedValue::from_type(tx), + TypedValue::from_type(te), ) - .into_thunk(), + .into_value(), Type::from_const(k), )) } @@ -80,15 +80,15 @@ fn tck_record_type( return Err(TypeError::new(ctx, RecordTypeDuplicateField)) } Entry::Vacant(_) => { - entry.or_insert_with(|| TypedThunk::from_type(t.clone())) + entry.or_insert_with(|| TypedValue::from_type(t.clone())) } }; } // An empty record type has type Type let k = k.unwrap_or(dhall_syntax::Const::Type); - Ok(Typed::from_thunk_and_type( - ValueF::RecordType(new_kts).into_thunk(), + Ok(Typed::from_value_and_type( + ValueF::RecordType(new_kts).into_value(), Type::from_const(k), )) } @@ -122,7 +122,7 @@ fn tck_union_type( return Err(TypeError::new(ctx, UnionTypeDuplicateField)) } Entry::Vacant(_) => entry.or_insert_with(|| { - t.as_ref().map(|t| TypedThunk::from_type(t.clone())) + t.as_ref().map(|t| TypedValue::from_type(t.clone())) }), }; } @@ -131,8 +131,8 @@ fn tck_union_type( // an union type with only unary variants also has type Type let k = k.unwrap_or(dhall_syntax::Const::Type); - Ok(Typed::from_thunk_and_type( - ValueF::UnionType(new_kts).into_thunk(), + Ok(Typed::from_value_and_type( + ValueF::UnionType(new_kts).into_value(), Type::from_const(k), )) } @@ -337,12 +337,12 @@ fn type_with( let b = type_with(&ctx2, b.clone())?; let v = ValueF::Lam( x.clone().into(), - TypedThunk::from_type(tx.clone()), - b.to_thunk(), + TypedValue::from_type(tx.clone()), + b.to_value(), ); let tb = b.get_type()?.into_owned(); let t = tck_pi_type(ctx, x.clone(), tx, tb)?.to_type(); - Typed::from_thunk_and_type(Thunk::from_valuef(v), t) + Typed::from_value_and_type(Value::from_valuef(v), t) } Pi(x, ta, tb) => { let ta = mktype(ctx, ta.clone())?; @@ -380,9 +380,9 @@ fn type_with( let ret = type_last_layer(ctx, &expr)?; match ret { RetTypeOnly(typ) => { - let expr = expr.map_ref(|typed| typed.to_thunk()); - Typed::from_thunk_and_type( - Thunk::from_partial_expr(expr), + let expr = expr.map_ref(|typed| typed.to_value()); + Typed::from_value_and_type( + Value::from_partial_expr(expr), typ, ) } @@ -505,10 +505,10 @@ fn type_last_layer( } Ok(RetTypeOnly( - Typed::from_thunk_and_type( + Typed::from_value_and_type( ValueF::from_builtin(dhall_syntax::Builtin::List) .app(t.to_valuef()) - .into_thunk(), + .into_value(), Typed::from_const(Type), ) .to_type(), @@ -524,10 +524,10 @@ fn type_last_layer( } Ok(RetTypeOnly( - Typed::from_thunk_and_type( + Typed::from_value_and_type( ValueF::from_builtin(dhall_syntax::Builtin::Optional) .app(t.to_valuef()) - .into_thunk(), + .into_value(), Typed::from_const(Type).into_type(), ) .to_type(), @@ -662,8 +662,8 @@ fn type_last_layer( // records of records when merging. fn combine_record_types( ctx: &TypecheckContext, - kts_l: HashMap, - kts_r: HashMap, + kts_l: HashMap, + kts_r: HashMap, ) -> Result { use crate::phase::normalize::outer_join; @@ -671,8 +671,8 @@ fn type_last_layer( // are records themselves, then we hit the recursive case. // Otherwise we have a field collision. let combine = |k: &Label, - inner_l: &TypedThunk, - inner_r: &TypedThunk| + inner_l: &TypedValue, + inner_r: &TypedValue| -> Result { match (inner_l.to_valuef(), inner_r.to_valuef()) { ( @@ -690,7 +690,7 @@ fn type_last_layer( let kts: HashMap> = outer_join( |l| Ok(l.to_type()), |r| Ok(r.to_type()), - |k: &Label, l: &TypedThunk, r: &TypedThunk| { + |k: &Label, l: &TypedValue, r: &TypedValue| { combine(k, l, r) }, &kts_l, @@ -735,8 +735,8 @@ fn type_last_layer( // records of records when merging. fn combine_record_types( ctx: &TypecheckContext, - kts_l: HashMap, - kts_r: HashMap, + kts_l: HashMap, + kts_r: HashMap, ) -> Result { use crate::phase::normalize::intersection_with_key; @@ -744,8 +744,8 @@ fn type_last_layer( // are records themselves, then we hit the recursive case. // Otherwise we have a field collision. let combine = |k: &Label, - kts_l_inner: &TypedThunk, - kts_r_inner: &TypedThunk| + kts_l_inner: &TypedValue, + kts_r_inner: &TypedValue| -> Result { match (kts_l_inner.to_valuef(), kts_r_inner.to_valuef()) { ( @@ -761,7 +761,7 @@ fn type_last_layer( }; let kts = intersection_with_key( - |k: &Label, l: &TypedThunk, r: &TypedThunk| { + |k: &Label, l: &TypedValue, r: &TypedValue| { combine(k, l, r) }, &kts_l, @@ -989,8 +989,8 @@ fn type_last_layer( } Ok(RetTypeOnly( - Typed::from_thunk_and_type( - ValueF::RecordType(new_kts).into_thunk(), + Typed::from_value_and_type( + ValueF::RecordType(new_kts).into_value(), trecord.get_type()?.into_owned(), ) .to_type(), -- cgit v1.2.3 From 29016b78736dca857e4e7f7c4dc68ed5e30c28bb Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 19 Aug 2019 12:25:09 +0200 Subject: s/to_valuef/to_whnf/ and avoid cloning ValueFs when possible --- dhall/src/phase/typecheck.rs | 198 ++++++++++++++++++++----------------------- 1 file changed, 94 insertions(+), 104 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 4154afe..c303ada 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -22,12 +22,7 @@ fn tck_pi_type( let ka = match tx.get_type()?.as_const() { Some(k) => k, - _ => { - return Err(TypeError::new( - ctx, - InvalidInputType(tx.to_normalized()), - )) - } + _ => return Err(TypeError::new(ctx, InvalidInputType(tx))), }; let kb = match te.get_type()?.as_const() { @@ -35,7 +30,7 @@ fn tck_pi_type( _ => { return Err(TypeError::new( &ctx2, - InvalidOutputType(te.get_type()?.to_normalized()), + InvalidOutputType(te.get_type()?.into_owned()), )) } }; @@ -415,18 +410,14 @@ fn type_last_layer( } App(f, a) => { let tf = f.get_type()?; - let (x, tx, tb) = match &tf.to_valuef() { + let (x, tx, tb) = match &*tf.as_whnf() { ValueF::Pi(x, tx, tb) => { (x.clone(), tx.to_type(), tb.to_type()) } _ => return Err(mkerr(NotAFunction(f.clone()))), }; if a.get_type()?.as_ref() != &tx { - return Err(mkerr(TypeMismatch( - f.clone(), - tx.to_normalized(), - a.clone(), - ))); + return Err(mkerr(TypeMismatch(f.clone(), tx, a.clone()))); } Ok(RetTypeOnly(tb.subst_shift(&x.into(), &a))) @@ -434,13 +425,13 @@ fn type_last_layer( Annot(x, t) => { let t = t.to_type(); if &t != x.get_type()?.as_ref() { - return Err(mkerr(AnnotMismatch(x.clone(), t.to_normalized()))); + return Err(mkerr(AnnotMismatch(x.clone(), t))); } Ok(RetTypeOnly(x.get_type()?.into_owned())) } Assert(t) => { - match t.to_valuef() { - ValueF::Equivalence(ref x, ref y) if x == y => {} + match &*t.as_whnf() { + ValueF::Equivalence(x, y) if x == y => {} ValueF::Equivalence(x, y) => { return Err(mkerr(AssertMismatch( x.to_typed(), @@ -472,14 +463,11 @@ fn type_last_layer( } EmptyListLit(t) => { let t = t.to_type(); - match &t.to_valuef() { + match &*t.as_whnf() { ValueF::AppliedBuiltin(dhall_syntax::Builtin::List, args) if args.len() == 1 => {} _ => { - return Err(TypeError::new( - ctx, - InvalidListType(t.to_normalized()), - )) + return Err(TypeError::new(ctx, InvalidListType(t.clone()))) } } Ok(RetTypeOnly(t)) @@ -491,7 +479,7 @@ fn type_last_layer( if x.get_type()? != y.get_type()? { return Err(mkerr(InvalidListElement( i, - x.get_type()?.to_normalized(), + x.get_type()?.into_owned(), y.clone(), ))); } @@ -500,14 +488,14 @@ fn type_last_layer( if t.get_type()?.as_const() != Some(Type) { return Err(TypeError::new( ctx, - InvalidListType(t.to_normalized()), + InvalidListType(t.into_owned()), )); } Ok(RetTypeOnly( Typed::from_value_and_type( ValueF::from_builtin(dhall_syntax::Builtin::List) - .app(t.to_valuef()) + .app_value(t.to_value()) .into_value(), Typed::from_const(Type), ) @@ -517,16 +505,13 @@ fn type_last_layer( SomeLit(x) => { let t = x.get_type()?.into_owned(); if t.get_type()?.as_const() != Some(Type) { - return Err(TypeError::new( - ctx, - InvalidOptionalType(t.to_normalized()), - )); + return Err(TypeError::new(ctx, InvalidOptionalType(t))); } Ok(RetTypeOnly( Typed::from_value_and_type( ValueF::from_builtin(dhall_syntax::Builtin::Optional) - .app(t.to_valuef()) + .app_value(t.to_value()) .into_value(), Typed::from_const(Type).into_type(), ) @@ -551,7 +536,7 @@ fn type_last_layer( .into_type(), )), Field(r, x) => { - match &r.get_type()?.to_valuef() { + match &*r.get_type()?.as_whnf() { ValueF::RecordType(kts) => match kts.get(&x) { Some(tth) => { Ok(RetTypeOnly(tth.to_type())) @@ -561,8 +546,7 @@ fn type_last_layer( }, // TODO: branch here only when r.get_type() is a Const _ => { - let r = r.to_type(); - match &r.to_valuef() { + match &*r.as_whnf() { ValueF::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > Some(Some(t)) => { @@ -581,21 +565,21 @@ fn type_last_layer( None => { Err(mkerr(MissingUnionField( x.clone(), - r.to_normalized(), + r.clone(), ))) }, }, _ => { Err(mkerr(NotARecord( x.clone(), - r.to_normalized() + r.clone() ))) }, } } // _ => Err(mkerr(NotARecord( // x, - // r.to_type()?.to_normalized(), + // r.to_type()?, // ))), } } @@ -633,20 +617,22 @@ fn type_last_layer( } // Extract the LHS record type - let kts_x = match l_type.to_valuef() { + let l_type_borrow = l_type.as_whnf(); + let kts_x = match &*l_type_borrow { ValueF::RecordType(kts) => kts, _ => return Err(mkerr(MustCombineRecord(l.clone()))), }; // Extract the RHS record type - let kts_y = match r_type.to_valuef() { + let r_type_borrow = r_type.as_whnf(); + let kts_y = match &*r_type_borrow { ValueF::RecordType(kts) => kts, _ => return Err(mkerr(MustCombineRecord(r.clone()))), }; // Union the two records, prefering // the values found in the RHS. - let kts = merge_maps(&kts_x, &kts_y, |_, r_t| r_t.clone()); + let kts = merge_maps(kts_x, kts_y, |_, r_t| r_t.clone()); // Construct the final record type from the union Ok(RetTypeOnly( @@ -662,8 +648,8 @@ fn type_last_layer( // records of records when merging. fn combine_record_types( ctx: &TypecheckContext, - kts_l: HashMap, - kts_r: HashMap, + kts_l: &HashMap, + kts_r: &HashMap, ) -> Result { use crate::phase::normalize::outer_join; @@ -674,7 +660,7 @@ fn type_last_layer( inner_l: &TypedValue, inner_r: &TypedValue| -> Result { - match (inner_l.to_valuef(), inner_r.to_valuef()) { + match (&*inner_l.as_whnf(), &*inner_r.as_whnf()) { ( ValueF::RecordType(inner_l_kvs), ValueF::RecordType(inner_r_kvs), @@ -690,11 +676,9 @@ fn type_last_layer( let kts: HashMap> = outer_join( |l| Ok(l.to_type()), |r| Ok(r.to_type()), - |k: &Label, l: &TypedValue, r: &TypedValue| { - combine(k, l, r) - }, - &kts_l, - &kts_r, + combine, + kts_l, + kts_r, ); Ok(tck_record_type( @@ -717,13 +701,15 @@ fn type_last_layer( } // Extract the LHS record type - let kts_x = match l_type.to_valuef() { + let l_type_borrow = l_type.as_whnf(); + let kts_x = match &*l_type_borrow { ValueF::RecordType(kts) => kts, _ => return Err(mkerr(MustCombineRecord(l.clone()))), }; // Extract the RHS record type - let kts_y = match r_type.to_valuef() { + let r_type_borrow = r_type.as_whnf(); + let kts_y = match &*r_type_borrow { ValueF::RecordType(kts) => kts, _ => return Err(mkerr(MustCombineRecord(r.clone()))), }; @@ -735,8 +721,8 @@ fn type_last_layer( // records of records when merging. fn combine_record_types( ctx: &TypecheckContext, - kts_l: HashMap, - kts_r: HashMap, + kts_l: &HashMap, + kts_r: &HashMap, ) -> Result { use crate::phase::normalize::intersection_with_key; @@ -747,7 +733,7 @@ fn type_last_layer( kts_l_inner: &TypedValue, kts_r_inner: &TypedValue| -> Result { - match (kts_l_inner.to_valuef(), kts_r_inner.to_valuef()) { + match (&*kts_l_inner.as_whnf(), &*kts_r_inner.as_whnf()) { ( ValueF::RecordType(kvs_l_inner), ValueF::RecordType(kvs_r_inner), @@ -760,13 +746,7 @@ fn type_last_layer( } }; - let kts = intersection_with_key( - |k: &Label, l: &TypedValue, r: &TypedValue| { - combine(k, l, r) - }, - &kts_l, - &kts_r, - ); + let kts = intersection_with_key(combine, kts_l, kts_r); Ok(tck_record_type( ctx, @@ -776,8 +756,8 @@ fn type_last_layer( }; // Extract the Const of the LHS - let k_l = match l.get_type()?.to_valuef() { - ValueF::Const(k) => k, + let k_l = match l.get_type()?.as_const() { + Some(k) => k, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( l.clone(), @@ -786,8 +766,8 @@ fn type_last_layer( }; // Extract the Const of the RHS - let k_r = match r.get_type()?.to_valuef() { - ValueF::Const(k) => k, + let k_r = match r.get_type()?.as_const() { + Some(k) => k, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( r.clone(), @@ -808,7 +788,8 @@ fn type_last_layer( }; // Extract the LHS record type - let kts_x = match l.to_valuef() { + let borrow_l = l.as_whnf(); + let kts_x = match &*borrow_l { ValueF::RecordType(kts) => kts, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( @@ -818,7 +799,8 @@ fn type_last_layer( }; // Extract the RHS record type - let kts_y = match r.to_valuef() { + let borrow_r = r.as_whnf(); + let kts_y = match &*borrow_r { ValueF::RecordType(kts) => kts, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( @@ -833,7 +815,7 @@ fn type_last_layer( .and(Ok(RetTypeOnly(Typed::from_const(k)))) } BinOp(o @ ListAppend, l, r) => { - match l.get_type()?.to_valuef() { + match &*l.get_type()?.as_whnf() { ValueF::AppliedBuiltin(List, _) => {} _ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone()))), } @@ -895,56 +877,63 @@ fn type_last_layer( Ok(RetTypeOnly(t)) } Merge(record, union, type_annot) => { - let handlers = match record.get_type()?.to_valuef() { + let record_type = record.get_type()?; + let record_borrow = record_type.as_whnf(); + let handlers = match &*record_borrow { ValueF::RecordType(kts) => kts, _ => return Err(mkerr(Merge1ArgMustBeRecord(record.clone()))), }; - let variants = match union.get_type()?.to_valuef() { + let union_type = union.get_type()?; + let union_borrow = union_type.as_whnf(); + let variants = match &*union_borrow { ValueF::UnionType(kts) => kts, _ => return Err(mkerr(Merge2ArgMustBeUnion(union.clone()))), }; let mut inferred_type = None; - for (x, handler) in handlers.iter() { - let handler_return_type = match variants.get(x) { - // Union alternative with type - Some(Some(variant_type)) => { - let variant_type = variant_type.to_type(); - let handler_type = handler.to_type(); - let (x, tx, tb) = match &handler_type.to_valuef() { - ValueF::Pi(x, tx, tb) => { - (x.clone(), tx.to_type(), tb.to_type()) + for (x, handler) in handlers { + let handler_return_type = + match variants.get(x) { + // Union alternative with type + Some(Some(variant_type)) => { + let variant_type = variant_type.to_type(); + let handler_type = handler.to_type(); + let (x, tx, tb) = match &*handler_type.as_whnf() { + ValueF::Pi(x, tx, tb) => { + (x.clone(), tx.to_type(), tb.to_type()) + } + _ => { + return Err(mkerr(NotAFunction( + handler_type.clone(), + ))) + } + }; + + if &variant_type != &tx { + return Err(mkerr(TypeMismatch( + handler_type, + tx, + variant_type, + ))); } - _ => return Err(mkerr(NotAFunction(handler_type))), - }; - - if &variant_type != &tx { - return Err(mkerr(TypeMismatch( - handler_type, - tx.to_normalized(), - variant_type, - ))); - } - // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`. - match tb.over_binder(x) { - Some(x) => x, - None => { - return Err(mkerr( + // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`. + match tb.over_binder(x) { + Some(x) => x, + None => return Err(mkerr( MergeHandlerReturnTypeMustNotBeDependent, - )) + )), } } - } - // Union alternative without type - Some(None) => handler.to_type(), - None => { - return Err(mkerr(MergeHandlerMissingVariant( - x.clone(), - ))) - } - }; + // Union alternative without type + Some(None) => handler.to_type(), + None => { + return Err(mkerr(MergeHandlerMissingVariant( + x.clone(), + ))) + } + }; match &inferred_type { None => inferred_type = Some(handler_return_type), Some(t) => { @@ -974,8 +963,9 @@ fn type_last_layer( } } Projection(record, labels) => { - let trecord = record.get_type()?; - let kts = match trecord.to_valuef() { + let record_type = record.get_type()?; + let record_borrow = record_type.as_whnf(); + let kts = match &*record_borrow { ValueF::RecordType(kts) => kts, _ => return Err(mkerr(ProjectionMustBeRecord)), }; @@ -991,7 +981,7 @@ fn type_last_layer( Ok(RetTypeOnly( Typed::from_value_and_type( ValueF::RecordType(new_kts).into_value(), - trecord.get_type()?.into_owned(), + record_type.get_type()?.into_owned(), ) .to_type(), )) -- cgit v1.2.3 From 26a1fd0f0861038a76a0f9b09eaef16d808d4139 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 19 Aug 2019 21:52:26 +0200 Subject: Use TypedValue instead of Typed in normalize and typecheck Now Typed is only used in dhall::phase, similarly to Parsed/Resolved/Normalized --- dhall/src/phase/typecheck.rs | 392 +++++++++++++++++++------------------------ 1 file changed, 174 insertions(+), 218 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index c303ada..07c4ad8 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -9,14 +9,14 @@ use crate::core::value::{TypedValue, Value}; use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; use crate::error::{TypeError, TypeMessage}; -use crate::phase::{Normalized, Resolved, Type, Typed}; +use crate::phase::Normalized; fn tck_pi_type( ctx: &TypecheckContext, x: Label, - tx: Type, - te: Type, -) -> Result { + tx: TypedValue, + te: TypedValue, +) -> Result { use crate::error::TypeMessage::*; let ctx2 = ctx.insert_type(&x, tx.clone()); @@ -37,21 +37,16 @@ fn tck_pi_type( let k = function_check(ka, kb); - Ok(Typed::from_value_and_type( - ValueF::Pi( - x.into(), - TypedValue::from_type(tx), - TypedValue::from_type(te), - ) - .into_value(), - Type::from_const(k), + Ok(TypedValue::from_value_and_type( + ValueF::Pi(x.into(), tx, te).into_value(), + TypedValue::from_const(k), )) } fn tck_record_type( ctx: &TypecheckContext, - kts: impl IntoIterator>, -) -> Result { + kts: impl IntoIterator>, +) -> Result { use crate::error::TypeMessage::*; use std::collections::hash_map::Entry; let mut new_kts = HashMap::new(); @@ -62,36 +57,32 @@ fn tck_record_type( match (k, t.get_type()?.as_const()) { (None, Some(k2)) => k = Some(k2), (Some(k1), Some(k2)) if k1 == k2 => {} - _ => { - return Err(TypeError::new( - ctx, - InvalidFieldType(x.clone(), t.clone()), - )) - } + _ => return Err(TypeError::new(ctx, InvalidFieldType(x, t))), } - let entry = new_kts.entry(x.clone()); + let entry = new_kts.entry(x); match &entry { Entry::Occupied(_) => { return Err(TypeError::new(ctx, RecordTypeDuplicateField)) } - Entry::Vacant(_) => { - entry.or_insert_with(|| TypedValue::from_type(t.clone())) - } + Entry::Vacant(_) => entry.or_insert_with(|| t), }; } // An empty record type has type Type - let k = k.unwrap_or(dhall_syntax::Const::Type); + let k = k.unwrap_or(Const::Type); - Ok(Typed::from_value_and_type( + Ok(TypedValue::from_value_and_type( ValueF::RecordType(new_kts).into_value(), - Type::from_const(k), + TypedValue::from_const(k), )) } -fn tck_union_type( +fn tck_union_type( ctx: &TypecheckContext, - kts: impl IntoIterator), TypeError>>, -) -> Result { + kts: Iter, +) -> Result +where + Iter: IntoIterator), TypeError>>, +{ use crate::error::TypeMessage::*; use std::collections::hash_map::Entry; let mut new_kts = HashMap::new(); @@ -106,46 +97,43 @@ fn tck_union_type( _ => { return Err(TypeError::new( ctx, - InvalidFieldType(x.clone(), t.clone()), + InvalidFieldType(x, t.clone()), )) } } } - let entry = new_kts.entry(x.clone()); + let entry = new_kts.entry(x); match &entry { Entry::Occupied(_) => { return Err(TypeError::new(ctx, UnionTypeDuplicateField)) } - Entry::Vacant(_) => entry.or_insert_with(|| { - t.as_ref().map(|t| TypedValue::from_type(t.clone())) - }), + Entry::Vacant(_) => entry.or_insert_with(|| t), }; } // An empty union type has type Type; // an union type with only unary variants also has type Type - let k = k.unwrap_or(dhall_syntax::Const::Type); + let k = k.unwrap_or(Const::Type); - Ok(Typed::from_value_and_type( + Ok(TypedValue::from_value_and_type( ValueF::UnionType(new_kts).into_value(), - Type::from_const(k), + TypedValue::from_const(k), )) } fn function_check(a: Const, b: Const) -> Const { - use dhall_syntax::Const::Type; use std::cmp::max; - if b == Type { - Type + if b == Const::Type { + Const::Type } else { max(a, b) } } -pub(crate) fn type_of_const(c: Const) -> Result { +pub(crate) fn type_of_const(c: Const) -> Result { match c { - Const::Type => Ok(Type::from_const(Const::Kind)), - Const::Kind => Ok(Type::from_const(Const::Sort)), + Const::Type => Ok(TypedValue::from_const(Const::Kind)), + Const::Kind => Ok(TypedValue::from_const(Const::Sort)), Const::Sort => { Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) } @@ -293,25 +281,16 @@ fn type_of_builtin(b: Builtin) -> Expr { } } -/// Takes an expression that is meant to contain a Type -/// and turn it into a type, typechecking it along the way. -pub(crate) fn mktype( - ctx: &TypecheckContext, - e: SubExpr, -) -> Result { - Ok(type_with(ctx, e)?.to_type()) -} - -pub(crate) fn builtin_to_type(b: Builtin) -> Result { - mktype(&TypecheckContext::new(), SubExpr::from_builtin(b)) +pub(crate) fn builtin_to_type(b: Builtin) -> Result { + type_with(&TypecheckContext::new(), SubExpr::from_builtin(b)) } /// Intermediary return type enum Ret { /// Returns the contained value as is - RetWhole(Typed), - /// Use the contained Type as the type of the input expression - RetTypeOnly(Type), + RetWhole(TypedValue), + /// Use the contained TypedValue as the type of the input expression + RetTypeOnly(TypedValue), } /// Type-check an expression and return the expression alongside its type if type-checking @@ -321,28 +300,24 @@ enum Ret { fn type_with( ctx: &TypecheckContext, e: SubExpr, -) -> Result { +) -> Result { use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var}; use Ret::*; Ok(match e.as_ref() { Lam(x, t, b) => { - let tx = mktype(ctx, t.clone())?; + let tx = type_with(ctx, t.clone())?; let ctx2 = ctx.insert_type(x, tx.clone()); let b = type_with(&ctx2, b.clone())?; - let v = ValueF::Lam( - x.clone().into(), - TypedValue::from_type(tx.clone()), - b.to_value(), - ); + let v = ValueF::Lam(x.clone().into(), tx.clone(), b.to_value()); let tb = b.get_type()?.into_owned(); - let t = tck_pi_type(ctx, x.clone(), tx, tb)?.to_type(); - Typed::from_value_and_type(Value::from_valuef(v), t) + let t = tck_pi_type(ctx, x.clone(), tx, tb)?; + TypedValue::from_valuef_and_type(v, t) } Pi(x, ta, tb) => { - let ta = mktype(ctx, ta.clone())?; + let ta = type_with(ctx, ta.clone())?; let ctx2 = ctx.insert_type(x, ta.clone()); - let tb = mktype(&ctx2, tb.clone())?; + let tb = type_with(&ctx2, tb.clone())?; return tck_pi_type(ctx, x.clone(), ta, tb); } Let(x, t, v, e) => { @@ -355,9 +330,9 @@ fn type_with( let v = type_with(ctx, v)?; return type_with(&ctx.insert_value(x, v.clone())?, e.clone()); } - Embed(p) => p.clone().into_typed(), + Embed(p) => p.clone().into_typed().into_typedvalue(), Var(var) => match ctx.lookup(&var) { - Some(typed) => typed, + Some(typed) => typed.clone(), None => { return Err(TypeError::new( ctx, @@ -376,7 +351,7 @@ fn type_with( match ret { RetTypeOnly(typ) => { let expr = expr.map_ref(|typed| typed.to_value()); - Typed::from_value_and_type( + TypedValue::from_value_and_type( Value::from_partial_expr(expr), typ, ) @@ -391,7 +366,7 @@ fn type_with( /// layer. fn type_last_layer( ctx: &TypecheckContext, - e: &ExprF, + e: &ExprF, ) -> Result { use crate::error::TypeMessage::*; use dhall_syntax::BinOp::*; @@ -410,22 +385,24 @@ fn type_last_layer( } App(f, a) => { let tf = f.get_type()?; - let (x, tx, tb) = match &*tf.as_whnf() { - ValueF::Pi(x, tx, tb) => { - (x.clone(), tx.to_type(), tb.to_type()) - } + let tf_borrow = tf.as_whnf(); + let (x, tx, tb) = match &*tf_borrow { + ValueF::Pi(x, tx, tb) => (x, tx, tb), _ => return Err(mkerr(NotAFunction(f.clone()))), }; - if a.get_type()?.as_ref() != &tx { - return Err(mkerr(TypeMismatch(f.clone(), tx, a.clone()))); + if a.get_type()?.as_ref() != tx { + return Err(mkerr(TypeMismatch( + f.clone(), + tx.clone(), + a.clone(), + ))); } - Ok(RetTypeOnly(tb.subst_shift(&x.into(), &a))) + Ok(RetTypeOnly(tb.subst_shift(&x.into(), a))) } Annot(x, t) => { - let t = t.to_type(); - if &t != x.get_type()?.as_ref() { - return Err(mkerr(AnnotMismatch(x.clone(), t))); + if t != x.get_type()?.as_ref() { + return Err(mkerr(AnnotMismatch(x.clone(), t.clone()))); } Ok(RetTypeOnly(x.get_type()?.into_owned())) } @@ -433,14 +410,11 @@ fn type_last_layer( match &*t.as_whnf() { ValueF::Equivalence(x, y) if x == y => {} ValueF::Equivalence(x, y) => { - return Err(mkerr(AssertMismatch( - x.to_typed(), - y.to_typed(), - ))) + return Err(mkerr(AssertMismatch(x.clone(), y.clone()))) } _ => return Err(mkerr(AssertMustTakeEquivalence)), } - Ok(RetTypeOnly(t.to_type())) + Ok(RetTypeOnly(t.clone())) } BoolIf(x, y, z) => { if x.get_type()?.as_ref() != &builtin_to_type(Bool)? { @@ -462,7 +436,6 @@ fn type_last_layer( Ok(RetTypeOnly(y.get_type()?.into_owned())) } EmptyListLit(t) => { - let t = t.to_type(); match &*t.as_whnf() { ValueF::AppliedBuiltin(dhall_syntax::Builtin::List, args) if args.len() == 1 => {} @@ -470,7 +443,7 @@ fn type_last_layer( return Err(TypeError::new(ctx, InvalidListType(t.clone()))) } } - Ok(RetTypeOnly(t)) + Ok(RetTypeOnly(t.clone())) } NEListLit(xs) => { let mut iter = xs.iter().enumerate(); @@ -492,15 +465,12 @@ fn type_last_layer( )); } - Ok(RetTypeOnly( - Typed::from_value_and_type( - ValueF::from_builtin(dhall_syntax::Builtin::List) - .app_value(t.to_value()) - .into_value(), - Typed::from_const(Type), - ) - .to_type(), - )) + Ok(RetTypeOnly(TypedValue::from_value_and_type( + ValueF::from_builtin(dhall_syntax::Builtin::List) + .app_value(t.to_value()) + .into_value(), + TypedValue::from_const(Type), + ))) } SomeLit(x) => { let t = x.get_type()?.into_owned(); @@ -508,38 +478,31 @@ fn type_last_layer( return Err(TypeError::new(ctx, InvalidOptionalType(t))); } - Ok(RetTypeOnly( - Typed::from_value_and_type( - ValueF::from_builtin(dhall_syntax::Builtin::Optional) - .app_value(t.to_value()) - .into_value(), - Typed::from_const(Type).into_type(), - ) - .to_type(), - )) + Ok(RetTypeOnly(TypedValue::from_value_and_type( + ValueF::from_builtin(dhall_syntax::Builtin::Optional) + .app_value(t.to_value()) + .into_value(), + TypedValue::from_const(Type), + ))) } RecordType(kts) => Ok(RetWhole(tck_record_type( ctx, - kts.iter().map(|(x, t)| Ok((x.clone(), t.to_type()))), + kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), )?)), UnionType(kts) => Ok(RetWhole(tck_union_type( ctx, - kts.iter() - .map(|(x, t)| Ok((x.clone(), t.as_ref().map(|t| t.to_type())))), + kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), + )?)), + RecordLit(kvs) => Ok(RetTypeOnly(tck_record_type( + ctx, + kvs.iter() + .map(|(x, v)| Ok((x.clone(), v.get_type()?.into_owned()))), )?)), - RecordLit(kvs) => Ok(RetTypeOnly( - tck_record_type( - ctx, - kvs.iter() - .map(|(x, v)| Ok((x.clone(), v.get_type()?.into_owned()))), - )? - .into_type(), - )), Field(r, x) => { match &*r.get_type()?.as_whnf() { ValueF::RecordType(kts) => match kts.get(&x) { Some(tth) => { - Ok(RetTypeOnly(tth.to_type())) + Ok(RetTypeOnly(tth.clone())) }, None => Err(mkerr(MissingRecordField(x.clone(), r.clone()))), @@ -554,9 +517,9 @@ fn type_last_layer( tck_pi_type( ctx, "_".into(), - t.to_type(), + t.clone(), r.under_binder(Label::from("_")), - )?.to_type() + )? )) }, Some(None) => { @@ -579,12 +542,12 @@ fn type_last_layer( } // _ => Err(mkerr(NotARecord( // x, - // r.to_type()?, + // r?, // ))), } } - Const(c) => Ok(RetWhole(Typed::from_const(*c))), - Builtin(b) => Ok(RetTypeOnly(mktype(ctx, rc(type_of_builtin(*b)))?)), + Const(c) => Ok(RetWhole(TypedValue::from_const(*c))), + Builtin(b) => Ok(RetTypeOnly(type_with(ctx, rc(type_of_builtin(*b)))?)), BoolLit(_) => Ok(RetTypeOnly(builtin_to_type(Bool)?)), NaturalLit(_) => Ok(RetTypeOnly(builtin_to_type(Natural)?)), IntegerLit(_) => Ok(RetTypeOnly(builtin_to_type(Integer)?)), @@ -635,13 +598,10 @@ fn type_last_layer( let kts = merge_maps(kts_x, kts_y, |_, r_t| r_t.clone()); // Construct the final record type from the union - Ok(RetTypeOnly( - tck_record_type( - ctx, - kts.iter().map(|(x, v)| Ok((x.clone(), v.to_type()))), - )? - .into_type(), - )) + Ok(RetTypeOnly(tck_record_type( + ctx, + kts.into_iter().map(|(x, v)| Ok((x.clone(), v))), + )?)) } BinOp(RecursiveRecordMerge, l, r) => { // A recursive function to dig down into @@ -650,42 +610,46 @@ fn type_last_layer( ctx: &TypecheckContext, kts_l: &HashMap, kts_r: &HashMap, - ) -> Result { + ) -> Result { use crate::phase::normalize::outer_join; - // If the Label exists for both records and Type for the values + // If the Label exists for both records and the values // are records themselves, then we hit the recursive case. // Otherwise we have a field collision. - let combine = |k: &Label, - inner_l: &TypedValue, - inner_r: &TypedValue| - -> Result { - match (&*inner_l.as_whnf(), &*inner_r.as_whnf()) { - ( - ValueF::RecordType(inner_l_kvs), - ValueF::RecordType(inner_r_kvs), - ) => { - combine_record_types(ctx, inner_l_kvs, inner_r_kvs) + let combine = + |k: &Label, + inner_l: &TypedValue, + inner_r: &TypedValue| + -> Result { + match (&*inner_l.as_whnf(), &*inner_r.as_whnf()) { + ( + ValueF::RecordType(inner_l_kvs), + ValueF::RecordType(inner_r_kvs), + ) => combine_record_types( + ctx, + inner_l_kvs, + inner_r_kvs, + ), + (_, _) => Err(TypeError::new( + ctx, + FieldCollision(k.clone()), + )), } - (_, _) => { - Err(TypeError::new(ctx, FieldCollision(k.clone()))) - } - } - }; + }; - let kts: HashMap> = outer_join( - |l| Ok(l.to_type()), - |r| Ok(r.to_type()), - combine, - kts_l, - kts_r, - ); + let kts: HashMap> = + outer_join( + |l| Ok(l.clone()), + |r| Ok(r.clone()), + combine, + kts_l, + kts_r, + ); Ok(tck_record_type( ctx, kts.into_iter().map(|(x, v)| v.map(|r| (x.clone(), r))), - )? - .into_type()) + )?) }; let l_type = l.get_type()?; @@ -723,36 +687,40 @@ fn type_last_layer( ctx: &TypecheckContext, kts_l: &HashMap, kts_r: &HashMap, - ) -> Result { + ) -> Result { use crate::phase::normalize::intersection_with_key; - // If the Label exists for both records and Type for the values + // If the Label exists for both records and the values // are records themselves, then we hit the recursive case. // Otherwise we have a field collision. - let combine = |k: &Label, - kts_l_inner: &TypedValue, - kts_r_inner: &TypedValue| - -> Result { - match (&*kts_l_inner.as_whnf(), &*kts_r_inner.as_whnf()) { - ( - ValueF::RecordType(kvs_l_inner), - ValueF::RecordType(kvs_r_inner), - ) => { - combine_record_types(ctx, kvs_l_inner, kvs_r_inner) + let combine = + |k: &Label, + kts_l_inner: &TypedValue, + kts_r_inner: &TypedValue| + -> Result { + match (&*kts_l_inner.as_whnf(), &*kts_r_inner.as_whnf()) + { + ( + ValueF::RecordType(kvs_l_inner), + ValueF::RecordType(kvs_r_inner), + ) => combine_record_types( + ctx, + kvs_l_inner, + kvs_r_inner, + ), + (_, _) => Err(TypeError::new( + ctx, + FieldCollision(k.clone()), + )), } - (_, _) => { - Err(TypeError::new(ctx, FieldCollision(k.clone()))) - } - } - }; + }; let kts = intersection_with_key(combine, kts_l, kts_r); Ok(tck_record_type( ctx, kts.into_iter().map(|(x, v)| v.map(|r| (x.clone(), r))), - )? - .into_type()) + )?) }; // Extract the Const of the LHS @@ -780,8 +748,8 @@ fn type_last_layer( k_l } else { return Err(mkerr(RecordTypeMismatch( - Typed::from_const(k_l), - Typed::from_const(k_r), + TypedValue::from_const(k_l), + TypedValue::from_const(k_r), l.clone(), r.clone(), ))); @@ -812,7 +780,7 @@ fn type_last_layer( // Ensure that the records combine without a type error // and if not output the final Const value. combine_record_types(ctx, kts_x, kts_y) - .and(Ok(RetTypeOnly(Typed::from_const(k)))) + .and(Ok(RetTypeOnly(TypedValue::from_const(k)))) } BinOp(o @ ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { @@ -847,7 +815,7 @@ fn type_last_layer( ))); } - Ok(RetTypeOnly(Typed::from_const(Type).into_type())) + Ok(RetTypeOnly(TypedValue::from_const(Type))) } BinOp(o, l, r) => { let t = builtin_to_type(match o { @@ -892,17 +860,14 @@ fn type_last_layer( }; let mut inferred_type = None; - for (x, handler) in handlers { + for (x, handler_type) in handlers { let handler_return_type = match variants.get(x) { // Union alternative with type Some(Some(variant_type)) => { - let variant_type = variant_type.to_type(); - let handler_type = handler.to_type(); - let (x, tx, tb) = match &*handler_type.as_whnf() { - ValueF::Pi(x, tx, tb) => { - (x.clone(), tx.to_type(), tb.to_type()) - } + let handler_type_borrow = handler_type.as_whnf(); + let (x, tx, tb) = match &*handler_type_borrow { + ValueF::Pi(x, tx, tb) => (x, tx, tb), _ => { return Err(mkerr(NotAFunction( handler_type.clone(), @@ -910,11 +875,11 @@ fn type_last_layer( } }; - if &variant_type != &tx { + if variant_type != tx { return Err(mkerr(TypeMismatch( - handler_type, - tx, - variant_type, + handler_type.clone(), + tx.clone(), + variant_type.clone(), ))); } @@ -927,7 +892,7 @@ fn type_last_layer( } } // Union alternative without type - Some(None) => handler.to_type(), + Some(None) => handler_type.clone(), None => { return Err(mkerr(MergeHandlerMissingVariant( x.clone(), @@ -951,14 +916,13 @@ fn type_last_layer( match (inferred_type, type_annot) { (Some(ref t1), Some(t2)) => { - let t2 = t2.to_type(); - if t1 != &t2 { + if t1 != t2 { return Err(mkerr(MergeAnnotMismatch)); } - Ok(RetTypeOnly(t2)) + Ok(RetTypeOnly(t2.clone())) } (Some(t), None) => Ok(RetTypeOnly(t)), - (None, Some(t)) => Ok(RetTypeOnly(t.to_type())), + (None, Some(t)) => Ok(RetTypeOnly(t.clone())), (None, None) => Err(mkerr(MergeEmptyNeedsAnnotation)), } } @@ -978,34 +942,26 @@ fn type_last_layer( }; } - Ok(RetTypeOnly( - Typed::from_value_and_type( - ValueF::RecordType(new_kts).into_value(), - record_type.get_type()?.into_owned(), - ) - .to_type(), - )) + Ok(RetTypeOnly(TypedValue::from_value_and_type( + ValueF::RecordType(new_kts).into_value(), + record_type.get_type()?.into_owned(), + ))) } } } -/// `typeOf` is the same as `type_with` with an empty context, meaning that the +/// `type_of` is the same as `type_with` with an empty context, meaning that the /// expression must be closed (i.e. no free variables), otherwise type-checking /// will fail. -fn type_of(e: SubExpr) -> Result { - let ctx = TypecheckContext::new(); - type_with(&ctx, e) -} - -pub(crate) fn typecheck(e: Resolved) -> Result { - type_of(e.0) +pub(crate) fn typecheck( + e: SubExpr, +) -> Result { + type_with(&TypecheckContext::new(), e) } pub(crate) fn typecheck_with( - e: Resolved, - ty: &Type, -) -> Result { - let expr: SubExpr<_> = e.0; - let ty: SubExpr<_> = ty.to_expr(); - type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty))) + expr: SubExpr, + ty: SubExpr, +) -> Result { + typecheck(expr.rewrap(ExprF::Annot(expr.clone(), ty))) } -- cgit v1.2.3 From 07a276c1d6ee892b93abbd7a73c78c96d56f4fe7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 19 Aug 2019 22:26:17 +0200 Subject: Reduce untyped construction of Values --- dhall/src/phase/typecheck.rs | 33 ++++++++++++++++----------------- 1 file changed, 16 insertions(+), 17 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 07c4ad8..e24f5a3 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -5,7 +5,7 @@ use dhall_syntax::{ }; use crate::core::context::TypecheckContext; -use crate::core::value::{TypedValue, Value}; +use crate::core::value::TypedValue; use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; use crate::error::{TypeError, TypeMessage}; @@ -37,8 +37,8 @@ fn tck_pi_type( let k = function_check(ka, kb); - Ok(TypedValue::from_value_and_type( - ValueF::Pi(x.into(), tx, te).into_value(), + Ok(TypedValue::from_valuef_and_type( + ValueF::Pi(x.into(), tx, te), TypedValue::from_const(k), )) } @@ -70,8 +70,8 @@ fn tck_record_type( // An empty record type has type Type let k = k.unwrap_or(Const::Type); - Ok(TypedValue::from_value_and_type( - ValueF::RecordType(new_kts).into_value(), + Ok(TypedValue::from_valuef_and_type( + ValueF::RecordType(new_kts), TypedValue::from_const(k), )) } @@ -115,8 +115,8 @@ where // an union type with only unary variants also has type Type let k = k.unwrap_or(Const::Type); - Ok(TypedValue::from_value_and_type( - ValueF::UnionType(new_kts).into_value(), + Ok(TypedValue::from_valuef_and_type( + ValueF::UnionType(new_kts), TypedValue::from_const(k), )) } @@ -281,6 +281,7 @@ fn type_of_builtin(b: Builtin) -> Expr { } } +// TODO: this can't fail in practise pub(crate) fn builtin_to_type(b: Builtin) -> Result { type_with(&TypecheckContext::new(), SubExpr::from_builtin(b)) } @@ -351,8 +352,8 @@ fn type_with( match ret { RetTypeOnly(typ) => { let expr = expr.map_ref(|typed| typed.to_value()); - TypedValue::from_value_and_type( - Value::from_partial_expr(expr), + TypedValue::from_valuef_and_type( + ValueF::PartialExpr(expr), typ, ) } @@ -465,10 +466,9 @@ fn type_last_layer( )); } - Ok(RetTypeOnly(TypedValue::from_value_and_type( + Ok(RetTypeOnly(TypedValue::from_valuef_and_type( ValueF::from_builtin(dhall_syntax::Builtin::List) - .app_value(t.to_value()) - .into_value(), + .app_value(t.to_value()), TypedValue::from_const(Type), ))) } @@ -478,10 +478,9 @@ fn type_last_layer( return Err(TypeError::new(ctx, InvalidOptionalType(t))); } - Ok(RetTypeOnly(TypedValue::from_value_and_type( + Ok(RetTypeOnly(TypedValue::from_valuef_and_type( ValueF::from_builtin(dhall_syntax::Builtin::Optional) - .app_value(t.to_value()) - .into_value(), + .app_value(t.to_value()), TypedValue::from_const(Type), ))) } @@ -942,8 +941,8 @@ fn type_last_layer( }; } - Ok(RetTypeOnly(TypedValue::from_value_and_type( - ValueF::RecordType(new_kts).into_value(), + Ok(RetTypeOnly(TypedValue::from_valuef_and_type( + ValueF::RecordType(new_kts), record_type.get_type()?.into_owned(), ))) } -- cgit v1.2.3 From 730f2ebb146792994c7492b6c05f7d09d42cbccf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 19 Aug 2019 23:00:49 +0200 Subject: Merge TypedValue and Value --- dhall/src/phase/typecheck.rs | 177 ++++++++++++++++++++----------------------- 1 file changed, 81 insertions(+), 96 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index e24f5a3..e65881e 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -5,7 +5,7 @@ use dhall_syntax::{ }; use crate::core::context::TypecheckContext; -use crate::core::value::TypedValue; +use crate::core::value::Value; use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; use crate::error::{TypeError, TypeMessage}; @@ -14,9 +14,9 @@ use crate::phase::Normalized; fn tck_pi_type( ctx: &TypecheckContext, x: Label, - tx: TypedValue, - te: TypedValue, -) -> Result { + tx: Value, + te: Value, +) -> Result { use crate::error::TypeMessage::*; let ctx2 = ctx.insert_type(&x, tx.clone()); @@ -37,16 +37,16 @@ fn tck_pi_type( let k = function_check(ka, kb); - Ok(TypedValue::from_valuef_and_type( + Ok(Value::from_valuef_and_type( ValueF::Pi(x.into(), tx, te), - TypedValue::from_const(k), + Value::from_const(k), )) } fn tck_record_type( ctx: &TypecheckContext, - kts: impl IntoIterator>, -) -> Result { + kts: impl IntoIterator>, +) -> Result { use crate::error::TypeMessage::*; use std::collections::hash_map::Entry; let mut new_kts = HashMap::new(); @@ -70,18 +70,18 @@ fn tck_record_type( // An empty record type has type Type let k = k.unwrap_or(Const::Type); - Ok(TypedValue::from_valuef_and_type( + Ok(Value::from_valuef_and_type( ValueF::RecordType(new_kts), - TypedValue::from_const(k), + Value::from_const(k), )) } fn tck_union_type( ctx: &TypecheckContext, kts: Iter, -) -> Result +) -> Result where - Iter: IntoIterator), TypeError>>, + Iter: IntoIterator), TypeError>>, { use crate::error::TypeMessage::*; use std::collections::hash_map::Entry; @@ -115,9 +115,9 @@ where // an union type with only unary variants also has type Type let k = k.unwrap_or(Const::Type); - Ok(TypedValue::from_valuef_and_type( + Ok(Value::from_valuef_and_type( ValueF::UnionType(new_kts), - TypedValue::from_const(k), + Value::from_const(k), )) } @@ -130,10 +130,10 @@ fn function_check(a: Const, b: Const) -> Const { } } -pub(crate) fn type_of_const(c: Const) -> Result { +pub(crate) fn type_of_const(c: Const) -> Result { match c { - Const::Type => Ok(TypedValue::from_const(Const::Kind)), - Const::Kind => Ok(TypedValue::from_const(Const::Sort)), + Const::Type => Ok(Value::from_const(Const::Kind)), + Const::Kind => Ok(Value::from_const(Const::Sort)), Const::Sort => { Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) } @@ -282,16 +282,16 @@ fn type_of_builtin(b: Builtin) -> Expr { } // TODO: this can't fail in practise -pub(crate) fn builtin_to_type(b: Builtin) -> Result { +pub(crate) fn builtin_to_type(b: Builtin) -> Result { type_with(&TypecheckContext::new(), SubExpr::from_builtin(b)) } /// Intermediary return type enum Ret { /// Returns the contained value as is - RetWhole(TypedValue), - /// Use the contained TypedValue as the type of the input expression - RetTypeOnly(TypedValue), + RetWhole(Value), + /// Use the contained Value as the type of the input expression + RetTypeOnly(Value), } /// Type-check an expression and return the expression alongside its type if type-checking @@ -301,7 +301,7 @@ enum Ret { fn type_with( ctx: &TypecheckContext, e: SubExpr, -) -> Result { +) -> Result { use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var}; use Ret::*; @@ -313,7 +313,7 @@ fn type_with( let v = ValueF::Lam(x.clone().into(), tx.clone(), b.to_value()); let tb = b.get_type()?.into_owned(); let t = tck_pi_type(ctx, x.clone(), tx, tb)?; - TypedValue::from_valuef_and_type(v, t) + Value::from_valuef_and_type(v, t) } Pi(x, ta, tb) => { let ta = type_with(ctx, ta.clone())?; @@ -331,7 +331,7 @@ fn type_with( let v = type_with(ctx, v)?; return type_with(&ctx.insert_value(x, v.clone())?, e.clone()); } - Embed(p) => p.clone().into_typed().into_typedvalue(), + Embed(p) => p.clone().into_typed().into_value(), Var(var) => match ctx.lookup(&var) { Some(typed) => typed.clone(), None => { @@ -352,10 +352,7 @@ fn type_with( match ret { RetTypeOnly(typ) => { let expr = expr.map_ref(|typed| typed.to_value()); - TypedValue::from_valuef_and_type( - ValueF::PartialExpr(expr), - typ, - ) + Value::from_valuef_and_type(ValueF::PartialExpr(expr), typ) } RetWhole(tt) => tt, } @@ -367,7 +364,7 @@ fn type_with( /// layer. fn type_last_layer( ctx: &TypecheckContext, - e: &ExprF, + e: &ExprF, ) -> Result { use crate::error::TypeMessage::*; use dhall_syntax::BinOp::*; @@ -466,10 +463,10 @@ fn type_last_layer( )); } - Ok(RetTypeOnly(TypedValue::from_valuef_and_type( + Ok(RetTypeOnly(Value::from_valuef_and_type( ValueF::from_builtin(dhall_syntax::Builtin::List) .app_value(t.to_value()), - TypedValue::from_const(Type), + Value::from_const(Type), ))) } SomeLit(x) => { @@ -478,10 +475,10 @@ fn type_last_layer( return Err(TypeError::new(ctx, InvalidOptionalType(t))); } - Ok(RetTypeOnly(TypedValue::from_valuef_and_type( + Ok(RetTypeOnly(Value::from_valuef_and_type( ValueF::from_builtin(dhall_syntax::Builtin::Optional) .app_value(t.to_value()), - TypedValue::from_const(Type), + Value::from_const(Type), ))) } RecordType(kts) => Ok(RetWhole(tck_record_type( @@ -545,7 +542,7 @@ fn type_last_layer( // ))), } } - Const(c) => Ok(RetWhole(TypedValue::from_const(*c))), + Const(c) => Ok(RetWhole(Value::from_const(*c))), Builtin(b) => Ok(RetTypeOnly(type_with(ctx, rc(type_of_builtin(*b)))?)), BoolLit(_) => Ok(RetTypeOnly(builtin_to_type(Bool)?)), NaturalLit(_) => Ok(RetTypeOnly(builtin_to_type(Natural)?)), @@ -607,43 +604,38 @@ fn type_last_layer( // records of records when merging. fn combine_record_types( ctx: &TypecheckContext, - kts_l: &HashMap, - kts_r: &HashMap, - ) -> Result { + kts_l: &HashMap, + kts_r: &HashMap, + ) -> Result { use crate::phase::normalize::outer_join; // If the Label exists for both records and the values // are records themselves, then we hit the recursive case. // Otherwise we have a field collision. - let combine = - |k: &Label, - inner_l: &TypedValue, - inner_r: &TypedValue| - -> Result { - match (&*inner_l.as_whnf(), &*inner_r.as_whnf()) { - ( - ValueF::RecordType(inner_l_kvs), - ValueF::RecordType(inner_r_kvs), - ) => combine_record_types( - ctx, - inner_l_kvs, - inner_r_kvs, - ), - (_, _) => Err(TypeError::new( - ctx, - FieldCollision(k.clone()), - )), + let combine = |k: &Label, + inner_l: &Value, + inner_r: &Value| + -> Result { + match (&*inner_l.as_whnf(), &*inner_r.as_whnf()) { + ( + ValueF::RecordType(inner_l_kvs), + ValueF::RecordType(inner_r_kvs), + ) => { + combine_record_types(ctx, inner_l_kvs, inner_r_kvs) } - }; + (_, _) => { + Err(TypeError::new(ctx, FieldCollision(k.clone()))) + } + } + }; - let kts: HashMap> = - outer_join( - |l| Ok(l.clone()), - |r| Ok(r.clone()), - combine, - kts_l, - kts_r, - ); + let kts: HashMap> = outer_join( + |l| Ok(l.clone()), + |r| Ok(r.clone()), + combine, + kts_l, + kts_r, + ); Ok(tck_record_type( ctx, @@ -684,35 +676,30 @@ fn type_last_layer( // records of records when merging. fn combine_record_types( ctx: &TypecheckContext, - kts_l: &HashMap, - kts_r: &HashMap, - ) -> Result { + kts_l: &HashMap, + kts_r: &HashMap, + ) -> Result { use crate::phase::normalize::intersection_with_key; // If the Label exists for both records and the values // are records themselves, then we hit the recursive case. // Otherwise we have a field collision. - let combine = - |k: &Label, - kts_l_inner: &TypedValue, - kts_r_inner: &TypedValue| - -> Result { - match (&*kts_l_inner.as_whnf(), &*kts_r_inner.as_whnf()) - { - ( - ValueF::RecordType(kvs_l_inner), - ValueF::RecordType(kvs_r_inner), - ) => combine_record_types( - ctx, - kvs_l_inner, - kvs_r_inner, - ), - (_, _) => Err(TypeError::new( - ctx, - FieldCollision(k.clone()), - )), + let combine = |k: &Label, + kts_l_inner: &Value, + kts_r_inner: &Value| + -> Result { + match (&*kts_l_inner.as_whnf(), &*kts_r_inner.as_whnf()) { + ( + ValueF::RecordType(kvs_l_inner), + ValueF::RecordType(kvs_r_inner), + ) => { + combine_record_types(ctx, kvs_l_inner, kvs_r_inner) } - }; + (_, _) => { + Err(TypeError::new(ctx, FieldCollision(k.clone()))) + } + } + }; let kts = intersection_with_key(combine, kts_l, kts_r); @@ -747,8 +734,8 @@ fn type_last_layer( k_l } else { return Err(mkerr(RecordTypeMismatch( - TypedValue::from_const(k_l), - TypedValue::from_const(k_r), + Value::from_const(k_l), + Value::from_const(k_r), l.clone(), r.clone(), ))); @@ -779,7 +766,7 @@ fn type_last_layer( // Ensure that the records combine without a type error // and if not output the final Const value. combine_record_types(ctx, kts_x, kts_y) - .and(Ok(RetTypeOnly(TypedValue::from_const(k)))) + .and(Ok(RetTypeOnly(Value::from_const(k)))) } BinOp(o @ ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { @@ -814,7 +801,7 @@ fn type_last_layer( ))); } - Ok(RetTypeOnly(TypedValue::from_const(Type))) + Ok(RetTypeOnly(Value::from_const(Type))) } BinOp(o, l, r) => { let t = builtin_to_type(match o { @@ -941,7 +928,7 @@ fn type_last_layer( }; } - Ok(RetTypeOnly(TypedValue::from_valuef_and_type( + Ok(RetTypeOnly(Value::from_valuef_and_type( ValueF::RecordType(new_kts), record_type.get_type()?.into_owned(), ))) @@ -952,15 +939,13 @@ fn type_last_layer( /// `type_of` is the same as `type_with` with an empty context, meaning that the /// expression must be closed (i.e. no free variables), otherwise type-checking /// will fail. -pub(crate) fn typecheck( - e: SubExpr, -) -> Result { +pub(crate) fn typecheck(e: SubExpr) -> Result { type_with(&TypecheckContext::new(), e) } pub(crate) fn typecheck_with( expr: SubExpr, ty: SubExpr, -) -> Result { +) -> Result { typecheck(expr.rewrap(ExprF::Annot(expr.clone(), ty))) } -- cgit v1.2.3 From 85cbed46aa6a5c76902576dcf2beb323bedb25b1 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 11:11:03 +0200 Subject: Tweak Ok/Err handling in typecheck --- dhall/src/phase/typecheck.rs | 285 +++++++++++++++++++------------------------ 1 file changed, 128 insertions(+), 157 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index e65881e..40017ee 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -286,14 +286,6 @@ pub(crate) fn builtin_to_type(b: Builtin) -> Result { type_with(&TypecheckContext::new(), SubExpr::from_builtin(b)) } -/// Intermediary return type -enum Ret { - /// Returns the contained value as is - RetWhole(Value), - /// Use the contained Value as the type of the input expression - RetTypeOnly(Value), -} - /// Type-check an expression and return the expression alongside its type if type-checking /// succeeded, or an error if type-checking failed. /// Some normalization is done while typechecking, so the returned expression might be partially @@ -304,7 +296,6 @@ fn type_with( ) -> Result { use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var}; - use Ret::*; Ok(match e.as_ref() { Lam(x, t, b) => { let tx = type_with(ctx, t.clone())?; @@ -341,21 +332,13 @@ fn type_with( )) } }, - _ => { + e => { // Typecheck recursively all subexpressions - let expr = - e.as_ref().traverse_ref_with_special_handling_of_binders( - |e| type_with(ctx, e.clone()), - |_, _| unreachable!(), - )?; - let ret = type_last_layer(ctx, &expr)?; - match ret { - RetTypeOnly(typ) => { - let expr = expr.map_ref(|typed| typed.to_value()); - Value::from_valuef_and_type(ValueF::PartialExpr(expr), typ) - } - RetWhole(tt) => tt, - } + let expr = e.traverse_ref_with_special_handling_of_binders( + |e| type_with(ctx, e.clone()), + |_, _| unreachable!(), + )?; + type_last_layer(ctx, expr)? } }) } @@ -364,17 +347,25 @@ fn type_with( /// layer. fn type_last_layer( ctx: &TypecheckContext, - e: &ExprF, -) -> Result { + e: ExprF, +) -> Result { use crate::error::TypeMessage::*; use dhall_syntax::BinOp::*; use dhall_syntax::Builtin::*; use dhall_syntax::Const::Type; use dhall_syntax::ExprF::*; + let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg)); + + /// Intermediary return type + enum Ret { + /// Returns the contained value as is + RetWhole(Value), + /// Returns the input expression `e` with the contained value as its type + RetTypeOnly(Value), + } use Ret::*; - let mkerr = |msg: TypeMessage| TypeError::new(ctx, msg); - match e { + let ret = match &e { Import(_) => unreachable!( "There should remain no imports in a resolved expression" ), @@ -386,122 +377,113 @@ fn type_last_layer( let tf_borrow = tf.as_whnf(); let (x, tx, tb) = match &*tf_borrow { ValueF::Pi(x, tx, tb) => (x, tx, tb), - _ => return Err(mkerr(NotAFunction(f.clone()))), + _ => return mkerr(NotAFunction(f.clone())), }; if a.get_type()?.as_ref() != tx { - return Err(mkerr(TypeMismatch( - f.clone(), - tx.clone(), - a.clone(), - ))); + return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone())); } - Ok(RetTypeOnly(tb.subst_shift(&x.into(), a))) + RetTypeOnly(tb.subst_shift(&x.into(), a)) } Annot(x, t) => { if t != x.get_type()?.as_ref() { - return Err(mkerr(AnnotMismatch(x.clone(), t.clone()))); + return mkerr(AnnotMismatch(x.clone(), t.clone())); } - Ok(RetTypeOnly(x.get_type()?.into_owned())) + RetTypeOnly(x.get_type()?.into_owned()) } Assert(t) => { match &*t.as_whnf() { ValueF::Equivalence(x, y) if x == y => {} ValueF::Equivalence(x, y) => { - return Err(mkerr(AssertMismatch(x.clone(), y.clone()))) + return mkerr(AssertMismatch(x.clone(), y.clone())) } - _ => return Err(mkerr(AssertMustTakeEquivalence)), + _ => return mkerr(AssertMustTakeEquivalence), } - Ok(RetTypeOnly(t.clone())) + RetTypeOnly(t.clone()) } BoolIf(x, y, z) => { if x.get_type()?.as_ref() != &builtin_to_type(Bool)? { - return Err(mkerr(InvalidPredicate(x.clone()))); + return mkerr(InvalidPredicate(x.clone())); } if y.get_type()?.get_type()?.as_const() != Some(Type) { - return Err(mkerr(IfBranchMustBeTerm(true, y.clone()))); + return mkerr(IfBranchMustBeTerm(true, y.clone())); } if z.get_type()?.get_type()?.as_const() != Some(Type) { - return Err(mkerr(IfBranchMustBeTerm(false, z.clone()))); + return mkerr(IfBranchMustBeTerm(false, z.clone())); } if y.get_type()? != z.get_type()? { - return Err(mkerr(IfBranchMismatch(y.clone(), z.clone()))); + return mkerr(IfBranchMismatch(y.clone(), z.clone())); } - Ok(RetTypeOnly(y.get_type()?.into_owned())) + RetTypeOnly(y.get_type()?.into_owned()) } EmptyListLit(t) => { match &*t.as_whnf() { ValueF::AppliedBuiltin(dhall_syntax::Builtin::List, args) if args.len() == 1 => {} - _ => { - return Err(TypeError::new(ctx, InvalidListType(t.clone()))) - } + _ => return mkerr(InvalidListType(t.clone())), } - Ok(RetTypeOnly(t.clone())) + RetTypeOnly(t.clone()) } NEListLit(xs) => { let mut iter = xs.iter().enumerate(); let (_, x) = iter.next().unwrap(); for (i, y) in iter { if x.get_type()? != y.get_type()? { - return Err(mkerr(InvalidListElement( + return mkerr(InvalidListElement( i, x.get_type()?.into_owned(), y.clone(), - ))); + )); } } let t = x.get_type()?; if t.get_type()?.as_const() != Some(Type) { - return Err(TypeError::new( - ctx, - InvalidListType(t.into_owned()), - )); + return mkerr(InvalidListType(t.into_owned())); } - Ok(RetTypeOnly(Value::from_valuef_and_type( + RetTypeOnly(Value::from_valuef_and_type( ValueF::from_builtin(dhall_syntax::Builtin::List) .app_value(t.to_value()), Value::from_const(Type), - ))) + )) } SomeLit(x) => { let t = x.get_type()?.into_owned(); if t.get_type()?.as_const() != Some(Type) { - return Err(TypeError::new(ctx, InvalidOptionalType(t))); + return mkerr(InvalidOptionalType(t)); } - Ok(RetTypeOnly(Value::from_valuef_and_type( + RetTypeOnly(Value::from_valuef_and_type( ValueF::from_builtin(dhall_syntax::Builtin::Optional) .app_value(t.to_value()), Value::from_const(Type), - ))) + )) } - RecordType(kts) => Ok(RetWhole(tck_record_type( + RecordType(kts) => RetWhole(tck_record_type( ctx, kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), - )?)), - UnionType(kts) => Ok(RetWhole(tck_union_type( + )?), + UnionType(kts) => RetWhole(tck_union_type( ctx, kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), - )?)), - RecordLit(kvs) => Ok(RetTypeOnly(tck_record_type( + )?), + RecordLit(kvs) => RetTypeOnly(tck_record_type( ctx, kvs.iter() .map(|(x, v)| Ok((x.clone(), v.get_type()?.into_owned()))), - )?)), + )?), Field(r, x) => { match &*r.get_type()?.as_whnf() { ValueF::RecordType(kts) => match kts.get(&x) { Some(tth) => { - Ok(RetTypeOnly(tth.clone())) + RetTypeOnly(tth.clone()) }, - None => Err(mkerr(MissingRecordField(x.clone(), - r.clone()))), + None => return mkerr(MissingRecordField(x.clone(), + r.clone())), }, // TODO: branch here only when r.get_type() is a Const _ => { @@ -509,56 +491,56 @@ fn type_last_layer( ValueF::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > Some(Some(t)) => { - Ok(RetTypeOnly( + RetTypeOnly( tck_pi_type( ctx, "_".into(), t.clone(), r.under_binder(Label::from("_")), )? - )) + ) }, Some(None) => { - Ok(RetTypeOnly(r.clone())) + RetTypeOnly(r.clone()) }, None => { - Err(mkerr(MissingUnionField( + return mkerr(MissingUnionField( x.clone(), r.clone(), - ))) + )) }, }, _ => { - Err(mkerr(NotARecord( + return mkerr(NotARecord( x.clone(), r.clone() - ))) + )) }, } } - // _ => Err(mkerr(NotARecord( + // _ => mkerr(NotARecord( // x, // r?, - // ))), + // )), } } - Const(c) => Ok(RetWhole(Value::from_const(*c))), - Builtin(b) => Ok(RetTypeOnly(type_with(ctx, rc(type_of_builtin(*b)))?)), - BoolLit(_) => Ok(RetTypeOnly(builtin_to_type(Bool)?)), - NaturalLit(_) => Ok(RetTypeOnly(builtin_to_type(Natural)?)), - IntegerLit(_) => Ok(RetTypeOnly(builtin_to_type(Integer)?)), - DoubleLit(_) => Ok(RetTypeOnly(builtin_to_type(Double)?)), + Const(c) => RetWhole(Value::from_const(*c)), + Builtin(b) => RetTypeOnly(type_with(ctx, rc(type_of_builtin(*b)))?), + BoolLit(_) => RetTypeOnly(builtin_to_type(Bool)?), + NaturalLit(_) => RetTypeOnly(builtin_to_type(Natural)?), + IntegerLit(_) => RetTypeOnly(builtin_to_type(Integer)?), + DoubleLit(_) => RetTypeOnly(builtin_to_type(Double)?), TextLit(interpolated) => { let text_type = builtin_to_type(Text)?; for contents in interpolated.iter() { use InterpolatedTextContents::Expr; if let Expr(x) = contents { if x.get_type()?.as_ref() != &text_type { - return Err(mkerr(InvalidTextInterpolation(x.clone()))); + return mkerr(InvalidTextInterpolation(x.clone())); } } } - Ok(RetTypeOnly(text_type)) + RetTypeOnly(text_type) } BinOp(RightBiasedRecordMerge, l, r) => { use crate::phase::normalize::merge_maps; @@ -572,21 +554,21 @@ fn type_last_layer( // This is to disallow expression such as: // "{ x = Text } // { y = 1 }" if l_kind != r_kind { - return Err(mkerr(RecordMismatch(l.clone(), r.clone()))); + return mkerr(RecordMismatch(l.clone(), r.clone())); } // Extract the LHS record type let l_type_borrow = l_type.as_whnf(); let kts_x = match &*l_type_borrow { ValueF::RecordType(kts) => kts, - _ => return Err(mkerr(MustCombineRecord(l.clone()))), + _ => return mkerr(MustCombineRecord(l.clone())), }; // Extract the RHS record type let r_type_borrow = r_type.as_whnf(); let kts_y = match &*r_type_borrow { ValueF::RecordType(kts) => kts, - _ => return Err(mkerr(MustCombineRecord(r.clone()))), + _ => return mkerr(MustCombineRecord(r.clone())), }; // Union the two records, prefering @@ -594,10 +576,10 @@ fn type_last_layer( let kts = merge_maps(kts_x, kts_y, |_, r_t| r_t.clone()); // Construct the final record type from the union - Ok(RetTypeOnly(tck_record_type( + RetTypeOnly(tck_record_type( ctx, kts.into_iter().map(|(x, v)| Ok((x.clone(), v))), - )?)) + )?) } BinOp(RecursiveRecordMerge, l, r) => { // A recursive function to dig down into @@ -637,10 +619,10 @@ fn type_last_layer( kts_r, ); - Ok(tck_record_type( + tck_record_type( ctx, kts.into_iter().map(|(x, v)| v.map(|r| (x.clone(), r))), - )?) + ) }; let l_type = l.get_type()?; @@ -652,24 +634,25 @@ fn type_last_layer( // This is to disallow expression such as: // "{ x = Text } // { y = 1 }" if l_kind != r_kind { - return Err(mkerr(RecordMismatch(l.clone(), r.clone()))); + return mkerr(RecordMismatch(l.clone(), r.clone())); } // Extract the LHS record type let l_type_borrow = l_type.as_whnf(); let kts_x = match &*l_type_borrow { ValueF::RecordType(kts) => kts, - _ => return Err(mkerr(MustCombineRecord(l.clone()))), + _ => return mkerr(MustCombineRecord(l.clone())), }; // Extract the RHS record type let r_type_borrow = r_type.as_whnf(); let kts_y = match &*r_type_borrow { ValueF::RecordType(kts) => kts, - _ => return Err(mkerr(MustCombineRecord(r.clone()))), + _ => return mkerr(MustCombineRecord(r.clone())), }; - combine_record_types(ctx, kts_x, kts_y).map(|r| RetTypeOnly(r)) + let r = combine_record_types(ctx, kts_x, kts_y)?; + RetTypeOnly(r) } BinOp(RecursiveRecordTypeMerge, l, r) => { // A recursive function to dig down into @@ -703,19 +686,17 @@ fn type_last_layer( let kts = intersection_with_key(combine, kts_l, kts_r); - Ok(tck_record_type( + tck_record_type( ctx, kts.into_iter().map(|(x, v)| v.map(|r| (x.clone(), r))), - )?) + ) }; // Extract the Const of the LHS let k_l = match l.get_type()?.as_const() { Some(k) => k, _ => { - return Err(mkerr(RecordTypeMergeRequiresRecordType( - l.clone(), - ))) + return mkerr(RecordTypeMergeRequiresRecordType(l.clone())) } }; @@ -723,9 +704,7 @@ fn type_last_layer( let k_r = match r.get_type()?.as_const() { Some(k) => k, _ => { - return Err(mkerr(RecordTypeMergeRequiresRecordType( - r.clone(), - ))) + return mkerr(RecordTypeMergeRequiresRecordType(r.clone())) } }; @@ -733,12 +712,12 @@ fn type_last_layer( let k = if k_l == k_r { k_l } else { - return Err(mkerr(RecordTypeMismatch( + return mkerr(RecordTypeMismatch( Value::from_const(k_l), Value::from_const(k_r), l.clone(), r.clone(), - ))); + )); }; // Extract the LHS record type @@ -746,9 +725,7 @@ fn type_last_layer( let kts_x = match &*borrow_l { ValueF::RecordType(kts) => kts, _ => { - return Err(mkerr(RecordTypeMergeRequiresRecordType( - l.clone(), - ))) + return mkerr(RecordTypeMergeRequiresRecordType(l.clone())) } }; @@ -757,51 +734,40 @@ fn type_last_layer( let kts_y = match &*borrow_r { ValueF::RecordType(kts) => kts, _ => { - return Err(mkerr(RecordTypeMergeRequiresRecordType( - r.clone(), - ))) + return mkerr(RecordTypeMergeRequiresRecordType(r.clone())) } }; // Ensure that the records combine without a type error - // and if not output the final Const value. - combine_record_types(ctx, kts_x, kts_y) - .and(Ok(RetTypeOnly(Value::from_const(k)))) + combine_record_types(ctx, kts_x, kts_y)?; + + RetTypeOnly(Value::from_const(k)) } BinOp(o @ ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { ValueF::AppliedBuiltin(List, _) => {} - _ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone()))), + _ => return mkerr(BinOpTypeMismatch(*o, l.clone())), } if l.get_type()? != r.get_type()? { - return Err(mkerr(BinOpTypeMismatch(*o, r.clone()))); + return mkerr(BinOpTypeMismatch(*o, r.clone())); } - Ok(RetTypeOnly(l.get_type()?.into_owned())) + RetTypeOnly(l.get_type()?.into_owned()) } BinOp(Equivalence, l, r) => { if l.get_type()?.get_type()?.as_const() != Some(Type) { - return Err(mkerr(EquivalenceArgumentMustBeTerm( - true, - l.clone(), - ))); + return mkerr(EquivalenceArgumentMustBeTerm(true, l.clone())); } if r.get_type()?.get_type()?.as_const() != Some(Type) { - return Err(mkerr(EquivalenceArgumentMustBeTerm( - false, - r.clone(), - ))); + return mkerr(EquivalenceArgumentMustBeTerm(false, r.clone())); } if l.get_type()? != r.get_type()? { - return Err(mkerr(EquivalenceTypeMismatch( - r.clone(), - l.clone(), - ))); + return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone())); } - Ok(RetTypeOnly(Value::from_const(Type))) + RetTypeOnly(Value::from_const(Type)) } BinOp(o, l, r) => { let t = builtin_to_type(match o { @@ -821,28 +787,28 @@ fn type_last_layer( })?; if l.get_type()?.as_ref() != &t { - return Err(mkerr(BinOpTypeMismatch(*o, l.clone()))); + return mkerr(BinOpTypeMismatch(*o, l.clone())); } if r.get_type()?.as_ref() != &t { - return Err(mkerr(BinOpTypeMismatch(*o, r.clone()))); + return mkerr(BinOpTypeMismatch(*o, r.clone())); } - Ok(RetTypeOnly(t)) + RetTypeOnly(t) } Merge(record, union, type_annot) => { let record_type = record.get_type()?; let record_borrow = record_type.as_whnf(); let handlers = match &*record_borrow { ValueF::RecordType(kts) => kts, - _ => return Err(mkerr(Merge1ArgMustBeRecord(record.clone()))), + _ => return mkerr(Merge1ArgMustBeRecord(record.clone())), }; let union_type = union.get_type()?; let union_borrow = union_type.as_whnf(); let variants = match &*union_borrow { ValueF::UnionType(kts) => kts, - _ => return Err(mkerr(Merge2ArgMustBeUnion(union.clone()))), + _ => return mkerr(Merge2ArgMustBeUnion(union.clone())), }; let mut inferred_type = None; @@ -855,61 +821,59 @@ fn type_last_layer( let (x, tx, tb) = match &*handler_type_borrow { ValueF::Pi(x, tx, tb) => (x, tx, tb), _ => { - return Err(mkerr(NotAFunction( + return mkerr(NotAFunction( handler_type.clone(), - ))) + )) } }; if variant_type != tx { - return Err(mkerr(TypeMismatch( + return mkerr(TypeMismatch( handler_type.clone(), tx.clone(), variant_type.clone(), - ))); + )); } // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`. match tb.over_binder(x) { Some(x) => x, - None => return Err(mkerr( + None => return mkerr( MergeHandlerReturnTypeMustNotBeDependent, - )), + ), } } // Union alternative without type Some(None) => handler_type.clone(), None => { - return Err(mkerr(MergeHandlerMissingVariant( - x.clone(), - ))) + return mkerr(MergeHandlerMissingVariant(x.clone())) } }; match &inferred_type { None => inferred_type = Some(handler_return_type), Some(t) => { if t != &handler_return_type { - return Err(mkerr(MergeHandlerTypeMismatch)); + return mkerr(MergeHandlerTypeMismatch); } } } } for x in variants.keys() { if !handlers.contains_key(x) { - return Err(mkerr(MergeVariantMissingHandler(x.clone()))); + return mkerr(MergeVariantMissingHandler(x.clone())); } } match (inferred_type, type_annot) { (Some(ref t1), Some(t2)) => { if t1 != t2 { - return Err(mkerr(MergeAnnotMismatch)); + return mkerr(MergeAnnotMismatch); } - Ok(RetTypeOnly(t2.clone())) + RetTypeOnly(t2.clone()) } - (Some(t), None) => Ok(RetTypeOnly(t)), - (None, Some(t)) => Ok(RetTypeOnly(t.clone())), - (None, None) => Err(mkerr(MergeEmptyNeedsAnnotation)), + (Some(t), None) => RetTypeOnly(t), + (None, Some(t)) => RetTypeOnly(t.clone()), + (None, None) => return mkerr(MergeEmptyNeedsAnnotation), } } Projection(record, labels) => { @@ -917,23 +881,30 @@ fn type_last_layer( let record_borrow = record_type.as_whnf(); let kts = match &*record_borrow { ValueF::RecordType(kts) => kts, - _ => return Err(mkerr(ProjectionMustBeRecord)), + _ => return mkerr(ProjectionMustBeRecord), }; let mut new_kts = HashMap::new(); for l in labels { match kts.get(l) { - None => return Err(mkerr(ProjectionMissingEntry)), + None => return mkerr(ProjectionMissingEntry), Some(t) => new_kts.insert(l.clone(), t.clone()), }; } - Ok(RetTypeOnly(Value::from_valuef_and_type( + RetTypeOnly(Value::from_valuef_and_type( ValueF::RecordType(new_kts), record_type.get_type()?.into_owned(), - ))) + )) } - } + }; + + Ok(match ret { + RetTypeOnly(typ) => { + Value::from_valuef_and_type(ValueF::PartialExpr(e), typ) + } + RetWhole(v) => v, + }) } /// `type_of` is the same as `type_with` with an empty context, meaning that the -- cgit v1.2.3 From f6d30f42bd3a6762b1f53b34a249c877260951bb Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 11:52:46 +0200 Subject: Reuse work to avoid complicated recursion in record merging --- dhall/src/phase/typecheck.rs | 121 +++++++++---------------------------------- 1 file changed, 25 insertions(+), 96 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 40017ee..77ef689 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -582,49 +582,6 @@ fn type_last_layer( )?) } BinOp(RecursiveRecordMerge, l, r) => { - // A recursive function to dig down into - // records of records when merging. - fn combine_record_types( - ctx: &TypecheckContext, - kts_l: &HashMap, - kts_r: &HashMap, - ) -> Result { - use crate::phase::normalize::outer_join; - - // If the Label exists for both records and the values - // are records themselves, then we hit the recursive case. - // Otherwise we have a field collision. - let combine = |k: &Label, - inner_l: &Value, - inner_r: &Value| - -> Result { - match (&*inner_l.as_whnf(), &*inner_r.as_whnf()) { - ( - ValueF::RecordType(inner_l_kvs), - ValueF::RecordType(inner_r_kvs), - ) => { - combine_record_types(ctx, inner_l_kvs, inner_r_kvs) - } - (_, _) => { - Err(TypeError::new(ctx, FieldCollision(k.clone()))) - } - } - }; - - let kts: HashMap> = outer_join( - |l| Ok(l.clone()), - |r| Ok(r.clone()), - combine, - kts_l, - kts_r, - ); - - tck_record_type( - ctx, - kts.into_iter().map(|(x, v)| v.map(|r| (x.clone(), r))), - ) - }; - let l_type = l.get_type()?; let l_kind = l_type.get_type()?; let r_type = r.get_type()?; @@ -637,60 +594,17 @@ fn type_last_layer( return mkerr(RecordMismatch(l.clone(), r.clone())); } - // Extract the LHS record type - let l_type_borrow = l_type.as_whnf(); - let kts_x = match &*l_type_borrow { - ValueF::RecordType(kts) => kts, - _ => return mkerr(MustCombineRecord(l.clone())), - }; - - // Extract the RHS record type - let r_type_borrow = r_type.as_whnf(); - let kts_y = match &*r_type_borrow { - ValueF::RecordType(kts) => kts, - _ => return mkerr(MustCombineRecord(r.clone())), - }; - - let r = combine_record_types(ctx, kts_x, kts_y)?; - RetTypeOnly(r) + RetTypeOnly(type_last_layer( + ctx, + ExprF::BinOp( + RecursiveRecordTypeMerge, + l_type.into_owned(), + r_type.into_owned(), + ), + )?) } BinOp(RecursiveRecordTypeMerge, l, r) => { - // A recursive function to dig down into - // records of records when merging. - fn combine_record_types( - ctx: &TypecheckContext, - kts_l: &HashMap, - kts_r: &HashMap, - ) -> Result { - use crate::phase::normalize::intersection_with_key; - - // If the Label exists for both records and the values - // are records themselves, then we hit the recursive case. - // Otherwise we have a field collision. - let combine = |k: &Label, - kts_l_inner: &Value, - kts_r_inner: &Value| - -> Result { - match (&*kts_l_inner.as_whnf(), &*kts_r_inner.as_whnf()) { - ( - ValueF::RecordType(kvs_l_inner), - ValueF::RecordType(kvs_r_inner), - ) => { - combine_record_types(ctx, kvs_l_inner, kvs_r_inner) - } - (_, _) => { - Err(TypeError::new(ctx, FieldCollision(k.clone()))) - } - } - }; - - let kts = intersection_with_key(combine, kts_l, kts_r); - - tck_record_type( - ctx, - kts.into_iter().map(|(x, v)| v.map(|r| (x.clone(), r))), - ) - }; + use crate::phase::normalize::intersection_with_key; // Extract the Const of the LHS let k_l = match l.get_type()?.as_const() { @@ -739,7 +653,22 @@ fn type_last_layer( }; // Ensure that the records combine without a type error - combine_record_types(ctx, kts_x, kts_y)?; + let kts = intersection_with_key( + // If the Label exists for both records, then we hit the recursive case. + |_: &Label, l: &Value, r: &Value| { + type_last_layer( + ctx, + ExprF::BinOp( + RecursiveRecordTypeMerge, + l.clone(), + r.clone(), + ), + ) + }, + kts_x, + kts_y, + ); + tck_record_type(ctx, kts.into_iter().map(|(x, v)| Ok((x, v?))))?; RetTypeOnly(Value::from_const(k)) } -- cgit v1.2.3 From 7dd22d6f55e3885835c7fe58b876f26937d0e7a4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 12:02:54 +0200 Subject: Standardize records of mixed kinds --- dhall/src/phase/typecheck.rs | 68 +++++++++++--------------------------------- 1 file changed, 17 insertions(+), 51 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 77ef689..8a3b43a 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -1,3 +1,4 @@ +use std::cmp::max; use std::collections::HashMap; use dhall_syntax::{ @@ -50,15 +51,16 @@ fn tck_record_type( use crate::error::TypeMessage::*; use std::collections::hash_map::Entry; let mut new_kts = HashMap::new(); - // Check that all types are the same const - let mut k = None; + // An empty record type has type Type + let mut k = Const::Type; for e in kts { let (x, t) = e?; - match (k, t.get_type()?.as_const()) { - (None, Some(k2)) => k = Some(k2), - (Some(k1), Some(k2)) if k1 == k2 => {} - _ => return Err(TypeError::new(ctx, InvalidFieldType(x, t))), + // Construct the union of the contained `Const`s + match t.get_type()?.as_const() { + Some(k2) => k = max(k, k2), + None => return Err(TypeError::new(ctx, InvalidFieldType(x, t))), } + // Check for duplicated entries let entry = new_kts.entry(x); match &entry { Entry::Occupied(_) => { @@ -67,8 +69,6 @@ fn tck_record_type( Entry::Vacant(_) => entry.or_insert_with(|| t), }; } - // An empty record type has type Type - let k = k.unwrap_or(Const::Type); Ok(Value::from_valuef_and_type( ValueF::RecordType(new_kts), @@ -122,7 +122,6 @@ where } fn function_check(a: Const, b: Const) -> Const { - use std::cmp::max; if b == Const::Type { Const::Type } else { @@ -546,16 +545,7 @@ fn type_last_layer( use crate::phase::normalize::merge_maps; let l_type = l.get_type()?; - let l_kind = l_type.get_type()?; let r_type = r.get_type()?; - let r_kind = r_type.get_type()?; - - // Check the equality of kinds. - // This is to disallow expression such as: - // "{ x = Text } // { y = 1 }" - if l_kind != r_kind { - return mkerr(RecordMismatch(l.clone(), r.clone())); - } // Extract the LHS record type let l_type_borrow = l_type.as_whnf(); @@ -581,28 +571,14 @@ fn type_last_layer( kts.into_iter().map(|(x, v)| Ok((x.clone(), v))), )?) } - BinOp(RecursiveRecordMerge, l, r) => { - let l_type = l.get_type()?; - let l_kind = l_type.get_type()?; - let r_type = r.get_type()?; - let r_kind = r_type.get_type()?; - - // Check the equality of kinds. - // This is to disallow expression such as: - // "{ x = Text } // { y = 1 }" - if l_kind != r_kind { - return mkerr(RecordMismatch(l.clone(), r.clone())); - } - - RetTypeOnly(type_last_layer( - ctx, - ExprF::BinOp( - RecursiveRecordTypeMerge, - l_type.into_owned(), - r_type.into_owned(), - ), - )?) - } + BinOp(RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer( + ctx, + ExprF::BinOp( + RecursiveRecordTypeMerge, + l.get_type()?.into_owned(), + r.get_type()?.into_owned(), + ), + )?), BinOp(RecursiveRecordTypeMerge, l, r) => { use crate::phase::normalize::intersection_with_key; @@ -622,17 +598,7 @@ fn type_last_layer( } }; - // Const values must match for the Records - let k = if k_l == k_r { - k_l - } else { - return mkerr(RecordTypeMismatch( - Value::from_const(k_l), - Value::from_const(k_r), - l.clone(), - r.clone(), - )); - }; + let k = max(k_l, k_r); // Extract the LHS record type let borrow_l = l.as_whnf(); -- cgit v1.2.3 From caf36246a517b884d7cfcf7c31e1b5d8fce60dfa Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 13:49:13 +0200 Subject: Cleanup --- dhall/src/phase/typecheck.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 8a3b43a..c47eb78 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -300,7 +300,7 @@ fn type_with( let tx = type_with(ctx, t.clone())?; let ctx2 = ctx.insert_type(x, tx.clone()); let b = type_with(&ctx2, b.clone())?; - let v = ValueF::Lam(x.clone().into(), tx.clone(), b.to_value()); + let v = ValueF::Lam(x.clone().into(), tx.clone(), b.clone()); let tb = b.get_type()?.into_owned(); let t = tck_pi_type(ctx, x.clone(), tx, tb)?; Value::from_valuef_and_type(v, t) @@ -446,7 +446,7 @@ fn type_last_layer( RetTypeOnly(Value::from_valuef_and_type( ValueF::from_builtin(dhall_syntax::Builtin::List) - .app_value(t.to_value()), + .app_value(t.into_owned()), Value::from_const(Type), )) } @@ -458,7 +458,7 @@ fn type_last_layer( RetTypeOnly(Value::from_valuef_and_type( ValueF::from_builtin(dhall_syntax::Builtin::Optional) - .app_value(t.to_value()), + .app_value(t), Value::from_const(Type), )) } -- cgit v1.2.3