From a506632b27b287d1bf898e2f77ae09a56902474c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 17:08:01 +0200 Subject: Naming tweaks --- dhall/src/phase/typecheck.rs | 5 ++--- 1 file changed, 2 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 1ea87d1..440d694 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -457,7 +457,7 @@ fn type_last_layer( RetTypeOnly(Value::from_valuef_and_type( ValueF::from_builtin(dhall_syntax::Builtin::List) - .app_value(t.into_owned()), + .app(t.into_owned()), Value::from_const(Type), )) } @@ -468,8 +468,7 @@ fn type_last_layer( } RetTypeOnly(Value::from_valuef_and_type( - ValueF::from_builtin(dhall_syntax::Builtin::Optional) - .app_value(t), + ValueF::from_builtin(dhall_syntax::Builtin::Optional).app(t), Value::from_const(Type), )) } -- cgit v1.2.3 From 4f1f37cfc115510500e83d2dfbfa8ed7ddeae74a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 18:03:59 +0200 Subject: Introduce a new enum to store either a Value or a ValueF --- dhall/src/phase/typecheck.rs | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 440d694..996c26c 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -455,11 +455,11 @@ fn type_last_layer( return mkerr(InvalidListType(t.into_owned())); } - RetTypeOnly(Value::from_valuef_and_type( + RetTypeOnly( ValueF::from_builtin(dhall_syntax::Builtin::List) - .app(t.into_owned()), - Value::from_const(Type), - )) + .app(t.into_owned()) + .into_value_simple_type(), + ) } SomeLit(x) => { let t = x.get_type()?.into_owned(); @@ -467,10 +467,11 @@ fn type_last_layer( return mkerr(InvalidOptionalType(t)); } - RetTypeOnly(Value::from_valuef_and_type( - ValueF::from_builtin(dhall_syntax::Builtin::Optional).app(t), - Value::from_const(Type), - )) + RetTypeOnly( + Value::from_builtin(dhall_syntax::Builtin::Optional) + .app(t) + .into_value_simple_type(), + ) } RecordType(kts) => RetWhole(tck_record_type( ctx, -- cgit v1.2.3 From c157df5e66fb80ff6184cb3934e5b0883f0fdbf0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 18:11:05 +0200 Subject: No need for Cow in return type of get_type --- dhall/src/phase/typecheck.rs | 39 +++++++++++++++++++-------------------- 1 file changed, 19 insertions(+), 20 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 996c26c..4abc314 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -31,7 +31,7 @@ fn tck_pi_type( _ => { return Err(TypeError::new( &ctx2, - InvalidOutputType(te.get_type()?.into_owned()), + InvalidOutputType(te.get_type()?), )) } }; @@ -312,7 +312,7 @@ fn type_with( 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.clone()); - let tb = b.get_type()?.into_owned(); + let tb = b.get_type()?; let t = tck_pi_type(ctx, x.clone(), tx, tb)?; Value::from_valuef_and_type(v, t) } @@ -389,17 +389,17 @@ fn type_last_layer( ValueF::Pi(x, tx, tb) => (x, tx, tb), _ => return mkerr(NotAFunction(f.clone())), }; - if a.get_type()?.as_ref() != tx { + if &a.get_type()? != tx { return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone())); } RetTypeOnly(tb.subst_shift(&x.into(), a)) } Annot(x, t) => { - if t != x.get_type()?.as_ref() { + if &x.get_type()? != t { return mkerr(AnnotMismatch(x.clone(), t.clone())); } - RetTypeOnly(x.get_type()?.into_owned()) + RetTypeOnly(x.get_type()?) } Assert(t) => { match &*t.as_whnf() { @@ -412,7 +412,7 @@ fn type_last_layer( RetTypeOnly(t.clone()) } BoolIf(x, y, z) => { - if x.get_type()?.as_ref() != &builtin_to_value(Bool) { + if &*x.get_type()?.as_whnf() != &ValueF::from_builtin(Bool) { return mkerr(InvalidPredicate(x.clone())); } @@ -428,7 +428,7 @@ fn type_last_layer( return mkerr(IfBranchMismatch(y.clone(), z.clone())); } - RetTypeOnly(y.get_type()?.into_owned()) + RetTypeOnly(y.get_type()?) } EmptyListLit(t) => { match &*t.as_whnf() { @@ -445,24 +445,24 @@ fn type_last_layer( if x.get_type()? != y.get_type()? { return mkerr(InvalidListElement( i, - x.get_type()?.into_owned(), + x.get_type()?, y.clone(), )); } } let t = x.get_type()?; if t.get_type()?.as_const() != Some(Type) { - return mkerr(InvalidListType(t.into_owned())); + return mkerr(InvalidListType(t)); } RetTypeOnly( ValueF::from_builtin(dhall_syntax::Builtin::List) - .app(t.into_owned()) + .app(t) .into_value_simple_type(), ) } SomeLit(x) => { - let t = x.get_type()?.into_owned(); + let t = x.get_type()?; if t.get_type()?.as_const() != Some(Type) { return mkerr(InvalidOptionalType(t)); } @@ -483,8 +483,7 @@ fn type_last_layer( )?), RecordLit(kvs) => RetTypeOnly(tck_record_type( ctx, - kvs.iter() - .map(|(x, v)| Ok((x.clone(), v.get_type()?.into_owned()))), + kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))), )?), Field(r, x) => { match &*r.get_type()?.as_whnf() { @@ -545,7 +544,7 @@ fn type_last_layer( for contents in interpolated.iter() { use InterpolatedTextContents::Expr; if let Expr(x) = contents { - if x.get_type()?.as_ref() != &text_type { + if x.get_type()? != text_type { return mkerr(InvalidTextInterpolation(x.clone())); } } @@ -586,8 +585,8 @@ fn type_last_layer( ctx, ExprF::BinOp( RecursiveRecordTypeMerge, - l.get_type()?.into_owned(), - r.get_type()?.into_owned(), + l.get_type()?, + r.get_type()?, ), )?), BinOp(RecursiveRecordTypeMerge, l, r) => { @@ -659,7 +658,7 @@ fn type_last_layer( return mkerr(BinOpTypeMismatch(*o, r.clone())); } - RetTypeOnly(l.get_type()?.into_owned()) + RetTypeOnly(l.get_type()?) } BinOp(Equivalence, l, r) => { if l.get_type()?.get_type()?.as_const() != Some(Type) { @@ -692,11 +691,11 @@ fn type_last_layer( Equivalence => unreachable!(), }); - if l.get_type()?.as_ref() != &t { + if l.get_type()? != t { return mkerr(BinOpTypeMismatch(*o, l.clone())); } - if r.get_type()?.as_ref() != &t { + if r.get_type()? != t { return mkerr(BinOpTypeMismatch(*o, r.clone())); } @@ -800,7 +799,7 @@ fn type_last_layer( RetTypeOnly(Value::from_valuef_and_type( ValueF::RecordType(new_kts), - record_type.get_type()?.into_owned(), + record_type.get_type()?, )) } }; -- cgit v1.2.3 From ec349d42703a8a31715cf97b44845ba3dd7a6805 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 22:20:59 +0200 Subject: Propagate type information in Value::app() --- dhall/src/phase/typecheck.rs | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 4abc314..abe05a3 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -455,11 +455,7 @@ fn type_last_layer( return mkerr(InvalidListType(t)); } - RetTypeOnly( - ValueF::from_builtin(dhall_syntax::Builtin::List) - .app(t) - .into_value_simple_type(), - ) + RetTypeOnly(Value::from_builtin(dhall_syntax::Builtin::List).app(t)) } SomeLit(x) => { let t = x.get_type()?; @@ -468,9 +464,7 @@ fn type_last_layer( } RetTypeOnly( - Value::from_builtin(dhall_syntax::Builtin::Optional) - .app(t) - .into_value_simple_type(), + Value::from_builtin(dhall_syntax::Builtin::Optional).app(t), ) } RecordType(kts) => RetWhole(tck_record_type( -- cgit v1.2.3 From d9e3bcca9b4350cbc1db2545d7ed28dde4e12be4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 23 Aug 2019 18:34:43 +0200 Subject: Keep type information after RecursiveRecordTypeMerge --- dhall/src/phase/typecheck.rs | 37 ++++++++++--------------------------- 1 file changed, 10 insertions(+), 27 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index abe05a3..363d733 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -567,7 +567,9 @@ fn type_last_layer( // 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| { + Ok(r_t.clone()) + })?; // Construct the final record type from the union RetTypeOnly(tck_record_type( @@ -584,25 +586,7 @@ fn type_last_layer( ), )?), BinOp(RecursiveRecordTypeMerge, l, r) => { - use crate::phase::normalize::intersection_with_key; - - // Extract the Const of the LHS - let k_l = match l.get_type()?.as_const() { - Some(k) => k, - _ => { - return mkerr(RecordTypeMergeRequiresRecordType(l.clone())) - } - }; - - // Extract the Const of the RHS - let k_r = match r.get_type()?.as_const() { - Some(k) => k, - _ => { - return mkerr(RecordTypeMergeRequiresRecordType(r.clone())) - } - }; - - let k = max(k_l, k_r); + use crate::phase::normalize::merge_maps; // Extract the LHS record type let borrow_l = l.as_whnf(); @@ -623,9 +607,11 @@ fn type_last_layer( }; // Ensure that the records combine without a type error - let kts = intersection_with_key( + let kts = merge_maps( + kts_x, + kts_y, // If the Label exists for both records, then we hit the recursive case. - |_: &Label, l: &Value, r: &Value| { + |l: &Value, r: &Value| { type_last_layer( ctx, ExprF::BinOp( @@ -635,12 +621,9 @@ fn type_last_layer( ), ) }, - kts_x, - kts_y, - ); - tck_record_type(ctx, kts.into_iter().map(|(x, v)| Ok((x, v?))))?; + )?; - RetTypeOnly(Value::from_const(k)) + RetWhole(tck_record_type(ctx, kts.into_iter().map(Ok))?) } BinOp(o @ ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { -- cgit v1.2.3 From d5bdd48d4c34b4e213e3e2431936c160e4320a80 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 23 Aug 2019 18:53:46 +0200 Subject: Clarify which syntax elements are completely handled in the tck phase --- dhall/src/phase/typecheck.rs | 9 ++++++--- 1 file changed, 6 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 363d733..0268b80 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -291,7 +291,7 @@ fn type_of_builtin(b: Builtin) -> Expr { pub(crate) fn builtin_to_value(b: Builtin) -> Value { let ctx = TypecheckContext::new(); Value::from_valuef_and_type( - ValueF::PartialExpr(ExprF::Builtin(b)), + ValueF::from_builtin(b), type_with(&ctx, rc(type_of_builtin(b))).unwrap(), ) } @@ -399,7 +399,7 @@ fn type_last_layer( if &x.get_type()? != t { return mkerr(AnnotMismatch(x.clone(), t.clone())); } - RetTypeOnly(x.get_type()?) + RetWhole(x.clone()) } Assert(t) => { match &*t.as_whnf() { @@ -649,7 +649,10 @@ fn type_last_layer( return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone())); } - RetTypeOnly(Value::from_const(Type)) + RetWhole(Value::from_valuef_and_type( + ValueF::Equivalence(l.clone(), r.clone()), + Value::from_const(Type), + )) } BinOp(o, l, r) => { let t = builtin_to_value(match o { -- cgit v1.2.3 From 98399997cf289d802fbed674558665547cf73d59 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 16:09:55 +0200 Subject: Keep type information through normalization --- dhall/src/phase/typecheck.rs | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 0268b80..270191a 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -307,14 +307,15 @@ fn type_with( use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var}; Ok(match e.as_ref() { - Lam(x, t, b) => { - 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.clone()); - let tb = b.get_type()?; - let t = tck_pi_type(ctx, x.clone(), tx, tb)?; - Value::from_valuef_and_type(v, t) + Lam(var, annot, body) => { + let annot = type_with(ctx, annot.clone())?; + let ctx2 = ctx.insert_type(var, annot.clone()); + let body = type_with(&ctx2, body.clone())?; + let body_type = body.get_type()?; + Value::from_valuef_and_type( + ValueF::Lam(var.clone().into(), annot.clone(), body), + tck_pi_type(ctx, var.clone(), annot, body_type)?, + ) } Pi(x, ta, tb) => { let ta = type_with(ctx, ta.clone())?; @@ -567,7 +568,7 @@ fn type_last_layer( // Union the two records, prefering // the values found in the RHS. - let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, r_t| { + let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, _, r_t| { Ok(r_t.clone()) })?; @@ -611,7 +612,7 @@ fn type_last_layer( kts_x, kts_y, // If the Label exists for both records, then we hit the recursive case. - |l: &Value, r: &Value| { + |_, l: &Value, r: &Value| { type_last_layer( ctx, ExprF::BinOp( -- cgit v1.2.3 From f9ec2cdf2803ed92fa404db989b786fc1dfac12e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 17:07:59 +0200 Subject: Enforce type information almost everywhere --- dhall/src/phase/typecheck.rs | 21 ++++++++------------- 1 file changed, 8 insertions(+), 13 deletions(-) (limited to 'dhall/src/phase/typecheck.rs') diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 270191a..ef2018a 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -129,21 +129,16 @@ fn function_check(a: Const, b: Const) -> Const { } } -fn type_of_const(c: Const) -> Result { - match c { - Const::Type => Ok(const_to_value(Const::Kind)), - Const::Kind => Ok(const_to_value(Const::Sort)), - Const::Sort => { - Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) - } - } -} - pub(crate) fn const_to_value(c: Const) -> Value { let v = ValueF::Const(c); - match type_of_const(c) { - Ok(t) => Value::from_valuef_and_type(v, t), - Err(_) => Value::from_valuef_untyped(v), + match c { + Const::Type => { + Value::from_valuef_and_type(v, const_to_value(Const::Kind)) + } + Const::Kind => { + Value::from_valuef_and_type(v, const_to_value(Const::Sort)) + } + Const::Sort => Value::const_sort(), } } -- cgit v1.2.3