From fff4c46e09d4edf25eba737f4d71bfdb1dbf4a82 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Apr 2020 22:11:54 +0100 Subject: Extract operation-related code to a new module --- dhall/src/semantics/tck/typecheck.rs | 515 +---------------------------------- 1 file changed, 4 insertions(+), 511 deletions(-) (limited to 'dhall/src/semantics/tck/typecheck.rs') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 427b39d..7481f07 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -1,51 +1,15 @@ -use std::borrow::Cow; use std::cmp::max; use std::collections::HashMap; use crate::error::{ErrorBuilder, TypeError, TypeMessage}; -use crate::semantics::merge_maps; +use crate::operations::typecheck_operation; use crate::semantics::{ - type_of_builtin, Binder, Closure, Hir, HirKind, Nir, NirKind, Tir, TyEnv, - Type, + type_of_builtin, Hir, HirKind, Nir, NirKind, Tir, TyEnv, Type, }; use crate::syntax::{ - BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, OpKind, - Span, + Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, Span, }; -fn check_rectymerge( - span: &Span, - env: &TyEnv, - x: Nir, - y: Nir, -) -> Result<(), TypeError> { - let kts_x = match x.kind() { - NirKind::RecordType(kts) => kts, - _ => { - return mk_span_err( - span.clone(), - "RecordTypeMergeRequiresRecordType", - ) - } - }; - let kts_y = match y.kind() { - NirKind::RecordType(kts) => kts, - _ => { - return mk_span_err( - span.clone(), - "RecordTypeMergeRequiresRecordType", - ) - } - }; - for (k, tx) in kts_x { - if let Some(ty) = kts_y.get(k) { - // TODO: store Type in RecordType ? - check_rectymerge(span, env, tx.clone(), ty.clone())?; - } - } - Ok(()) -} - fn function_check(a: Const, b: Const) -> Const { if b == Const::Type { Const::Type @@ -66,477 +30,6 @@ pub fn mk_span_err(span: Span, msg: S) -> Result { ) } -fn type_of_binop( - env: &TyEnv, - 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}; - - Ok(match op { - RightBiasedRecordMerge => { - let x_type = l.ty(); - let y_type = r.ty(); - - // 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) - } - 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)) - } - 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)) - } - ListAppend => { - match l.ty().kind() { - ListType(..) => {} - _ => return span_err("BinOpTypeMismatch"), - } - - if l.ty() != r.ty() { - return span_err("BinOpTypeMismatch"); - } - - l.ty().clone() - } - Equivalence => { - 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) - } - 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"), - }); - - if *l.ty() != t { - return span_err("BinOpTypeMismatch"); - } - - if *r.ty() != t { - return span_err("BinOpTypeMismatch"); - } - - t - } - }) -} - -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}; - - let record_type = record.ty(); - let handlers = match record_type.kind() { - RecordType(kts) => kts, - _ => return span_err("Merge1ArgMustBeRecord"), - }; - - 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) - } - _ => 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() { - 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(), - ); - } - - // 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( - 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"); - } - } - } - } - 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"); - } - t1 - } - (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 - PiClosure { annot, closure, .. } => { - if arg.ty().as_nir() != annot { - return mkerr( - ErrorBuilder::new(format!( - "wrong type of function argument" - )) - .span_err( - f.span(), - format!( - "this expects an argument of type: {}", - annot.to_expr_tyenv(env), - ), - ) - .span_err( - arg.span(), - format!( - "but this has type: {}", - arg.ty().to_expr_tyenv(env), - ), - ) - .note(format!( - "expected type `{}`\n found type `{}`", - annot.to_expr_tyenv(env), - arg.ty().to_expr_tyenv(env), - )) - .format(), - ); - } - - let arg_nf = arg.eval(env); - Type::new_infer_universe(env, closure.apply(arg_nf))? - } - _ => return mkerr( - ErrorBuilder::new(format!( - "expected function, found `{}`", - f.ty().to_expr_tyenv(env) - )) - .span_err( - f.span(), - format!("function application requires a function",), - ) - .format(), - ), - } - } - 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"); - } - if y.ty().ty().as_const() != Some(Const::Type) { - return span_err("IfBranchMustBeTerm"); - } - if y.ty() != z.ty() { - return span_err("IfBranchMismatch"); - } - - y.ty().clone() - } - Merge(record, scrut, type_annot) => { - type_of_merge(env, span, record, scrut, type_annot.as_ref())? - } - 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() { - RecordType(kts) => kts, - _ => { - return span_err("The argument to `toMap` must be a record") - } - }; - - if kts.is_empty() { - let annot = if let Some(annot) = annot { - annot - } else { - return span_err( - "`toMap` applied to an empty record requires a type \ - annotation", - ); - }; - let annot_val = annot.eval_to_type(env)?; - - let err_msg = "The type of `toMap x` must be of the form \ - `List { mapKey : Text, mapValue : T }`"; - let arg = match annot_val.kind() { - ListType(t) => t, - _ => return span_err(err_msg), - }; - let kts = match arg.kind() { - RecordType(kts) => kts, - _ => return span_err(err_msg), - }; - if kts.len() != 2 { - return span_err(err_msg); - } - match kts.get(&"mapKey".into()) { - Some(t) if *t == Nir::from_builtin(Builtin::Text) => {} - _ => return span_err(err_msg), - } - match kts.get(&"mapValue".into()) { - Some(_) => {} - None => return span_err(err_msg), - } - annot_val - } else { - let entry_type = kts.iter().next().unwrap().1.clone(); - for (_, t) in kts.iter() { - if *t != entry_type { - return span_err( - "Every field of the record must have the same type", - ); - } - } - - let mut kts = HashMap::new(); - 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(RecordType(kts))) - .to_type(Const::Type); - if let Some(annot) = annot { - let annot_val = annot.eval_to_type(env)?; - if output_type != annot_val { - return span_err("Annotation mismatch"); - } - } - output_type - } - } - 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() { - RecordType(kts) => kts, - _ => return span_err("ProjectionMustBeRecord"), - }; - - let mut new_kts = HashMap::new(); - for l in labels { - match kts.get(l) { - None => return span_err("ProjectionMissingEntry"), - Some(t) => { - use std::collections::hash_map::Entry; - match new_kts.entry(l.clone()) { - Entry::Occupied(_) => { - return span_err("ProjectionDuplicateField") - } - Entry::Vacant(e) => e.insert(t.clone()), - } - } - }; - } - - Type::new_infer_universe(env, Nir::from_kind(RecordType(new_kts)))? - } - ProjectionByExpr(record, selection) => { - let record_type = record.ty(); - let rec_kts = match record_type.kind() { - RecordType(kts) => kts, - _ => return span_err("ProjectionMustBeRecord"), - }; - - let selection_val = selection.eval_to_type(env)?; - let sel_kts = match selection_val.kind() { - RecordType(kts) => kts, - _ => return span_err("ProjectionByExprTakesRecordType"), - }; - - for (l, sel_ty) in sel_kts { - match rec_kts.get(l) { - Some(rec_ty) => { - if rec_ty != sel_ty { - return span_err("ProjectionWrongType"); - } - } - None => return span_err("ProjectionMissingEntry"), - } - } - - selection_val - } - Completion(..) => { - unreachable!("This case should have been handled in resolution") - } - }) -} - /// When all sub-expressions have been typed, check the remaining toplevel /// layer. fn type_one_layer( @@ -690,7 +183,7 @@ fn type_one_layer( Type::from_const(k) } - ExprKind::Op(op) => type_of_operation(env, span, op)?, + ExprKind::Op(op) => typecheck_operation(env, span, op)?, ExprKind::Assert(t) => { let t = t.eval_to_type(env)?; match t.kind() { -- cgit v1.2.3