summaryrefslogtreecommitdiff
path: root/dhall/src/phase/typecheck.rs
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/phase/typecheck.rs')
-rw-r--r--dhall/src/phase/typecheck.rs131
1 files changed, 53 insertions, 78 deletions
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 1ea87d1..ef2018a 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -31,7 +31,7 @@ fn tck_pi_type(
_ => {
return Err(TypeError::new(
&ctx2,
- InvalidOutputType(te.get_type()?.into_owned()),
+ InvalidOutputType(te.get_type()?),
))
}
};
@@ -129,21 +129,16 @@ fn function_check(a: Const, b: Const) -> Const {
}
}
-fn type_of_const(c: Const) -> Result<Value, TypeError> {
- match c {
- Const::Type => Ok(const_to_value(Const::Kind)),
- Const::Kind => Ok(const_to_value(Const::Sort)),
- Const::Sort => {
- Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
- }
- }
-}
-
pub(crate) fn const_to_value(c: Const) -> Value {
let v = ValueF::Const(c);
- match type_of_const(c) {
- Ok(t) => Value::from_valuef_and_type(v, t),
- Err(_) => Value::from_valuef_untyped(v),
+ match c {
+ Const::Type => {
+ Value::from_valuef_and_type(v, const_to_value(Const::Kind))
+ }
+ Const::Kind => {
+ Value::from_valuef_and_type(v, const_to_value(Const::Sort))
+ }
+ Const::Sort => Value::const_sort(),
}
}
@@ -291,7 +286,7 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
pub(crate) fn builtin_to_value(b: Builtin) -> Value {
let ctx = TypecheckContext::new();
Value::from_valuef_and_type(
- ValueF::PartialExpr(ExprF::Builtin(b)),
+ ValueF::from_builtin(b),
type_with(&ctx, rc(type_of_builtin(b))).unwrap(),
)
}
@@ -307,14 +302,15 @@ fn type_with(
use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var};
Ok(match e.as_ref() {
- Lam(x, t, b) => {
- let tx = type_with(ctx, t.clone())?;
- let ctx2 = ctx.insert_type(x, tx.clone());
- let b = type_with(&ctx2, b.clone())?;
- let v = ValueF::Lam(x.clone().into(), tx.clone(), b.clone());
- let tb = b.get_type()?.into_owned();
- let t = tck_pi_type(ctx, x.clone(), tx, tb)?;
- Value::from_valuef_and_type(v, t)
+ Lam(var, annot, body) => {
+ let annot = type_with(ctx, annot.clone())?;
+ let ctx2 = ctx.insert_type(var, annot.clone());
+ let body = type_with(&ctx2, body.clone())?;
+ let body_type = body.get_type()?;
+ Value::from_valuef_and_type(
+ ValueF::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())?;
@@ -389,17 +385,17 @@ fn type_last_layer(
ValueF::Pi(x, tx, tb) => (x, tx, tb),
_ => return mkerr(NotAFunction(f.clone())),
};
- if a.get_type()?.as_ref() != tx {
+ if &a.get_type()? != tx {
return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone()));
}
RetTypeOnly(tb.subst_shift(&x.into(), a))
}
Annot(x, t) => {
- if t != x.get_type()?.as_ref() {
+ if &x.get_type()? != t {
return mkerr(AnnotMismatch(x.clone(), t.clone()));
}
- RetTypeOnly(x.get_type()?.into_owned())
+ RetWhole(x.clone())
}
Assert(t) => {
match &*t.as_whnf() {
@@ -412,7 +408,7 @@ fn type_last_layer(
RetTypeOnly(t.clone())
}
BoolIf(x, y, z) => {
- if x.get_type()?.as_ref() != &builtin_to_value(Bool) {
+ if &*x.get_type()?.as_whnf() != &ValueF::from_builtin(Bool) {
return mkerr(InvalidPredicate(x.clone()));
}
@@ -428,7 +424,7 @@ fn type_last_layer(
return mkerr(IfBranchMismatch(y.clone(), z.clone()));
}
- RetTypeOnly(y.get_type()?.into_owned())
+ RetTypeOnly(y.get_type()?)
}
EmptyListLit(t) => {
match &*t.as_whnf() {
@@ -445,33 +441,27 @@ fn type_last_layer(
if x.get_type()? != y.get_type()? {
return mkerr(InvalidListElement(
i,
- x.get_type()?.into_owned(),
+ x.get_type()?,
y.clone(),
));
}
}
let t = x.get_type()?;
if t.get_type()?.as_const() != Some(Type) {
- return mkerr(InvalidListType(t.into_owned()));
+ return mkerr(InvalidListType(t));
}
- RetTypeOnly(Value::from_valuef_and_type(
- ValueF::from_builtin(dhall_syntax::Builtin::List)
- .app_value(t.into_owned()),
- Value::from_const(Type),
- ))
+ RetTypeOnly(Value::from_builtin(dhall_syntax::Builtin::List).app(t))
}
SomeLit(x) => {
- let t = x.get_type()?.into_owned();
+ let t = x.get_type()?;
if t.get_type()?.as_const() != Some(Type) {
return mkerr(InvalidOptionalType(t));
}
- RetTypeOnly(Value::from_valuef_and_type(
- ValueF::from_builtin(dhall_syntax::Builtin::Optional)
- .app_value(t),
- Value::from_const(Type),
- ))
+ RetTypeOnly(
+ Value::from_builtin(dhall_syntax::Builtin::Optional).app(t),
+ )
}
RecordType(kts) => RetWhole(tck_record_type(
ctx,
@@ -483,8 +473,7 @@ fn type_last_layer(
)?),
RecordLit(kvs) => RetTypeOnly(tck_record_type(
ctx,
- kvs.iter()
- .map(|(x, v)| Ok((x.clone(), v.get_type()?.into_owned()))),
+ kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))),
)?),
Field(r, x) => {
match &*r.get_type()?.as_whnf() {
@@ -545,7 +534,7 @@ fn type_last_layer(
for contents in interpolated.iter() {
use InterpolatedTextContents::Expr;
if let Expr(x) = contents {
- if x.get_type()?.as_ref() != &text_type {
+ if x.get_type()? != text_type {
return mkerr(InvalidTextInterpolation(x.clone()));
}
}
@@ -574,7 +563,9 @@ fn type_last_layer(
// Union the two records, prefering
// the values found in the RHS.
- let kts = merge_maps(kts_x, kts_y, |_, r_t| r_t.clone());
+ let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, _, r_t| {
+ Ok(r_t.clone())
+ })?;
// Construct the final record type from the union
RetTypeOnly(tck_record_type(
@@ -586,30 +577,12 @@ fn type_last_layer(
ctx,
ExprF::BinOp(
RecursiveRecordTypeMerge,
- l.get_type()?.into_owned(),
- r.get_type()?.into_owned(),
+ l.get_type()?,
+ r.get_type()?,
),
)?),
BinOp(RecursiveRecordTypeMerge, l, r) => {
- use crate::phase::normalize::intersection_with_key;
-
- // Extract the Const of the LHS
- let k_l = match l.get_type()?.as_const() {
- Some(k) => k,
- _ => {
- return mkerr(RecordTypeMergeRequiresRecordType(l.clone()))
- }
- };
-
- // Extract the Const of the RHS
- let k_r = match r.get_type()?.as_const() {
- Some(k) => k,
- _ => {
- return mkerr(RecordTypeMergeRequiresRecordType(r.clone()))
- }
- };
-
- let k = max(k_l, k_r);
+ use crate::phase::normalize::merge_maps;
// Extract the LHS record type
let borrow_l = l.as_whnf();
@@ -630,9 +603,11 @@ fn type_last_layer(
};
// Ensure that the records combine without a type error
- let kts = intersection_with_key(
+ let kts = merge_maps(
+ kts_x,
+ kts_y,
// If the Label exists for both records, then we hit the recursive case.
- |_: &Label, l: &Value, r: &Value| {
+ |_, l: &Value, r: &Value| {
type_last_layer(
ctx,
ExprF::BinOp(
@@ -642,12 +617,9 @@ fn type_last_layer(
),
)
},
- kts_x,
- kts_y,
- );
- tck_record_type(ctx, kts.into_iter().map(|(x, v)| Ok((x, v?))))?;
+ )?;
- RetTypeOnly(Value::from_const(k))
+ RetWhole(tck_record_type(ctx, kts.into_iter().map(Ok))?)
}
BinOp(o @ ListAppend, l, r) => {
match &*l.get_type()?.as_whnf() {
@@ -659,7 +631,7 @@ fn type_last_layer(
return mkerr(BinOpTypeMismatch(*o, r.clone()));
}
- RetTypeOnly(l.get_type()?.into_owned())
+ RetTypeOnly(l.get_type()?)
}
BinOp(Equivalence, l, r) => {
if l.get_type()?.get_type()?.as_const() != Some(Type) {
@@ -673,7 +645,10 @@ fn type_last_layer(
return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone()));
}
- RetTypeOnly(Value::from_const(Type))
+ RetWhole(Value::from_valuef_and_type(
+ ValueF::Equivalence(l.clone(), r.clone()),
+ Value::from_const(Type),
+ ))
}
BinOp(o, l, r) => {
let t = builtin_to_value(match o {
@@ -692,11 +667,11 @@ fn type_last_layer(
Equivalence => unreachable!(),
});
- if l.get_type()?.as_ref() != &t {
+ if l.get_type()? != t {
return mkerr(BinOpTypeMismatch(*o, l.clone()));
}
- if r.get_type()?.as_ref() != &t {
+ if r.get_type()? != t {
return mkerr(BinOpTypeMismatch(*o, r.clone()));
}
@@ -800,7 +775,7 @@ fn type_last_layer(
RetTypeOnly(Value::from_valuef_and_type(
ValueF::RecordType(new_kts),
- record_type.get_type()?.into_owned(),
+ record_type.get_type()?,
))
}
};
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 19:16:44 +0000