diff options
author | Nadrieril | 2019-04-20 23:13:15 +0200 |
---|---|---|
committer | Nadrieril | 2019-04-20 23:13:15 +0200 |
commit | b31690a87e2963d4093210a2c58735a2095e651d (patch) | |
tree | d6bff16ce18dda443aa8b9a2fb31c31f0a502ec4 /dhall_core | |
parent | 9c8ba84fa5d0b392f19e9e9b8569ee2fbe96bd28 (diff) | |
parent | 83bc67d4572fe7961842f915d5559ee489e13dfd (diff) |
Merge branch 'whnf'
Massive normalization rewrite, for greatly improved flexibility
and performance.
Closes #84
Diffstat (limited to '')
-rw-r--r-- | dhall_core/Cargo.toml | 2 | ||||
-rw-r--r-- | dhall_core/src/context.rs | 28 | ||||
-rw-r--r-- | dhall_core/src/core.rs | 70 | ||||
-rw-r--r-- | dhall_core/src/parser.rs | 8 | ||||
-rw-r--r-- | dhall_core/src/printer.rs | 34 | ||||
-rw-r--r-- | dhall_core/src/text.rs | 59 | ||||
-rw-r--r-- | dhall_core/src/visitor.rs | 10 |
7 files changed, 131 insertions, 80 deletions
diff --git a/dhall_core/Cargo.toml b/dhall_core/Cargo.toml index a2aced0..80cf721 100644 --- a/dhall_core/Cargo.toml +++ b/dhall_core/Cargo.toml @@ -12,4 +12,4 @@ doctest = false itertools = "0.8.0" pest = "2.1" dhall_generated_parser = { path = "../dhall_generated_parser" } -improved_slice_patterns = { version = "1.0.1", path = "../improved_slice_patterns" } +improved_slice_patterns = { version = "2.0.0", path = "../improved_slice_patterns" } 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)?, |