summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2020-04-07 12:22:27 +0100
committerGitHub2020-04-07 12:22:27 +0100
commit832c99a3b28e70512d580a51fc378473834b2891 (patch)
tree95b417cb3349bd1896f661a3fce67531c52d5b7b /dhall
parentd35cb130d80d628807a4247ddf84a8d0230c87ab (diff)
parent214a3c998a3358849495b54a60d46f626b131f0a (diff)
Merge pull request #159 from Nadrieril/operations
Factor out operations
Diffstat (limited to '')
-rw-r--r--dhall/build.rs3
-rw-r--r--dhall/src/builtins.rs (renamed from dhall/src/semantics/builtins.rs)153
-rw-r--r--dhall/src/lib.rs2
-rw-r--r--dhall/src/operations/kind.rs97
-rw-r--r--dhall/src/operations/mod.rs6
-rw-r--r--dhall/src/operations/normalization.rs306
-rw-r--r--dhall/src/operations/typecheck.rs510
-rw-r--r--dhall/src/semantics/mod.rs2
-rw-r--r--dhall/src/semantics/nze/nir.rs84
-rw-r--r--dhall/src/semantics/nze/normalize.rs406
-rw-r--r--dhall/src/semantics/resolve/resolve.rs29
-rw-r--r--dhall/src/semantics/tck/tir.rs3
-rw-r--r--dhall/src/semantics/tck/typecheck.rs603
-rw-r--r--dhall/src/syntax/ast/expr.rs134
-rw-r--r--dhall/src/syntax/ast/map.rs282
-rw-r--r--dhall/src/syntax/ast/mod.rs1
-rw-r--r--dhall/src/syntax/ast/visitor.rs100
-rw-r--r--dhall/src/syntax/binary/decode.rs37
-rw-r--r--dhall/src/syntax/binary/encode.rs51
-rw-r--r--dhall/src/syntax/text/parser.rs148
-rw-r--r--dhall/src/syntax/text/printer.rs192
-rw-r--r--dhall/src/tests.rs2
-rw-r--r--dhall/tests/type-inference/failure/mixedUnions.txt6
-rw-r--r--dhall/tests/type-inference/failure/recordOfKind.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/RecordMixedKinds3.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/RecordProjectionDuplicateFields.txt8
-rw-r--r--dhall/tests/type-inference/failure/unit/RecordTypeDuplicateFields.txt8
-rw-r--r--dhall/tests/type-inference/failure/unit/RecordTypeValueMember.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds2.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/RightBiasedRecordMergeMixedKinds3.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants1.txt8
-rw-r--r--dhall/tests/type-inference/failure/unit/UnionTypeDuplicateVariants2.txt8
-rw-r--r--dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds.txt6
-rw-r--r--dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds2.txt6
-rw-r--r--dhall/tests/type-inference/failure/unit/UnionTypeMixedKinds3.txt6
-rw-r--r--dhall/tests/type-inference/failure/unit/UnionTypeNotType.txt6
36 files changed, 1527 insertions, 1706 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
|