diff options
Diffstat (limited to 'dhall_core/src/core.rs')
-rw-r--r-- | dhall_core/src/core.rs | 502 |
1 files changed, 337 insertions, 165 deletions
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs index afa3d3f..3d1b9f3 100644 --- a/dhall_core/src/core.rs +++ b/dhall_core/src/core.rs @@ -100,7 +100,7 @@ pub enum Const { /// appear as a numeric suffix. /// #[derive(Debug, Clone, PartialEq, Eq)] -pub struct V(pub Label, pub usize); +pub struct V<Label>(pub Label, pub usize); // Definition order must match precedence order for // pretty-printing to work correctly @@ -170,45 +170,42 @@ pub type ParsedExpr = SubExpr<X, Import>; pub type ResolvedExpr = SubExpr<X, X>; pub type DhallExpr = ResolvedExpr; -pub type SubExpr<Note, Embed> = Rc<Expr<Note, Embed>>; +#[derive(Debug, PartialEq, Eq)] +pub struct SubExpr<Note, Embed>(pub Rc<Expr<Note, Embed>>); + +pub type Expr<Note, Embed> = ExprF<SubExpr<Note, Embed>, Label, Note, Embed>; /// Syntax tree for expressions +// Having the recursion out of the enum definition enables writing +// much more generic code and improves pattern-matching behind +// smart pointers. #[derive(Debug, Clone, PartialEq, Eq)] -pub enum Expr<Note, Embed> { +pub enum ExprF<SubExpr, Label, Note, Embed> { /// `Const c ~ c` Const(Const), /// `Var (V x 0) ~ x`<br> /// `Var (V x n) ~ x@n` - Var(V), + Var(V<Label>), /// `Lam x A b ~ λ(x : A) -> b` - Lam(Label, SubExpr<Note, Embed>, SubExpr<Note, Embed>), + Lam(Label, SubExpr, SubExpr), /// `Pi "_" A B ~ A -> B` /// `Pi x A B ~ ∀(x : A) -> B` - Pi(Label, SubExpr<Note, Embed>, SubExpr<Note, Embed>), + Pi(Label, SubExpr, SubExpr), /// `App f A ~ f A` - App(SubExpr<Note, Embed>, Vec<SubExpr<Note, Embed>>), + App(SubExpr, Vec<SubExpr>), /// `Let x Nothing r e ~ let x = r in e` /// `Let x (Just t) r e ~ let x : t = r in e` - Let( - Label, - Option<SubExpr<Note, Embed>>, - SubExpr<Note, Embed>, - SubExpr<Note, Embed>, - ), + Let(Label, Option<SubExpr>, SubExpr, SubExpr), /// `Annot x t ~ x : t` - Annot(SubExpr<Note, Embed>, SubExpr<Note, Embed>), + Annot(SubExpr, SubExpr), /// Built-in values Builtin(Builtin), // Binary operations - BinOp(BinOp, SubExpr<Note, Embed>, SubExpr<Note, Embed>), + BinOp(BinOp, SubExpr, SubExpr), /// `BoolLit b ~ b` BoolLit(bool), /// `BoolIf x y z ~ if x then y else z` - BoolIf( - SubExpr<Note, Embed>, - SubExpr<Note, Embed>, - SubExpr<Note, Embed>, - ), + BoolIf(SubExpr, SubExpr, SubExpr), /// `NaturalLit n ~ +n` NaturalLit(Natural), /// `IntegerLit n ~ n` @@ -216,39 +213,31 @@ pub enum Expr<Note, Embed> { /// `DoubleLit n ~ n` DoubleLit(Double), /// `TextLit t ~ t` - TextLit(InterpolatedText<Note, Embed>), + TextLit(InterpolatedText<SubExpr>), /// [] : List t` - EmptyListLit(SubExpr<Note, Embed>), + EmptyListLit(SubExpr), /// [x, y, z] - NEListLit(Vec<SubExpr<Note, Embed>>), + NEListLit(Vec<SubExpr>), /// None t - EmptyOptionalLit(SubExpr<Note, Embed>), + EmptyOptionalLit(SubExpr), /// Some e - NEOptionalLit(SubExpr<Note, Embed>), + NEOptionalLit(SubExpr), /// `Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }` - RecordType(BTreeMap<Label, SubExpr<Note, Embed>>), + RecordType(BTreeMap<Label, SubExpr>), /// `RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }` - RecordLit(BTreeMap<Label, SubExpr<Note, Embed>>), + RecordLit(BTreeMap<Label, SubExpr>), /// `Union [(k1, t1), (k2, t2)] ~ < k1 : t1, k2 : t2 >` - UnionType(BTreeMap<Label, SubExpr<Note, Embed>>), + UnionType(BTreeMap<Label, SubExpr>), /// `UnionLit (k1, v1) [(k2, t2), (k3, t3)] ~ < k1 = t1, k2 : t2, k3 : t3 >` - UnionLit( - Label, - SubExpr<Note, Embed>, - BTreeMap<Label, SubExpr<Note, Embed>>, - ), + UnionLit(Label, SubExpr, BTreeMap<Label, SubExpr>), /// `Merge x y t ~ merge x y : t` - Merge( - SubExpr<Note, Embed>, - SubExpr<Note, Embed>, - Option<SubExpr<Note, Embed>>, - ), + Merge(SubExpr, SubExpr, Option<SubExpr>), /// e.x - Field(SubExpr<Note, Embed>, Label), + Field(SubExpr, Label), /// e.{ x, y, z } - Projection(SubExpr<Note, Embed>, Vec<Label>), + Projection(SubExpr, Vec<Label>), /// Annotation on the AST. Unused for now but could hold e.g. file location information - Note(Note, SubExpr<Note, Embed>), + Note(Note, SubExpr), /// Embeds an import or the result of resolving the import Embed(Embed), } @@ -270,13 +259,12 @@ impl<S, A> Expr<S, A> { F3: FnOnce(&A) -> B, F4: Fn(&Label) -> Label, { - map_subexpr( - self, + self.map_ref( |x| rc(map_expr(x.as_ref())), + |_, x| rc(map_expr(x.as_ref())), map_note, map_embed, map_label, - |_, x| rc(map_expr(x.as_ref())), ) } @@ -299,12 +287,21 @@ impl<S, A> Expr<S, A> { let recurse = |e: &Self| -> Self { e.map_label(map_label) }; self.map_shallow(recurse, |x| x.clone(), |x| x.clone(), map_label) } + + #[inline(always)] + pub fn roll(&self) -> SubExpr<S, A> + where + S: Clone, + A: Clone, + { + rc(ExprF::clone(self)) + } } impl<S: Clone, A: Clone> Expr<S, Expr<S, A>> { pub fn squash_embed(&self) -> Expr<S, A> { match self { - Expr::Embed(e) => e.clone(), + ExprF::Embed(e) => e.clone(), e => e.map_shallow( |e| e.squash_embed(), |x| x.clone(), @@ -315,20 +312,297 @@ impl<S: Clone, A: Clone> Expr<S, Expr<S, A>> { } } +impl<SE, L, N, E> ExprF<SE, L, N, E> { + #[inline(always)] + pub fn as_ref(&self) -> ExprF<&SE, &L, &N, &E> + where + L: Ord, + { + fn opt<T>(x: &Option<T>) -> Option<&T> { + x.as_ref() + } + fn vec<T>(x: &Vec<T>) -> Vec<&T> { + x.iter().collect() + } + fn btmap<L: Ord, SE>(x: &BTreeMap<L, SE>) -> BTreeMap<&L, &SE> { + x.iter().collect() + } + + use crate::ExprF::*; + match self { + Var(V(l, n)) => Var(V(l, *n)), + Lam(l, t, b) => Lam(l, t, b), + Pi(l, t, b) => Pi(l, t, b), + Let(l, t, a, b) => Let(l, opt(t), a, b), + App(f, args) => App(f, vec(args)), + Annot(x, t) => Annot(x, t), + Const(k) => Const(*k), + Builtin(v) => Builtin(*v), + BoolLit(b) => BoolLit(*b), + NaturalLit(n) => NaturalLit(*n), + IntegerLit(n) => IntegerLit(*n), + DoubleLit(n) => DoubleLit(*n), + TextLit(t) => TextLit(t.as_ref()), + BinOp(o, x, y) => BinOp(*o, x, y), + BoolIf(b, t, f) => BoolIf(b, t, f), + EmptyListLit(t) => EmptyListLit(t), + NEListLit(es) => NEListLit(vec(es)), + EmptyOptionalLit(t) => EmptyOptionalLit(t), + NEOptionalLit(e) => NEOptionalLit(e), + RecordType(kts) => RecordType(btmap(kts)), + RecordLit(kvs) => RecordLit(btmap(kvs)), + UnionType(kts) => UnionType(btmap(kts)), + UnionLit(k, v, kvs) => UnionLit(k, v, btmap(kvs)), + Merge(x, y, t) => Merge(x, y, opt(t)), + Field(e, l) => Field(e, l), + Projection(e, ls) => Projection(e, vec(ls)), + Note(n, e) => Note(n, e), + Embed(a) => Embed(a), + } + } + + #[inline(always)] + pub fn map<SE2, L2, N2, E2, F1, F2, F3, F4, F5>( + self, + map_subexpr: F1, + map_under_binder: F2, + map_note: F3, + map_embed: F4, + mut map_label: F5, + ) -> ExprF<SE2, L2, N2, E2> + where + L: Ord, + L2: Ord, + F1: FnMut(SE) -> SE2, + F2: FnOnce(&L, SE) -> SE2, + F3: FnOnce(N) -> N2, + F4: FnOnce(E) -> E2, + F5: FnMut(L) -> L2, + { + let mut map = map_subexpr; + fn vec<T, U, F: FnMut(T) -> U>(x: Vec<T>, f: F) -> Vec<U> { + x.into_iter().map(f).collect() + } + fn btmap<K, L, T, U, FK, FV>( + x: BTreeMap<K, T>, + mut fk: FK, + mut fv: FV, + ) -> BTreeMap<L, U> + where + K: Ord, + L: Ord, + FK: FnMut(K) -> L, + FV: FnMut(T) -> U, + { + x.into_iter().map(|(k, v)| (fk(k), fv(v))).collect() + } + + use crate::ExprF::*; + match self { + Var(V(l, n)) => Var(V(map_label(l), n)), + Lam(l, t, b) => { + let b = map_under_binder(&l, b); + Lam(map_label(l), map(t), b) + } + Pi(l, t, b) => { + let b = map_under_binder(&l, b); + Pi(map_label(l), map(t), b) + } + Let(l, t, a, b) => { + let b = map_under_binder(&l, b); + Let(map_label(l), t.map(&mut map), map(a), b) + } + App(f, args) => App(map(f), vec(args, map)), + Annot(x, t) => Annot(map(x), map(t)), + Const(k) => Const(k), + Builtin(v) => Builtin(v), + BoolLit(b) => BoolLit(b), + NaturalLit(n) => NaturalLit(n), + IntegerLit(n) => IntegerLit(n), + DoubleLit(n) => DoubleLit(n), + TextLit(t) => TextLit(t.map(map)), + BinOp(o, x, y) => BinOp(o, map(x), map(y)), + BoolIf(b, t, f) => BoolIf(map(b), map(t), map(f)), + EmptyListLit(t) => EmptyListLit(map(t)), + NEListLit(es) => NEListLit(vec(es, map)), + EmptyOptionalLit(t) => EmptyOptionalLit(map(t)), + NEOptionalLit(e) => NEOptionalLit(map(e)), + RecordType(kts) => RecordType(btmap(kts, map_label, map)), + RecordLit(kvs) => RecordLit(btmap(kvs, map_label, map)), + UnionType(kts) => UnionType(btmap(kts, map_label, map)), + UnionLit(k, v, kvs) => { + UnionLit(map_label(k), map(v), btmap(kvs, map_label, map)) + } + Merge(x, y, t) => Merge(map(x), map(y), t.map(map)), + Field(e, l) => Field(map(e), map_label(l)), + Projection(e, ls) => Projection(map(e), vec(ls, map_label)), + Note(n, e) => Note(map_note(n), map(e)), + Embed(a) => Embed(map_embed(a)), + } + } + + #[inline(always)] + pub fn map_ref<'a, SE2, L2, N2, E2, F1, F2, F3, F4, F5>( + &'a self, + map_subexpr: F1, + map_under_binder: F2, + map_note: F3, + map_embed: F4, + map_label: F5, + ) -> ExprF<SE2, L2, N2, E2> + where + L: Ord, + L2: Ord, + F1: FnMut(&'a SE) -> SE2, + F2: FnOnce(&'a L, &'a SE) -> SE2, + F3: FnOnce(&'a N) -> N2, + F4: FnOnce(&'a E) -> E2, + F5: FnMut(&'a L) -> L2, + { + // Not optimal: reallocates all the Vecs and BTreeMaps for nothing. + self.as_ref().map( + map_subexpr, + |l, e| map_under_binder(*l, e), + map_note, + map_embed, + map_label, + ) + } + + #[inline(always)] + pub fn map_ref_simple<'a, SE2, F1>( + &'a self, + map_subexpr: F1, + ) -> ExprF<SE2, L, N, E> + where + L: Ord, + L: Clone, + N: Clone, + E: Clone, + F1: Fn(&'a SE) -> SE2, + { + self.map_ref( + &map_subexpr, + |_, e| map_subexpr(e), + N::clone, + E::clone, + L::clone, + ) + } + + // #[inline(always)] + // pub fn zip<SE2, L2, N2, E2>( + // self, + // other: ExprF<SE2, L2, N2, E2> + // ) -> Option<ExprF<(SE, SE2), (L, L2), (N, N2), (E, E2)>> + // where + // L: Ord, + // L2: Ord, + // { + // // What to do with Var ? + // use crate::ExprF::*; + // match (self, other) { + // // Var(V(l, n)) => Var(V(map_label(l), n)), + // // Lam(l, t, b) => { + // // Pi(l, t, b) => { + // // Let(l, t, a, b) => { + // // App(f, args) => App(map(f), vec(args, map)), + // // Annot(x, t) => Annot(map(x), map(t)), + // (Const(x), Const(y)) if x == y => Some(Const(x)), + // (Builtin(x), Builtin(y)) if x == y => Some(Builtin(x)), + // (BoolLit(x), BoolLit(y)) if x == y => Some(BoolLit(x)), + // (NaturalLit(x), NaturalLit(y)) if x == y => Some(NaturalLit(x)), + // (IntegerLit(x), IntegerLit(y)) if x == y => Some(IntegerLit(x)), + // (DoubleLit(x), DoubleLit(y)) if x == y => Some(DoubleLit(x)), + // // TextLit(t) => TextLit(t.map(map)), + // // BinOp(o, x, y) => BinOp(o, map(x), map(y)), + // // BoolIf(b, t, f) => BoolIf(map(b), map(t), map(f)), + // // EmptyListLit(t) => EmptyListLit(map(t)), + // // NEListLit(es) => NEListLit(vec(es, map)), + // // EmptyOptionalLit(t) => EmptyOptionalLit(map(t)), + // // NEOptionalLit(e) => NEOptionalLit(map(e)), + // // RecordType(kts) => RecordType(btmap(kts, map_label, map)), + // // RecordLit(kvs) => RecordLit(btmap(kvs, map_label, map)), + // // UnionType(kts) => UnionType(btmap(kts, map_label, map)), + // // UnionLit(k, v, kvs) => { + // // Merge(x, y, t) => Merge(map(x), map(y), t.map(map)), + // // Field(e, l) => Field(map(e), map_label(l)), + // // Projection(e, ls) => Projection(map(e), vec(ls, map_label)), + // // Note(n, e) => Note(map_note(n), map(e)), + // // Embed(a) => Embed(map_embed(a)), + // } + // } +} + +impl<N, E> SubExpr<N, E> { + #[inline(always)] + pub fn as_ref(&self) -> &Expr<N, E> { + self.0.as_ref() + } + + pub fn map_ref<'a, F1, F2>( + &'a self, + map_expr: F1, + map_under_binder: F2, + ) -> Self + where + F1: FnMut(&'a Self) -> Self, + F2: FnOnce(&'a Label, &'a Self) -> Self, + { + match self.as_ref() { + ExprF::Embed(_) => SubExpr::clone(self), + // Recursive call + ExprF::Note(_, e) => e.map_ref(map_expr, map_under_binder), + // Call ExprF::map_ref + e => rc(e.map_ref( + map_expr, + map_under_binder, + |_| unreachable!(), + |_| unreachable!(), + Label::clone, + )), + } + } + + pub fn map_ref_simple<F1>(&self, map_expr: F1) -> Self + where + F1: Fn(&Self) -> Self, + { + self.map_ref(&map_expr, |_, e| map_expr(e)) + } + + #[inline(always)] + pub fn unroll(&self) -> Expr<N, E> + where + N: Clone, + E: Clone, + { + ExprF::clone(self.as_ref()) + } +} + +impl<N, E> Clone for SubExpr<N, E> { + #[inline(always)] + fn clone(&self) -> Self { + SubExpr(Rc::clone(&self.0)) + } +} + // Remains of a previous life, where everything was in Boxes -pub fn bx<T>(x: T) -> Rc<T> { - Rc::new(x) +pub fn bx<N, E>(x: Expr<N, E>) -> SubExpr<N, E> { + SubExpr(Rc::new(x)) } -pub fn rc<T>(x: T) -> Rc<T> { - Rc::new(x) +// Should probably rename this too +pub fn rc<N, E>(x: Expr<N, E>) -> SubExpr<N, E> { + SubExpr(Rc::new(x)) } pub fn app<N, E>(f: Expr<N, E>, args: Vec<SubExpr<N, E>>) -> Expr<N, E> { if args.is_empty() { f } else { - Expr::App(rc(f), args) + ExprF::App(rc(f), args) } } @@ -339,7 +613,7 @@ pub fn app_rc<N, E>( if args.is_empty() { f } else { - rc(Expr::App(f, args)) + rc(ExprF::App(f, args)) } } @@ -351,100 +625,6 @@ fn add_ui(u: usize, i: isize) -> usize { } } -/// Map over the immediate children of the passed Expr -pub fn map_subexpr<S, T, A, B, F1, F2, F3, F4, F5>( - e: &Expr<S, A>, - map: F1, - map_note: F2, - map_embed: F3, - map_label: F4, - map_under_binder: F5, -) -> Expr<T, B> -where - F1: Fn(&SubExpr<S, A>) -> SubExpr<T, B>, - F2: FnOnce(&S) -> T, - F3: FnOnce(&A) -> B, - F4: Fn(&Label) -> Label, - F5: FnOnce(&Label, &SubExpr<S, A>) -> SubExpr<T, B>, -{ - use crate::Expr::*; - let map = ↦ - let opt = |x: &Option<_>| x.as_ref().map(&map); - let vec = |x: &Vec<_>| x.iter().map(&map).collect(); - let btmap = |x: &BTreeMap<_, _>| { - x.into_iter().map(|(k, v)| (map_label(k), map(v))).collect() - }; - match e { - Const(k) => Const(*k), - Var(V(l, n)) => Var(V(map_label(l), *n)), - Lam(l, t, b) => Lam(map_label(l), map(t), map_under_binder(l, b)), - Pi(l, t, b) => Pi(map_label(l), map(t), map_under_binder(l, b)), - App(f, args) => App(map(f), vec(args)), - Let(l, t, a, b) => { - Let(map_label(l), opt(t), map(a), map_under_binder(l, b)) - } - Annot(x, t) => Annot(map(x), map(t)), - Builtin(v) => Builtin(*v), - BoolLit(b) => BoolLit(*b), - BoolIf(b, t, f) => BoolIf(map(b), map(t), map(f)), - NaturalLit(n) => NaturalLit(*n), - IntegerLit(n) => IntegerLit(*n), - DoubleLit(n) => DoubleLit(*n), - TextLit(t) => TextLit(t.map(&map)), - BinOp(o, x, y) => BinOp(*o, map(x), map(y)), - EmptyListLit(t) => EmptyListLit(map(t)), - NEListLit(es) => NEListLit(vec(es)), - EmptyOptionalLit(t) => EmptyOptionalLit(map(t)), - NEOptionalLit(e) => NEOptionalLit(map(e)), - RecordType(kts) => RecordType(btmap(kts)), - RecordLit(kvs) => RecordLit(btmap(kvs)), - UnionType(kts) => UnionType(btmap(kts)), - UnionLit(k, v, kvs) => UnionLit(map_label(k), map(v), btmap(kvs)), - Merge(x, y, t) => Merge(map(x), map(y), opt(t)), - Field(e, l) => Field(map(e), map_label(l)), - Projection(e, ls) => { - Projection(map(e), ls.iter().map(&map_label).collect()) - } - Note(n, e) => Note(map_note(n), map(e)), - Embed(a) => Embed(map_embed(a)), - } -} - -pub fn map_subexpr_rc_binder<S, A, F1, F2>( - e: &SubExpr<S, A>, - map_expr: F1, - map_under_binder: F2, -) -> SubExpr<S, A> -where - F1: Fn(&SubExpr<S, A>) -> SubExpr<S, A>, - F2: FnOnce(&Label, &SubExpr<S, A>) -> SubExpr<S, A>, -{ - match e.as_ref() { - Expr::Embed(_) => Rc::clone(e), - Expr::Note(_, e) => { - map_subexpr_rc_binder(e, map_expr, map_under_binder) - } - _ => rc(map_subexpr( - e, - map_expr, - |_| unreachable!(), - |_| unreachable!(), - Label::clone, - map_under_binder, - )), - } -} - -pub fn map_subexpr_rc<S, A, F1>( - e: &SubExpr<S, A>, - map_expr: F1, -) -> SubExpr<S, A> -where - F1: Fn(&SubExpr<S, A>) -> SubExpr<S, A>, -{ - map_subexpr_rc_binder(e, &map_expr, |_, e| map_expr(e)) -} - /// `shift` is used by both normalization and type-checking to avoid variable /// capture by shifting variable indices /// @@ -518,10 +698,10 @@ where /// pub fn shift<S, A>( delta: isize, - var: &V, - in_expr: &Rc<Expr<S, A>>, -) -> Rc<Expr<S, A>> { - use crate::Expr::*; + var: &V<Label>, + in_expr: &SubExpr<S, A>, +) -> SubExpr<S, A> { + use crate::ExprF::*; let V(x, n) = var; let under_binder = |y: &Label, e: &SubExpr<_, _>| { let n = if x == y { n + 1 } else { *n }; @@ -532,11 +712,7 @@ pub fn shift<S, A>( Var(V(y, m)) if x == y && n <= m => { rc(Var(V(y.clone(), add_ui(*m, delta)))) } - _ => map_subexpr_rc_binder( - in_expr, - |e| shift(delta, var, e), - under_binder, - ), + _ => in_expr.map_ref(|e| shift(delta, var, e), under_binder), } } @@ -547,11 +723,11 @@ pub fn shift<S, A>( /// ``` /// pub fn subst<S, A>( - var: &V, - value: &Rc<Expr<S, A>>, - in_expr: &Rc<Expr<S, A>>, -) -> Rc<Expr<S, A>> { - use crate::Expr::*; + var: &V<Label>, + value: &SubExpr<S, A>, + in_expr: &SubExpr<S, A>, +) -> SubExpr<S, A> { + use crate::ExprF::*; let under_binder = |y: &Label, e: &SubExpr<_, _>| { let V(x, n) = var; let n = if x == y { n + 1 } else { *n }; @@ -559,11 +735,7 @@ pub fn subst<S, A>( subst(newvar, &shift(1, &V(y.clone(), 0), value), e) }; match in_expr.as_ref() { - Var(v) if var == v => Rc::clone(value), - _ => map_subexpr_rc_binder( - in_expr, - |e| subst(var, value, e), - under_binder, - ), + Var(v) if var == v => SubExpr::clone(value), + _ => in_expr.map_ref(|e| subst(var, value, e), under_binder), } } |