summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-04-23 17:16:29 +0200
committerNadrieril2019-04-23 17:16:29 +0200
commita97ebd37169193c6392658aa8b022c7e0f8c4a34 (patch)
tree8764f6375d2164e061e0f1b7f04e27a6537b7ab1
parent2f1fa26abd9c9f2b75d24b18877d3b278f7d2a01 (diff)
Avoid constructing ExprF::Pi while typechecking
-rw-r--r--dhall/src/typecheck.rs150
1 files changed, 93 insertions, 57 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 38b3d68..c23794f 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -222,18 +222,6 @@ impl TypedImproved {
) -> Result<Type<'static>, TypeError> {
match self {
TypedImproved::Expr(e) => Ok(e.normalize_to_type(ctx)?),
- // TypedImproved::Pi(ctx, c, x, t, e) => Ok(Typed(
- // rc(ExprF::Pi(
- // x,
- // t.into_normalized()?.embed(),
- // e.into_normalized()?.embed(),
- // )),
- // Some(const_to_type(c)),
- // ctx,
- // PhantomData,
- // )
- // .normalize()
- // .into_type()?),
TypedImproved::Pi(ctx, c, x, t, e) => {
Ok(Type(TypeInternal::Pi(ctx, c, x, Box::new(t), Box::new(e))))
}
@@ -527,6 +515,78 @@ macro_rules! ensure_is_const {
};
}
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) enum TypeIntermediate {
+ Pi(TypecheckContext, Label, Type<'static>, Type<'static>),
+}
+
+impl TypeIntermediate {
+ fn typecheck(self) -> Result<TypedImproved, TypeError> {
+ match &self {
+ TypeIntermediate::Pi(ctx, x, ta, tb) => {
+ let ctx2 = ctx.insert_type(x, ta.clone());
+
+ let kA = ensure_is_const!(
+ &ta.get_type()?,
+ TypeError::new(
+ ctx,
+ self.clone().into_expr()?,
+ InvalidInputType(ta.clone().into_normalized()?),
+ ),
+ );
+
+ let kB = ensure_is_const!(
+ &tb.get_type()?,
+ TypeError::new(
+ &ctx2,
+ self.clone().into_expr()?,
+ InvalidOutputType(
+ tb.clone()
+ .into_normalized()?
+ .get_type_move()?
+ .into_normalized()?
+ ),
+ ),
+ );
+
+ let k = match function_check(kA, kB) {
+ Ok(k) => k,
+ Err(()) => {
+ return Err(TypeError::new(
+ ctx,
+ self.clone().into_expr()?,
+ NoDependentTypes(
+ ta.clone().into_normalized()?,
+ tb.clone()
+ .into_normalized()?
+ .get_type_move()?
+ .into_normalized()?,
+ ),
+ ))
+ }
+ };
+
+ Ok(TypedImproved::Pi(
+ ctx.clone(),
+ k,
+ x.clone(),
+ ta.clone(),
+ tb.clone(),
+ ))
+ }
+ }
+ }
+ fn into_expr(self) -> Result<SubExpr<X, Normalized<'static>>, TypeError> {
+ match self {
+ TypeIntermediate::Pi(_, x, t, e) => Ok(rc(ExprF::Pi(
+ x,
+ t.into_normalized()?.embed(),
+ e.into_normalized()?.embed(),
+ ))),
+ }
+ }
+}
+
/// Takes an expression that is meant to contain a Type
/// and turn it into a type, typechecking it along the way.
fn mktype(
@@ -565,51 +625,22 @@ fn type_with(
use Ret::*;
let ret = match e.as_ref() {
Lam(x, t, b) => {
- let t = mktype(ctx, t.clone())?;
- let ctx2 = ctx.insert_type(x, t.clone());
+ let tx = mktype(ctx, t.clone())?;
+ let ctx2 = ctx.insert_type(x, tx.clone());
let b = type_with(&ctx2, b.clone())?.into_typed()?;
- Ok(RetExpr(Pi(
- x.clone(),
- t.embed()?,
- b.get_type_move()?.embed()?,
- )))
+ let tb = b.get_type_move()?;
+ Ok(RetType(
+ TypeIntermediate::Pi(ctx.clone(), x.clone(), tx, tb)
+ .typecheck()?
+ .normalize_to_type(ctx)?,
+ ))
}
Pi(x, ta, tb) => {
let ta = mktype(ctx, ta.clone())?;
- let kA = ensure_is_const!(
- &ta.get_type()?,
- mkerr(InvalidInputType(ta.into_normalized()?)),
- );
-
let ctx2 = ctx.insert_type(x, ta.clone());
let tb = mktype(&ctx2, tb.clone())?;
- let kB = ensure_is_const!(
- &tb.get_type()?,
- TypeError::new(
- &ctx2,
- e.clone(),
- InvalidOutputType(
- tb.into_normalized()?
- .get_type_move()?
- .into_normalized()?
- ),
- ),
- );
-
- let k = match function_check(kA, kB) {
- Ok(k) => k,
- Err(()) => {
- return Err(mkerr(NoDependentTypes(
- ta.clone().into_normalized()?,
- tb.into_normalized()?
- .get_type_move()?
- .into_normalized()?,
- )))
- }
- };
-
- return Ok(TypedImproved::Pi(ctx.clone(), k, x.clone(), ta, tb));
- // Ok(RetExpr(Const(k)))
+ return TypeIntermediate::Pi(ctx.clone(), x.clone(), ta, tb)
+ .typecheck();
}
Let(x, t, v, e) => {
let v = if let Some(t) = t {
@@ -857,12 +888,17 @@ fn type_last_layer(
match r.as_normalized()?.as_expr().as_ref() {
UnionType(kts) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
- // TODO: use "_" instead of x
- Some(Some(t)) => Ok(RetExpr(Pi(
- x.clone(),
- t.embed_absurd(),
- r.into_normalized()?.embed(),
- ))),
+ // TODO: use "_" instead of x (i.e. compare types using equivalence)
+ Some(Some(t)) => Ok(RetType(
+ TypeIntermediate::Pi(
+ ctx.clone(),
+ x.clone(),
+ mktype(ctx, t.embed_absurd())?,
+ r,
+ )
+ .typecheck()?
+ .normalize_to_type(ctx)?,
+ )),
Some(None) => Ok(RetType(r)),
None => Err(mkerr(MissingUnionField(
x,