summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/typecheck.rs84
1 files changed, 35 insertions, 49 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 22d3c42..e5b81bd 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -215,19 +215,19 @@ where
let ctx2 = ctx
.insert(x.clone(), tA.clone())
.map(|e| shift(1, &V(x.clone(), 0), e));
- let tB = normalized_type_with(&ctx2, b.clone())?;
+ let tB = type_with(&ctx2, b.clone())?;
let p = Pi(x.clone(), tA.clone(), tB);
- let _ = normalized_type_with(ctx, rc(p.clone()))?;
+ let _ = type_with(ctx, rc(p.clone()))?;
Ok(p)
}
Pi(x, tA, tB) => {
- let tA2 = normalized_type_with(ctx, tA.clone())?;
+ let tA2 = type_with(ctx, tA.clone())?;
let kA = ensure_const(&tA2, InvalidInputType(tA.clone()))?;
let ctx2 = ctx
.insert(x.clone(), tA.clone())
.map(|e| shift(1, &V(x.clone(), 0), e));
- let tB = normalized_type_with(&ctx2, tB.clone())?;
+ let tB = type_with(&ctx2, tB.clone())?;
let kB = match tB.as_ref() {
Const(k) => *k,
_ => {
@@ -247,14 +247,10 @@ where
App(f, args) => {
// Recurse on args
let (a, tf) = match args.split_last() {
- None => return normalized_type_with(ctx, f.clone()),
- Some((a, args)) => (
- a,
- normalized_type_with(
- ctx,
- rc(App(f.clone(), args.to_vec())),
- )?,
- ),
+ None => return type_with(ctx, f.clone()),
+ Some((a, args)) => {
+ (a, type_with(ctx, rc(App(f.clone(), args.to_vec())))?)
+ }
};
let (x, tA, tB) = match tf.as_ref() {
Pi(x, tA, tB) => (x, tA, tB),
@@ -262,7 +258,7 @@ where
return Err(mkerr(NotAFunction(f.clone(), tf)));
}
};
- let tA2 = normalized_type_with(ctx, a.clone())?;
+ let tA2 = type_with(ctx, a.clone())?;
if prop_equal(tA.as_ref(), tA2.as_ref()) {
let vx0 = &V(x.clone(), 0);
Ok(subst_shift(vx0, &a, &tB).unroll())
@@ -277,15 +273,15 @@ where
SubExpr::clone(r)
};
- let tR = normalized_type_with(ctx, r)?;
- let ttR = normalized_type_with(ctx, tR.clone())?;
+ let tR = type_with(ctx, r)?;
+ let ttR = type_with(ctx, tR.clone())?;
// Don't bother to provide a `let`-specific version of this error
// message because this should never happen anyway
let kR = ensure_const(&ttR, InvalidInputType(tR.clone()))?;
let ctx2 = ctx.insert(f.clone(), tR.clone());
- let tB = normalized_type_with(&ctx2, b.clone())?;
- let ttB = normalized_type_with(ctx, tB.clone())?;
+ let tB = type_with(&ctx2, b.clone())?;
+ let ttB = type_with(ctx, tB.clone())?;
// Don't bother to provide a `let`-specific version of this error
// message because this should never happen anyway
let kB = ensure_const(&ttB, InvalidOutputType(tB.clone()))?;
@@ -298,9 +294,9 @@ where
}
Annot(x, t) => {
// This is mainly just to check that `t` is not `Kind`
- let _ = normalized_type_with(ctx, t.clone())?;
+ let _ = type_with(ctx, t.clone())?;
- let t2 = normalized_type_with(ctx, x.clone())?;
+ let t2 = type_with(ctx, x.clone())?;
let t = normalize(t.clone());
if prop_equal(t.as_ref(), t2.as_ref()) {
Ok(t.unroll())
@@ -309,22 +305,22 @@ where
}
}
BoolIf(x, y, z) => {
- let tx = normalized_type_with(ctx, x.clone())?;
+ let tx = type_with(ctx, x.clone())?;
match tx.as_ref() {
Builtin(Bool) => {}
_ => {
return Err(mkerr(InvalidPredicate(x.clone(), tx)));
}
}
- let ty = normalized_type_with(ctx, y.clone())?;
- let tty = normalized_type_with(ctx, ty.clone())?;
+ let ty = type_with(ctx, y.clone())?;
+ let tty = type_with(ctx, ty.clone())?;
ensure_is_type(
tty.clone(),
IfBranchMustBeTerm(true, y.clone(), ty.clone(), tty.clone()),
)?;
- let tz = normalized_type_with(ctx, z.clone())?;
- let ttz = normalized_type_with(ctx, tz.clone())?;
+ let tz = type_with(ctx, z.clone())?;
+ let ttz = type_with(ctx, tz.clone())?;
ensure_is_type(
ttz.clone(),
IfBranchMustBeTerm(false, z.clone(), tz.clone(), ttz.clone()),
@@ -341,7 +337,7 @@ where
Ok(ty.unroll())
}
EmptyListLit(t) => {
- let s = normalized_type_with(ctx, t.clone())?;
+ let s = type_with(ctx, t.clone())?;
ensure_is_type(s, InvalidListType(t.clone()))?;
let t = normalize(SubExpr::clone(t));
Ok(dhall::expr!(List t))
@@ -349,11 +345,11 @@ where
NEListLit(xs) => {
let mut iter = xs.iter().enumerate();
let (_, first_x) = iter.next().unwrap();
- let t = normalized_type_with(ctx, first_x.clone())?;
- let s = normalized_type_with(ctx, t.clone())?;
+ let t = type_with(ctx, first_x.clone())?;
+ let s = type_with(ctx, t.clone())?;
ensure_is_type(s, InvalidListType(t.clone()))?;
for (i, x) in iter {
- let t2 = normalized_type_with(ctx, x.clone())?;
+ let t2 = type_with(ctx, x.clone())?;
if !prop_equal(t.as_ref(), t2.as_ref()) {
return Err(mkerr(InvalidListElement(i, t, x.clone(), t2)));
}
@@ -361,20 +357,20 @@ where
Ok(dhall::expr!(List t))
}
EmptyOptionalLit(t) => {
- let s = normalized_type_with(ctx, t.clone())?;
+ let s = type_with(ctx, t.clone())?;
ensure_is_type(s, InvalidOptionalType(t.clone()))?;
let t = normalize(t.clone());
Ok(dhall::expr!(Optional t))
}
NEOptionalLit(x) => {
- let t = normalized_type_with(ctx, x.clone())?;
- let s = normalized_type_with(ctx, t.clone())?;
+ let t = type_with(ctx, x.clone())?;
+ let s = type_with(ctx, t.clone())?;
ensure_is_type(s, InvalidOptionalType(t.clone()))?;
Ok(dhall::expr!(Optional t))
}
RecordType(kts) => {
for (k, t) in kts {
- let s = normalized_type_with(ctx, t.clone())?;
+ let s = type_with(ctx, t.clone())?;
ensure_is_type(s, InvalidFieldType(k.clone(), t.clone()))?;
}
Ok(Const(Type))
@@ -383,8 +379,8 @@ where
let kts = kvs
.iter()
.map(|(k, v)| {
- let t = normalized_type_with(ctx, v.clone())?;
- let s = normalized_type_with(ctx, t.clone())?;
+ let t = type_with(ctx, v.clone())?;
+ let s = type_with(ctx, t.clone())?;
ensure_is_type(s, InvalidField(k.clone(), v.clone()))?;
Ok((k.clone(), t))
})
@@ -392,7 +388,7 @@ where
Ok(RecordType(kts))
}
Field(r, x) => {
- let t = normalized_type_with(ctx, r.clone())?;
+ let t = type_with(ctx, r.clone())?;
match t.as_ref() {
RecordType(kts) => match kts.get(x) {
Some(e) => Ok(e.unroll()),
@@ -418,13 +414,13 @@ where
TextAppend => Text,
_ => panic!("Unimplemented typecheck case: {:?}", e),
};
- let tl = normalized_type_with(ctx, l.clone())?;
+ let tl = type_with(ctx, l.clone())?;
match tl.as_ref() {
Builtin(lt) if *lt == t => {}
_ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone(), tl))),
}
- let tr = normalized_type_with(ctx, r.clone())?;
+ let tr = type_with(ctx, r.clone())?;
match tr.as_ref() {
Builtin(rt) if *rt == t => {}
_ => return Err(mkerr(BinOpTypeMismatch(*o, r.clone(), tr))),
@@ -435,17 +431,7 @@ where
Embed(p) => match *p {},
_ => panic!("Unimplemented typecheck case: {:?}", e),
}?;
- Ok(rc(ret))
-}
-
-pub fn normalized_type_with<S>(
- ctx: &Context<Label, SubExpr<S, X>>,
- e: SubExpr<S, X>,
-) -> Result<SubExpr<S, X>, TypeError<S>>
-where
- S: ::std::fmt::Debug + Clone,
-{
- Ok(normalize(type_with(ctx, e)?))
+ Ok(normalize(rc(ret)))
}
/// `typeOf` is the same as `type_with` with an empty context, meaning that the
@@ -455,7 +441,7 @@ pub fn type_of<S: ::std::fmt::Debug + Clone>(
e: SubExpr<S, X>,
) -> Result<SubExpr<S, X>, TypeError<S>> {
let ctx = Context::new();
- normalized_type_with(&ctx, e) //.map(|e| e.into_owned())
+ type_with(&ctx, e) //.map(|e| e.into_owned())
}
/// The specific type error
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 05:50:32 +0000