From 320eddc8850b1a36a006cbb136e54a9e2322674f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 11:26:56 +0200 Subject: Remove an unnecessary normalization --- dhall/src/typecheck.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 145de63..97c4de6 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -264,13 +264,12 @@ where return Err(mkerr(NotAFunction(f.clone(), tf))); } }; - let tA = normalize(SubExpr::clone(tA)); let tA2 = normalized_type_with(ctx, a.clone())?; if prop_equal(tA.as_ref(), tA2.as_ref()) { let vx0 = &V(x.clone(), 0); return Ok(subst_shift(vx0, &a, &tB)); } else { - Err(mkerr(TypeMismatch(f.clone(), tA, a.clone(), tA2))) + Err(mkerr(TypeMismatch(f.clone(), tA.clone(), a.clone(), tA2))) } } Let(f, mt, r, b) => { -- cgit v1.2.3 From 3ce264fb88fb659f238601b70d6b7c5683a43aee Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 11:33:10 +0200 Subject: Ensure all type errors carry normalized types --- dhall/src/typecheck.rs | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 97c4de6..5184e72 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -279,14 +279,14 @@ where SubExpr::clone(r) }; - let tR = type_with(ctx, r)?; + let tR = normalized_type_with(ctx, r)?; let ttR = normalized_type_with(ctx, tR.clone())?; // Don't bother to provide a `let`-specific version of this error // message because this should never happen anyway let kR = ensure_const(&ttR, InvalidInputType(tR.clone()))?; let ctx2 = ctx.insert(f.clone(), tR.clone()); - let tB = type_with(&ctx2, b.clone())?; + let tB = normalized_type_with(&ctx2, b.clone())?; let ttB = normalized_type_with(ctx, tB.clone())?; // Don't bother to provide a `let`-specific version of this error // message because this should never happen anyway @@ -351,11 +351,9 @@ where NEListLit(xs) => { let mut iter = xs.iter().enumerate(); let (_, first_x) = iter.next().unwrap(); - let t = type_with(ctx, first_x.clone())?; - + let t = normalized_type_with(ctx, first_x.clone())?; let s = normalized_type_with(ctx, t.clone())?; ensure_is_type(s, InvalidListType(t.clone()))?; - let t = normalize(t); for (i, x) in iter { let t2 = normalized_type_with(ctx, x.clone())?; if !prop_equal(t.as_ref(), t2.as_ref()) { @@ -371,10 +369,9 @@ where return Ok(dhall_expr!(Optional t)); } NEOptionalLit(x) => { - let t: SubExpr<_, _> = type_with(ctx, x.clone())?; + let t = normalized_type_with(ctx, x.clone())?; let s = normalized_type_with(ctx, t.clone())?; ensure_is_type(s, InvalidOptionalType(t.clone()))?; - let t = normalize(t); return Ok(dhall_expr!(Optional t)); } RecordType(kts) => { -- cgit v1.2.3 From e56b23ea05f7827c54187173eb86b31f7fe70422 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 11:36:11 +0200 Subject: Normalize output of type inference --- dhall/src/typecheck.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 5184e72..a9b9d7d 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -217,7 +217,7 @@ where let ctx2 = ctx .insert(x.clone(), tA.clone()) .map(|e| shift(1, &V(x.clone(), 0), e)); - let tB = type_with(&ctx2, b.clone())?; + let tB = normalized_type_with(&ctx2, b.clone())?; let p = rc(Pi(x.clone(), tA.clone(), tB)); let _ = type_with(ctx, p.clone())?; return Ok(p); @@ -249,7 +249,7 @@ where App(f, args) => { // Recurse on args let (a, tf) = match args.split_last() { - None => return type_with(ctx, f.clone()), + None => return normalized_type_with(ctx, f.clone()), Some((a, args)) => ( a, normalized_type_with( @@ -385,7 +385,7 @@ where let kts = kvs .iter() .map(|(k, v)| { - let t = type_with(ctx, v.clone())?; + let t = normalized_type_with(ctx, v.clone())?; let s = normalized_type_with(ctx, t.clone())?; ensure_is_type(s, InvalidField(k.clone(), v.clone()))?; Ok((k.clone(), t)) @@ -458,7 +458,7 @@ pub fn type_of( e: SubExpr, ) -> Result, TypeError> { let ctx = Context::new(); - type_with(&ctx, e) //.map(|e| e.into_owned()) + normalized_type_with(&ctx, e) //.map(|e| e.into_owned()) } /// The specific type error -- cgit v1.2.3 From 35d735e3e1404fa917c95cbd914bccf0b3908ba0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 11:46:27 +0200 Subject: Split dhall_expr!() into 2 --- dhall/src/lib.rs | 2 ++ 1 file changed, 2 insertions(+) (limited to 'dhall/src') diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 0270103..103fd29 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -14,6 +14,8 @@ mod dhall_type; pub mod imports; pub mod typecheck; pub use crate::dhall_type::*; +pub use dhall_generator::expr; +pub use dhall_generator::subexpr; pub use dhall_generator::Type; pub use crate::imports::*; -- cgit v1.2.3 From 58e83f17452d7a4a68716c6b8933726963f4b1d6 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 12:15:10 +0200 Subject: Avoid early returns in type_with --- dhall/src/typecheck.rs | 79 ++++++++++++++++++++++++-------------------------- 1 file changed, 38 insertions(+), 41 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index a9b9d7d..22d3c42 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -6,7 +6,7 @@ use crate::normalize::normalize; use dhall_core; use dhall_core::context::Context; use dhall_core::*; -use dhall_generator::dhall_expr; +use dhall_generator as dhall; use self::TypeMessage::*; @@ -112,31 +112,31 @@ where go::(&mut ctx, eL0, eR0) } -fn type_of_builtin(b: Builtin) -> SubExpr { +fn type_of_builtin(b: Builtin) -> Expr { use dhall_core::Builtin::*; match b { - Bool | Natural | Integer | Double | Text => dhall_expr!(Type), - List | Optional => dhall_expr!( + Bool | Natural | Integer | Double | Text => dhall::expr!(Type), + List | Optional => dhall::expr!( Type -> Type ), - NaturalFold => dhall_expr!( + NaturalFold => dhall::expr!( Natural -> forall (natural: Type) -> forall (succ: natural -> natural) -> forall (zero: natural) -> natural ), - NaturalBuild => dhall_expr!( + NaturalBuild => dhall::expr!( (forall (natural: Type) -> forall (succ: natural -> natural) -> forall (zero: natural) -> natural) -> Natural ), - NaturalIsZero | NaturalEven | NaturalOdd => dhall_expr!( + NaturalIsZero | NaturalEven | NaturalOdd => dhall::expr!( Natural -> Bool ), - ListBuild => dhall_expr!( + ListBuild => dhall::expr!( forall (a: Type) -> (forall (list: Type) -> forall (cons: a -> list -> list) -> @@ -144,7 +144,7 @@ fn type_of_builtin(b: Builtin) -> SubExpr { list) -> List a ), - ListFold => dhall_expr!( + ListFold => dhall::expr!( forall (a: Type) -> List a -> forall (list: Type) -> @@ -152,19 +152,19 @@ fn type_of_builtin(b: Builtin) -> SubExpr { forall (nil: list) -> list ), - ListLength => dhall_expr!(forall (a: Type) -> List a -> Natural), + ListLength => dhall::expr!(forall (a: Type) -> List a -> Natural), ListHead | ListLast => { - dhall_expr!(forall (a: Type) -> List a -> Optional a) + dhall::expr!(forall (a: Type) -> List a -> Optional a) } - ListIndexed => dhall_expr!( + ListIndexed => dhall::expr!( forall (a: Type) -> List a -> List { index: Natural, value: a } ), - ListReverse => dhall_expr!( + ListReverse => dhall::expr!( forall (a: Type) -> List a -> List a ), - OptionalFold => dhall_expr!( + OptionalFold => dhall::expr!( forall (a: Type) -> Optional a -> forall (optional: Type) -> @@ -205,22 +205,20 @@ where _ => Err(mkerr(msg)), }; - match e.as_ref() { + let ret = match e.as_ref() { Const(c) => axiom(*c).map(Const), - Var(V(x, n)) => { - return ctx - .lookup(x, *n) - .cloned() - .ok_or_else(|| mkerr(UnboundVariable)) - } + Var(V(x, n)) => match ctx.lookup(x, *n) { + Some(e) => Ok(e.unroll()), + None => Err(mkerr(UnboundVariable)), + }, Lam(x, tA, b) => { let ctx2 = ctx .insert(x.clone(), tA.clone()) .map(|e| shift(1, &V(x.clone(), 0), e)); let tB = normalized_type_with(&ctx2, b.clone())?; - let p = rc(Pi(x.clone(), tA.clone(), tB)); - let _ = type_with(ctx, p.clone())?; - return Ok(p); + let p = Pi(x.clone(), tA.clone(), tB); + let _ = normalized_type_with(ctx, rc(p.clone()))?; + Ok(p) } Pi(x, tA, tB) => { let tA2 = normalized_type_with(ctx, tA.clone())?; @@ -267,7 +265,7 @@ where let tA2 = normalized_type_with(ctx, a.clone())?; if prop_equal(tA.as_ref(), tA2.as_ref()) { let vx0 = &V(x.clone(), 0); - return Ok(subst_shift(vx0, &a, &tB)); + Ok(subst_shift(vx0, &a, &tB).unroll()) } else { Err(mkerr(TypeMismatch(f.clone(), tA.clone(), a.clone(), tA2))) } @@ -296,16 +294,16 @@ where return Err(mkerr(NoDependentLet(tR, tB))); } - return Ok(tB); + Ok(tB.unroll()) } Annot(x, t) => { // This is mainly just to check that `t` is not `Kind` - let _ = type_with(ctx, t.clone())?; + let _ = normalized_type_with(ctx, t.clone())?; let t2 = normalized_type_with(ctx, x.clone())?; let t = normalize(t.clone()); if prop_equal(t.as_ref(), t2.as_ref()) { - return Ok(t.clone()); + Ok(t.unroll()) } else { Err(mkerr(AnnotMismatch(x.clone(), t, t2))) } @@ -340,13 +338,13 @@ where tz, ))); } - return Ok(ty); + Ok(ty.unroll()) } EmptyListLit(t) => { let s = normalized_type_with(ctx, t.clone())?; ensure_is_type(s, InvalidListType(t.clone()))?; let t = normalize(SubExpr::clone(t)); - return Ok(dhall_expr!(List t)); + Ok(dhall::expr!(List t)) } NEListLit(xs) => { let mut iter = xs.iter().enumerate(); @@ -360,19 +358,19 @@ where return Err(mkerr(InvalidListElement(i, t, x.clone(), t2))); } } - return Ok(dhall_expr!(List t)); + Ok(dhall::expr!(List t)) } EmptyOptionalLit(t) => { let s = normalized_type_with(ctx, t.clone())?; ensure_is_type(s, InvalidOptionalType(t.clone()))?; let t = normalize(t.clone()); - return Ok(dhall_expr!(Optional t)); + Ok(dhall::expr!(Optional t)) } NEOptionalLit(x) => { let t = normalized_type_with(ctx, x.clone())?; let s = normalized_type_with(ctx, t.clone())?; ensure_is_type(s, InvalidOptionalType(t.clone()))?; - return Ok(dhall_expr!(Optional t)); + Ok(dhall::expr!(Optional t)) } RecordType(kts) => { for (k, t) in kts { @@ -396,15 +394,14 @@ where Field(r, x) => { let t = normalized_type_with(ctx, r.clone())?; match t.as_ref() { - RecordType(kts) => { - return kts.get(x).cloned().ok_or_else(|| { - mkerr(MissingField(x.clone(), t.clone())) - }) - } + RecordType(kts) => match kts.get(x) { + Some(e) => Ok(e.unroll()), + None => Err(mkerr(MissingField(x.clone(), t.clone()))), + }, _ => Err(mkerr(NotARecord(x.clone(), r.clone(), t.clone()))), } } - Builtin(b) => return Ok(type_of_builtin(*b)), + Builtin(b) => Ok(type_of_builtin(*b)), BoolLit(_) => Ok(Builtin(Bool)), NaturalLit(_) => Ok(Builtin(Natural)), IntegerLit(_) => Ok(Builtin(Integer)), @@ -437,8 +434,8 @@ where } Embed(p) => match *p {}, _ => panic!("Unimplemented typecheck case: {:?}", e), - } - .map(rc) + }?; + Ok(rc(ret)) } pub fn normalized_type_with( -- cgit v1.2.3 From 79721ab94c8ee5daa43bab779841b2d8467fc588 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 12:20:04 +0200 Subject: type_with always normalizes --- dhall/src/typecheck.rs | 84 +++++++++++++++++++++----------------------------- 1 file changed, 35 insertions(+), 49 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 22d3c42..e5b81bd 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -215,19 +215,19 @@ where let ctx2 = ctx .insert(x.clone(), tA.clone()) .map(|e| shift(1, &V(x.clone(), 0), e)); - let tB = normalized_type_with(&ctx2, b.clone())?; + let tB = type_with(&ctx2, b.clone())?; let p = Pi(x.clone(), tA.clone(), tB); - let _ = normalized_type_with(ctx, rc(p.clone()))?; + let _ = type_with(ctx, rc(p.clone()))?; Ok(p) } Pi(x, tA, tB) => { - let tA2 = normalized_type_with(ctx, tA.clone())?; + let tA2 = type_with(ctx, tA.clone())?; let kA = ensure_const(&tA2, InvalidInputType(tA.clone()))?; let ctx2 = ctx .insert(x.clone(), tA.clone()) .map(|e| shift(1, &V(x.clone(), 0), e)); - let tB = normalized_type_with(&ctx2, tB.clone())?; + let tB = type_with(&ctx2, tB.clone())?; let kB = match tB.as_ref() { Const(k) => *k, _ => { @@ -247,14 +247,10 @@ where App(f, args) => { // Recurse on args let (a, tf) = match args.split_last() { - None => return normalized_type_with(ctx, f.clone()), - Some((a, args)) => ( - a, - normalized_type_with( - ctx, - rc(App(f.clone(), args.to_vec())), - )?, - ), + None => return type_with(ctx, f.clone()), + Some((a, args)) => { + (a, type_with(ctx, rc(App(f.clone(), args.to_vec())))?) + } }; let (x, tA, tB) = match tf.as_ref() { Pi(x, tA, tB) => (x, tA, tB), @@ -262,7 +258,7 @@ where return Err(mkerr(NotAFunction(f.clone(), tf))); } }; - let tA2 = normalized_type_with(ctx, a.clone())?; + let tA2 = type_with(ctx, a.clone())?; if prop_equal(tA.as_ref(), tA2.as_ref()) { let vx0 = &V(x.clone(), 0); Ok(subst_shift(vx0, &a, &tB).unroll()) @@ -277,15 +273,15 @@ where SubExpr::clone(r) }; - let tR = normalized_type_with(ctx, r)?; - let ttR = normalized_type_with(ctx, tR.clone())?; + let tR = type_with(ctx, r)?; + let ttR = type_with(ctx, tR.clone())?; // Don't bother to provide a `let`-specific version of this error // message because this should never happen anyway let kR = ensure_const(&ttR, InvalidInputType(tR.clone()))?; let ctx2 = ctx.insert(f.clone(), tR.clone()); - let tB = normalized_type_with(&ctx2, b.clone())?; - let ttB = normalized_type_with(ctx, tB.clone())?; + let tB = type_with(&ctx2, b.clone())?; + let ttB = type_with(ctx, tB.clone())?; // Don't bother to provide a `let`-specific version of this error // message because this should never happen anyway let kB = ensure_const(&ttB, InvalidOutputType(tB.clone()))?; @@ -298,9 +294,9 @@ where } Annot(x, t) => { // This is mainly just to check that `t` is not `Kind` - let _ = normalized_type_with(ctx, t.clone())?; + let _ = type_with(ctx, t.clone())?; - let t2 = normalized_type_with(ctx, x.clone())?; + let t2 = type_with(ctx, x.clone())?; let t = normalize(t.clone()); if prop_equal(t.as_ref(), t2.as_ref()) { Ok(t.unroll()) @@ -309,22 +305,22 @@ where } } BoolIf(x, y, z) => { - let tx = normalized_type_with(ctx, x.clone())?; + let tx = type_with(ctx, x.clone())?; match tx.as_ref() { Builtin(Bool) => {} _ => { return Err(mkerr(InvalidPredicate(x.clone(), tx))); } } - let ty = normalized_type_with(ctx, y.clone())?; - let tty = normalized_type_with(ctx, ty.clone())?; + let ty = type_with(ctx, y.clone())?; + let tty = type_with(ctx, ty.clone())?; ensure_is_type( tty.clone(), IfBranchMustBeTerm(true, y.clone(), ty.clone(), tty.clone()), )?; - let tz = normalized_type_with(ctx, z.clone())?; - let ttz = normalized_type_with(ctx, tz.clone())?; + let tz = type_with(ctx, z.clone())?; + let ttz = type_with(ctx, tz.clone())?; ensure_is_type( ttz.clone(), IfBranchMustBeTerm(false, z.clone(), tz.clone(), ttz.clone()), @@ -341,7 +337,7 @@ where Ok(ty.unroll()) } EmptyListLit(t) => { - let s = normalized_type_with(ctx, t.clone())?; + let s = type_with(ctx, t.clone())?; ensure_is_type(s, InvalidListType(t.clone()))?; let t = normalize(SubExpr::clone(t)); Ok(dhall::expr!(List t)) @@ -349,11 +345,11 @@ where NEListLit(xs) => { let mut iter = xs.iter().enumerate(); let (_, first_x) = iter.next().unwrap(); - let t = normalized_type_with(ctx, first_x.clone())?; - let s = normalized_type_with(ctx, t.clone())?; + let t = type_with(ctx, first_x.clone())?; + let s = type_with(ctx, t.clone())?; ensure_is_type(s, InvalidListType(t.clone()))?; for (i, x) in iter { - let t2 = normalized_type_with(ctx, x.clone())?; + let t2 = type_with(ctx, x.clone())?; if !prop_equal(t.as_ref(), t2.as_ref()) { return Err(mkerr(InvalidListElement(i, t, x.clone(), t2))); } @@ -361,20 +357,20 @@ where Ok(dhall::expr!(List t)) } EmptyOptionalLit(t) => { - let s = normalized_type_with(ctx, t.clone())?; + let s = type_with(ctx, t.clone())?; ensure_is_type(s, InvalidOptionalType(t.clone()))?; let t = normalize(t.clone()); Ok(dhall::expr!(Optional t)) } NEOptionalLit(x) => { - let t = normalized_type_with(ctx, x.clone())?; - let s = normalized_type_with(ctx, t.clone())?; + let t = type_with(ctx, x.clone())?; + let s = type_with(ctx, t.clone())?; ensure_is_type(s, InvalidOptionalType(t.clone()))?; Ok(dhall::expr!(Optional t)) } RecordType(kts) => { for (k, t) in kts { - let s = normalized_type_with(ctx, t.clone())?; + let s = type_with(ctx, t.clone())?; ensure_is_type(s, InvalidFieldType(k.clone(), t.clone()))?; } Ok(Const(Type)) @@ -383,8 +379,8 @@ where let kts = kvs .iter() .map(|(k, v)| { - let t = normalized_type_with(ctx, v.clone())?; - let s = normalized_type_with(ctx, t.clone())?; + let t = type_with(ctx, v.clone())?; + let s = type_with(ctx, t.clone())?; ensure_is_type(s, InvalidField(k.clone(), v.clone()))?; Ok((k.clone(), t)) }) @@ -392,7 +388,7 @@ where Ok(RecordType(kts)) } Field(r, x) => { - let t = normalized_type_with(ctx, r.clone())?; + let t = type_with(ctx, r.clone())?; match t.as_ref() { RecordType(kts) => match kts.get(x) { Some(e) => Ok(e.unroll()), @@ -418,13 +414,13 @@ where TextAppend => Text, _ => panic!("Unimplemented typecheck case: {:?}", e), }; - let tl = normalized_type_with(ctx, l.clone())?; + let tl = type_with(ctx, l.clone())?; match tl.as_ref() { Builtin(lt) if *lt == t => {} _ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone(), tl))), } - let tr = normalized_type_with(ctx, r.clone())?; + let tr = type_with(ctx, r.clone())?; match tr.as_ref() { Builtin(rt) if *rt == t => {} _ => return Err(mkerr(BinOpTypeMismatch(*o, r.clone(), tr))), @@ -435,17 +431,7 @@ where Embed(p) => match *p {}, _ => panic!("Unimplemented typecheck case: {:?}", e), }?; - Ok(rc(ret)) -} - -pub fn normalized_type_with( - ctx: &Context>, - e: SubExpr, -) -> Result, TypeError> -where - S: ::std::fmt::Debug + Clone, -{ - Ok(normalize(type_with(ctx, e)?)) + Ok(normalize(rc(ret))) } /// `typeOf` is the same as `type_with` with an empty context, meaning that the @@ -455,7 +441,7 @@ pub fn type_of( e: SubExpr, ) -> Result, TypeError> { let ctx = Context::new(); - normalized_type_with(&ctx, e) //.map(|e| e.into_owned()) + type_with(&ctx, e) //.map(|e| e.into_owned()) } /// The specific type error -- cgit v1.2.3 From e0d16abfbd4ecc080dab960b531b749bd72c68e6 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 12:39:07 +0200 Subject: Normalize only as needed while typechecking --- dhall/src/typecheck.rs | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index e5b81bd..ff656f8 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -176,12 +176,11 @@ fn type_of_builtin(b: Builtin) -> Expr { } } -/// Type-check an expression and return the expression'i type if type-checking -/// suceeds or an error if type-checking fails +/// Type-check an expression and return the expression's type if type-checking +/// succeeds or an error if type-checking fails /// -/// `type_with` does not necessarily normalize the type since full normalization -/// is not necessary for just type-checking. If you actually care about the -/// returned type then you may want to `normalize` it afterwards. +/// `type_with` normalizes the type since while type-checking. It expects the +/// context to contain only normalized expressions. pub fn type_with( ctx: &Context>, e: SubExpr, @@ -211,18 +210,19 @@ where Some(e) => Ok(e.unroll()), None => Err(mkerr(UnboundVariable)), }, - Lam(x, tA, b) => { + Lam(x, t, b) => { + let t2 = normalize(SubExpr::clone(t)); let ctx2 = ctx - .insert(x.clone(), tA.clone()) + .insert(x.clone(), t2.clone()) .map(|e| shift(1, &V(x.clone(), 0), e)); let tB = type_with(&ctx2, b.clone())?; - let p = Pi(x.clone(), tA.clone(), tB); - let _ = type_with(ctx, rc(p.clone()))?; - Ok(p) + let _ = type_with(ctx, rc(Pi(x.clone(), t.clone(), tB.clone())))?; + Ok(Pi(x.clone(), t2, tB)) } Pi(x, tA, tB) => { - let tA2 = type_with(ctx, tA.clone())?; - let kA = ensure_const(&tA2, InvalidInputType(tA.clone()))?; + let ttA = type_with(ctx, tA.clone())?; + let tA = normalize(SubExpr::clone(tA)); + let kA = ensure_const(&ttA, InvalidInputType(tA.clone()))?; let ctx2 = ctx .insert(x.clone(), tA.clone()) @@ -261,7 +261,7 @@ where let tA2 = type_with(ctx, a.clone())?; if prop_equal(tA.as_ref(), tA2.as_ref()) { let vx0 = &V(x.clone(), 0); - Ok(subst_shift(vx0, &a, &tB).unroll()) + Ok(normalize(subst_shift(vx0, &a, &tB)).unroll()) } else { Err(mkerr(TypeMismatch(f.clone(), tA.clone(), a.clone(), tA2))) } @@ -296,12 +296,12 @@ where // This is mainly just to check that `t` is not `Kind` let _ = type_with(ctx, t.clone())?; - let t2 = type_with(ctx, x.clone())?; + let tx = type_with(ctx, x.clone())?; let t = normalize(t.clone()); - if prop_equal(t.as_ref(), t2.as_ref()) { + if prop_equal(t.as_ref(), tx.as_ref()) { Ok(t.unroll()) } else { - Err(mkerr(AnnotMismatch(x.clone(), t, t2))) + Err(mkerr(AnnotMismatch(x.clone(), t, tx))) } } BoolIf(x, y, z) => { @@ -431,7 +431,7 @@ where Embed(p) => match *p {}, _ => panic!("Unimplemented typecheck case: {:?}", e), }?; - Ok(normalize(rc(ret))) + Ok(rc(ret)) } /// `typeOf` is the same as `type_with` with an empty context, meaning that the -- cgit v1.2.3 From f20aa69322394e648ebd0556a5862b6211c1061c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 13:49:49 +0200 Subject: Factor out the recursion when possible in typecheck --- dhall/src/typecheck.rs | 256 +++++++++++++++++++++++++------------------------ 1 file changed, 131 insertions(+), 125 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index ff656f8..8c911fb 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -292,144 +292,150 @@ where Ok(tB.unroll()) } - Annot(x, t) => { - // This is mainly just to check that `t` is not `Kind` - let _ = type_with(ctx, t.clone())?; - - let tx = type_with(ctx, x.clone())?; - let t = normalize(t.clone()); - if prop_equal(t.as_ref(), tx.as_ref()) { - Ok(t.unroll()) - } else { - Err(mkerr(AnnotMismatch(x.clone(), t, tx))) - } - } - BoolIf(x, y, z) => { - let tx = type_with(ctx, x.clone())?; - match tx.as_ref() { - Builtin(Bool) => {} - _ => { - return Err(mkerr(InvalidPredicate(x.clone(), tx))); + _ => match e + .as_ref() + .traverse_ref_simple(|e| Ok((e, type_with(ctx, e.clone())?)))? + { + Annot((x, tx), (t, _)) => { + let t = normalize(t.clone()); + if prop_equal(t.as_ref(), tx.as_ref()) { + Ok(t.unroll()) + } else { + Err(mkerr(AnnotMismatch(x.clone(), t, tx))) } } - let ty = type_with(ctx, y.clone())?; - let tty = type_with(ctx, ty.clone())?; - ensure_is_type( - tty.clone(), - IfBranchMustBeTerm(true, y.clone(), ty.clone(), tty.clone()), - )?; + BoolIf((x, tx), (y, ty), (z, tz)) => { + match tx.as_ref() { + Builtin(Bool) => {} + _ => { + return Err(mkerr(InvalidPredicate(x.clone(), tx))); + } + } + let tty = type_with(ctx, ty.clone())?; + ensure_is_type( + tty.clone(), + IfBranchMustBeTerm( + true, + y.clone(), + ty.clone(), + tty.clone(), + ), + )?; - let tz = type_with(ctx, z.clone())?; - let ttz = type_with(ctx, tz.clone())?; - ensure_is_type( - ttz.clone(), - IfBranchMustBeTerm(false, z.clone(), tz.clone(), ttz.clone()), - )?; + let ttz = type_with(ctx, tz.clone())?; + ensure_is_type( + ttz.clone(), + IfBranchMustBeTerm( + false, + z.clone(), + tz.clone(), + ttz.clone(), + ), + )?; - if !prop_equal(ty.as_ref(), tz.as_ref()) { - return Err(mkerr(IfBranchMismatch( - y.clone(), - z.clone(), - ty, - tz, - ))); + if !prop_equal(ty.as_ref(), tz.as_ref()) { + return Err(mkerr(IfBranchMismatch( + y.clone(), + z.clone(), + ty, + tz, + ))); + } + Ok(ty.unroll()) } - Ok(ty.unroll()) - } - EmptyListLit(t) => { - let s = type_with(ctx, t.clone())?; - ensure_is_type(s, InvalidListType(t.clone()))?; - let t = normalize(SubExpr::clone(t)); - Ok(dhall::expr!(List t)) - } - NEListLit(xs) => { - let mut iter = xs.iter().enumerate(); - let (_, first_x) = iter.next().unwrap(); - let t = type_with(ctx, first_x.clone())?; - let s = type_with(ctx, t.clone())?; - ensure_is_type(s, InvalidListType(t.clone()))?; - for (i, x) in iter { - let t2 = type_with(ctx, x.clone())?; - if !prop_equal(t.as_ref(), t2.as_ref()) { - return Err(mkerr(InvalidListElement(i, t, x.clone(), t2))); + EmptyListLit((t, tt)) => { + ensure_is_type(tt, InvalidListType(t.clone()))?; + let t = normalize(SubExpr::clone(t)); + Ok(dhall::expr!(List t)) + } + NEListLit(xs) => { + let mut iter = xs.into_iter().enumerate(); + let (_, (_, t)) = iter.next().unwrap(); + let s = type_with(ctx, t.clone())?; + ensure_is_type(s, InvalidListType(t.clone()))?; + for (i, (y, ty)) in iter { + if !prop_equal(t.as_ref(), ty.as_ref()) { + return Err(mkerr(InvalidListElement( + i, + t, + y.clone(), + ty, + ))); + } } + Ok(dhall::expr!(List t)) } - Ok(dhall::expr!(List t)) - } - EmptyOptionalLit(t) => { - let s = type_with(ctx, t.clone())?; - ensure_is_type(s, InvalidOptionalType(t.clone()))?; - let t = normalize(t.clone()); - Ok(dhall::expr!(Optional t)) - } - NEOptionalLit(x) => { - let t = type_with(ctx, x.clone())?; - let s = type_with(ctx, t.clone())?; - ensure_is_type(s, InvalidOptionalType(t.clone()))?; - Ok(dhall::expr!(Optional t)) - } - RecordType(kts) => { - for (k, t) in kts { + EmptyOptionalLit((t, tt)) => { + ensure_is_type(tt, InvalidOptionalType(t.clone()))?; + let t = normalize(t.clone()); + Ok(dhall::expr!(Optional t)) + } + NEOptionalLit((_, t)) => { let s = type_with(ctx, t.clone())?; - ensure_is_type(s, InvalidFieldType(k.clone(), t.clone()))?; + ensure_is_type(s, InvalidOptionalType(t.clone()))?; + Ok(dhall::expr!(Optional t)) } - Ok(Const(Type)) - } - RecordLit(kvs) => { - let kts = kvs - .iter() - .map(|(k, v)| { - let t = type_with(ctx, v.clone())?; - let s = type_with(ctx, t.clone())?; - ensure_is_type(s, InvalidField(k.clone(), v.clone()))?; - Ok((k.clone(), t)) - }) - .collect::>()?; - Ok(RecordType(kts)) - } - Field(r, x) => { - let t = type_with(ctx, r.clone())?; - match t.as_ref() { - RecordType(kts) => match kts.get(x) { - Some(e) => Ok(e.unroll()), - None => Err(mkerr(MissingField(x.clone(), t.clone()))), - }, - _ => Err(mkerr(NotARecord(x.clone(), r.clone(), t.clone()))), + RecordType(kts) => { + for (k, (t, tt)) in kts { + ensure_is_type(tt, InvalidFieldType(k.clone(), t.clone()))?; + } + Ok(Const(Type)) } - } - Builtin(b) => Ok(type_of_builtin(*b)), - BoolLit(_) => Ok(Builtin(Bool)), - NaturalLit(_) => Ok(Builtin(Natural)), - IntegerLit(_) => Ok(Builtin(Integer)), - DoubleLit(_) => Ok(Builtin(Double)), - TextLit(_) => Ok(Builtin(Text)), - BinOp(o, l, r) => { - let t = match o { - BoolAnd => Bool, - BoolOr => Bool, - BoolEQ => Bool, - BoolNE => Bool, - NaturalPlus => Natural, - NaturalTimes => Natural, - TextAppend => Text, - _ => panic!("Unimplemented typecheck case: {:?}", e), - }; - let tl = type_with(ctx, l.clone())?; - match tl.as_ref() { - Builtin(lt) if *lt == t => {} - _ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone(), tl))), + RecordLit(kvs) => { + let kts = kvs + .into_iter() + .map(|(k, (v, t))| { + let s = type_with(ctx, t.clone())?; + ensure_is_type(s, InvalidField(k.clone(), v.clone()))?; + Ok((k.clone(), t)) + }) + .collect::>()?; + Ok(RecordType(kts)) } + Field((r, tr), x) => match tr.as_ref() { + RecordType(kts) => match kts.get(&x) { + Some(e) => Ok(e.unroll()), + None => Err(mkerr(MissingField(x.clone(), tr.clone()))), + }, + _ => Err(mkerr(NotARecord(x.clone(), r.clone(), tr.clone()))), + }, + Builtin(b) => Ok(type_of_builtin(b)), + BoolLit(_) => Ok(Builtin(Bool)), + NaturalLit(_) => Ok(Builtin(Natural)), + IntegerLit(_) => Ok(Builtin(Integer)), + DoubleLit(_) => Ok(Builtin(Double)), + // TODO: check type of interpolations + TextLit(_) => Ok(Builtin(Text)), + BinOp(o, (l, tl), (r, tr)) => { + let t = match o { + BoolAnd => Bool, + BoolOr => Bool, + BoolEQ => Bool, + BoolNE => Bool, + NaturalPlus => Natural, + NaturalTimes => Natural, + TextAppend => Text, + _ => panic!("Unimplemented typecheck case: {:?}", e), + }; + match tl.as_ref() { + Builtin(lt) if *lt == t => {} + _ => { + return Err(mkerr(BinOpTypeMismatch(o, l.clone(), tl))) + } + } - let tr = type_with(ctx, r.clone())?; - match tr.as_ref() { - Builtin(rt) if *rt == t => {} - _ => return Err(mkerr(BinOpTypeMismatch(*o, r.clone(), tr))), - } + match tr.as_ref() { + Builtin(rt) if *rt == t => {} + _ => { + return Err(mkerr(BinOpTypeMismatch(o, r.clone(), tr))) + } + } - Ok(Builtin(t)) - } - Embed(p) => match *p {}, - _ => panic!("Unimplemented typecheck case: {:?}", e), + Ok(Builtin(t)) + } + Embed(p) => match p {}, + _ => panic!("Unimplemented typecheck case: {:?}", e), + }, }?; Ok(rc(ret)) } -- cgit v1.2.3 From 02698056218c53635582001c5517c570f122f94d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 14:15:48 +0200 Subject: Loop through args when typechecking App --- dhall/src/typecheck.rs | 41 ++++++++++++++++++++++++----------------- 1 file changed, 24 insertions(+), 17 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 8c911fb..e21669d 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -245,26 +245,33 @@ where } } App(f, args) => { - // Recurse on args - let (a, tf) = match args.split_last() { - None => return type_with(ctx, f.clone()), - Some((a, args)) => { - (a, type_with(ctx, rc(App(f.clone(), args.to_vec())))?) - } - }; - let (x, tA, tB) = match tf.as_ref() { - Pi(x, tA, tB) => (x, tA, tB), - _ => { - return Err(mkerr(NotAFunction(f.clone(), tf))); + let mut iter = args.iter().cloned(); + let mut tf: SubExpr<_, _> = type_with(ctx, f.clone())?; + let mut seen_args: Vec> = vec![]; + while let Some(a) = iter.next() { + seen_args.push(a.clone()); + let (x, tA, tB) = match tf.as_ref() { + Pi(x, tA, tB) => (x, tA, tB), + _ => { + return Err(mkerr(NotAFunction( + rc(App(f.clone(), seen_args)), + tf, + ))); + } + }; + let tA2 = type_with(ctx, a.clone())?; + if !prop_equal(tA.as_ref(), tA2.as_ref()) { + return Err(mkerr(TypeMismatch( + rc(App(f.clone(), seen_args)), + tA.clone(), + a.clone(), + tA2, + ))); } - }; - let tA2 = type_with(ctx, a.clone())?; - if prop_equal(tA.as_ref(), tA2.as_ref()) { let vx0 = &V(x.clone(), 0); - Ok(normalize(subst_shift(vx0, &a, &tB)).unroll()) - } else { - Err(mkerr(TypeMismatch(f.clone(), tA.clone(), a.clone(), tA2))) + tf = normalize(subst_shift(vx0, &a, &tB)); } + Ok(tf.unroll()) } Let(f, mt, r, b) => { let r = if let Some(t) = mt { -- cgit v1.2.3 From 615797412fabf60b9dd7464f9bc1668dd859ea53 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 14:28:59 +0200 Subject: Move more cases after recursion --- dhall/src/typecheck.rs | 68 +++++++++++++++++++++++++------------------------- 1 file changed, 34 insertions(+), 34 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index e21669d..08e5928 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -205,11 +205,6 @@ where }; let ret = match e.as_ref() { - Const(c) => axiom(*c).map(Const), - Var(V(x, n)) => match ctx.lookup(x, *n) { - Some(e) => Ok(e.unroll()), - None => Err(mkerr(UnboundVariable)), - }, Lam(x, t, b) => { let t2 = normalize(SubExpr::clone(t)); let ctx2 = ctx @@ -244,35 +239,6 @@ where Ok(_) => Ok(Const(kB)), } } - App(f, args) => { - let mut iter = args.iter().cloned(); - let mut tf: SubExpr<_, _> = type_with(ctx, f.clone())?; - let mut seen_args: Vec> = vec![]; - while let Some(a) = iter.next() { - seen_args.push(a.clone()); - let (x, tA, tB) = match tf.as_ref() { - Pi(x, tA, tB) => (x, tA, tB), - _ => { - return Err(mkerr(NotAFunction( - rc(App(f.clone(), seen_args)), - tf, - ))); - } - }; - let tA2 = type_with(ctx, a.clone())?; - if !prop_equal(tA.as_ref(), tA2.as_ref()) { - return Err(mkerr(TypeMismatch( - rc(App(f.clone(), seen_args)), - tA.clone(), - a.clone(), - tA2, - ))); - } - let vx0 = &V(x.clone(), 0); - tf = normalize(subst_shift(vx0, &a, &tB)); - } - Ok(tf.unroll()) - } Let(f, mt, r, b) => { let r = if let Some(t) = mt { rc(Annot(SubExpr::clone(r), SubExpr::clone(t))) @@ -303,6 +269,40 @@ where .as_ref() .traverse_ref_simple(|e| Ok((e, type_with(ctx, e.clone())?)))? { + Lam(_, _, _) => unreachable!(), + Pi(_, _, _) => unreachable!(), + Let(_, _, _, _) => unreachable!(), + Const(c) => axiom(c).map(Const), + Var(V(x, n)) => match ctx.lookup(&x, n) { + Some(e) => Ok(e.unroll()), + None => Err(mkerr(UnboundVariable)), + }, + App((f, mut tf), args) => { + let mut iter = args.into_iter(); + let mut seen_args: Vec> = vec![]; + while let Some((a, ta)) = iter.next() { + seen_args.push(a.clone()); + let (x, tx, tb) = match tf.as_ref() { + Pi(x, tx, tb) => (x, tx, tb), + _ => { + return Err(mkerr(NotAFunction( + rc(App(f.clone(), seen_args)), + tf, + ))); + } + }; + if !prop_equal(tx.as_ref(), ta.as_ref()) { + return Err(mkerr(TypeMismatch( + rc(App(f.clone(), seen_args)), + tx.clone(), + a.clone(), + ta, + ))); + } + tf = normalize(subst_shift(&V(x.clone(), 0), &a, &tb)); + } + Ok(tf.unroll()) + } Annot((x, tx), (t, _)) => { let t = normalize(t.clone()); if prop_equal(t.as_ref(), tx.as_ref()) { -- cgit v1.2.3 From be3f8b2c5327428a0aafbefd024f2a66fb122037 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 6 Apr 2019 16:38:51 +0200 Subject: Factor out type equality checking --- dhall/src/typecheck.rs | 96 ++++++++++++++++++++++++++------------------------ 1 file changed, 50 insertions(+), 46 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 08e5928..e63b032 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -176,6 +176,24 @@ fn type_of_builtin(b: Builtin) -> Expr { } } +fn ensure_equal<'a, S, F1, F2>( + x: &'a Expr, + y: &'a Expr, + mkerr: F1, + mkmsg: F2, +) -> Result<(), TypeError> +where + S: std::fmt::Debug, + F1: FnOnce(TypeMessage) -> TypeError, + F2: FnOnce() -> TypeMessage, +{ + if prop_equal(x, y) { + Ok(()) + } else { + Err(mkerr(mkmsg())) + } +} + /// Type-check an expression and return the expression's type if type-checking /// succeeds or an error if type-checking fails /// @@ -291,33 +309,29 @@ where ))); } }; - if !prop_equal(tx.as_ref(), ta.as_ref()) { - return Err(mkerr(TypeMismatch( - rc(App(f.clone(), seen_args)), + ensure_equal(tx.as_ref(), ta.as_ref(), mkerr, || { + TypeMismatch( + rc(App(f.clone(), seen_args.clone())), tx.clone(), a.clone(), - ta, - ))); - } + ta.clone(), + ) + })?; tf = normalize(subst_shift(&V(x.clone(), 0), &a, &tb)); } Ok(tf.unroll()) } Annot((x, tx), (t, _)) => { let t = normalize(t.clone()); - if prop_equal(t.as_ref(), tx.as_ref()) { - Ok(t.unroll()) - } else { - Err(mkerr(AnnotMismatch(x.clone(), t, tx))) - } + ensure_equal(t.as_ref(), tx.as_ref(), mkerr, || { + AnnotMismatch(x.clone(), t.clone(), tx.clone()) + })?; + Ok(t.unroll()) } BoolIf((x, tx), (y, ty), (z, tz)) => { - match tx.as_ref() { - Builtin(Bool) => {} - _ => { - return Err(mkerr(InvalidPredicate(x.clone(), tx))); - } - } + ensure_equal(tx.as_ref(), &Builtin(Bool), mkerr, || { + InvalidPredicate(x.clone(), tx.clone()) + })?; let tty = type_with(ctx, ty.clone())?; ensure_is_type( tty.clone(), @@ -340,14 +354,14 @@ where ), )?; - if !prop_equal(ty.as_ref(), tz.as_ref()) { - return Err(mkerr(IfBranchMismatch( + ensure_equal(ty.as_ref(), tz.as_ref(), mkerr, || { + IfBranchMismatch( y.clone(), z.clone(), - ty, - tz, - ))); - } + ty.clone(), + tz.clone(), + ) + })?; Ok(ty.unroll()) } EmptyListLit((t, tt)) => { @@ -361,14 +375,9 @@ where let s = type_with(ctx, t.clone())?; ensure_is_type(s, InvalidListType(t.clone()))?; for (i, (y, ty)) in iter { - if !prop_equal(t.as_ref(), ty.as_ref()) { - return Err(mkerr(InvalidListElement( - i, - t, - y.clone(), - ty, - ))); - } + ensure_equal(t.as_ref(), ty.as_ref(), mkerr, || { + InvalidListElement(i, t.clone(), y.clone(), ty.clone()) + })?; } Ok(dhall::expr!(List t)) } @@ -414,7 +423,7 @@ where // TODO: check type of interpolations TextLit(_) => Ok(Builtin(Text)), BinOp(o, (l, tl), (r, tr)) => { - let t = match o { + let t = Builtin(match o { BoolAnd => Bool, BoolOr => Bool, BoolEQ => Bool, @@ -423,22 +432,17 @@ where NaturalTimes => Natural, TextAppend => Text, _ => panic!("Unimplemented typecheck case: {:?}", e), - }; - match tl.as_ref() { - Builtin(lt) if *lt == t => {} - _ => { - return Err(mkerr(BinOpTypeMismatch(o, l.clone(), tl))) - } - } + }); - match tr.as_ref() { - Builtin(rt) if *rt == t => {} - _ => { - return Err(mkerr(BinOpTypeMismatch(o, r.clone(), tr))) - } - } + ensure_equal(tl.as_ref(), &t, mkerr, || { + BinOpTypeMismatch(o, l.clone(), tl.clone()) + })?; + + ensure_equal(tr.as_ref(), &t, mkerr, || { + BinOpTypeMismatch(o, r.clone(), tr.clone()) + })?; - Ok(Builtin(t)) + Ok(t) } Embed(p) => match p {}, _ => panic!("Unimplemented typecheck case: {:?}", e), -- cgit v1.2.3