summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/expr.rs3
-rw-r--r--dhall/src/typecheck.rs104
2 files changed, 56 insertions, 51 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index a84b41d..cda1d8d 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -116,9 +116,6 @@ impl<'a> Normalized<'a> {
pub(crate) fn as_expr(&self) -> &SubExpr<X, X> {
&self.0
}
- pub(crate) fn into_expr<T>(self) -> SubExpr<X, T> {
- self.0.absurd()
- }
pub(crate) fn into_type(self) -> Type<'a> {
crate::expr::Type(TypeInternal::Expr(Box::new(self)))
}
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 5162f4f..86c5ebd 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -48,6 +48,11 @@ impl<'a> Normalized<'a> {
Normalized(shift(delta, var, &self.0), self.1.clone(), self.2)
}
}
+impl Normalized<'static> {
+ fn embed<N>(self) -> SubExpr<N, Normalized<'static>> {
+ rc(ExprF::Embed(self))
+ }
+}
impl<'a> Type<'a> {
pub(crate) fn as_normalized(&self) -> Result<&Normalized<'a>, TypeError> {
use TypeInternal::*;
@@ -108,6 +113,11 @@ impl<'a> Type<'a> {
.into_type()
}
}
+impl Type<'static> {
+ fn embed<N>(self) -> Result<SubExpr<N, Normalized<'static>>, TypeError> {
+ Ok(self.into_normalized()?.embed())
+ }
+}
fn function_check(a: Const, b: Const) -> Result<Const, ()> {
use dhall_core::Const::*;
@@ -348,27 +358,27 @@ fn type_with(
let b = type_with(&ctx2, b.clone())?;
Ok(RetExpr(Pi(
x.clone(),
- t.into_normalized()?.into_expr(),
- b.get_type_move()?.into_normalized()?.into_expr(),
+ t.embed()?,
+ b.get_type_move()?.embed()?,
)))
}
- Pi(x, tA, tB) => {
- let tA = mktype(ctx, tA.clone())?;
+ Pi(x, ta, tb) => {
+ let ta = mktype(ctx, ta.clone())?;
let kA = ensure_is_const!(
- &tA.get_type()?,
- mkerr(InvalidInputType(tA.into_normalized()?)),
+ &ta.get_type()?,
+ mkerr(InvalidInputType(ta.into_normalized()?)),
);
let ctx2 = ctx
- .insert(x.clone(), tA.clone())
+ .insert(x.clone(), ta.clone())
.map(|e| e.shift(1, &V(x.clone(), 0)));
- let tB = type_with(&ctx2, tB.clone())?;
+ let tb = type_with(&ctx2, tb.clone())?;
let kB = ensure_is_const!(
- &tB.get_type()?,
+ &tb.get_type()?,
TypeError::new(
&ctx2,
e.clone(),
- InvalidOutputType(tB.get_type_move()?.into_normalized()?),
+ InvalidOutputType(tb.get_type_move()?.into_normalized()?),
),
);
@@ -376,8 +386,8 @@ fn type_with(
Ok(k) => k,
Err(()) => {
return Err(mkerr(NoDependentTypes(
- tA.clone().into_normalized()?,
- tB.get_type_move()?.into_normalized()?,
+ ta.clone().into_normalized()?,
+ tb.get_type_move()?.into_normalized()?,
)))
}
};
@@ -395,7 +405,7 @@ fn type_with(
let e = type_with(
ctx,
// TODO: Use a substitution context
- subst_shift(&V(x.clone(), 0), &v.as_expr().absurd(), e),
+ subst_shift(&V(x.clone(), 0), &v.embed(), e),
)?;
Ok(RetType(e.get_type_move()?))
@@ -442,17 +452,20 @@ fn type_last_layer(
},
App(f, args) => {
let mut tf = f.get_type()?.into_owned();
+ // Reconstruct the application `f a0 a1 ...`
+ // for error reporting
+ let mkf = |args: Vec<_>, i| {
+ rc(App(
+ f.into_expr(),
+ args.into_iter().take(i).map(Typed::into_expr).collect(),
+ ))
+ };
+
for (i, a) in args.iter().enumerate() {
let (x, tx, tb) = ensure_matches!(tf,
Pi(x, tx, tb) => (x, tx, tb),
mkerr(NotAFunction(Typed(
- rc(App(
- f.into_expr(),
- args.into_iter()
- .take(i)
- .map(Typed::into_expr)
- .collect()
- )),
+ mkf(args, i),
Some(tf),
PhantomData
)))
@@ -461,24 +474,19 @@ fn type_last_layer(
ensure_equal!(&tx, a.get_type()?, {
let a = a.clone();
mkerr(TypeMismatch(
- Typed(
- rc(App(
- f.into_expr(),
- args.into_iter()
- .take(i + 1)
- .map(Typed::into_expr)
- .collect(),
- )),
- Some(tf),
- PhantomData,
- ),
+ Typed(mkf(args, i + 1), Some(tf), PhantomData),
tx.into_normalized()?,
a,
))
});
tf = mktype(
ctx,
- rc(Let(x.clone(), None, a.as_expr().clone(), tb.absurd())),
+ rc(Let(
+ x.clone(),
+ None,
+ a.clone().normalize().embed(),
+ tb.absurd(),
+ )),
)?;
}
Ok(RetType(tf))
@@ -523,7 +531,7 @@ fn type_last_layer(
t,
mkerr(InvalidListType(t.into_normalized()?)),
);
- let t = t.into_normalized()?.into_expr();
+ let t = t.embed()?;
Ok(RetExpr(dhall::expr!(List t)))
}
NEListLit(xs) => {
@@ -544,43 +552,41 @@ fn type_last_layer(
))
);
}
- let t = x.get_type_move()?.into_normalized()?.into_expr();
+ let t = x.get_type_move()?;
+ let t = t.embed()?;
Ok(RetExpr(dhall::expr!(List t)))
}
OldOptionalLit(None, t) => {
- let t = t.into_expr();
+ let t = t.normalize().embed();
let e = dhall::subexpr!(None t);
Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned()))
}
OldOptionalLit(Some(x), t) => {
- let x = x.into_expr();
- let t = t.into_expr();
+ let t = t.normalize().embed();
+ let x = x.normalize().embed();
let e = dhall::subexpr!(Some x : Optional t);
Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned()))
}
EmptyOptionalLit(t) => {
- let t = t.normalize().into_type();
- ensure_simple_type!(
- t,
- mkerr(InvalidOptionalType(t.into_normalized()?)),
- );
- let t = t.into_normalized()?.into_expr();
+ let t = t.normalize();
+ ensure_simple_type!(t, mkerr(InvalidOptionalType(t)));
+ let t = t.embed();
Ok(RetExpr(dhall::expr!(Optional t)))
}
NEOptionalLit(x) => {
let tx = x.get_type_move()?;
ensure_simple_type!(
tx,
- mkerr(InvalidOptionalType(tx.into_normalized()?,)),
+ mkerr(InvalidOptionalType(tx.into_normalized()?)),
);
- let t = tx.into_normalized()?.into_expr();
+ let t = tx.embed()?;
Ok(RetExpr(dhall::expr!(Optional t)))
}
RecordType(kts) => {
for (k, t) in kts {
- ensure_simple_type!(t, mkerr(InvalidFieldType(k, t)),);
+ ensure_simple_type!(t, mkerr(InvalidFieldType(k, t)));
}
- Ok(RetExpr(dhall::expr!(Type)))
+ Ok(RetType(crate::expr::Type::const_type()))
}
RecordLit(kvs) => {
let kts = kvs
@@ -590,7 +596,9 @@ fn type_last_layer(
v.get_type()?,
mkerr(InvalidField(k, v)),
);
- Ok((k, v.get_type_move()?.into_normalized()?.into_expr()))
+ let t = v.get_type_move()?;
+ let t = t.embed()?;
+ Ok((k, t))
})
.collect::<Result<_, _>>()?;
Ok(RetExpr(RecordType(kts)))
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 12:31:45 +0000