From 711164a7a24ab832006b72cac162e78cf434861a Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 4 Aug 2019 11:11:37 +0200
Subject: Remove old-style optional literals

---
 dhall_syntax/src/core/expr.rs | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'dhall_syntax/src/core/expr.rs')

diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs
index da9465d..df2dc97 100644
--- a/dhall_syntax/src/core/expr.rs
+++ b/dhall_syntax/src/core/expr.rs
@@ -194,10 +194,6 @@ pub enum ExprF<SubExpr, Embed> {
     EmptyListLit(SubExpr),
     ///  `[x, y, z]`
     NEListLit(Vec<SubExpr>),
-    /// Deprecated Optional literal form
-    ///  `[] : Optional a`
-    ///  `[x] : Optional a`
-    OldOptionalLit(Option<SubExpr>, SubExpr),
     ///  `Some e`
     SomeLit(SubExpr),
     ///  `{ k1 : t1, k2 : t1 }`
-- 
cgit v1.2.3


From 696efe66336a268054c475fab9fe6505bdfc7b60 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 4 Aug 2019 13:00:56 +0200
Subject: Add some new tests and implement import alternatives

---
 dhall_syntax/src/core/expr.rs | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

(limited to 'dhall_syntax/src/core/expr.rs')

diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs
index df2dc97..e33859b 100644
--- a/dhall_syntax/src/core/expr.rs
+++ b/dhall_syntax/src/core/expr.rs
@@ -307,6 +307,35 @@ impl<N, E> Expr<N, E> {
     {
         trivial_result(self.traverse_embed(|x| Ok(map_embed(x))))
     }
+
+    pub fn traverse_resolve<E2, Err>(
+        &self,
+        visit_embed: impl FnMut(&E) -> Result<E2, Err>,
+    ) -> Result<Expr<N, E2>, Err>
+    where
+        N: Clone,
+    {
+        self.traverse_resolve_with_visitor(&mut visitor::ResolveVisitor(
+            visit_embed,
+        ))
+    }
+
+    pub(crate) fn traverse_resolve_with_visitor<E2, Err, F1>(
+        &self,
+        visitor: &mut visitor::ResolveVisitor<F1>,
+    ) -> Result<Expr<N, E2>, Err>
+    where
+        N: Clone,
+        F1: FnMut(&E) -> Result<E2, Err>,
+    {
+        match self {
+            ExprF::BinOp(BinOp::ImportAlt, l, r) => l
+                .as_ref()
+                .traverse_resolve_with_visitor(visitor)
+                .or(r.as_ref().traverse_resolve_with_visitor(visitor)),
+            _ => self.visit(visitor),
+        }
+    }
 }
 
 impl Expr<X, X> {
@@ -383,6 +412,16 @@ impl<N, E> SubExpr<N, E> {
             )),
         }
     }
