From 1ea478858573045e5d3e3f8ccc3773021ea68ffa Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 8 May 2019 17:16:59 +0200 Subject: Implement normalization of missing builtins --- dhall/src/core/value.rs | 9 ++++- dhall/src/phase/normalize.rs | 89 +++++++++++++++++++++++++++++++++----------- 2 files changed, 75 insertions(+), 23 deletions(-) (limited to 'dhall') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 412fe11..72949be 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -3,7 +3,7 @@ use std::collections::BTreeMap; use dhall_proc_macros as dhall; use dhall_syntax::{ rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, - Natural, X, + NaiveDouble, Natural, X, }; use crate::core::thunk::{Thunk, TypeThunk}; @@ -44,6 +44,7 @@ pub(crate) enum Value { BoolLit(bool), NaturalLit(Natural), IntegerLit(Integer), + DoubleLit(NaiveDouble), EmptyOptionalLit(TypeThunk), NEOptionalLit(Thunk), EmptyListLit(TypeThunk), @@ -122,6 +123,7 @@ impl Value { Value::BoolLit(b) => rc(ExprF::BoolLit(*b)), Value::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), Value::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), + Value::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), Value::EmptyOptionalLit(n) => rc(ExprF::App( rc(ExprF::Builtin(Builtin::OptionalNone)), n.normalize_to_expr_maybe_alpha(alpha), @@ -224,7 +226,8 @@ impl Value { | Value::Const(_) | Value::BoolLit(_) | Value::NaturalLit(_) - | Value::IntegerLit(_) => {} + | Value::IntegerLit(_) + | Value::DoubleLit(_) => {} Value::EmptyOptionalLit(tth) | Value::OptionalSomeClosure(tth) @@ -348,6 +351,7 @@ impl Shift for Value { Value::BoolLit(b) => Value::BoolLit(*b), Value::NaturalLit(n) => Value::NaturalLit(*n), Value::IntegerLit(n) => Value::IntegerLit(*n), + Value::DoubleLit(n) => Value::DoubleLit(*n), Value::EmptyOptionalLit(tth) => { Value::EmptyOptionalLit(tth.shift(delta, var)) } @@ -479,6 +483,7 @@ impl Subst for Value { Value::BoolLit(b) => Value::BoolLit(*b), Value::NaturalLit(n) => Value::NaturalLit(*n), Value::IntegerLit(n) => Value::IntegerLit(*n), + Value::DoubleLit(n) => Value::DoubleLit(*n), Value::EmptyOptionalLit(tth) => { Value::EmptyOptionalLit(tth.subst_shift(var, val)) } diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index e9fc570..81abb9c 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -1,6 +1,9 @@ use std::collections::BTreeMap; -use dhall_syntax::{BinOp, Builtin, ExprF, InterpolatedTextContents, Label, X}; +use dhall_syntax::{ + BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label, + NaiveDouble, X, +}; use crate::core::context::NormalizationContext; use crate::core::thunk::{Thunk, TypeThunk}; @@ -43,6 +46,50 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> Value { )), _ => Err(()), }, + (IntegerShow, [n, r..]) => match &*n.as_value() { + IntegerLit(n) => { + let s = if *n < 0 { + n.to_string() + } else { + format!("+{}", n) + }; + Ok((r, TextLit(vec![InterpolatedTextContents::Text(s)]))) + } + _ => Err(()), + }, + (IntegerToDouble, [n, r..]) => match &*n.as_value() { + IntegerLit(n) => Ok((r, DoubleLit(NaiveDouble::from(*n as f64)))), + _ => Err(()), + }, + (DoubleShow, [n, r..]) => match &*n.as_value() { + DoubleLit(n) => Ok(( + r, + TextLit(vec![InterpolatedTextContents::Text(n.to_string())]), + )), + _ => Err(()), + }, + (TextShow, [v, r..]) => match &*v.as_value() { + TextLit(elts) => { + match elts.as_slice() { + // If there are no interpolations (invariants ensure that when there are no + // interpolations, there is a single Text item) in the literal. + [InterpolatedTextContents::Text(s)] => { + // Printing InterpolatedText takes care of all the escaping + let txt: InterpolatedText = std::iter::once( + InterpolatedTextContents::Text(s.clone()), + ) + .collect(); + let s = txt.to_string(); + Ok(( + r, + TextLit(vec![InterpolatedTextContents::Text(s)]), + )) + } + _ => Err(()), + } + } + _ => Err(()), + }, (ListLength, [_, l, r..]) => match &*l.as_value() { EmptyListLit(_) => Ok((r, NaturalLit(0))), NEListLit(xs) => Ok((r, NaturalLit(xs.len()))), @@ -322,9 +369,9 @@ pub(crate) fn normalize_whnf( pub(crate) fn normalize_one_layer(expr: ExprF) -> Value { use Value::{ - BoolLit, EmptyListLit, EmptyOptionalLit, IntegerLit, Lam, NEListLit, - NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType, TextLit, - UnionConstructor, UnionLit, UnionType, + BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit, Lam, + NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType, + TextLit, UnionConstructor, UnionLit, UnionType, }; // Small helper enum to avoid repetition @@ -358,7 +405,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> Value { ExprF::BoolLit(b) => RetValue(BoolLit(b)), ExprF::NaturalLit(n) => RetValue(NaturalLit(n)), ExprF::IntegerLit(n) => RetValue(IntegerLit(n)), - ExprF::DoubleLit(_) => RetExpr(expr), + ExprF::DoubleLit(n) => RetValue(DoubleLit(n)), ExprF::OldOptionalLit(None, t) => { RetValue(EmptyOptionalLit(TypeThunk::from_thunk(t))) } @@ -613,12 +660,12 @@ mod spec_tests { norm!(success_prelude_Bool_or_1, "prelude/Bool/or/1"); norm!(success_prelude_Bool_show_0, "prelude/Bool/show/0"); norm!(success_prelude_Bool_show_1, "prelude/Bool/show/1"); - // norm!(success_prelude_Double_show_0, "prelude/Double/show/0"); - // norm!(success_prelude_Double_show_1, "prelude/Double/show/1"); - // norm!(success_prelude_Integer_show_0, "prelude/Integer/show/0"); - // norm!(success_prelude_Integer_show_1, "prelude/Integer/show/1"); - // norm!(success_prelude_Integer_toDouble_0, "prelude/Integer/toDouble/0"); - // norm!(success_prelude_Integer_toDouble_1, "prelude/Integer/toDouble/1"); + norm!(success_prelude_Double_show_0, "prelude/Double/show/0"); + norm!(success_prelude_Double_show_1, "prelude/Double/show/1"); + norm!(success_prelude_Integer_show_0, "prelude/Integer/show/0"); + norm!(success_prelude_Integer_show_1, "prelude/Integer/show/1"); + norm!(success_prelude_Integer_toDouble_0, "prelude/Integer/toDouble/0"); + norm!(success_prelude_Integer_toDouble_1, "prelude/Integer/toDouble/1"); norm!(success_prelude_List_all_0, "prelude/List/all/0"); norm!(success_prelude_List_all_1, "prelude/List/all/1"); norm!(success_prelude_List_any_0, "prelude/List/any/0"); @@ -677,8 +724,8 @@ mod spec_tests { norm!(success_prelude_Natural_show_1, "prelude/Natural/show/1"); norm!(success_prelude_Natural_sum_0, "prelude/Natural/sum/0"); norm!(success_prelude_Natural_sum_1, "prelude/Natural/sum/1"); - // norm!(success_prelude_Natural_toDouble_0, "prelude/Natural/toDouble/0"); - // norm!(success_prelude_Natural_toDouble_1, "prelude/Natural/toDouble/1"); + norm!(success_prelude_Natural_toDouble_0, "prelude/Natural/toDouble/0"); + norm!(success_prelude_Natural_toDouble_1, "prelude/Natural/toDouble/1"); norm!(success_prelude_Natural_toInteger_0, "prelude/Natural/toInteger/0"); norm!(success_prelude_Natural_toInteger_1, "prelude/Natural/toInteger/1"); norm!(success_prelude_Optional_all_0, "prelude/Optional/all/0"); @@ -722,9 +769,9 @@ mod spec_tests { // norm!(success_prelude_Text_show_1, "prelude/Text/show/1"); // norm!(success_remoteSystems, "remoteSystems"); - // norm!(success_simple_doubleShow, "simple/doubleShow"); + norm!(success_simple_doubleShow, "simple/doubleShow"); norm!(success_simple_enum, "simple/enum"); - // norm!(success_simple_integerShow, "simple/integerShow"); + norm!(success_simple_integerShow, "simple/integerShow"); // norm!(success_simple_integerToDouble, "simple/integerToDouble"); norm!(success_simple_letlet, "simple/letlet"); norm!(success_simple_listBuild, "simple/listBuild"); @@ -747,7 +794,7 @@ mod spec_tests { norm!(success_unit_Double, "unit/Double"); norm!(success_unit_DoubleLiteral, "unit/DoubleLiteral"); norm!(success_unit_DoubleShow, "unit/DoubleShow"); - // norm!(success_unit_DoubleShowValue, "unit/DoubleShowValue"); + norm!(success_unit_DoubleShowValue, "unit/DoubleShowValue"); norm!(success_unit_EmptyAlternative, "unit/EmptyAlternative"); norm!(success_unit_FunctionApplicationCapture, "unit/FunctionApplicationCapture"); norm!(success_unit_FunctionApplicationNoSubstitute, "unit/FunctionApplicationNoSubstitute"); @@ -763,11 +810,11 @@ mod spec_tests { norm!(success_unit_Integer, "unit/Integer"); norm!(success_unit_IntegerNegative, "unit/IntegerNegative"); norm!(success_unit_IntegerPositive, "unit/IntegerPositive"); - // norm!(success_unit_IntegerShow_12, "unit/IntegerShow-12"); - // norm!(success_unit_IntegerShow12, "unit/IntegerShow12"); + norm!(success_unit_IntegerShow_12, "unit/IntegerShow-12"); + norm!(success_unit_IntegerShow12, "unit/IntegerShow12"); norm!(success_unit_IntegerShow, "unit/IntegerShow"); - // norm!(success_unit_IntegerToDouble_12, "unit/IntegerToDouble-12"); - // norm!(success_unit_IntegerToDouble12, "unit/IntegerToDouble12"); + norm!(success_unit_IntegerToDouble_12, "unit/IntegerToDouble-12"); + norm!(success_unit_IntegerToDouble12, "unit/IntegerToDouble12"); norm!(success_unit_IntegerToDouble, "unit/IntegerToDouble"); norm!(success_unit_Kind, "unit/Kind"); norm!(success_unit_Let, "unit/Let"); @@ -900,7 +947,7 @@ mod spec_tests { norm!(success_unit_TextLiteral, "unit/TextLiteral"); norm!(success_unit_TextNormalizeInterpolations, "unit/TextNormalizeInterpolations"); norm!(success_unit_TextShow, "unit/TextShow"); - // norm!(success_unit_TextShowAllEscapes, "unit/TextShowAllEscapes"); + norm!(success_unit_TextShowAllEscapes, "unit/TextShowAllEscapes"); norm!(success_unit_True, "unit/True"); norm!(success_unit_Type, "unit/Type"); norm!(success_unit_TypeAnnotation, "unit/TypeAnnotation"); -- cgit v1.2.3