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 ++++++++++++++++++++++++++++++++++---------------- 1 file changed, 34 insertions(+), 16 deletions(-) (limited to 'dhall') 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(); -- cgit v1.2.3