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')

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 ----
 dhall_syntax/src/parser.rs       | 18 +++---------------
 dhall_syntax/src/printer.rs      |  8 --------
 4 files changed, 3 insertions(+), 31 deletions(-)

(limited to 'dhall_syntax')

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)?),
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 9d9a374..db1699b 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -724,6 +724,9 @@ make_parser! {
         [merge(()), expression(x), expression(y), expression(z)] => {
             spanned(span, Merge(x, y, Some(z)))
         },
+        [List(()), expression(x)] => {
+            spanned(span, EmptyListLit(x))
+        },
         [expression(e)] => e,
     ));
 
@@ -738,21 +741,6 @@ make_parser! {
     token_rule!(List<()>);
     token_rule!(Optional<()>);
 
-    rule!(empty_collection<ParsedSubExpr> as expression; span; children!(
-        [List(_), expression(t)] => {
-            spanned(span, EmptyListLit(t))
-        },
-        [Optional(_), expression(t)] => {
-            spanned(span, OldOptionalLit(None, t))
-        },
-    ));
-
-    rule!(non_empty_optional<ParsedSubExpr> as expression; span; children!(
-        [expression(x), Optional(_), expression(t)] => {
-            spanned(span, OldOptionalLit(Some(x), t))
-        }
-    ));
-
     rule!(import_alt_expression<ParsedSubExpr> as expression; children!(
         [expression(e)] => e,
         [expression(first), expression(rest)..] => {
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index dbed55d..b585a5b 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -32,12 +32,6 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, E> {
             NEListLit(es) => {
                 fmt_list("[", ", ", "]", es, f, Display::fmt)?;
             }
-            OldOptionalLit(None, t) => {
-                write!(f, "[] : Optional {}", t)?;
-            }
-            OldOptionalLit(Some(x), t) => {
-                write!(f, "[{}] : Optional {}", x, t)?;
-            }
             SomeLit(e) => {
                 write!(f, "Some {}", e)?;
             }
@@ -154,7 +148,6 @@ impl<S: Clone, A: Display + Clone> Expr<S, A> {
             | Let(_, _, _, _)
             | EmptyListLit(_)
             | NEListLit(_)
-            | OldOptionalLit(_, _)
             | SomeLit(_)
             | Merge(_, _, _)
             | Annot(_, _)
@@ -190,7 +183,6 @@ impl<S: Clone, A: Display + Clone> Expr<S, A> {
                 b.phase(PrintPhase::BinOp(op)),
             ),
             EmptyListLit(t) => EmptyListLit(t.phase(Import)),
-            OldOptionalLit(x, t) => OldOptionalLit(x, t.phase(Import)),
             SomeLit(e) => SomeLit(e.phase(Import)),
             ExprF::App(f, a) => ExprF::App(f.phase(Import), a.phase(Import)),
             Field(a, b) => Field(a.phase(Primitive), b),
-- 
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')

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 e52f50080d8e0e6d6a05b1045e3e0e840acb50d0 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 4 Aug 2019 14:07:34 +0200
Subject: Braced escape sequences

---
 dhall_syntax/src/parser.rs | 28 ++++++++++++++++++++++++----
 1 file changed, 24 insertions(+), 4 deletions(-)

(limited to 'dhall_syntax')

diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index db1699b..2450c76 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -402,11 +402,31 @@ make_parser! {
                 "n" => "\n".to_owned(),
                 "r" => "\r".to_owned(),
                 "t" => "\t".to_owned(),
+                // "uXXXX" or "u{XXXXX}"
                 _ => {
-                    // "uXXXX"
-                    use std::convert::TryFrom;
-                    let c = u16::from_str_radix(&s[1..5], 16).unwrap();
-                    let c = char::try_from(u32::from(c)).unwrap();
+                    use std::convert::{TryFrom, TryInto};
+
+                    let s = &s[1..];
+                    let s = if &s[0..1] == "{" {
+                        &s[1..s.len()-1]
+                    } else {
+                        &s[0..s.len()]
+                    };
+
+                    if s.len() > 8 {
+                        Err(format!("Escape sequences can't have more than 8 chars: \"{}\"", s))?
+                    }
+
+                    // pad with zeroes
+                    let s: String = std::iter::repeat('0')
+                        .take(8 - s.len())
+                        .chain(s.chars())
+                        .collect();
+
+                    // `s` has length 8, so `bytes` has length 4
+                    let bytes: &[u8] = &hex::decode(s).unwrap();
+                    let c = u32::from_be_bytes(bytes.try_into().unwrap());
+                    let c = char::try_from(c).unwrap();
                     std::iter::once(c).collect()
                 }
             }
-- 
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 +
 dhall_syntax/src/parser.rs      | 7 +++++++
 dhall_syntax/src/printer.rs     | 1 +
 3 files changed, 9 insertions(+)

(limited to 'dhall_syntax')

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)]
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 2450c76..2c0cee9 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -697,6 +697,7 @@ make_parser! {
     ));
 
     token_rule!(Text<()>);
+    token_rule!(Location<()>);
 
     rule!(import<ParsedSubExpr> as expression; span; children!(
         [import_hashed(location_hashed)] => {
@@ -711,6 +712,12 @@ make_parser! {
                 location_hashed
             }))
         },
+        [import_hashed(location_hashed), Location(_)] => {
+            spanned(span, Embed(Import {
+                mode: ImportMode::Location,
+                location_hashed
+            }))
+        },
     ));
 
     token_rule!(lambda<()>);
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index b585a5b..2b2bbcc 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -435,6 +435,7 @@ impl Display for Import {
         match self.mode {
             Code => {}
             RawText => write!(f, " as Text")?,
+            Location => write!(f, " as Location")?,
         }
         Ok(())
     }
-- 
cgit v1.2.3


From 3e157f0a05b0b93753ed377332597a37fa379541 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 6 Aug 2019 21:28:12 +0200
Subject: Add toMap keyword

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

(limited to 'dhall_syntax')

diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 2c0cee9..8355ebf 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -861,6 +861,7 @@ make_parser! {
     ));
 
     token_rule!(Some_<()>);
