summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
authorNadrieril2020-02-06 17:58:48 +0000
committerNadrieril2020-02-09 20:13:23 +0000
commit5870a46d5ab5810901198f03ed461d5c3bb5aa8a (patch)
treee1bb2ae195e926a0027144f678ca2eedcfa4e0b0 /dhall/src/semantics/tck
parentdb1375eccd1e6943b504cd54ed17eb8f4d19c25f (diff)
Remove move type propagation through Value
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r--dhall/src/semantics/tck/typecheck.rs42
1 files changed, 12 insertions, 30 deletions
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index ceb83de..810e483 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -183,11 +183,11 @@ fn type_one_layer(
};
}
- let ty = type_of_recordtype(
+ type_of_recordtype(
span.clone(),
kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))),
)?;
- Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
+ Value::from_kind(ValueKind::RecordType(kts))
}
ExprKind::RecordType(kts) => {
use std::collections::hash_map::Entry;
@@ -247,22 +247,11 @@ fn type_one_layer(
ValueKind::UnionType(kts) => match kts.get(x) {
// Constructor has type T -> < x: T, ... >
Some(Some(ty)) => {
- // Can't fail because uniontypes must have type Const(_).
- let kt = scrut.get_type()?.as_const().unwrap();
- // The type of the field must be Const smaller than `kt`, thus the
- // function type has type `kt`.
- let pi_ty = Value::from_const(kt);
-
- Value::from_kind_and_type(
- ValueKind::PiClosure {
- binder: Binder::new(x.clone()),
- annot: ty.clone(),
- closure: Closure::new_constant(
- scrut_nf,
- ),
- },
- pi_ty,
- )
+ Value::from_kind(ValueKind::PiClosure {
+ binder: Binder::new(x.clone()),
+ annot: ty.clone(),
+ closure: Closure::new_constant(scrut_nf),
+ })
}
Some(None) => scrut_nf,
None => return span_err("MissingUnionField"),
@@ -386,11 +375,11 @@ fn type_one_layer(
})?;
// Construct the final record type
- let ty = type_of_recordtype(
+ type_of_recordtype(
span.clone(),
kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))),
)?;
- Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
+ Value::from_kind(ValueKind::RecordType(kts))
}
ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
let ekind = ExprKind::BinOp(
@@ -685,12 +674,8 @@ fn type_one_layer(
let mut kts = HashMap::new();
kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text));
kts.insert("mapValue".into(), entry_type);
- let output_type = Value::from_builtin(Builtin::List).app(
- Value::from_kind_and_type(
- ValueKind::RecordType(kts),
- Value::from_const(Const::Type),
- ),
- );
+ let output_type = Value::from_builtin(Builtin::List)
+ .app(Value::from_kind(ValueKind::RecordType(kts)));
if let Some(annot) = annot {
let annot_val = annot.eval(env.as_nzenv());
if output_type != annot_val {
@@ -723,10 +708,7 @@ fn type_one_layer(
};
}
- Value::from_kind_and_type(
- ValueKind::RecordType(new_kts),
- record_type.get_type(env)?,
- )
+ Value::from_kind(ValueKind::RecordType(new_kts))
}
ExprKind::ProjectionByExpr(record, selection) => {
let record_type = record.get_type()?;