summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--dhall/src/typecheck.rs79
1 files changed, 38 insertions, 41 deletions
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::<S, T>(&mut ctx, eL0, eR0)
}
-fn type_of_builtin<S>(b: Builtin) -> SubExpr<S, X> {
+fn type_of_builtin<S>(b: Builtin) -> Expr<S, X> {
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<S>(b: Builtin) -> SubExpr<S, X> {
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<S>(b: Builtin) -> SubExpr<S, X> {
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<S>(