diff options
Diffstat (limited to '')
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 487 |
1 files changed, 342 insertions, 145 deletions
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 1687185..1b64d28 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -1,5 +1,4 @@ #![allow(dead_code)] -#![allow(unused_variables)] #![allow(unreachable_code)] #![allow(unused_imports)] use std::borrow::Cow; @@ -68,6 +67,41 @@ impl TyEnv { } } +fn type_of_recordtype<'a>( + tys: impl Iterator<Item = Cow<'a, TyExpr>>, +) -> Result<Type, TypeError> { + // An empty record type has type Type + let mut k = Const::Type; + for t in tys { + match t.get_type()?.as_const() { + Some(c) => k = max(k, c), + None => return mkerr("InvalidFieldType"), + } + } + Ok(Value::from_const(k)) +} + +fn function_check(a: Const, b: Const) -> Const { + if b == Const::Type { + Const::Type + } else { + max(a, b) + } +} + +fn type_of_function(src: Type, tgt: Type) -> Result<Type, TypeError> { + let ks = match src.as_const() { + Some(k) => k, + _ => return Err(TypeError::new(TypeMessage::InvalidInputType(src))), + }; + let kt = match tgt.as_const() { + Some(k) => k, + _ => return Err(TypeError::new(TypeMessage::InvalidOutputType(tgt))), + }; + + Ok(Value::from_const(function_check(ks, kt))) +} + fn mkerr<T>(x: impl ToString) -> Result<T, TypeError> { Err(TypeError::new(TypeMessage::Custom(x.to_string()))) } @@ -76,7 +110,7 @@ fn type_one_layer( env: &TyEnv, kind: &ExprKind<TyExpr, Normalized>, ) -> Result<Type, TypeError> { - Ok(match &kind { + Ok(match kind { ExprKind::Import(..) => unreachable!( "There should remain no imports in a resolved expression" ), @@ -90,7 +124,9 @@ fn type_one_layer( ExprKind::Const(Const::Type) => const_to_value(Const::Kind), ExprKind::Const(Const::Kind) => const_to_value(Const::Sort), ExprKind::Builtin(b) => { - type_with(env, &type_of_builtin(*b))?.normalize_whnf(env.as_nzenv()) + let t_expr = type_of_builtin(*b); + let t_tyexpr = type_with(env, &t_expr)?; + t_tyexpr.normalize_whnf(env.as_nzenv()) } ExprKind::BoolLit(_) => builtin_to_value(Builtin::Bool), ExprKind::NaturalLit(_) => builtin_to_value(Builtin::Natural), @@ -108,25 +144,19 @@ fn type_one_layer( } text_type } - - // ExprKind::EmptyListLit(t) => { - // let arg = match &*t.as_whnf() { - // ValueKind::AppliedBuiltin(Builtin::List, args, _) - // if args.len() == 1 => - // { - // args[0].clone() - // } - // _ => return mkerr("InvalidListType"), - // }; - // RetWhole(Value::from_kind_and_type( - // ValueKind::EmptyListLit(arg), - // t.clone(), - // )) - // } + ExprKind::EmptyListLit(t) => { + let t = t.normalize_whnf(env.as_nzenv()); + match &*t.as_whnf() { + ValueKind::AppliedBuiltin(Builtin::List, args, _) + if args.len() == 1 => {} + _ => return mkerr("InvalidListType"), + }; + t + } ExprKind::NEListLit(xs) => { - let mut iter = xs.iter().enumerate(); - let (_, x) = iter.next().unwrap(); - for (i, y) in iter { + let mut iter = xs.iter(); + let x = iter.next().unwrap(); + for y in iter { if x.get_type()? != y.get_type()? { return mkerr("InvalidListElement"); } @@ -146,42 +176,96 @@ fn type_one_layer( Value::from_builtin(Builtin::Optional).app(t) } - // ExprKind::RecordType(kts) => RetWhole(tck_record_type( - // kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), - // )?), - // ExprKind::UnionType(kts) => RetWhole(tck_union_type( - // kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), - // )?), - // ExprKind::RecordLit(kvs) => RetTypeOnly(tck_record_type( - // kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))), - // )?), - ExprKind::Field(r, x) => { - match &*r.get_type()?.as_whnf() { + ExprKind::RecordLit(kvs) => { + use std::collections::hash_map::Entry; + let mut kts = HashMap::new(); + for (x, v) in kvs { + // Check for duplicated entries + match kts.entry(x.clone()) { + Entry::Occupied(_) => { + return mkerr("RecordTypeDuplicateField") + } + Entry::Vacant(e) => e.insert(v.get_type()?), + }; + } + + let ty = type_of_recordtype( + kts.iter() + .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_quoteenv()))), + )?; + Value::from_kind_and_type(ValueKind::RecordType(kts), ty) + } + ExprKind::RecordType(kts) => { + use std::collections::hash_map::Entry; + let mut seen_fields = HashMap::new(); + for (x, _) in kts { + // Check for duplicated entries + match seen_fields.entry(x.clone()) { + Entry::Occupied(_) => { + return mkerr("RecordTypeDuplicateField") + } + Entry::Vacant(e) => e.insert(()), + }; + } + + type_of_recordtype(kts.iter().map(|(_, t)| Cow::Borrowed(t)))? + } + ExprKind::UnionType(kts) => { + use std::collections::hash_map::Entry; + let mut seen_fields = HashMap::new(); + // Check that all types are the same const + let mut k = None; + for (x, t) in kts { + if let Some(t) = t { + match (k, t.get_type()?.as_const()) { + (None, Some(k2)) => k = Some(k2), + (Some(k1), Some(k2)) if k1 == k2 => {} + _ => return mkerr("InvalidFieldType"), + } + } + match seen_fields.entry(x) { + Entry::Occupied(_) => { + return mkerr("UnionTypeDuplicateField") + } + Entry::Vacant(e) => e.insert(()), + }; + } + + // An empty union type has type Type; + // an union type with only unary variants also has type Type + let k = k.unwrap_or(Const::Type); + + Value::from_const(k) + } + ExprKind::Field(scrut, x) => { + match &*scrut.get_type()?.as_whnf() { ValueKind::RecordType(kts) => match kts.get(&x) { Some(tth) => tth.clone(), None => return mkerr("MissingRecordField"), }, - // TODO: branch here only when r.get_type() is a Const + // TODO: branch here only when scrut.get_type() is a Const _ => { - let r_nf = r.normalize_whnf(env.as_nzenv()); - let r_nf_borrow = r_nf.as_whnf(); - match &*r_nf_borrow { + let scrut_nf = scrut.normalize_whnf(env.as_nzenv()); + let scrut_nf_borrow = scrut_nf.as_whnf(); + match &*scrut_nf_borrow { ValueKind::UnionType(kts) => match kts.get(x) { // Constructor has type T -> < x: T, ... > - // TODO: check pi type properly - Some(Some(t)) => Value::from_kind_and_type( + Some(Some(ty)) => Value::from_kind_and_type( ValueKind::PiClosure { binder: Binder::new(x.clone()), - annot: t.clone(), + annot: ty.clone(), closure: Closure::new( - t.clone(), + ty.clone(), env.as_nzenv(), - r.clone(), + scrut.clone(), ), }, - Value::from_const(Const::Type), + type_of_function( + ty.get_type()?, + scrut.get_type()?, + )?, ), - Some(None) => r_nf.clone(), + Some(None) => scrut_nf.clone(), None => return mkerr("MissingUnionField"), }, _ => return mkerr("NotARecord"), @@ -190,28 +274,45 @@ fn type_one_layer( } } ExprKind::Annot(x, t) => { - if x.get_type()? != t.normalize_whnf(env.as_nzenv()) { + let t = t.normalize_whnf(env.as_nzenv()); + if x.get_type()? != t { return mkerr("annot mismatch"); } - x.normalize_whnf(env.as_nzenv()) + t } ExprKind::App(f, arg) => { let tf = f.get_type()?; let tf_borrow = tf.as_whnf(); - let (expected_arg_ty, ty_closure) = match &*tf_borrow { - ValueKind::PiClosure { annot, closure, .. } => (annot, closure), + match &*tf_borrow { + // ValueKind::PiClosure { annot, closure, .. } => (annot, closure), + ValueKind::PiClosure { + annot: _expected_arg_ty, + closure: ty_closure, + .. + } => { + // if arg.get_type()? != *expected_arg_ty { + // return mkerr(format!( + // "function annot mismatch: {:?}, {:?}", + // arg.get_type()?, + // expected_arg_ty + // )); + // } + + let arg_nf = arg.normalize_whnf(env.as_nzenv()); + ty_closure.apply(arg_nf) + } + // ValueKind::Pi(_, _expected_arg_ty, body) => { + // // if arg.get_type()? != *tx { + // // return mkerr("TypeMismatch"); + // // } + + // let arg_nf = arg.normalize_whnf(env.as_nzenv()); + // let ret = body.subst_shift(&AlphaVar::default(), &arg_nf); + // ret.normalize_nf(); + // ret + // } _ => return mkerr(format!("apply to not Pi: {:?}", tf_borrow)), - }; - // if arg.get_type()? != *expected_arg_ty { - // return mkerr(format!( - // "function annot mismatch: {:?}, {:?}", - // arg.get_type()?, - // expected_arg_ty - // )); - // } - - let arg_nf = arg.normalize_whnf(env.as_nzenv()); - ty_closure.apply(arg_nf) + } } ExprKind::BoolIf(x, y, z) => { if *x.get_type()?.as_whnf() @@ -231,83 +332,63 @@ fn type_one_layer( y.get_type()? } - // ExprKind::BinOp(BinOp::RightBiasedRecordMerge, l, r) => { - // let l_type = l.get_type()?; - // let r_type = r.get_type()?; - - // // Extract the LHS record type - // let l_type_borrow = l_type.as_whnf(); - // let kts_x = match &*l_type_borrow { - // ValueKind::RecordType(kts) => kts, - // _ => return mkerr("MustCombineRecord"), - // }; - - // // Extract the RHS record type - // let r_type_borrow = r_type.as_whnf(); - // let kts_y = match &*r_type_borrow { - // ValueKind::RecordType(kts) => kts, - // _ => return mkerr("MustCombineRecord"), - // }; + ExprKind::BinOp(BinOp::RightBiasedRecordMerge, x, y) => { + let x_type = x.get_type()?; + let y_type = y.get_type()?; - // // Union the two records, prefering - // // the values found in the RHS. - // let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, _, r_t| { - // Ok(r_t.clone()) - // })?; + // Extract the LHS record type + let x_type_borrow = x_type.as_whnf(); + let kts_x = match &*x_type_borrow { + ValueKind::RecordType(kts) => kts, + _ => return mkerr("MustCombineRecord"), + }; - // // Construct the final record type from the union - // RetTypeOnly(tck_record_type( - // kts.into_iter().map(|(x, v)| Ok((x.clone(), v))), - // )?) - // } - // ExprKind::BinOp(BinOp::RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer( - // ctx, - // ExprKind::BinOp( - // RecursiveRecordTypeMerge, - // l.get_type()?, - // r.get_type()?, - // ), - // Span::Artificial, - // )?), - // ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, l, r) => { - // // Extract the LHS record type - // let borrow_l = l.as_whnf(); - // let kts_x = match &*borrow_l { - // ValueKind::RecordType(kts) => kts, - // _ => { - // return mkerr("RecordTypeMergeRequiresRecordType") - // } - // }; + // Extract the RHS record type + let y_type_borrow = y_type.as_whnf(); + let kts_y = match &*y_type_borrow { + ValueKind::RecordType(kts) => kts, + _ => return mkerr("MustCombineRecord"), + }; - // // Extract the RHS record type - // let borrow_r = r.as_whnf(); - // let kts_y = match &*borrow_r { - // ValueKind::RecordType(kts) => kts, - // _ => { - // return mkerr("RecordTypeMergeRequiresRecordType") - // } - // }; + // Union the two records, prefering + // the values found in the RHS. + let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, _, r_t| { + Ok(r_t.clone()) + })?; - // // Ensure that the records combine without a type error - // let kts = merge_maps( - // kts_x, - // kts_y, - // // If the Label exists for both records, then we hit the recursive case. - // |_, l: &Value, r: &Value| { - // type_last_layer( - // ctx, - // ExprKind::BinOp( - // RecursiveRecordTypeMerge, - // l.clone(), - // r.clone(), - // ), - // Span::Artificial, - // ) - // }, - // )?; - - // RetWhole(tck_record_type(kts.into_iter().map(Ok))?) - // } + // Construct the final record type + let ty = type_of_recordtype( + kts.iter() + .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_quoteenv()))), + )?; + Value::from_kind_and_type(ValueKind::RecordType(kts), ty) + } + ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { + let ekind = ExprKind::BinOp( + BinOp::RecursiveRecordTypeMerge, + x.get_type()?.to_tyexpr(env.as_quoteenv()), + y.get_type()?.to_tyexpr(env.as_quoteenv()), + ); + let ty = type_one_layer(env, &ekind)?; + TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial) + .normalize_whnf(env.as_nzenv()) + } + ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { + let x_val = x.normalize_whnf(env.as_nzenv()); + let y_val = y.normalize_whnf(env.as_nzenv()); + match &*x_val.as_whnf() { + ValueKind::RecordType(_) => {} + _ => return mkerr("RecordTypeMergeRequiresRecordType"), + } + match &*y_val.as_whnf() { + ValueKind::RecordType(_) => {} + _ => return mkerr("RecordTypeMergeRequiresRecordType"), + } + // A RecordType's type is always a const + let xk = x.get_type()?.as_const().unwrap(); + let yk = y.get_type()?.as_const().unwrap(); + Value::from_const(max(xk, yk)) + } // ExprKind::BinOp(o @ BinOp::ListAppend, l, r) => { // match &*l.get_type()?.as_whnf() { // ValueKind::AppliedBuiltin(List, _, _) => {} @@ -363,6 +444,122 @@ fn type_one_layer( t } + // ExprKind::Merge(record, union, type_annot) => { + // let record_type = record.get_type()?; + // let record_borrow = record_type.as_whnf(); + // let handlers = match &*record_borrow { + // ValueKind::RecordType(kts) => kts, + // _ => return mkerr("Merge1ArgMustBeRecord"), + // }; + + // let union_type = union.get_type()?; + // let union_borrow = union_type.as_whnf(); + // let variants = match &*union_borrow { + // ValueKind::UnionType(kts) => Cow::Borrowed(kts), + // ValueKind::AppliedBuiltin( + // syntax::Builtin::Optional, + // args, + // _, + // ) if args.len() == 1 => { + // let ty = &args[0]; + // let mut kts = HashMap::new(); + // kts.insert("None".into(), None); + // kts.insert("Some".into(), Some(ty.clone())); + // Cow::Owned(kts) + // } + // _ => return mkerr("Merge2ArgMustBeUnionOrOptional"), + // }; + + // let mut inferred_type = None; + // for (x, handler_type) in handlers { + // let handler_return_type = + // match variants.get(x) { + // // Union alternative with type + // Some(Some(variant_type)) => { + // let handler_type_borrow = handler_type.as_whnf(); + // let (tx, tb) = match &*handler_type_borrow { + // ValueKind::Pi(_, tx, tb) => (tx, tb), + // _ => return mkerr("NotAFunction"), + // }; + + // if variant_type != tx { + // return mkerr("TypeMismatch"); + // } + + // // Extract `tb` from under the binder. Fails if the variable was used + // // in `tb`. + // match tb.over_binder() { + // Some(x) => x, + // None => return mkerr( + // "MergeHandlerReturnTypeMustNotBeDependent", + // ), + // } + // } + // // Union alternative without type + // Some(None) => handler_type.clone(), + // None => return mkerr("MergeHandlerMissingVariant"), + // }; + // match &inferred_type { + // None => inferred_type = Some(handler_return_type), + // Some(t) => { + // if t != &handler_return_type { + // return mkerr("MergeHandlerTypeMismatch"); + // } + // } + // } + // } + // for x in variants.keys() { + // if !handlers.contains_key(x) { + // return mkerr("MergeVariantMissingHandler"); + // } + // } + + // match (inferred_type, type_annot.as_ref()) { + // (Some(t1), Some(t2)) => { + // if &t1 != t2 { + // return mkerr("MergeAnnotMismatch"); + // } + // RetTypeOnly(t1) + // } + // (Some(t), None) => RetTypeOnly(t), + // (None, Some(t)) => RetTypeOnly(t.clone()), + // (None, None) => return mkerr("MergeEmptyNeedsAnnotation"), + // } + // } + ExprKind::ToMap(_, _) => unimplemented!("toMap"), + ExprKind::Projection(record, labels) => { + let record_type = record.get_type()?; + let record_type_borrow = record_type.as_whnf(); + let kts = match &*record_type_borrow { + ValueKind::RecordType(kts) => kts, + _ => return mkerr("ProjectionMustBeRecord"), + }; + + let mut new_kts = HashMap::new(); + for l in labels { + match kts.get(l) { + None => return mkerr("ProjectionMissingEntry"), + Some(t) => { + use std::collections::hash_map::Entry; + match new_kts.entry(l.clone()) { + Entry::Occupied(_) => { + return mkerr("ProjectionDuplicateField") + } + Entry::Vacant(e) => e.insert(t.clone()), + } + } + }; + } + + Value::from_kind_and_type( + ValueKind::RecordType(new_kts), + record_type.get_type()?, + ) + } + ExprKind::ProjectionByExpr(_, _) => { + unimplemented!("selection by expression") + } + ExprKind::Completion(_, _) => unimplemented!("record completion"), _ => Value::from_const(Const::Type), // TODO }) } @@ -383,18 +580,17 @@ fn type_with( let annot_nf = annot.normalize_whnf(env.as_nzenv()); let body = type_with(&env.insert_type(&binder, annot_nf.clone()), body)?; - let ty = Value::from_kind_and_type( - ValueKind::PiClosure { - binder: Binder::new(binder.clone()), - annot: annot_nf.clone(), - closure: Closure::new( - annot_nf, - env.as_nzenv(), - body.get_type()?.to_tyexpr(env.as_quoteenv().insert()), - ), - }, - Value::from_const(Const::Type), // TODO: function_check + let body_ty = body.get_type()?; + let ty = TyExpr::new( + TyExprKind::Expr(ExprKind::Pi( + binder.clone(), + annot.clone(), + body_ty.to_tyexpr(env.as_quoteenv().insert()), + )), + Some(type_of_function(annot.get_type()?, body_ty.get_type()?)?), + Span::Artificial, ); + let ty = ty.normalize_whnf(env.as_nzenv()); ( TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)), Some(ty), @@ -405,19 +601,20 @@ fn type_with( let annot_nf = annot.normalize_whnf(env.as_nzenv()); let body = type_with(&env.insert_type(binder, annot_nf.clone()), body)?; + let ty = type_of_function(annot.get_type()?, body.get_type()?)?; ( TyExprKind::Expr(ExprKind::Pi(binder.clone(), annot, body)), - Some(Value::from_const(Const::Type)), // TODO: function_check + Some(ty), ) } ExprKind::Let(binder, annot, val, body) => { - let v = if let Some(t) = annot { + let val = if let Some(t) = annot { t.rewrap(ExprKind::Annot(val.clone(), t.clone())) } else { val.clone() }; - let val = type_with(env, val)?; + let val = type_with(env, &val)?; let val_nf = val.normalize_whnf(&env.as_nzenv()); let body = type_with(&env.insert_value(&binder, val_nf), body)?; let body_ty = body.get_type().ok(); |