Merge pull request #159 from Nadrieril/operations

Factor out operations

2 files changed, 51 insertions, 555 deletions

diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs
index 89a8027..ec15a1f 100644
--- a/dhall/src/semantics/tck/tir.rs
+++ b/dhall/src/semantics/tck/tir.rs
@@ -1,6 +1,7 @@
+use crate::builtins::Builtin;
 use crate::error::{ErrorBuilder, TypeError};
 use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv};
-use crate::syntax::{Builtin, Const, Expr, Span};
+use crate::syntax::{Const, Expr, Span};
 
 /// The type of a type. 0 is `Type`, 1 is `Kind`, etc...
 #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)]
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index c3334b5..361e1b4 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -1,49 +1,10 @@
-use std::borrow::Cow;
 use std::cmp::max;
-use std::collections::HashMap;
 
+use crate::builtins::{type_of_builtin, Builtin};
 use crate::error::{ErrorBuilder, TypeError, TypeMessage};
-use crate::semantics::merge_maps;
-use crate::semantics::{
-    type_of_builtin, Binder, Closure, Hir, HirKind, Nir, NirKind, Tir, TyEnv,
-    Type,
-};
-use crate::syntax::{
-    BinOp, 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(())
-}
+use crate::operations::typecheck_operation;
+use crate::semantics::{Hir, HirKind, Nir, NirKind, Tir, TyEnv, Type};
+use crate::syntax::{Const, ExprKind, InterpolatedTextContents, NumKind, Span};
 
 fn function_check(a: Const, b: Const) -> Const {
     if b == Const::Type {
@@ -74,8 +35,8 @@ fn type_one_layer(
 ) -> Result<Type, TypeError> {
     let span_err = |msg: &str| mk_span_err(span.clone(), msg);
 
-    let ty = match &ekind {
-        ExprKind::Import(..) | ExprKind::Completion(..) => {
+    Ok(match &ekind {
+        ExprKind::Import(..) => {
             unreachable!("This case should have been handled in resolution")
         }
         ExprKind::Var(..)
@@ -89,20 +50,16 @@ fn type_one_layer(
 
         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::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)
-        }
         ExprKind::TextLit(interpolated) => {
             let text_type = Type::from_builtin(Builtin::Text);
             for contents in interpolated.iter() {
@@ -115,6 +72,16 @@ fn type_one_layer(
             }
             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() {
@@ -138,82 +105,56 @@ fn type_one_layer(
             let t = x.ty().to_nir();
             Nir::from_builtin(Builtin::List).app(t).to_type(Const::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::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()),
-                };
-
+            for v in kvs.values() {
                 // 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"),
+                    None => return mk_span_err(v.span(), "InvalidFieldType"),
                 }
             }
 
+            let kts = kvs
+                .iter()
+                .map(|(x, v)| (x.clone(), v.ty().to_nir()))
+                .collect();
+
             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(()),
-                };
-
+            for t in kts.values() {
                 // 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"),
+                    None => return mk_span_err(t.span(), "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 {
+            for t in kts.values() {
                 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"),
+                    let c = match t.ty().as_const() {
+                        Some(c) => c,
+                        None => {
+                            return mk_span_err(t.span(), "InvalidVariantType")
+                        }
+                    };
+                    match k {
+                        None => k = Some(c),
+                        Some(k) if k == c => {}
+                        _ => {
+                            return mk_span_err(t.span(), "InvalidVariantType")
+                        }
                     }
                 }
-                match seen_fields.entry(x) {
-                    Entry::Occupied(_) => {
-                        return span_err("UnionTypeDuplicateField")
-                    }
-                    Entry::Vacant(e) => e.insert(()),
-                };
             }
 
             // An empty union type has type Type;
@@ -222,36 +163,7 @@ fn type_one_layer(
 
             Type::from_const(k)
         }
-        ExprKind::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"),
-                    }
-                }
-                _ => return span_err("NotARecord"),
-            }
-        }
+        ExprKind::Op(op) => typecheck_operation(env, span, op)?,
         ExprKind::Assert(t) => {
             let t = t.eval_to_type(env)?;
             match t.kind() {
@@ -261,430 +173,13 @@ fn type_one_layer(
             }
             t
         }
-        ExprKind::App(f, arg) => {
-            match f.ty().kind() {
-                // TODO: store Type in closure
-                NirKind::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(),
-                ),
-            }
-        }
-        ExprKind::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()
-        }
-        ExprKind::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)
-        }
-        ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
-            check_rectymerge(&span, env, x.ty().to_nir(), y.ty().to_nir())?;
-
-            let hir = Hir::new(
-                HirKind::Expr(ExprKind::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::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::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::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::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::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::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,
-                _ => {
-                    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() {
-                    NirKind::ListType(t) => t,
-                    _ => return span_err(err_msg),
-                };
-                let kts = match arg.kind() {
-                    NirKind::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(NirKind::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
-            }
-        }
-        ExprKind::Projection(record, labels) => {
-            let record_type = record.ty();
-            let kts = match record_type.kind() {
-                NirKind::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(NirKind::RecordType(new_kts)),
-            )?
-        }
-        ExprKind::ProjectionByExpr(record, selection) => {
-            let record_type = record.ty();
-            let rec_kts = match record_type.kind() {
-                NirKind::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,
-                _ => 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
-        }
-    };
-
-    Ok(ty)
+    })
 }
 
 /// `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,
@@ -780,7 +275,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<Tir<'hir>, TypeError> {
     type_with(&TyEnv::new(), hir, None)