diff options
author | Nadrieril Feneanar | 2019-08-20 14:10:54 +0200 |
---|---|---|
committer | GitHub | 2019-08-20 14:10:54 +0200 |
commit | 9470664a5e481c63fd96939e7b8986b8fe881dbe (patch) | |
tree | 13bab9e1145a8769b6dd4ca1d76d34af1ff6c12b /dhall/src/phase/normalize.rs | |
parent | 88ebc0f9d561a2541aad84a3152511a0439db8b4 (diff) | |
parent | caf36246a517b884d7cfcf7c31e1b5d8fce60dfa (diff) |
Merge pull request #104 from Nadrieril/rework-value
Rework Value
Diffstat (limited to 'dhall/src/phase/normalize.rs')
-rw-r--r-- | dhall/src/phase/normalize.rs | 588 |
1 files changed, 273 insertions, 315 deletions
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index fd0197d..a379a4b 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -5,13 +5,11 @@ use dhall_syntax::{ NaiveDouble, }; -use crate::core::context::NormalizationContext; -use crate::core::thunk::{Thunk, TypedThunk}; use crate::core::value::Value; +use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; -use crate::phase::{Normalized, NormalizedSubExpr, ResolvedSubExpr, Typed}; +use crate::phase::{Normalized, NormalizedSubExpr}; -pub(crate) type InputSubExpr = ResolvedSubExpr; pub(crate) type OutputSubExpr = NormalizedSubExpr; // Ad-hoc macro to help construct closures @@ -22,67 +20,76 @@ macro_rules! make_closure { Label::from(stringify!($var)).into(), $n ); - Value::Var(var).into_thunk() + ValueF::Var(var).into_value_untyped() }}; + // Warning: assumes that $ty, as a dhall value, has type `Type` (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { - Value::Lam( + ValueF::Lam( Label::from(stringify!($var)).into(), - TypedThunk::from_thunk_untyped(make_closure!($($ty)*)), + make_closure!($($ty)*), make_closure!($($rest)*), - ).into_thunk() + ).into_value_untyped() + }; + (Natural) => { + ValueF::from_builtin(Builtin::Natural) + .into_value_simple_type() }; - (Natural) => { Value::from_builtin(Builtin::Natural).into_thunk() }; (List $($rest:tt)*) => { - Value::from_builtin(Builtin::List) - .app_thunk(make_closure!($($rest)*)) - .into_thunk() + ValueF::from_builtin(Builtin::List) + .app_value(make_closure!($($rest)*)) + .into_value_simple_type() }; - (Some $($rest:tt)*) => { - Value::NEOptionalLit(make_closure!($($rest)*)).into_thunk() + (Some($($rest:tt)*)) => { + ValueF::NEOptionalLit(make_closure!($($rest)*)) + .into_value_untyped() }; (1 + $($rest:tt)*) => { - Value::PartialExpr(ExprF::BinOp( + ValueF::PartialExpr(ExprF::BinOp( dhall_syntax::BinOp::NaturalPlus, make_closure!($($rest)*), - Thunk::from_value(Value::NaturalLit(1)), - )).into_thunk() + Value::from_valuef_and_type( + ValueF::NaturalLit(1), + make_closure!(Natural) + ), + )).into_value_with_type( + make_closure!(Natural) + ) }; ([ $($head:tt)* ] # $($tail:tt)*) => { - Value::PartialExpr(ExprF::BinOp( + ValueF::PartialExpr(ExprF::BinOp( dhall_syntax::BinOp::ListAppend, - Value::NEListLit(vec![make_closure!($($head)*)]).into_thunk(), + ValueF::NEListLit(vec![make_closure!($($head)*)]) + .into_value_untyped(), make_closure!($($tail)*), - )).into_thunk() + )).into_value_untyped() }; } #[allow(clippy::cognitive_complexity)] -pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { +pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { use dhall_syntax::Builtin::*; - use Value::*; + use ValueF::*; // Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced. let ret = match (b, args.as_slice()) { - (OptionalNone, [t, r..]) => { - Ok((r, EmptyOptionalLit(TypedThunk::from_thunk(t.clone())))) - } - (NaturalIsZero, [n, r..]) => match &*n.as_value() { + (OptionalNone, [t, r..]) => Ok((r, EmptyOptionalLit(t.clone()))), + (NaturalIsZero, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok((r, BoolLit(*n == 0))), _ => Err(()), }, - (NaturalEven, [n, r..]) => match &*n.as_value() { + (NaturalEven, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0))), _ => Err(()), }, - (NaturalOdd, [n, r..]) => match &*n.as_value() { + (NaturalOdd, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0))), _ => Err(()), }, - (NaturalToInteger, [n, r..]) => match &*n.as_value() { + (NaturalToInteger, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok((r, IntegerLit(*n as isize))), _ => Err(()), }, - (NaturalShow, [n, r..]) => match &*n.as_value() { + (NaturalShow, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok(( r, TextLit(vec![InterpolatedTextContents::Text(n.to_string())]), @@ -90,7 +97,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { _ => Err(()), }, (NaturalSubtract, [a, b, r..]) => { - match (&*a.as_value(), &*b.as_value()) { + match (&*a.as_whnf(), &*b.as_whnf()) { (NaturalLit(a), NaturalLit(b)) => { Ok((r, NaturalLit(if b > a { b - a } else { 0 }))) } @@ -100,7 +107,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { _ => Err(()), } } - (IntegerShow, [n, r..]) => match &*n.as_value() { + (IntegerShow, [n, r..]) => match &*n.as_whnf() { IntegerLit(n) => { let s = if *n < 0 { n.to_string() @@ -111,18 +118,18 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { } _ => Err(()), }, - (IntegerToDouble, [n, r..]) => match &*n.as_value() { + (IntegerToDouble, [n, r..]) => match &*n.as_whnf() { IntegerLit(n) => Ok((r, DoubleLit(NaiveDouble::from(*n as f64)))), _ => Err(()), }, - (DoubleShow, [n, r..]) => match &*n.as_value() { + (DoubleShow, [n, r..]) => match &*n.as_whnf() { DoubleLit(n) => Ok(( r, TextLit(vec![InterpolatedTextContents::Text(n.to_string())]), )), _ => Err(()), }, - (TextShow, [v, r..]) => match &*v.as_value() { + (TextShow, [v, r..]) => match &*v.as_whnf() { TextLit(elts) => { match elts.as_slice() { // Empty string literal. @@ -156,41 +163,44 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { } _ => Err(()), }, - (ListLength, [_, l, r..]) => match &*l.as_value() { + (ListLength, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(_) => Ok((r, NaturalLit(0))), NEListLit(xs) => Ok((r, NaturalLit(xs.len()))), _ => Err(()), }, - (ListHead, [_, l, r..]) => match &*l.as_value() { + (ListHead, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))), NEListLit(xs) => { Ok((r, NEOptionalLit(xs.iter().next().unwrap().clone()))) } _ => Err(()), }, - (ListLast, [_, l, r..]) => match &*l.as_value() { + (ListLast, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))), NEListLit(xs) => { Ok((r, NEOptionalLit(xs.iter().rev().next().unwrap().clone()))) } _ => Err(()), }, - (ListReverse, [_, l, r..]) => match &*l.as_value() { + (ListReverse, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()))), NEListLit(xs) => { Ok((r, NEListLit(xs.iter().rev().cloned().collect()))) } _ => Err(()), }, - (ListIndexed, [_, l, r..]) => match &*l.as_value() { + (ListIndexed, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(t) => { let mut kts = HashMap::new(); kts.insert( "index".into(), - TypedThunk::from_value(Value::from_builtin(Natural)), + Value::from_valuef_untyped(ValueF::from_builtin(Natural)), ); kts.insert("value".into(), t.clone()); - Ok((r, EmptyListLit(TypedThunk::from_value(RecordType(kts))))) + Ok(( + r, + EmptyListLit(Value::from_valuef_untyped(RecordType(kts))), + )) } NEListLit(xs) => { let xs = xs @@ -199,105 +209,131 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { .map(|(i, e)| { let i = NaturalLit(i); let mut kvs = HashMap::new(); - kvs.insert("index".into(), Thunk::from_value(i)); + kvs.insert( + "index".into(), + Value::from_valuef_untyped(i), + ); kvs.insert("value".into(), e.clone()); - Thunk::from_value(RecordLit(kvs)) + Value::from_valuef_untyped(RecordLit(kvs)) }) .collect(); Ok((r, NEListLit(xs))) } _ => Err(()), }, - (ListBuild, [t, f, r..]) => match &*f.as_value() { + (ListBuild, [t, f, r..]) => match &*f.as_whnf() { // fold/build fusion - Value::AppliedBuiltin(ListFold, args) => { + ValueF::AppliedBuiltin(ListFold, args) => { if args.len() >= 2 { - Ok((r, args[1].to_value())) + Ok((r, args[1].to_whnf())) } else { // Do we really need to handle this case ? unimplemented!() } } - _ => Ok(( - r, - f.app_val(Value::from_builtin(List).app_thunk(t.clone())) - .app_thunk({ - // Move `t` under new `x` variable - let t1 = t.under_binder(Label::from("x")); - make_closure!( - λ(x : #t) -> - λ(xs : List #t1) -> - [ var(x, 1) ] # var(xs, 0) - ) - }) - .app_val(EmptyListLit(TypedThunk::from_thunk(t.clone()))), - )), + _ => { + let list_t = ValueF::from_builtin(List) + .app_value(t.clone()) + .into_value_simple_type(); + Ok(( + r, + f.app_value(list_t.clone()) + .app_value({ + // Move `t` under new `x` variable + let t1 = t.under_binder(Label::from("x")); + make_closure!( + λ(x : #t) -> + λ(xs : List #t1) -> + [ var(x, 1) ] # var(xs, 0) + ) + }) + .app_value( + EmptyListLit(t.clone()) + .into_value_with_type(list_t), + ), + )) + } }, - (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_value() { - EmptyListLit(_) => Ok((r, nil.to_value())), + (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() { + EmptyListLit(_) => Ok((r, nil.to_whnf())), NEListLit(xs) => { let mut v = nil.clone(); for x in xs.iter().rev() { v = cons .clone() - .app_thunk(x.clone()) - .app_thunk(v) - .into_thunk(); + .app_value(x.clone()) + .app_value(v) + .into_value_untyped(); } - Ok((r, v.to_value())) + Ok((r, v.to_whnf())) } _ => Err(()), }, - (OptionalBuild, [t, f, r..]) => match &*f.as_value() { + (OptionalBuild, [t, f, r..]) => match &*f.as_whnf() { // fold/build fusion - Value::AppliedBuiltin(OptionalFold, args) => { + ValueF::AppliedBuiltin(OptionalFold, args) => { if args.len() >= 2 { - Ok((r, args[1].to_value())) + Ok((r, args[1].to_whnf())) } else { // Do we really need to handle this case ? unimplemented!() } } - _ => Ok(( - r, - f.app_val(Value::from_builtin(Optional).app_thunk(t.clone())) - .app_thunk(make_closure!(λ(x: #t) -> Some var(x, 0))) - .app_val(EmptyOptionalLit(TypedThunk::from_thunk( - t.clone(), - ))), - )), + _ => { + let optional_t = ValueF::from_builtin(Optional) + .app_value(t.clone()) + .into_value_simple_type(); + Ok(( + r, + f.app_value(optional_t.clone()) + .app_value(make_closure!(λ(x: #t) -> Some(var(x, 0)))) + .app_value( + EmptyOptionalLit(t.clone()) + .into_value_with_type(optional_t), + ), + )) + } }, - (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_value() { - EmptyOptionalLit(_) => Ok((r, nothing.to_value())), - NEOptionalLit(x) => Ok((r, just.app_thunk(x.clone()))), + (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() { + EmptyOptionalLit(_) => Ok((r, nothing.to_whnf())), + NEOptionalLit(x) => Ok((r, just.app_value(x.clone()))), _ => Err(()), }, - (NaturalBuild, [f, r..]) => match &*f.as_value() { + (NaturalBuild, [f, r..]) => match &*f.as_whnf() { // fold/build fusion - Value::AppliedBuiltin(NaturalFold, args) => { + ValueF::AppliedBuiltin(NaturalFold, args) => { if !args.is_empty() { - Ok((r, args[0].to_value())) + Ok((r, args[0].to_whnf())) } else { // Do we really need to handle this case ? unimplemented!() } } - _ => Ok(( - r, - f.app_val(Value::from_builtin(Natural)) - .app_thunk(make_closure!(λ(x : Natural) -> 1 + var(x, 0))) - .app_val(NaturalLit(0)), - )), + _ => { + let nat_type = + ValueF::from_builtin(Natural).into_value_simple_type(); + Ok(( + r, + f.app_value(nat_type.clone()) + .app_value( + make_closure!(λ(x : Natural) -> 1 + var(x, 0)), + ) + .app_value( + NaturalLit(0).into_value_with_type(nat_type), + ), + )) + } }, - (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_value() { - NaturalLit(0) => Ok((r, zero.to_value())), + (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() { + NaturalLit(0) => Ok((r, zero.to_whnf())), NaturalLit(n) => { - let fold = Value::from_builtin(NaturalFold) + let fold = ValueF::from_builtin(NaturalFold) .app(NaturalLit(n - 1)) - .app_thunk(t.clone()) - .app_thunk(succ.clone()) - .app_thunk(zero.clone()); - Ok((r, succ.app_val(fold))) + .app_value(t.clone()) + .app_value(succ.clone()) + .app_value(zero.clone()) + .into_value_with_type(t.clone()); + Ok((r, succ.app_value(fold))) } _ => Err(()), }, @@ -307,7 +343,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { Ok((unconsumed_args, mut v)) => { let n_consumed_args = args.len() - unconsumed_args.len(); for x in args.into_iter().skip(n_consumed_args) { - v = v.app_thunk(x); + v = v.app_value(x); } v } @@ -315,22 +351,19 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { } } -pub(crate) fn apply_any(f: Thunk, a: Thunk) -> Value { - let fallback = |f: Thunk, a: Thunk| Value::PartialExpr(ExprF::App(f, a)); +pub(crate) fn apply_any(f: Value, a: Value) -> ValueF { + let fallback = |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a)); - let f_borrow = f.as_value(); + let f_borrow = f.as_whnf(); match &*f_borrow { - Value::Lam(x, _, e) => { - let val = Typed::from_thunk_untyped(a); - e.subst_shift(&x.into(), &val).to_value() - } - Value::AppliedBuiltin(b, args) => { + ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).to_whnf(), + ValueF::AppliedBuiltin(b, args) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); apply_builtin(*b, args) } - Value::UnionConstructor(l, kts) => { - Value::UnionLit(l.clone(), a, kts.clone()) + ValueF::UnionConstructor(l, kts) => { + ValueF::UnionLit(l.clone(), a, kts.clone()) } _ => { drop(f_borrow); @@ -340,23 +373,23 @@ pub(crate) fn apply_any(f: Thunk, a: Thunk) -> Value { } pub(crate) fn squash_textlit( - elts: impl Iterator<Item = InterpolatedTextContents<Thunk>>, -) -> Vec<InterpolatedTextContents<Thunk>> { + elts: impl Iterator<Item = InterpolatedTextContents<Value>>, +) -> Vec<InterpolatedTextContents<Value>> { use std::mem::replace; use InterpolatedTextContents::{Expr, Text}; fn inner( - elts: impl Iterator<Item = InterpolatedTextContents<Thunk>>, + elts: impl Iterator<Item = InterpolatedTextContents<Value>>, crnt_str: &mut String, - ret: &mut Vec<InterpolatedTextContents<Thunk>>, + ret: &mut Vec<InterpolatedTextContents<Value>>, ) { for contents in elts { match contents { Text(s) => crnt_str.push_str(&s), Expr(e) => { - let e_borrow = e.as_value(); + let e_borrow = e.as_whnf(); match &*e_borrow { - Value::TextLit(elts2) => { + ValueF::TextLit(elts2) => { inner(elts2.iter().cloned(), crnt_str, ret) } _ => { @@ -381,32 +414,6 @@ pub(crate) fn squash_textlit( ret } -/// Reduces the imput expression to a Value. Evaluates as little as possible. -pub(crate) fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value { - match expr.as_ref() { - ExprF::Embed(e) => return e.to_value(), - ExprF::Var(v) => return ctx.lookup(v), - _ => {} - } - - // Thunk subexpressions - let expr: ExprF<Thunk, Normalized> = - expr.as_ref().map_ref_with_special_handling_of_binders( - |e| Thunk::new(ctx.clone(), e.clone()), - |x, e| Thunk::new(ctx.skip(x), e.clone()), - ); - - normalize_one_layer(expr) -} - -// Small helper enum to avoid repetition -enum Ret<'a> { - Value(Value), - Thunk(Thunk), - ThunkRef(&'a Thunk), - Expr(ExprF<Thunk, Normalized>), -} - /// Performs an intersection of two HashMaps. /// /// # Arguments @@ -441,60 +448,6 @@ where kvs } -/// Performs an outer join of two HashMaps. -/// -/// # Arguments -/// -/// * `ft` - Will convert the values of the first map -/// into the target value. -/// -/// * `fu` - Will convert the values of the second map -/// into the target value. -/// -/// * `fktu` - Will convert the key and values from both maps -/// into the target type. -/// -/// # Description -/// -/// If the key is present in both maps then the final value for -/// that key is computed via the `fktu` function. Otherwise, the -/// final value will be calculated by either the `ft` or `fu` value -/// depending on which map the key is present in. -/// -/// The final map will contain all keys from the two input maps with -/// also values computed as per above. -pub(crate) fn outer_join<K, T, U, V>( - mut ft: impl FnMut(&T) -> V, - mut fu: impl FnMut(&U) -> V, - mut fktu: impl FnMut(&K, &T, &U) -> V, - map1: &HashMap<K, T>, - map2: &HashMap<K, U>, -) -> HashMap<K, V> -where - K: std::hash::Hash + Eq + Clone, -{ - let mut kvs = HashMap::new(); - - for (k1, t) in map1 { - let v = if let Some(u) = map2.get(k1) { - // The key exists in both maps - // so use all values for computation - fktu(k1, t, u) - } else { - // Key only exists in map1 - ft(t) - }; - kvs.insert(k1.clone(), v); - } - - for (k1, u) in map2 { - // Insert if key was missing in map1 - kvs.entry(k1.clone()).or_insert(fu(u)); - } - - kvs -} - pub(crate) fn merge_maps<K, V>( map1: &HashMap<K, V>, map2: &HashMap<K, V>, @@ -520,82 +473,90 @@ where kvs } -fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> { +// Small helper enum to avoid repetition +enum Ret<'a> { + ValueF(ValueF), + Value(Value), + ValueRef(&'a Value), + Expr(ExprF<Value, Normalized>), +} + +fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> { use BinOp::{ BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus, NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, RightBiasedRecordMerge, TextAppend, }; - use Value::{ + use ValueF::{ BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, TextLit, }; - let x_borrow = x.as_value(); - let y_borrow = y.as_value(); + let x_borrow = x.as_whnf(); + let y_borrow = y.as_whnf(); Some(match (o, &*x_borrow, &*y_borrow) { - (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), _) => Ret::ThunkRef(y), - (NaturalPlus, _, NaturalLit(0)) => Ret::ThunkRef(x), + (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y), + (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x), + (BoolAnd, BoolLit(false), _) => Ret::ValueF(BoolLit(false)), + (BoolAnd, _, BoolLit(false)) => Ret::ValueF(BoolLit(false)), + (BoolAnd, _, _) if x == y => Ret::ValueRef(x), + (BoolOr, BoolLit(true), _) => Ret::ValueF(BoolLit(true)), + (BoolOr, _, BoolLit(true)) => Ret::ValueF(BoolLit(true)), + (BoolOr, BoolLit(false), _) => Ret::ValueRef(y), + (BoolOr, _, BoolLit(false)) => Ret::ValueRef(x), + (BoolOr, _, _) if x == y => Ret::ValueRef(x), + (BoolEQ, BoolLit(true), _) => Ret::ValueRef(y), + (BoolEQ, _, BoolLit(true)) => Ret::ValueRef(x), + (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x == y)), + (BoolEQ, _, _) if x == y => Ret::ValueF(BoolLit(true)), + (BoolNE, BoolLit(false), _) => Ret::ValueRef(y), + (BoolNE, _, BoolLit(false)) => Ret::ValueRef(x), + (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x != y)), + (BoolNE, _, _) if x == y => Ret::ValueF(BoolLit(false)), + + (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y), + (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x), (NaturalPlus, NaturalLit(x), NaturalLit(y)) => { - Ret::Value(NaturalLit(x + y)) + Ret::ValueF(NaturalLit(x + y)) } - (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(0), _) => Ret::ValueF(NaturalLit(0)), + (NaturalTimes, _, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)), + (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y), + (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x), (NaturalTimes, NaturalLit(x), NaturalLit(y)) => { - Ret::Value(NaturalLit(x * y)) + Ret::ValueF(NaturalLit(x * y)) } - (ListAppend, EmptyListLit(_), _) => Ret::ThunkRef(y), - (ListAppend, _, EmptyListLit(_)) => Ret::ThunkRef(x), - (ListAppend, NEListLit(xs), NEListLit(ys)) => { - Ret::Value(NEListLit(xs.iter().chain(ys.iter()).cloned().collect())) - } + (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y), + (ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x), + (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueF(NEListLit( + xs.iter().chain(ys.iter()).cloned().collect(), + )), - (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( + (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ValueRef(y), + (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ValueRef(x), + (TextAppend, TextLit(x), TextLit(y)) => Ret::ValueF(TextLit( squash_textlit(x.iter().chain(y.iter()).cloned()), )), (TextAppend, TextLit(x), _) => { use std::iter::once; let y = InterpolatedTextContents::Expr(y.clone()); - Ret::Value(TextLit(squash_textlit( + Ret::ValueF(TextLit(squash_textlit( x.iter().cloned().chain(once(y)), ))) } (TextAppend, _, TextLit(y)) => { use std::iter::once; let x = InterpolatedTextContents::Expr(x.clone()); - Ret::Value(TextLit(squash_textlit( + Ret::ValueF(TextLit(squash_textlit( once(x).chain(y.iter().cloned()), ))) } (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::ThunkRef(x) + Ret::ValueRef(x) } (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::ThunkRef(y) + Ret::ValueRef(y) } (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { let mut kvs = kvs2.clone(); @@ -603,54 +564,53 @@ 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()); } - Ret::Value(RecordLit(kvs)) + Ret::ValueF(RecordLit(kvs)) } (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::ThunkRef(x) + Ret::ValueRef(x) } (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::ThunkRef(y) + Ret::ValueRef(y) } (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { let kvs = merge_maps(kvs1, kvs2, |v1, v2| { - Thunk::from_partial_expr(ExprF::BinOp( + Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp( RecursiveRecordMerge, v1.clone(), v2.clone(), - )) + ))) }); - Ret::Value(RecordLit(kvs)) + Ret::ValueF(RecordLit(kvs)) } (RecursiveRecordTypeMerge, _, RecordType(kvs)) if kvs.is_empty() => { - Ret::ThunkRef(x) + Ret::ValueRef(x) } (RecursiveRecordTypeMerge, RecordType(kvs), _) if kvs.is_empty() => { - Ret::ThunkRef(y) + Ret::ValueRef(y) } (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => { let kvs = merge_maps(kvs1, kvs2, |v1, v2| { - TypedThunk::from_thunk(Thunk::from_partial_expr(ExprF::BinOp( + Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp( RecursiveRecordTypeMerge, - v1.to_thunk(), - v2.to_thunk(), + v1.clone(), + v2.clone(), ))) }); - Ret::Value(RecordType(kvs)) + Ret::ValueF(RecordType(kvs)) } - (Equivalence, _, _) => Ret::Value(Value::Equivalence( - TypedThunk::from_thunk(x.clone()), - TypedThunk::from_thunk(y.clone()), - )), + (Equivalence, _, _) => { + Ret::ValueF(ValueF::Equivalence(x.clone(), y.clone())) + } _ => return None, }) } -pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value { - use Value::{ +pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { + use ValueF::{ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam, NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType, TextLit, UnionConstructor, UnionLit, UnionType, @@ -662,36 +622,25 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value { ), ExprF::Embed(_) => unreachable!(), ExprF::Var(_) => unreachable!(), - ExprF::Annot(x, _) => Ret::Thunk(x), + ExprF::Annot(x, _) => Ret::Value(x), ExprF::Assert(_) => Ret::Expr(expr), - ExprF::Lam(x, t, e) => { - Ret::Value(Lam(x.into(), TypedThunk::from_thunk(t), e)) - } - ExprF::Pi(x, t, e) => Ret::Value(Pi( - x.into(), - TypedThunk::from_thunk(t), - TypedThunk::from_thunk(e), - )), - ExprF::Let(x, _, v, b) => { - let v = Typed::from_thunk_untyped(v); - 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::SomeLit(e) => Ret::Value(NEOptionalLit(e)), + ExprF::Lam(x, t, e) => Ret::ValueF(Lam(x.into(), t, e)), + ExprF::Pi(x, t, e) => Ret::ValueF(Pi(x.into(), t, e)), + ExprF::Let(x, _, v, b) => Ret::Value(b.subst_shift(&x.into(), &v)), + ExprF::App(v, a) => Ret::ValueF(v.app_value(a)), + ExprF::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)), + ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)), + ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)), + ExprF::NaturalLit(n) => Ret::ValueF(NaturalLit(n)), + ExprF::IntegerLit(n) => Ret::ValueF(IntegerLit(n)), + ExprF::DoubleLit(n) => Ret::ValueF(DoubleLit(n)), + ExprF::SomeLit(e) => Ret::ValueF(NEOptionalLit(e)), ExprF::EmptyListLit(ref t) => { // Check if the type is of the form `List x` - let t_borrow = t.as_value(); + let t_borrow = t.as_whnf(); match &*t_borrow { AppliedBuiltin(Builtin::List, args) if args.len() == 1 => { - Ret::Value(EmptyListLit(TypedThunk::from_thunk( - args[0].clone(), - ))) + Ret::ValueF(EmptyListLit(args[0].clone())) } _ => { drop(t_borrow); @@ -700,43 +649,39 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value { } } ExprF::NEListLit(elts) => { - Ret::Value(NEListLit(elts.into_iter().collect())) + Ret::ValueF(NEListLit(elts.into_iter().collect())) } ExprF::RecordLit(kvs) => { - Ret::Value(RecordLit(kvs.into_iter().collect())) + Ret::ValueF(RecordLit(kvs.into_iter().collect())) + } + ExprF::RecordType(kts) => { + Ret::ValueF(RecordType(kts.into_iter().collect())) + } + ExprF::UnionType(kts) => { + Ret::ValueF(UnionType(kts.into_iter().collect())) } - ExprF::RecordType(kts) => Ret::Value(RecordType( - kts.into_iter() - .map(|(k, t)| (k, TypedThunk::from_thunk(t))) - .collect(), - )), - ExprF::UnionType(kts) => Ret::Value(UnionType( - kts.into_iter() - .map(|(k, t)| (k, t.map(|t| TypedThunk::from_thunk(t)))) - .collect(), - )), ExprF::TextLit(elts) => { use InterpolatedTextContents::Expr; let elts: Vec<_> = squash_textlit(elts.into_iter()); // Simplify bare interpolation if let [Expr(th)] = elts.as_slice() { - Ret::Thunk(th.clone()) + Ret::Value(th.clone()) } else { - Ret::Value(TextLit(elts)) + Ret::ValueF(TextLit(elts)) } } ExprF::BoolIf(ref b, ref e1, ref e2) => { - let b_borrow = b.as_value(); + let b_borrow = b.as_whnf(); match &*b_borrow { - BoolLit(true) => Ret::ThunkRef(e1), - BoolLit(false) => Ret::ThunkRef(e2), + BoolLit(true) => Ret::ValueRef(e1), + BoolLit(false) => Ret::ValueRef(e2), _ => { - let e1_borrow = e1.as_value(); - let e2_borrow = e2.as_value(); + let e1_borrow = e1.as_whnf(); + let e2_borrow = e2.as_whnf(); match (&*e1_borrow, &*e2_borrow) { // Simplify `if b then True else False` - (BoolLit(true), BoolLit(false)) => Ret::ThunkRef(b), - _ if e1 == e2 => Ret::ThunkRef(e1), + (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b), + _ if e1 == e2 => Ret::ValueRef(e1), _ => { drop(b_borrow); drop(e1_borrow); @@ -753,12 +698,12 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value { }, ExprF::Projection(_, ref ls) if ls.is_empty() => { - Ret::Value(RecordLit(HashMap::new())) + Ret::ValueF(RecordLit(HashMap::new())) } ExprF::Projection(ref v, ref ls) => { - let v_borrow = v.as_value(); + let v_borrow = v.as_whnf(); match &*v_borrow { - RecordLit(kvs) => Ret::Value(RecordLit( + RecordLit(kvs) => Ret::ValueF(RecordLit( ls.iter() .filter_map(|l| { kvs.get(l).map(|x| (l.clone(), x.clone())) @@ -772,17 +717,17 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value { } } ExprF::Field(ref v, ref l) => { - let v_borrow = v.as_value(); + let v_borrow = v.as_whnf(); match &*v_borrow { RecordLit(kvs) => match kvs.get(l) { - Some(r) => Ret::Thunk(r.clone()), + Some(r) => Ret::Value(r.clone()), None => { drop(v_borrow); Ret::Expr(expr) } }, UnionType(kts) => { - Ret::Value(UnionConstructor(l.clone(), kts.clone())) + Ret::ValueF(UnionConstructor(l.clone(), kts.clone())) } _ => { drop(v_borrow); @@ -792,11 +737,11 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value { } ExprF::Merge(ref handlers, ref variant, _) => { - let handlers_borrow = handlers.as_value(); - let variant_borrow = variant.as_value(); + let handlers_borrow = handlers.as_whnf(); + let variant_borrow = variant.as_whnf(); match (&*handlers_borrow, &*variant_borrow) { (RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) { - Some(h) => Ret::Thunk(h.clone()), + Some(h) => Ret::Value(h.clone()), None => { drop(handlers_borrow); drop(variant_borrow); @@ -804,7 +749,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value { } }, (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) { - Some(h) => Ret::Value(h.app_thunk(v.clone())), + Some(h) => Ret::ValueF(h.app_value(v.clone())), None => { drop(handlers_borrow); drop(variant_borrow); @@ -821,9 +766,22 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value { }; match ret { - Ret::Value(v) => v, - Ret::Thunk(th) => th.to_value(), - Ret::ThunkRef(th) => th.to_value(), - Ret::Expr(expr) => Value::PartialExpr(expr), + Ret::ValueF(v) => v, + Ret::Value(th) => th.as_whnf().clone(), + Ret::ValueRef(th) => th.as_whnf().clone(), + Ret::Expr(expr) => ValueF::PartialExpr(expr), + } +} + +/// Normalize a ValueF into WHNF +pub(crate) fn normalize_whnf(v: ValueF) -> ValueF { + match v { + ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args), + ValueF::PartialExpr(e) => normalize_one_layer(e), + ValueF::TextLit(elts) => { + ValueF::TextLit(squash_textlit(elts.into_iter())) + } + // All other cases are already in WHNF + v => v, } } |