summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/lib.rs1
-rw-r--r--dhall/src/operations.rs865
-rw-r--r--dhall/src/semantics/builtins.rs5
-rw-r--r--dhall/src/semantics/nze/nir.rs3
-rw-r--r--dhall/src/semantics/nze/normalize.rs301
-rw-r--r--dhall/src/semantics/resolve/resolve.rs3
-rw-r--r--dhall/src/semantics/tck/typecheck.rs515
-rw-r--r--dhall/src/syntax/ast/expr.rs65
-rw-r--r--dhall/src/syntax/binary/decode.rs3
-rw-r--r--dhall/src/syntax/binary/encode.rs5
-rw-r--r--dhall/src/syntax/text/parser.rs2
-rw-r--r--dhall/src/syntax/text/printer.rs11
12 files changed, 898 insertions, 881 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)?;
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 19:38:16 +0000