summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2019-04-06 14:28:59 +0200
committerNadrieril2019-04-06 14:29:49 +0200
commit615797412fabf60b9dd7464f9bc1668dd859ea53 (patch)
treee7f46d4b7a7965c88ac7f3cb50e0116c728280ff /dhall
parent02698056218c53635582001c5517c570f122f94d (diff)
Move more cases after recursion
Diffstat (limited to '')
-rw-r--r--dhall/src/typecheck.rs68
1 files changed, 34 insertions, 34 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index e21669d..08e5928 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -205,11 +205,6 @@ where
};
let ret = match e.as_ref() {
- Const(c) => axiom(*c).map(Const),
- Var(V(x, n)) => match ctx.lookup(x, *n) {
- Some(e) => Ok(e.unroll()),
- None => Err(mkerr(UnboundVariable)),
- },
Lam(x, t, b) => {
let t2 = normalize(SubExpr::clone(t));
let ctx2 = ctx
@@ -244,35 +239,6 @@ where
Ok(_) => Ok(Const(kB)),
}
}
- App(f, args) => {
- let mut iter = args.iter().cloned();
- let mut tf: SubExpr<_, _> = type_with(ctx, f.clone())?;
- let mut seen_args: Vec<SubExpr<_, _>> = vec![];
- while let Some(a) = iter.next() {
- seen_args.push(a.clone());
- let (x, tA, tB) = match tf.as_ref() {
- Pi(x, tA, tB) => (x, tA, tB),
- _ => {
- return Err(mkerr(NotAFunction(
- rc(App(f.clone(), seen_args)),
- tf,
- )));
- }
- };
- let tA2 = type_with(ctx, a.clone())?;
- if !prop_equal(tA.as_ref(), tA2.as_ref()) {
- return Err(mkerr(TypeMismatch(
- rc(App(f.clone(), seen_args)),
- tA.clone(),
- a.clone(),
- tA2,
- )));
- }
- let vx0 = &V(x.clone(), 0);
- tf = normalize(subst_shift(vx0, &a, &tB));
- }
- Ok(tf.unroll())
- }
Let(f, mt, r, b) => {
let r = if let Some(t) = mt {
rc(Annot(SubExpr::clone(r), SubExpr::clone(t)))
@@ -303,6 +269,40 @@ where
.as_ref()
.traverse_ref_simple(|e| Ok((e, type_with(ctx, e.clone())?)))?
{
+ Lam(_, _, _) => unreachable!(),
+ Pi(_, _, _) => unreachable!(),
+ Let(_, _, _, _) => unreachable!(),
+ Const(c) => axiom(c).map(Const),
+ Var(V(x, n)) => match ctx.lookup(&x, n) {
+ Some(e) => Ok(e.unroll()),
+ None => Err(mkerr(UnboundVariable)),
+ },
+ App((f, mut tf), args) => {
+ let mut iter = args.into_iter();
+ let mut seen_args: Vec<SubExpr<_, _>> = vec![];
+ while let Some((a, ta)) = iter.next() {
+ seen_args.push(a.clone());
+ let (x, tx, tb) = match tf.as_ref() {
+ Pi(x, tx, tb) => (x, tx, tb),
+ _ => {
+ return Err(mkerr(NotAFunction(
+ rc(App(f.clone(), seen_args)),
+ tf,
+ )));
+ }
+ };
+ if !prop_equal(tx.as_ref(), ta.as_ref()) {
+ return Err(mkerr(TypeMismatch(
+ rc(App(f.clone(), seen_args)),
+ tx.clone(),
+ a.clone(),
+ ta,
+ )));
+ }
+ tf = normalize(subst_shift(&V(x.clone(), 0), &a, &tb));
+ }
+ Ok(tf.unroll())
+ }
Annot((x, tx), (t, _)) => {
let t = normalize(t.clone());
if prop_equal(t.as_ref(), tx.as_ref()) {