summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/typecheck.rs112
1 files changed, 66 insertions, 46 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index fe9f68c..3815f9f 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -61,10 +61,10 @@ impl<'a> Type<'a> {
}
}
#[inline(always)]
- fn as_expr(&'a self) -> Result<&'a SubExpr<X, X>, TypeError<X>> {
+ fn as_expr(&'a self) -> Result<&'a Normalized, TypeError<X>> {
use TypeInternal::*;
match self.0.as_ref() {
- Expr(e) => Ok(e.as_expr()),
+ Expr(e) => Ok(e),
Universe(_) => Err(TypeError::new(
&Context::new(),
rc(ExprF::Const(Const::Sort)),
@@ -73,10 +73,10 @@ impl<'a> Type<'a> {
}
}
#[inline(always)]
- fn into_expr(self) -> Result<SubExpr<X, X>, TypeError<X>> {
+ fn into_expr(self) -> Result<Normalized, TypeError<X>> {
use TypeInternal::*;
match self.0.into_owned() {
- Expr(e) => Ok(e.into_expr()),
+ Expr(e) => Ok(*e),
Universe(_) => Err(TypeError::new(
&Context::new(),
rc(ExprF::Const(Const::Sort)),
@@ -292,6 +292,7 @@ pub fn type_with(
let mkerr = |msg: TypeMessage<_>| TypeError::new(ctx, e.clone(), msg);
let ensure_const = |x: &crate::expr::Type, msg: TypeMessage<_>| match x
.as_expr()?
+ .as_expr()
.as_ref()
{
Const(k) => Ok(*k),
@@ -299,6 +300,7 @@ pub fn type_with(
};
let ensure_is_type = |x: &crate::expr::Type, msg: TypeMessage<_>| match x
.as_expr()?
+ .as_expr()
.as_ref()
{
Const(Type) => Ok(()),
@@ -317,43 +319,51 @@ pub fn type_with(
Lam(x, t, b) => {
let t2 = mktype(ctx, t.clone())?;
let ctx2 = ctx
- .insert(x.clone(), t2.as_expr()?.clone())
+ .insert(x.clone(), t2.as_expr()?.as_expr().clone())
.map(|e| shift(1, &V(x.clone(), 0), e));
let b = type_with(&ctx2, b.clone())?;
let _ = type_with(
ctx,
- rc(Pi(x.clone(), t.clone(), b.get_type().as_expr()?.clone())),
+ rc(Pi(
+ x.clone(),
+ t.clone(),
+ b.get_type().as_expr()?.as_expr().clone(),
+ )),
)?;
Ok(RetExpr(Pi(
x.clone(),
- t2.as_expr()?.clone(),
- b.get_type().into_expr()?,
+ t2.as_expr()?.as_expr().clone(),
+ b.get_type().into_expr()?.into_expr(),
)))
}
Pi(x, tA, tB) => {
let tA = mktype(ctx, tA.clone())?;
- let kA =
- ensure_const(&tA.get_type(), InvalidInputType(tA.clone()))?;
+ let kA = ensure_const(
+ &tA.get_type(),
+ InvalidInputType(tA.clone().into_expr()?),
+ )?;
let ctx2 = ctx
- .insert(x.clone(), tA.as_expr()?.clone())
+ .insert(x.clone(), tA.as_expr()?.as_expr().clone())
.map(|e| shift(1, &V(x.clone(), 0), e));
let tB = type_with(&ctx2, tB.clone())?;
- let kB = match tB.get_type().as_expr()?.as_ref() {
+ let kB = match tB.get_type().as_expr()?.as_expr().as_ref() {
Const(k) => *k,
_ => {
return Err(TypeError::new(
&ctx2,
e.clone(),
- InvalidOutputType(tB.get_type().into_owned()),
+ InvalidOutputType(
+ tB.get_type().into_owned().into_expr()?,
+ ),
));
}
};
match rule(kA, kB) {
Err(()) => Err(mkerr(NoDependentTypes(
- tA.clone(),
- tB.get_type().into_owned(),
+ tA.clone().into_expr()?,
+ tB.get_type().into_owned().into_expr()?,
))),
Ok(k) => Ok(RetExpr(Const(k))),
}
@@ -370,22 +380,23 @@ pub fn type_with(
// message because this should never happen anyway
let kR = ensure_const(
&r.get_type().get_type(),
- InvalidInputType(r.get_type().into_owned()),
+ InvalidInputType(r.get_type().into_owned().into_expr()?),
)?;
- let ctx2 = ctx.insert(f.clone(), r.get_type().as_expr()?.clone());
+ let ctx2 = ctx
+ .insert(f.clone(), r.get_type().as_expr()?.as_expr().clone());
let b = type_with(&ctx2, b.clone())?;
// Don't bother to provide a `let`-specific version of this error
// message because this should never happen anyway
let kB = ensure_const(
&b.get_type().get_type(),
- InvalidOutputType(b.get_type().into_owned()),
+ InvalidOutputType(b.get_type().into_owned().into_expr()?),
)?;
if let Err(()) = rule(kR, kB) {
return Err(mkerr(NoDependentLet(
- r.get_type().into_owned(),
- b.get_type().into_owned(),
+ r.get_type().into_owned().into_expr()?,
+ b.get_type().into_owned().into_expr()?,
)));
}
@@ -411,7 +422,7 @@ pub fn type_with(
let mut tf = f.get_type().into_owned();
while let Some(a) = iter.next() {
seen_args.push(a.as_expr().clone());
- let (x, tx, tb) = match tf.as_expr()?.as_ref() {
+ let (x, tx, tb) = match tf.as_expr()?.as_expr().as_ref() {
Pi(x, tx, tb) => (x, tx, tb),
_ => {
return Err(mkerr(NotAFunction(Typed(
@@ -427,7 +438,7 @@ pub fn type_with(
rc(App(f.as_expr().clone(), seen_args.clone())),
tf.clone(),
),
- tx.clone(),
+ tx.clone().into_expr().unwrap(),
a.clone(),
)
})?;
@@ -441,7 +452,7 @@ pub fn type_with(
Annot(x, t) => {
let t = t.normalize().into_type();
ensure_equal(&t, &x.get_type(), mkerr, || {
- AnnotMismatch(x.clone(), t.clone())
+ AnnotMismatch(x.clone(), t.clone().into_expr().unwrap())
})?;
Ok(RetType(x.get_type().into_owned()))
}
@@ -470,8 +481,11 @@ pub fn type_with(
}
EmptyListLit(t) => {
let t = t.normalize().into_type();
- ensure_is_type(&t.get_type(), InvalidListType(t.clone()))?;
- let t = t.into_expr()?;
+ ensure_is_type(
+ &t.get_type(),
+ InvalidListType(t.clone().into_expr()?),
+ )?;
+ let t = t.into_expr()?.into_expr();
Ok(RetExpr(dhall::expr!(List t)))
}
NEListLit(xs) => {
@@ -479,32 +493,35 @@ pub fn type_with(
let (_, x) = iter.next().unwrap();
ensure_is_type(
&x.get_type().get_type(),
- InvalidListType(x.get_type().into_owned()),
+ InvalidListType(x.get_type().into_owned().into_expr()?),
)?;
for (i, y) in iter {
ensure_equal(&x.get_type(), &y.get_type(), mkerr, || {
InvalidListElement(
i,
- x.get_type().into_owned(),
+ x.get_type().into_owned().into_expr().unwrap(),
y.clone(),
)
})?;
}
- let t = x.get_type().into_expr()?;
+ let t = x.get_type().into_expr()?.into_expr();
Ok(RetExpr(dhall::expr!(List t)))
}
EmptyOptionalLit(t) => {
let t = t.normalize().into_type();
- ensure_is_type(&t.get_type(), InvalidOptionalType(t.clone()))?;
- let t = t.into_expr()?;
+ ensure_is_type(
+ &t.get_type(),
+ InvalidOptionalType(t.clone().into_expr()?),
+ )?;
+ let t = t.into_expr()?.into_expr();
Ok(RetExpr(dhall::expr!(Optional t)))
}
NEOptionalLit(x) => {
ensure_is_type(
&x.get_type().get_type(),
- InvalidOptionalType(x.get_type().into_owned()),
+ InvalidOptionalType(x.get_type().into_owned().into_expr()?),
)?;
- let t = x.get_type().into_expr()?;
+ let t = x.get_type().into_expr()?.into_expr();
Ok(RetExpr(dhall::expr!(Optional t)))
}
RecordType(kts) => {
@@ -524,12 +541,12 @@ pub fn type_with(
&v.get_type().get_type(),
InvalidField(k.clone(), v.clone()),
)?;
- Ok((k.clone(), v.get_type().into_expr()?))
+ Ok((k.clone(), v.get_type().into_expr()?.into_expr()))
})
.collect::<Result<_, _>>()?;
Ok(RetExpr(RecordType(kts)))
}
- Field(r, x) => match r.get_type().as_expr()?.as_ref() {
+ Field(r, x) => match r.get_type().as_expr()?.as_expr().as_ref() {
RecordType(kts) => match kts.get(&x) {
Some(e) => Ok(RetExpr(e.unroll())),
None => Err(mkerr(MissingField(x.clone(), r.clone()))),
@@ -584,7 +601,7 @@ pub fn type_with(
pub fn type_of(e: SubExpr<X, X>) -> Result<SubExpr<X, X>, TypeError<X>> {
let ctx = Context::new();
let e = type_with(&ctx, e)?;
- e.get_type().into_expr()
+ Ok(e.get_type().into_expr()?.into_expr())
}
pub fn type_of_(e: SubExpr<X, X>) -> Result<Typed, TypeError<X>> {
@@ -596,15 +613,15 @@ pub fn type_of_(e: SubExpr<X, X>) -> Result<Typed, TypeError<X>> {
#[derive(Debug)]
pub enum TypeMessage<S> {
UnboundVariable,
- InvalidInputType(Type<'static>),
- InvalidOutputType(Type<'static>),
+ InvalidInputType(Normalized),
+ InvalidOutputType(Normalized),
NotAFunction(Typed),
- TypeMismatch(Typed, Type<'static>, Typed),
- AnnotMismatch(Typed, Type<'static>),
+ TypeMismatch(Typed, Normalized, Typed),
+ AnnotMismatch(Typed, Normalized),
Untyped,
- InvalidListElement(usize, Type<'static>, Typed),
- InvalidListType(Type<'static>),
- InvalidOptionalType(Type<'static>),
+ InvalidListElement(usize, Normalized, Typed),
+ InvalidListType(Normalized),
+ InvalidOptionalType(Normalized),
InvalidPredicate(Typed),
IfBranchMismatch(Typed, Typed),
IfBranchMustBeTerm(bool, Typed),
@@ -615,8 +632,8 @@ pub enum TypeMessage<S> {
NotARecord(Label, Typed),
MissingField(Label, Typed),
BinOpTypeMismatch(BinOp, Typed),
- NoDependentLet(Type<'static>, Type<'static>),
- NoDependentTypes(Type<'static>, Type<'static>),
+ NoDependentLet(Normalized, Normalized),
+ NoDependentTypes(Normalized, Normalized),
MustCombineARecord(SubExpr<S, X>, SubExpr<S, X>),
}
@@ -665,11 +682,14 @@ impl<S> fmt::Display for TypeMessage<S> {
let template = include_str!("errors/TypeMismatch.txt");
let s = template
.replace("$txt0", &format!("{}", e0.as_expr()))
- .replace("$txt1", &format!("{}", e1.as_expr().unwrap()))
+ .replace("$txt1", &format!("{}", e1.as_expr()))
.replace("$txt2", &format!("{}", e2.as_expr()))
.replace(
"$txt3",
- &format!("{}", e2.get_type().as_expr().unwrap()),
+ &format!(
+ "{}",
+ e2.get_type().as_expr().unwrap().as_expr()
+ ),
);
f.write_str(&s)
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 14:52:09 +0000