diff options
Diffstat (limited to '')
-rw-r--r-- | dhall/src/phase/typecheck.rs | 131 |
1 files changed, 53 insertions, 78 deletions
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 1ea87d1..ef2018a 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()?), )) } }; @@ -129,21 +129,16 @@ fn function_check(a: Const, b: Const) -> Const { } } -fn type_of_const(c: Const) -> Result<Value, TypeError> { - 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(), } } @@ -291,7 +286,7 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> { 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(), ) } @@ -307,14 +302,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()?.into_owned(); - 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())?; @@ -389,17 +385,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()) + RetWhole(x.clone()) } Assert(t) => { match &*t.as_whnf() { @@ -412,7 +408,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 +424,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,33 +441,27 @@ 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(Value::from_valuef_and_type( - ValueF::from_builtin(dhall_syntax::Builtin::List) - .app_value(t.into_owned()), - Value::from_const(Type), - )) + RetTypeOnly(Value::from_builtin(dhall_syntax::Builtin::List).app(t)) } 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)); } - RetTypeOnly(Value::from_valuef_and_type( - ValueF::from_builtin(dhall_syntax::Builtin::Optional) - .app_value(t), - Value::from_const(Type), - )) + RetTypeOnly( + Value::from_builtin(dhall_syntax::Builtin::Optional).app(t), + ) } RecordType(kts) => RetWhole(tck_record_type( ctx, @@ -483,8 +473,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 +534,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())); } } @@ -574,7 +563,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( @@ -586,30 +577,12 @@ 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) => { - 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(); @@ -630,9 +603,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( @@ -642,12 +617,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() { @@ -659,7 +631,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) { @@ -673,7 +645,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 { @@ -692,11 +667,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 +775,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()?, )) } }; |