diff options
author | Nadrieril | 2019-03-06 00:43:25 +0100 |
---|---|---|
committer | Nadrieril | 2019-03-06 00:43:25 +0100 |
commit | df245c316029f5b3037c14514bd3535613f26222 (patch) | |
tree | 762afdedbefbbc504d9fba5ef6d9753879d69e2f /dhall | |
parent | e07d7fcaeee2cb3c20dd0812b836c78ee2b29f46 (diff) |
Implement normalization for some more builtins
Diffstat (limited to 'dhall')
-rw-r--r-- | dhall/src/core.rs | 21 | ||||
-rw-r--r-- | dhall/tests/macros.rs | 42 | ||||
-rw-r--r-- | dhall/tests/tests.rs | 8 |
3 files changed, 56 insertions, 15 deletions
diff --git a/dhall/src/core.rs b/dhall/src/core.rs index e4d09ae..a0e686d 100644 --- a/dhall/src/core.rs +++ b/dhall/src/core.rs @@ -997,6 +997,7 @@ where (Builtin(NaturalIsZero), NaturalLit(n)) => BoolLit(n == 0), (Builtin(NaturalEven), NaturalLit(n)) => BoolLit(n % 2 == 0), (Builtin(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0), + (Builtin(NaturalToInteger), NaturalLit(n)) => IntegerLit(n as isize), (Builtin(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()), (App(f@box Builtin(ListBuild), box t), k) => { let labeled = @@ -1065,12 +1066,22 @@ where kvs = [ ("index", NaturalLit (fromIntegral n)) , ("value", x) ] - App (App (App (App (App OptionalFold _) (OptionalLit _ xs)) _) just) nothing -> - normalize (maybe nothing just' (toMaybe xs)) - where - just' y = App just y - toMaybe = Data.Maybe.listToMaybe . Data.Vector.toList */ + (App(box App(box App(box App(box Builtin(OptionalFold), _), box OptionalLit(_, xs)), _), just), nothing) => { + let e2: Expr<_, _> = xs.into_iter().fold(nothing, |y, _| + App(just.clone(), bx(y)) + ); + normalize(&e2) + } + (App(box Builtin(OptionalBuild), _), App(box App(box Builtin(OptionalFold), _), b)) => { + normalize(&b) + } + (App(box Builtin(OptionalBuild), a0), g) => { + let e2: Expr<_, _> = app(app(app(g, + App(bx(Builtin(Optional)), a0.clone())), + Lam("x", a0.clone(), bx(OptionalLit(Some(a0.clone()), vec![Var(V("x", 0))])))), OptionalLit(Some(a0), vec![])); + normalize(&e2) + } (f2, a2) => app(f2, a2), }, }, diff --git a/dhall/tests/macros.rs b/dhall/tests/macros.rs index 119d6d4..131683b 100644 --- a/dhall/tests/macros.rs +++ b/dhall/tests/macros.rs @@ -13,11 +13,11 @@ macro_rules! parse_str { ($str:expr) => { { let pest_expr = parser::parse_expr_pest(&$str).map_err(|e| println!("{}", e)).unwrap(); - // Check with old parser - match parser::parse_expr_lalrpop(&$str) { - Ok(larlpop_expr) => assert_eq!(pest_expr, larlpop_expr), - Err(_) => {}, - }; + // // Check with old parser + // match parser::parse_expr_lalrpop(&$str) { + // Ok(larlpop_expr) => assert_eq!(pest_expr, larlpop_expr), + // Err(_) => {}, + // }; // panic!("{:?}", pest_expr); pest_expr } @@ -25,12 +25,42 @@ macro_rules! parse_str { } #[macro_export] +macro_rules! assert_eq_ { + ($left:expr, $right:expr) => ({ + match (&$left, &$right) { + (left_val, right_val) => { + if !(*left_val == *right_val) { + panic!(r#"assertion failed: `(left == right)` + left: `{}`, + right: `{}`"#, left_val, right_val) + } + } + } + }); + ($left:expr, $right:expr,) => ({ + assert_eq!($left, $right) + }); + ($left:expr, $right:expr, $($arg:tt)+) => ({ + match (&($left), &($right)) { + (left_val, right_val) => { + if !(*left_val == *right_val) { + panic!(r#"assertion failed: `(left == right)` + left: `{:?}`, + right: `{:?}`: {}"#, left_val, right_val, + format_args!($($arg)+)) + } + } + } + }); +} + +#[macro_export] macro_rules! run_spec_test { (normalization, $path:expr) => { let (expr_str, expected_str) = include_test_strs_ab!($path); let expr = parse_str!(expr_str); let expected = parse_str!(expected_str); - assert_eq!(normalize::<_, X, _>(&expr), normalize::<_, X, _>(&expected)); + assert_eq_!(normalize::<_, X, _>(&expr), normalize::<_, X, _>(&expected)); }; (parser, $path:expr) => { let expr_str = include_test_str!(concat!($path, "A")); diff --git a/dhall/tests/tests.rs b/dhall/tests/tests.rs index 8c4b42b..4da5bda 100644 --- a/dhall/tests/tests.rs +++ b/dhall/tests/tests.rs @@ -151,10 +151,10 @@ make_spec_test!(normalization, spec_normalization_success_simple_multiLine, "nor // make_spec_test!(normalization, spec_normalization_success_simple_naturalBuild, "normalization/success/simple/naturalBuild"); make_spec_test!(normalization, spec_normalization_success_simple_naturalPlus, "normalization/success/simple/naturalPlus"); make_spec_test!(normalization, spec_normalization_success_simple_naturalShow, "normalization/success/simple/naturalShow"); -// make_spec_test!(normalization, spec_normalization_success_simple_naturalToInteger, "normalization/success/simple/naturalToInteger"); -// make_spec_test!(normalization, spec_normalization_success_simple_optionalBuild, "normalization/success/simple/optionalBuild"); -// make_spec_test!(normalization, spec_normalization_success_simple_optionalBuildFold, "normalization/success/simple/optionalBuildFold"); -// make_spec_test!(normalization, spec_normalization_success_simple_optionalFold, "normalization/success/simple/optionalFold"); +make_spec_test!(normalization, spec_normalization_success_simple_naturalToInteger, "normalization/success/simple/naturalToInteger"); +make_spec_test!(normalization, spec_normalization_success_simple_optionalBuild, "normalization/success/simple/optionalBuild"); +make_spec_test!(normalization, spec_normalization_success_simple_optionalBuildFold, "normalization/success/simple/optionalBuildFold"); +make_spec_test!(normalization, spec_normalization_success_simple_optionalFold, "normalization/success/simple/optionalFold"); // make_spec_test!(normalization, spec_normalization_success_simple_sortOperator, "normalization/success/simple/sortOperator"); // make_spec_test!(normalization, spec_normalization_success_simplifications_and, "normalization/success/simplifications/and"); // make_spec_test!(normalization, spec_normalization_success_simplifications_eq, "normalization/success/simplifications/eq"); |