+    token_rule!(toMap<()>);
 
     rule!(application_expression<ParsedSubExpr> as expression; children!(
         [expression(e)] => e,
-- 
cgit v1.2.3


From 705433487da3cd3b4517fcf74b0497c76dbb4080 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 6 Aug 2019 22:36:43 +0200
Subject: Prepare for https://github.com/dhall-lang/dhall-lang/pull/630

---
 dhall_syntax/src/parser.rs  | 3 ++-
 dhall_syntax/src/printer.rs | 3 +--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'dhall_syntax')

diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 8355ebf..0832af3 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -752,7 +752,8 @@ make_parser! {
             spanned(span, Merge(x, y, Some(z)))
         },
         [List(()), expression(x)] => {
-            spanned(span, EmptyListLit(x))
+            let list = unspanned(Builtin(crate::Builtin::List));
+            spanned(span, EmptyListLit(unspanned(App(list, x))))
         },
         [expression(e)] => e,
     ));
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index 2b2bbcc..52d3d81 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -27,7 +27,7 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, E> {
                 write!(f, " = {} in {}", c, d)?;
             }
             EmptyListLit(t) => {
-                write!(f, "[] : List {}", t)?;
+                write!(f, "[] : {}", t)?;
             }
             NEListLit(es) => {
                 fmt_list("[", ", ", "]", es, f, Display::fmt)?;
@@ -182,7 +182,6 @@ impl<S: Clone, A: Display + Clone> Expr<S, A> {
                 a.phase(PrintPhase::BinOp(op)),
                 b.phase(PrintPhase::BinOp(op)),
             ),
-            EmptyListLit(t) => EmptyListLit(t.phase(Import)),
             SomeLit(e) => SomeLit(e.phase(Import)),
             ExprF::App(f, a) => ExprF::App(f.phase(Import), a.phase(Import)),
             Field(a, b) => Field(a.phase(Primitive), b),
-- 
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 +-
 dhall_syntax/src/parser.rs    | 10 ++++++----
 2 files changed, 7 insertions(+), 5 deletions(-)

(limited to 'dhall_syntax')

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>),
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 0832af3..8a84b00 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -727,6 +727,12 @@ make_parser! {
     token_rule!(if_<()>);
     token_rule!(in_<()>);
 
+    rule!(empty_list_literal<ParsedSubExpr> as expression; span; children!(
+        [expression(e)] => {
+            spanned(span, EmptyListLit(e))
+        },
+    ));
+
     rule!(expression<ParsedSubExpr> as expression; span; children!(
         [lambda(()), label(l), expression(typ),
                 arrow(()), expression(body)] => {
@@ -751,10 +757,6 @@ make_parser! {
         [merge(()), expression(x), expression(y), expression(z)] => {
             spanned(span, Merge(x, y, Some(z)))
         },
-        [List(()), expression(x)] => {
-            let list = unspanned(Builtin(crate::Builtin::List));
-            spanned(span, EmptyListLit(unspanned(App(list, x))))
-        },
         [expression(e)] => e,
     ));
 
-- 
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 +++++++++++++++++++++++++++++++++++++++++++
 dhall_syntax/src/parser.rs    |  6 +--
 3 files changed, 100 insertions(+), 5 deletions(-)

(limited to 'dhall_syntax')

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 }
+        }
+    }
+}
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 8a84b00..5be8477 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -6,7 +6,7 @@ use std::rc::Rc;
 
 use dhall_generated_parser::{DhallParser, Rule};
 
