From 1a644d25f60309ec2fa9a75282841bb7b1ad6269 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 9 Mar 2019 00:43:34 +0100 Subject: rustfmt --- dhall/src/typecheck.rs | 50 ++++++++++++++++++++++++++++++++--------------- dhall_core/src/core.rs | 53 +++++++++++++++++++++++++++++--------------------- 2 files changed, 65 insertions(+), 38 deletions(-) diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index fa938ef..6e7775c 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -10,7 +10,7 @@ use dhall_core::core::Builtin::*; use dhall_core::core::Const::*; use dhall_core::core::Expr::*; use dhall_core::core::{app, pi}; -use dhall_core::core::{bx, shift, subst, Expr, V, X, StringLike}; +use dhall_core::core::{bx, shift, subst, Expr, StringLike, V, X}; use self::TypeMessage::*; @@ -48,7 +48,10 @@ fn match_vars(vl: &V, vr: &V, ctx: &[(L, L)]) -> bool { } } -fn prop_equal(eL0: &Expr, eR0: &Expr) -> bool +fn prop_equal( + eL0: &Expr, + eR0: &Expr, +) -> bool where S: Clone + ::std::fmt::Debug, T: Clone + ::std::fmt::Debug, @@ -387,7 +390,8 @@ where pi("zero", "natural", "natural"), ), ), - ).take_ownership_of_labels()), + ) + .take_ownership_of_labels()), Builtin(NaturalBuild) => Ok(pi( "_", pi( @@ -400,9 +404,14 @@ where ), ), Natural, - ).take_ownership_of_labels()), + ) + .take_ownership_of_labels()), Builtin(NaturalIsZero) | Builtin(NaturalEven) | Builtin(NaturalOdd) => { - Ok(Pi("_".to_owned().into(), bx(Natural.into()), bx(Bool.into()))) + Ok(Pi( + "_".to_owned().into(), + bx(Natural.into()), + bx(Bool.into()), + )) } BinOp(NaturalPlus, ref l, ref r) => { op2_type(ctx, e, Natural, CantAdd, l, r) @@ -461,7 +470,8 @@ where ), app(List, "a"), ), - ).take_ownership_of_labels()), + ) + .take_ownership_of_labels()), Builtin(ListFold) => Ok(pi( "a", Const(Type), @@ -478,15 +488,18 @@ where ), ), ), - ).take_ownership_of_labels()), + ) + .take_ownership_of_labels()), Builtin(ListLength) => { - Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural)).take_ownership_of_labels()) + Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural)) + .take_ownership_of_labels()) } Builtin(ListHead) | Builtin(ListLast) => Ok(pi( "a", Const(Type), pi("_", app(List, "a"), app(Optional, "a")), - ).take_ownership_of_labels()), + ) + .take_ownership_of_labels()), Builtin(ListIndexed) => { let mut m: BTreeMap> = BTreeMap::new(); m.insert("index".into(), Builtin(Natural)); @@ -497,11 +510,12 @@ where pi("_", app(List, Var(V("a".into(), 0))), app(List, Record(m))), )) } - Builtin(ListReverse) => Ok(pi( - "a", - Const(Type), - pi("_", app(List, "a"), app(List, "a")), - ).take_ownership_of_labels()), + Builtin(ListReverse) => { + Ok( + pi("a", Const(Type), pi("_", app(List, "a"), app(List, "a"))) + .take_ownership_of_labels(), + ) + } OptionalLit(ref t, ref xs) => { let mut iter = xs.iter(); let t: Box> = match t { @@ -553,7 +567,8 @@ where ), ), ), - ).take_ownership_of_labels()), + ) + .take_ownership_of_labels()), Builtin(List) | Builtin(Optional) => { Ok(pi("_", Const(Type), Const(Type)).take_ownership_of_labels()) } @@ -708,7 +723,10 @@ where /// `typeOf` is the same as `type_with` with an empty context, meaning that the /// expression must be closed (i.e. no free variables), otherwise type-checking /// will fail. -pub fn type_of, S: Clone + ::std::fmt::Debug>( +pub fn type_of< + Label: StringLike + From, + S: Clone + ::std::fmt::Debug, +>( e: &Expr, ) -> Result, TypeError> { let ctx = Context::new(); diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs index 3b98b39..eed9e0c 100644 --- a/dhall_core/src/core.rs +++ b/dhall_core/src/core.rs @@ -157,10 +157,7 @@ pub enum Expr { Box>, ), /// `App f A ~ f A` - App( - Box>, - Box>, - ), + App(Box>, Box>), /// `Let x Nothing r e ~ let x = r in e` /// `Let x (Just t) r e ~ let x : t = r in e` Let( @@ -170,10 +167,7 @@ pub enum Expr { Box>, ), /// `Annot x t ~ x : t` - Annot( - Box>, - Box>, - ), + Annot(Box>, Box>), /// Built-in values Builtin(Builtin), // Binary operations @@ -369,19 +363,32 @@ impl Expr { } impl<'i, S: Clone, A: Clone> Expr<&'i str, S, A> { - pub fn take_ownership_of_labels>(&self) -> Expr { - let recurse = - |e: &Expr<&'i str, S, A>| -> Expr { e.take_ownership_of_labels() }; - map_shallow(self, recurse, |x| x.clone(), |x| x.clone(), |x: &&str| -> L { (*x).to_owned().into() }) + pub fn take_ownership_of_labels>( + &self, + ) -> Expr { + let recurse = |e: &Expr<&'i str, S, A>| -> Expr { + e.take_ownership_of_labels() + }; + map_shallow( + self, + recurse, + |x| x.clone(), + |x| x.clone(), + |x: &&str| -> L { (*x).to_owned().into() }, + ) } } impl Expr> { - pub fn squash_embed(&self) -> Expr - { + pub fn squash_embed(&self) -> Expr { match self { Expr::Embed(e) => e.clone(), - e => e.map_shallow(|e| e.squash_embed(), |x| x.clone(), |_| unreachable!(), |x| x.clone()) + e => e.map_shallow( + |e| e.squash_embed(), + |x| x.clone(), + |_| unreachable!(), + |x| x.clone(), + ), } } } @@ -779,7 +786,8 @@ where A: Clone, S: Clone, T: Clone, - Label1: Display + fmt::Debug + Clone + Hash + Ord + Eq + Into + Default, + Label1: + Display + fmt::Debug + Clone + Hash + Ord + Eq + Into + Default, Label2: StringLike, F1: Fn(&Expr) -> Expr, F2: FnOnce(&S) -> T, @@ -1007,9 +1015,7 @@ where es.iter().map(|e| shift(d, v, e)).collect(), ), Record(a) => Record(map_record_value(a, |val| shift(d, v, val))), - RecordLit(a) => { - RecordLit(map_record_value(a, |val| shift(d, v, val))) - } + RecordLit(a) => RecordLit(map_record_value(a, |val| shift(d, v, val))), Union(a) => Union(map_record_value(a, |val| shift(d, v, val))), UnionLit(k, uv, a) => UnionLit( k.clone(), @@ -1068,13 +1074,15 @@ where Const(a) => Const(*a), Lam(y, tA, b) => { let n2 = if x == y { n + 1 } else { *n }; - let b2 = subst(&V(x.clone(), n2), &shift(1, &V(y.clone(), 0), e), b); + let b2 = + subst(&V(x.clone(), n2), &shift(1, &V(y.clone(), 0), e), b); let tA2 = subst(v, e, tA); Lam(y.clone(), bx(tA2), bx(b2)) } Pi(y, tA, tB) => { let n2 = if x == y { n + 1 } else { *n }; - let tB2 = subst(&V(x.clone(), n2), &shift(1, &V(y.clone(), 0), e), tB); + let tB2 = + subst(&V(x.clone(), n2), &shift(1, &V(y.clone(), 0), e), tB); let tA2 = subst(v, e, tA); Pi(y.clone(), bx(tA2), bx(tB2)) } @@ -1092,7 +1100,8 @@ where } Let(f, mt, r, b) => { let n2 = if x == f { n + 1 } else { *n }; - let b2 = subst(&V(x.clone(), n2), &shift(1, &V(f.clone(), 0), e), b); + let b2 = + subst(&V(x.clone(), n2), &shift(1, &V(f.clone(), 0), e), b); let mt2 = mt.as_ref().map(|t| bx(subst(v, e, t))); let r2 = subst(v, e, r); Let(f.clone(), mt2, bx(r2), bx(b2)) -- cgit v1.2.3