summaryrefslogtreecommitdiff
path: root/dhall/src/phase
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/phase')
-rw-r--r--dhall/src/phase/normalize.rs199
-rw-r--r--dhall/src/phase/typecheck.rs33
2 files changed, 112 insertions, 120 deletions
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 2253ae0..be2ba51 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -14,6 +14,7 @@ use crate::phase::{NormalizedSubExpr, ResolvedSubExpr, Typed};
pub type InputSubExpr = ResolvedSubExpr;
pub type OutputSubExpr = NormalizedSubExpr;
+#[allow(clippy::cognitive_complexity)]
pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
use dhall_syntax::Builtin::*;
use Value::*;
@@ -206,7 +207,7 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
(NaturalBuild, [f, r..]) => match &*f.as_value() {
// fold/build fusion
Value::AppliedBuiltin(NaturalFold, args) => {
- if args.len() >= 1 {
+ if !args.is_empty() {
Ok((r, args[0].to_value()))
} else {
// Do we really need to handle this case ?
@@ -365,10 +366,10 @@ pub fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
// Small helper enum to avoid repetition
enum Ret<'a> {
- RetValue(Value),
- RetThunk(Thunk),
- RetThunkRef(&'a Thunk),
- RetExpr(ExprF<Thunk, X>),
+ Value(Value),
+ Thunk(Thunk),
+ ThunkRef(&'a Thunk),
+ Expr(ExprF<Thunk, X>),
}
fn merge_maps<K, V>(
@@ -402,7 +403,6 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
RecursiveRecordMerge, RecursiveRecordTypeMerge, RightBiasedRecordMerge,
TextAppend,
};
- use Ret::{RetThunkRef, RetValue};
use Value::{
BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
TextLit,
@@ -410,65 +410,69 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
let x_borrow = x.as_value();
let y_borrow = y.as_value();
Some(match (o, &*x_borrow, &*y_borrow) {
- (BoolAnd, BoolLit(true), _) => RetThunkRef(y),
- (BoolAnd, _, BoolLit(true)) => RetThunkRef(x),
- (BoolAnd, BoolLit(false), _) => RetValue(BoolLit(false)),
- (BoolAnd, _, BoolLit(false)) => RetValue(BoolLit(false)),
- (BoolAnd, _, _) if x == y => RetThunkRef(x),
- (BoolOr, BoolLit(true), _) => RetValue(BoolLit(true)),
- (BoolOr, _, BoolLit(true)) => RetValue(BoolLit(true)),
- (BoolOr, BoolLit(false), _) => RetThunkRef(y),
- (BoolOr, _, BoolLit(false)) => RetThunkRef(x),
- (BoolOr, _, _) if x == y => RetThunkRef(x),
- (BoolEQ, BoolLit(true), _) => RetThunkRef(y),
- (BoolEQ, _, BoolLit(true)) => RetThunkRef(x),
- (BoolEQ, BoolLit(x), BoolLit(y)) => RetValue(BoolLit(x == y)),
- (BoolEQ, _, _) if x == y => RetValue(BoolLit(true)),
- (BoolNE, BoolLit(false), _) => RetThunkRef(y),
- (BoolNE, _, BoolLit(false)) => RetThunkRef(x),
- (BoolNE, BoolLit(x), BoolLit(y)) => RetValue(BoolLit(x != y)),
- (BoolNE, _, _) if x == y => RetValue(BoolLit(false)),
+ (BoolAnd, BoolLit(true), _) => Ret::ThunkRef(y),
+ (BoolAnd, _, BoolLit(true)) => Ret::ThunkRef(x),
+ (BoolAnd, BoolLit(false), _) => Ret::Value(BoolLit(false)),
+ (BoolAnd, _, BoolLit(false)) => Ret::Value(BoolLit(false)),
+ (BoolAnd, _, _) if x == y => Ret::ThunkRef(x),
+ (BoolOr, BoolLit(true), _) => Ret::Value(BoolLit(true)),
+ (BoolOr, _, BoolLit(true)) => Ret::Value(BoolLit(true)),
+ (BoolOr, BoolLit(false), _) => Ret::ThunkRef(y),
+ (BoolOr, _, BoolLit(false)) => Ret::ThunkRef(x),
+ (BoolOr, _, _) if x == y => Ret::ThunkRef(x),
+ (BoolEQ, BoolLit(true), _) => Ret::ThunkRef(y),
+ (BoolEQ, _, BoolLit(true)) => Ret::ThunkRef(x),
+ (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::Value(BoolLit(x == y)),
+ (BoolEQ, _, _) if x == y => Ret::Value(BoolLit(true)),
+ (BoolNE, BoolLit(false), _) => Ret::ThunkRef(y),
+ (BoolNE, _, BoolLit(false)) => Ret::ThunkRef(x),
+ (BoolNE, BoolLit(x), BoolLit(y)) => Ret::Value(BoolLit(x != y)),
+ (BoolNE, _, _) if x == y => Ret::Value(BoolLit(false)),
- (NaturalPlus, NaturalLit(0), _) => RetThunkRef(y),
- (NaturalPlus, _, NaturalLit(0)) => RetThunkRef(x),
+ (NaturalPlus, NaturalLit(0), _) => Ret::ThunkRef(y),
+ (NaturalPlus, _, NaturalLit(0)) => Ret::ThunkRef(x),
(NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
- RetValue(NaturalLit(x + y))
+ Ret::Value(NaturalLit(x + y))
}
- (NaturalTimes, NaturalLit(0), _) => RetValue(NaturalLit(0)),
- (NaturalTimes, _, NaturalLit(0)) => RetValue(NaturalLit(0)),
- (NaturalTimes, NaturalLit(1), _) => RetThunkRef(y),
- (NaturalTimes, _, NaturalLit(1)) => RetThunkRef(x),
+ (NaturalTimes, NaturalLit(0), _) => Ret::Value(NaturalLit(0)),
+ (NaturalTimes, _, NaturalLit(0)) => Ret::Value(NaturalLit(0)),
+ (NaturalTimes, NaturalLit(1), _) => Ret::ThunkRef(y),
+ (NaturalTimes, _, NaturalLit(1)) => Ret::ThunkRef(x),
(NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
- RetValue(NaturalLit(x * y))
+ Ret::Value(NaturalLit(x * y))
}
- (ListAppend, EmptyListLit(_), _) => RetThunkRef(y),
- (ListAppend, _, EmptyListLit(_)) => RetThunkRef(x),
+ (ListAppend, EmptyListLit(_), _) => Ret::ThunkRef(y),
+ (ListAppend, _, EmptyListLit(_)) => Ret::ThunkRef(x),
(ListAppend, NEListLit(xs), NEListLit(ys)) => {
- RetValue(NEListLit(xs.iter().chain(ys.iter()).cloned().collect()))
+ Ret::Value(NEListLit(xs.iter().chain(ys.iter()).cloned().collect()))
}
- (TextAppend, TextLit(x), _) if x.is_empty() => RetThunkRef(y),
- (TextAppend, _, TextLit(y)) if y.is_empty() => RetThunkRef(x),
- (TextAppend, TextLit(x), TextLit(y)) => {
- RetValue(TextLit(squash_textlit(x.iter().chain(y.iter()).cloned())))
- }
+ (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ThunkRef(y),
+ (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ThunkRef(x),
+ (TextAppend, TextLit(x), TextLit(y)) => Ret::Value(TextLit(
+ squash_textlit(x.iter().chain(y.iter()).cloned()),
+ )),
(TextAppend, TextLit(x), _) => {
use std::iter::once;
let y = InterpolatedTextContents::Expr(y.clone());
- RetValue(TextLit(squash_textlit(x.iter().cloned().chain(once(y)))))
+ Ret::Value(TextLit(squash_textlit(
+ x.iter().cloned().chain(once(y)),
+ )))
}
(TextAppend, _, TextLit(y)) => {
use std::iter::once;
let x = InterpolatedTextContents::Expr(x.clone());
- RetValue(TextLit(squash_textlit(once(x).chain(y.iter().cloned()))))
+ Ret::Value(TextLit(squash_textlit(
+ once(x).chain(y.iter().cloned()),
+ )))
}
(RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
- RetThunkRef(x)
+ Ret::ThunkRef(x)
}
(RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
- RetThunkRef(y)
+ Ret::ThunkRef(y)
}
(RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
let mut kvs = kvs2.clone();
@@ -476,14 +480,14 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
// Insert only if key not already present
kvs.entry(x.clone()).or_insert_with(|| v.clone());
}
- RetValue(RecordLit(kvs))
+ Ret::Value(RecordLit(kvs))
}
(RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
- RetThunkRef(x)
+ Ret::ThunkRef(x)
}
(RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
- RetThunkRef(y)
+ Ret::ThunkRef(y)
}
(RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
@@ -493,14 +497,14 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
v2.clone(),
))
});
- RetValue(RecordLit(kvs))
+ Ret::Value(RecordLit(kvs))
}
(RecursiveRecordTypeMerge, _, RecordType(kvs)) if kvs.is_empty() => {
- RetThunkRef(x)
+ Ret::ThunkRef(x)
}
(RecursiveRecordTypeMerge, RecordType(kvs), _) if kvs.is_empty() => {
- RetThunkRef(y)
+ Ret::ThunkRef(y)
}
(RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => {
let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
@@ -510,7 +514,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
v2.to_thunk(),
)))
});
- RetValue(RecordType(kvs))
+ Ret::Value(RecordType(kvs))
}
_ => return None,
@@ -518,7 +522,6 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
}
pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
- use Ret::{RetExpr, RetThunk, RetThunkRef, RetValue};
use Value::{
BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit, Lam,
NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
@@ -528,51 +531,53 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
let ret = match expr {
ExprF::Embed(_) => unreachable!(),
ExprF::Var(_) => unreachable!(),
- ExprF::Annot(x, _) => RetThunk(x),
+ ExprF::Annot(x, _) => Ret::Thunk(x),
ExprF::Lam(x, t, e) => {
- RetValue(Lam(x.into(), TypeThunk::from_thunk(t), e))
+ Ret::Value(Lam(x.into(), TypeThunk::from_thunk(t), e))
}
- ExprF::Pi(x, t, e) => RetValue(Pi(
+ ExprF::Pi(x, t, e) => Ret::Value(Pi(
x.into(),
TypeThunk::from_thunk(t),
TypeThunk::from_thunk(e),
)),
ExprF::Let(x, _, v, b) => {
let v = Typed::from_thunk_untyped(v);
- RetThunk(b.subst_shift(&x.into(), &v))
- }
- ExprF::App(v, a) => RetValue(v.app_thunk(a)),
- ExprF::Builtin(b) => RetValue(Value::from_builtin(b)),
- ExprF::Const(c) => RetValue(Value::Const(c)),
- ExprF::BoolLit(b) => RetValue(BoolLit(b)),
- ExprF::NaturalLit(n) => RetValue(NaturalLit(n)),
- ExprF::IntegerLit(n) => RetValue(IntegerLit(n)),
- ExprF::DoubleLit(n) => RetValue(DoubleLit(n)),
+ Ret::Thunk(b.subst_shift(&x.into(), &v))
+ }
+ ExprF::App(v, a) => Ret::Value(v.app_thunk(a)),
+ ExprF::Builtin(b) => Ret::Value(Value::from_builtin(b)),
+ ExprF::Const(c) => Ret::Value(Value::Const(c)),
+ ExprF::BoolLit(b) => Ret::Value(BoolLit(b)),
+ ExprF::NaturalLit(n) => Ret::Value(NaturalLit(n)),
+ ExprF::IntegerLit(n) => Ret::Value(IntegerLit(n)),
+ ExprF::DoubleLit(n) => Ret::Value(DoubleLit(n)),
ExprF::OldOptionalLit(None, t) => {
- RetValue(EmptyOptionalLit(TypeThunk::from_thunk(t)))
+ Ret::Value(EmptyOptionalLit(TypeThunk::from_thunk(t)))
}
- ExprF::OldOptionalLit(Some(e), _) => RetValue(NEOptionalLit(e)),
- ExprF::SomeLit(e) => RetValue(NEOptionalLit(e)),
+ ExprF::OldOptionalLit(Some(e), _) => Ret::Value(NEOptionalLit(e)),
+ ExprF::SomeLit(e) => Ret::Value(NEOptionalLit(e)),
ExprF::EmptyListLit(t) => {
- RetValue(EmptyListLit(TypeThunk::from_thunk(t)))
+ Ret::Value(EmptyListLit(TypeThunk::from_thunk(t)))
}
ExprF::NEListLit(elts) => {
- RetValue(NEListLit(elts.into_iter().collect()))
+ Ret::Value(NEListLit(elts.into_iter().collect()))
+ }
+ ExprF::RecordLit(kvs) => {
+ Ret::Value(RecordLit(kvs.into_iter().collect()))
}
- ExprF::RecordLit(kvs) => RetValue(RecordLit(kvs.into_iter().collect())),
- ExprF::RecordType(kts) => RetValue(RecordType(
+ ExprF::RecordType(kts) => Ret::Value(RecordType(
kts.into_iter()
.map(|(k, t)| (k, TypeThunk::from_thunk(t)))
.collect(),
)),
- ExprF::UnionLit(l, x, kts) => RetValue(UnionLit(
+ ExprF::UnionLit(l, x, kts) => Ret::Value(UnionLit(
l,
x,
kts.into_iter()
.map(|(k, t)| (k, t.map(|t| TypeThunk::from_thunk(t))))
.collect(),
)),
- ExprF::UnionType(kts) => RetValue(UnionType(
+ ExprF::UnionType(kts) => Ret::Value(UnionType(
kts.into_iter()
.map(|(k, t)| (k, t.map(|t| TypeThunk::from_thunk(t))))
.collect(),
@@ -582,28 +587,28 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
let elts: Vec<_> = squash_textlit(elts.into_iter());
// Simplify bare interpolation
if let [Expr(th)] = elts.as_slice() {
- RetThunk(th.clone())
+ Ret::Thunk(th.clone())
} else {
- RetValue(TextLit(elts))
+ Ret::Value(TextLit(elts))
}
}
ExprF::BoolIf(ref b, ref e1, ref e2) => {
let b_borrow = b.as_value();
match &*b_borrow {
- BoolLit(true) => RetThunkRef(e1),
- BoolLit(false) => RetThunkRef(e2),
+ BoolLit(true) => Ret::ThunkRef(e1),
+ BoolLit(false) => Ret::ThunkRef(e2),
_ => {
let e1_borrow = e1.as_value();
let e2_borrow = e2.as_value();
match (&*e1_borrow, &*e2_borrow) {
// Simplify `if b then True else False`
- (BoolLit(true), BoolLit(false)) => RetThunkRef(b),
- _ if e1 == e2 => RetThunkRef(e1),
+ (BoolLit(true), BoolLit(false)) => Ret::ThunkRef(b),
+ _ if e1 == e2 => Ret::ThunkRef(e1),
_ => {
drop(b_borrow);
drop(e1_borrow);
drop(e2_borrow);
- RetExpr(expr)
+ Ret::Expr(expr)
}
}
}
@@ -611,16 +616,16 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
}
ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) {
Some(ret) => ret,
- None => RetExpr(expr),
+ None => Ret::Expr(expr),
},
ExprF::Projection(_, ls) if ls.is_empty() => {
- RetValue(RecordLit(HashMap::new()))
+ Ret::Value(RecordLit(HashMap::new()))
}
ExprF::Projection(ref v, ref ls) => {
let v_borrow = v.as_value();
match &*v_borrow {
- RecordLit(kvs) => RetValue(RecordLit(
+ RecordLit(kvs) => Ret::Value(RecordLit(
ls.iter()
.filter_map(|l| {
kvs.get(l).map(|x| (l.clone(), x.clone()))
@@ -629,7 +634,7 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
)),
_ => {
drop(v_borrow);
- RetExpr(expr)
+ Ret::Expr(expr)
}
}
}
@@ -637,18 +642,18 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
let v_borrow = v.as_value();
match &*v_borrow {
RecordLit(kvs) => match kvs.get(l) {
- Some(r) => RetThunk(r.clone()),
+ Some(r) => Ret::Thunk(r.clone()),
None => {
drop(v_borrow);
- RetExpr(expr)
+ Ret::Expr(expr)
}
},
UnionType(kts) => {
- RetValue(UnionConstructor(l.clone(), kts.clone()))
+ Ret::Value(UnionConstructor(l.clone(), kts.clone()))
}
_ => {
drop(v_borrow);
- RetExpr(expr)
+ Ret::Expr(expr)
}
}
}
@@ -658,34 +663,34 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
let variant_borrow = variant.as_value();
match (&*handlers_borrow, &*variant_borrow) {
(RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) {
- Some(h) => RetThunk(h.clone()),
+ Some(h) => Ret::Thunk(h.clone()),
None => {
drop(handlers_borrow);
drop(variant_borrow);
- RetExpr(expr)
+ Ret::Expr(expr)
}
},
(RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
- Some(h) => RetValue(h.app_thunk(v.clone())),
+ Some(h) => Ret::Value(h.app_thunk(v.clone())),
None => {
drop(handlers_borrow);
drop(variant_borrow);
- RetExpr(expr)
+ Ret::Expr(expr)
}
},
_ => {
drop(handlers_borrow);
drop(variant_borrow);
- RetExpr(expr)
+ Ret::Expr(expr)
}
}
}
};
match ret {
- RetValue(v) => v,
- RetThunk(th) => th.to_value(),
- RetThunkRef(th) => th.to_value(),
- RetExpr(expr) => Value::PartialExpr(expr),
+ Ret::Value(v) => v,
+ Ret::Thunk(th) => th.to_value(),
+ Ret::ThunkRef(th) => th.to_value(),
+ Ret::Expr(expr) => Value::PartialExpr(expr),
}
}
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index bb36060..419b2e2 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -1,5 +1,3 @@
-#![allow(non_snake_case)]
-use std::borrow::Borrow;
use std::collections::HashMap;
use dhall_proc_macros as dhall;
@@ -17,7 +15,7 @@ use crate::phase::{Normalized, Resolved, Type, Typed};
macro_rules! ensure_equal {
($x:expr, $y:expr, $err:expr $(,)*) => {
- if !prop_equal($x, $y) {
+ if $x.to_value() != $y.to_value() {
return Err($err);
}
};
@@ -42,7 +40,7 @@ fn tck_pi_type(
use crate::error::TypeMessage::*;
let ctx2 = ctx.insert_type(&x, tx.clone());
- let kA = match tx.get_type()?.as_const() {
+ let ka = match tx.get_type()?.as_const() {
Some(k) => k,
_ => {
return Err(TypeError::new(
@@ -52,7 +50,7 @@ fn tck_pi_type(
}
};
- let kB = match te.get_type()?.as_const() {
+ let kb = match te.get_type()?.as_const() {
Some(k) => k,
_ => {
return Err(TypeError::new(
@@ -62,7 +60,7 @@ fn tck_pi_type(
}
};
- let k = match function_check(kA, kB) {
+ let k = match function_check(ka, kb) {
Ok(k) => k,
Err(()) => {
return Err(TypeError::new(
@@ -109,7 +107,7 @@ fn tck_record_type(
return Err(TypeError::new(ctx, RecordTypeDuplicateField))
}
Entry::Vacant(_) => {
- entry.or_insert(TypeThunk::from_type(t.clone()))
+ entry.or_insert_with(|| TypeThunk::from_type(t.clone()))
}
};
}
@@ -150,8 +148,9 @@ fn tck_union_type(
Entry::Occupied(_) => {
return Err(TypeError::new(ctx, UnionTypeDuplicateField))
}
- Entry::Vacant(_) => entry
- .or_insert(t.as_ref().map(|t| TypeThunk::from_type(t.clone()))),
+ Entry::Vacant(_) => entry.or_insert_with(|| {
+ t.as_ref().map(|t| TypeThunk::from_type(t.clone()))
+ }),
};
}
@@ -207,24 +206,12 @@ fn function_check(a: Const, b: Const) -> Result<Const, ()> {
}
}
-// Equality up to alpha-equivalence (renaming of bound variables)
-fn prop_equal<T, U>(eL0: T, eR0: U) -> bool
-where
- T: Borrow<Type>,
- U: Borrow<Type>,
-{
- eL0.borrow().to_value() == eR0.borrow().to_value()
-}
-
pub fn type_of_const(c: Const) -> Result<Type, TypeError> {
match c {
Const::Type => Ok(Type::from_const(Const::Kind)),
Const::Kind => Ok(Type::from_const(Const::Sort)),
Const::Sort => {
- return Err(TypeError::new(
- &TypecheckContext::new(),
- TypeMessage::Sort,
- ))
+ Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
}
}
}
@@ -728,7 +715,7 @@ fn type_last_layer(
}
(Some(t), None) => Ok(RetTypeOnly(t)),
(None, Some(t)) => Ok(RetTypeOnly(t.to_type())),
- (None, None) => return Err(mkerr(MergeEmptyNeedsAnnotation)),
+ (None, None) => Err(mkerr(MergeEmptyNeedsAnnotation)),
}
}
Projection(record, labels) => {