-use crate::map::DupTreeMap;
+use crate::map::{DupTreeMap, DupTreeSet};
 use crate::ExprF::*;
 use crate::*;
 
@@ -894,13 +894,13 @@ make_parser! {
         }
     ));
 
-    rule!(selector<Either<Label, Vec<Label>>>; children!(
+    rule!(selector<Either<Label, DupTreeSet<Label>>>; children!(
         [label(l)] => Either::Left(l),
         [labels(ls)] => Either::Right(ls),
         [expression(e)] => unimplemented!("selection by expression"), // TODO
     ));
 
-    rule!(labels<Vec<Label>>; children!(
+    rule!(labels<DupTreeSet<Label>>; children!(
         [label(ls)..] => ls.collect(),
     ));
 
-- 
cgit v1.2.3


From d5c3e8f2ef7438b7ac84be34cfe019ce365ae529 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 7 Aug 2019 16:22:00 +0200
Subject: Forbid surrogate pairs and non-characters

---
 dhall_syntax/src/parser.rs | 23 +++++++++++++++++++++--
 1 file changed, 21 insertions(+), 2 deletions(-)

(limited to 'dhall_syntax')

diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 5be8477..8336c74 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -425,8 +425,27 @@ make_parser! {
 
                     // `s` has length 8, so `bytes` has length 4
                     let bytes: &[u8] = &hex::decode(s).unwrap();
-                    let c = u32::from_be_bytes(bytes.try_into().unwrap());
-                    let c = char::try_from(c).unwrap();
+                    let i = u32::from_be_bytes(bytes.try_into().unwrap());
+                    let c = char::try_from(i).unwrap();
+                    match i {
+                        0xD800..=0xDFFF => {
+                            let c_ecapsed = c.escape_unicode();
+                            Err(format!("Escape sequences can't contain surrogate pairs: \"{}\"", c_ecapsed))?
+                        },
+                        0x0FFFE..=0x0FFFF | 0x1FFFE..=0x1FFFF |
+                        0x2FFFE..=0x2FFFF | 0x3FFFE..=0x3FFFF |
+                        0x4FFFE..=0x4FFFF | 0x5FFFE..=0x5FFFF |
+                        0x6FFFE..=0x6FFFF | 0x7FFFE..=0x7FFFF |
+                        0x8FFFE..=0x8FFFF | 0x9FFFE..=0x9FFFF |
+                        0xAFFFE..=0xAFFFF | 0xBFFFE..=0xBFFFF |
+                        0xCFFFE..=0xCFFFF | 0xDFFFE..=0xDFFFF |
+                        0xEFFFE..=0xEFFFF | 0xFFFFE..=0xFFFFF |
+                        0x10FFFE..=0x10FFFF => {
+                            let c_ecapsed = c.escape_unicode();
+                            Err(format!("Escape sequences can't contain non-characters: \"{}\"", c_ecapsed))?
+                        },
+                        _ => {}
+                    }
                     std::iter::once(c).collect()
                 }
             }
-- 
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 ---
 dhall_syntax/src/parser.rs       | 51 +++-------------------------------------
 dhall_syntax/src/printer.rs      | 10 --------
 4 files changed, 3 insertions(+), 63 deletions(-)

(limited to 'dhall_syntax')

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)?,
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 8336c74..a7f419a 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -976,67 +976,22 @@ make_parser! {
         [label(name), expression(expr)] => (name, expr)
     ));
 
-    rule!(union_type_or_literal<ParsedSubExpr> as expression; span; children!(
+    rule!(union_type<ParsedSubExpr> as expression; span; children!(
         [empty_union_type(_)] => {
             spanned(span, UnionType(Default::default()))
         },
-        [non_empty_union_type_or_literal((Some((l, e)), entries))] => {
-            spanned(span, UnionLit(l, e, entries))
-        },
-        [non_empty_union_type_or_literal((None, entries))] => {
-            spanned(span, UnionType(entries))
+        [union_type_entry(entries)..] => {
+            spanned(span, UnionType(entries.collect()))
         },
     ));
 
     token_rule!(empty_union_type<()>);
 
-    rule!(non_empty_union_type_or_literal
-          <(Option<(Label, ParsedSubExpr)>,
-            DupTreeMap<Label, Option<ParsedSubExpr>>)>;
-            children!(
-        [label(l), union_literal_variant_value((e, entries))] => {
-            (Some((l, e)), entries)
-        },
-        [label(l), union_type_or_literal_variant_type((e, rest))] => {
-            let (x, mut entries) = rest;
-            entries.insert(l, e);
-            (x, entries)
-        },
-    ));
-
-    rule!(union_literal_variant_value
-          <(ParsedSubExpr, DupTreeMap<Label, Option<ParsedSubExpr>>)>;
-            children!(
-        [expression(e), union_type_entry(entries)..] => {
-            (e, entries.collect())
-        },
-    ));
-
     rule!(union_type_entry<(Label, Option<ParsedSubExpr>)>; children!(
         [label(name), expression(expr)] => (name, Some(expr)),
         [label(name)] => (name, None),
     ));
 
-    // TODO: unary union variants
-    rule!(union_type_or_literal_variant_type
-          <(Option<ParsedSubExpr>,
-            (Option<(Label, ParsedSubExpr)>,
-             DupTreeMap<Label, Option<ParsedSubExpr>>))>;
-                children!(
-        [expression(e), non_empty_union_type_or_literal(rest)] => {
-            (Some(e), rest)
-        },
-        [expression(e)] => {
-            (Some(e), (None, Default::default()))
-        },
-        [non_empty_union_type_or_literal(rest)] => {
-            (None, rest)
-        },
-        [] => {
-            (None, (None, Default::default()))
-        },
-    ));
-
     rule!(non_empty_list_literal<ParsedSubExpr> as expression; span;
           children!(
         [expression(items)..] => spanned(
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index 52d3d81..db688bd 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -85,16 +85,6 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, E> {
                 }
                 Ok(())
             })?,
-            UnionLit(a, b, c) => {
-                write!(f, "< {} = {}", a, b)?;
-                for (k, v) in c {
-                    write!(f, " | {}", k)?;
-                    if let Some(v) = v {
-                        write!(f, ": {}", v)?;
-                    }
-                }
-                f.write_str(" >")?
-            }
             Embed(a) => a.fmt(f)?,
         }
         Ok(())
-- 
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 +
 dhall_syntax/src/parser.rs    | 1 +
 dhall_syntax/src/printer.rs   | 1 +
 3 files changed, 3 insertions(+)

(limited to 'dhall_syntax')

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,
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index a7f419a..72dfcdd 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -80,6 +80,7 @@ impl crate::Builtin {
             "Natural/odd" => Some(NaturalOdd),
             "Natural/toInteger" => Some(NaturalToInteger),
             "Natural/show" => Some(NaturalShow),
+            "Natural/subtract" => Some(NaturalSubtract),
             "Integer/toDouble" => Some(IntegerToDouble),
             "Integer/show" => Some(IntegerShow),
             "Double/show" => Some(DoubleShow),
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index db688bd..1d6c113 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -449,6 +449,7 @@ impl Display for Builtin {
             NaturalOdd => "Natural/odd",
             NaturalToInteger => "Natural/toInteger",
             NaturalShow => "Natural/show",
+            NaturalSubtract => "Natural/subtract",
             IntegerToDouble => "Integer/toDouble",
             IntegerShow => "Integer/show",
             DoubleShow => "Double/show",
-- 
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 +
 dhall_syntax/src/parser.rs       | 12 ++++++++++++
 dhall_syntax/src/printer.rs      |  4 ++++
 4 files changed, 22 insertions(+), 1 deletion(-)

(limited to 'dhall_syntax')

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),
         })
     }
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 72dfcdd..9ae6dc8 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -311,6 +311,7 @@ fn can_be_shortcutted(rule: Rule) -> bool {
         | times_expression
         | equal_expression
         | not_equal_expression
+        | equivalent_expression
         | application_expression
         | first_application_expression
         | selector_expression
@@ -744,6 +745,7 @@ make_parser! {
     token_rule!(forall<()>);
     token_rule!(arrow<()>);
     token_rule!(merge<()>);
+    token_rule!(assert<()>);
     token_rule!(if_<()>);
     token_rule!(in_<()>);
 
@@ -777,6 +779,9 @@ make_parser! {
         [merge(()), expression(x), expression(y), expression(z)] => {
             spanned(span, Merge(x, y, Some(z)))
         },
+        [assert(()), expression(x)] => {
+            spanned(span, Assert(x))
+        },
         [expression(e)] => e,
     ));
 
@@ -875,6 +880,13 @@ make_parser! {
             rest.fold(first, |acc, e| unspanned(BinOp(o, acc, e)))
         },
     ));
+    rule!(equivalent_expression<ParsedSubExpr> as expression; children!(
+        [expression(e)] => e,
+        [expression(first), expression(rest)..] => {
+            let o = crate::BinOp::Equivalence;
+            rest.fold(first, |acc, e| unspanned(BinOp(o, acc, e)))
+        },
+    ));
 
     rule!(annotated_expression<ParsedSubExpr> as expression; span; children!(
         [expression(e)] => e,
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index 1d6c113..70b224e 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -44,6 +44,9 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, E> {
             Annot(a, b) => {
                 write!(f, "{} : {}", a, b)?;
             }
+            Assert(a) => {
+                write!(f, "assert : {}", a)?;
+            }
             ExprF::BinOp(op, a, b) => {
                 write!(f, "{} {} {}", a, op, b)?;
             }
@@ -286,6 +289,7 @@ impl Display for BinOp {
             ImportAlt => "?",
             RightBiasedRecordMerge => "⫽",
             ListAppend => "#",
+            Equivalence => "≡",
         })
     }
 }
-- 
cgit v1.2.3