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') 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 Expr { self.map_shallow(recurse, |x| x.clone(), map_embed, |x| x.clone()) } + #[inline(always)] + pub fn traverse_embed( + &self, + map_embed: &F, + ) -> Result, Err> + where + S: Clone, + B: Clone, + F: Fn(&A) -> Result, + { + let recurse = |e: &SubExpr| -> Result, 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(&self, map_label: &F) -> Self where A: Clone, @@ -319,6 +341,23 @@ impl Expr> { } } +impl Expr> { + pub fn squash_embed(&self) -> SubExpr { + 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 ExprF { #[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') 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 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') 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