From 531fdb1757a97a3accc8e836a1ff3a3977c37bfe Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Apr 2020 17:51:53 +0100 Subject: Factor out operations in typecheck --- dhall/src/semantics/tck/typecheck.rs | 851 ++++++++++++++++++----------------- dhall/src/syntax/ast/expr.rs | 4 +- 2 files changed, 438 insertions(+), 417 deletions(-) diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 8f3fcb2..28d08b9 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -66,206 +66,263 @@ pub fn mk_span_err(span: Span, msg: S) -> Result { ) } -/// When all sub-expressions have been typed, check the remaining toplevel -/// layer. -fn type_one_layer( +fn type_of_binop( env: &TyEnv, - ekind: ExprKind>, span: Span, + op: BinOp, + l: &Tir<'_>, + r: &Tir<'_>, ) -> Result { let span_err = |msg: &str| mk_span_err(span.clone(), msg); + use BinOp::*; + use NirKind::{ListType, RecordType}; - let ty = match &ekind { - ExprKind::Import(..) | ExprKind::Op(OpKind::Completion(..)) => { - unreachable!("This case should have been handled in resolution") - } - ExprKind::Var(..) - | ExprKind::Const(Const::Sort) - | ExprKind::Lam(..) - | ExprKind::Pi(..) - | ExprKind::Let(..) - | ExprKind::Annot(..) => { - unreachable!("This case should have been handled in type_with") - } + Ok(match op { + RightBiasedRecordMerge => { + let x_type = l.ty(); + let y_type = r.ty(); - ExprKind::Const(Const::Type) => Type::from_const(Const::Kind), - ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort), - ExprKind::Builtin(b) => { - let t_hir = type_of_builtin(*b); - typecheck(&t_hir)?.eval_to_type(env)? - } - ExprKind::Num(NumKind::Bool(_)) => Type::from_builtin(Builtin::Bool), - ExprKind::Num(NumKind::Natural(_)) => { - Type::from_builtin(Builtin::Natural) - } - ExprKind::Num(NumKind::Integer(_)) => { - Type::from_builtin(Builtin::Integer) - } - ExprKind::Num(NumKind::Double(_)) => { - Type::from_builtin(Builtin::Double) + // Extract the LHS record type + let kts_x = match x_type.kind() { + RecordType(kts) => kts, + _ => return span_err("MustCombineRecord"), + }; + // Extract the RHS record type + let kts_y = match y_type.kind() { + RecordType(kts) => kts, + _ => return span_err("MustCombineRecord"), + }; + + // 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 u = max(l.ty().ty(), r.ty().ty()); + Nir::from_kind(RecordType(kts)).to_type(u) } - ExprKind::TextLit(interpolated) => { - let text_type = Type::from_builtin(Builtin::Text); - for contents in interpolated.iter() { - use InterpolatedTextContents::Expr; - if let Expr(x) = contents { - if *x.ty() != text_type { - return span_err("InvalidTextInterpolation"); - } - } - } - text_type + RecursiveRecordMerge => { + check_rectymerge(&span, env, l.ty().to_nir(), r.ty().to_nir())?; + + let hir = Hir::new( + HirKind::Expr(ExprKind::Op(OpKind::BinOp( + RecursiveRecordTypeMerge, + l.ty().to_hir(env.as_varenv()), + r.ty().to_hir(env.as_varenv()), + ))), + span.clone(), + ); + let x_u = l.ty().ty(); + let y_u = r.ty().ty(); + Type::new(hir.eval(env), max(x_u, y_u)) } - ExprKind::EmptyListLit(t) => { - let t = t.eval_to_type(env)?; - match t.kind() { - NirKind::ListType(..) => {} - _ => return span_err("InvalidListType"), - }; - t + RecursiveRecordTypeMerge => { + check_rectymerge(&span, env, l.eval(env), r.eval(env))?; + + // A RecordType's type is always a const + let xk = l.ty().as_const().unwrap(); + let yk = r.ty().as_const().unwrap(); + Type::from_const(max(xk, yk)) } - ExprKind::NEListLit(xs) => { - let mut iter = xs.iter(); - let x = iter.next().unwrap(); - for y in iter { - if x.ty() != y.ty() { - return span_err("InvalidListElement"); - } + ListAppend => { + match l.ty().kind() { + ListType(..) => {} + _ => return span_err("BinOpTypeMismatch"), } - if x.ty().ty().as_const() != Some(Const::Type) { - return span_err("InvalidListType"); + + if l.ty() != r.ty() { + return span_err("BinOpTypeMismatch"); } - let t = x.ty().to_nir(); - Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type) + l.ty().clone() } - ExprKind::SomeLit(x) => { - if x.ty().ty().as_const() != Some(Const::Type) { - return span_err("InvalidOptionalType"); + Equivalence => { + if l.ty() != r.ty() { + return span_err("EquivalenceTypeMismatch"); + } + if l.ty().ty().as_const() != Some(Const::Type) { + return span_err("EquivalenceArgumentsMustBeTerms"); } - let t = x.ty().to_nir(); - Nir::from_builtin(Builtin::Optional) - .app(t) - .to_type(Const::Type) + Type::from_const(Const::Type) } - ExprKind::RecordLit(kvs) => { - use std::collections::hash_map::Entry; - let mut kts = HashMap::new(); - // An empty record type has type Type - let mut k = Const::Type; - for (x, v) in kvs { - // Check for duplicated entries - match kts.entry(x.clone()) { - Entry::Occupied(_) => { - return span_err("RecordTypeDuplicateField") - } - Entry::Vacant(e) => e.insert(v.ty().to_nir()), - }; + op => { + let t = Type::from_builtin(match op { + BoolAnd | BoolOr | BoolEQ | BoolNE => Builtin::Bool, + NaturalPlus | NaturalTimes => Builtin::Natural, + TextAppend => Builtin::Text, + ListAppend + | RightBiasedRecordMerge + | RecursiveRecordMerge + | RecursiveRecordTypeMerge + | Equivalence => unreachable!(), + ImportAlt => unreachable!("ImportAlt leftover in tck"), + }); - // Check that the fields have a valid kind - match v.ty().ty().as_const() { - Some(c) => k = max(k, c), - None => return span_err("InvalidFieldType"), - } + if *l.ty() != t { + return span_err("BinOpTypeMismatch"); } - Nir::from_kind(NirKind::RecordType(kts)).to_type(k) + if *r.ty() != t { + return span_err("BinOpTypeMismatch"); + } + + t } - ExprKind::RecordType(kts) => { - use std::collections::hash_map::Entry; - let mut seen_fields = HashMap::new(); - // An empty record type has type Type - let mut k = Const::Type; + }) +} - for (x, t) in kts { - // Check for duplicated entries - match seen_fields.entry(x.clone()) { - Entry::Occupied(_) => { - return span_err("RecordTypeDuplicateField") - } - Entry::Vacant(e) => e.insert(()), - }; +fn type_of_merge( + env: &TyEnv, + span: Span, + record: &Tir<'_>, + scrut: &Tir<'_>, + type_annot: Option<&Tir<'_>>, +) -> Result { + let span_err = |msg: &str| mk_span_err(span.clone(), msg); + use NirKind::{OptionalType, PiClosure, RecordType, UnionType}; - // Check the type is a Const and compute final type - match t.ty().as_const() { - Some(c) => k = max(k, c), - None => return span_err("InvalidFieldType"), - } - } + let record_type = scrut.ty(); + let handlers = match record_type.kind() { + RecordType(kts) => kts, + _ => return span_err("Merge1ArgMustBeRecord"), + }; - Type::from_const(k) + let scrut_type = scrut.ty(); + let variants = match scrut_type.kind() { + UnionType(kts) => Cow::Borrowed(kts), + OptionalType(ty) => { + let mut kts = HashMap::new(); + kts.insert("None".into(), None); + kts.insert("Some".into(), Some(ty.clone())); + Cow::Owned(kts) } - 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.ty().as_const()) { - (None, Some(k2)) => k = Some(k2), - (Some(k1), Some(k2)) if k1 == k2 => {} - _ => return span_err("InvalidFieldType"), - } - } - match seen_fields.entry(x) { - Entry::Occupied(_) => { - return span_err("UnionTypeDuplicateField") - } - Entry::Vacant(e) => e.insert(()), - }; - } + _ => return span_err("Merge2ArgMustBeUnionOrOptional"), + }; - // 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); + let mut inferred_type = None; + for (x, handler_type) in handlers { + let handler_return_type: Type = match variants.get(x) { + // Union alternative with type + Some(Some(variant_type)) => match handler_type.kind() { + PiClosure { closure, annot, .. } => { + if variant_type != annot { + return mkerr( + ErrorBuilder::new(format!( + "Wrong handler input type" + )) + .span_err( + span, + format!("in this merge expression",), + ) + .span_err( + record.span(), + format!( + "the handler for `{}` expects a value of \ + type: `{}`", + x, + annot.to_expr_tyenv(env) + ), + ) + .span_err( + scrut.span(), + format!( + "but the corresponding variant has type: \ + `{}`", + variant_type.to_expr_tyenv(env) + ), + ) + .format(), + ); + } - Type::from_const(k) - } - ExprKind::Op(OpKind::Field(scrut, x)) => { - match scrut.ty().kind() { - NirKind::RecordType(kts) => match kts.get(&x) { - Some(val) => Type::new_infer_universe(env, val.clone())?, - None => return span_err("MissingRecordField"), - }, - NirKind::Const(_) => { - let scrut = scrut.eval_to_type(env)?; - match scrut.kind() { - NirKind::UnionType(kts) => match kts.get(x) { - // Constructor has type T -> < x: T, ... > - Some(Some(ty)) => { - Nir::from_kind(NirKind::PiClosure { - binder: Binder::new(x.clone()), - annot: ty.clone(), - closure: Closure::new_constant( - scrut.to_nir(), - ), - }) - .to_type(scrut.ty()) - } - Some(None) => scrut, - None => return span_err("MissingUnionField"), - }, - _ => return span_err("NotARecord"), + // TODO: this actually doesn't check anything yet + match closure.remove_binder() { + Ok(v) => Type::new_infer_universe(env, v.clone())?, + Err(()) => { + return span_err("MergeReturnTypeIsDependent") + } } } - _ => return span_err("NotARecord"), + _ => { + return mkerr( + ErrorBuilder::new(format!( + "merge handler is not a function" + )) + .span_err(span, format!("in this merge expression")) + .span_err( + record.span(), + format!( + "the handler for `{}` has type: `{}`", + x, + handler_type.to_expr_tyenv(env) + ), + ) + .span_help( + scrut.span(), + format!( + "the corresponding variant has type: `{}`", + variant_type.to_expr_tyenv(env) + ), + ) + .help(format!( + "a handler for this variant must be a function \ + that takes an input of type: `{}`", + variant_type.to_expr_tyenv(env) + )) + .format(), + ) + } + }, + // Union alternative without type + Some(None) => Type::new_infer_universe(env, handler_type.clone())?, + None => return span_err("MergeHandlerMissingVariant"), + }; + match &inferred_type { + None => inferred_type = Some(handler_return_type), + Some(t) => { + if t != &handler_return_type { + return span_err("MergeHandlerTypeMismatch"); + } } } - ExprKind::Assert(t) => { - let t = t.eval_to_type(env)?; - match t.kind() { - NirKind::Equivalence(x, y) if x == y => {} - NirKind::Equivalence(..) => return span_err("AssertMismatch"), - _ => return span_err("AssertMustTakeEquivalence"), + } + for x in variants.keys() { + if !handlers.contains_key(x) { + return span_err("MergeVariantMissingHandler"); + } + } + + let type_annot = type_annot + .as_ref() + .map(|t| t.eval_to_type(env)) + .transpose()?; + Ok(match (inferred_type, type_annot) { + (Some(t1), Some(t2)) => { + if t1 != t2 { + return span_err("MergeAnnotMismatch"); } - t + t1 } - ExprKind::Op(OpKind::App(f, arg)) => { + (Some(t), None) => t, + (None, Some(t)) => t, + (None, None) => return span_err("MergeEmptyNeedsAnnotation"), + }) +} + +fn type_of_operation( + env: &TyEnv, + span: Span, + opkind: &OpKind>, +) -> Result { + let span_err = |msg: &str| mk_span_err(span.clone(), msg); + use NirKind::{ListType, PiClosure, RecordType, UnionType}; + use OpKind::*; + + Ok(match opkind { + App(f, arg) => { match f.ty().kind() { // TODO: store Type in closure - NirKind::PiClosure { annot, closure, .. } => { + PiClosure { annot, closure, .. } => { if arg.ty().as_nir() != annot { return mkerr( ErrorBuilder::new(format!( @@ -310,7 +367,8 @@ fn type_one_layer( ), } } - ExprKind::Op(OpKind::BoolIf(x, y, z)) => { + BinOp(o, l, r) => type_of_binop(env, span, *o, l, r)?, + BoolIf(x, y, z) => { if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) { return span_err("InvalidPredicate"); } @@ -323,245 +381,16 @@ fn type_one_layer( y.ty().clone() } - ExprKind::Op(OpKind::BinOp(BinOp::RightBiasedRecordMerge, x, y)) => { - let x_type = x.ty(); - let y_type = y.ty(); - - // Extract the LHS record type - let kts_x = match x_type.kind() { - NirKind::RecordType(kts) => kts, - _ => return span_err("MustCombineRecord"), - }; - // Extract the RHS record type - let kts_y = match y_type.kind() { - NirKind::RecordType(kts) => kts, - _ => return span_err("MustCombineRecord"), - }; - - // 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 u = max(x.ty().ty(), y.ty().ty()); - Nir::from_kind(NirKind::RecordType(kts)).to_type(u) + Merge(record, scrut, type_annot) => { + type_of_merge(env, span, record, scrut, type_annot.as_ref())? } - ExprKind::Op(OpKind::BinOp(BinOp::RecursiveRecordMerge, x, y)) => { - check_rectymerge(&span, env, x.ty().to_nir(), y.ty().to_nir())?; - - let hir = Hir::new( - HirKind::Expr(ExprKind::Op(OpKind::BinOp( - BinOp::RecursiveRecordTypeMerge, - x.ty().to_hir(env.as_varenv()), - y.ty().to_hir(env.as_varenv()), - ))), - span.clone(), - ); - let x_u = x.ty().ty(); - let y_u = y.ty().ty(); - Type::new(hir.eval(env), max(x_u, y_u)) - } - ExprKind::Op(OpKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y)) => { - check_rectymerge(&span, env, x.eval(env), y.eval(env))?; - - // A RecordType's type is always a const - let xk = x.ty().as_const().unwrap(); - let yk = y.ty().as_const().unwrap(); - Type::from_const(max(xk, yk)) - } - ExprKind::Op(OpKind::BinOp(BinOp::ListAppend, l, r)) => { - match l.ty().kind() { - NirKind::ListType(..) => {} - _ => return span_err("BinOpTypeMismatch"), - } - - if l.ty() != r.ty() { - return span_err("BinOpTypeMismatch"); - } - - l.ty().clone() - } - ExprKind::Op(OpKind::BinOp(BinOp::Equivalence, l, r)) => { - if l.ty() != r.ty() { - return span_err("EquivalenceTypeMismatch"); - } - if l.ty().ty().as_const() != Some(Const::Type) { - return span_err("EquivalenceArgumentsMustBeTerms"); - } - - Type::from_const(Const::Type) - } - ExprKind::Op(OpKind::BinOp(o, l, r)) => { - let t = Type::from_builtin(match o { - BinOp::BoolAnd - | BinOp::BoolOr - | BinOp::BoolEQ - | BinOp::BoolNE => Builtin::Bool, - BinOp::NaturalPlus | BinOp::NaturalTimes => Builtin::Natural, - BinOp::TextAppend => Builtin::Text, - BinOp::ListAppend - | BinOp::RightBiasedRecordMerge - | BinOp::RecursiveRecordMerge - | BinOp::RecursiveRecordTypeMerge - | BinOp::Equivalence => unreachable!(), - BinOp::ImportAlt => unreachable!("ImportAlt leftover in tck"), - }); - - if *l.ty() != t { - return span_err("BinOpTypeMismatch"); - } - - if *r.ty() != t { - return span_err("BinOpTypeMismatch"); - } - - t - } - ExprKind::Op(OpKind::Merge(record, union, type_annot)) => { - let record_type = record.ty(); - let handlers = match record_type.kind() { - NirKind::RecordType(kts) => kts, - _ => return span_err("Merge1ArgMustBeRecord"), - }; - - let union_type = union.ty(); - let variants = match union_type.kind() { - NirKind::UnionType(kts) => Cow::Borrowed(kts), - NirKind::OptionalType(ty) => { - let mut kts = HashMap::new(); - kts.insert("None".into(), None); - kts.insert("Some".into(), Some(ty.clone())); - Cow::Owned(kts) - } - _ => return span_err("Merge2ArgMustBeUnionOrOptional"), - }; - - let mut inferred_type = None; - for (x, handler_type) in handlers { - let handler_return_type: Type = match variants.get(x) { - // Union alternative with type - Some(Some(variant_type)) => match handler_type.kind() { - NirKind::PiClosure { closure, annot, .. } => { - if variant_type != annot { - return mkerr( - ErrorBuilder::new(format!( - "Wrong handler input type" - )) - .span_err( - span, - format!("in this merge expression",), - ) - .span_err( - record.span(), - format!( - "the handler for `{}` expects a \ - value of type: `{}`", - x, - annot.to_expr_tyenv(env) - ), - ) - .span_err( - union.span(), - format!( - "but the corresponding variant \ - has type: `{}`", - variant_type.to_expr_tyenv(env) - ), - ) - .format(), - ); - } - - // TODO: this actually doesn't check anything yet - match closure.remove_binder() { - Ok(v) => { - Type::new_infer_universe(env, v.clone())? - } - Err(()) => { - return span_err( - "MergeReturnTypeIsDependent", - ) - } - } - } - _ => { - return mkerr( - ErrorBuilder::new(format!( - "merge handler is not a function" - )) - .span_err( - span, - format!("in this merge expression"), - ) - .span_err( - record.span(), - format!( - "the handler for `{}` has type: `{}`", - x, - handler_type.to_expr_tyenv(env) - ), - ) - .span_help( - union.span(), - format!( - "the corresponding variant has type: \ - `{}`", - variant_type.to_expr_tyenv(env) - ), - ) - .help(format!( - "a handler for this variant must be a \ - function that takes an input of type: \ - `{}`", - variant_type.to_expr_tyenv(env) - )) - .format(), - ) - } - }, - // Union alternative without type - Some(None) => { - Type::new_infer_universe(env, handler_type.clone())? - } - None => return span_err("MergeHandlerMissingVariant"), - }; - match &inferred_type { - None => inferred_type = Some(handler_return_type), - Some(t) => { - if t != &handler_return_type { - return span_err("MergeHandlerTypeMismatch"); - } - } - } - } - for x in variants.keys() { - if !handlers.contains_key(x) { - return span_err("MergeVariantMissingHandler"); - } - } - - let type_annot = type_annot - .as_ref() - .map(|t| t.eval_to_type(env)) - .transpose()?; - match (inferred_type, type_annot) { - (Some(t1), Some(t2)) => { - if t1 != t2 { - return span_err("MergeAnnotMismatch"); - } - t1 - } - (Some(t), None) => t, - (None, Some(t)) => t, - (None, None) => return span_err("MergeEmptyNeedsAnnotation"), - } - } - ExprKind::Op(OpKind::ToMap(record, annot)) => { + ToMap(record, annot) => { if record.ty().ty().as_const() != Some(Const::Type) { return span_err("`toMap` only accepts records of type `Type`"); } let record_t = record.ty(); let kts = match record_t.kind() { - NirKind::RecordType(kts) => kts, + RecordType(kts) => kts, _ => { return span_err("The argument to `toMap` must be a record") } @@ -581,11 +410,11 @@ fn type_one_layer( let err_msg = "The type of `toMap x` must be of the form \ `List { mapKey : Text, mapValue : T }`"; let arg = match annot_val.kind() { - NirKind::ListType(t) => t, + ListType(t) => t, _ => return span_err(err_msg), }; let kts = match arg.kind() { - NirKind::RecordType(kts) => kts, + RecordType(kts) => kts, _ => return span_err(err_msg), }; if kts.len() != 2 { @@ -614,7 +443,7 @@ fn type_one_layer( kts.insert("mapKey".into(), Nir::from_builtin(Builtin::Text)); kts.insert("mapValue".into(), entry_type); let output_type: Type = Nir::from_builtin(Builtin::List) - .app(Nir::from_kind(NirKind::RecordType(kts))) + .app(Nir::from_kind(RecordType(kts))) .to_type(Const::Type); if let Some(annot) = annot { let annot_val = annot.eval_to_type(env)?; @@ -625,10 +454,36 @@ fn type_one_layer( output_type } } - ExprKind::Op(OpKind::Projection(record, labels)) => { + Field(scrut, x) => { + match scrut.ty().kind() { + RecordType(kts) => match kts.get(&x) { + Some(val) => Type::new_infer_universe(env, val.clone())?, + None => return span_err("MissingRecordField"), + }, + NirKind::Const(_) => { + let scrut = scrut.eval_to_type(env)?; + match scrut.kind() { + UnionType(kts) => match kts.get(x) { + // Constructor has type T -> < x: T, ... > + Some(Some(ty)) => Nir::from_kind(PiClosure { + binder: Binder::new(x.clone()), + annot: ty.clone(), + closure: Closure::new_constant(scrut.to_nir()), + }) + .to_type(scrut.ty()), + Some(None) => scrut, + None => return span_err("MissingUnionField"), + }, + _ => return span_err("NotARecord"), + } + } + _ => return span_err("NotARecord"), + } + } + Projection(record, labels) => { let record_type = record.ty(); let kts = match record_type.kind() { - NirKind::RecordType(kts) => kts, + RecordType(kts) => kts, _ => return span_err("ProjectionMustBeRecord"), }; @@ -648,21 +503,18 @@ fn type_one_layer( }; } - Type::new_infer_universe( - env, - Nir::from_kind(NirKind::RecordType(new_kts)), - )? + Type::new_infer_universe(env, Nir::from_kind(RecordType(new_kts)))? } - ExprKind::Op(OpKind::ProjectionByExpr(record, selection)) => { + ProjectionByExpr(record, selection) => { let record_type = record.ty(); let rec_kts = match record_type.kind() { - NirKind::RecordType(kts) => kts, + RecordType(kts) => kts, _ => return span_err("ProjectionMustBeRecord"), }; let selection_val = selection.eval_to_type(env)?; let sel_kts = match selection_val.kind() { - NirKind::RecordType(kts) => kts, + RecordType(kts) => kts, _ => return span_err("ProjectionByExprTakesRecordType"), }; @@ -679,13 +531,182 @@ fn type_one_layer( selection_val } - }; + Completion(..) => { + unreachable!("This case should have been handled in resolution") + } + }) +} - Ok(ty) +/// When all sub-expressions have been typed, check the remaining toplevel +/// layer. +fn type_one_layer( + env: &TyEnv, + ekind: ExprKind>, + span: Span, +) -> Result { + let span_err = |msg: &str| mk_span_err(span.clone(), msg); + + Ok(match &ekind { + ExprKind::Import(..) => { + unreachable!("This case should have been handled in resolution") + } + ExprKind::Var(..) + | ExprKind::Const(Const::Sort) + | ExprKind::Lam(..) + | ExprKind::Pi(..) + | ExprKind::Let(..) + | ExprKind::Annot(..) => { + unreachable!("This case should have been handled in type_with") + } + + ExprKind::Const(Const::Type) => Type::from_const(Const::Kind), + ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort), + ExprKind::Num(num) => Type::from_builtin(match num { + NumKind::Bool(_) => Builtin::Bool, + NumKind::Natural(_) => Builtin::Natural, + NumKind::Integer(_) => Builtin::Integer, + NumKind::Double(_) => Builtin::Double, + }), + ExprKind::Builtin(b) => { + let t_hir = type_of_builtin(*b); + typecheck(&t_hir)?.eval_to_type(env)? + } + ExprKind::TextLit(interpolated) => { + let text_type = Type::from_builtin(Builtin::Text); + for contents in interpolated.iter() { + use InterpolatedTextContents::Expr; + if let Expr(x) = contents { + if *x.ty() != text_type { + return span_err("InvalidTextInterpolation"); + } + } + } + text_type + } + ExprKind::SomeLit(x) => { + if x.ty().ty().as_const() != Some(Const::Type) { + return span_err("InvalidOptionalType"); + } + + let t = x.ty().to_nir(); + Nir::from_builtin(Builtin::Optional) + .app(t) + .to_type(Const::Type) + } + ExprKind::EmptyListLit(t) => { + let t = t.eval_to_type(env)?; + match t.kind() { + NirKind::ListType(..) => {} + _ => return span_err("InvalidListType"), + }; + t + } + ExprKind::NEListLit(xs) => { + let mut iter = xs.iter(); + let x = iter.next().unwrap(); + for y in iter { + if x.ty() != y.ty() { + return span_err("InvalidListElement"); + } + } + if x.ty().ty().as_const() != Some(Const::Type) { + return span_err("InvalidListType"); + } + + let t = x.ty().to_nir(); + Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type) + } + ExprKind::RecordLit(kvs) => { + use std::collections::hash_map::Entry; + let mut kts = HashMap::new(); + // An empty record type has type Type + let mut k = Const::Type; + for (x, v) in kvs { + // Check for duplicated entries + match kts.entry(x.clone()) { + Entry::Occupied(_) => { + return span_err("RecordTypeDuplicateField") + } + Entry::Vacant(e) => e.insert(v.ty().to_nir()), + }; + + // Check that the fields have a valid kind + match v.ty().ty().as_const() { + Some(c) => k = max(k, c), + None => return span_err("InvalidFieldType"), + } + } + + Nir::from_kind(NirKind::RecordType(kts)).to_type(k) + } + ExprKind::RecordType(kts) => { + use std::collections::hash_map::Entry; + let mut seen_fields = HashMap::new(); + // An empty record type has type Type + let mut k = Const::Type; + + for (x, t) in kts { + // Check for duplicated entries + match seen_fields.entry(x.clone()) { + Entry::Occupied(_) => { + return span_err("RecordTypeDuplicateField") + } + Entry::Vacant(e) => e.insert(()), + }; + + // Check the type is a Const and compute final type + match t.ty().as_const() { + Some(c) => k = max(k, c), + None => return span_err("InvalidFieldType"), + } + } + + Type::from_const(k) + } + 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.ty().as_const()) { + (None, Some(k2)) => k = Some(k2), + (Some(k1), Some(k2)) if k1 == k2 => {} + _ => return span_err("InvalidFieldType"), + } + } + match seen_fields.entry(x) { + Entry::Occupied(_) => { + return span_err("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); + + Type::from_const(k) + } + ExprKind::Op(op) => type_of_operation(env, span, op)?, + ExprKind::Assert(t) => { + let t = t.eval_to_type(env)?; + match t.kind() { + NirKind::Equivalence(x, y) if x == y => {} + NirKind::Equivalence(..) => return span_err("AssertMismatch"), + _ => return span_err("AssertMustTakeEquivalence"), + } + t + } + }) } /// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation /// to compare with. +// We pass the annotation to avoid duplicating the annot checking logic. I hope one day we can use +// it to handle the annotations in merge/toMap/etc. uniformly. pub fn type_with<'hir>( env: &TyEnv, hir: &'hir Hir, @@ -781,7 +802,7 @@ pub fn type_with<'hir>( Ok(tir) } -/// Typecheck an expression and return the expression annotated with types if type-checking +/// Typecheck an expression and return the expression annotated with its type if type-checking /// succeeded, or an error if type-checking failed. pub fn typecheck<'hir>(hir: &'hir Hir) -> Result, TypeError> { type_with(&TyEnv::new(), hir, None) diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs index 51426ce..51e9ea7 100644 --- a/dhall/src/syntax/ast/expr.rs +++ b/dhall/src/syntax/ast/expr.rs @@ -161,10 +161,10 @@ pub enum ExprKind { Num(NumKind), /// Built-in functions and types Builtin(Builtin), - /// `Some e` - SomeLit(SubExpr), /// `"Some ${interpolated} text"` TextLit(InterpolatedText), + /// `Some e` + SomeLit(SubExpr), /// `[] : t` EmptyListLit(SubExpr), /// `[x, y, z]` -- cgit v1.2.3