diff options
-rw-r--r-- | dhall/src/lib.rs | 1 | ||||
-rw-r--r-- | dhall/src/operations.rs | 865 | ||||
-rw-r--r-- | dhall/src/semantics/builtins.rs | 5 | ||||
-rw-r--r-- | dhall/src/semantics/nze/nir.rs | 3 | ||||
-rw-r--r-- | dhall/src/semantics/nze/normalize.rs | 301 | ||||
-rw-r--r-- | dhall/src/semantics/resolve/resolve.rs | 3 | ||||
-rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 515 | ||||
-rw-r--r-- | dhall/src/syntax/ast/expr.rs | 65 | ||||
-rw-r--r-- | dhall/src/syntax/binary/decode.rs | 3 | ||||
-rw-r--r-- | dhall/src/syntax/binary/encode.rs | 5 | ||||
-rw-r--r-- | dhall/src/syntax/text/parser.rs | 2 | ||||
-rw-r--r-- | dhall/src/syntax/text/printer.rs | 11 | ||||
-rw-r--r-- | serde_dhall/src/value.rs | 3 |
13 files changed, 900 insertions, 882 deletions
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 98ad4f0..e00177c 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -11,6 +11,7 @@ mod tests; pub mod error; +pub mod operations; pub mod semantics; pub mod syntax; diff --git a/dhall/src/operations.rs b/dhall/src/operations.rs new file mode 100644 index 0000000..363cd10 --- /dev/null +++ b/dhall/src/operations.rs @@ -0,0 +1,865 @@ +use itertools::Itertools; +use std::borrow::Cow; +use std::cmp::max; +use std::collections::HashMap; + +use crate::error::{ErrorBuilder, TypeError}; +use crate::semantics::{ + merge_maps, mk_span_err, mkerr, ret_kind, ret_op, ret_ref, Binder, Closure, + Hir, HirKind, Nir, NirKind, Ret, TextLit, Tir, TyEnv, Type, +}; +use crate::syntax::map::DupTreeSet; +use crate::syntax::{ + trivial_result, BinOp, Builtin, Const, ExprKind, Label, NumKind, Span, +}; + +/// Operations +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub enum OpKind<SubExpr> { + /// `f a` + App(SubExpr, SubExpr), + /// Binary operations + BinOp(BinOp, SubExpr, SubExpr), + /// `if x then y else z` + BoolIf(SubExpr, SubExpr, SubExpr), + /// `merge x y : t` + Merge(SubExpr, SubExpr, Option<SubExpr>), + /// `toMap x : t` + ToMap(SubExpr, Option<SubExpr>), + /// `e.x` + Field(SubExpr, Label), + /// `e.{ x, y, z }` + Projection(SubExpr, DupTreeSet<Label>), + /// `e.(t)` + ProjectionByExpr(SubExpr, SubExpr), + /// `x::y` + Completion(SubExpr, SubExpr), +} + +impl<SE> OpKind<SE> { + pub fn traverse_ref<'a, SE2, Err>( + &'a self, + mut f: impl FnMut(&'a SE) -> Result<SE2, Err>, + ) -> Result<OpKind<SE2>, Err> { + // Can't use closures because of borrowing rules + macro_rules! expr { + ($e:expr) => { + f($e)? + }; + } + macro_rules! opt { + ($e:expr) => { + $e.as_ref().map(|e| Ok(expr!(e))).transpose()? + }; + } + + use OpKind::*; + Ok(match self { + App(f, a) => App(expr!(f), expr!(a)), + BinOp(o, x, y) => BinOp(*o, expr!(x), expr!(y)), + BoolIf(b, t, f) => BoolIf(expr!(b), expr!(t), expr!(f)), + Merge(x, y, t) => Merge(expr!(x), expr!(y), opt!(t)), + ToMap(x, t) => ToMap(expr!(x), opt!(t)), + Field(e, l) => Field(expr!(e), l.clone()), + Projection(e, ls) => Projection(expr!(e), ls.clone()), + ProjectionByExpr(e, x) => ProjectionByExpr(expr!(e), expr!(x)), + Completion(e, x) => Completion(expr!(e), expr!(x)), + }) + } + + pub fn map_ref<'a, SE2>( + &'a self, + mut f: impl FnMut(&'a SE) -> SE2, + ) -> OpKind<SE2> { + trivial_result(self.traverse_ref(|x| Ok(f(x)))) + } +} + +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 typecheck_binop( + env: &TyEnv, + span: Span, + op: BinOp, + l: &Tir<'_>, + r: &Tir<'_>, +) -> Result<Type, TypeError> { + 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 typecheck_merge( + env: &TyEnv, + span: Span, + record: &Tir<'_>, + scrut: &Tir<'_>, + type_annot: Option<&Tir<'_>>, +) -> Result<Type, TypeError> { + 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"), + }) +} + +pub fn typecheck_operation( + env: &TyEnv, + span: Span, + opkind: &OpKind<Tir<'_>>, +) -> Result<Type, TypeError> { + 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) => typecheck_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) => { + typecheck_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") + } + }) +} + +fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Ret { + use BinOp::*; + use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType}; + use NumKind::{Bool, Natural}; + + match (o, x.kind(), y.kind()) { + (BoolAnd, Num(Bool(true)), _) => ret_ref(y), + (BoolAnd, _, Num(Bool(true))) => ret_ref(x), + (BoolAnd, Num(Bool(false)), _) => ret_kind(Num(Bool(false))), + (BoolAnd, _, Num(Bool(false))) => ret_kind(Num(Bool(false))), + (BoolAnd, _, _) if x == y => ret_ref(x), + (BoolOr, Num(Bool(true)), _) => ret_kind(Num(Bool(true))), + (BoolOr, _, Num(Bool(true))) => ret_kind(Num(Bool(true))), + (BoolOr, Num(Bool(false)), _) => ret_ref(y), + (BoolOr, _, Num(Bool(false))) => ret_ref(x), + (BoolOr, _, _) if x == y => ret_ref(x), + (BoolEQ, Num(Bool(true)), _) => ret_ref(y), + (BoolEQ, _, Num(Bool(true))) => ret_ref(x), + (BoolEQ, Num(Bool(x)), Num(Bool(y))) => ret_kind(Num(Bool(x == y))), + (BoolEQ, _, _) if x == y => ret_kind(Num(Bool(true))), + (BoolNE, Num(Bool(false)), _) => ret_ref(y), + (BoolNE, _, Num(Bool(false))) => ret_ref(x), + (BoolNE, Num(Bool(x)), Num(Bool(y))) => ret_kind(Num(Bool(x != y))), + (BoolNE, _, _) if x == y => ret_kind(Num(Bool(false))), + + (NaturalPlus, Num(Natural(0)), _) => ret_ref(y), + (NaturalPlus, _, Num(Natural(0))) => ret_ref(x), + (NaturalPlus, Num(Natural(x)), Num(Natural(y))) => { + ret_kind(Num(Natural(x + y))) + } + (NaturalTimes, Num(Natural(0)), _) => ret_kind(Num(Natural(0))), + (NaturalTimes, _, Num(Natural(0))) => ret_kind(Num(Natural(0))), + (NaturalTimes, Num(Natural(1)), _) => ret_ref(y), + (NaturalTimes, _, Num(Natural(1))) => ret_ref(x), + (NaturalTimes, Num(Natural(x)), Num(Natural(y))) => { + ret_kind(Num(Natural(x * y))) + } + + (ListAppend, EmptyListLit(_), _) => ret_ref(y), + (ListAppend, _, EmptyListLit(_)) => ret_ref(x), + (ListAppend, NEListLit(xs), NEListLit(ys)) => { + ret_kind(NEListLit(xs.iter().chain(ys.iter()).cloned().collect())) + } + + (TextAppend, NirKind::TextLit(x), _) if x.is_empty() => ret_ref(y), + (TextAppend, _, NirKind::TextLit(y)) if y.is_empty() => ret_ref(x), + (TextAppend, NirKind::TextLit(x), NirKind::TextLit(y)) => { + ret_kind(NirKind::TextLit(x.concat(y))) + } + (TextAppend, NirKind::TextLit(x), _) => ret_kind(NirKind::TextLit( + x.concat(&TextLit::interpolate(y.clone())), + )), + (TextAppend, _, NirKind::TextLit(y)) => ret_kind(NirKind::TextLit( + TextLit::interpolate(x.clone()).concat(y), + )), + + (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { + ret_ref(x) + } + (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { + ret_ref(y) + } + (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { + let mut kvs = kvs2.clone(); + for (x, v) in kvs1 { + // Insert only if key not already present + kvs.entry(x.clone()).or_insert_with(|| v.clone()); + } + ret_kind(RecordLit(kvs)) + } + (RightBiasedRecordMerge, _, _) if x == y => ret_ref(y), + + (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { + ret_ref(x) + } + (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { + ret_ref(y) + } + (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { + let kvs = merge_maps(kvs1, kvs2, |_, v1, v2| { + Nir::from_partial_expr(ExprKind::Op(OpKind::BinOp( + RecursiveRecordMerge, + v1.clone(), + v2.clone(), + ))) + }); + ret_kind(RecordLit(kvs)) + } + + (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => { + let kts = merge_maps( + kts_x, + kts_y, + // If the Label exists for both records, then we hit the recursive case. + |_, l: &Nir, r: &Nir| { + Nir::from_partial_expr(ExprKind::Op(OpKind::BinOp( + RecursiveRecordTypeMerge, + l.clone(), + r.clone(), + ))) + }, + ); + ret_kind(RecordType(kts)) + } + + (Equivalence, _, _) => { + ret_kind(NirKind::Equivalence(x.clone(), y.clone())) + } + + _ => ret_op(OpKind::BinOp(o, x.clone(), y.clone())), + } +} + +fn normalize_field(v: &Nir, field: &Label) -> Ret { + use self::BinOp::{RecursiveRecordMerge, RightBiasedRecordMerge}; + use NirKind::{Op, RecordLit, UnionConstructor, UnionType}; + use OpKind::{BinOp, Field, Projection}; + let nothing_to_do = || ret_op(Field(v.clone(), field.clone())); + + match v.kind() { + RecordLit(kvs) => match kvs.get(field) { + Some(r) => ret_ref(r), + None => nothing_to_do(), + }, + UnionType(kts) => { + ret_kind(UnionConstructor(field.clone(), kts.clone())) + } + Op(Projection(x, _)) => normalize_field(x, field), + Op(BinOp(RightBiasedRecordMerge, x, y)) => match (x.kind(), y.kind()) { + (_, RecordLit(kvs)) => match kvs.get(field) { + Some(r) => ret_ref(r), + None => normalize_field(x, field), + }, + (RecordLit(kvs), _) => match kvs.get(field) { + Some(r) => ret_op(Field( + Nir::from_kind(Op(BinOp( + RightBiasedRecordMerge, + Nir::from_kind(RecordLit( + Some((field.clone(), r.clone())) + .into_iter() + .collect(), + )), + y.clone(), + ))), + field.clone(), + )), + None => normalize_field(y, field), + }, + _ => nothing_to_do(), + }, + Op(BinOp(RecursiveRecordMerge, x, y)) => match (x.kind(), y.kind()) { + (RecordLit(kvs), _) => match kvs.get(field) { + Some(r) => ret_op(Field( + Nir::from_kind(Op(BinOp( + RecursiveRecordMerge, + Nir::from_kind(RecordLit( + Some((field.clone(), r.clone())) + .into_iter() + .collect(), + )), + y.clone(), + ))), + field.clone(), + )), + None => normalize_field(y, field), + }, + (_, RecordLit(kvs)) => match kvs.get(field) { + Some(r) => ret_op(Field( + Nir::from_kind(Op(BinOp( + RecursiveRecordMerge, + x.clone(), + Nir::from_kind(RecordLit( + Some((field.clone(), r.clone())) + .into_iter() + .collect(), + )), + ))), + field.clone(), + )), + None => normalize_field(x, field), + }, + _ => nothing_to_do(), + }, + _ => nothing_to_do(), + } +} + +pub fn normalize_operation(opkind: &OpKind<Nir>) -> Ret { + use NirKind::{ + EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, Op, + RecordLit, RecordType, UnionConstructor, UnionLit, + }; + use NumKind::Bool; + use OpKind::*; + let nothing_to_do = || ret_op(opkind.clone()); + + match opkind { + App(v, a) => ret_kind(v.app_to_kind(a.clone())), + BinOp(o, x, y) => normalize_binop(*o, x, y), + BoolIf(b, e1, e2) => { + match b.kind() { + Num(Bool(true)) => ret_ref(e1), + Num(Bool(false)) => ret_ref(e2), + _ => { + match (e1.kind(), e2.kind()) { + // Simplify `if b then True else False` + (Num(Bool(true)), Num(Bool(false))) => ret_ref(b), + _ if e1 == e2 => ret_ref(e1), + _ => nothing_to_do(), + } + } + } + } + Merge(handlers, variant, _) => match handlers.kind() { + RecordLit(kvs) => match variant.kind() { + UnionConstructor(l, _) => match kvs.get(l) { + Some(h) => ret_ref(h), + None => nothing_to_do(), + }, + UnionLit(l, v, _) => match kvs.get(l) { + Some(h) => ret_kind(h.app_to_kind(v.clone())), + None => nothing_to_do(), + }, + EmptyOptionalLit(_) => match kvs.get(&"None".into()) { + Some(h) => ret_ref(h), + None => nothing_to_do(), + }, + NEOptionalLit(v) => match kvs.get(&"Some".into()) { + Some(h) => ret_kind(h.app_to_kind(v.clone())), + None => nothing_to_do(), + }, + _ => nothing_to_do(), + }, + _ => nothing_to_do(), + }, + ToMap(v, annot) => match v.kind() { + RecordLit(kvs) if kvs.is_empty() => { + match annot.as_ref().map(|v| v.kind()) { + Some(NirKind::ListType(t)) => { + ret_kind(EmptyListLit(t.clone())) + } + _ => nothing_to_do(), + } + } + RecordLit(kvs) => ret_kind(NEListLit( + kvs.iter() + .sorted_by_key(|(k, _)| *k) + .map(|(k, v)| { + let mut rec = HashMap::new(); + rec.insert("mapKey".into(), Nir::from_text(k)); + rec.insert("mapValue".into(), v.clone()); + Nir::from_kind(NirKind::RecordLit(rec)) + }) + .collect(), + )), + _ => nothing_to_do(), + }, + Field(v, field) => normalize_field(v, field), + Projection(_, ls) if ls.is_empty() => { + ret_kind(RecordLit(HashMap::new())) + } + Projection(v, ls) => match v.kind() { + RecordLit(kvs) => ret_kind(RecordLit( + ls.iter() + .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone()))) + .collect(), + )), + Op(Projection(v2, _)) => { + normalize_operation(&Projection(v2.clone(), ls.clone())) + } + _ => nothing_to_do(), + }, + ProjectionByExpr(v, t) => match t.kind() { + RecordType(kts) => normalize_operation(&Projection( + v.clone(), + kts.keys().cloned().collect(), + )), + _ => nothing_to_do(), + }, + Completion(..) => { + unreachable!("This case should have been handled in resolution") + } + } +} diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index 45be448..f65e8d1 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -1,3 +1,4 @@ +use crate::operations::OpKind; use crate::semantics::{ skip_resolve_expr, typecheck, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv, }; @@ -5,8 +6,8 @@ use crate::syntax::map::DupTreeMap; use crate::syntax::Const::Type; use crate::syntax::{ BinOp, Builtin, Const, Expr, ExprKind, InterpolatedText, - InterpolatedTextContents, Label, NaiveDouble, NumKind, OpKind, Span, - UnspannedExpr, V, + InterpolatedTextContents, Label, NaiveDouble, NumKind, Span, UnspannedExpr, + V, }; use std::collections::HashMap; use std::convert::TryInto; diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs index 88123d8..5c67c02 100644 --- a/dhall/src/semantics/nze/nir.rs +++ b/dhall/src/semantics/nze/nir.rs @@ -1,6 +1,7 @@ use std::collections::HashMap; use std::rc::Rc; +use crate::operations::OpKind; use crate::semantics::nze::lazy; use crate::semantics::{ apply_any, normalize_hir, normalize_one_layer, squash_textlit, Binder, @@ -8,7 +9,7 @@ use crate::semantics::{ }; use crate::syntax::{ BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, - NumKind, OpKind, Span, + NumKind, Span, }; use crate::ToExprOptions; diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index c0e41cb..d042f3f 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -1,11 +1,9 @@ -use itertools::Itertools; use std::collections::HashMap; +use crate::operations::{normalize_operation, OpKind}; use crate::semantics::NzEnv; use crate::semantics::{Binder, Closure, Hir, HirKind, Nir, NirKind, TextLit}; -use crate::syntax::{ - BinOp, ExprKind, InterpolatedTextContents, Label, NumKind, OpKind, -}; +use crate::syntax::{ExprKind, InterpolatedTextContents}; pub fn apply_any(f: &Nir, a: Nir) -> NirKind { match f.kind() { @@ -83,306 +81,21 @@ where kvs } -type Ret = NirKind; +pub type Ret = NirKind; -fn ret_nir(x: Nir) -> Ret { +pub fn ret_nir(x: Nir) -> Ret { ret_ref(&x) } -fn ret_kind(x: NirKind) -> Ret { +pub fn ret_kind(x: NirKind) -> Ret { x } -fn ret_ref(x: &Nir) -> Ret { +pub fn ret_ref(x: &Nir) -> Ret { x.kind().clone() } -fn ret_op(x: OpKind<Nir>) -> Ret { +pub fn ret_op(x: OpKind<Nir>) -> Ret { NirKind::Op(x) } -fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Ret { - use BinOp::*; - use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType}; - use NumKind::{Bool, Natural}; - - match (o, x.kind(), y.kind()) { - (BoolAnd, Num(Bool(true)), _) => ret_ref(y), - (BoolAnd, _, Num(Bool(true))) => ret_ref(x), - (BoolAnd, Num(Bool(false)), _) => ret_kind(Num(Bool(false))), - (BoolAnd, _, Num(Bool(false))) => ret_kind(Num(Bool(false))), - (BoolAnd, _, _) if x == y => ret_ref(x), - (BoolOr, Num(Bool(true)), _) => ret_kind(Num(Bool(true))), - (BoolOr, _, Num(Bool(true))) => ret_kind(Num(Bool(true))), - (BoolOr, Num(Bool(false)), _) => ret_ref(y), - (BoolOr, _, Num(Bool(false))) => ret_ref(x), - (BoolOr, _, _) if x == y => ret_ref(x), - (BoolEQ, Num(Bool(true)), _) => ret_ref(y), - (BoolEQ, _, Num(Bool(true))) => ret_ref(x), - (BoolEQ, Num(Bool(x)), Num(Bool(y))) => ret_kind(Num(Bool(x == y))), - (BoolEQ, _, _) if x == y => ret_kind(Num(Bool(true))), - (BoolNE, Num(Bool(false)), _) => ret_ref(y), - (BoolNE, _, Num(Bool(false))) => ret_ref(x), - (BoolNE, Num(Bool(x)), Num(Bool(y))) => ret_kind(Num(Bool(x != y))), - (BoolNE, _, _) if x == y => ret_kind(Num(Bool(false))), - - (NaturalPlus, Num(Natural(0)), _) => ret_ref(y), - (NaturalPlus, _, Num(Natural(0))) => ret_ref(x), - (NaturalPlus, Num(Natural(x)), Num(Natural(y))) => { - ret_kind(Num(Natural(x + y))) - } - (NaturalTimes, Num(Natural(0)), _) => ret_kind(Num(Natural(0))), - (NaturalTimes, _, Num(Natural(0))) => ret_kind(Num(Natural(0))), - (NaturalTimes, Num(Natural(1)), _) => ret_ref(y), - (NaturalTimes, _, Num(Natural(1))) => ret_ref(x), - (NaturalTimes, Num(Natural(x)), Num(Natural(y))) => { - ret_kind(Num(Natural(x * y))) - } - - (ListAppend, EmptyListLit(_), _) => ret_ref(y), - (ListAppend, _, EmptyListLit(_)) => ret_ref(x), - (ListAppend, NEListLit(xs), NEListLit(ys)) => { - ret_kind(NEListLit(xs.iter().chain(ys.iter()).cloned().collect())) - } - - (TextAppend, NirKind::TextLit(x), _) if x.is_empty() => ret_ref(y), - (TextAppend, _, NirKind::TextLit(y)) if y.is_empty() => ret_ref(x), - (TextAppend, NirKind::TextLit(x), NirKind::TextLit(y)) => { - ret_kind(NirKind::TextLit(x.concat(y))) - } - (TextAppend, NirKind::TextLit(x), _) => ret_kind(NirKind::TextLit( - x.concat(&TextLit::interpolate(y.clone())), - )), - (TextAppend, _, NirKind::TextLit(y)) => ret_kind(NirKind::TextLit( - TextLit::interpolate(x.clone()).concat(y), - )), - - (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - ret_ref(x) - } - (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - ret_ref(y) - } - (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let mut kvs = kvs2.clone(); - for (x, v) in kvs1 { - // Insert only if key not already present - kvs.entry(x.clone()).or_insert_with(|| v.clone()); - } - ret_kind(RecordLit(kvs)) - } - (RightBiasedRecordMerge, _, _) if x == y => ret_ref(y), - - (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - ret_ref(x) - } - (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - ret_ref(y) - } - (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let kvs = merge_maps(kvs1, kvs2, |_, v1, v2| { - Nir::from_partial_expr(ExprKind::Op(OpKind::BinOp( - RecursiveRecordMerge, - v1.clone(), - v2.clone(), - ))) - }); - ret_kind(RecordLit(kvs)) - } - - (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => { - let kts = merge_maps( - kts_x, - kts_y, - // If the Label exists for both records, then we hit the recursive case. - |_, l: &Nir, r: &Nir| { - Nir::from_partial_expr(ExprKind::Op(OpKind::BinOp( - RecursiveRecordTypeMerge, - l.clone(), - r.clone(), - ))) - }, - ); - ret_kind(RecordType(kts)) - } - - (Equivalence, _, _) => { - ret_kind(NirKind::Equivalence(x.clone(), y.clone())) - } - - _ => ret_op(OpKind::BinOp(o, x.clone(), y.clone())), - } -} - -fn normalize_field(v: &Nir, field: &Label) -> Ret { - use self::BinOp::{RecursiveRecordMerge, RightBiasedRecordMerge}; - use NirKind::{Op, RecordLit, UnionConstructor, UnionType}; - use OpKind::{BinOp, Field, Projection}; - let nothing_to_do = || ret_op(Field(v.clone(), field.clone())); - - match v.kind() { - RecordLit(kvs) => match kvs.get(field) { - Some(r) => ret_ref(r), - None => nothing_to_do(), - }, - UnionType(kts) => { - ret_kind(UnionConstructor(field.clone(), kts.clone())) - } - Op(Projection(x, _)) => normalize_field(x, field), - Op(BinOp(RightBiasedRecordMerge, x, y)) => match (x.kind(), y.kind()) { - (_, RecordLit(kvs)) => match kvs.get(field) { - Some(r) => ret_ref(r), - None => normalize_field(x, field), - }, - (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => ret_op(Field( - Nir::from_kind(Op(BinOp( - RightBiasedRecordMerge, - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - y.clone(), - ))), - field.clone(), - )), - None => normalize_field(y, field), - }, - _ => nothing_to_do(), - }, - Op(BinOp(RecursiveRecordMerge, x, y)) => match (x.kind(), y.kind()) { - (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => ret_op(Field( - Nir::from_kind(Op(BinOp( - RecursiveRecordMerge, - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - y.clone(), - ))), - field.clone(), - )), - None => normalize_field(y, field), - }, - (_, RecordLit(kvs)) => match kvs.get(field) { - Some(r) => ret_op(Field( - Nir::from_kind(Op(BinOp( - RecursiveRecordMerge, - x.clone(), - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - ))), - field.clone(), - )), - None => normalize_field(x, field), - }, - _ => nothing_to_do(), - }, - _ => nothing_to_do(), - } -} - -fn normalize_operation(opkind: &OpKind<Nir>) -> Ret { - use NirKind::{ - EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, Op, - RecordLit, RecordType, UnionConstructor, UnionLit, - }; - use NumKind::Bool; - use OpKind::*; - let nothing_to_do = || ret_op(opkind.clone()); - - match opkind { - App(v, a) => ret_kind(v.app_to_kind(a.clone())), - BinOp(o, x, y) => normalize_binop(*o, x, y), - BoolIf(b, e1, e2) => { - match b.kind() { - Num(Bool(true)) => ret_ref(e1), - Num(Bool(false)) => ret_ref(e2), - _ => { - match (e1.kind(), e2.kind()) { - // Simplify `if b then True else False` - (Num(Bool(true)), Num(Bool(false))) => ret_ref(b), - _ if e1 == e2 => ret_ref(e1), - _ => nothing_to_do(), - } - } - } - } - Merge(handlers, variant, _) => match handlers.kind() { - RecordLit(kvs) => match variant.kind() { - UnionConstructor(l, _) => match kvs.get(l) { - Some(h) => ret_ref(h), - None => nothing_to_do(), - }, - UnionLit(l, v, _) => match kvs.get(l) { - Some(h) => ret_kind(h.app_to_kind(v.clone())), - None => nothing_to_do(), - }, - EmptyOptionalLit(_) => match kvs.get(&"None".into()) { - Some(h) => ret_ref(h), - None => nothing_to_do(), - }, - NEOptionalLit(v) => match kvs.get(&"Some".into()) { - Some(h) => ret_kind(h.app_to_kind(v.clone())), - None => nothing_to_do(), - }, - _ => nothing_to_do(), - }, - _ => nothing_to_do(), - }, - ToMap(v, annot) => match v.kind() { - RecordLit(kvs) if kvs.is_empty() => { - match annot.as_ref().map(|v| v.kind()) { - Some(NirKind::ListType(t)) => { - ret_kind(EmptyListLit(t.clone())) - } - _ => nothing_to_do(), - } - } - RecordLit(kvs) => ret_kind(NEListLit( - kvs.iter() - .sorted_by_key(|(k, _)| *k) - .map(|(k, v)| { - let mut rec = HashMap::new(); - rec.insert("mapKey".into(), Nir::from_text(k)); - rec.insert("mapValue".into(), v.clone()); - Nir::from_kind(NirKind::RecordLit(rec)) - }) - .collect(), - )), - _ => nothing_to_do(), - }, - Field(v, field) => normalize_field(v, field), - Projection(_, ls) if ls.is_empty() => { - ret_kind(RecordLit(HashMap::new())) - } - Projection(v, ls) => match v.kind() { - RecordLit(kvs) => ret_kind(RecordLit( - ls.iter() - .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone()))) - .collect(), - )), - Op(Projection(v2, _)) => { - normalize_operation(&Projection(v2.clone(), ls.clone())) - } - _ => nothing_to_do(), - }, - ProjectionByExpr(v, t) => match t.kind() { - RecordType(kts) => normalize_operation(&Projection( - v.clone(), - kts.keys().cloned().collect(), - )), - _ => nothing_to_do(), - }, - Completion(..) => { - unreachable!("This case should have been handled in resolution") - } - } -} - pub fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind { use NirKind::{ Assert, Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType, diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs index 3e0022f..bbcd240 100644 --- a/dhall/src/semantics/resolve/resolve.rs +++ b/dhall/src/semantics/resolve/resolve.rs @@ -6,12 +6,13 @@ use url::Url; use crate::error::ErrorBuilder; use crate::error::{Error, ImportError}; +use crate::operations::OpKind; use crate::semantics::{mkerr, Hir, HirKind, ImportEnv, NameEnv, Type}; use crate::syntax; use crate::syntax::map::DupTreeMap; use crate::syntax::{ BinOp, Builtin, Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, - ImportTarget, OpKind, Span, UnspannedExpr, URL, + ImportTarget, Span, UnspannedExpr, URL, }; use crate::{Parsed, Resolved}; 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<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> { ) } -fn type_of_binop( - env: &TyEnv, - span: Span, - op: BinOp, - l: &Tir<'_>, - r: &Tir<'_>, -) -> Result<Type, TypeError> { - 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<Type, TypeError> { - 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<Tir<'_>>, -) -> Result<Type, TypeError> { - 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() { diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs index 51e9ea7..62734bf 100644 --- a/dhall/src/syntax/ast/expr.rs +++ b/dhall/src/syntax/ast/expr.rs @@ -1,8 +1,9 @@ use std::collections::BTreeMap; use crate::error::Error; +use crate::operations::OpKind; use crate::semantics::Universe; -use crate::syntax::map::{DupTreeMap, DupTreeSet}; +use crate::syntax::map::DupTreeMap; use crate::syntax::visitor; use crate::syntax::*; @@ -126,29 +127,6 @@ pub enum NumKind { Double(Double), } -/// Operations -#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] -pub enum OpKind<SubExpr> { - /// `f a` - App(SubExpr, SubExpr), - /// Binary operations - BinOp(BinOp, SubExpr, SubExpr), - /// `if x then y else z` - BoolIf(SubExpr, SubExpr, SubExpr), - /// `merge x y : t` - Merge(SubExpr, SubExpr, Option<SubExpr>), - /// `toMap x : t` - ToMap(SubExpr, Option<SubExpr>), - /// `e.x` - Field(SubExpr, Label), - /// `e.{ x, y, z }` - Projection(SubExpr, DupTreeSet<Label>), - /// `e.(t)` - ProjectionByExpr(SubExpr, SubExpr), - /// `x::y` - Completion(SubExpr, SubExpr), -} - /// Syntax tree for expressions // Having the recursion out of the enum definition enables writing // much more generic code and improves pattern-matching behind @@ -249,45 +227,6 @@ impl<SE> ExprKind<SE> { } } -impl<SE> OpKind<SE> { - pub fn traverse_ref<'a, SE2, Err>( - &'a self, - mut f: impl FnMut(&'a SE) -> Result<SE2, Err>, - ) -> Result<OpKind<SE2>, Err> { - // Can't use closures because of borrowing rules - macro_rules! expr { - ($e:expr) => { - f($e)? - }; - } - macro_rules! opt { - ($e:expr) => { - $e.as_ref().map(|e| Ok(expr!(e))).transpose()? - }; - } - - use OpKind::*; - Ok(match self { - App(f, a) => App(expr!(f), expr!(a)), - BinOp(o, x, y) => BinOp(*o, expr!(x), expr!(y)), - BoolIf(b, t, f) => BoolIf(expr!(b), expr!(t), expr!(f)), - Merge(x, y, t) => Merge(expr!(x), expr!(y), opt!(t)), - ToMap(x, t) => ToMap(expr!(x), opt!(t)), - Field(e, l) => Field(expr!(e), l.clone()), - Projection(e, ls) => Projection(expr!(e), ls.clone()), - ProjectionByExpr(e, x) => ProjectionByExpr(expr!(e), expr!(x)), - Completion(e, x) => Completion(expr!(e), expr!(x)), - }) - } - - pub fn map_ref<'a, SE2>( - &'a self, - mut f: impl FnMut(&'a SE) -> SE2, - ) -> OpKind<SE2> { - trivial_result(self.traverse_ref(|x| Ok(f(x)))) - } -} - impl Expr { pub fn as_ref(&self) -> &UnspannedExpr { &self.kind diff --git a/dhall/src/syntax/binary/decode.rs b/dhall/src/syntax/binary/decode.rs index b183f6c..f062089 100644 --- a/dhall/src/syntax/binary/decode.rs +++ b/dhall/src/syntax/binary/decode.rs @@ -3,10 +3,11 @@ use serde_cbor::value::value as cbor; use std::iter::FromIterator; use crate::error::DecodeError; +use crate::operations::OpKind; use crate::syntax; use crate::syntax::{ Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, ImportTarget, - Integer, InterpolatedText, Label, Natural, NumKind, OpKind, Scheme, Span, + Integer, InterpolatedText, Label, Natural, NumKind, Scheme, Span, UnspannedExpr, URL, V, }; type DecodedExpr = Expr; diff --git a/dhall/src/syntax/binary/encode.rs b/dhall/src/syntax/binary/encode.rs index f2bc6f1..cef2af8 100644 --- a/dhall/src/syntax/binary/encode.rs +++ b/dhall/src/syntax/binary/encode.rs @@ -3,11 +3,12 @@ use std::collections::BTreeMap; use std::vec; use crate::error::EncodeError; +use crate::operations::OpKind; use crate::syntax; use crate::syntax::map::DupTreeMap; use crate::syntax::{ Expr, ExprKind, FilePrefix, Hash, Import, ImportMode, ImportTarget, Label, - OpKind, Scheme, V, + Scheme, V, }; pub fn encode(expr: &Expr) -> Result<Vec<u8>, EncodeError> { @@ -49,7 +50,7 @@ where use syntax::Builtin; use syntax::ExprKind::*; use syntax::NumKind::*; - use syntax::OpKind::*; + use OpKind::*; use self::Serialize::{RecordDupMap, RecordMap, UnionMap}; fn expr(x: &Expr) -> self::Serialize<'_> { diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs index ab9bc24..8d76225 100644 --- a/dhall/src/syntax/text/parser.rs +++ b/dhall/src/syntax/text/parser.rs @@ -7,10 +7,10 @@ use std::rc::Rc; use pest_consume::{match_nodes, Parser}; +use crate::operations::OpKind::*; use crate::syntax::map::{DupTreeMap, DupTreeSet}; use crate::syntax::ExprKind::*; use crate::syntax::NumKind::*; -use crate::syntax::OpKind::*; use crate::syntax::{ Double, Expr, FilePath, FilePrefix, Hash, ImportMode, ImportTarget, Integer, InterpolatedText, InterpolatedTextContents, Label, NaiveDouble, diff --git a/dhall/src/syntax/text/printer.rs b/dhall/src/syntax/text/printer.rs index d655489..a85f435 100644 --- a/dhall/src/syntax/text/printer.rs +++ b/dhall/src/syntax/text/printer.rs @@ -1,3 +1,4 @@ +use crate::operations::OpKind; use crate::syntax::*; use itertools::Itertools; use std::fmt::{self, Display}; @@ -37,8 +38,8 @@ impl<'a> PhasedExpr<'a> { impl UnspannedExpr { // Annotate subexpressions with the appropriate phase, defaulting to Base fn annotate_with_phases(&self) -> ExprKind<PhasedExpr<'_>> { - use crate::syntax::ExprKind::*; - use crate::syntax::OpKind::*; + use ExprKind::*; + use OpKind::*; use PrintPhase::*; let with_base = self.map_ref(|e| PhasedExpr(e, Base)); match with_base { @@ -89,8 +90,8 @@ impl UnspannedExpr { f: &mut fmt::Formatter, phase: PrintPhase, ) -> Result<(), fmt::Error> { - use crate::syntax::ExprKind::*; - use crate::syntax::OpKind::*; + use ExprKind::*; + use OpKind::*; let needs_paren = match self { Lam(_, _, _) @@ -212,7 +213,7 @@ impl<SE: Display + Clone> Display for ExprKind<SE> { /// Generic instance that delegates to subexpressions impl<SE: Display + Clone> Display for OpKind<SE> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { - use crate::syntax::OpKind::*; + use OpKind::*; match self { App(a, b) => { write!(f, "{} {}", a, b)?; diff --git a/serde_dhall/src/value.rs b/serde_dhall/src/value.rs index 587349c..e8f333e 100644 --- a/serde_dhall/src/value.rs +++ b/serde_dhall/src/value.rs @@ -1,7 +1,8 @@ use std::collections::{BTreeMap, HashMap}; +use dhall::operations::OpKind; use dhall::semantics::{Hir, HirKind, Nir, NirKind}; -use dhall::syntax::{Builtin, Expr, ExprKind, NumKind, OpKind, Span}; +use dhall::syntax::{Builtin, Expr, ExprKind, NumKind, Span}; use crate::{Error, ErrorKind, FromDhall, Result, Sealed}; |