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/core/value.rs | 32 ++-- dhall/src/phase/normalize.rs | 339 ++++++++++++++++++++----------------------- tests_buffer | 2 + 3 files changed, 173 insertions(+), 200 deletions(-) diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 4a78b05..2554da1 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -116,18 +116,24 @@ impl ValueInternal { } impl Value { - pub(crate) fn new(value: ValueF, form: Form, ty: Option) -> Value { - ValueInternal { form, value, ty }.into_value() - } - // TODO: this is very wrong - pub(crate) fn from_valuef_untyped(v: ValueF) -> Value { - Value::new(v, Unevaled, None) + fn new(value: ValueF, form: Form, ty: Value) -> Value { + ValueInternal { + form, + value, + ty: Some(ty), + } + .into_value() } pub(crate) fn const_sort() -> Value { - Value::new(ValueF::Const(Const::Sort), NF, None) + ValueInternal { + form: NF, + value: ValueF::Const(Const::Sort), + ty: None, + } + .into_value() } pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { - Value::new(v, Unevaled, Some(t)) + Value::new(v, Unevaled, t) } pub(crate) fn from_const(c: Const) -> Self { const_to_value(c) @@ -286,17 +292,9 @@ impl VoVF { ); v } - VoVF::ValueF { val, form } => Value::new(val, form, Some(ty)), + VoVF::ValueF { val, form } => Value::new(val, form, ty), } } - - pub(crate) fn app(self, x: Value) -> VoVF { - VoVF::Value(match self { - VoVF::Value(v) => v.app(x), - // TODO: this is very wrong - VoVF::ValueF { val, .. } => Value::from_valuef_untyped(val).app(x), - }) - } } impl Shift for Value { 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 diff --git a/tests_buffer b/tests_buffer index 93eb626..1ad880e 100644 --- a/tests_buffer +++ b/tests_buffer @@ -28,6 +28,8 @@ variables across import boundaries TextLitNested1 "${""}${x}" TextLitNested2 "${"${x}"}" TextLitNested3 "${"${""}"}${x}" + regression/ + NaturalFoldExtraArg Natural/fold 0 (Bool -> Bool) (λ(_ : (Bool -> Bool)) → λ(_ : Bool) → True) (λ(_ : Bool) → False) True typecheck: something that involves destructuring a recordtype after merge -- cgit v1.2.3