diff options
Diffstat (limited to 'dhall/src/phase')
| -rw-r--r-- | dhall/src/phase/normalize.rs | 199 | ||||
| -rw-r--r-- | dhall/src/phase/typecheck.rs | 33 |
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) => { |