From 396ec334bac1e8d10a2d2b2d683c93e3b2ff4d8d Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 6 Apr 2019 20:04:04 +0200
Subject: Massage import loading into new API

Closes #9
---
 dhall_core/src/core.rs | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

(limited to 'dhall_core/src')

diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index a56c5a3..d832cd5 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -285,6 +285,28 @@ impl<S, A> Expr<S, A> {
         self.map_shallow(recurse, |x| x.clone(), map_embed, |x| x.clone())
     }
 
+    #[inline(always)]
+    pub fn traverse_embed<B, Err, F>(
+        &self,
+        map_embed: &F,
+    ) -> Result<Expr<S, B>, Err>
+    where
+        S: Clone,
+        B: Clone,
+        F: Fn(&A) -> Result<B, Err>,
+    {
+        let recurse = |e: &SubExpr<S, A>| -> Result<SubExpr<S, B>, Err> {
+            Ok(e.as_ref().traverse_embed(map_embed)?.roll())
+        };
+        self.as_ref().traverse(
+            |e| recurse(e),
+            |_, e| recurse(e),
+            |x| Ok(S::clone(x)),
+            map_embed,
+            |x| Ok(Label::clone(x)),
+        )
+    }
+
     pub fn map_label<F>(&self, map_label: &F) -> Self
     where
         A: Clone,
@@ -319,6 +341,23 @@ impl<S: Clone, A: Clone> Expr<S, Expr<S, A>> {
     }
 }
 
+impl<S: Clone, A: Clone> Expr<S, SubExpr<S, A>> {
+    pub fn squash_embed(&self) -> SubExpr<S, A> {
+        match self.as_ref() {
+            ExprF::Embed(e) => e.clone(),
+            e => e
+                .map(
+                    |e| e.as_ref().squash_embed(),
+                    |_, e| e.as_ref().squash_embed(),
+                    S::clone,
+                    |_| unreachable!(),
+                    Label::clone,
+                )
+                .roll(),
+        }
+    }
+}
+
 impl<SE, L, N, E> ExprF<SE, L, N, E> {
     #[inline(always)]
     pub fn as_ref(&self) -> ExprF<&SE, &L, &N, &E>
-- 
cgit v1.2.3


From f93aee4dcf71c85b826244b3b57949ffbdb820c4 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 6 Apr 2019 22:37:39 +0200
Subject: Add Sort type universe

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

(limited to 'dhall_core/src')

diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index d832cd5..89506ec 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -68,6 +68,7 @@ impl From<NaiveDouble> for f64 {
 pub enum Const {
     Type,
     Kind,
+    Sort,
 }
 
 /// Bound variable
-- 
cgit v1.2.3


From c461548c32f8cb3ee2db5ade88ae4f91b3838ab5 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 7 Apr 2019 11:09:57 +0200
Subject: Avoid constructing exprs manually when possible

---
 dhall_core/src/parser.rs | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dhall_core/src')

diff --git a/dhall_core/src/parser.rs b/dhall_core/src/parser.rs
index 67bcf77..41a2ce7 100644
--- a/dhall_core/src/parser.rs
+++ b/dhall_core/src/parser.rs
@@ -764,6 +764,7 @@ make_parser! {
                     "False" => BoolLit(false),
                     "Type" => Const(crate::Const::Type),
                     "Kind" => Const(crate::Const::Kind),
+                    "Sort" => Const(crate::Const::Sort),
                     _ => Var(V(l, idx)),
                 }
             }
@@ -777,6 +778,7 @@ make_parser! {
                     "False" => BoolLit(false),
                     "Type" => Const(crate::Const::Type),
                     "Kind" => Const(crate::Const::Kind),
+                    "Sort" => Const(crate::Const::Sort),
                     _ => Var(V(l, 0)),
                 }
             }
-- 
cgit v1.2.3