summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck/typecheck.rs
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/tck/typecheck.rs603
1 files changed, 49 insertions, 554 deletions
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)
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 13:50:17 +0000