summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/nze/normalize.rs170
-rw-r--r--dhall/src/semantics/tck/typecheck.rs54
2 files changed, 75 insertions, 149 deletions
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index e677f78..e9d140b 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -11,8 +11,7 @@ use crate::syntax::{
use crate::Normalized;
pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind {
- let f_borrow = f.kind();
- match &*f_borrow {
+ match f.kind() {
ValueKind::LamClosure { closure, .. } => {
closure.apply(a).to_whnf_check_type(ty)
}
@@ -26,10 +25,7 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind {
uniont.clone(),
f.get_type().unwrap(),
),
- _ => {
- drop(f_borrow);
- ValueKind::PartialExpr(ExprKind::App(f, a))
- }
+ _ => ValueKind::PartialExpr(ExprKind::App(f, a)),
}
}
@@ -47,21 +43,17 @@ pub(crate) fn squash_textlit(
for contents in elts {
match contents {
Text(s) => crnt_str.push_str(&s),
- Expr(e) => {
- let e_borrow = e.kind();
- match &*e_borrow {
- ValueKind::TextLit(elts2) => {
- inner(elts2.iter().cloned(), crnt_str, ret)
- }
- _ => {
- drop(e_borrow);
- if !crnt_str.is_empty() {
- ret.push(Text(replace(crnt_str, String::new())))
- }
- ret.push(Expr(e.clone()))
+ Expr(e) => match e.kind() {
+ ValueKind::TextLit(elts2) => {
+ inner(elts2.iter().cloned(), crnt_str, ret)
+ }
+ _ => {
+ if !crnt_str.is_empty() {
+ ret.push(Text(replace(crnt_str, String::new())))
}
+ ret.push(Expr(e.clone()))
}
- }
+ },
}
}
}
@@ -123,9 +115,7 @@ fn apply_binop<'a>(
use ValueKind::{
BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
};
- let x_borrow = x.kind();
- let y_borrow = y.kind();
- Some(match (o, &*x_borrow, &*y_borrow) {
+ Some(match (o, x.kind(), y.kind()) {
(BoolAnd, BoolLit(true), _) => Ret::ValueRef(y),
(BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x),
(BoolAnd, BoolLit(false), _) => Ret::ValueKind(BoolLit(false)),
@@ -202,8 +192,7 @@ fn apply_binop<'a>(
Ret::ValueRef(y)
}
(RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
- let ty_borrow = ty.kind();
- let kts = match &*ty_borrow {
+ let kts = match ty.kind() {
RecordType(kts) => kts,
_ => unreachable!("Internal type error"),
};
@@ -314,23 +303,15 @@ pub(crate) fn normalize_one_layer(
}
}
ExprKind::BoolIf(ref b, ref e1, ref e2) => {
- let b_borrow = b.kind();
- match &*b_borrow {
+ match b.kind() {
BoolLit(true) => Ret::ValueRef(e1),
BoolLit(false) => Ret::ValueRef(e2),
_ => {
- let e1_borrow = e1.kind();
- let e2_borrow = e2.kind();
- match (&*e1_borrow, &*e2_borrow) {
+ match (e1.kind(), e2.kind()) {
// Simplify `if b then True else False`
(BoolLit(true), BoolLit(false)) => Ret::ValueRef(b),
_ if e1 == e2 => Ret::ValueRef(e1),
- _ => {
- drop(b_borrow);
- drop(e1_borrow);
- drop(e2_borrow);
- Ret::Expr(expr)
- }
+ _ => Ret::Expr(expr),
}
}
}
@@ -343,94 +324,53 @@ pub(crate) fn normalize_one_layer(
ExprKind::Projection(_, ref ls) if ls.is_empty() => {
Ret::ValueKind(RecordLit(HashMap::new()))
}
- ExprKind::Projection(ref v, ref ls) => {
- let v_borrow = v.kind();
- match &*v_borrow {
- RecordLit(kvs) => Ret::ValueKind(RecordLit(
- ls.iter()
- .filter_map(|l| {
- kvs.get(l).map(|x| (l.clone(), x.clone()))
- })
- .collect(),
- )),
- _ => {
- drop(v_borrow);
- Ret::Expr(expr)
- }
- }
- }
- ExprKind::Field(ref v, ref l) => {
- let v_borrow = v.kind();
- match &*v_borrow {
- RecordLit(kvs) => match kvs.get(l) {
- Some(r) => Ret::Value(r.clone()),
- None => {
- drop(v_borrow);
- Ret::Expr(expr)
- }
- },
- UnionType(kts) => Ret::ValueKind(UnionConstructor(
- l.clone(),
- kts.clone(),
- v.get_type().unwrap(),
- )),
- _ => {
- drop(v_borrow);
- Ret::Expr(expr)
- }
- }
- }
+ ExprKind::Projection(ref v, ref ls) => match v.kind() {
+ RecordLit(kvs) => Ret::ValueKind(RecordLit(
+ ls.iter()
+ .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone())))
+ .collect(),
+ )),
+ _ => Ret::Expr(expr),
+ },
+ ExprKind::Field(ref v, ref l) => match v.kind() {
+ RecordLit(kvs) => match kvs.get(l) {
+ Some(r) => Ret::Value(r.clone()),
+ None => Ret::Expr(expr),
+ },
+ UnionType(kts) => Ret::ValueKind(UnionConstructor(
+ l.clone(),
+ kts.clone(),
+ v.get_type().unwrap(),
+ )),
+ _ => Ret::Expr(expr),
+ },
ExprKind::ProjectionByExpr(_, _) => {
unimplemented!("selection by expression")
}
ExprKind::Completion(_, _) => unimplemented!("record completion"),
ExprKind::Merge(ref handlers, ref variant, _) => {
- let handlers_borrow = handlers.kind();
- let variant_borrow = variant.kind();
- match (&*handlers_borrow, &*variant_borrow) {
- (RecordLit(kvs), UnionConstructor(l, _, _)) => match kvs.get(l)
- {
- Some(h) => Ret::Value(h.clone()),
- None => {
- drop(handlers_borrow);
- drop(variant_borrow);
- Ret::Expr(expr)
- }
- },
- (RecordLit(kvs), UnionLit(l, v, _, _, _)) => match kvs.get(l) {
- Some(h) => Ret::Value(h.app(v.clone())),
- None => {
- drop(handlers_borrow);
- drop(variant_borrow);
- Ret::Expr(expr)
- }
- },
- (RecordLit(kvs), EmptyOptionalLit(_)) => {
- match kvs.get(&"None".into()) {
+ match handlers.kind() {
+ RecordLit(kvs) => match variant.kind() {
+ UnionConstructor(l, _, _) => match kvs.get(l) {
Some(h) => Ret::Value(h.clone()),
- None => {
- drop(handlers_borrow);
- drop(variant_borrow);
- Ret::Expr(expr)
- }
- }
- }
- (RecordLit(kvs), NEOptionalLit(v)) => {
- match kvs.get(&"Some".into()) {
+ None => Ret::Expr(expr),
+ },
+ UnionLit(l, v, _, _, _) => match kvs.get(l) {
Some(h) => Ret::Value(h.app(v.clone())),
- None => {
- drop(handlers_borrow);
- drop(variant_borrow);
- Ret::Expr(expr)
- }
- }
- }
- _ => {
- drop(handlers_borrow);
- drop(variant_borrow);
- Ret::Expr(expr)
- }
+ None => Ret::Expr(expr),
+ },
+ EmptyOptionalLit(_) => match kvs.get(&"None".into()) {
+ Some(h) => Ret::Value(h.clone()),
+ None => Ret::Expr(expr),
+ },
+ NEOptionalLit(v) => match kvs.get(&"Some".into()) {
+ Some(h) => Ret::Value(h.app(v.clone())),
+ None => Ret::Expr(expr),
+ },
+ _ => Ret::Expr(expr),
+ },
+ _ => Ret::Expr(expr),
}
}
ExprKind::ToMap(_, _) => unimplemented!("toMap"),
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 212e6e7..e3f57c2 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -197,8 +197,7 @@ fn type_one_layer(
// TODO: branch here only when scrut.get_type() is a Const
_ => {
let scrut_nf = scrut.eval(env.as_nzenv());
- let scrut_nf_borrow = scrut_nf.kind();
- match &*scrut_nf_borrow {
+ match scrut_nf.kind() {
ValueKind::UnionType(kts) => match kts.get(x) {
// Constructor has type T -> < x: T, ... >
Some(Some(ty)) => Value::from_kind_and_type(
@@ -215,7 +214,7 @@ fn type_one_layer(
scrut.get_type()?,
)?,
),
- Some(None) => scrut_nf.clone(),
+ Some(None) => scrut_nf,
None => return mkerr("MissingUnionField"),
},
_ => return mkerr("NotARecord"),
@@ -252,9 +251,7 @@ fn type_one_layer(
t
}
ExprKind::App(f, arg) => {
- let tf = f.get_type()?;
- let tf_borrow = tf.kind();
- match &*tf_borrow {
+ match f.get_type()?.kind() {
ValueKind::PiClosure { annot, closure, .. } => {
if arg.get_type()? != *annot {
// return mkerr(format!("function annot mismatch"));
@@ -295,15 +292,12 @@ fn type_one_layer(
let y_type = y.get_type()?;
// Extract the LHS record type
- let x_type_borrow = x_type.kind();
- let kts_x = match &*x_type_borrow {
+ let kts_x = match x_type.kind() {
ValueKind::RecordType(kts) => kts,
_ => return mkerr("MustCombineRecord"),
};
-
// Extract the RHS record type
- let y_type_borrow = y_type.kind();
- let kts_y = match &*y_type_borrow {
+ let kts_y = match y_type.kind() {
ValueKind::RecordType(kts) => kts,
_ => return mkerr("MustCombineRecord"),
};
@@ -334,13 +328,11 @@ fn type_one_layer(
ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
let x_val = x.eval(env.as_nzenv());
let y_val = y.eval(env.as_nzenv());
- let x_val_borrow = x_val.kind();
- let y_val_borrow = y_val.kind();
- let kts_x = match &*x_val_borrow {
+ let kts_x = match x_val.kind() {
ValueKind::RecordType(kts) => kts,
_ => return mkerr("RecordTypeMergeRequiresRecordType"),
};
- let kts_y = match &*y_val_borrow {
+ let kts_y = match y_val.kind() {
ValueKind::RecordType(kts) => kts,
_ => return mkerr("RecordTypeMergeRequiresRecordType"),
};
@@ -416,15 +408,13 @@ fn type_one_layer(
}
ExprKind::Merge(record, union, type_annot) => {
let record_type = record.get_type()?;
- let record_borrow = record_type.kind();
- let handlers = match &*record_borrow {
+ let handlers = match record_type.kind() {
ValueKind::RecordType(kts) => kts,
_ => return mkerr("Merge1ArgMustBeRecord"),
};
let union_type = union.get_type()?;
- let union_borrow = union_type.kind();
- let variants = match &*union_borrow {
+ let variants = match union_type.kind() {
ValueKind::UnionType(kts) => Cow::Borrowed(kts),
ValueKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::Optional,
@@ -444,21 +434,18 @@ fn type_one_layer(
for (x, handler_type) in handlers {
let handler_return_type = match variants.get(x) {
// Union alternative with type
- Some(Some(variant_type)) => {
- let handler_type_borrow = handler_type.kind();
- match &*handler_type_borrow {
- ValueKind::PiClosure { closure, annot, .. } => {
- if variant_type != annot {
- return mkerr("MergeHandlerTypeMismatch");
- }
-
- closure.remove_binder().or_else(|()| {
- mkerr("MergeReturnTypeIsDependent")
- })?
+ Some(Some(variant_type)) => match handler_type.kind() {
+ ValueKind::PiClosure { closure, annot, .. } => {
+ if variant_type != annot {
+ return mkerr("MergeHandlerTypeMismatch");
}
- _ => return mkerr("NotAFunction"),
+
+ closure.remove_binder().or_else(|()| {
+ mkerr("MergeReturnTypeIsDependent")
+ })?
}
- }
+ _ => return mkerr("NotAFunction"),
+ },
// Union alternative without type
Some(None) => handler_type.clone(),
None => return mkerr("MergeHandlerMissingVariant"),
@@ -495,8 +482,7 @@ fn type_one_layer(
ExprKind::ToMap(_, _) => unimplemented!("toMap"),
ExprKind::Projection(record, labels) => {
let record_type = record.get_type()?;
- let record_type_borrow = record_type.kind();
- let kts = match &*record_type_borrow {
+ let kts = match record_type.kind() {
ValueKind::RecordType(kts) => kts,
_ => return mkerr("ProjectionMustBeRecord"),
};
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 03:04:20 +0000