summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/phase/typecheck.rs
diff options
context:
space:
mode:
authorNadrieril2019-12-27 15:36:10 +0000
committerNadrieril2020-01-17 10:06:00 +0000
commitce706817dcb5cb951c566410de92a4f85aae5361 (patch)
treeda7653980ca9f3ee33ec9d7bcead97883cc5373f /dhall/src/semantics/phase/typecheck.rs
parent5542797c77a9dfcdffec539f1a82341a450291a2 (diff)
Tiny clarification
Diffstat (limited to 'dhall/src/semantics/phase/typecheck.rs')
-rw-r--r--dhall/src/semantics/phase/typecheck.rs23
1 files changed, 10 insertions, 13 deletions
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 16eabea..c8d934d 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -306,23 +306,23 @@ fn type_with(ctx: &TyCtx, e: Expr<Normalized>) -> Result<Value, TypeError> {
use syntax::ExprKind::{Annot, Embed, Lam, Let, Pi, Var};
let span = e.span();
- Ok(match e.as_ref() {
+ match e.as_ref() {
Lam(var, annot, body) => {
let annot = type_with(ctx, annot.clone())?;
annot.normalize_nf();
let ctx2 = ctx.insert_type(var, annot.clone());
let body = type_with(&ctx2, body.clone())?;
let body_type = body.get_type()?;
- Value::from_kind_and_type(
+ Ok(Value::from_kind_and_type(
ValueKind::Lam(var.clone().into(), annot.clone(), body),
tck_pi_type(ctx, var.clone(), annot, body_type)?,
- )
+ ))
}
Pi(x, ta, tb) => {
let ta = type_with(ctx, ta.clone())?;
let ctx2 = ctx.insert_type(x, ta.clone());
let tb = type_with(&ctx2, tb.clone())?;
- return tck_pi_type(ctx, x.clone(), ta, tb);
+ tck_pi_type(ctx, x.clone(), ta, tb)
}
Let(x, t, v, e) => {
let v = if let Some(t) = t {
@@ -332,16 +332,13 @@ fn type_with(ctx: &TyCtx, e: Expr<Normalized>) -> Result<Value, TypeError> {
};
let v = type_with(ctx, v)?;
- return type_with(&ctx.insert_value(x, v.clone())?, e.clone());
+ type_with(&ctx.insert_value(x, v.clone())?, e.clone())
}
- Embed(p) => p.clone().into_typed().into_value(),
+ Embed(p) => Ok(p.clone().into_typed().into_value()),
Var(var) => match ctx.lookup(&var) {
- Some(typed) => typed.clone(),
+ Some(typed) => Ok(typed.clone()),
None => {
- return Err(TypeError::new(
- ctx,
- TypeMessage::UnboundVariable(span),
- ))
+ Err(TypeError::new(ctx, TypeMessage::UnboundVariable(span)))
}
},
e => {
@@ -350,9 +347,9 @@ fn type_with(ctx: &TyCtx, e: Expr<Normalized>) -> Result<Value, TypeError> {
|e| type_with(ctx, e.clone()),
|_, _| unreachable!(),
)?;
- type_last_layer(ctx, expr, span)?
+ type_last_layer(ctx, expr, span)
}
- })
+ }
}
/// When all sub-expressions have been typed, check the remaining toplevel