From cc03ada4e713f145f2eb1bbf0f131a4c5746cf74 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 3 Aug 2019 22:55:51 +0200
Subject: Inline headers

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

(limited to 'dhall_syntax/src/core')

diff --git a/dhall_syntax/src/core/import.rs b/dhall_syntax/src/core/import.rs
index c328e34..306460b 100644
--- a/dhall_syntax/src/core/import.rs
+++ b/dhall_syntax/src/core/import.rs
@@ -26,6 +26,7 @@ pub struct URL {
     pub authority: String,
     pub path: Vec<String>,
     pub query: Option<String>,
+    // TODO: implement inline headers
     pub headers: Option<Box<ImportHashed>>,
 }
 
-- 
cgit v1.2.3


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 ----
 dhall_syntax/src/core/visitor.rs | 4 ----
 2 files changed, 8 deletions(-)

(limited to 'dhall_syntax/src/core')

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 }`
diff --git a/dhall_syntax/src/core/visitor.rs b/dhall_syntax/src/core/visitor.rs
index 99a9c11..1745fdb 100644
--- a/dhall_syntax/src/core/visitor.rs
+++ b/dhall_syntax/src/core/visitor.rs
@@ -137,10 +137,6 @@ where
             ),
             EmptyListLit(t) => EmptyListLit(v.visit_subexpr(t)?),
             NEListLit(es) => NEListLit(vec(es, |e| v.visit_subexpr(e))?),
-            OldOptionalLit(x, t) => OldOptionalLit(
-                opt(x, |e| v.visit_subexpr(e))?,
-                v.visit_subexpr(t)?,
-            ),
             SomeLit(e) => SomeLit(v.visit_subexpr(e)?),
             RecordType(kts) => RecordType(dupmap(kts, v)?),
             RecordLit(kvs) => RecordLit(dupmap(kvs, v)?),
-- 
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 +++++++++++++++++++++++++++++++++++++++
 dhall_syntax/src/core/visitor.rs | 25 +++++++++++++++++++++++++
 2 files changed, 64 insertions(+)

(limited to 'dhall_syntax/src/core')

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> {
diff --git a/dhall_syntax/src/core/visitor.rs b/dhall_syntax/src/core/visitor.rs
index 1745fdb..b02544f 100644
--- a/dhall_syntax/src/core/visitor.rs
+++ b/dhall_syntax/src/core/visitor.rs
@@ -358,6 +358,31 @@ where
     }
 }
 
+pub struct ResolveVisitor<F1>(pub F1);
+
+impl<'a, 'b, N, E, E2, Err, F1>
+    ExprFFallibleVisitor<'a, SubExpr<N, E>, SubExpr<N, E2>, E, E2>
+    for &'b mut ResolveVisitor<F1>
+where
+    N: Clone + 'a,
+    F1: FnMut(&E) -> Result<E2, Err>,
+{
+    type Error = Err;
+
+    fn visit_subexpr(
+        &mut self,
+        subexpr: &'a SubExpr<N, E>,
+    ) -> Result<SubExpr<N, E2>, Self::Error> {
+        Ok(subexpr.rewrap(
+            subexpr
+                .as_ref()
+                .traverse_resolve_with_visitor(&mut **self)?,
+        ))
+    }
+    fn visit_embed(self, embed: &'a E) -> Result<E2, Self::Error> {
+        (self.0)(embed)
+    }
+}
 pub struct NoteAbsurdVisitor;
 
 impl<'a, 'b, N, E>
-- 
cgit v1.2.3


From 482be29e0f03e10c2469ef80bdd6ac7593207dc5 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 6 Aug 2019 20:38:06 +0200
Subject: RFC3986 URLs

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

(limited to 'dhall_syntax/src/core')

diff --git a/dhall_syntax/src/core/import.rs b/dhall_syntax/src/core/import.rs
index 306460b..d41eae2 100644
--- a/dhall_syntax/src/core/import.rs
+++ b/dhall_syntax/src/core/import.rs
@@ -41,6 +41,7 @@ pub enum Scheme {
 pub enum ImportMode {
     Code,
     RawText,
+    Location,
 }
 
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
-- 
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')

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 +-
 dhall_syntax/src/core/map.rs  | 95 +++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 97 insertions(+), 2 deletions(-)

(limited to 'dhall_syntax/src/core')

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),
 }
diff --git a/dhall_syntax/src/core/map.rs b/dhall_syntax/src/core/map.rs
index 63f19cd..6a0ebda 100644
--- a/dhall_syntax/src/core/map.rs
+++ b/dhall_syntax/src/core/map.rs
@@ -1,5 +1,6 @@
 /// A sorted map that allows multiple values for each key.
 pub use dup_tree_map::DupTreeMap;
+pub use dup_tree_set::DupTreeSet;
 
 mod one_or_more {
     use either::Either;
@@ -232,3 +233,97 @@ mod dup_tree_map {
 
     // unsafe impl<K, V> iter::TrustedLen for IntoIter<K, V> {}
 }
+
+mod dup_tree_set {
+    use super::DupTreeMap;
+    use std::iter;
+
+    #[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+    pub struct DupTreeSet<K> {
+        map: DupTreeMap<K, ()>,
+    }
+
+    pub type Iter<'a, K> = iter::Map<
+        super::dup_tree_map::Iter<'a, K, ()>,
+        for<'b> fn((&'b K, &'b ())) -> &'b K,
+    >;
+    pub type IntoIter<K> =
+        iter::Map<super::dup_tree_map::IntoIter<K, ()>, fn((K, ())) -> K>;
+
+    impl<K> DupTreeSet<K> {
+        pub fn new() -> Self
+        where
+            K: Ord,
+        {
+            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>
+        where
+            K: Ord,
+        {
+            fn foo<'a, K>((k, ()): (&'a K, &'a ())) -> &'a K {
+                k
+            }
+            self.map.iter().map(foo)
+        }
+    }
+
+    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 {
+            fn foo<K>((k, ()): (K, ())) -> K {
+                k
+            }
+            self.map.into_iter().map(foo)
+        }
+    }
+
+    impl<'a, K> IntoIterator for &'a DupTreeSet<K>
+    where
+        K: Ord,
+    {
+        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 }
+        }
+    }
+}
-- 
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 --
 dhall_syntax/src/core/visitor.rs | 3 ---
 2 files changed, 5 deletions(-)

(limited to 'dhall_syntax/src/core')

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`
diff --git a/dhall_syntax/src/core/visitor.rs b/dhall_syntax/src/core/visitor.rs
index b02544f..68ad956 100644
--- a/dhall_syntax/src/core/visitor.rs
+++ b/dhall_syntax/src/core/visitor.rs
@@ -141,9 +141,6 @@ where
             RecordType(kts) => RecordType(dupmap(kts, v)?),
             RecordLit(kvs) => RecordLit(dupmap(kvs, v)?),
             UnionType(kts) => UnionType(optdupmap(kts, v)?),
-            UnionLit(k, x, kts) => {
-                UnionLit(k.clone(), v.visit_subexpr(x)?, optdupmap(kts, v)?)
-            }
             Merge(x, y, t) => Merge(
                 v.visit_subexpr(x)?,
                 v.visit_subexpr(y)?,
-- 
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')

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 +++++-
 dhall_syntax/src/core/visitor.rs | 1 +
 2 files changed, 6 insertions(+), 1 deletion(-)

(limited to 'dhall_syntax/src/core')

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
diff --git a/dhall_syntax/src/core/visitor.rs b/dhall_syntax/src/core/visitor.rs
index 68ad956..18f76d9 100644
--- a/dhall_syntax/src/core/visitor.rs
+++ b/dhall_syntax/src/core/visitor.rs
@@ -148,6 +148,7 @@ where
             ),
             Field(e, l) => Field(v.visit_subexpr(e)?, l.clone()),
             Projection(e, ls) => Projection(v.visit_subexpr(e)?, ls.clone()),
+            Assert(e) => Assert(v.visit_subexpr(e)?),
             Embed(a) => return v.visit_embed_squash(a),
         })
     }
-- 
cgit v1.2.3