summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
authorNadrieril2019-04-25 14:24:15 +0200
committerNadrieril2019-04-25 14:24:15 +0200
commit1e499c4321e36938170a5b48d7f99fb8ee6cdc5b (patch)
tree39ad41a8b2cadc3348d6cddb02318a4077c842d2 /dhall/src
parent814c22dfe44a7ff896187cc87f212eb7de28a10a (diff)
normalize_to_type can use the captured context
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/typecheck.rs28
1 files changed, 14 insertions, 14 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index f006ec6..7fcf28e 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -69,7 +69,7 @@ impl<'a> Normalized<'a> {
Ok(match self.0.as_ref() {
ExprF::Const(c) => Type(TypeInternal::Const(*c)),
ExprF::Pi(_, _, _) => {
- type_with(ctx, self.0.embed_absurd())?.normalize_to_type(ctx)?
+ type_with(ctx, self.0.embed_absurd())?.normalize_to_type()?
}
_ => Type(TypeInternal::Expr(Box::new(self))),
})
@@ -230,12 +230,12 @@ impl TypedOrType {
TypedOrType::Type(t) => Ok(t.into_normalized()?.into()),
}
}
- fn normalize_to_type(
- self,
- ctx: &TypecheckContext,
- ) -> Result<Type<'static>, TypeError> {
+ fn normalize_to_type(self) -> Result<Type<'static>, TypeError> {
match self {
- TypedOrType::Typed(e) => Ok(e.normalize().into_type_ctx(ctx)?),
+ TypedOrType::Typed(e) => {
+ let ctx = e.2.clone();
+ Ok(e.normalize().into_type_ctx(&ctx)?)
+ }
TypedOrType::Type(t) => Ok(t),
}
}
@@ -648,7 +648,7 @@ fn mktype(
ctx: &TypecheckContext,
e: SubExpr<X, Normalized<'static>>,
) -> Result<Type<'static>, TypeError> {
- Ok(type_with(ctx, e)?.normalize_to_type(ctx)?)
+ Ok(type_with(ctx, e)?.normalize_to_type()?)
}
fn into_simple_type<'a>(ctx: &TypecheckContext, e: SubExpr<X, X>) -> Type<'a> {
@@ -688,7 +688,7 @@ fn type_with(
Ok(RetType(
TypeIntermediate::Pi(ctx.clone(), x.clone(), tx, tb)
.typecheck()?
- .normalize_to_type(ctx)?,
+ .normalize_to_type()?,
))
}
Pi(x, ta, tb) => {
@@ -785,7 +785,7 @@ fn type_last_layer(
// )?))
}
Annot(x, t) => {
- let t = t.normalize_to_type(ctx)?;
+ let t = t.normalize_to_type()?;
ensure_equal!(
&t,
x.get_type()?,
@@ -819,7 +819,7 @@ fn type_last_layer(
Ok(RetType(y.get_type_move()?))
}
EmptyListLit(t) => {
- let t = t.normalize_to_type(ctx)?;
+ let t = t.normalize_to_type()?;
ensure_simple_type!(
t,
mkerr(InvalidListType(t.into_normalized()?)),
@@ -876,7 +876,7 @@ fn type_last_layer(
RecordType(kts) => {
let kts: BTreeMap<_, _> = kts
.into_iter()
- .map(|(x, t)| Ok((x, t.normalize_to_type(ctx)?)))
+ .map(|(x, t)| Ok((x, t.normalize_to_type()?)))
.collect::<Result<_, _>>()?;
Ok(RetTypedOrType(
TypeIntermediate::RecordType(ctx.clone(), kts).typecheck()?,
@@ -913,7 +913,7 @@ fn type_last_layer(
Ok(RetType(
TypeIntermediate::RecordType(ctx.clone(), kts)
.typecheck()?
- .normalize_to_type(ctx)?,
+ .normalize_to_type()?,
))
}
UnionLit(x, v, kvs) => {
@@ -942,7 +942,7 @@ fn type_last_layer(
None => Err(mkerr(MissingRecordField(x, r))),
},
_ => {
- let r = r.normalize_to_type(ctx)?;
+ let r = r.normalize_to_type()?;
match r.as_normalized()?.as_expr().as_ref() {
UnionType(kts) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
@@ -955,7 +955,7 @@ fn type_last_layer(
r,
)
.typecheck()?
- .normalize_to_type(ctx)?,
+ .normalize_to_type()?,
)),
Some(None) => Ok(RetType(r)),
None => Err(mkerr(MissingUnionField(