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>) -> 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<Value, Normalized>),
-}
-
-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<Value>, _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<Value>, _ty: &Value) -> VoVF {
let txt: InterpolatedText<Normalized> =
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<Value>, _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<Value>, _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<Value>, _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<Value>, _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<Value>, _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<Value, Normalized>),
+}
+
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