+
+    pub fn traverse_resolve<E2, Err>(
+        &self,
+        visit_embed: impl FnMut(&E) -> Result<E2, Err>,
+    ) -> Result<SubExpr<N, E2>, Err>
+    where
+        N: Clone,
+    {
+        Ok(self.rewrap(self.as_ref().traverse_resolve(visit_embed)?))
+    }
 }
 
 impl SubExpr<X, X> {
-- 
cgit v1.2.3


From f7b0c6b9c52f65624dc765fb9eaa7d0d94eeae76 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 6 Aug 2019 23:03:01 +0200
Subject: Generalize empty list annotations

---
 dhall_syntax/src/core/expr.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dhall_syntax/src/core/expr.rs')

diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs
index e33859b..14dc165 100644
--- a/dhall_syntax/src/core/expr.rs
+++ b/dhall_syntax/src/core/expr.rs
@@ -190,7 +190,7 @@ pub enum ExprF<SubExpr, Embed> {
     DoubleLit(Double),
     ///  `"Some ${interpolated} text"`
     TextLit(InterpolatedText<SubExpr>),
-    ///  `[] : List t`
+    ///  `[] : t`
     EmptyListLit(SubExpr),
     ///  `[x, y, z]`
     NEListLit(Vec<SubExpr>),
-- 
cgit v1.2.3


From 2755cb01092363062016bc51349870b1330d1d6f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 7 Aug 2019 15:58:57 +0200
Subject: Sort labels in projection expressions

---
 dhall_syntax/src/core/expr.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dhall_syntax/src/core/expr.rs')

diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs
index 14dc165..668ab45 100644
--- a/dhall_syntax/src/core/expr.rs
+++ b/dhall_syntax/src/core/expr.rs
@@ -1,6 +1,6 @@
 use std::rc::Rc;
 
-use crate::map::DupTreeMap;
+use crate::map::{DupTreeMap, DupTreeSet};
 use crate::visitor;
 use crate::*;
 
@@ -209,7 +209,7 @@ pub enum ExprF<SubExpr, Embed> {
     ///  `e.x`
     Field(SubExpr, Label),
     ///  `e.{ x, y, z }`
-    Projection(SubExpr, Vec<Label>),
+    Projection(SubExpr, DupTreeSet<Label>),
     /// Embeds an import or the result of resolving the import
     Embed(Embed),
 }
-- 
cgit v1.2.3


From d248762095908246951b6aa6c211587c6e333c0e Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 7 Aug 2019 21:05:01 +0200
Subject: Remove union literals from the language

---
 dhall_syntax/src/core/expr.rs | 2 --
 1 file changed, 2 deletions(-)

(limited to 'dhall_syntax/src/core/expr.rs')

diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs
index 668ab45..aab4b6a 100644
--- a/dhall_syntax/src/core/expr.rs
+++ b/dhall_syntax/src/core/expr.rs
@@ -202,8 +202,6 @@ pub enum ExprF<SubExpr, Embed> {
     RecordLit(DupTreeMap<Label, SubExpr>),
     ///  `< k1 : t1, k2 >`
     UnionType(DupTreeMap<Label, Option<SubExpr>>),
-    ///  `< k1 = t1, k2 : t2, k3 >`
-    UnionLit(Label, SubExpr, DupTreeMap<Label, Option<SubExpr>>),
     ///  `merge x y : t`
     Merge(SubExpr, SubExpr, Option<SubExpr>),
     ///  `e.x`
-- 
cgit v1.2.3


From 51c4f79fe092191d670ffa2f9098693079dbc1be Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 7 Aug 2019 21:18:11 +0200
Subject: Add truncated Natural subtraction

---
 dhall_syntax/src/core/expr.rs | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dhall_syntax/src/core/expr.rs')

diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs
index aab4b6a..b293357 100644
--- a/dhall_syntax/src/core/expr.rs
+++ b/dhall_syntax/src/core/expr.rs
@@ -119,6 +119,7 @@ pub enum Builtin {
     NaturalOdd,
     NaturalToInteger,
     NaturalShow,
+    NaturalSubtract,
     IntegerToDouble,
     IntegerShow,
     DoubleShow,
-- 
cgit v1.2.3


From 071ba528cd8c6a222be345ddec7560bb45cca6be Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 8 Aug 2019 19:33:07 +0200
Subject: Add support for dependent types

---
 dhall_syntax/src/core/expr.rs | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'dhall_syntax/src/core/expr.rs')

diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs
index b293357..6522cb1 100644
--- a/dhall_syntax/src/core/expr.rs
+++ b/dhall_syntax/src/core/expr.rs
@@ -44,7 +44,7 @@ impl From<NaiveDouble> for f64 {
 }
 
 /// Constants for a pure type system
-#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)]
 pub enum Const {
     Type,
     Kind,
@@ -99,6 +99,8 @@ pub enum BinOp {
     BoolEQ,
     /// `x != y`
     BoolNE,
+    /// x === y
+    Equivalence,
 }
 
 /// Built-ins
@@ -175,6 +177,8 @@ pub enum ExprF<SubExpr, Embed> {
     Let(Label, Option<SubExpr>, SubExpr, SubExpr),
     ///  `x : t`
     Annot(SubExpr, SubExpr),
+    ///  `assert : t`
+    Assert(SubExpr),
     /// Built-in values
     Builtin(Builtin),
     // Binary operations
-- 
cgit v1.2.3