summaryrefslogtreecommitdiff
path: root/dhall_core/src
diff options
context:
space:
mode:
authorNadrieril2019-04-20 23:13:15 +0200
committerNadrieril2019-04-20 23:13:15 +0200
commitb31690a87e2963d4093210a2c58735a2095e651d (patch)
treed6bff16ce18dda443aa8b9a2fb31c31f0a502ec4 /dhall_core/src
parent9c8ba84fa5d0b392f19e9e9b8569ee2fbe96bd28 (diff)
parent83bc67d4572fe7961842f915d5559ee489e13dfd (diff)
Merge branch 'whnf'
Massive normalization rewrite, for greatly improved flexibility and performance. Closes #84
Diffstat (limited to 'dhall_core/src')
-rw-r--r--dhall_core/src/context.rs28
-rw-r--r--dhall_core/src/core.rs70
-rw-r--r--dhall_core/src/parser.rs8
-rw-r--r--dhall_core/src/printer.rs34
-rw-r--r--dhall_core/src/text.rs59
-rw-r--r--dhall_core/src/visitor.rs10
6 files changed, 130 insertions, 79 deletions
diff --git a/dhall_core/src/context.rs b/dhall_core/src/context.rs
index 877843d..55bfff5 100644
--- a/dhall_core/src/context.rs
+++ b/dhall_core/src/context.rs
@@ -32,17 +32,39 @@ impl<K: Hash + Eq + Clone, T> Context<K, T> {
/// lookup k n (insert j v c) = lookup k n c -- k /= j
/// ```
pub fn lookup<'a>(&'a self, k: &K, n: usize) -> Option<&'a T> {
- self.0.get(k).and_then(|v| v.get(v.len() - 1 - n))
+ self.0.get(k).and_then(|v| {
+ if n < v.len() {
+ v.get(v.len() - 1 - n)
+ } else {
+ None
+ }
+ })
}
- pub fn map<U, F: Fn(&T) -> U>(&self, f: F) -> Context<K, U> {
+ pub fn map<U, F: Fn(&K, &T) -> U>(&self, f: F) -> Context<K, U> {
Context(
self.0
.iter()
- .map(|(k, v)| ((*k).clone(), v.iter().map(&f).collect()))
+ .map(|(k, vs)| {
+ ((*k).clone(), vs.iter().map(|v| f(k, v)).collect())
+ })
.collect(),
)
}
+
+ pub fn lookup_all<'a>(&'a self, k: &K) -> impl Iterator<Item = &T> {
+ self.0.get(k).into_iter().flat_map(|v| v.iter())
+ }
+
+ pub fn iter<'a>(&'a self) -> impl Iterator<Item = (&K, &T)> {
+ self.0
+ .iter()
+ .flat_map(|(k, vs)| vs.iter().map(move |v| (k, v)))
+ }
+
+ pub fn iter_keys<'a>(&'a self) -> impl Iterator<Item = (&K, &Vec<T>)> {
+ self.0.iter()
+ }
}
impl<K: Hash + Eq + Clone, T: Clone> Context<K, T> {
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index aeb6f23..fa6fca4 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -1,7 +1,9 @@
#![allow(non_snake_case)]
use std::collections::BTreeMap;
+use std::collections::HashMap;
use std::rc::Rc;
+use crate::context::Context;
use crate::visitor;
use crate::*;
@@ -148,7 +150,7 @@ pub enum ExprF<SubExpr, Label, Note, Embed> {
/// `∀(x : A) -> B`
Pi(Label, SubExpr, SubExpr),
/// `f a`
- App(SubExpr, Vec<SubExpr>),
+ App(SubExpr, SubExpr),
/// `let x = r in e`
/// `let x : t = r in e`
Let(Label, Option<SubExpr>, SubExpr, SubExpr),
@@ -178,10 +180,8 @@ pub enum ExprF<SubExpr, Label, Note, Embed> {
/// `[] : Optional a`
/// `[x] : Optional a`
OldOptionalLit(Option<SubExpr>, SubExpr),
- /// `None t`
- EmptyOptionalLit(SubExpr),
/// `Some e`
- NEOptionalLit(SubExpr),
+ SomeLit(SubExpr),
/// `{ k1 : t1, k2 : t1 }`
RecordType(BTreeMap<Label, SubExpr>),
/// `{ k1 = v1, k2 = v2 }`
@@ -190,8 +190,6 @@ pub enum ExprF<SubExpr, Label, Note, Embed> {
UnionType(BTreeMap<Label, Option<SubExpr>>),
/// `< k1 = t1, k2 : t2, k3 >`
UnionLit(Label, SubExpr, BTreeMap<Label, Option<SubExpr>>),
- /// `< k1 : t1, k2 >.k1`
- UnionConstructor(Label, BTreeMap<Label, Option<SubExpr>>),
/// `merge x y : t`
Merge(SubExpr, SubExpr, Option<SubExpr>),
/// `e.x`
@@ -486,6 +484,7 @@ fn shift_var(delta: isize, var: &V<Label>, in_expr: &V<Label>) -> V<Label> {
/// capture by shifting variable indices
/// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
/// for details
+///
pub fn shift<N, E>(
delta: isize,
var: &V<Label>,
@@ -505,6 +504,41 @@ pub fn shift<N, E>(
}
}
+pub fn shift0<N, E>(
+ delta: isize,
+ label: &Label,
+ in_expr: &SubExpr<N, E>,
+) -> SubExpr<N, E> {
+ shift(delta, &V(label.clone(), 0), in_expr)
+}
+
+fn shift0_multiple<N, E>(
+ deltas: &HashMap<Label, isize>,
+ in_expr: &SubExpr<N, E>,
+) -> SubExpr<N, E> {
+ shift0_multiple_inner(&Context::new(), deltas, in_expr)
+}
+
+fn shift0_multiple_inner<N, E>(
+ ctx: &Context<Label, ()>,
+ deltas: &HashMap<Label, isize>,
+ in_expr: &SubExpr<N, E>,
+) -> SubExpr<N, E> {
+ use crate::ExprF::*;
+ match in_expr.as_ref() {
+ Var(V(y, m)) if ctx.lookup(y, *m).is_none() => {
+ let delta = deltas.get(y).unwrap_or(&0);
+ rc(Var(V(y.clone(), add_ui(*m, *delta))))
+ }
+ _ => in_expr.map_subexprs_with_special_handling_of_binders(
+ |e| shift0_multiple_inner(ctx, deltas, e),
+ |l: &Label, e| {
+ shift0_multiple_inner(&ctx.insert(l.clone(), ()), deltas, e)
+ },
+ ),
+ }
+}
+
/// Substitute all occurrences of a variable with an expression, and
/// removes the variable from the environment by shifting the indices
/// of other variables appropriately.
@@ -518,15 +552,29 @@ pub fn subst_shift<N, E>(
value: &SubExpr<N, E>,
in_expr: &SubExpr<N, E>,
) -> SubExpr<N, E> {
+ subst_shift_inner(&HashMap::new(), var, value, in_expr)
+}
+
+fn subst_shift_inner<N, E>(
+ ctx: &HashMap<Label, isize>,
+ var: &V<Label>,
+ value: &SubExpr<N, E>,
+ in_expr: &SubExpr<N, E>,
+) -> SubExpr<N, E> {
use crate::ExprF::*;
+ let V(x, n) = var;
+ let dn = ctx.get(x).unwrap_or(&0);
+ let actual_var = V(x.clone(), add_ui(*n, *dn));
match in_expr.as_ref() {
- Var(v) if v == var => SubExpr::clone(value),
- Var(v) => rc(Var(shift_var(-1, var, v))),
+ Var(v) if v == &actual_var => shift0_multiple(ctx, value),
+ Var(v) => rc(Var(shift_var(-1, &actual_var, v))),
_ => in_expr.map_subexprs_with_special_handling_of_binders(
- |e| subst_shift(var, &value, e),
+ |e| subst_shift_inner(ctx, var, value, e),
|l: &Label, e| {
- let vl = V(l.clone(), 0);
- subst_shift(&shift_var(1, &vl, var), &shift(1, &vl, value), e)
+ let mut ctx = ctx.clone();
+ let count = ctx.entry(l.clone()).or_insert(0);
+ *count += 1;
+ subst_shift_inner(&ctx, var, value, e)
},
),
}
diff --git a/dhall_core/src/parser.rs b/dhall_core/src/parser.rs
index 2a30b2b..ba15bae 100644
--- a/dhall_core/src/parser.rs
+++ b/dhall_core/src/parser.rs
@@ -176,7 +176,7 @@ macro_rules! make_parser {
[x..] => Err(
format!("Unexpected children: {:?}", x.collect::<Vec<_>>())
)?,
- ).ok_or_else(|| -> String { unreachable!() })?;
+ ).map_err(|_| -> String { unreachable!() })?;
Ok(ParsedValue::$group(res))
});
(@body,
@@ -743,10 +743,10 @@ make_parser! {
token_rule!(Some_<()>);
- rule!(application_expression<ParsedExpr<'a>> as expression; span; children!(
+ rule!(application_expression<ParsedExpr<'a>> as expression; children!(
[expression(e)] => e,
[expression(first), expression(rest)..] => {
- spanned(span, App(rc(first), rest.map(rc).collect()))
+ rest.fold(first, |acc, e| App(rc(acc), rc(e)))
},
));
@@ -754,7 +754,7 @@ make_parser! {
children!(
[expression(e)] => e,
[Some_(()), expression(e)] => {
- spanned(span, NEOptionalLit(rc(e)))
+ spanned(span, SomeLit(rc(e)))
},
[merge(()), expression(x), expression(y)] => {
spanned(span, Merge(rc(x), rc(y), None))
diff --git a/dhall_core/src/printer.rs b/dhall_core/src/printer.rs
index 4d1ae2d..c4bad71 100644
--- a/dhall_core/src/printer.rs
+++ b/dhall_core/src/printer.rs
@@ -38,10 +38,7 @@ impl<SE: Display + Clone, N, E: Display> Display for ExprF<SE, Label, N, E> {
OldOptionalLit(Some(x), t) => {
write!(f, "[{}] : Optional {}", x, t)?;
}
- EmptyOptionalLit(t) => {
- write!(f, "None {}", t)?;
- }
- NEOptionalLit(e) => {
+ SomeLit(e) => {
write!(f, "Some {}", e)?;
}
Merge(a, b, c) => {
@@ -56,12 +53,8 @@ impl<SE: Display + Clone, N, E: Display> Display for ExprF<SE, Label, N, E> {
ExprF::BinOp(op, a, b) => {
write!(f, "{} {} {}", a, op, b)?;
}
- ExprF::App(a, args) => {
- a.fmt(f)?;
- for x in args {
- f.write_str(" ")?;
- x.fmt(f)?;
- }
+ ExprF::App(a, b) => {
+ write!(f, "{} {}", a, b)?;
}
Field(a, b) => {
write!(f, "{}.{}", a, b)?;
@@ -108,16 +101,6 @@ impl<SE: Display + Clone, N, E: Display> Display for ExprF<SE, Label, N, E> {
}
f.write_str(" >")?
}
- UnionConstructor(x, map) => {
- fmt_list("< ", " | ", " >", map, f, |(k, v), f| {
- write!(f, "{}", k)?;
- if let Some(v) = v {
- write!(f, ": {}", v)?;
- }
- Ok(())
- })?;
- write!(f, ".{}", x)?
- }
Embed(a) => a.fmt(f)?,
Note(_, b) => b.fmt(f)?,
}
@@ -173,8 +156,7 @@ impl<S: Clone, A: Display + Clone> Expr<S, A> {
| EmptyListLit(_)
| NEListLit(_)
| OldOptionalLit(_, _)
- | EmptyOptionalLit(_)
- | NEOptionalLit(_)
+ | SomeLit(_)
| Merge(_, _, _)
| Annot(_, _)
if phase > Base =>
@@ -214,12 +196,8 @@ impl<S: Clone, A: Display + Clone> Expr<S, A> {
),
EmptyListLit(t) => EmptyListLit(t.phase(Import)),
OldOptionalLit(x, t) => OldOptionalLit(x, t.phase(Import)),
- EmptyOptionalLit(t) => EmptyOptionalLit(t.phase(Import)),
- NEOptionalLit(e) => NEOptionalLit(e.phase(Import)),
- ExprF::App(a, args) => ExprF::App(
- a.phase(Import),
- args.into_iter().map(|x| x.phase(Import)).collect(),
- ),
+ 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),
Projection(e, ls) => Projection(e.phase(Primitive), ls),
Note(n, b) => Note(n, b.phase(phase)),
diff --git a/dhall_core/src/text.rs b/dhall_core/src/text.rs
index 0cfbd7b..83643d9 100644
--- a/dhall_core/src/text.rs
+++ b/dhall_core/src/text.rs
@@ -1,5 +1,4 @@
use std::iter::FromIterator;
-use std::ops::Add;
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct InterpolatedText<SubExpr> {
@@ -33,6 +32,16 @@ pub enum InterpolatedTextContents<SubExpr> {
Expr(SubExpr),
}
+impl<SubExpr> InterpolatedTextContents<SubExpr> {
+ pub fn is_empty(&self) -> bool {
+ use InterpolatedTextContents::{Expr, Text};
+ match self {
+ Expr(_) => false,
+ Text(s) => s.is_empty(),
+ }
+ }
+}
+
impl<SubExpr> InterpolatedText<SubExpr> {
pub fn traverse_ref<'a, SubExpr2, E, F>(
&'a self,
@@ -51,13 +60,6 @@ impl<SubExpr> InterpolatedText<SubExpr> {
})
}
- pub fn as_ref(&self) -> InterpolatedText<&SubExpr> {
- InterpolatedText {
- head: self.head.clone(),
- tail: self.tail.iter().map(|(e, s)| (e, s.clone())).collect(),
- }
- }
-
pub fn iter<'a>(
&'a self,
) -> impl Iterator<Item = InterpolatedTextContents<SubExpr>> + 'a
@@ -65,16 +67,30 @@ impl<SubExpr> InterpolatedText<SubExpr> {
SubExpr: Clone,
{
use std::iter::once;
- once(InterpolatedTextContents::Text(self.head.clone())).chain(
- self.tail.iter().flat_map(|(e, s)| {
- once(InterpolatedTextContents::Expr(SubExpr::clone(e)))
- .chain(once(InterpolatedTextContents::Text(s.clone())))
- }),
- )
+ use InterpolatedTextContents::{Expr, Text};
+ once(Text(self.head.clone()))
+ .chain(self.tail.iter().flat_map(|(e, s)| {
+ once(Expr(SubExpr::clone(e))).chain(once(Text(s.clone())))
+ }))
+ .filter(|c| !c.is_empty())
+ }
+
+ pub fn into_iter(
+ self,
+ ) -> impl Iterator<Item = InterpolatedTextContents<SubExpr>> {
+ use std::iter::once;
+ use InterpolatedTextContents::{Expr, Text};
+ once(Text(self.head))
+ .chain(
+ self.tail
+ .into_iter()
+ .flat_map(|(e, s)| once(Expr(e)).chain(once(Text(s)))),
+ )
+ .filter(|c| !c.is_empty())
}
}
-impl<'a, SubExpr: Clone + 'a> FromIterator<InterpolatedTextContents<SubExpr>>
+impl<SubExpr> FromIterator<InterpolatedTextContents<SubExpr>>
for InterpolatedText<SubExpr>
{
fn from_iter<T>(iter: T) -> Self
@@ -82,15 +98,15 @@ impl<'a, SubExpr: Clone + 'a> FromIterator<InterpolatedTextContents<SubExpr>>
T: IntoIterator<Item = InterpolatedTextContents<SubExpr>>,
{
let mut res = InterpolatedText {
- head: "".to_owned(),
- tail: vec![],
+ head: String::new(),
+ tail: Vec::new(),
};
let mut crnt_str = &mut res.head;
for x in iter.into_iter() {
match x {
InterpolatedTextContents::Text(s) => crnt_str.push_str(&s),
InterpolatedTextContents::Expr(e) => {
- res.tail.push((e.clone(), "".to_owned()));
+ res.tail.push((e, String::new()));
crnt_str = &mut res.tail.last_mut().unwrap().1;
}
}
@@ -98,10 +114,3 @@ impl<'a, SubExpr: Clone + 'a> FromIterator<InterpolatedTextContents<SubExpr>>
res
}
}
-
-impl<SubExpr: Clone> Add for &InterpolatedText<SubExpr> {
- type Output = InterpolatedText<SubExpr>;
- fn add(self, rhs: &InterpolatedText<SubExpr>) -> Self::Output {
- self.iter().chain(rhs.iter()).collect()
- }
-}
diff --git a/dhall_core/src/visitor.rs b/dhall_core/src/visitor.rs
index 16ad418..caaefce 100644
--- a/dhall_core/src/visitor.rs
+++ b/dhall_core/src/visitor.rs
@@ -130,9 +130,7 @@ where
let (l, e) = v.visit_binder(l, e)?;
Let(l, t, a, e)
}
- App(f, args) => {
- App(v.visit_subexpr(f)?, vec(args, |e| v.visit_subexpr(e))?)
- }
+ App(f, a) => App(v.visit_subexpr(f)?, v.visit_subexpr(a)?),
Annot(x, t) => Annot(v.visit_subexpr(x)?, v.visit_subexpr(t)?),
Const(k) => Const(*k),
Builtin(v) => Builtin(*v),
@@ -155,8 +153,7 @@ where
opt(x, |e| v.visit_subexpr(e))?,
v.visit_subexpr(t)?,
),
- EmptyOptionalLit(t) => EmptyOptionalLit(v.visit_subexpr(t)?),
- NEOptionalLit(e) => NEOptionalLit(v.visit_subexpr(e)?),
+ SomeLit(e) => SomeLit(v.visit_subexpr(e)?),
RecordType(kts) => RecordType(btmap(kts, v)?),
RecordLit(kvs) => RecordLit(btmap(kvs, v)?),
UnionType(kts) => UnionType(btoptmap(kts, v)?),
@@ -165,9 +162,6 @@ where
v.visit_subexpr(x)?,
btoptmap(kts, v)?,
),
- UnionConstructor(x, kts) => {
- UnionConstructor(v.visit_label(x)?, btoptmap(kts, v)?)
- }
Merge(x, y, t) => Merge(
v.visit_subexpr(x)?,
v.visit_subexpr(y)?,