summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-05-07 20:30:05 +0200
committerNadrieril2019-05-07 20:30:05 +0200
commit372c78ab875c8aa1e967ffb594f26df8beb43bea (patch)
treea2e6a7d0a7a59c9c1102e347ea684f5335a2d6ba
parent833cb91cec6ae708e17a0f9589eba9560e81bd07 (diff)
Slight improvement to typecheck ergonomics
-rw-r--r--dhall/src/phase/typecheck.rs87
1 files changed, 28 insertions, 59 deletions
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index bfe85b9..b163af6 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -35,19 +35,19 @@ macro_rules! ensure_simple_type {
#[derive(Debug, Clone, PartialEq, Eq)]
pub(crate) enum TypeIntermediate {
- Pi(TypecheckContext, Label, Type, Type),
- RecordType(TypecheckContext, BTreeMap<Label, Type>),
- UnionType(TypecheckContext, BTreeMap<Label, Option<Type>>),
- ListType(TypecheckContext, Type),
- OptionalType(TypecheckContext, Type),
+ Pi(Label, Type, Type),
+ RecordType(BTreeMap<Label, Type>),
+ UnionType(BTreeMap<Label, Option<Type>>),
+ ListType(Type),
+ OptionalType(Type),
}
impl TypeIntermediate {
- fn typecheck(self) -> Result<Typed, TypeError> {
+ fn typecheck(self, ctx: &TypecheckContext) -> Result<Typed, TypeError> {
use crate::error::TypeMessage::*;
- let mkerr = |ctx, msg| TypeError::new(ctx, msg);
+ let mkerr = |ctx: &TypecheckContext, msg| TypeError::new(ctx, msg);
Ok(match &self {
- TypeIntermediate::Pi(ctx, x, ta, tb) => {
+ TypeIntermediate::Pi(x, ta, tb) => {
let ctx2 = ctx.insert_type(x, ta.clone());
let kA = match ta.get_type()?.as_const() {
@@ -101,7 +101,7 @@ impl TypeIntermediate {
Type::from_const(k),
)
}
- TypeIntermediate::RecordType(ctx, kts) => {
+ TypeIntermediate::RecordType(kts) => {
// Check that all types are the same const
let mut k = None;
for (x, t) in kts {
@@ -131,7 +131,7 @@ impl TypeIntermediate {
Type::from_const(k),
)
}
- TypeIntermediate::UnionType(ctx, kts) => {
+ TypeIntermediate::UnionType(kts) => {
// Check that all types are the same const
let mut k = None;
for (x, t) in kts {
@@ -170,7 +170,7 @@ impl TypeIntermediate {
Type::from_const(k),
)
}
- TypeIntermediate::ListType(ctx, t) => {
+ TypeIntermediate::ListType(t) => {
ensure_simple_type!(
t,
mkerr(ctx, InvalidListType(t.clone().to_normalized())),
@@ -182,7 +182,7 @@ impl TypeIntermediate {
Type::from_const(Const::Type),
)
}
- TypeIntermediate::OptionalType(ctx, t) => {
+ TypeIntermediate::OptionalType(t) => {
ensure_simple_type!(
t,
mkerr(ctx, InvalidOptionalType(t.clone().to_normalized())),
@@ -337,6 +337,7 @@ enum Ret {
RetTyped(Typed),
/// Use the contained Type as the type of the input expression
RetType(Type),
+ RetTypeIntermediate(TypeIntermediate),
}
/// Type-check an expression and return the expression alongside its type if type-checking
@@ -356,20 +357,13 @@ fn type_with(
let ctx2 = ctx.insert_type(x, tx.clone());
let b = type_with(&ctx2, b.clone())?;
let tb = b.get_type()?.into_owned();
- Ok(RetType(
- TypeIntermediate::Pi(ctx.clone(), x.clone(), tx, tb)
- .typecheck()?
- .to_type(),
- ))
+ Ok(RetTypeIntermediate(TypeIntermediate::Pi(x.clone(), tx, tb)))
}
Pi(x, ta, tb) => {
let ta = mktype(ctx, ta.clone())?;
let ctx2 = ctx.insert_type(x, ta.clone());
let tb = mktype(&ctx2, tb.clone())?;
- Ok(RetTyped(
- TypeIntermediate::Pi(ctx.clone(), x.clone(), ta, tb)
- .typecheck()?,
- ))
+ return TypeIntermediate::Pi(x.clone(), ta, tb).typecheck(ctx);
}
Let(x, t, v, e) => {
let v = if let Some(t) = t {
@@ -379,9 +373,7 @@ fn type_with(
};
let v = type_with(ctx, v)?;
- let e = type_with(&ctx.insert_value(x, v.clone())?, e.clone())?;
-
- Ok(RetType(e.get_type()?.into_owned()))
+ return type_with(&ctx.insert_value(x, v.clone())?, e.clone());
}
OldOptionalLit(None, t) => {
let none = SubExpr::from_expr_no_note(ExprF::Builtin(
@@ -411,6 +403,10 @@ fn type_with(
Thunk::new(ctx.to_normalization_ctx(), e),
typ,
),
+ RetTypeIntermediate(ti) => Typed::from_thunk_and_type(
+ Thunk::new(ctx.to_normalization_ctx(), e),
+ ti.typecheck(ctx)?.to_type(),
+ ),
RetTyped(tt) => tt,
})
}
@@ -493,11 +489,7 @@ fn type_last_layer(
}
EmptyListLit(t) => {
let t = t.to_type();
- Ok(RetType(
- TypeIntermediate::ListType(ctx.clone(), t)
- .typecheck()?
- .to_type(),
- ))
+ Ok(RetTypeIntermediate(TypeIntermediate::ListType(t)))
}
NEListLit(xs) => {
let mut iter = xs.into_iter().enumerate();
@@ -514,28 +506,18 @@ fn type_last_layer(
);
}
let t = x.get_type()?.into_owned();
- Ok(RetType(
- TypeIntermediate::ListType(ctx.clone(), t)
- .typecheck()?
- .to_type(),
- ))
+ Ok(RetTypeIntermediate(TypeIntermediate::ListType(t)))
}
SomeLit(x) => {
let t = x.get_type()?.into_owned();
- Ok(RetType(
- TypeIntermediate::OptionalType(ctx.clone(), t)
- .typecheck()?
- .to_type(),
- ))
+ Ok(RetTypeIntermediate(TypeIntermediate::OptionalType(t)))
}
RecordType(kts) => {
let kts: BTreeMap<_, _> = kts
.into_iter()
.map(|(x, t)| Ok((x, t.to_type())))
.collect::<Result<_, _>>()?;
- Ok(RetTyped(
- TypeIntermediate::RecordType(ctx.clone(), kts).typecheck()?,
- ))
+ Ok(RetTyped(TypeIntermediate::RecordType(kts).typecheck(ctx)?))
}
UnionType(kts) => {
let kts: BTreeMap<_, _> = kts
@@ -550,20 +532,14 @@ fn type_last_layer(
))
})
.collect::<Result<_, _>>()?;
- Ok(RetTyped(
- TypeIntermediate::UnionType(ctx.clone(), kts).typecheck()?,
- ))
+ Ok(RetTyped(TypeIntermediate::UnionType(kts).typecheck(ctx)?))
}
RecordLit(kvs) => {
let kts = kvs
.into_iter()
.map(|(x, v)| Ok((x, v.get_type()?.into_owned())))
.collect::<Result<_, _>>()?;
- Ok(RetType(
- TypeIntermediate::RecordType(ctx.clone(), kts)
- .typecheck()?
- .to_type(),
- ))
+ Ok(RetTypeIntermediate(TypeIntermediate::RecordType(kts)))
}
UnionLit(x, v, kvs) => {
let mut kts: std::collections::BTreeMap<_, _> = kvs
@@ -578,11 +554,7 @@ fn type_last_layer(
.collect::<Result<_, _>>()?;
let t = v.get_type()?.into_owned();
kts.insert(x, Some(t));
- Ok(RetType(
- TypeIntermediate::UnionType(ctx.clone(), kts)
- .typecheck()?
- .to_type(),
- ))
+ Ok(RetTypeIntermediate(TypeIntermediate::UnionType(kts)))
}
Field(r, x) => {
match &r.get_type()?.internal_whnf() {
@@ -599,15 +571,12 @@ fn type_last_layer(
Some(Value::UnionType(kts)) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
Some(Some(t)) => {
- Ok(RetType(
+ Ok(RetTypeIntermediate(
TypeIntermediate::Pi(
- ctx.clone(),
"_".into(),
t.to_type(ctx)?,
r.clone(),
)
- .typecheck()?
- .to_type(),
))
},
Some(None) => {