summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-02-27 20:39:29 +0100
committerNadrieril2019-02-27 20:39:29 +0100
commit2c00699d217e0a54d44678529fa3d87936071fec (patch)
treeb01bce29b06c71f50bbc8a2ce8beb127f7ed5bb2
parent8680920be83ecff0aaf6472b78599bb9108272a7 (diff)
Add Natural/Show builtin
-rw-r--r--src/core.rs3
-rw-r--r--src/lexer.rs1
-rw-r--r--tests/tests.rs27
3 files changed, 24 insertions, 7 deletions
diff --git a/src/core.rs b/src/core.rs
index 67a7492..473a6a6 100644
--- a/src/core.rs
+++ b/src/core.rs
@@ -213,6 +213,7 @@ pub enum BuiltinValue {
NaturalEven,
/// `NaturalOdd ~ Natural/odd`
NaturalOdd,
+ NaturalShow,
/// `ListBuild ~ List/build`
ListBuild,
/// `ListFold ~ List/fold`
@@ -478,6 +479,7 @@ impl Display for BuiltinValue {
NaturalFold => "Natural/fold",
NaturalIsZero => "Natural/isZero",
NaturalOdd => "Natural/odd",
+ NaturalShow => "Natural/show",
OptionalFold => "Optional/fold",
})
}
@@ -882,6 +884,7 @@ pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
(BuiltinValue(NaturalIsZero), NaturalLit(n)) => BoolLit(n == 0),
(BuiltinValue(NaturalEven), NaturalLit(n)) => BoolLit(n % 2 == 0),
(BuiltinValue(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0),
+ (BuiltinValue(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()),
(App(f@box BuiltinValue(ListBuild), box t), k) => {
let labeled =
normalize::<_, T, _>(&app(app(app(k.clone(), app(
diff --git a/src/lexer.rs b/src/lexer.rs
index 32e6abe..5b4dcaa 100644
--- a/src/lexer.rs
+++ b/src/lexer.rs
@@ -214,6 +214,7 @@ named!(builtin<&str, Builtin>, alt!(
value!(Builtin::Value(NaturalIsZero), ident_tag!("Natural/isZero")) |
value!(Builtin::Value(NaturalEven), ident_tag!("Natural/even")) |
value!(Builtin::Value(NaturalOdd), ident_tag!("Natural/odd")) |
+ value!(Builtin::Value(NaturalShow), ident_tag!("Natural/show")) |
value!(Builtin::Type(Natural), ident_tag!("Natural")) |
value!(Builtin::Type(Integer), ident_tag!("Integer")) |
value!(Builtin::Type(Double), ident_tag!("Double")) |
diff --git a/tests/tests.rs b/tests/tests.rs
index 5089ae8..d381efc 100644
--- a/tests/tests.rs
+++ b/tests/tests.rs
@@ -1,12 +1,25 @@
use dhall::*;
+macro_rules! include_test_str {
+ ($x:expr) => { include_str!(concat!("../dhall-lang/tests/", $x, ".dhall")) };
+}
+
+macro_rules! include_test_strs_ab {
+ ($x:expr) => { (include_test_str!(concat!($x, "A")), include_test_str!(concat!($x, "B"))) };
+}
+
+macro_rules! test_normalization {
+ ($x:expr) => {
+ let (expr_str, expected_str) = include_test_strs_ab!($x);
+ let expr = parser::parse_expr(&expr_str).unwrap();
+ let expected = parser::parse_expr(&expected_str).unwrap();
+ assert_eq!(normalize::<_, X, _>(&expr), normalize::<_, X, _>(&expected));
+ };
+}
+
+
#[test]
fn test(){
- let buffer_expr = String::from(include_str!("../dhall-lang/tests/normalization/success/simple/naturalPlusA.dhall"));
- let buffer_expected = String::from(include_str!("../dhall-lang/tests/normalization/success/simple/naturalPlusB.dhall"));
- let expr = parser::parse_expr(&buffer_expr).unwrap();
- let expected = parser::parse_expr(&buffer_expected).unwrap();
- // let type_expr = typecheck::type_of(&expr).unwrap();
- // let normalized = normalize::<_, X, _>(&expr);
- assert_eq!(normalize::<_, X, _>(&expr), normalize::<_, X, _>(&expected));
+ test_normalization!("normalization/success/simple/naturalPlus");
+ test_normalization!("normalization/success/simple/naturalShow");
}