From 04438824db21fb5d9d3a2abdb3fa167875bda892 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 16:39:27 +0200 Subject: Add Value::from_builtin --- dhall/src/phase/normalize.rs | 44 +++++++++++++++++++------------------------- 1 file changed, 19 insertions(+), 25 deletions(-) (limited to 'dhall/src/phase/normalize.rs') diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index a379a4b..f943171 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -31,11 +31,10 @@ macro_rules! make_closure { ).into_value_untyped() }; (Natural) => { - ValueF::from_builtin(Builtin::Natural) - .into_value_simple_type() + Value::from_builtin(Builtin::Natural) }; (List $($rest:tt)*) => { - ValueF::from_builtin(Builtin::List) + Value::from_builtin(Builtin::List) .app_value(make_closure!($($rest)*)) .into_value_simple_type() }; @@ -192,10 +191,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { (ListIndexed, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(t) => { let mut kts = HashMap::new(); - kts.insert( - "index".into(), - Value::from_valuef_untyped(ValueF::from_builtin(Natural)), - ); + kts.insert("index".into(), Value::from_builtin(Natural)); kts.insert("value".into(), t.clone()); Ok(( r, @@ -232,7 +228,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { } } _ => { - let list_t = ValueF::from_builtin(List) + let list_t = Value::from_builtin(List) .app_value(t.clone()) .into_value_simple_type(); Ok(( @@ -280,7 +276,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { } } _ => { - let optional_t = ValueF::from_builtin(Optional) + let optional_t = Value::from_builtin(Optional) .app_value(t.clone()) .into_value_simple_type(); Ok(( @@ -309,26 +305,24 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { unimplemented!() } } - _ => { - 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), - ), - )) - } + _ => Ok(( + r, + f.app_value(Value::from_builtin(Natural)) + .app_value(make_closure!(λ(x : Natural) -> 1 + var(x, 0))) + .app_value( + NaturalLit(0) + .into_value_with_type(Value::from_builtin(Natural)), + ), + )), }, (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() { NaturalLit(0) => Ok((r, zero.to_whnf())), NaturalLit(n) => { - let fold = ValueF::from_builtin(NaturalFold) - .app(NaturalLit(n - 1)) + let fold = Value::from_builtin(NaturalFold) + .app_value( + NaturalLit(n - 1) + .into_value_with_type(Value::from_builtin(Natural)), + ) .app_value(t.clone()) .app_value(succ.clone()) .app_value(zero.clone()) -- cgit v1.2.3 From a506632b27b287d1bf898e2f77ae09a56902474c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 17:08:01 +0200 Subject: Naming tweaks --- dhall/src/phase/normalize.rs | 52 ++++++++++++++++++++------------------------ 1 file changed, 23 insertions(+), 29 deletions(-) (limited to 'dhall/src/phase/normalize.rs') diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index f943171..afc2e7f 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -8,9 +8,7 @@ use dhall_syntax::{ use crate::core::value::Value; use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; -use crate::phase::{Normalized, NormalizedSubExpr}; - -pub(crate) type OutputSubExpr = NormalizedSubExpr; +use crate::phase::Normalized; // Ad-hoc macro to help construct closures macro_rules! make_closure { @@ -35,7 +33,7 @@ macro_rules! make_closure { }; (List $($rest:tt)*) => { Value::from_builtin(Builtin::List) - .app_value(make_closure!($($rest)*)) + .app(make_closure!($($rest)*)) .into_value_simple_type() }; (Some($($rest:tt)*)) => { @@ -229,12 +227,12 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { } _ => { let list_t = Value::from_builtin(List) - .app_value(t.clone()) + .app(t.clone()) .into_value_simple_type(); Ok(( r, - f.app_value(list_t.clone()) - .app_value({ + f.app(list_t.clone()) + .app({ // Move `t` under new `x` variable let t1 = t.under_binder(Label::from("x")); make_closure!( @@ -243,7 +241,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { [ var(x, 1) ] # var(xs, 0) ) }) - .app_value( + .app( EmptyListLit(t.clone()) .into_value_with_type(list_t), ), @@ -255,11 +253,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { NEListLit(xs) => { let mut v = nil.clone(); for x in xs.iter().rev() { - v = cons - .clone() - .app_value(x.clone()) - .app_value(v) - .into_value_untyped(); + v = cons.clone().app(x.clone()).app(v).into_value_untyped(); } Ok((r, v.to_whnf())) } @@ -277,13 +271,13 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { } _ => { let optional_t = Value::from_builtin(Optional) - .app_value(t.clone()) + .app(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( + f.app(optional_t.clone()) + .app(make_closure!(λ(x: #t) -> Some(var(x, 0)))) + .app( EmptyOptionalLit(t.clone()) .into_value_with_type(optional_t), ), @@ -292,7 +286,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { }, (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() { EmptyOptionalLit(_) => Ok((r, nothing.to_whnf())), - NEOptionalLit(x) => Ok((r, just.app_value(x.clone()))), + NEOptionalLit(x) => Ok((r, just.app(x.clone()))), _ => Err(()), }, (NaturalBuild, [f, r..]) => match &*f.as_whnf() { @@ -307,9 +301,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { } _ => Ok(( r, - f.app_value(Value::from_builtin(Natural)) - .app_value(make_closure!(λ(x : Natural) -> 1 + var(x, 0))) - .app_value( + f.app(Value::from_builtin(Natural)) + .app(make_closure!(λ(x : Natural) -> 1 + var(x, 0))) + .app( NaturalLit(0) .into_value_with_type(Value::from_builtin(Natural)), ), @@ -319,15 +313,15 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { NaturalLit(0) => Ok((r, zero.to_whnf())), NaturalLit(n) => { let fold = Value::from_builtin(NaturalFold) - .app_value( + .app( NaturalLit(n - 1) .into_value_with_type(Value::from_builtin(Natural)), ) - .app_value(t.clone()) - .app_value(succ.clone()) - .app_value(zero.clone()) + .app(t.clone()) + .app(succ.clone()) + .app(zero.clone()) .into_value_with_type(t.clone()); - Ok((r, succ.app_value(fold))) + Ok((r, succ.app(fold))) } _ => Err(()), }, @@ -337,7 +331,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { 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_value(x); + v = v.app(x); } v } @@ -621,7 +615,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { 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::App(v, a) => Ret::ValueF(v.app(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)), @@ -743,7 +737,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { } }, (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) { - Some(h) => Ret::ValueF(h.app_value(v.clone())), + Some(h) => Ret::ValueF(h.app(v.clone())), None => { drop(handlers_borrow); drop(variant_borrow); -- cgit v1.2.3 From 4f1f37cfc115510500e83d2dfbfa8ed7ddeae74a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 18:03:59 +0200 Subject: Introduce a new enum to store either a Value or a ValueF --- dhall/src/phase/normalize.rs | 141 +++++++++++++++++++++++++------------------ 1 file changed, 81 insertions(+), 60 deletions(-) (limited to 'dhall/src/phase/normalize.rs') diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index afc2e7f..e044018 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -5,7 +5,7 @@ use dhall_syntax::{ NaiveDouble, }; -use crate::core::value::Value; +use crate::core::value::{Value, VoVF}; use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; use crate::phase::Normalized; @@ -63,44 +63,48 @@ macro_rules! make_closure { } #[allow(clippy::cognitive_complexity)] -pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { +pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { use dhall_syntax::Builtin::*; 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(t.clone()))), + (OptionalNone, [t, r..]) => { + Ok((r, EmptyOptionalLit(t.clone()).into_vovf())) + } (NaturalIsZero, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, BoolLit(*n == 0))), + NaturalLit(n) => Ok((r, BoolLit(*n == 0).into_vovf())), _ => Err(()), }, (NaturalEven, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0))), + NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0).into_vovf())), _ => Err(()), }, (NaturalOdd, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0))), + NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0).into_vovf())), _ => Err(()), }, (NaturalToInteger, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, IntegerLit(*n as isize))), + NaturalLit(n) => Ok((r, IntegerLit(*n as isize).into_vovf())), _ => Err(()), }, (NaturalShow, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok(( r, - TextLit(vec![InterpolatedTextContents::Text(n.to_string())]), + TextLit(vec![InterpolatedTextContents::Text(n.to_string())]) + .into_vovf(), )), _ => Err(()), }, (NaturalSubtract, [a, b, r..]) => { match (&*a.as_whnf(), &*b.as_whnf()) { - (NaturalLit(a), NaturalLit(b)) => { - Ok((r, NaturalLit(if b > a { b - a } else { 0 }))) - } - (NaturalLit(0), b) => Ok((r, b.clone())), - (_, NaturalLit(0)) => Ok((r, NaturalLit(0))), - _ if a == b => Ok((r, NaturalLit(0))), + (NaturalLit(a), NaturalLit(b)) => Ok(( + r, + NaturalLit(if b > a { b - a } else { 0 }).into_vovf(), + )), + (NaturalLit(0), _) => Ok((r, b.clone().into_vovf())), + (_, NaturalLit(0)) => Ok((r, NaturalLit(0).into_vovf())), + _ if a == b => Ok((r, NaturalLit(0).into_vovf())), _ => Err(()), } } @@ -111,18 +115,25 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { } else { format!("+{}", n) }; - Ok((r, TextLit(vec![InterpolatedTextContents::Text(s)]))) + Ok(( + r, + TextLit(vec![InterpolatedTextContents::Text(s)]) + .into_vovf(), + )) } _ => Err(()), }, (IntegerToDouble, [n, r..]) => match &*n.as_whnf() { - IntegerLit(n) => Ok((r, DoubleLit(NaiveDouble::from(*n as f64)))), + IntegerLit(n) => { + Ok((r, DoubleLit(NaiveDouble::from(*n as f64)).into_vovf())) + } _ => Err(()), }, (DoubleShow, [n, r..]) => match &*n.as_whnf() { DoubleLit(n) => Ok(( r, - TextLit(vec![InterpolatedTextContents::Text(n.to_string())]), + TextLit(vec![InterpolatedTextContents::Text(n.to_string())]) + .into_vovf(), )), _ => Err(()), }, @@ -137,7 +148,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { let s = txt.to_string(); Ok(( r, - TextLit(vec![InterpolatedTextContents::Text(s)]), + TextLit(vec![InterpolatedTextContents::Text(s)]) + .into_vovf(), )) } // If there are no interpolations (invariants ensure that when there are no @@ -152,7 +164,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { let s = txt.to_string(); Ok(( r, - TextLit(vec![InterpolatedTextContents::Text(s)]), + TextLit(vec![InterpolatedTextContents::Text(s)]) + .into_vovf(), )) } _ => Err(()), @@ -161,29 +174,33 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { _ => Err(()), }, (ListLength, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(_) => Ok((r, NaturalLit(0))), - NEListLit(xs) => Ok((r, NaturalLit(xs.len()))), + EmptyListLit(_) => Ok((r, NaturalLit(0).into_vovf())), + NEListLit(xs) => Ok((r, NaturalLit(xs.len()).into_vovf())), _ => Err(()), }, (ListHead, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))), - NEListLit(xs) => { - Ok((r, NEOptionalLit(xs.iter().next().unwrap().clone()))) - } + EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()).into_vovf())), + NEListLit(xs) => Ok(( + r, + NEOptionalLit(xs.iter().next().unwrap().clone()).into_vovf(), + )), _ => Err(()), }, (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()))) - } + EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()).into_vovf())), + NEListLit(xs) => Ok(( + r, + NEOptionalLit(xs.iter().rev().next().unwrap().clone()) + .into_vovf(), + )), _ => Err(()), }, (ListReverse, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()))), - NEListLit(xs) => { - Ok((r, NEListLit(xs.iter().rev().cloned().collect()))) - } + EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()).into_vovf())), + NEListLit(xs) => Ok(( + r, + NEListLit(xs.iter().rev().cloned().collect()).into_vovf(), + )), _ => Err(()), }, (ListIndexed, [_, l, r..]) => match &*l.as_whnf() { @@ -193,7 +210,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { kts.insert("value".into(), t.clone()); Ok(( r, - EmptyListLit(Value::from_valuef_untyped(RecordType(kts))), + EmptyListLit(Value::from_valuef_untyped(RecordType(kts))) + .into_vovf(), )) } NEListLit(xs) => { @@ -211,7 +229,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { Value::from_valuef_untyped(RecordLit(kvs)) }) .collect(); - Ok((r, NEListLit(xs))) + Ok((r, NEListLit(xs).into_vovf())) } _ => Err(()), }, @@ -219,7 +237,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { // fold/build fusion ValueF::AppliedBuiltin(ListFold, args) => { if args.len() >= 2 { - Ok((r, args[1].to_whnf())) + Ok((r, args[1].clone().into_vovf())) } else { // Do we really need to handle this case ? unimplemented!() @@ -249,13 +267,13 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { } }, (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() { - EmptyListLit(_) => Ok((r, nil.to_whnf())), + EmptyListLit(_) => Ok((r, nil.clone().into_vovf())), NEListLit(xs) => { - let mut v = nil.clone(); - for x in xs.iter().rev() { - v = cons.clone().app(x.clone()).app(v).into_value_untyped(); + let mut v = nil.clone().into_vovf(); + for x in xs.iter().cloned().rev() { + v = cons.app(x).app(v.into_value_untyped()); } - Ok((r, v.to_whnf())) + Ok((r, v)) } _ => Err(()), }, @@ -263,7 +281,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { // fold/build fusion ValueF::AppliedBuiltin(OptionalFold, args) => { if args.len() >= 2 { - Ok((r, args[1].to_whnf())) + Ok((r, args[1].clone().into_vovf())) } else { // Do we really need to handle this case ? unimplemented!() @@ -285,7 +303,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { } }, (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() { - EmptyOptionalLit(_) => Ok((r, nothing.to_whnf())), + EmptyOptionalLit(_) => Ok((r, nothing.clone().into_vovf())), NEOptionalLit(x) => Ok((r, just.app(x.clone()))), _ => Err(()), }, @@ -293,7 +311,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { // fold/build fusion ValueF::AppliedBuiltin(NaturalFold, args) => { if !args.is_empty() { - Ok((r, args[0].to_whnf())) + Ok((r, args[0].clone().into_vovf())) } else { // Do we really need to handle this case ? unimplemented!() @@ -310,7 +328,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { )), }, (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() { - NaturalLit(0) => Ok((r, zero.to_whnf())), + NaturalLit(0) => Ok((r, zero.clone().into_vovf())), NaturalLit(n) => { let fold = Value::from_builtin(NaturalFold) .app( @@ -335,23 +353,24 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { } v } - Err(()) => AppliedBuiltin(b, args), + Err(()) => AppliedBuiltin(b, args).into_vovf(), } } -pub(crate) fn apply_any(f: Value, a: Value) -> ValueF { - let fallback = |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a)); +pub(crate) fn apply_any(f: Value, a: Value) -> VoVF { + let fallback = + |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a)).into_vovf(); let f_borrow = f.as_whnf(); match &*f_borrow { - ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).to_whnf(), + ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).into_vovf(), ValueF::AppliedBuiltin(b, args) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); apply_builtin(*b, args) } ValueF::UnionConstructor(l, kts) => { - ValueF::UnionLit(l.clone(), a, kts.clone()) + ValueF::UnionLit(l.clone(), a, kts.clone()).into_vovf() } _ => { drop(f_borrow); @@ -465,6 +484,7 @@ where enum Ret<'a> { ValueF(ValueF), Value(Value), + VoVF(VoVF), ValueRef(&'a Value), Expr(ExprF), } @@ -597,7 +617,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { }) } -pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { +pub(crate) fn normalize_one_layer(expr: ExprF) -> VoVF { use ValueF::{ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam, NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType, @@ -615,7 +635,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { 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(a)), + ExprF::App(v, a) => Ret::VoVF(v.app(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)), @@ -737,7 +757,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { } }, (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) { - Some(h) => Ret::ValueF(h.app(v.clone())), + Some(h) => Ret::VoVF(h.app(v.clone())), None => { drop(handlers_borrow); drop(variant_borrow); @@ -754,22 +774,23 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { }; match ret { - Ret::ValueF(v) => v, - Ret::Value(th) => th.as_whnf().clone(), - Ret::ValueRef(th) => th.as_whnf().clone(), - Ret::Expr(expr) => ValueF::PartialExpr(expr), + Ret::ValueF(v) => v.into_vovf(), + Ret::Value(v) => v.into_vovf(), + Ret::VoVF(v) => v, + Ret::ValueRef(v) => v.clone().into_vovf(), + Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf(), } } /// Normalize a ValueF into WHNF -pub(crate) fn normalize_whnf(v: ValueF) -> ValueF { +pub(crate) fn normalize_whnf(v: ValueF) -> VoVF { 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())) + ValueF::TextLit(squash_textlit(elts.into_iter())).into_vovf() } // All other cases are already in WHNF - v => v, + v => v.into_vovf(), } } -- cgit v1.2.3 From f70e45daef2570259eccd227a0126493c015d7b0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 21:50:47 +0200 Subject: Track evaluation status alongside ValueF in VoVF --- dhall/src/phase/normalize.rs | 72 ++++++++++++++++++++++++-------------------- 1 file changed, 40 insertions(+), 32 deletions(-) (limited to 'dhall/src/phase/normalize.rs') diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index e044018..a146ec7 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -70,29 +70,29 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { // 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(t.clone()).into_vovf())) + Ok((r, EmptyOptionalLit(t.clone()).into_vovf_whnf())) } (NaturalIsZero, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, BoolLit(*n == 0).into_vovf())), + NaturalLit(n) => Ok((r, BoolLit(*n == 0).into_vovf_nf())), _ => Err(()), }, (NaturalEven, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0).into_vovf())), + NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0).into_vovf_nf())), _ => Err(()), }, (NaturalOdd, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0).into_vovf())), + NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0).into_vovf_nf())), _ => Err(()), }, (NaturalToInteger, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, IntegerLit(*n as isize).into_vovf())), + NaturalLit(n) => Ok((r, IntegerLit(*n as isize).into_vovf_nf())), _ => Err(()), }, (NaturalShow, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok(( r, TextLit(vec![InterpolatedTextContents::Text(n.to_string())]) - .into_vovf(), + .into_vovf_nf(), )), _ => Err(()), }, @@ -100,11 +100,11 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { match (&*a.as_whnf(), &*b.as_whnf()) { (NaturalLit(a), NaturalLit(b)) => Ok(( r, - NaturalLit(if b > a { b - a } else { 0 }).into_vovf(), + NaturalLit(if b > a { b - a } else { 0 }).into_vovf_nf(), )), (NaturalLit(0), _) => Ok((r, b.clone().into_vovf())), - (_, NaturalLit(0)) => Ok((r, NaturalLit(0).into_vovf())), - _ if a == b => Ok((r, NaturalLit(0).into_vovf())), + (_, NaturalLit(0)) => Ok((r, NaturalLit(0).into_vovf_nf())), + _ if a == b => Ok((r, NaturalLit(0).into_vovf_nf())), _ => Err(()), } } @@ -118,14 +118,14 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { Ok(( r, TextLit(vec![InterpolatedTextContents::Text(s)]) - .into_vovf(), + .into_vovf_nf(), )) } _ => Err(()), }, (IntegerToDouble, [n, r..]) => match &*n.as_whnf() { IntegerLit(n) => { - Ok((r, DoubleLit(NaiveDouble::from(*n as f64)).into_vovf())) + Ok((r, DoubleLit(NaiveDouble::from(*n as f64)).into_vovf_nf())) } _ => Err(()), }, @@ -133,7 +133,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { DoubleLit(n) => Ok(( r, TextLit(vec![InterpolatedTextContents::Text(n.to_string())]) - .into_vovf(), + .into_vovf_nf(), )), _ => Err(()), }, @@ -149,7 +149,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { Ok(( r, TextLit(vec![InterpolatedTextContents::Text(s)]) - .into_vovf(), + .into_vovf_nf(), )) } // If there are no interpolations (invariants ensure that when there are no @@ -165,7 +165,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { Ok(( r, TextLit(vec![InterpolatedTextContents::Text(s)]) - .into_vovf(), + .into_vovf_nf(), )) } _ => Err(()), @@ -174,32 +174,39 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { _ => Err(()), }, (ListLength, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(_) => Ok((r, NaturalLit(0).into_vovf())), - NEListLit(xs) => Ok((r, NaturalLit(xs.len()).into_vovf())), + EmptyListLit(_) => Ok((r, NaturalLit(0).into_vovf_nf())), + NEListLit(xs) => Ok((r, NaturalLit(xs.len()).into_vovf_nf())), _ => Err(()), }, (ListHead, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()).into_vovf())), + EmptyListLit(n) => { + Ok((r, EmptyOptionalLit(n.clone()).into_vovf_whnf())) + } NEListLit(xs) => Ok(( r, - NEOptionalLit(xs.iter().next().unwrap().clone()).into_vovf(), + NEOptionalLit(xs.iter().next().unwrap().clone()) + .into_vovf_whnf(), )), _ => Err(()), }, (ListLast, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()).into_vovf())), + EmptyListLit(n) => { + Ok((r, EmptyOptionalLit(n.clone()).into_vovf_whnf())) + } NEListLit(xs) => Ok(( r, NEOptionalLit(xs.iter().rev().next().unwrap().clone()) - .into_vovf(), + .into_vovf_whnf(), )), _ => Err(()), }, (ListReverse, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()).into_vovf())), + EmptyListLit(n) => { + Ok((r, EmptyListLit(n.clone()).into_vovf_whnf())) + } NEListLit(xs) => Ok(( r, - NEListLit(xs.iter().rev().cloned().collect()).into_vovf(), + NEListLit(xs.iter().rev().cloned().collect()).into_vovf_whnf(), )), _ => Err(()), }, @@ -211,7 +218,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { Ok(( r, EmptyListLit(Value::from_valuef_untyped(RecordType(kts))) - .into_vovf(), + .into_vovf_whnf(), )) } NEListLit(xs) => { @@ -229,7 +236,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { Value::from_valuef_untyped(RecordLit(kvs)) }) .collect(); - Ok((r, NEListLit(xs).into_vovf())) + Ok((r, NEListLit(xs).into_vovf_whnf())) } _ => Err(()), }, @@ -353,13 +360,14 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { } v } - Err(()) => AppliedBuiltin(b, args).into_vovf(), + Err(()) => AppliedBuiltin(b, args).into_vovf_whnf(), } } pub(crate) fn apply_any(f: Value, a: Value) -> VoVF { - let fallback = - |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a)).into_vovf(); + let fallback = |f: Value, a: Value| { + ValueF::PartialExpr(ExprF::App(f, a)).into_vovf_whnf() + }; let f_borrow = f.as_whnf(); match &*f_borrow { @@ -370,7 +378,7 @@ pub(crate) fn apply_any(f: Value, a: Value) -> VoVF { apply_builtin(*b, args) } ValueF::UnionConstructor(l, kts) => { - ValueF::UnionLit(l.clone(), a, kts.clone()).into_vovf() + ValueF::UnionLit(l.clone(), a, kts.clone()).into_vovf_whnf() } _ => { drop(f_borrow); @@ -774,11 +782,11 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> VoVF { }; match ret { - Ret::ValueF(v) => v.into_vovf(), + Ret::ValueF(v) => v.into_vovf_whnf(), Ret::Value(v) => v.into_vovf(), Ret::VoVF(v) => v, Ret::ValueRef(v) => v.clone().into_vovf(), - Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf(), + Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf_whnf(), } } @@ -788,9 +796,9 @@ pub(crate) fn normalize_whnf(v: ValueF) -> VoVF { 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())).into_vovf() + ValueF::TextLit(squash_textlit(elts.into_iter())).into_vovf_whnf() } // All other cases are already in WHNF - v => v.into_vovf(), + v => v.into_vovf_whnf(), } } -- cgit v1.2.3 From ec349d42703a8a31715cf97b44845ba3dd7a6805 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 22:20:59 +0200 Subject: Propagate type information in Value::app() --- dhall/src/phase/normalize.rs | 35 ++++++++++++++++------------------- 1 file changed, 16 insertions(+), 19 deletions(-) (limited to 'dhall/src/phase/normalize.rs') diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index a146ec7..e4a0c5b 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -34,7 +34,6 @@ macro_rules! make_closure { (List $($rest:tt)*) => { Value::from_builtin(Builtin::List) .app(make_closure!($($rest)*)) - .into_value_simple_type() }; (Some($($rest:tt)*)) => { ValueF::NEOptionalLit(make_closure!($($rest)*)) @@ -251,9 +250,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { } } _ => { - let list_t = Value::from_builtin(List) - .app(t.clone()) - .into_value_simple_type(); + let list_t = Value::from_builtin(List).app(t.clone()); Ok(( r, f.app(list_t.clone()) @@ -269,18 +266,19 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { .app( EmptyListLit(t.clone()) .into_value_with_type(list_t), - ), + ) + .into_vovf(), )) } }, (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() { EmptyListLit(_) => Ok((r, nil.clone().into_vovf())), NEListLit(xs) => { - let mut v = nil.clone().into_vovf(); + let mut v = nil.clone(); for x in xs.iter().cloned().rev() { - v = cons.app(x).app(v.into_value_untyped()); + v = cons.app(x).app(v); } - Ok((r, v)) + Ok((r, v.into_vovf())) } _ => Err(()), }, @@ -295,9 +293,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { } } _ => { - let optional_t = Value::from_builtin(Optional) - .app(t.clone()) - .into_value_simple_type(); + let optional_t = Value::from_builtin(Optional).app(t.clone()); Ok(( r, f.app(optional_t.clone()) @@ -305,13 +301,14 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { .app( EmptyOptionalLit(t.clone()) .into_value_with_type(optional_t), - ), + ) + .into_vovf(), )) } }, (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() { EmptyOptionalLit(_) => Ok((r, nothing.clone().into_vovf())), - NEOptionalLit(x) => Ok((r, just.app(x.clone()))), + NEOptionalLit(x) => Ok((r, just.app(x.clone()).into_vovf())), _ => Err(()), }, (NaturalBuild, [f, r..]) => match &*f.as_whnf() { @@ -331,7 +328,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { .app( NaturalLit(0) .into_value_with_type(Value::from_builtin(Natural)), - ), + ) + .into_vovf(), )), }, (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() { @@ -344,9 +342,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { ) .app(t.clone()) .app(succ.clone()) - .app(zero.clone()) - .into_value_with_type(t.clone()); - Ok((r, succ.app(fold))) + .app(zero.clone()); + Ok((r, succ.app(fold).into_vovf())) } _ => Err(()), }, @@ -643,7 +640,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> VoVF { 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::VoVF(v.app(a)), + ExprF::App(v, a) => Ret::Value(v.app(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)), @@ -765,7 +762,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> VoVF { } }, (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) { - Some(h) => Ret::VoVF(h.app(v.clone())), + Some(h) => Ret::Value(h.app(v.clone())), None => { drop(handlers_borrow); drop(variant_borrow); -- cgit v1.2.3 From 8e68396e9fe3751bcf8bcfd68301ca7fea836787 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 22:35:53 +0200 Subject: Use Ret in apply_builtin --- dhall/src/phase/normalize.rs | 191 +++++++++++++++++++++++-------------------- 1 file changed, 101 insertions(+), 90 deletions(-) (limited to 'dhall/src/phase/normalize.rs') diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index e4a0c5b..0c4e185 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -10,6 +10,25 @@ use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; use crate::phase::Normalized; +// Small helper enum to avoid repetition +enum Ret<'a> { + ValueF(ValueF), + Value(Value), + ValueRef(&'a Value), + Expr(ExprF), +} + +impl<'a> Ret<'a> { + fn into_vovf_whnf(self) -> VoVF { + match self { + Ret::ValueF(v) => v.into_vovf_whnf(), + Ret::Value(v) => v.into_vovf(), + Ret::ValueRef(v) => v.clone().into_vovf(), + Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf_whnf(), + } + } +} + // Ad-hoc macro to help construct closures macro_rules! make_closure { (#$var:ident) => { $var.clone() }; @@ -69,29 +88,30 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { // 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(t.clone()).into_vovf_whnf())) + Ok((r, Ret::ValueF(EmptyOptionalLit(t.clone())))) } (NaturalIsZero, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, BoolLit(*n == 0).into_vovf_nf())), + NaturalLit(n) => Ok((r, Ret::ValueF(BoolLit(*n == 0)))), _ => Err(()), }, (NaturalEven, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0).into_vovf_nf())), + NaturalLit(n) => Ok((r, Ret::ValueF(BoolLit(*n % 2 == 0)))), _ => Err(()), }, (NaturalOdd, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0).into_vovf_nf())), + NaturalLit(n) => Ok((r, Ret::ValueF(BoolLit(*n % 2 != 0)))), _ => Err(()), }, (NaturalToInteger, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, IntegerLit(*n as isize).into_vovf_nf())), + NaturalLit(n) => Ok((r, Ret::ValueF(IntegerLit(*n as isize)))), _ => Err(()), }, (NaturalShow, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok(( r, - TextLit(vec![InterpolatedTextContents::Text(n.to_string())]) - .into_vovf_nf(), + Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text( + n.to_string(), + )])), )), _ => Err(()), }, @@ -99,11 +119,11 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { match (&*a.as_whnf(), &*b.as_whnf()) { (NaturalLit(a), NaturalLit(b)) => Ok(( r, - NaturalLit(if b > a { b - a } else { 0 }).into_vovf_nf(), + Ret::ValueF(NaturalLit(if b > a { b - a } else { 0 })), )), - (NaturalLit(0), _) => Ok((r, b.clone().into_vovf())), - (_, NaturalLit(0)) => Ok((r, NaturalLit(0).into_vovf_nf())), - _ if a == b => Ok((r, NaturalLit(0).into_vovf_nf())), + (NaturalLit(0), _) => Ok((r, Ret::ValueRef(b))), + (_, NaturalLit(0)) => Ok((r, Ret::ValueF(NaturalLit(0)))), + _ if a == b => Ok((r, Ret::ValueF(NaturalLit(0)))), _ => Err(()), } } @@ -116,23 +136,25 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { }; Ok(( r, - TextLit(vec![InterpolatedTextContents::Text(s)]) - .into_vovf_nf(), + Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text( + s, + )])), )) } _ => Err(()), }, (IntegerToDouble, [n, r..]) => match &*n.as_whnf() { IntegerLit(n) => { - Ok((r, DoubleLit(NaiveDouble::from(*n as f64)).into_vovf_nf())) + Ok((r, Ret::ValueF(DoubleLit(NaiveDouble::from(*n as f64))))) } _ => Err(()), }, (DoubleShow, [n, r..]) => match &*n.as_whnf() { DoubleLit(n) => Ok(( r, - TextLit(vec![InterpolatedTextContents::Text(n.to_string())]) - .into_vovf_nf(), + Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text( + n.to_string(), + )])), )), _ => Err(()), }, @@ -147,8 +169,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { let s = txt.to_string(); Ok(( r, - TextLit(vec![InterpolatedTextContents::Text(s)]) - .into_vovf_nf(), + Ret::ValueF(TextLit(vec![ + InterpolatedTextContents::Text(s), + ])), )) } // If there are no interpolations (invariants ensure that when there are no @@ -163,8 +186,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { let s = txt.to_string(); Ok(( r, - TextLit(vec![InterpolatedTextContents::Text(s)]) - .into_vovf_nf(), + Ret::ValueF(TextLit(vec![ + InterpolatedTextContents::Text(s), + ])), )) } _ => Err(()), @@ -173,39 +197,37 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { _ => Err(()), }, (ListLength, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(_) => Ok((r, NaturalLit(0).into_vovf_nf())), - NEListLit(xs) => Ok((r, NaturalLit(xs.len()).into_vovf_nf())), + EmptyListLit(_) => Ok((r, Ret::ValueF(NaturalLit(0)))), + NEListLit(xs) => Ok((r, Ret::ValueF(NaturalLit(xs.len())))), _ => Err(()), }, (ListHead, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(n) => { - Ok((r, EmptyOptionalLit(n.clone()).into_vovf_whnf())) + Ok((r, Ret::ValueF(EmptyOptionalLit(n.clone())))) } NEListLit(xs) => Ok(( r, - NEOptionalLit(xs.iter().next().unwrap().clone()) - .into_vovf_whnf(), + Ret::ValueF(NEOptionalLit(xs.iter().next().unwrap().clone())), )), _ => Err(()), }, (ListLast, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(n) => { - Ok((r, EmptyOptionalLit(n.clone()).into_vovf_whnf())) + Ok((r, Ret::ValueF(EmptyOptionalLit(n.clone())))) } NEListLit(xs) => Ok(( r, - NEOptionalLit(xs.iter().rev().next().unwrap().clone()) - .into_vovf_whnf(), + Ret::ValueF(NEOptionalLit( + xs.iter().rev().next().unwrap().clone(), + )), )), _ => Err(()), }, (ListReverse, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(n) => { - Ok((r, EmptyListLit(n.clone()).into_vovf_whnf())) - } + EmptyListLit(n) => Ok((r, Ret::ValueF(EmptyListLit(n.clone())))), NEListLit(xs) => Ok(( r, - NEListLit(xs.iter().rev().cloned().collect()).into_vovf_whnf(), + Ret::ValueF(NEListLit(xs.iter().rev().cloned().collect())), )), _ => Err(()), }, @@ -216,8 +238,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { kts.insert("value".into(), t.clone()); Ok(( r, - EmptyListLit(Value::from_valuef_untyped(RecordType(kts))) - .into_vovf_whnf(), + Ret::ValueF(EmptyListLit(Value::from_valuef_untyped( + RecordType(kts), + ))), )) } NEListLit(xs) => { @@ -235,7 +258,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { Value::from_valuef_untyped(RecordLit(kvs)) }) .collect(); - Ok((r, NEListLit(xs).into_vovf_whnf())) + Ok((r, Ret::ValueF(NEListLit(xs)))) } _ => Err(()), }, @@ -243,7 +266,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { // fold/build fusion ValueF::AppliedBuiltin(ListFold, args) => { if args.len() >= 2 { - Ok((r, args[1].clone().into_vovf())) + Ok((r, Ret::Value(args[1].clone()))) } else { // Do we really need to handle this case ? unimplemented!() @@ -253,32 +276,33 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { let list_t = Value::from_builtin(List).app(t.clone()); Ok(( r, - f.app(list_t.clone()) - .app({ - // 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( - EmptyListLit(t.clone()) - .into_value_with_type(list_t), - ) - .into_vovf(), + Ret::Value( + f.app(list_t.clone()) + .app({ + // 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( + EmptyListLit(t.clone()) + .into_value_with_type(list_t), + ), + ), )) } }, (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() { - EmptyListLit(_) => Ok((r, nil.clone().into_vovf())), + EmptyListLit(_) => Ok((r, Ret::ValueRef(nil))), NEListLit(xs) => { let mut v = nil.clone(); for x in xs.iter().cloned().rev() { v = cons.app(x).app(v); } - Ok((r, v.into_vovf())) + Ok((r, Ret::Value(v))) } _ => Err(()), }, @@ -286,7 +310,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { // fold/build fusion ValueF::AppliedBuiltin(OptionalFold, args) => { if args.len() >= 2 { - Ok((r, args[1].clone().into_vovf())) + Ok((r, Ret::Value(args[1].clone()))) } else { // Do we really need to handle this case ? unimplemented!() @@ -296,26 +320,27 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { let optional_t = Value::from_builtin(Optional).app(t.clone()); Ok(( r, - f.app(optional_t.clone()) - .app(make_closure!(λ(x: #t) -> Some(var(x, 0)))) - .app( - EmptyOptionalLit(t.clone()) - .into_value_with_type(optional_t), - ) - .into_vovf(), + Ret::Value( + f.app(optional_t.clone()) + .app(make_closure!(λ(x: #t) -> Some(var(x, 0)))) + .app( + EmptyOptionalLit(t.clone()) + .into_value_with_type(optional_t), + ), + ), )) } }, (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() { - EmptyOptionalLit(_) => Ok((r, nothing.clone().into_vovf())), - NEOptionalLit(x) => Ok((r, just.app(x.clone()).into_vovf())), + EmptyOptionalLit(_) => Ok((r, Ret::ValueRef(nothing))), + NEOptionalLit(x) => Ok((r, Ret::Value(just.app(x.clone())))), _ => Err(()), }, (NaturalBuild, [f, r..]) => match &*f.as_whnf() { // fold/build fusion ValueF::AppliedBuiltin(NaturalFold, args) => { if !args.is_empty() { - Ok((r, args[0].clone().into_vovf())) + Ok((r, Ret::Value(args[0].clone()))) } else { // Do we really need to handle this case ? unimplemented!() @@ -323,17 +348,17 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { } _ => Ok(( r, - f.app(Value::from_builtin(Natural)) - .app(make_closure!(λ(x : Natural) -> 1 + var(x, 0))) - .app( - NaturalLit(0) - .into_value_with_type(Value::from_builtin(Natural)), - ) - .into_vovf(), + Ret::Value( + f.app(Value::from_builtin(Natural)) + .app(make_closure!(λ(x : Natural) -> 1 + var(x, 0))) + .app(NaturalLit(0).into_value_with_type( + Value::from_builtin(Natural), + )), + ), )), }, (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() { - NaturalLit(0) => Ok((r, zero.clone().into_vovf())), + NaturalLit(0) => Ok((r, Ret::ValueRef(zero))), NaturalLit(n) => { let fold = Value::from_builtin(NaturalFold) .app( @@ -343,14 +368,15 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { .app(t.clone()) .app(succ.clone()) .app(zero.clone()); - Ok((r, succ.app(fold).into_vovf())) + Ok((r, Ret::Value(succ.app(fold)))) } _ => Err(()), }, _ => Err(()), }; match ret { - Ok((unconsumed_args, mut v)) => { + Ok((unconsumed_args, ret)) => { + let mut v = ret.into_vovf_whnf(); let n_consumed_args = args.len() - unconsumed_args.len(); for x in args.into_iter().skip(n_consumed_args) { v = v.app(x); @@ -485,15 +511,6 @@ where kvs } -// Small helper enum to avoid repetition -enum Ret<'a> { - ValueF(ValueF), - Value(Value), - VoVF(VoVF), - ValueRef(&'a Value), - Expr(ExprF), -} - fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { use BinOp::{ BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus, @@ -778,13 +795,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> VoVF { } }; - match ret { - Ret::ValueF(v) => v.into_vovf_whnf(), - Ret::Value(v) => v.into_vovf(), - Ret::VoVF(v) => v, - Ret::ValueRef(v) => v.clone().into_vovf(), - Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf_whnf(), - } + ret.into_vovf_whnf() } /// Normalize a ValueF into WHNF -- cgit v1.2.3 From d9e3bcca9b4350cbc1db2545d7ed28dde4e12be4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 23 Aug 2019 18:34:43 +0200 Subject: Keep type information after RecursiveRecordTypeMerge --- dhall/src/phase/normalize.rs | 75 ++++++++------------------------------------ 1 file changed, 13 insertions(+), 62 deletions(-) (limited to 'dhall/src/phase/normalize.rs') diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 0c4e185..28dc0f6 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -452,53 +452,20 @@ pub(crate) fn squash_textlit( ret } -/// Performs an intersection of two HashMaps. -/// -/// # Arguments -/// -/// * `f` - Will compute the final value from the intersecting -/// key and the values from both maps. -/// -/// # Description -/// -/// If the key is present in both maps then the final value for -/// that key is computed via the `f` function. -/// -/// The final map will contain the shared keys from the -/// two input maps with the final computed value from `f`. -pub(crate) fn intersection_with_key( - mut f: impl FnMut(&K, &T, &U) -> V, - map1: &HashMap, - map2: &HashMap, -) -> HashMap -where - K: std::hash::Hash + Eq + Clone, -{ - let mut kvs = HashMap::new(); - - for (k, t) in map1 { - // Only insert in the final map if the key exists in both - if let Some(u) = map2.get(k) { - kvs.insert(k.clone(), f(k, t, u)); - } - } - - kvs -} - -pub(crate) fn merge_maps( +pub(crate) fn merge_maps( map1: &HashMap, map2: &HashMap, - mut f: impl FnMut(&V, &V) -> V, -) -> HashMap + mut f: F, +) -> Result, Err> where + F: FnMut(&V, &V) -> Result, K: std::hash::Hash + Eq + Clone, V: Clone, { let mut kvs = HashMap::new(); for (x, v2) in map2 { let newv = if let Some(v1) = map1.get(x) { - f(v1, v2) + f(v1, v2)? } else { v2.clone() }; @@ -508,7 +475,7 @@ where // Insert only if key not already present kvs.entry(x.clone()).or_insert_with(|| v1.clone()); } - kvs + Ok(kvs) } fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { @@ -518,8 +485,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { RightBiasedRecordMerge, TextAppend, }; use ValueF::{ - BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, - TextLit, + BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, TextLit, }; let x_borrow = x.as_whnf(); let y_borrow = y.as_whnf(); @@ -604,31 +570,16 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { Ret::ValueRef(y) } (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let kvs = merge_maps(kvs1, kvs2, |v1, v2| { - Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp( - RecursiveRecordMerge, - v1.clone(), - v2.clone(), + let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |v1, v2| { + Ok(Value::from_valuef_untyped(ValueF::PartialExpr( + ExprF::BinOp(RecursiveRecordMerge, v1.clone(), v2.clone()), ))) - }); + })?; Ret::ValueF(RecordLit(kvs)) } - (RecursiveRecordTypeMerge, _, RecordType(kvs)) if kvs.is_empty() => { - Ret::ValueRef(x) - } - (RecursiveRecordTypeMerge, RecordType(kvs), _) if kvs.is_empty() => { - Ret::ValueRef(y) - } - (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => { - let kvs = merge_maps(kvs1, kvs2, |v1, v2| { - Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp( - RecursiveRecordTypeMerge, - v1.clone(), - v2.clone(), - ))) - }); - Ret::ValueF(RecordType(kvs)) + (RecursiveRecordTypeMerge, _, _) => { + unreachable!("This case should have been handled in typecheck") } (Equivalence, _, _) => { -- cgit v1.2.3 From d5bdd48d4c34b4e213e3e2431936c160e4320a80 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 23 Aug 2019 18:53:46 +0200 Subject: Clarify which syntax elements are completely handled in the tck phase --- dhall/src/phase/normalize.rs | 40 ++++++++++++++++++---------------------- 1 file changed, 18 insertions(+), 22 deletions(-) (limited to 'dhall/src/phase/normalize.rs') diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 28dc0f6..c8f5bc2 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -578,39 +578,41 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { Ret::ValueF(RecordLit(kvs)) } - (RecursiveRecordTypeMerge, _, _) => { + (RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => { unreachable!("This case should have been handled in typecheck") } - (Equivalence, _, _) => { - Ret::ValueF(ValueF::Equivalence(x.clone(), y.clone())) - } - _ => return None, }) } pub(crate) fn normalize_one_layer(expr: ExprF) -> VoVF { use ValueF::{ - AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam, - NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType, - TextLit, UnionConstructor, UnionLit, UnionType, + AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, + NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit, + UnionConstructor, UnionLit, UnionType, }; let ret = match expr { ExprF::Import(_) => unreachable!( "There should remain no imports in a resolved expression" ), - ExprF::Embed(_) => unreachable!(), - ExprF::Var(_) => unreachable!(), - ExprF::Annot(x, _) => Ret::Value(x), + // Those cases have already been completely handled in the typechecking phase (using + // `RetWhole`), so they won't appear here. + ExprF::Lam(_, _, _) + | ExprF::Pi(_, _, _) + | ExprF::Let(_, _, _, _) + | ExprF::Embed(_) + | ExprF::Const(_) + | ExprF::Builtin(_) + | ExprF::Var(_) + | ExprF::Annot(_, _) + | ExprF::RecordType(_) + | ExprF::UnionType(_) => { + unreachable!("This case should have been handled in typecheck") + } ExprF::Assert(_) => Ret::Expr(expr), - 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::Value(v.app(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)), @@ -635,12 +637,6 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> VoVF { ExprF::RecordLit(kvs) => { 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::TextLit(elts) => { use InterpolatedTextContents::Expr; let elts: Vec<_> = squash_textlit(elts.into_iter()); -- cgit v1.2.3 From 98399997cf289d802fbed674558665547cf73d59 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 16:09:55 +0200 Subject: Keep type information through normalization --- dhall/src/phase/normalize.rs | 200 ++++++++++++++++++++++++++++--------------- 1 file changed, 131 insertions(+), 69 deletions(-) (limited to 'dhall/src/phase/normalize.rs') diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index c8f5bc2..5743b0d 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -1,5 +1,6 @@ use std::collections::HashMap; +use dhall_syntax::Const::Type; use dhall_syntax::{ BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label, NaiveDouble, @@ -7,7 +8,7 @@ use dhall_syntax::{ use crate::core::value::{Value, VoVF}; use crate::core::valuef::ValueF; -use crate::core::var::{Shift, Subst}; +use crate::core::var::{AlphaLabel, Shift, Subst}; use crate::phase::Normalized; // Small helper enum to avoid repetition @@ -32,21 +33,24 @@ impl<'a> Ret<'a> { // Ad-hoc macro to help construct closures macro_rules! make_closure { (#$var:ident) => { $var.clone() }; - (var($var:ident, $n:expr)) => {{ + (var($var:ident, $n:expr, $($ty:tt)*)) => {{ let var = crate::core::var::AlphaVar::from_var_and_alpha( Label::from(stringify!($var)).into(), $n ); - ValueF::Var(var).into_value_untyped() + ValueF::Var(var) + .into_value_with_type(make_closure!($($ty)*)) }}; // Warning: assumes that $ty, as a dhall value, has type `Type` - (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { - ValueF::Lam( - Label::from(stringify!($var)).into(), - make_closure!($($ty)*), - make_closure!($($rest)*), - ).into_value_untyped() - }; + (λ($var:ident : $($ty:tt)*) -> $($body:tt)*) => {{ + let var: AlphaLabel = Label::from(stringify!($var)).into(); + let ty = make_closure!($($ty)*); + let body = make_closure!($($body)*); + let body_ty = body.get_type().expect("Internal type error"); + let lam_ty = ValueF::Pi(var.clone(), ty.clone(), body_ty) + .into_value_with_type(Value::from_const(Type)); + ValueF::Lam(var, ty, body).into_value_with_type(lam_ty) + }}; (Natural) => { Value::from_builtin(Builtin::Natural) }; @@ -54,10 +58,12 @@ macro_rules! make_closure { Value::from_builtin(Builtin::List) .app(make_closure!($($rest)*)) }; - (Some($($rest:tt)*)) => { - ValueF::NEOptionalLit(make_closure!($($rest)*)) - .into_value_untyped() - }; + (Some($($rest:tt)*)) => {{ + let v = make_closure!($($rest)*); + let v_type = v.get_type().expect("Internal type error"); + ValueF::NEOptionalLit(v) + .into_value_with_type(v_type) + }}; (1 + $($rest:tt)*) => { ValueF::PartialExpr(ExprF::BinOp( dhall_syntax::BinOp::NaturalPlus, @@ -70,18 +76,25 @@ macro_rules! make_closure { make_closure!(Natural) ) }; - ([ $($head:tt)* ] # $($tail:tt)*) => { + ([ $($head:tt)* ] # $($tail:tt)*) => {{ + let head = make_closure!($($head)*); + let tail = make_closure!($($tail)*); + let list_type = tail.get_type().expect("Internal type error"); ValueF::PartialExpr(ExprF::BinOp( dhall_syntax::BinOp::ListAppend, - ValueF::NEListLit(vec![make_closure!($($head)*)]) - .into_value_untyped(), - make_closure!($($tail)*), - )).into_value_untyped() - }; + ValueF::NEListLit(vec![head]) + .into_value_with_type(list_type.clone()), + tail, + )).into_value_with_type(list_type) + }}; } #[allow(clippy::cognitive_complexity)] -pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { +pub(crate) fn apply_builtin( + b: Builtin, + args: Vec, + _ty: Option<&Value>, +) -> VoVF { use dhall_syntax::Builtin::*; use ValueF::*; @@ -231,37 +244,60 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { )), _ => Err(()), }, - (ListIndexed, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(t) => { - let mut kts = HashMap::new(); - kts.insert("index".into(), Value::from_builtin(Natural)); - kts.insert("value".into(), t.clone()); - Ok(( - r, - Ret::ValueF(EmptyListLit(Value::from_valuef_untyped( + (ListIndexed, [_, l, r..]) => { + let l_whnf = l.as_whnf(); + match &*l_whnf { + EmptyListLit(_) | NEListLit(_) => { + // Extract the type of the list elements + let t = match &*l_whnf { + EmptyListLit(t) => t.clone(), + NEListLit(xs) => { + xs[0].get_type().expect("Internal type error") + } + _ => unreachable!(), + }; + + // Construct the returned record type: { index: Natural, value: t } + let mut kts = HashMap::new(); + kts.insert("index".into(), Value::from_builtin(Natural)); + kts.insert("value".into(), t.clone()); + let t = Value::from_valuef_and_type( RecordType(kts), - ))), - )) - } - NEListLit(xs) => { - let xs = xs - .iter() - .enumerate() - .map(|(i, e)| { - let i = NaturalLit(i); - let mut kvs = HashMap::new(); - kvs.insert( - "index".into(), - Value::from_valuef_untyped(i), - ); - kvs.insert("value".into(), e.clone()); - Value::from_valuef_untyped(RecordLit(kvs)) - }) - .collect(); - Ok((r, Ret::ValueF(NEListLit(xs)))) + Value::from_const(Type), + ); + + // Construct the new list, with added indices + let list = match &*l_whnf { + EmptyListLit(_) => EmptyListLit(t), + NEListLit(xs) => NEListLit( + xs.iter() + .enumerate() + .map(|(i, e)| { + let mut kvs = HashMap::new(); + kvs.insert( + "index".into(), + Value::from_valuef_and_type( + NaturalLit(i), + Value::from_builtin( + Builtin::Natural, + ), + ), + ); + kvs.insert("value".into(), e.clone()); + Value::from_valuef_and_type( + RecordLit(kvs), + t.clone(), + ) + }) + .collect(), + ), + _ => unreachable!(), + }; + Ok((r, Ret::ValueF(list))) + } + _ => Err(()), } - _ => Err(()), - }, + } (ListBuild, [t, f, r..]) => match &*f.as_whnf() { // fold/build fusion ValueF::AppliedBuiltin(ListFold, args) => { @@ -279,12 +315,13 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { Ret::Value( f.app(list_t.clone()) .app({ - // Move `t` under new `x` variable + // Move `t` under new variables let t1 = t.under_binder(Label::from("x")); + let t2 = t1.under_binder(Label::from("xs")); make_closure!( λ(x : #t) -> λ(xs : List #t1) -> - [ var(x, 1) ] # var(xs, 0) + [ var(x, 1, #t2) ] # var(xs, 0, List #t2) ) }) .app( @@ -322,7 +359,10 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { r, Ret::Value( f.app(optional_t.clone()) - .app(make_closure!(λ(x: #t) -> Some(var(x, 0)))) + .app({ + let t1 = t.under_binder(Label::from("x")); + make_closure!(λ(x: #t) -> Some(var(x, 0, #t1))) + }) .app( EmptyOptionalLit(t.clone()) .into_value_with_type(optional_t), @@ -350,7 +390,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { r, Ret::Value( f.app(Value::from_builtin(Natural)) - .app(make_closure!(λ(x : Natural) -> 1 + var(x, 0))) + .app(make_closure!( + λ(x : Natural) -> 1 + var(x, 0, Natural) + )) .app(NaturalLit(0).into_value_with_type( Value::from_builtin(Natural), )), @@ -387,7 +429,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> VoVF { } } -pub(crate) fn apply_any(f: Value, a: Value) -> VoVF { +pub(crate) fn apply_any(f: Value, a: Value, ty: Option<&Value>) -> VoVF { let fallback = |f: Value, a: Value| { ValueF::PartialExpr(ExprF::App(f, a)).into_vovf_whnf() }; @@ -398,7 +440,7 @@ pub(crate) fn apply_any(f: Value, a: Value) -> VoVF { ValueF::AppliedBuiltin(b, args) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); - apply_builtin(*b, args) + apply_builtin(*b, args, ty) } ValueF::UnionConstructor(l, kts) => { ValueF::UnionLit(l.clone(), a, kts.clone()).into_vovf_whnf() @@ -458,14 +500,14 @@ pub(crate) fn merge_maps( mut f: F, ) -> Result, Err> where - F: FnMut(&V, &V) -> Result, + F: FnMut(&K, &V, &V) -> Result, K: std::hash::Hash + Eq + Clone, V: Clone, { let mut kvs = HashMap::new(); for (x, v2) in map2 { let newv = if let Some(v1) = map1.get(x) { - f(v1, v2)? + f(x, v1, v2)? } else { v2.clone() }; @@ -478,14 +520,20 @@ where Ok(kvs) } -fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { +fn apply_binop<'a>( + o: BinOp, + x: &'a Value, + y: &'a Value, + ty: Option<&Value>, +) -> Option> { use BinOp::{ BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus, NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, RightBiasedRecordMerge, TextAppend, }; use ValueF::{ - BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, TextLit, + BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, + TextLit, }; let x_borrow = x.as_whnf(); let y_borrow = y.as_whnf(); @@ -570,10 +618,21 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { Ret::ValueRef(y) } (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |v1, v2| { - Ok(Value::from_valuef_untyped(ValueF::PartialExpr( - ExprF::BinOp(RecursiveRecordMerge, v1.clone(), v2.clone()), - ))) + let ty = ty.expect("Internal type error"); + let ty_borrow = ty.as_whnf(); + let kts = match &*ty_borrow { + RecordType(kts) => kts, + _ => unreachable!("Internal type error"), + }; + let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| { + Ok(Value::from_valuef_and_type( + ValueF::PartialExpr(ExprF::BinOp( + RecursiveRecordMerge, + v1.clone(), + v2.clone(), + )), + kts.get(k).expect("Internal type error").clone(), + )) })?; Ret::ValueF(RecordLit(kvs)) } @@ -586,7 +645,10 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { }) } -pub(crate) fn normalize_one_layer(expr: ExprF) -> VoVF { +pub(crate) fn normalize_one_layer( + expr: ExprF, + ty: Option<&Value>, +) -> VoVF { use ValueF::{ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit, @@ -669,7 +731,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> VoVF { } } } - ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) { + ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) { Some(ret) => ret, None => Ret::Expr(expr), }, @@ -746,10 +808,10 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> VoVF { } /// Normalize a ValueF into WHNF -pub(crate) fn normalize_whnf(v: ValueF) -> VoVF { +pub(crate) fn normalize_whnf(v: ValueF, ty: Option<&Value>) -> VoVF { match v { - ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args), - ValueF::PartialExpr(e) => normalize_one_layer(e), + ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty), + ValueF::PartialExpr(e) => normalize_one_layer(e, ty), ValueF::TextLit(elts) => { ValueF::TextLit(squash_textlit(elts.into_iter())).into_vovf_whnf() } -- cgit v1.2.3 From 80fb5355ea90377492b9863f632c01a808f8aade Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 16:33:12 +0200 Subject: Check consistency of type information --- dhall/src/phase/normalize.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dhall/src/phase/normalize.rs') diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 5743b0d..fe99696 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -61,8 +61,8 @@ macro_rules! make_closure { (Some($($rest:tt)*)) => {{ let v = make_closure!($($rest)*); let v_type = v.get_type().expect("Internal type error"); - ValueF::NEOptionalLit(v) - .into_value_with_type(v_type) + let opt_v_type = Value::from_builtin(Builtin::Optional).app(v_type); + ValueF::NEOptionalLit(v).into_value_with_type(opt_v_type) }}; (1 + $($rest:tt)*) => { ValueF::PartialExpr(ExprF::BinOp( -- cgit v1.2.3 From f9ec2cdf2803ed92fa404db989b786fc1dfac12e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 17:07:59 +0200 Subject: Enforce type information almost everywhere --- dhall/src/phase/normalize.rs | 25 +++++++++---------------- 1 file changed, 9 insertions(+), 16 deletions(-) (limited to 'dhall/src/phase/normalize.rs') diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index fe99696..9837a8b 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -46,7 +46,7 @@ macro_rules! make_closure { let var: AlphaLabel = Label::from(stringify!($var)).into(); let ty = make_closure!($($ty)*); let body = make_closure!($($body)*); - let body_ty = body.get_type().expect("Internal type error"); + let body_ty = body.get_type_not_sort(); let lam_ty = ValueF::Pi(var.clone(), ty.clone(), body_ty) .into_value_with_type(Value::from_const(Type)); ValueF::Lam(var, ty, body).into_value_with_type(lam_ty) @@ -60,7 +60,7 @@ macro_rules! make_closure { }; (Some($($rest:tt)*)) => {{ let v = make_closure!($($rest)*); - let v_type = v.get_type().expect("Internal type error"); + let v_type = v.get_type_not_sort(); let opt_v_type = Value::from_builtin(Builtin::Optional).app(v_type); ValueF::NEOptionalLit(v).into_value_with_type(opt_v_type) }}; @@ -79,7 +79,7 @@ macro_rules! make_closure { ([ $($head:tt)* ] # $($tail:tt)*) => {{ let head = make_closure!($($head)*); let tail = make_closure!($($tail)*); - let list_type = tail.get_type().expect("Internal type error"); + let list_type = tail.get_type_not_sort(); ValueF::PartialExpr(ExprF::BinOp( dhall_syntax::BinOp::ListAppend, ValueF::NEListLit(vec![head]) @@ -90,11 +90,7 @@ macro_rules! make_closure { } #[allow(clippy::cognitive_complexity)] -pub(crate) fn apply_builtin( - b: Builtin, - args: Vec, - _ty: Option<&Value>, -) -> VoVF { +pub(crate) fn apply_builtin(b: Builtin, args: Vec, _ty: &Value) -> VoVF { use dhall_syntax::Builtin::*; use ValueF::*; @@ -251,9 +247,7 @@ pub(crate) fn apply_builtin( // Extract the type of the list elements let t = match &*l_whnf { EmptyListLit(t) => t.clone(), - NEListLit(xs) => { - xs[0].get_type().expect("Internal type error") - } + NEListLit(xs) => xs[0].get_type_not_sort(), _ => unreachable!(), }; @@ -429,7 +423,7 @@ pub(crate) fn apply_builtin( } } -pub(crate) fn apply_any(f: Value, a: Value, ty: Option<&Value>) -> VoVF { +pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> VoVF { let fallback = |f: Value, a: Value| { ValueF::PartialExpr(ExprF::App(f, a)).into_vovf_whnf() }; @@ -524,7 +518,7 @@ fn apply_binop<'a>( o: BinOp, x: &'a Value, y: &'a Value, - ty: Option<&Value>, + ty: &Value, ) -> Option> { use BinOp::{ BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus, @@ -618,7 +612,6 @@ fn apply_binop<'a>( Ret::ValueRef(y) } (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let ty = ty.expect("Internal type error"); let ty_borrow = ty.as_whnf(); let kts = match &*ty_borrow { RecordType(kts) => kts, @@ -647,7 +640,7 @@ fn apply_binop<'a>( pub(crate) fn normalize_one_layer( expr: ExprF, - ty: Option<&Value>, + ty: &Value, ) -> VoVF { use ValueF::{ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, @@ -808,7 +801,7 @@ pub(crate) fn normalize_one_layer( } /// Normalize a ValueF into WHNF -pub(crate) fn normalize_whnf(v: ValueF, ty: Option<&Value>) -> VoVF { +pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> VoVF { match v { ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty), ValueF::PartialExpr(e) => normalize_one_layer(e, ty), -- cgit v1.2.3 From bf37fd9da3782134ca4bca9567c34bbee81784b9 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 21:16:38 +0200 Subject: Rework apply_builtin to enforce preservation of type information --- dhall/src/phase/normalize.rs | 339 ++++++++++++++++++++----------------------- 1 file changed, 156 insertions(+), 183 deletions(-) (limited to 'dhall/src/phase/normalize.rs') diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 9837a8b..77f5023 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -11,25 +11,6 @@ use crate::core::valuef::ValueF; use crate::core::var::{AlphaLabel, Shift, Subst}; use crate::phase::Normalized; -// Small helper enum to avoid repetition -enum Ret<'a> { - ValueF(ValueF), - Value(Value), - ValueRef(&'a Value), - Expr(ExprF), -} - -impl<'a> Ret<'a> { - fn into_vovf_whnf(self) -> VoVF { - match self { - Ret::ValueF(v) => v.into_vovf_whnf(), - Ret::Value(v) => v.into_vovf(), - Ret::ValueRef(v) => v.clone().into_vovf(), - Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf_whnf(), - } - } -} - // Ad-hoc macro to help construct closures macro_rules! make_closure { (#$var:ident) => { $var.clone() }; @@ -94,80 +75,77 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec, _ty: &Value) -> VoVF { use dhall_syntax::Builtin::*; use ValueF::*; - // Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced. + // Small helper enum + enum Ret<'a> { + ValueF(ValueF), + Value(Value), + // For applications that can return a function, it's important to keep the remaining + // arguments to apply them to the resulting function. + ValueWithRemainingArgs(&'a [Value], Value), + DoneAsIs, + } + let ret = match (b, args.as_slice()) { - (OptionalNone, [t, r..]) => { - Ok((r, Ret::ValueF(EmptyOptionalLit(t.clone())))) - } - (NaturalIsZero, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, Ret::ValueF(BoolLit(*n == 0)))), - _ => Err(()), + (OptionalNone, [t]) => Ret::ValueF(EmptyOptionalLit(t.clone())), + (NaturalIsZero, [n]) => match &*n.as_whnf() { + NaturalLit(n) => Ret::ValueF(BoolLit(*n == 0)), + _ => Ret::DoneAsIs, }, - (NaturalEven, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, Ret::ValueF(BoolLit(*n % 2 == 0)))), - _ => Err(()), + (NaturalEven, [n]) => match &*n.as_whnf() { + NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 == 0)), + _ => Ret::DoneAsIs, }, - (NaturalOdd, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, Ret::ValueF(BoolLit(*n % 2 != 0)))), - _ => Err(()), + (NaturalOdd, [n]) => match &*n.as_whnf() { + NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 != 0)), + _ => Ret::DoneAsIs, }, - (NaturalToInteger, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok((r, Ret::ValueF(IntegerLit(*n as isize)))), - _ => Err(()), + (NaturalToInteger, [n]) => match &*n.as_whnf() { + NaturalLit(n) => Ret::ValueF(IntegerLit(*n as isize)), + _ => Ret::DoneAsIs, }, - (NaturalShow, [n, r..]) => match &*n.as_whnf() { - NaturalLit(n) => Ok(( - r, + (NaturalShow, [n]) => match &*n.as_whnf() { + NaturalLit(n) => { Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text( n.to_string(), - )])), - )), - _ => Err(()), + )])) + } + _ => Ret::DoneAsIs, }, - (NaturalSubtract, [a, b, r..]) => { - match (&*a.as_whnf(), &*b.as_whnf()) { - (NaturalLit(a), NaturalLit(b)) => Ok(( - r, - Ret::ValueF(NaturalLit(if b > a { b - a } else { 0 })), - )), - (NaturalLit(0), _) => Ok((r, Ret::ValueRef(b))), - (_, NaturalLit(0)) => Ok((r, Ret::ValueF(NaturalLit(0)))), - _ if a == b => Ok((r, Ret::ValueF(NaturalLit(0)))), - _ => Err(()), + (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) { + (NaturalLit(a), NaturalLit(b)) => { + Ret::ValueF(NaturalLit(if b > a { b - a } else { 0 })) } - } - (IntegerShow, [n, r..]) => match &*n.as_whnf() { + (NaturalLit(0), _) => Ret::Value(b.clone()), + (_, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)), + _ if a == b => Ret::ValueF(NaturalLit(0)), + _ => Ret::DoneAsIs, + }, + (IntegerShow, [n]) => match &*n.as_whnf() { IntegerLit(n) => { let s = if *n < 0 { n.to_string() } else { format!("+{}", n) }; - Ok(( - r, - Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text( - s, - )])), - )) + Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(s)])) } - _ => Err(()), + _ => Ret::DoneAsIs, }, - (IntegerToDouble, [n, r..]) => match &*n.as_whnf() { + (IntegerToDouble, [n]) => match &*n.as_whnf() { IntegerLit(n) => { - Ok((r, Ret::ValueF(DoubleLit(NaiveDouble::from(*n as f64))))) + Ret::ValueF(DoubleLit(NaiveDouble::from(*n as f64))) } - _ => Err(()), + _ => Ret::DoneAsIs, }, - (DoubleShow, [n, r..]) => match &*n.as_whnf() { - DoubleLit(n) => Ok(( - r, + (DoubleShow, [n]) => match &*n.as_whnf() { + DoubleLit(n) => { Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text( n.to_string(), - )])), - )), - _ => Err(()), + )])) + } + _ => Ret::DoneAsIs, }, - (TextShow, [v, r..]) => match &*v.as_whnf() { + (TextShow, [v]) => match &*v.as_whnf() { TextLit(elts) => { match elts.as_slice() { // Empty string literal. @@ -176,12 +154,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec, _ty: &Value) -> VoVF { let txt: InterpolatedText = std::iter::empty().collect(); let s = txt.to_string(); - Ok(( - r, - Ret::ValueF(TextLit(vec![ - InterpolatedTextContents::Text(s), - ])), - )) + Ret::ValueF(TextLit(vec![ + InterpolatedTextContents::Text(s), + ])) } // If there are no interpolations (invariants ensure that when there are no // interpolations, there is a single Text item) in the literal. @@ -193,54 +168,42 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec, _ty: &Value) -> VoVF { )) .collect(); let s = txt.to_string(); - Ok(( - r, - Ret::ValueF(TextLit(vec![ - InterpolatedTextContents::Text(s), - ])), - )) + Ret::ValueF(TextLit(vec![ + InterpolatedTextContents::Text(s), + ])) } - _ => Err(()), + _ => Ret::DoneAsIs, } } - _ => Err(()), + _ => Ret::DoneAsIs, }, - (ListLength, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(_) => Ok((r, Ret::ValueF(NaturalLit(0)))), - NEListLit(xs) => Ok((r, Ret::ValueF(NaturalLit(xs.len())))), - _ => Err(()), + (ListLength, [_, l]) => match &*l.as_whnf() { + EmptyListLit(_) => Ret::ValueF(NaturalLit(0)), + NEListLit(xs) => Ret::ValueF(NaturalLit(xs.len())), + _ => Ret::DoneAsIs, }, - (ListHead, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(n) => { - Ok((r, Ret::ValueF(EmptyOptionalLit(n.clone())))) + (ListHead, [_, l]) => match &*l.as_whnf() { + EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())), + NEListLit(xs) => { + Ret::ValueF(NEOptionalLit(xs.iter().next().unwrap().clone())) } - NEListLit(xs) => Ok(( - r, - Ret::ValueF(NEOptionalLit(xs.iter().next().unwrap().clone())), - )), - _ => Err(()), + _ => Ret::DoneAsIs, }, - (ListLast, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(n) => { - Ok((r, Ret::ValueF(EmptyOptionalLit(n.clone())))) - } - NEListLit(xs) => Ok(( - r, - Ret::ValueF(NEOptionalLit( - xs.iter().rev().next().unwrap().clone(), - )), + (ListLast, [_, l]) => match &*l.as_whnf() { + EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())), + NEListLit(xs) => Ret::ValueF(NEOptionalLit( + xs.iter().rev().next().unwrap().clone(), )), - _ => Err(()), + _ => Ret::DoneAsIs, }, - (ListReverse, [_, l, r..]) => match &*l.as_whnf() { - EmptyListLit(n) => Ok((r, Ret::ValueF(EmptyListLit(n.clone())))), - NEListLit(xs) => Ok(( - r, - Ret::ValueF(NEListLit(xs.iter().rev().cloned().collect())), - )), - _ => Err(()), + (ListReverse, [_, l]) => match &*l.as_whnf() { + EmptyListLit(n) => Ret::ValueF(EmptyListLit(n.clone())), + NEListLit(xs) => { + Ret::ValueF(NEListLit(xs.iter().rev().cloned().collect())) + } + _ => Ret::DoneAsIs, }, - (ListIndexed, [_, l, r..]) => { + (ListIndexed, [_, l]) => { let l_whnf = l.as_whnf(); match &*l_whnf { EmptyListLit(_) | NEListLit(_) => { @@ -287,16 +250,16 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec, _ty: &Value) -> VoVF { ), _ => unreachable!(), }; - Ok((r, Ret::ValueF(list))) + Ret::ValueF(list) } - _ => Err(()), + _ => Ret::DoneAsIs, } } - (ListBuild, [t, f, r..]) => match &*f.as_whnf() { + (ListBuild, [t, f]) => match &*f.as_whnf() { // fold/build fusion ValueF::AppliedBuiltin(ListFold, args) => { if args.len() >= 2 { - Ok((r, Ret::Value(args[1].clone()))) + Ret::Value(args[1].clone()) } else { // Do we really need to handle this case ? unimplemented!() @@ -304,44 +267,41 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec, _ty: &Value) -> VoVF { } _ => { let list_t = Value::from_builtin(List).app(t.clone()); - Ok(( - r, - Ret::Value( - f.app(list_t.clone()) - .app({ - // Move `t` under new variables - let t1 = t.under_binder(Label::from("x")); - let t2 = t1.under_binder(Label::from("xs")); - make_closure!( - λ(x : #t) -> - λ(xs : List #t1) -> - [ var(x, 1, #t2) ] # var(xs, 0, List #t2) - ) - }) - .app( - EmptyListLit(t.clone()) - .into_value_with_type(list_t), - ), - ), - )) + Ret::Value( + f.app(list_t.clone()) + .app({ + // Move `t` under new variables + let t1 = t.under_binder(Label::from("x")); + let t2 = t1.under_binder(Label::from("xs")); + make_closure!( + λ(x : #t) -> + λ(xs : List #t1) -> + [ var(x, 1, #t2) ] # var(xs, 0, List #t2) + ) + }) + .app( + EmptyListLit(t.clone()) + .into_value_with_type(list_t), + ), + ) } }, (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() { - EmptyListLit(_) => Ok((r, Ret::ValueRef(nil))), + EmptyListLit(_) => Ret::ValueWithRemainingArgs(r, nil.clone()), NEListLit(xs) => { let mut v = nil.clone(); for x in xs.iter().cloned().rev() { v = cons.app(x).app(v); } - Ok((r, Ret::Value(v))) + Ret::ValueWithRemainingArgs(r, v) } - _ => Err(()), + _ => Ret::DoneAsIs, }, - (OptionalBuild, [t, f, r..]) => match &*f.as_whnf() { + (OptionalBuild, [t, f]) => match &*f.as_whnf() { // fold/build fusion ValueF::AppliedBuiltin(OptionalFold, args) => { if args.len() >= 2 { - Ok((r, Ret::Value(args[1].clone()))) + Ret::Value(args[1].clone()) } else { // Do we really need to handle this case ? unimplemented!() @@ -349,52 +309,51 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec, _ty: &Value) -> VoVF { } _ => { let optional_t = Value::from_builtin(Optional).app(t.clone()); - Ok(( - r, - Ret::Value( - f.app(optional_t.clone()) - .app({ - let t1 = t.under_binder(Label::from("x")); - make_closure!(λ(x: #t) -> Some(var(x, 0, #t1))) - }) - .app( - EmptyOptionalLit(t.clone()) - .into_value_with_type(optional_t), - ), - ), - )) + Ret::Value( + f.app(optional_t.clone()) + .app({ + let t1 = t.under_binder(Label::from("x")); + make_closure!(λ(x: #t) -> Some(var(x, 0, #t1))) + }) + .app( + EmptyOptionalLit(t.clone()) + .into_value_with_type(optional_t), + ), + ) } }, (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() { - EmptyOptionalLit(_) => Ok((r, Ret::ValueRef(nothing))), - NEOptionalLit(x) => Ok((r, Ret::Value(just.app(x.clone())))), - _ => Err(()), + EmptyOptionalLit(_) => { + Ret::ValueWithRemainingArgs(r, nothing.clone()) + } + NEOptionalLit(x) => { + Ret::ValueWithRemainingArgs(r, just.app(x.clone())) + } + _ => Ret::DoneAsIs, }, - (NaturalBuild, [f, r..]) => match &*f.as_whnf() { + (NaturalBuild, [f]) => match &*f.as_whnf() { // fold/build fusion ValueF::AppliedBuiltin(NaturalFold, args) => { if !args.is_empty() { - Ok((r, Ret::Value(args[0].clone()))) + Ret::Value(args[0].clone()) } else { // Do we really need to handle this case ? unimplemented!() } } - _ => Ok(( - r, - Ret::Value( - f.app(Value::from_builtin(Natural)) - .app(make_closure!( - λ(x : Natural) -> 1 + var(x, 0, Natural) - )) - .app(NaturalLit(0).into_value_with_type( - Value::from_builtin(Natural), - )), - ), - )), + _ => Ret::Value( + f.app(Value::from_builtin(Natural)) + .app(make_closure!( + λ(x : Natural) -> 1 + var(x, 0, Natural) + )) + .app( + NaturalLit(0) + .into_value_with_type(Value::from_builtin(Natural)), + ), + ), }, (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() { - NaturalLit(0) => Ok((r, Ret::ValueRef(zero))), + NaturalLit(0) => Ret::ValueWithRemainingArgs(r, zero.clone()), NaturalLit(n) => { let fold = Value::from_builtin(NaturalFold) .app( @@ -404,22 +363,23 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec, _ty: &Value) -> VoVF { .app(t.clone()) .app(succ.clone()) .app(zero.clone()); - Ok((r, Ret::Value(succ.app(fold)))) + Ret::ValueWithRemainingArgs(r, succ.app(fold)) } - _ => Err(()), + _ => Ret::DoneAsIs, }, - _ => Err(()), + _ => Ret::DoneAsIs, }; match ret { - Ok((unconsumed_args, ret)) => { - let mut v = ret.into_vovf_whnf(); + Ret::ValueF(v) => v.into_vovf_whnf(), + Ret::Value(v) => v.into_vovf(), + Ret::ValueWithRemainingArgs(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(x); } - v + v.into_vovf() } - Err(()) => AppliedBuiltin(b, args).into_vovf_whnf(), + Ret::DoneAsIs => AppliedBuiltin(b, args).into_vovf_whnf(), } } @@ -514,6 +474,14 @@ where Ok(kvs) } +// Small helper enum to avoid repetition +enum Ret<'a> { + ValueF(ValueF), + Value(Value), + ValueRef(&'a Value), + Expr(ExprF), +} + fn apply_binop<'a>( o: BinOp, x: &'a Value, @@ -797,7 +765,12 @@ pub(crate) fn normalize_one_layer( } }; - ret.into_vovf_whnf() + match ret { + Ret::ValueF(v) => v.into_vovf_whnf(), + Ret::Value(v) => v.into_vovf(), + Ret::ValueRef(v) => v.clone().into_vovf(), + Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf_whnf(), + } } /// Normalize a ValueF into WHNF -- cgit v1.2.3 From 906cbf5fc4c3bee65f24df1604497e33c6a20833 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 21:52:59 +0200 Subject: Remove now unnecessary VoVF enum --- dhall/src/phase/normalize.rs | 46 +++++++++++++++++++++++--------------------- 1 file changed, 24 insertions(+), 22 deletions(-) (limited to 'dhall/src/phase/normalize.rs') diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 77f5023..82a378c 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -6,7 +6,7 @@ use dhall_syntax::{ NaiveDouble, }; -use crate::core::value::{Value, VoVF}; +use crate::core::value::Value; use crate::core::valuef::ValueF; use crate::core::var::{AlphaLabel, Shift, Subst}; use crate::phase::Normalized; @@ -71,7 +71,11 @@ macro_rules! make_closure { } #[allow(clippy::cognitive_complexity)] -pub(crate) fn apply_builtin(b: Builtin, args: Vec, _ty: &Value) -> VoVF { +pub(crate) fn apply_builtin( + b: Builtin, + args: Vec, + ty: &Value, +) -> ValueF { use dhall_syntax::Builtin::*; use ValueF::*; @@ -370,38 +374,36 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec, _ty: &Value) -> VoVF { _ => Ret::DoneAsIs, }; match ret { - Ret::ValueF(v) => v.into_vovf_whnf(), - Ret::Value(v) => v.into_vovf(), + Ret::ValueF(v) => v, + Ret::Value(v) => v.to_whnf_check_type(ty), Ret::ValueWithRemainingArgs(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(x); } - v.into_vovf() + v.to_whnf_check_type(ty) } - Ret::DoneAsIs => AppliedBuiltin(b, args).into_vovf_whnf(), + Ret::DoneAsIs => AppliedBuiltin(b, args), } } -pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> VoVF { - let fallback = |f: Value, a: Value| { - ValueF::PartialExpr(ExprF::App(f, a)).into_vovf_whnf() - }; - +pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueF { let f_borrow = f.as_whnf(); match &*f_borrow { - ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).into_vovf(), + ValueF::Lam(x, _, e) => { + e.subst_shift(&x.into(), &a).to_whnf_check_type(ty) + } ValueF::AppliedBuiltin(b, args) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); apply_builtin(*b, args, ty) } ValueF::UnionConstructor(l, kts) => { - ValueF::UnionLit(l.clone(), a, kts.clone()).into_vovf_whnf() + ValueF::UnionLit(l.clone(), a, kts.clone()) } _ => { drop(f_borrow); - fallback(f, a) + ValueF::PartialExpr(ExprF::App(f, a)) } } } @@ -609,7 +611,7 @@ fn apply_binop<'a>( pub(crate) fn normalize_one_layer( expr: ExprF, ty: &Value, -) -> VoVF { +) -> ValueF { use ValueF::{ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit, @@ -766,22 +768,22 @@ pub(crate) fn normalize_one_layer( }; match ret { - Ret::ValueF(v) => v.into_vovf_whnf(), - Ret::Value(v) => v.into_vovf(), - Ret::ValueRef(v) => v.clone().into_vovf(), - Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf_whnf(), + Ret::ValueF(v) => v, + Ret::Value(v) => v.to_whnf_check_type(ty), + Ret::ValueRef(v) => v.to_whnf_check_type(ty), + Ret::Expr(expr) => ValueF::PartialExpr(expr), } } /// Normalize a ValueF into WHNF -pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> VoVF { +pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> ValueF { match v { ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty), ValueF::PartialExpr(e) => normalize_one_layer(e, ty), ValueF::TextLit(elts) => { - ValueF::TextLit(squash_textlit(elts.into_iter())).into_vovf_whnf() + ValueF::TextLit(squash_textlit(elts.into_iter())) } // All other cases are already in WHNF - v => v.into_vovf_whnf(), + v => v, } } -- cgit v1.2.3