diff options
38 files changed, 1537 insertions, 1712 deletions
diff --git a/dhall/build.rs b/dhall/build.rs index 784ce93..893a4f9 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -308,9 +308,6 @@ fn generate_tests() -> std::io::Result<()> { || path == "simple/integerToDouble" // TODO: fix Double/show || path == "prelude/JSON/number/1" - // TODO: Further record simplifications - || path == "simplifications/issue661" - || path == "unit/RightBiasedRecordMergeWithinRecordProjection" }), output_type: Some(FileType::Text), ..default_feature.clone() diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/builtins.rs index 6007a92..67929a0 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/builtins.rs @@ -1,15 +1,91 @@ +use std::collections::{BTreeMap, HashMap}; +use std::convert::TryInto; + +use crate::operations::{BinOp, OpKind}; use crate::semantics::{ skip_resolve_expr, typecheck, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv, }; -use crate::syntax::map::DupTreeMap; use crate::syntax::Const::Type; use crate::syntax::{ - BinOp, Builtin, Const, Expr, ExprKind, InterpolatedText, - InterpolatedTextContents, Label, NaiveDouble, NumKind, Span, UnspannedExpr, - V, + Const, Expr, ExprKind, InterpolatedText, InterpolatedTextContents, Label, + NaiveDouble, NumKind, Span, UnspannedExpr, V, }; -use std::collections::HashMap; -use std::convert::TryInto; + +/// Built-ins +#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] +pub enum Builtin { + Bool, + Natural, + Integer, + Double, + Text, + List, + Optional, + OptionalNone, + NaturalBuild, + NaturalFold, + NaturalIsZero, + NaturalEven, + NaturalOdd, + NaturalToInteger, + NaturalShow, + NaturalSubtract, + IntegerToDouble, + IntegerShow, + IntegerNegate, + IntegerClamp, + DoubleShow, + ListBuild, + ListFold, + ListLength, + ListHead, + ListLast, + ListIndexed, + ListReverse, + OptionalFold, + OptionalBuild, + TextShow, +} + +impl Builtin { + pub fn parse(s: &str) -> Option<Self> { + use Builtin::*; + match s { + "Bool" => Some(Bool), + "Natural" => Some(Natural), + "Integer" => Some(Integer), + "Double" => Some(Double), + "Text" => Some(Text), + "List" => Some(List), + "Optional" => Some(Optional), + "None" => Some(OptionalNone), + "Natural/build" => Some(NaturalBuild), + "Natural/fold" => Some(NaturalFold), + "Natural/isZero" => Some(NaturalIsZero), + "Natural/even" => Some(NaturalEven), + "Natural/odd" => Some(NaturalOdd), + "Natural/toInteger" => Some(NaturalToInteger), + "Natural/show" => Some(NaturalShow), + "Natural/subtract" => Some(NaturalSubtract), + "Integer/toDouble" => Some(IntegerToDouble), + "Integer/show" => Some(IntegerShow), + "Integer/negate" => Some(IntegerNegate), + "Integer/clamp" => Some(IntegerClamp), + "Double/show" => Some(DoubleShow), + "List/build" => Some(ListBuild), + "List/fold" => Some(ListFold), + "List/length" => Some(ListLength), + "List/head" => Some(ListHead), + "List/last" => Some(ListLast), + "List/indexed" => Some(ListIndexed), + "List/reverse" => Some(ListReverse), + "Optional/fold" => Some(OptionalFold), + "Optional/build" => Some(OptionalBuild), + "Text/show" => Some(TextShow), + _ => None, + } + } +} /// A partially applied builtin. /// Invariant: the evaluation of the given args must not be able to progress further @@ -34,10 +110,10 @@ impl BuiltinClosure { HirKind::Expr(self.args.iter().fold( ExprKind::Builtin(self.b), |acc, v| { - ExprKind::App( + ExprKind::Op(OpKind::App( Hir::new(HirKind::Expr(acc), Span::Artificial), v.to_hir(venv), - ) + )) }, )) } @@ -59,19 +135,19 @@ macro_rules! make_type { rc(ExprKind::Var(V(stringify!($var).into(), 0))) }; (Optional $ty:ident) => { - rc(ExprKind::App( + rc(ExprKind::Op(OpKind::App( rc(ExprKind::Builtin(Builtin::Optional)), make_type!($ty) - )) + ))) }; (List $($rest:tt)*) => { - rc(ExprKind::App( + rc(ExprKind::Op(OpKind::App( rc(ExprKind::Builtin(Builtin::List)), make_type!($($rest)*) - )) + ))) }; ({ $($label:ident : $ty:ident),* }) => {{ - let mut kts = DupTreeMap::new(); + let mut kts = BTreeMap::new(); $( kts.insert( Label::from(stringify!($label)), @@ -214,10 +290,10 @@ macro_rules! make_closure { }; (List $($ty:tt)*) => {{ let ty = make_closure!($($ty)*); - rc(ExprKind::App( + rc(ExprKind::Op(OpKind::App( rc(ExprKind::Builtin(Builtin::List)), ty - )) + ))) }}; (Some($($v:tt)*)) => { rc(ExprKind::SomeLit( @@ -225,20 +301,20 @@ macro_rules! make_closure { )) }; (1 + $($v:tt)*) => { - rc(ExprKind::BinOp( + rc(ExprKind::Op(OpKind::BinOp( BinOp::NaturalPlus, make_closure!($($v)*), rc(ExprKind::Num(NumKind::Natural(1))) - )) + ))) }; ([ $($head:tt)* ] # $($tail:tt)*) => {{ let head = make_closure!($($head)*); let tail = make_closure!($($tail)*); - rc(ExprKind::BinOp( + rc(ExprKind::Op(OpKind::BinOp( BinOp::ListAppend, rc(ExprKind::NEListLit(vec![head])), tail, - )) + ))) }}; } @@ -491,3 +567,42 @@ impl std::cmp::PartialEq for BuiltinClosure { } } impl std::cmp::Eq for BuiltinClosure {} + +impl std::fmt::Display for Builtin { + fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { + use Builtin::*; + f.write_str(match *self { + Bool => "Bool", + Natural => "Natural", + Integer => "Integer", + Double => "Double", + Text => "Text", + List => "List", + Optional => "Optional", + OptionalNone => "None", + NaturalBuild => "Natural/build", + NaturalFold => "Natural/fold", + NaturalIsZero => "Natural/isZero", + NaturalEven => "Natural/even", + NaturalOdd => "Natural/odd", + NaturalToInteger => "Natural/toInteger", + NaturalShow => "Natural/show", + NaturalSubtract => "Natural/subtract", + IntegerToDouble => "Integer/toDouble", + IntegerNegate => "Integer/negate", + IntegerClamp => "Integer/clamp", + IntegerShow => "Integer/show", + DoubleShow => "Double/show", + ListBuild => "List/build", + ListFold => "List/fold", + ListLength => "List/length", + ListHead => "List/head", + ListLast => "List/last", + ListIndexed => "List/indexed", + ListReverse => "List/reverse", + OptionalFold => "Optional/fold", + OptionalBuild => "Optional/build", + TextShow => "Text/show", + }) + } +} diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 98ad4f0..61327cb 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -10,7 +10,9 @@ mod tests; +pub mod builtins; pub mod error; +pub mod operations; pub mod semantics; pub mod syntax; diff --git a/dhall/src/operations/kind.rs b/dhall/src/operations/kind.rs new file mode 100644 index 0000000..5415637 --- /dev/null +++ b/dhall/src/operations/kind.rs @@ -0,0 +1,97 @@ +use std::collections::BTreeSet; + +use crate::syntax::{trivial_result, Label}; + +// Definition order must match precedence order for +// pretty-printing to work correctly +#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub enum BinOp { + /// `x ? y` + ImportAlt, + /// `x || y` + BoolOr, + /// `x + y` + NaturalPlus, + /// `x ++ y` + TextAppend, + /// `x # y` + ListAppend, + /// `x && y` + BoolAnd, + /// `x ∧ y` + RecursiveRecordMerge, + /// `x ⫽ y` + RightBiasedRecordMerge, + /// `x ⩓ y` + RecursiveRecordTypeMerge, + /// `x * y` + NaturalTimes, + /// `x == y` + BoolEQ, + /// `x != y` + BoolNE, + /// x === y + Equivalence, +} + +/// 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, BTreeSet<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)))) + } +} diff --git a/dhall/src/operations/mod.rs b/dhall/src/operations/mod.rs new file mode 100644 index 0000000..1a3b65b --- /dev/null +++ b/dhall/src/operations/mod.rs @@ -0,0 +1,6 @@ +mod kind; +mod normalization; +mod typecheck; +pub use kind::*; +pub use normalization::*; +pub use typecheck::*; diff --git a/dhall/src/operations/normalization.rs b/dhall/src/operations/normalization.rs new file mode 100644 index 0000000..e3a9415 --- /dev/null +++ b/dhall/src/operations/normalization.rs @@ -0,0 +1,306 @@ +use itertools::Itertools; +use std::collections::HashMap; +use std::iter::once; + +use crate::operations::{BinOp, OpKind}; +use crate::semantics::{ + merge_maps, ret_kind, ret_op, ret_ref, Nir, NirKind, Ret, TextLit, +}; +use crate::syntax::{ExprKind, Label, NumKind}; + +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( + once((field.clone(), r.clone())).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( + once((field.clone(), r.clone())).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( + once((field.clone(), r.clone())).collect(), + )), + ))), + field.clone(), + )), + None => normalize_field(x, field), + }, + _ => nothing_to_do(), + }, + _ => nothing_to_do(), + } +} + +pub fn normalize_operation(opkind: &OpKind<Nir>) -> Ret { + use self::BinOp::RightBiasedRecordMerge; + 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())) + } + Op(BinOp(RightBiasedRecordMerge, l, r)) => match r.kind() { + RecordLit(kvs) => { + let r_keys = kvs.keys().cloned().collect(); + normalize_operation(&BinOp( + RightBiasedRecordMerge, + Nir::from_partial_expr(ExprKind::Op(Projection( + l.clone(), + ls.difference(&r_keys).cloned().collect(), + ))), + Nir::from_partial_expr(ExprKind::Op(Projection( + r.clone(), + ls.intersection(&r_keys).cloned().collect(), + ))), + )) + } + _ => nothing_to_do(), + }, + _ => 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/operations/typecheck.rs b/dhall/src/operations/typecheck.rs new file mode 100644 index 0000000..91d5059 --- /dev/null +++ b/dhall/src/operations/typecheck.rs @@ -0,0 +1,510 @@ +use std::borrow::Cow; +use std::cmp::max; +use std::collections::HashMap; + +use crate::builtins::Builtin; +use crate::error::{ErrorBuilder, TypeError}; +use crate::operations::{BinOp, OpKind}; +use crate::semantics::{ + merge_maps, mk_span_err, mkerr, Binder, Closure, Hir, HirKind, Nir, + NirKind, Tir, TyEnv, Type, +}; +use crate::syntax::{Const, ExprKind, 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 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) => { + new_kts.insert(l.clone(), 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") + } + }) +} diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs index 468d8b1..a488c31 100644 --- a/dhall/src/semantics/mod.rs +++ b/dhall/src/semantics/mod.rs @@ -1,9 +1,7 @@ -pub mod builtins; pub mod nze; pub mod parse; pub mod resolve; pub mod tck; -pub use self::builtins::*; pub use self::nze::*; pub use self::resolve::*; pub use self::tck::*; diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs index e0d227e..12f1b14 100644 --- a/dhall/src/semantics/nze/nir.rs +++ b/dhall/src/semantics/nze/nir.rs @@ -1,14 +1,15 @@ use std::collections::HashMap; use std::rc::Rc; +use crate::builtins::{Builtin, BuiltinClosure}; +use crate::operations::{BinOp, OpKind}; use crate::semantics::nze::lazy; use crate::semantics::{ - apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder, - BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv, + apply_any, normalize_hir, normalize_one_layer, squash_textlit, Binder, Hir, + HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv, }; use crate::syntax::{ - BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, - NumKind, Span, + Const, Expr, ExprKind, InterpolatedTextContents, Label, NumKind, Span, }; use crate::ToExprOptions; @@ -74,25 +75,27 @@ pub enum NirKind { Var(NzVar), Const(Const), + Num(NumKind), // Must be a number type, Bool or Text BuiltinType(Builtin), - Num(NumKind), - OptionalType(Nir), + TextLit(TextLit), EmptyOptionalLit(Nir), NEOptionalLit(Nir), - ListType(Nir), + OptionalType(Nir), // EmptyListLit(t) means `[] : List t`, not `[] : t` EmptyListLit(Nir), NEListLit(Vec<Nir>), - RecordType(HashMap<Label, Nir>), + ListType(Nir), RecordLit(HashMap<Label, Nir>), - UnionType(HashMap<Label, Option<Nir>>), + RecordType(HashMap<Label, Nir>), UnionConstructor(Label, HashMap<Label, Option<Nir>>), UnionLit(Label, Nir, HashMap<Label, Option<Nir>>), - TextLit(TextLit), + UnionType(HashMap<Label, Option<Nir>>), Equivalence(Nir, Nir), - /// Invariant: evaluation must not be able to progress with `normalize_one_layer`. - PartialExpr(ExprKind<Nir>), + Assert(Nir), + /// Invariant: evaluation must not be able to progress with `normalize_operation`. + /// This is used when an operation couldn't proceed further, for example because of variables. + Op(OpKind<Nir>), } impl Nir { @@ -111,8 +114,7 @@ impl Nir { NirInternal::from_whnf(v).into_nir() } pub fn from_const(c: Const) -> Self { - let v = NirKind::Const(c); - NirInternal::from_whnf(v).into_nir() + Self::from_kind(NirKind::Const(c)) } pub fn from_builtin(b: Builtin) -> Self { Self::from_builtin_env(b, &NzEnv::new()) @@ -148,7 +150,10 @@ impl Nir { } pub fn app(&self, v: Nir) -> Nir { - Nir::from_kind(apply_any(self.clone(), v)) + Nir::from_kind(self.app_to_kind(v)) + } + pub fn app_to_kind(&self, v: Nir) -> NirKind { + apply_any(self, v) } pub fn to_hir(&self, venv: VarEnv) -> Hir { @@ -190,24 +195,24 @@ impl Nir { NirKind::Const(c) => ExprKind::Const(*c), NirKind::BuiltinType(b) => ExprKind::Builtin(*b), NirKind::Num(l) => ExprKind::Num(l.clone()), - NirKind::OptionalType(t) => ExprKind::App( + NirKind::OptionalType(t) => ExprKind::Op(OpKind::App( Nir::from_builtin(Builtin::Optional).to_hir(venv), t.to_hir(venv), - ), - NirKind::EmptyOptionalLit(n) => ExprKind::App( + )), + NirKind::EmptyOptionalLit(n) => ExprKind::Op(OpKind::App( Nir::from_builtin(Builtin::OptionalNone).to_hir(venv), n.to_hir(venv), - ), + )), NirKind::NEOptionalLit(n) => ExprKind::SomeLit(n.to_hir(venv)), - NirKind::ListType(t) => ExprKind::App( + NirKind::ListType(t) => ExprKind::Op(OpKind::App( Nir::from_builtin(Builtin::List).to_hir(venv), t.to_hir(venv), - ), + )), NirKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new( - HirKind::Expr(ExprKind::App( + HirKind::Expr(ExprKind::Op(OpKind::App( Nir::from_builtin(Builtin::List).to_hir(venv), n.to_hir(venv), - )), + ))), Span::Artificial, )), NirKind::NEListLit(elts) => ExprKind::NEListLit( @@ -229,32 +234,35 @@ impl Nir { .collect(), ), NirKind::UnionType(kts) => map_uniontype(kts), - NirKind::UnionConstructor(l, kts) => ExprKind::Field( - Hir::new( - HirKind::Expr(map_uniontype(kts)), - Span::Artificial, - ), - l.clone(), - ), - NirKind::UnionLit(l, v, kts) => ExprKind::App( + NirKind::UnionConstructor(l, kts) => { + ExprKind::Op(OpKind::Field( + Hir::new( + HirKind::Expr(map_uniontype(kts)), + Span::Artificial, + ), + l.clone(), + )) + } + NirKind::UnionLit(l, v, kts) => ExprKind::Op(OpKind::App( Hir::new( - HirKind::Expr(ExprKind::Field( + HirKind::Expr(ExprKind::Op(OpKind::Field( Hir::new( HirKind::Expr(map_uniontype(kts)), Span::Artificial, ), l.clone(), - )), + ))), Span::Artificial, ), v.to_hir(venv), - ), - NirKind::Equivalence(x, y) => ExprKind::BinOp( + )), + NirKind::Equivalence(x, y) => ExprKind::Op(OpKind::BinOp( BinOp::Equivalence, x.to_hir(venv), y.to_hir(venv), - ), - NirKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)), + )), + NirKind::Assert(x) => ExprKind::Assert(x.to_hir(venv)), + NirKind::Op(e) => ExprKind::Op(e.map_ref(|v| v.to_hir(venv))), }), }; @@ -307,7 +315,7 @@ impl Thunk { } fn eval(self) -> NirKind { match self { - Thunk::Thunk { env, body } => normalize_hir_whnf(&env, &body), + Thunk::Thunk { env, body } => normalize_hir(&env, &body), Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env), } } diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 570e106..d042f3f 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -1,18 +1,18 @@ -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, NumKind}; +use crate::syntax::{ExprKind, InterpolatedTextContents}; -pub fn apply_any(f: Nir, a: Nir) -> NirKind { +pub fn apply_any(f: &Nir, a: Nir) -> NirKind { match f.kind() { NirKind::LamClosure { closure, .. } => closure.apply(a).kind().clone(), NirKind::AppliedBuiltin(closure) => closure.apply(a), NirKind::UnionConstructor(l, kts) => { NirKind::UnionLit(l.clone(), a, kts.clone()) } - _ => NirKind::PartialExpr(ExprKind::App(f, a)), + _ => NirKind::Op(OpKind::App(f.clone(), a)), } } @@ -81,393 +81,83 @@ where kvs } -// Small helper enum to avoid repetition -enum Ret<'a> { - NirKind(NirKind), - Nir(Nir), - NirRef(&'a Nir), - Expr(ExprKind<Nir>), -} - -fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option<Ret<'a>> { - use BinOp::{ - BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus, - NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, - RightBiasedRecordMerge, TextAppend, - }; - use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType}; - use NumKind::{Bool, Natural}; - - Some(match (o, x.kind(), y.kind()) { - (BoolAnd, Num(Bool(true)), _) => Ret::NirRef(y), - (BoolAnd, _, Num(Bool(true))) => Ret::NirRef(x), - (BoolAnd, Num(Bool(false)), _) => Ret::NirKind(Num(Bool(false))), - (BoolAnd, _, Num(Bool(false))) => Ret::NirKind(Num(Bool(false))), - (BoolAnd, _, _) if x == y => Ret::NirRef(x), - (BoolOr, Num(Bool(true)), _) => Ret::NirKind(Num(Bool(true))), - (BoolOr, _, Num(Bool(true))) => Ret::NirKind(Num(Bool(true))), - (BoolOr, Num(Bool(false)), _) => Ret::NirRef(y), - (BoolOr, _, Num(Bool(false))) => Ret::NirRef(x), - (BoolOr, _, _) if x == y => Ret::NirRef(x), - (BoolEQ, Num(Bool(true)), _) => Ret::NirRef(y), - (BoolEQ, _, Num(Bool(true))) => Ret::NirRef(x), - (BoolEQ, Num(Bool(x)), Num(Bool(y))) => Ret::NirKind(Num(Bool(x == y))), - (BoolEQ, _, _) if x == y => Ret::NirKind(Num(Bool(true))), - (BoolNE, Num(Bool(false)), _) => Ret::NirRef(y), - (BoolNE, _, Num(Bool(false))) => Ret::NirRef(x), - (BoolNE, Num(Bool(x)), Num(Bool(y))) => Ret::NirKind(Num(Bool(x != y))), - (BoolNE, _, _) if x == y => Ret::NirKind(Num(Bool(false))), - - (NaturalPlus, Num(Natural(0)), _) => Ret::NirRef(y), - (NaturalPlus, _, Num(Natural(0))) => Ret::NirRef(x), - (NaturalPlus, Num(Natural(x)), Num(Natural(y))) => { - Ret::NirKind(Num(Natural(x + y))) - } - (NaturalTimes, Num(Natural(0)), _) => Ret::NirKind(Num(Natural(0))), - (NaturalTimes, _, Num(Natural(0))) => Ret::NirKind(Num(Natural(0))), - (NaturalTimes, Num(Natural(1)), _) => Ret::NirRef(y), - (NaturalTimes, _, Num(Natural(1))) => Ret::NirRef(x), - (NaturalTimes, Num(Natural(x)), Num(Natural(y))) => { - Ret::NirKind(Num(Natural(x * y))) - } - - (ListAppend, EmptyListLit(_), _) => Ret::NirRef(y), - (ListAppend, _, EmptyListLit(_)) => Ret::NirRef(x), - (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::NirKind(NEListLit( - xs.iter().chain(ys.iter()).cloned().collect(), - )), - - (TextAppend, NirKind::TextLit(x), _) if x.is_empty() => Ret::NirRef(y), - (TextAppend, _, NirKind::TextLit(y)) if y.is_empty() => Ret::NirRef(x), - (TextAppend, NirKind::TextLit(x), NirKind::TextLit(y)) => { - Ret::NirKind(NirKind::TextLit(x.concat(y))) - } - (TextAppend, NirKind::TextLit(x), _) => Ret::NirKind(NirKind::TextLit( - x.concat(&TextLit::interpolate(y.clone())), - )), - (TextAppend, _, NirKind::TextLit(y)) => Ret::NirKind(NirKind::TextLit( - TextLit::interpolate(x.clone()).concat(y), - )), +pub type Ret = NirKind; - (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::NirRef(x) - } - (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::NirRef(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::NirKind(RecordLit(kvs)) - } - (RightBiasedRecordMerge, _, _) if x == y => Ret::NirRef(y), - - (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::NirRef(x) - } - (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::NirRef(y) - } - (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let kvs = merge_maps(kvs1, kvs2, |_, v1, v2| { - Nir::from_partial_expr(ExprKind::BinOp( - RecursiveRecordMerge, - v1.clone(), - v2.clone(), - )) - }); - Ret::NirKind(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::BinOp( - RecursiveRecordTypeMerge, - l.clone(), - r.clone(), - )) - }, - ); - Ret::NirKind(RecordType(kts)) - } - - (Equivalence, _, _) => { - Ret::NirKind(NirKind::Equivalence(x.clone(), y.clone())) - } - - _ => return None, - }) +pub fn ret_nir(x: Nir) -> Ret { + ret_ref(&x) +} +pub fn ret_kind(x: NirKind) -> Ret { + x +} +pub fn ret_ref(x: &Nir) -> Ret { + x.kind().clone() +} +pub fn ret_op(x: OpKind<Nir>) -> Ret { + NirKind::Op(x) } -#[allow(clippy::cognitive_complexity)] pub fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind { use NirKind::{ - EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, - PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit, + Assert, Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType, UnionType, }; - use NumKind::Bool; - let ret = match expr { - ExprKind::Import(..) | ExprKind::Completion(..) => { - unreachable!("This case should have been handled in resolution") - } + match expr { ExprKind::Var(..) | ExprKind::Lam(..) | ExprKind::Pi(..) - | ExprKind::Let(..) => unreachable!( - "This case should have been handled in normalize_hir_whnf" - ), + | ExprKind::Let(..) => { + unreachable!("This case should have been handled in normalize_hir") + } - ExprKind::Annot(x, _) => Ret::Nir(x), - ExprKind::Const(c) => Ret::Nir(Nir::from_const(c)), - ExprKind::Builtin(b) => Ret::Nir(Nir::from_builtin_env(b, env)), - ExprKind::Assert(_) => Ret::Expr(expr), - ExprKind::App(v, a) => Ret::Nir(v.app(a)), - ExprKind::Num(l) => Ret::NirKind(Num(l)), - ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)), + ExprKind::Const(c) => ret_kind(Const(c)), + ExprKind::Num(l) => ret_kind(Num(l)), + ExprKind::Builtin(b) => { + ret_kind(NirKind::from_builtin_env(b, env.clone())) + } + ExprKind::TextLit(elts) => { + let tlit = TextLit::new(elts.into_iter()); + // Simplify bare interpolation + if let Some(v) = tlit.as_single_expr() { + ret_ref(v) + } else { + ret_kind(NirKind::TextLit(tlit)) + } + } + ExprKind::SomeLit(e) => ret_kind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { let arg = match t.kind() { NirKind::ListType(t) => t.clone(), _ => panic!("internal type error"), }; - Ret::NirKind(NirKind::EmptyListLit(arg)) + ret_kind(NirKind::EmptyListLit(arg)) } ExprKind::NEListLit(elts) => { - Ret::NirKind(NEListLit(elts.into_iter().collect())) + ret_kind(NEListLit(elts.into_iter().collect())) } ExprKind::RecordLit(kvs) => { - Ret::NirKind(RecordLit(kvs.into_iter().collect())) + ret_kind(RecordLit(kvs.into_iter().collect())) } ExprKind::RecordType(kvs) => { - Ret::NirKind(RecordType(kvs.into_iter().collect())) + ret_kind(RecordType(kvs.into_iter().collect())) } ExprKind::UnionType(kvs) => { - Ret::NirKind(UnionType(kvs.into_iter().collect())) - } - ExprKind::TextLit(elts) => { - let tlit = TextLit::new(elts.into_iter()); - // Simplify bare interpolation - if let Some(v) = tlit.as_single_expr() { - Ret::Nir(v.clone()) - } else { - Ret::NirKind(NirKind::TextLit(tlit)) - } - } - ExprKind::BoolIf(ref b, ref e1, ref e2) => { - match b.kind() { - Num(Bool(true)) => Ret::NirRef(e1), - Num(Bool(false)) => Ret::NirRef(e2), - _ => { - match (e1.kind(), e2.kind()) { - // Simplify `if b then True else False` - (Num(Bool(true)), Num(Bool(false))) => Ret::NirRef(b), - _ if e1 == e2 => Ret::NirRef(e1), - _ => Ret::Expr(expr), - } - } - } - } - ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) { - Some(ret) => ret, - None => Ret::Expr(expr), - }, - - ExprKind::Field(ref v, ref field) => match v.kind() { - RecordLit(kvs) => match kvs.get(field) { - Some(r) => Ret::Nir(r.clone()), - None => Ret::Expr(expr), - }, - UnionType(kts) => { - Ret::NirKind(UnionConstructor(field.clone(), kts.clone())) - } - PartialExpr(ExprKind::Projection(x, _)) => { - return normalize_one_layer( - ExprKind::Field(x.clone(), field.clone()), - env, - ) - } - PartialExpr(ExprKind::BinOp( - BinOp::RightBiasedRecordMerge, - x, - y, - )) => match (x.kind(), y.kind()) { - (_, RecordLit(kvs)) => match kvs.get(field) { - Some(r) => Ret::Nir(r.clone()), - None => { - return normalize_one_layer( - ExprKind::Field(x.clone(), field.clone()), - env, - ) - } - }, - (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => Ret::Expr(ExprKind::Field( - Nir::from_kind(PartialExpr(ExprKind::BinOp( - BinOp::RightBiasedRecordMerge, - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - y.clone(), - ))), - field.clone(), - )), - None => { - return normalize_one_layer( - ExprKind::Field(y.clone(), field.clone()), - env, - ) - } - }, - _ => Ret::Expr(expr), - }, - PartialExpr(ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y)) => { - match (x.kind(), y.kind()) { - (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => Ret::Expr(ExprKind::Field( - Nir::from_kind(PartialExpr(ExprKind::BinOp( - BinOp::RecursiveRecordMerge, - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - y.clone(), - ))), - field.clone(), - )), - None => { - return normalize_one_layer( - ExprKind::Field(y.clone(), field.clone()), - env, - ) - } - }, - (_, RecordLit(kvs)) => match kvs.get(field) { - Some(r) => Ret::Expr(ExprKind::Field( - Nir::from_kind(PartialExpr(ExprKind::BinOp( - BinOp::RecursiveRecordMerge, - x.clone(), - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - ))), - field.clone(), - )), - None => { - return normalize_one_layer( - ExprKind::Field(x.clone(), field.clone()), - env, - ) - } - }, - _ => Ret::Expr(expr), - } - } - _ => Ret::Expr(expr), - }, - ExprKind::Projection(_, ref ls) if ls.is_empty() => { - Ret::NirKind(RecordLit(HashMap::new())) + ret_kind(UnionType(kvs.into_iter().collect())) } - ExprKind::Projection(ref v, ref ls) => match v.kind() { - RecordLit(kvs) => Ret::NirKind(RecordLit( - ls.iter() - .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone()))) - .collect(), - )), - PartialExpr(ExprKind::Projection(v2, _)) => { - return normalize_one_layer( - ExprKind::Projection(v2.clone(), ls.clone()), - env, - ) - } - _ => Ret::Expr(expr), - }, - ExprKind::ProjectionByExpr(ref v, ref t) => match t.kind() { - RecordType(kts) => { - return normalize_one_layer( - ExprKind::Projection( - v.clone(), - kts.keys().cloned().collect(), - ), - env, - ) - } - _ => Ret::Expr(expr), - }, - - ExprKind::Merge(ref handlers, ref variant, _) => { - match handlers.kind() { - RecordLit(kvs) => match variant.kind() { - UnionConstructor(l, _) => match kvs.get(l) { - Some(h) => Ret::Nir(h.clone()), - None => Ret::Expr(expr), - }, - UnionLit(l, v, _) => match kvs.get(l) { - Some(h) => Ret::Nir(h.app(v.clone())), - None => Ret::Expr(expr), - }, - EmptyOptionalLit(_) => match kvs.get(&"None".into()) { - Some(h) => Ret::Nir(h.clone()), - None => Ret::Expr(expr), - }, - NEOptionalLit(v) => match kvs.get(&"Some".into()) { - Some(h) => Ret::Nir(h.app(v.clone())), - None => Ret::Expr(expr), - }, - _ => Ret::Expr(expr), - }, - _ => Ret::Expr(expr), - } + ExprKind::Op(ref op) => normalize_operation(op), + ExprKind::Annot(x, _) => ret_nir(x), + ExprKind::Assert(x) => ret_kind(Assert(x)), + ExprKind::Import(..) => { + unreachable!("This case should have been handled in resolution") } - ExprKind::ToMap(ref v, ref annot) => match v.kind() { - RecordLit(kvs) if kvs.is_empty() => { - match annot.as_ref().map(|v| v.kind()) { - Some(NirKind::ListType(t)) => { - Ret::NirKind(EmptyListLit(t.clone())) - } - _ => Ret::Expr(expr), - } - } - RecordLit(kvs) => Ret::NirKind(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(), - )), - _ => Ret::Expr(expr), - }, - }; - - match ret { - Ret::NirKind(v) => v, - Ret::Nir(v) => v.kind().clone(), - Ret::NirRef(v) => v.kind().clone(), - Ret::Expr(expr) => NirKind::PartialExpr(expr), } } /// Normalize Hir into WHNF -pub fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind { +pub fn normalize_hir(env: &NzEnv, hir: &Hir) -> NirKind { match hir.kind() { HirKind::Var(var) => env.lookup_val(*var), - HirKind::Import(hir, _) => normalize_hir_whnf(env, hir), + HirKind::Import(hir, _) => normalize_hir(env, hir), HirKind::Expr(ExprKind::Lam(binder, annot, body)) => { let annot = annot.eval(env); NirKind::LamClosure { diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs index 6e50fa6..e96f16b 100644 --- a/dhall/src/semantics/resolve/resolve.rs +++ b/dhall/src/semantics/resolve/resolve.rs @@ -1,17 +1,19 @@ use itertools::Itertools; use std::borrow::Cow; +use std::collections::BTreeMap; use std::env; use std::path::PathBuf; use url::Url; +use crate::builtins::Builtin; use crate::error::ErrorBuilder; use crate::error::{Error, ImportError}; +use crate::operations::{BinOp, 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, Span, UnspannedExpr, URL, + Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, ImportTarget, Span, + UnspannedExpr, URL, }; use crate::{Parsed, Resolved}; @@ -179,12 +181,13 @@ impl ImportLocation { }; let asloc_ty = make_aslocation_uniontype(); - let expr = mkexpr(ExprKind::Field(asloc_ty, field_name.into())); + let expr = + mkexpr(ExprKind::Op(OpKind::Field(asloc_ty, field_name.into()))); match arg { - Some(arg) => mkexpr(ExprKind::App( + Some(arg) => mkexpr(ExprKind::Op(OpKind::App( expr, mkexpr(ExprKind::TextLit(arg.into())), - )), + ))), None => expr, } } @@ -196,7 +199,7 @@ fn mkexpr(kind: UnspannedExpr) -> Expr { fn make_aslocation_uniontype() -> Expr { let text_type = mkexpr(ExprKind::Builtin(Builtin::Text)); - let mut union = DupTreeMap::default(); + let mut union = BTreeMap::default(); union.insert("Local".into(), Some(text_type.clone())); union.insert("Remote".into(), Some(text_type.clone())); union.insert("Environment".into(), Some(text_type)); @@ -261,21 +264,21 @@ fn resolve_one_import( /// Desugar the first level of the expression. fn desugar(expr: &Expr) -> Cow<'_, Expr> { match expr.kind() { - ExprKind::Completion(ty, compl) => { + ExprKind::Op(OpKind::Completion(ty, compl)) => { let ty_field_default = Expr::new( - ExprKind::Field(ty.clone(), "default".into()), + ExprKind::Op(OpKind::Field(ty.clone(), "default".into())), expr.span(), ); let merged = Expr::new( - ExprKind::BinOp( + ExprKind::Op(OpKind::BinOp( BinOp::RightBiasedRecordMerge, ty_field_default, compl.clone(), - ), + )), expr.span(), ); let ty_field_type = Expr::new( - ExprKind::Field(ty.clone(), "Type".into()), + ExprKind::Op(OpKind::Field(ty.clone(), "Type".into())), expr.span(), ); Cow::Owned(Expr::new( @@ -304,7 +307,7 @@ fn traverse_resolve_expr( .format(), )?, }, - ExprKind::BinOp(BinOp::ImportAlt, l, r) => { + ExprKind::Op(OpKind::BinOp(BinOp::ImportAlt, l, r)) => { match traverse_resolve_expr(name_env, l, f) { Ok(l) => l, Err(_) => { diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs index 89a8027..ec15a1f 100644 --- a/dhall/src/semantics/tck/tir.rs +++ b/dhall/src/semantics/tck/tir.rs @@ -1,6 +1,7 @@ +use crate::builtins::Builtin; use crate::error::{ErrorBuilder, TypeError}; use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv}; -use crate::syntax::{Builtin, Const, Expr, Span}; +use crate::syntax::{Const, Expr, Span}; /// The type of a type. 0 is `Type`, 1 is `Kind`, etc... #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)] diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index c3334b5..361e1b4 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -1,49 +1,10 @@ -use std::borrow::Cow; use std::cmp::max; -use std::collections::HashMap; +use crate::builtins::{type_of_builtin, Builtin}; use crate::error::{ErrorBuilder, TypeError, TypeMessage}; -use crate::semantics::merge_maps; -use crate::semantics::{ - type_of_builtin, Binder, Closure, Hir, HirKind, Nir, NirKind, Tir, TyEnv, - Type, -}; -use crate::syntax::{ - BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, Span, -}; - -fn check_rectymerge( - span: &Span, - env: &TyEnv, - x: Nir, - y: Nir, -) -> Result<(), TypeError> { - let kts_x = match x.kind() { - NirKind::RecordType(kts) => kts, - _ => { - return mk_span_err( - span.clone(), - "RecordTypeMergeRequiresRecordType", - ) - } - }; - let kts_y = match y.kind() { - NirKind::RecordType(kts) => kts, - _ => { - return mk_span_err( - span.clone(), - "RecordTypeMergeRequiresRecordType", - ) - } - }; - for (k, tx) in kts_x { - if let Some(ty) = kts_y.get(k) { - // TODO: store Type in RecordType ? - check_rectymerge(span, env, tx.clone(), ty.clone())?; - } - } - Ok(()) -} +use crate::operations::typecheck_operation; +use crate::semantics::{Hir, HirKind, Nir, NirKind, Tir, TyEnv, Type}; +use crate::syntax::{Const, ExprKind, InterpolatedTextContents, NumKind, Span}; fn function_check(a: Const, b: Const) -> Const { if b == Const::Type { @@ -74,8 +35,8 @@ fn type_one_layer( ) -> Result<Type, TypeError> { let span_err = |msg: &str| mk_span_err(span.clone(), msg); - let ty = match &ekind { - ExprKind::Import(..) | ExprKind::Completion(..) => { + Ok(match &ekind { + ExprKind::Import(..) => { unreachable!("This case should have been handled in resolution") } ExprKind::Var(..) @@ -89,20 +50,16 @@ fn type_one_layer( ExprKind::Const(Const::Type) => Type::from_const(Const::Kind), ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort), + ExprKind::Num(num) => Type::from_builtin(match num { + NumKind::Bool(_) => Builtin::Bool, + NumKind::Natural(_) => Builtin::Natural, + NumKind::Integer(_) => Builtin::Integer, + NumKind::Double(_) => Builtin::Double, + }), ExprKind::Builtin(b) => { let t_hir = type_of_builtin(*b); typecheck(&t_hir)?.eval_to_type(env)? } - ExprKind::Num(NumKind::Bool(_)) => Type::from_builtin(Builtin::Bool), - ExprKind::Num(NumKind::Natural(_)) => { - Type::from_builtin(Builtin::Natural) - } - ExprKind::Num(NumKind::Integer(_)) => { - Type::from_builtin(Builtin::Integer) - } - ExprKind::Num(NumKind::Double(_)) => { - Type::from_builtin(Builtin::Double) - } ExprKind::TextLit(interpolated) => { let text_type = Type::from_builtin(Builtin::Text); for contents in interpolated.iter() { @@ -115,6 +72,16 @@ fn type_one_layer( } text_type } + ExprKind::SomeLit(x) => { + if x.ty().ty().as_const() != Some(Const::Type) { + return span_err("InvalidOptionalType"); + } + + let t = x.ty().to_nir(); + Nir::from_builtin(Builtin::Optional) + .app(t) + .to_type(Const::Type) + } ExprKind::EmptyListLit(t) => { let t = t.eval_to_type(env)?; match t.kind() { @@ -138,82 +105,56 @@ fn type_one_layer( let t = x.ty().to_nir(); Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type) } - ExprKind::SomeLit(x) => { - if x.ty().ty().as_const() != Some(Const::Type) { - return span_err("InvalidOptionalType"); - } - - let t = x.ty().to_nir(); - Nir::from_builtin(Builtin::Optional) - .app(t) - .to_type(Const::Type) - } ExprKind::RecordLit(kvs) => { - use std::collections::hash_map::Entry; - let mut kts = HashMap::new(); // An empty record type has type Type let mut k = Const::Type; - for (x, v) in kvs { - // Check for duplicated entries - match kts.entry(x.clone()) { - Entry::Occupied(_) => { - return span_err("RecordTypeDuplicateField") - } - Entry::Vacant(e) => e.insert(v.ty().to_nir()), - }; - + for v in kvs.values() { // Check that the fields have a valid kind match v.ty().ty().as_const() { Some(c) => k = max(k, c), - None => return span_err("InvalidFieldType"), + None => return mk_span_err(v.span(), "InvalidFieldType"), } } + let kts = kvs + .iter() + .map(|(x, v)| (x.clone(), v.ty().to_nir())) + .collect(); + Nir::from_kind(NirKind::RecordType(kts)).to_type(k) } ExprKind::RecordType(kts) => { - use std::collections::hash_map::Entry; - let mut seen_fields = HashMap::new(); // An empty record type has type Type let mut k = Const::Type; - - for (x, t) in kts { - // Check for duplicated entries - match seen_fields.entry(x.clone()) { - Entry::Occupied(_) => { - return span_err("RecordTypeDuplicateField") - } - Entry::Vacant(e) => e.insert(()), - }; - + for t in kts.values() { // Check the type is a Const and compute final type match t.ty().as_const() { Some(c) => k = max(k, c), - None => return span_err("InvalidFieldType"), + None => return mk_span_err(t.span(), "InvalidFieldType"), } } Type::from_const(k) } ExprKind::UnionType(kts) => { - use std::collections::hash_map::Entry; - let mut seen_fields = HashMap::new(); // Check that all types are the same const let mut k = None; - for (x, t) in kts { + for t in kts.values() { if let Some(t) = t { - match (k, t.ty().as_const()) { - (None, Some(k2)) => k = Some(k2), - (Some(k1), Some(k2)) if k1 == k2 => {} - _ => return span_err("InvalidFieldType"), + let c = match t.ty().as_const() { + Some(c) => c, + None => { + return mk_span_err(t.span(), "InvalidVariantType") + } + }; + match k { + None => k = Some(c), + Some(k) if k == c => {} + _ => { + return mk_span_err(t.span(), "InvalidVariantType") + } } } - match seen_fields.entry(x) { - Entry::Occupied(_) => { - return span_err("UnionTypeDuplicateField") - } - Entry::Vacant(e) => e.insert(()), - }; } // An empty union type has type Type; @@ -222,36 +163,7 @@ fn type_one_layer( Type::from_const(k) } - ExprKind::Field(scrut, x) => { - match scrut.ty().kind() { - NirKind::RecordType(kts) => match kts.get(&x) { - Some(val) => Type::new_infer_universe(env, val.clone())?, - None => return span_err("MissingRecordField"), - }, - NirKind::Const(_) => { - let scrut = scrut.eval_to_type(env)?; - match scrut.kind() { - NirKind::UnionType(kts) => match kts.get(x) { - // Constructor has type T -> < x: T, ... > - Some(Some(ty)) => { - Nir::from_kind(NirKind::PiClosure { - binder: Binder::new(x.clone()), - annot: ty.clone(), - closure: Closure::new_constant( - scrut.to_nir(), - ), - }) - .to_type(scrut.ty()) - } - Some(None) => scrut, - None => return span_err("MissingUnionField"), - }, - _ => return span_err("NotARecord"), - } - } - _ => return span_err("NotARecord"), - } - } + ExprKind::Op(op) => typecheck_operation(env, span, op)?, ExprKind::Assert(t) => { let t = t.eval_to_type(env)?; match t.kind() { @@ -261,430 +173,13 @@ fn type_one_layer( } t } - ExprKind::App(f, arg) => { - match f.ty().kind() { - // TODO: store Type in closure - NirKind::PiClosure { annot, closure, .. } => { - if arg.ty().as_nir() != annot { - return mkerr( - ErrorBuilder::new(format!( - "wrong type of function argument" - )) - .span_err( - f.span(), - format!( - "this expects an argument of type: {}", - annot.to_expr_tyenv(env), - ), - ) - .span_err( - arg.span(), - format!( - "but this has type: {}", - arg.ty().to_expr_tyenv(env), - ), - ) - .note(format!( - "expected type `{}`\n found type `{}`", - annot.to_expr_tyenv(env), - arg.ty().to_expr_tyenv(env), - )) - .format(), - ); - } - - let arg_nf = arg.eval(env); - Type::new_infer_universe(env, closure.apply(arg_nf))? - } - _ => return mkerr( - ErrorBuilder::new(format!( - "expected function, found `{}`", - f.ty().to_expr_tyenv(env) - )) - .span_err( - f.span(), - format!("function application requires a function",), - ) - .format(), - ), - } - } - ExprKind::BoolIf(x, y, z) => { - if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) { - return span_err("InvalidPredicate"); - } - if y.ty().ty().as_const() != Some(Const::Type) { - return span_err("IfBranchMustBeTerm"); - } - if y.ty() != z.ty() { - return span_err("IfBranchMismatch"); - } - - y.ty().clone() - } - ExprKind::BinOp(BinOp::RightBiasedRecordMerge, x, y) => { - let x_type = x.ty(); - let y_type = y.ty(); - - // Extract the LHS record type - let kts_x = match x_type.kind() { - NirKind::RecordType(kts) => kts, - _ => return span_err("MustCombineRecord"), - }; - // Extract the RHS record type - let kts_y = match y_type.kind() { - NirKind::RecordType(kts) => kts, - _ => return span_err("MustCombineRecord"), - }; - - // Union the two records, prefering - // the values found in the RHS. - let kts = merge_maps(kts_x, kts_y, |_, _, r_t| r_t.clone()); - - let u = max(x.ty().ty(), y.ty().ty()); - Nir::from_kind(NirKind::RecordType(kts)).to_type(u) - } - ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { - check_rectymerge(&span, env, x.ty().to_nir(), y.ty().to_nir())?; - - let hir = Hir::new( - HirKind::Expr(ExprKind::BinOp( - BinOp::RecursiveRecordTypeMerge, - x.ty().to_hir(env.as_varenv()), - y.ty().to_hir(env.as_varenv()), - )), - span.clone(), - ); - let x_u = x.ty().ty(); - let y_u = y.ty().ty(); - Type::new(hir.eval(env), max(x_u, y_u)) - } - ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { - check_rectymerge(&span, env, x.eval(env), y.eval(env))?; - - // A RecordType's type is always a const - let xk = x.ty().as_const().unwrap(); - let yk = y.ty().as_const().unwrap(); - Type::from_const(max(xk, yk)) - } - ExprKind::BinOp(BinOp::ListAppend, l, r) => { - match l.ty().kind() { - NirKind::ListType(..) => {} - _ => return span_err("BinOpTypeMismatch"), - } - - if l.ty() != r.ty() { - return span_err("BinOpTypeMismatch"); - } - - l.ty().clone() - } - ExprKind::BinOp(BinOp::Equivalence, l, r) => { - if l.ty() != r.ty() { - return span_err("EquivalenceTypeMismatch"); - } - if l.ty().ty().as_const() != Some(Const::Type) { - return span_err("EquivalenceArgumentsMustBeTerms"); - } - - Type::from_const(Const::Type) - } - ExprKind::BinOp(o, l, r) => { - let t = Type::from_builtin(match o { - BinOp::BoolAnd - | BinOp::BoolOr - | BinOp::BoolEQ - | BinOp::BoolNE => Builtin::Bool, - BinOp::NaturalPlus | BinOp::NaturalTimes => Builtin::Natural, - BinOp::TextAppend => Builtin::Text, - BinOp::ListAppend - | BinOp::RightBiasedRecordMerge - | BinOp::RecursiveRecordMerge - | BinOp::RecursiveRecordTypeMerge - | BinOp::Equivalence => unreachable!(), - BinOp::ImportAlt => unreachable!("ImportAlt leftover in tck"), - }); - - if *l.ty() != t { - return span_err("BinOpTypeMismatch"); - } - - if *r.ty() != t { - return span_err("BinOpTypeMismatch"); - } - - t - } - ExprKind::Merge(record, union, type_annot) => { - let record_type = record.ty(); - let handlers = match record_type.kind() { - NirKind::RecordType(kts) => kts, - _ => return span_err("Merge1ArgMustBeRecord"), - }; - - let union_type = union.ty(); - let variants = match union_type.kind() { - NirKind::UnionType(kts) => Cow::Borrowed(kts), - NirKind::OptionalType(ty) => { - let mut kts = HashMap::new(); - kts.insert("None".into(), None); - kts.insert("Some".into(), Some(ty.clone())); - Cow::Owned(kts) - } - _ => return span_err("Merge2ArgMustBeUnionOrOptional"), - }; - - let mut inferred_type = None; - for (x, handler_type) in handlers { - let handler_return_type: Type = match variants.get(x) { - // Union alternative with type - Some(Some(variant_type)) => match handler_type.kind() { - NirKind::PiClosure { closure, annot, .. } => { - if variant_type != annot { - return mkerr( - ErrorBuilder::new(format!( - "Wrong handler input type" - )) - .span_err( - span, - format!("in this merge expression",), - ) - .span_err( - record.span(), - format!( - "the handler for `{}` expects a \ - value of type: `{}`", - x, - annot.to_expr_tyenv(env) - ), - ) - .span_err( - union.span(), - format!( - "but the corresponding variant \ - has type: `{}`", - variant_type.to_expr_tyenv(env) - ), - ) - .format(), - ); - } - - // TODO: this actually doesn't check anything yet - match closure.remove_binder() { - Ok(v) => { - Type::new_infer_universe(env, v.clone())? - } - Err(()) => { - return span_err( - "MergeReturnTypeIsDependent", - ) - } - } - } - _ => { - return mkerr( - ErrorBuilder::new(format!( - "merge handler is not a function" - )) - .span_err( - span, - format!("in this merge expression"), - ) - .span_err( - record.span(), - format!( - "the handler for `{}` has type: `{}`", - x, - handler_type.to_expr_tyenv(env) - ), - ) - .span_help( - union.span(), - format!( - "the corresponding variant has type: \ - `{}`", - variant_type.to_expr_tyenv(env) - ), - ) - .help(format!( - "a handler for this variant must be a \ - function that takes an input of type: \ - `{}`", - variant_type.to_expr_tyenv(env) - )) - .format(), - ) - } - }, - // Union alternative without type - Some(None) => { - Type::new_infer_universe(env, handler_type.clone())? - } - None => return span_err("MergeHandlerMissingVariant"), - }; - match &inferred_type { - None => inferred_type = Some(handler_return_type), - Some(t) => { - if t != &handler_return_type { - return span_err("MergeHandlerTypeMismatch"); - } - } - } - } - for x in variants.keys() { - if !handlers.contains_key(x) { - return span_err("MergeVariantMissingHandler"); - } - } - - let type_annot = type_annot - .as_ref() - .map(|t| t.eval_to_type(env)) - .transpose()?; - match (inferred_type, type_annot) { - (Some(t1), Some(t2)) => { - if t1 != t2 { - return span_err("MergeAnnotMismatch"); - } - t1 - } - (Some(t), None) => t, - (None, Some(t)) => t, - (None, None) => return span_err("MergeEmptyNeedsAnnotation"), - } - } - ExprKind::ToMap(record, annot) => { - if record.ty().ty().as_const() != Some(Const::Type) { - return span_err("`toMap` only accepts records of type `Type`"); - } - let record_t = record.ty(); - let kts = match record_t.kind() { - NirKind::RecordType(kts) => kts, - _ => { - return span_err("The argument to `toMap` must be a record") - } - }; - - if kts.is_empty() { - let annot = if let Some(annot) = annot { - annot - } else { - return span_err( - "`toMap` applied to an empty record requires a type \ - annotation", - ); - }; - let annot_val = annot.eval_to_type(env)?; - - let err_msg = "The type of `toMap x` must be of the form \ - `List { mapKey : Text, mapValue : T }`"; - let arg = match annot_val.kind() { - NirKind::ListType(t) => t, - _ => return span_err(err_msg), - }; - let kts = match arg.kind() { - NirKind::RecordType(kts) => kts, - _ => return span_err(err_msg), - }; - if kts.len() != 2 { - return span_err(err_msg); - } - match kts.get(&"mapKey".into()) { - Some(t) if *t == Nir::from_builtin(Builtin::Text) => {} - _ => return span_err(err_msg), - } - match kts.get(&"mapValue".into()) { - Some(_) => {} - None => return span_err(err_msg), - } - annot_val - } else { - let entry_type = kts.iter().next().unwrap().1.clone(); - for (_, t) in kts.iter() { - if *t != entry_type { - return span_err( - "Every field of the record must have the same type", - ); - } - } - - let mut kts = HashMap::new(); - kts.insert("mapKey".into(), Nir::from_builtin(Builtin::Text)); - kts.insert("mapValue".into(), entry_type); - let output_type: Type = Nir::from_builtin(Builtin::List) - .app(Nir::from_kind(NirKind::RecordType(kts))) - .to_type(Const::Type); - if let Some(annot) = annot { - let annot_val = annot.eval_to_type(env)?; - if output_type != annot_val { - return span_err("Annotation mismatch"); - } - } - output_type - } - } - ExprKind::Projection(record, labels) => { - let record_type = record.ty(); - let kts = match record_type.kind() { - NirKind::RecordType(kts) => kts, - _ => return span_err("ProjectionMustBeRecord"), - }; - - let mut new_kts = HashMap::new(); - for l in labels { - match kts.get(l) { - None => return span_err("ProjectionMissingEntry"), - Some(t) => { - use std::collections::hash_map::Entry; - match new_kts.entry(l.clone()) { - Entry::Occupied(_) => { - return span_err("ProjectionDuplicateField") - } - Entry::Vacant(e) => e.insert(t.clone()), - } - } - }; - } - - Type::new_infer_universe( - env, - Nir::from_kind(NirKind::RecordType(new_kts)), - )? - } - ExprKind::ProjectionByExpr(record, selection) => { - let record_type = record.ty(); - let rec_kts = match record_type.kind() { - NirKind::RecordType(kts) => kts, - _ => return span_err("ProjectionMustBeRecord"), - }; - - let selection_val = selection.eval_to_type(env)?; - let sel_kts = match selection_val.kind() { - NirKind::RecordType(kts) => kts, - _ => return span_err("ProjectionByExprTakesRecordType"), - }; - - for (l, sel_ty) in sel_kts { - match rec_kts.get(l) { - Some(rec_ty) => { - if rec_ty != sel_ty { - return span_err("ProjectionWrongType"); - } - } - None => return span_err("ProjectionMissingEntry"), - } - } - - selection_val - } - }; - - Ok(ty) + }) } /// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation /// to compare with. +// We pass the annotation to avoid duplicating the annot checking logic. I hope one day we can use +// it to handle the annotations in merge/toMap/etc. uniformly. pub fn type_with<'hir>( env: &TyEnv, hir: &'hir Hir, @@ -780,7 +275,7 @@ pub fn type_with<'hir>( Ok(tir) } -/// Typecheck an expression and return the expression annotated with types if type-checking +/// Typecheck an expression and return the expression annotated with its type if type-checking /// succeeded, or an error if type-checking failed. pub fn typecheck<'hir>(hir: &'hir Hir) -> Result<Tir<'hir>, TypeError> { type_with(&TyEnv::new(), hir, None) diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs index 9e935dc..9d216a7 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::builtins::Builtin; use crate::error::Error; +use crate::operations::OpKind; use crate::semantics::Universe; -use crate::syntax::map::{DupTreeMap, DupTreeSet}; use crate::syntax::visitor; use crate::syntax::*; @@ -36,74 +37,6 @@ impl Const { #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct V(pub Label, pub usize); -// Definition order must match precedence order for -// pretty-printing to work correctly -#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] -pub enum BinOp { - /// `x ? y` - ImportAlt, - /// `x || y` - BoolOr, - /// `x + y` - NaturalPlus, - /// `x ++ y` - TextAppend, - /// `x # y` - ListAppend, - /// `x && y` - BoolAnd, - /// `x ∧ y` - RecursiveRecordMerge, - /// `x ⫽ y` - RightBiasedRecordMerge, - /// `x ⩓ y` - RecursiveRecordTypeMerge, - /// `x * y` - NaturalTimes, - /// `x == y` - BoolEQ, - /// `x != y` - BoolNE, - /// x === y - Equivalence, -} - -/// Built-ins -#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] -pub enum Builtin { - Bool, - Natural, - Integer, - Double, - Text, - List, - Optional, - OptionalNone, - NaturalBuild, - NaturalFold, - NaturalIsZero, - NaturalEven, - NaturalOdd, - NaturalToInteger, - NaturalShow, - NaturalSubtract, - IntegerToDouble, - IntegerShow, - IntegerNegate, - IntegerClamp, - DoubleShow, - ListBuild, - ListFold, - ListLength, - ListHead, - ListLast, - ListIndexed, - ListReverse, - OptionalFold, - OptionalBuild, - TextShow, -} - // Each node carries an annotation. #[derive(Debug, Clone)] pub struct Expr { @@ -132,57 +65,44 @@ pub enum NumKind { // smart pointers. #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum ExprKind<SubExpr> { + /// `Type`, `Kind` and `Sort` Const(Const), + /// Numbers and booleans Num(NumKind), - /// `x` - /// `x@n` - Var(V), - /// `λ(x : A) -> b` - Lam(Label, SubExpr, SubExpr), - /// `A -> B` - /// `∀(x : A) -> B` - Pi(Label, SubExpr, SubExpr), - /// `f a` - App(SubExpr, SubExpr), - /// `let x = r in e` - /// `let x : t = r in e` - Let(Label, Option<SubExpr>, SubExpr, SubExpr), - /// `x : t` - Annot(SubExpr, SubExpr), - /// `assert : t` - Assert(SubExpr), - /// Built-in values + /// Built-in functions and types Builtin(Builtin), - // Binary operations - BinOp(BinOp, SubExpr, SubExpr), - /// `if x then y else z` - BoolIf(SubExpr, SubExpr, SubExpr), /// `"Some ${interpolated} text"` TextLit(InterpolatedText<SubExpr>), + /// `Some e` + SomeLit(SubExpr), /// `[] : t` EmptyListLit(SubExpr), /// `[x, y, z]` NEListLit(Vec<SubExpr>), - /// `Some e` - SomeLit(SubExpr), /// `{ k1 : t1, k2 : t1 }` - RecordType(DupTreeMap<Label, SubExpr>), + RecordType(BTreeMap<Label, SubExpr>), /// `{ k1 = v1, k2 = v2 }` RecordLit(BTreeMap<Label, SubExpr>), /// `< k1 : t1, k2 >` - UnionType(DupTreeMap<Label, Option<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), + UnionType(BTreeMap<Label, Option<SubExpr>>), + + /// `x`, `x@n` + Var(V), + /// `λ(x : A) -> b` + Lam(Label, SubExpr, SubExpr), + /// `A -> B`, `∀(x : A) -> B` + Pi(Label, SubExpr, SubExpr), + /// `let x : t = r in e` + Let(Label, Option<SubExpr>, SubExpr, SubExpr), + + /// Operations + Op(OpKind<SubExpr>), + + /// `x : t` + Annot(SubExpr, SubExpr), + /// `assert : t` + Assert(SubExpr), + /// `./some/path` Import(Import<SubExpr>), } diff --git a/dhall/src/syntax/ast/map.rs b/dhall/src/syntax/ast/map.rs deleted file mode 100644 index 7a88204..0000000 --- a/dhall/src/syntax/ast/map.rs +++ /dev/null @@ -1,282 +0,0 @@ -/// A sorted map that allows multiple values for each key. -pub use dup_tree_map::DupTreeMap; -pub use dup_tree_set::DupTreeSet; - -mod known_size_iter { - pub struct KnownSizeIterator<I> { - pub iter: I, - pub size: usize, - } - - impl<I: Iterator> Iterator for KnownSizeIterator<I> { - type Item = I::Item; - - fn next(&mut self) -> Option<Self::Item> { - let next = self.iter.next(); - if next.is_some() { - self.size -= 1; - } - next - } - - fn size_hint(&self) -> (usize, Option<usize>) { - (self.size, Some(self.size)) - } - } - - // unsafe impl<I: Iterator> iter::TrustedLen for KnownSizeIterator<I> {} -} - -mod tuple { - mod sealed { - pub trait Sealed {} - } - pub trait Tuple: sealed::Sealed { - type First; - type Second; - } - impl<A, B> sealed::Sealed for (A, B) {} - impl<A, B> Tuple for (A, B) { - type First = A; - type Second = B; - } -} - -mod dup_tree_map { - use super::known_size_iter::KnownSizeIterator; - use super::tuple::Tuple; - use smallvec::SmallVec; - use std::collections::BTreeMap; - use std::iter; - - type OneOrMore<V> = SmallVec<[V; 1]>; - type DupTreeMapInternal<K, V> = BTreeMap<K, OneOrMore<V>>; - - #[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] - pub struct DupTreeMap<K, V> { - map: DupTreeMapInternal<K, V>, - size: usize, - } - - // Generic types and functions to construct the iterators for this struct. - type ZipRepeatIter<T> = iter::Zip< - iter::Repeat<<T as Tuple>::First>, - <<T as Tuple>::Second as IntoIterator>::IntoIter, - >; - type DupTreeMapIter<M> = KnownSizeIterator< - iter::FlatMap< - <M as IntoIterator>::IntoIter, - ZipRepeatIter<<M as IntoIterator>::Item>, - fn( - <M as IntoIterator>::Item, - ) -> ZipRepeatIter<<M as IntoIterator>::Item>, - >, - >; - - fn zip_repeat<K, I>((k, iter): (K, I)) -> ZipRepeatIter<(K, I)> - where - K: Clone, - I: IntoIterator, - { - iter::repeat(k).zip(iter.into_iter()) - } - - fn make_map_iter<M, K, I>(map: M, size: usize) -> DupTreeMapIter<M> - where - M: IntoIterator<Item = (K, I)>, - K: Clone, - I: IntoIterator, - { - KnownSizeIterator { - iter: map.into_iter().flat_map(zip_repeat), - size, - } - } - - pub type IterMut<'a, K, V> = - DupTreeMapIter<&'a mut DupTreeMapInternal<K, V>>; - pub type Iter<'a, K, V> = DupTreeMapIter<&'a DupTreeMapInternal<K, V>>; - pub type IntoIter<K, V> = DupTreeMapIter<DupTreeMapInternal<K, V>>; - - impl<K: Ord, V> DupTreeMap<K, V> { - pub fn new() -> Self { - DupTreeMap { - map: BTreeMap::new(), - size: 0, - } - } - - pub fn insert(&mut self, key: K, value: V) { - self.map.entry(key).or_default().push(value); - self.size += 1; - } - - pub fn len(&self) -> usize { - self.size - } - pub fn is_empty(&self) -> bool { - self.size == 0 - } - - pub fn iter(&self) -> Iter<'_, K, V> { - make_map_iter(&self.map, self.size) - } - - pub fn iter_mut(&mut self) -> IterMut<'_, K, V> { - make_map_iter(&mut self.map, self.size) - } - } - - impl<K, V> Default for DupTreeMap<K, V> - where - K: Ord, - { - fn default() -> Self { - Self::new() - } - } - - impl<K, V> IntoIterator for DupTreeMap<K, V> - where - K: Ord + Clone, - { - type Item = (K, V); - type IntoIter = IntoIter<K, V>; - - fn into_iter(self) -> Self::IntoIter { - make_map_iter(self.map, self.size) - } - } - - impl<'a, K, V> IntoIterator for &'a DupTreeMap<K, V> - where - K: Ord + 'a, - V: 'a, - { - type Item = (&'a K, &'a V); - type IntoIter = Iter<'a, K, V>; - - fn into_iter(self) -> Self::IntoIter { - self.iter() - } - } - - impl<'a, K, V> IntoIterator for &'a mut DupTreeMap<K, V> - where - K: Ord + 'a, - V: 'a, - { - type Item = (&'a K, &'a mut V); - type IntoIter = IterMut<'a, K, V>; - - fn into_iter(self) -> Self::IntoIter { - self.iter_mut() - } - } - - impl<K, V> iter::FromIterator<(K, V)> for DupTreeMap<K, V> - where - K: Ord, - { - fn from_iter<T>(iter: T) -> Self - where - T: IntoIterator<Item = (K, V)>, - { - let mut map = DupTreeMap::new(); - for (k, v) in iter { - map.insert(k, v); - } - map - } - } -} - -mod dup_tree_set { - use super::tuple::Tuple; - use super::DupTreeMap; - use std::iter; - - #[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] - pub struct DupTreeSet<K> { - map: DupTreeMap<K, ()>, - } - - type DupTreeSetIter<M> = iter::Map< - <M as IntoIterator>::IntoIter, - fn( - <M as IntoIterator>::Item, - ) -> <<M as IntoIterator>::Item as Tuple>::First, - >; - - pub type Iter<'a, K> = DupTreeSetIter<&'a DupTreeMap<K, ()>>; - pub type IntoIter<K> = DupTreeSetIter<DupTreeMap<K, ()>>; - - fn drop_second<A, B>((a, _): (A, B)) -> A { - a - } - - impl<K: Ord> DupTreeSet<K> { - pub fn new() -> Self { - DupTreeSet { - map: DupTreeMap::new(), - } - } - - pub fn len(&self) -> usize { - self.map.len() - } - pub fn is_empty(&self) -> bool { - self.map.is_empty() - } - - pub fn iter(&self) -> Iter<'_, K> { - self.map.iter().map(drop_second) - } - } - - impl<K> Default for DupTreeSet<K> - where - K: Ord, - { - fn default() -> Self { - Self::new() - } - } - - impl<K> IntoIterator for DupTreeSet<K> - where - K: Ord + Clone, - { - type Item = K; - type IntoIter = IntoIter<K>; - - fn into_iter(self) -> Self::IntoIter { - self.map.into_iter().map(drop_second) - } - } - - impl<'a, K> IntoIterator for &'a DupTreeSet<K> - where - K: Ord + 'a, - { - type Item = &'a K; - type IntoIter = Iter<'a, K>; - - fn into_iter(self) -> Self::IntoIter { - self.iter() - } - } - - impl<K> iter::FromIterator<K> for DupTreeSet<K> - where - K: Ord, - { - fn from_iter<T>(iter: T) -> Self - where - T: IntoIterator<Item = K>, - { - let map = iter.into_iter().map(|k| (k, ())).collect(); - DupTreeSet { map } - } - } -} diff --git a/dhall/src/syntax/ast/mod.rs b/dhall/src/syntax/ast/mod.rs index 1950154..c341af7 100644 --- a/dhall/src/syntax/ast/mod.rs +++ b/dhall/src/syntax/ast/mod.rs @@ -8,5 +8,4 @@ mod span; pub use span::*; mod text; pub use text::*; -pub mod map; pub mod visitor; diff --git a/dhall/src/syntax/ast/visitor.rs b/dhall/src/syntax/ast/visitor.rs index 0a0c5ef..7244d0a 100644 --- a/dhall/src/syntax/ast/visitor.rs +++ b/dhall/src/syntax/ast/visitor.rs @@ -1,22 +1,13 @@ +use itertools::Itertools; use std::iter::FromIterator; use crate::syntax::*; -fn vec<'a, T, U, Err>( - x: &'a [T], - f: impl FnMut(&'a T) -> Result<U, Err>, -) -> Result<Vec<U>, Err> { - x.iter().map(f).collect() -} - fn opt<'a, T, U, Err>( x: &'a Option<T>, f: impl FnOnce(&'a T) -> Result<U, Err>, ) -> Result<Option<U>, Err> { - Ok(match x { - Some(x) => Some(f(x)?), - None => None, - }) + x.as_ref().map(f).transpose() } fn dupmap<'a, SE1, SE2, T, Err>( @@ -30,27 +21,6 @@ where x.into_iter().map(|(k, x)| Ok((k.clone(), f(x)?))).collect() } -fn optdupmap<'a, SE1, SE2, T, Err>( - x: impl IntoIterator<Item = (&'a Label, &'a Option<SE1>)>, - mut f: impl FnMut(&'a SE1) -> Result<SE2, Err>, -) -> Result<T, Err> -where - SE1: 'a, - T: FromIterator<(Label, Option<SE2>)>, -{ - x.into_iter() - .map(|(k, x)| { - Ok(( - k.clone(), - match x { - Some(x) => Some(f(x)?), - None => None, - }, - )) - }) - .collect() -} - pub fn visit_ref<'a, F, SE1, SE2, Err>( input: &'a ExprKind<SE1>, mut f: F, @@ -60,54 +30,44 @@ where { // Can't use closures because of borrowing rules macro_rules! expr { + () => { + |e| Ok(expr!(e)) + }; ($e:expr) => { - f(None, $e) + f(None, $e)? }; ($l:expr, $e:expr) => { - f(Some($l), $e) + f(Some($l), $e)? + }; + } + macro_rules! opt { + () => { + |e| Ok(opt!(e)) + }; + ($e:expr) => { + opt($e, |e| Ok(expr!(e)))? }; } use crate::syntax::ExprKind::*; Ok(match input { Var(v) => Var(v.clone()), - Lam(l, t, e) => { - let t = expr!(t)?; - let e = expr!(l, e)?; - Lam(l.clone(), t, e) - } - Pi(l, t, e) => { - let t = expr!(t)?; - let e = expr!(l, e)?; - Pi(l.clone(), t, e) - } - Let(l, t, a, e) => { - let t = opt(t, &mut |e| expr!(e))?; - let a = expr!(a)?; - let e = expr!(l, e)?; - Let(l.clone(), t, a, e) - } - App(f, a) => App(expr!(f)?, expr!(a)?), - Annot(x, t) => Annot(expr!(x)?, expr!(t)?), + Lam(l, t, e) => Lam(l.clone(), expr!(t), expr!(l, e)), + Pi(l, t, e) => Pi(l.clone(), expr!(t), expr!(l, e)), + Let(l, t, a, e) => Let(l.clone(), opt!(t), expr!(a), expr!(l, e)), Const(k) => Const(*k), - Builtin(v) => Builtin(*v), Num(n) => Num(n.clone()), - TextLit(t) => TextLit(t.traverse_ref(|e| expr!(e))?), - BinOp(o, x, y) => BinOp(*o, expr!(x)?, expr!(y)?), - BoolIf(b, t, f) => BoolIf(expr!(b)?, expr!(t)?, expr!(f)?), - EmptyListLit(t) => EmptyListLit(expr!(t)?), - NEListLit(es) => NEListLit(vec(es, |e| expr!(e))?), - SomeLit(e) => SomeLit(expr!(e)?), - RecordType(kts) => RecordType(dupmap(kts, |e| expr!(e))?), - RecordLit(kvs) => RecordLit(dupmap(kvs, |e| expr!(e))?), - UnionType(kts) => UnionType(optdupmap(kts, |e| expr!(e))?), - Merge(x, y, t) => Merge(expr!(x)?, expr!(y)?, opt(t, |e| expr!(e))?), - ToMap(x, t) => ToMap(expr!(x)?, opt(t, |e| expr!(e))?), - 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)?), - Assert(e) => Assert(expr!(e)?), - Import(i) => Import(i.traverse_ref(|e| expr!(e))?), + Builtin(v) => Builtin(*v), + TextLit(t) => TextLit(t.traverse_ref(expr!())?), + SomeLit(e) => SomeLit(expr!(e)), + EmptyListLit(t) => EmptyListLit(expr!(t)), + NEListLit(es) => NEListLit(es.iter().map(expr!()).try_collect()?), + RecordType(kts) => RecordType(dupmap(kts, expr!())?), + RecordLit(kvs) => RecordLit(dupmap(kvs, expr!())?), + UnionType(kts) => UnionType(dupmap(kts, opt!())?), + Op(op) => Op(op.traverse_ref(expr!())?), + Annot(x, t) => Annot(expr!(x), expr!(t)), + Assert(e) => Assert(expr!(e)), + Import(i) => Import(i.traverse_ref(expr!())?), }) } diff --git a/dhall/src/syntax/binary/decode.rs b/dhall/src/syntax/binary/decode.rs index 3c93419..195bd0a 100644 --- a/dhall/src/syntax/binary/decode.rs +++ b/dhall/src/syntax/binary/decode.rs @@ -3,6 +3,7 @@ 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, @@ -24,9 +25,12 @@ fn rc(x: UnspannedExpr) -> Expr { } fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> { + use crate::builtins::Builtin; + use crate::operations::BinOp; use cbor::Value::*; - use syntax::{BinOp, Builtin, Const}; + use syntax::Const; use ExprKind::*; + use OpKind::*; Ok(rc(match data { String(s) => match Builtin::parse(s) { Some(b) => ExprKind::Builtin(b), @@ -66,7 +70,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> { let mut f = cbor_value_to_dhall(&f)?; for a in args { let a = cbor_value_to_dhall(&a)?; - f = rc(App(f, a)) + f = rc(Op(App(f, a))) } return Ok(f); } @@ -105,7 +109,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> { [U64(3), U64(13), x, y] => { let x = cbor_value_to_dhall(&x)?; let y = cbor_value_to_dhall(&y)?; - Completion(x, y) + Op(Completion(x, y)) } [U64(3), U64(n), x, y] => { let x = cbor_value_to_dhall(&x)?; @@ -131,11 +135,14 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> { )) } }; - BinOp(op, x, y) + Op(BinOp(op, x, y)) } [U64(4), t] => { let t = cbor_value_to_dhall(&t)?; - EmptyListLit(rc(App(rc(ExprKind::Builtin(Builtin::List)), t))) + EmptyListLit(rc(Op(App( + rc(ExprKind::Builtin(Builtin::List)), + t, + )))) } [U64(4), Null, rest @ ..] => { let rest = rest @@ -151,26 +158,26 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> { // Old-style optional literals [U64(5), t] => { let t = cbor_value_to_dhall(&t)?; - App(rc(ExprKind::Builtin(Builtin::OptionalNone)), t) + Op(App(rc(ExprKind::Builtin(Builtin::OptionalNone)), t)) } [U64(5), t, x] => { let x = cbor_value_to_dhall(&x)?; let t = cbor_value_to_dhall(&t)?; Annot( rc(SomeLit(x)), - rc(App(rc(ExprKind::Builtin(Builtin::Optional)), t)), + rc(Op(App(rc(ExprKind::Builtin(Builtin::Optional)), t))), ) } [U64(6), x, y] => { let x = cbor_value_to_dhall(&x)?; let y = cbor_value_to_dhall(&y)?; - Merge(x, y, None) + Op(Merge(x, y, None)) } [U64(6), x, y, z] => { let x = cbor_value_to_dhall(&x)?; let y = cbor_value_to_dhall(&y)?; let z = cbor_value_to_dhall(&z)?; - Merge(x, y, Some(z)) + Op(Merge(x, y, Some(z))) } [U64(7), Object(map)] => { let map = cbor_map_to_dhall_map(map)?; @@ -183,13 +190,13 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> { [U64(9), x, String(l)] => { let x = cbor_value_to_dhall(&x)?; let l = Label::from(l.as_str()); - Field(x, l) + Op(Field(x, l)) } [U64(10), x, Array(arr)] => { let x = cbor_value_to_dhall(&x)?; if let [y] = arr.as_slice() { let y = cbor_value_to_dhall(&y)?; - ProjectionByExpr(x, y) + Op(ProjectionByExpr(x, y)) } else { return Err(DecodeError::WrongFormatError( "projection-by-expr".to_owned(), @@ -207,7 +214,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> { )), }) .collect::<Result<_, _>>()?; - Projection(x, labels) + Op(Projection(x, labels)) } [U64(11), Object(map)] => { let map = cbor_map_to_dhall_opt_map(map)?; @@ -222,7 +229,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> { let x = cbor_value_to_dhall(&x)?; let y = cbor_value_to_dhall(&y)?; let z = cbor_value_to_dhall(&z)?; - BoolIf(x, y, z) + Op(BoolIf(x, y, z)) } [U64(15), U64(x)] => Num(NumKind::Natural(*x as Natural)), [U64(16), U64(x)] => Num(NumKind::Integer(*x as Integer)), @@ -416,12 +423,12 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> { } [U64(27), x] => { let x = cbor_value_to_dhall(&x)?; - ToMap(x, None) + Op(ToMap(x, None)) } [U64(27), x, y] => { let x = cbor_value_to_dhall(&x)?; let y = cbor_value_to_dhall(&y)?; - ToMap(x, Some(y)) + Op(ToMap(x, Some(y))) } [U64(28), x] => { let x = cbor_value_to_dhall(&x)?; diff --git a/dhall/src/syntax/binary/encode.rs b/dhall/src/syntax/binary/encode.rs index 8d22a9b..b6bbabe 100644 --- a/dhall/src/syntax/binary/encode.rs +++ b/dhall/src/syntax/binary/encode.rs @@ -2,9 +2,10 @@ use serde_cbor::value::value as cbor; use std::collections::BTreeMap; use std::vec; +use crate::builtins::Builtin; use crate::error::EncodeError; +use crate::operations::{BinOp, OpKind}; use crate::syntax; -use crate::syntax::map::DupTreeMap; use crate::syntax::{ Expr, ExprKind, FilePrefix, Hash, Import, ImportMode, ImportTarget, Label, Scheme, V, @@ -19,8 +20,7 @@ enum Serialize<'a> { Expr(&'a Expr), CBOR(cbor::Value), RecordMap(&'a BTreeMap<Label, Expr>), - RecordDupMap(&'a DupTreeMap<Label, Expr>), - UnionMap(&'a DupTreeMap<Label, Option<Expr>>), + UnionMap(&'a BTreeMap<Label, Option<Expr>>), } macro_rules! count { @@ -46,11 +46,11 @@ where { use cbor::Value::{String, I64, U64}; use std::iter::once; - use syntax::Builtin; use syntax::ExprKind::*; use syntax::NumKind::*; + use OpKind::*; - use self::Serialize::{RecordDupMap, RecordMap, UnionMap}; + use self::Serialize::{RecordMap, UnionMap}; fn expr(x: &Expr) -> self::Serialize<'_> { self::Serialize::Expr(x) } @@ -70,7 +70,9 @@ where let n: f64 = (*n).into(); ser.serialize_f64(n) } - BoolIf(x, y, z) => ser_seq!(ser; tag(14), expr(x), expr(y), expr(z)), + Op(BoolIf(x, y, z)) => { + ser_seq!(ser; tag(14), expr(x), expr(y), expr(z)) + } Var(V(l, n)) if l == &"_".into() => ser.serialize_u64(*n as u64), Var(V(l, n)) => ser_seq!(ser; label(l), U64(*n as u64)), Lam(l, x, y) if l == &"_".into() => { @@ -99,7 +101,7 @@ where ser_seq.serialize_element(&expr(bound_e))?; ser_seq.end() } - App(_, _) => { + Op(App(_, _)) => { let (f, args) = collect_nested_applications(e); ser.collect_seq( once(tag(0)) @@ -111,8 +113,8 @@ where Assert(x) => ser_seq!(ser; tag(19), expr(x)), SomeLit(x) => ser_seq!(ser; tag(5), null(), expr(x)), EmptyListLit(x) => match x.as_ref() { - App(f, a) => match f.as_ref() { - ExprKind::Builtin(Builtin::List) => { + Op(App(f, a)) => match f.as_ref() { + ExprKind::Builtin(self::Builtin::List) => { ser_seq!(ser; tag(4), expr(a)) } _ => ser_seq!(ser; tag(28), expr(x)), @@ -129,12 +131,12 @@ where Text(x) => cbor(String(x)), }))) } - RecordType(map) => ser_seq!(ser; tag(7), RecordDupMap(map)), + RecordType(map) => ser_seq!(ser; tag(7), RecordMap(map)), RecordLit(map) => ser_seq!(ser; tag(8), RecordMap(map)), UnionType(map) => ser_seq!(ser; tag(11), UnionMap(map)), - Field(x, l) => ser_seq!(ser; tag(9), expr(x), label(l)), - BinOp(op, x, y) => { - use syntax::BinOp::*; + Op(Field(x, l)) => ser_seq!(ser; tag(9), expr(x), label(l)), + Op(BinOp(op, x, y)) => { + use self::BinOp::*; let op = match op { BoolOr => 0, BoolAnd => 1, @@ -152,21 +154,23 @@ where }; ser_seq!(ser; tag(3), U64(op), expr(x), expr(y)) } - Merge(x, y, None) => ser_seq!(ser; tag(6), expr(x), expr(y)), - Merge(x, y, Some(z)) => { + Op(Merge(x, y, None)) => ser_seq!(ser; tag(6), expr(x), expr(y)), + Op(Merge(x, y, Some(z))) => { ser_seq!(ser; tag(6), expr(x), expr(y), expr(z)) } - ToMap(x, None) => ser_seq!(ser; tag(27), expr(x)), - ToMap(x, Some(y)) => ser_seq!(ser; tag(27), expr(x), expr(y)), - Projection(x, ls) => ser.collect_seq( + Op(ToMap(x, None)) => ser_seq!(ser; tag(27), expr(x)), + Op(ToMap(x, Some(y))) => ser_seq!(ser; tag(27), expr(x), expr(y)), + Op(Projection(x, ls)) => ser.collect_seq( once(tag(10)) .chain(once(expr(x))) .chain(ls.iter().map(label)), ), - ProjectionByExpr(x, y) => { + Op(ProjectionByExpr(x, y)) => { ser_seq!(ser; tag(10), expr(x), vec![expr(y)]) } - Completion(x, y) => ser_seq!(ser; tag(3), tag(13), expr(x), expr(y)), + Op(Completion(x, y)) => { + ser_seq!(ser; tag(3), tag(13), expr(x), expr(y)) + } Import(import) => serialize_import(ser, import), } } @@ -260,11 +264,6 @@ impl<'a> serde::ser::Serialize for Serialize<'a> { match self { Serialize::Expr(e) => serialize_subexpr(ser, e), Serialize::CBOR(v) => v.serialize(ser), - Serialize::RecordDupMap(map) => { - ser.collect_map(map.iter().map(|(k, v)| { - (cbor::Value::String(k.into()), Serialize::Expr(v)) - })) - } Serialize::RecordMap(map) => { ser.collect_map(map.iter().map(|(k, v)| { (cbor::Value::String(k.into()), Serialize::Expr(v)) @@ -286,7 +285,7 @@ impl<'a> serde::ser::Serialize for Serialize<'a> { fn collect_nested_applications<'a>(e: &'a Expr) -> (&'a Expr, Vec<&'a Expr>) { fn go<'a>(e: &'a Expr, vec: &mut Vec<&'a Expr>) -> &'a Expr { match e.as_ref() { - ExprKind::App(f, a) => { + ExprKind::Op(OpKind::App(f, a)) => { vec.push(a); go(f, vec) } diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs index 6f5949f..dcaf5e4 100644 --- a/dhall/src/syntax/text/parser.rs +++ b/dhall/src/syntax/text/parser.rs @@ -1,13 +1,13 @@ use itertools::Itertools; use pest::prec_climber as pcl; use pest::prec_climber::PrecClimber; -use std::collections::BTreeMap; +use std::collections::{BTreeMap, BTreeSet}; use std::iter::once; use std::rc::Rc; use pest_consume::{match_nodes, Parser}; -use crate::syntax::map::{DupTreeMap, DupTreeSet}; +use crate::operations::OpKind::*; use crate::syntax::ExprKind::*; use crate::syntax::NumKind::*; use crate::syntax::{ @@ -31,50 +31,10 @@ pub type ParseResult<T> = Result<T, ParseError>; #[derive(Debug)] enum Selector { Field(Label), - Projection(DupTreeSet<Label>), + Projection(BTreeSet<Label>), ProjectionByExpr(Expr), } -impl crate::syntax::Builtin { - pub fn parse(s: &str) -> Option<Self> { - use crate::syntax::Builtin::*; - match s { - "Bool" => Some(Bool), - "Natural" => Some(Natural), - "Integer" => Some(Integer), - "Double" => Some(Double), - "Text" => Some(Text), - "List" => Some(List), - "Optional" => Some(Optional), - "None" => Some(OptionalNone), - "Natural/build" => Some(NaturalBuild), - "Natural/fold" => Some(NaturalFold), - "Natural/isZero" => Some(NaturalIsZero), - "Natural/even" => Some(NaturalEven), - "Natural/odd" => Some(NaturalOdd), - "Natural/toInteger" => Some(NaturalToInteger), - "Natural/show" => Some(NaturalShow), - "Natural/subtract" => Some(NaturalSubtract), - "Integer/toDouble" => Some(IntegerToDouble), - "Integer/show" => Some(IntegerShow), - "Integer/negate" => Some(IntegerNegate), - "Integer/clamp" => Some(IntegerClamp), - "Double/show" => Some(DoubleShow), - "List/build" => Some(ListBuild), - "List/fold" => Some(ListFold), - "List/length" => Some(ListLength), - "List/head" => Some(ListHead), - "List/last" => Some(ListLast), - "List/indexed" => Some(ListIndexed), - "List/reverse" => Some(ListReverse), - "Optional/fold" => Some(OptionalFold), - "Optional/build" => Some(OptionalBuild), - "Text/show" => Some(TextShow), - _ => None, - } - } -} - fn input_to_span(input: ParseInput) -> Span { Span::make(input.user_data().clone(), input.as_pair().as_span()) } @@ -128,7 +88,7 @@ fn trim_indent(lines: &mut Vec<ParsedText>) { /// Insert the expr into the map; in case of collision, create a RecursiveRecordMerge node. fn insert_recordlit_entry(map: &mut BTreeMap<Label, Expr>, l: Label, e: Expr) { - use crate::syntax::BinOp::RecursiveRecordMerge; + use crate::operations::BinOp::RecursiveRecordMerge; use std::collections::btree_map::Entry; match map.entry(l) { Entry::Vacant(entry) => { @@ -138,7 +98,7 @@ fn insert_recordlit_entry(map: &mut BTreeMap<Label, Expr>, l: Label, e: Expr) { let dummy = Expr::new(Num(Bool(false)), Span::Artificial); let other = entry.insert(dummy); entry.insert(Expr::new( - BinOp(RecursiveRecordMerge, other, e), + Op(BinOp(RecursiveRecordMerge, other, e)), Span::DuplicateRecordFieldsSugar, )); } @@ -146,18 +106,21 @@ fn insert_recordlit_entry(map: &mut BTreeMap<Label, Expr>, l: Label, e: Expr) { } fn desugar_with_expr(x: Expr, labels: &[Label], y: Expr) -> Expr { - use crate::syntax::BinOp::RightBiasedRecordMerge; + use crate::operations::BinOp::RightBiasedRecordMerge; let expr = |k| Expr::new(k, Span::WithSugar); match labels { [] => y, [l, rest @ ..] => { - let res = - desugar_with_expr(expr(Field(x.clone(), l.clone())), rest, y); - expr(BinOp( + let res = desugar_with_expr( + expr(Op(Field(x.clone(), l.clone()))), + rest, + y, + ); + expr(Op(BinOp( RightBiasedRecordMerge, x, expr(RecordLit(once((l.clone(), res)).collect())), - )) + ))) } } } @@ -387,7 +350,7 @@ impl DhallParser { #[alias(expression)] fn builtin(input: ParseInput) -> ParseResult<Expr> { let s = input.as_str(); - let e = match crate::syntax::Builtin::parse(s) { + let e = match crate::builtins::Builtin::parse(s) { Some(b) => Builtin(b), None => match s { "True" => Num(Bool(true)), @@ -725,7 +688,7 @@ impl DhallParser { }, [if_(()), expression(cond), expression(left), expression(right)] => { - spanned(input, BoolIf(cond, left, right)) + spanned(input, Op(BoolIf(cond, left, right))) }, [let_binding(bindings).., expression(final_expr)] => { bindings.rev().fold( @@ -747,13 +710,13 @@ impl DhallParser { spanned(input, Pi("_".into(), typ, body)) }, [merge(()), expression(x), expression(y), expression(z)] => { - spanned(input, Merge(x, y, Some(z))) + spanned(input, Op(Merge(x, y, Some(z)))) }, [assert(()), expression(x)] => { spanned(input, Assert(x)) }, [toMap(()), expression(x), expression(y)] => { - spanned(input, ToMap(x, Some(y))) + spanned(input, Op(ToMap(x, Some(y)))) }, [expression(e), expression(annot)] => { spanned(input, Annot(e, annot)) @@ -780,7 +743,7 @@ impl DhallParser { op: ParseInput, r: Expr, ) -> ParseResult<Expr> { - use crate::syntax::BinOp::*; + use crate::operations::BinOp::*; use Rule::*; let op = match op.as_rule() { import_alt => ImportAlt, @@ -801,7 +764,7 @@ impl DhallParser { } }; - Ok(spanned_union(l.span(), r.span(), BinOp(op, l, r))) + Ok(spanned_union(l.span(), r.span(), Op(BinOp(op, l, r)))) } fn Some_(_input: ParseInput) -> ParseResult<()> { @@ -840,7 +803,7 @@ impl DhallParser { spanned_union( acc.span(), e.span(), - App(acc, e) + Op(App(acc, e)) ) } ) @@ -855,10 +818,10 @@ impl DhallParser { spanned(input, SomeLit(e)) }, [merge(()), expression(x), expression(y)] => { - spanned(input, Merge(x, y, None)) + spanned(input, Op(Merge(x, y, None))) }, [toMap(()), expression(x)] => { - spanned(input, ToMap(x, None)) + spanned(input, Op(ToMap(x, None))) }, [expression(e)] => e, )) @@ -875,7 +838,7 @@ impl DhallParser { spanned_union( acc.span(), e.span(), - Completion(acc, e), + Op(Completion(acc, e)), ) } ) @@ -895,9 +858,9 @@ impl DhallParser { acc.span(), e.1, match e.0 { - Selector::Field(l) => Field(acc, l), - Selector::Projection(ls) => Projection(acc, ls), - Selector::ProjectionByExpr(e) => ProjectionByExpr(acc, e) + Selector::Field(l) => Op(Field(acc, l)), + Selector::Projection(ls) => Op(Projection(acc, ls)), + Selector::ProjectionByExpr(e) => Op(ProjectionByExpr(acc, e)) } ) } @@ -915,9 +878,20 @@ impl DhallParser { Ok((stor, input_to_span(input))) } - fn labels(input: ParseInput) -> ParseResult<DupTreeSet<Label>> { - Ok(match_nodes!(input.into_children(); - [label(ls)..] => ls.collect(), + fn labels(input: ParseInput) -> ParseResult<BTreeSet<Label>> { + Ok(match_nodes!(input.children(); + [label(ls)..] => { + let mut set = BTreeSet::default(); + for l in ls { + if set.contains(&l) { + return Err( + input.error(format!("Duplicate field in projection")) + ) + } + set.insert(l); + } + set + }, )) } @@ -957,9 +931,26 @@ impl DhallParser { fn non_empty_record_type( input: ParseInput, - ) -> ParseResult<DupTreeMap<Label, Expr>> { - Ok(match_nodes!(input.into_children(); - [record_type_entry(entries)..] => entries.collect() + ) -> ParseResult<BTreeMap<Label, Expr>> { + Ok(match_nodes!(input.children(); + [record_type_entry(entries)..] => { + let mut map = BTreeMap::default(); + for (l, t) in entries { + use std::collections::btree_map::Entry; + match map.entry(l) { + Entry::Occupied(_) => { + return Err(input.error( + "Duplicate field in record type" + .to_string(), + )); + } + Entry::Vacant(e) => { + e.insert(t); + } + } + } + map + }, )) } @@ -1008,7 +999,24 @@ impl DhallParser { fn union_type(input: ParseInput) -> ParseResult<UnspannedExpr> { let map = match_nodes!(input.children(); [empty_union_type(_)] => Default::default(), - [union_type_entry(entries)..] => entries.collect(), + [union_type_entry(entries)..] => { + let mut map = BTreeMap::default(); + for (l, t) in entries { + use std::collections::btree_map::Entry; + match map.entry(l) { + Entry::Occupied(_) => { + return Err(input.error( + "Duplicate variant in union type" + .to_string(), + )); + } + Entry::Vacant(e) => { + e.insert(t); + } + } + } + map + }, ); Ok(UnionType(map)) } diff --git a/dhall/src/syntax/text/printer.rs b/dhall/src/syntax/text/printer.rs index 378f408..9e90660 100644 --- a/dhall/src/syntax/text/printer.rs +++ b/dhall/src/syntax/text/printer.rs @@ -1,3 +1,5 @@ +use crate::builtins::Builtin; +use crate::operations::{BinOp, OpKind}; use crate::syntax::*; use itertools::Itertools; use std::fmt::{self, Display}; @@ -5,15 +7,16 @@ use std::fmt::{self, Display}; // There is a one-to-one correspondence between the formatter and the grammar. Each phase is // named after a corresponding grammar group, and the structure of the formatter reflects // the relationship between the corresponding grammar rules. This leads to the nice property -// of automatically getting all the parentheses and precedences right. +// of automatically getting all the parentheses and precedences right (in a manner dual do Pratt +// parsing). #[derive(Debug, Copy, Clone, Ord, PartialOrd, Eq, PartialEq)] enum PrintPhase { // `expression` Base, // `operator-expression` Operator, - // All the operator `*-expression`s - BinOp(ast::BinOp), + // All the `<operator>-expression`s + BinOp(self::BinOp), // `application-expression` App, // `import-expression` @@ -36,7 +39,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 ExprKind::*; + use OpKind::*; use PrintPhase::*; let with_base = self.map_ref(|e| PhasedExpr(e, Base)); match with_base { @@ -47,31 +51,33 @@ impl UnspannedExpr { Pi(a, b, c) } } - Merge(a, b, c) => Merge( + Op(Merge(a, b, c)) => Op(Merge( a.phase(PrintPhase::Import), b.phase(PrintPhase::Import), c.map(|x| x.phase(PrintPhase::App)), - ), - ToMap(a, b) => ToMap( + )), + Op(ToMap(a, b)) => Op(ToMap( a.phase(PrintPhase::Import), b.map(|x| x.phase(PrintPhase::App)), - ), + )), Annot(a, b) => Annot(a.phase(Operator), b), - ExprKind::BinOp(op, a, b) => ExprKind::BinOp( + Op(OpKind::BinOp(op, a, b)) => Op(OpKind::BinOp( op, a.phase(PrintPhase::BinOp(op)), b.phase(PrintPhase::BinOp(op)), - ), + )), SomeLit(e) => SomeLit(e.phase(PrintPhase::Import)), - ExprKind::App(f, a) => ExprKind::App( + Op(OpKind::App(f, a)) => Op(OpKind::App( f.phase(PrintPhase::App), a.phase(PrintPhase::Import), - ), - Field(a, b) => Field(a.phase(Primitive), b), - Projection(e, ls) => Projection(e.phase(Primitive), ls), - ProjectionByExpr(a, b) => ProjectionByExpr(a.phase(Primitive), b), - Completion(a, b) => { - Completion(a.phase(Primitive), b.phase(Primitive)) + )), + Op(Field(a, b)) => Op(Field(a.phase(Primitive), b)), + Op(Projection(e, ls)) => Op(Projection(e.phase(Primitive), ls)), + Op(ProjectionByExpr(a, b)) => { + Op(ProjectionByExpr(a.phase(Primitive), b)) + } + Op(Completion(a, b)) => { + Op(Completion(a.phase(Primitive), b.phase(Primitive))) } ExprKind::Import(a) => { ExprKind::Import(a.map_ref(|x| x.phase(PrintPhase::Import))) @@ -85,22 +91,24 @@ impl UnspannedExpr { f: &mut fmt::Formatter, phase: PrintPhase, ) -> Result<(), fmt::Error> { - use crate::syntax::ExprKind::*; + use ExprKind::*; + use OpKind::*; let needs_paren = match self { Lam(_, _, _) - | BoolIf(_, _, _) | Pi(_, _, _) | Let(_, _, _, _) - | EmptyListLit(_) | SomeLit(_) - | Merge(_, _, _) - | ToMap(_, _) + | EmptyListLit(_) + | Op(BoolIf(_, _, _)) + | Op(Merge(_, _, _)) + | Op(ToMap(_, _)) | Annot(_, _) => phase > PrintPhase::Base, - // Precedence is magically handled by the ordering of BinOps. - ExprKind::BinOp(op, _, _) => phase > PrintPhase::BinOp(*op), - ExprKind::App(_, _) => phase > PrintPhase::App, - Completion(_, _) => phase > PrintPhase::Import, + // Precedence is magically handled by the ordering of BinOps. This is reverse Pratt + // parsing. + Op(BinOp(op, _, _)) => phase > PrintPhase::BinOp(*op), + Op(App(_, _)) => phase > PrintPhase::App, + Op(Completion(_, _)) => phase > PrintPhase::Import, _ => false, }; @@ -143,12 +151,10 @@ impl<SE: Display + Clone> Display for ExprKind<SE> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { use crate::syntax::ExprKind::*; match self { + Var(a) => a.fmt(f)?, Lam(a, b, c) => { write!(f, "λ({} : {}) → {}", a, b, c)?; } - BoolIf(a, b, c) => { - write!(f, "if {} then {} else {}", a, b, c)?; - } Pi(a, b, c) if &String::from(a) == "_" => { write!(f, "{} → {}", b, c)?; } @@ -162,14 +168,62 @@ impl<SE: Display + Clone> Display for ExprKind<SE> { } write!(f, " = {} in {}", c, d)?; } + Const(k) => k.fmt(f)?, + Builtin(v) => v.fmt(f)?, + Num(a) => a.fmt(f)?, + TextLit(a) => a.fmt(f)?, + SomeLit(e) => { + write!(f, "Some {}", e)?; + } EmptyListLit(t) => { write!(f, "[] : {}", t)?; } NEListLit(es) => { fmt_list("[", ", ", "]", es, f, Display::fmt)?; } - SomeLit(e) => { - write!(f, "Some {}", e)?; + RecordLit(a) if a.is_empty() => f.write_str("{=}")?, + RecordLit(a) => fmt_list("{ ", ", ", " }", a, f, |(k, v), f| { + write!(f, "{} = {}", k, v) + })?, + RecordType(a) if a.is_empty() => f.write_str("{}")?, + RecordType(a) => fmt_list("{ ", ", ", " }", a, f, |(k, t), f| { + write!(f, "{} : {}", k, t) + })?, + UnionType(a) => fmt_list("< ", " | ", " >", a, f, |(k, v), f| { + write!(f, "{}", k)?; + if let Some(v) = v { + write!(f, ": {}", v)?; + } + Ok(()) + })?, + Op(op) => { + op.fmt(f)?; + } + Annot(a, b) => { + write!(f, "{} : {}", a, b)?; + } + Assert(a) => { + write!(f, "assert : {}", a)?; + } + Import(a) => a.fmt(f)?, + } + Ok(()) + } +} + +/// 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 OpKind::*; + match self { + App(a, b) => { + write!(f, "{} {}", a, b)?; + } + BinOp(op, a, b) => { + write!(f, "{} {} {}", a, op, b)?; + } + BoolIf(a, b, c) => { + write!(f, "if {} then {} else {}", a, b, c)?; } Merge(a, b, c) => { write!(f, "merge {} {}", a, b)?; @@ -183,41 +237,9 @@ impl<SE: Display + Clone> Display for ExprKind<SE> { write!(f, " : {}", b)?; } } - Annot(a, b) => { - write!(f, "{} : {}", a, b)?; - } - Assert(a) => { - write!(f, "assert : {}", a)?; - } - ExprKind::BinOp(op, a, b) => { - write!(f, "{} {} {}", a, op, b)?; - } - ExprKind::App(a, b) => { - write!(f, "{} {}", a, b)?; - } Field(a, b) => { write!(f, "{}.{}", a, b)?; } - Var(a) => a.fmt(f)?, - Const(k) => k.fmt(f)?, - Builtin(v) => v.fmt(f)?, - Num(a) => a.fmt(f)?, - TextLit(a) => a.fmt(f)?, - RecordType(a) if a.is_empty() => f.write_str("{}")?, - RecordType(a) => fmt_list("{ ", ", ", " }", a, f, |(k, t), f| { - write!(f, "{} : {}", k, t) - })?, - RecordLit(a) if a.is_empty() => f.write_str("{=}")?, - RecordLit(a) => fmt_list("{ ", ", ", " }", a, f, |(k, v), f| { - write!(f, "{} = {}", k, v) - })?, - UnionType(a) => fmt_list("< ", " | ", " >", a, f, |(k, v), f| { - write!(f, "{}", k)?; - if let Some(v) = v { - write!(f, ": {}", v)?; - } - Ok(()) - })?, Projection(e, ls) => { write!(f, "{}.", e)?; fmt_list("{ ", ", ", " }", ls, f, Display::fmt)?; @@ -228,7 +250,6 @@ impl<SE: Display + Clone> Display for ExprKind<SE> { Completion(a, b) => { write!(f, "{}::{}", a, b)?; } - Import(a) => a.fmt(f)?, } Ok(()) } @@ -315,7 +336,7 @@ impl Display for Const { impl Display for BinOp { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { - use crate::syntax::BinOp::*; + use BinOp::*; f.write_str(match self { BoolOr => "||", TextAppend => "++", @@ -363,7 +384,7 @@ impl Display for Label { let is_reserved = match s.as_str() { "let" | "in" | "if" | "then" | "else" | "Type" | "Kind" | "Sort" | "True" | "False" | "Some" => true, - _ => crate::syntax::Builtin::parse(&s).is_some(), + _ => Builtin::parse(&s).is_some(), }; if !is_reserved && s.chars().all(|c| c.is_ascii_alphanumeric()) { write!(f, "{}", s) @@ -461,45 +482,6 @@ impl<SubExpr: Display> Display for Import<SubExpr> { } } -impl Display for Builtin { - fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { - use crate::syntax::Builtin::*; - f.write_str(match *self { - Bool => "Bool", - Natural => "Natural", - Integer => "Integer", - Double => "Double", - Text => "Text", - List => "List", - Optional => "Optional", - OptionalNone => "None", - NaturalBuild => "Natural/build", - NaturalFold => "Natural/fold", - NaturalIsZero => "Natural/isZero", - NaturalEven => "Natural/even", - NaturalOdd => "Natural/odd", - NaturalToInteger => "Natural/toInteger", - NaturalShow => "Natural/show", - NaturalSubtract => "Natural/subtract", - IntegerToDouble => "Integer/toDouble", - IntegerNegate => "Integer/negate", - IntegerClamp => "Integer/clamp", - IntegerShow => "Integer/show", - DoubleShow => "Double/show", - ListBuild => "List/build", - ListFold => "List/fold", - ListLength => "List/length", - ListHead => "List/head", - ListLast => "List/last", - ListIndexed => "List/indexed", - ListReverse => "List/reverse", - OptionalFold => "Optional/fold", - OptionalBuild => "Optional/build", - TextShow => "Text/show", - }) - } -} - impl Display for Scheme { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { use crate::syntax::Scheme::*; diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 5bcdb1c..468d550 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -225,7 +225,7 @@ impl TestFile { if Self::force_update() { self.write_ui(x)?; } else { - assert_eq_pretty_str!(msg, expected); + assert_eq_pretty_str!(expected, msg); } } Ok(()) diff --git a/dhall/tests/type-inference/failure/mixedUnions.txt b/dhall/tests/type-inference/failure/mixedUnions.txt index a6ca913..2b307d0 100644 --- a/dhall/tests/type-inference/failure/mixedUnions.txt +++ b/dhall/tests/type-inference/failure/mixedUnions.txt @@ -1,6 +1,6 @@ -Type error: error: InvalidFieldType - --> <current file>:1:1 +Type error: error: InvalidVariantType + --> <current file>:1:28 | 1 | < Left : Natural | Right : Type > - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType + | ^^^^ InvalidVariantType | diff --git a/dhall/tests/type-inference/failure/recordOfKind.txt b/dhall/tests/type-inference/failure/recordOfKind.txt index 7dcbe4f..9a243c3 100644 --- a/dhall/tests/type-inference/failure/recordOfKind.txt +++ b/dhall/tests/type-inference/failure/recordOfKind.txt @@ -1,6 +1,6 @@ Type error: error: InvalidFieldType - --> <current file>:1:1 + --> <current file>:1:7 | 1 | { a = Kind } - | ^^^^^^^^^^^^ InvalidFieldType + | ^^^^ InvalidFieldType | diff --git a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt index fa8b153..a83bb4f 100644 --- a/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt +++ b/dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt @@ -1,6 +1,6 @@ Type error: error: InvalidFieldType - --> <current file>:1:1 + --> <current file>:1:17 | 1 | { x = Type, y = Kind } - | ^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType + | ^^^^ InvalidFieldType | diff --git a/dhall/tests/type-inference/failure/unit/RecordProjectionDuplicateFields.txt b/dhall/tests/type-inference/failure/unit/RecordProjectionDuplicateFields.txt index 05c3eed..7b35481 100644 --- a/dhall/tests/type-inference/failure/unit/RecordProjectionDuplicateFields.txt +++ b/dhall/tests/type-inference/failure/unit/RecordProjectionDuplicateFields.txt @@ -1,6 +1,6 @@ -Type error: error: ProjectionDuplicateField - --> <current file>:1:1 + --> 1:11 | -1 | { x = 1 }.{ x, x } - | ^^^^^^^^^^^^^^^^^^ ProjectionDuplicateField +1 | { x = 1 }.{ x, x }␊ + | ^------^ | + = Duplicate field in projection diff --git a/dhall/tests/type-inference/failure/unit/RecordTypeDuplicateFields.txt b/dhall/tests/type-inference/failure/unit/RecordTypeDuplicateFields.txt index d8bec44..aced8a9 100644 --- a/dhall/tests/type-inference/failure/unit/RecordTypeDuplicateFields.txt +++ b/dhall/tests/type-inference/failure/unit/RecordTypeDuplicateFields.txt @@ -1,6 +1,6 @@ -Type error: error: RecordTypeDuplicateField - --> <current file>:1:1 + --> 1:3 | -1 | { x: Natural, x: Natural } - | ^^^^^^^^^^^^^^^^^^^^^^^^^^ RecordTypeDuplicateField +1 | { x: Natural, x: Natural }␊ + | ^--------------------^ | + = Duplicate field in record type diff --git a/dhall/tests/type-inference/failure/unit/RecordTypeValueMember.txt b/dhall/tests/type-inference/failure/unit/RecordTypeValueMember.txt index 81815a2..c6c274c 100644 --- a/dhall/tests/type-inference/failure/unit/RecordTypeValueMember.txt +++ b/dhall/tests/type-inference/failure/unit/RecordTypeValueMember.txt @@ -1,6 +1,6 @@ Type error: error: InvalidFieldType - --> <current file>:1:1 + --> <current file>:1:7 | 1 | { x : True } - | ^^^^^^^^^^^^ InvalidFieldType + | ^^^^ InvalidFieldType | diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt index 146bf7f..6a6da80 100644 --- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt +++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt @@ -1,6 +1,6 @@ Type error: error: InvalidFieldType - --> <current file>:1:16 + --> <current file>:1:22 | 1 | { x = Bool } ⫽ { x = Kind } - | ^^^^^^^^^^^^ InvalidFieldType + | ^^^^ InvalidFieldType | diff --git a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt index 71914e1..322e7f4 100644 --- a/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt +++ b/dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt @@ -1,6 +1,6 @@ Type error: error: InvalidFieldType - --> <current file>:1:15 + --> <current file>:1:21 | 1 | { x = {=} } ⫽ { x = Kind } - | ^^^^^^^^^^^^ InvalidFieldType + | ^^^^ InvalidFieldType | diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants1.txt b/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants1.txt index 84bfe4d..9984693 100644 --- a/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants1.txt +++ b/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants1.txt @@ -1,6 +1,6 @@ -Type error: error: UnionTypeDuplicateField - --> <current file>:1:1 + --> 1:2 | -1 | <x | x> - | ^^^^^^^ UnionTypeDuplicateField +1 | <x | x>␊ + | ^---^ | + = Duplicate variant in union type diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants2.txt b/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants2.txt index eb20b12..fdf6dc0 100644 --- a/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants2.txt +++ b/dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants2.txt @@ -1,6 +1,6 @@ -Type error: error: UnionTypeDuplicateField - --> <current file>:1:1 + --> 1:2 | -1 | <x | x: Natural> - | ^^^^^^^^^^^^^^^^ UnionTypeDuplicateField +1 | <x | x: Natural>␊ + | ^------------^ | + = Duplicate variant in union type diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt index 44ce7a3..ae6c845 100644 --- a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt +++ b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt @@ -1,6 +1,6 @@ -Type error: error: InvalidFieldType - --> <current file>:1:1 +Type error: error: InvalidVariantType + --> <current file>:1:18 | 1 | < x : Bool | y : Type > - | ^^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType + | ^^^^ InvalidVariantType | diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt index 01f706d..faf81a9 100644 --- a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt +++ b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt @@ -1,6 +1,6 @@ -Type error: error: InvalidFieldType - --> <current file>:1:1 +Type error: error: InvalidVariantType + --> <current file>:1:18 | 1 | < x : Kind | y : Type > - | ^^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType + | ^^^^ InvalidVariantType | diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt index 496462d..bbfb1f3 100644 --- a/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt +++ b/dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt @@ -1,6 +1,6 @@ -Type error: error: InvalidFieldType - --> <current file>:1:1 +Type error: error: InvalidVariantType + --> <current file>:1:18 | 1 | < x : Kind | y : Bool > - | ^^^^^^^^^^^^^^^^^^^^^^^ InvalidFieldType + | ^^^^ InvalidVariantType | diff --git a/dhall/tests/type-inference/failure/unit/UnionTypeNotType.txt b/dhall/tests/type-inference/failure/unit/UnionTypeNotType.txt index 450a3dd..cedf06e 100644 --- a/dhall/tests/type-inference/failure/unit/UnionTypeNotType.txt +++ b/dhall/tests/type-inference/failure/unit/UnionTypeNotType.txt @@ -1,6 +1,6 @@ -Type error: error: InvalidFieldType - --> <current file>:1:1 +Type error: error: InvalidVariantType + --> <current file>:1:7 | 1 | < x : True > - | ^^^^^^^^^^^^ InvalidFieldType + | ^^^^ InvalidVariantType | diff --git a/serde_dhall/src/value.rs b/serde_dhall/src/value.rs index d6631da..03cfdba 100644 --- a/serde_dhall/src/value.rs +++ b/serde_dhall/src/value.rs @@ -1,7 +1,9 @@ use std::collections::{BTreeMap, HashMap}; +use dhall::builtins::Builtin; +use dhall::operations::OpKind; use dhall::semantics::{Hir, HirKind, Nir, NirKind}; -use dhall::syntax::{Builtin, Expr, ExprKind, NumKind, Span}; +use dhall::syntax::{Expr, ExprKind, NumKind, Span}; use crate::{Error, ErrorKind, FromDhall, Result, Sealed}; @@ -218,13 +220,14 @@ impl SimpleType { SimpleType::Integer => ExprKind::Builtin(Builtin::Integer), SimpleType::Double => ExprKind::Builtin(Builtin::Double), SimpleType::Text => ExprKind::Builtin(Builtin::Text), - SimpleType::Optional(t) => ExprKind::App( + SimpleType::Optional(t) => ExprKind::Op(OpKind::App( hir(ExprKind::Builtin(Builtin::Optional)), t.to_hir(), - ), - SimpleType::List(t) => { - ExprKind::App(hir(ExprKind::Builtin(Builtin::List)), t.to_hir()) - } + )), + SimpleType::List(t) => ExprKind::Op(OpKind::App( + hir(ExprKind::Builtin(Builtin::List)), + t.to_hir(), + )), SimpleType::Record(kts) => ExprKind::RecordType( kts.iter() .map(|(k, t)| (k.as_str().into(), t.to_hir())) diff --git a/tests_buffer b/tests_buffer index afb270f..bd76d36 100644 --- a/tests_buffer +++ b/tests_buffer @@ -35,5 +35,6 @@ failure/ merge { x = True, y = 1 } < x | y >.x merge {x=...,y=...} <x>.x merge {x=...,y=...} <x:T>.x +fix unit_RightBiasedRecordMergeMixedKinds3 & 2 & unit_RecordMixedKinds3 equivalence: |