diff --git a/dhall-bash/src/Dhall/Bash.hs b/dhall-bash/src/Dhall/Bash.hs index 756c5532d..5c69977d4 100644 --- a/dhall-bash/src/Dhall/Bash.hs +++ b/dhall-bash/src/Dhall/Bash.hs @@ -303,6 +303,8 @@ dhallToStatement expr0 var0 = go (Dhall.Core.normalize expr0) go e@(NaturalToInteger ) = Left (UnsupportedStatement e) go e@(NaturalShow ) = Left (UnsupportedStatement e) go e@(NaturalSubtract ) = Left (UnsupportedStatement e) + go e@(NaturalEqual ) = Left (UnsupportedStatement e) + go e@(NaturalLessThan ) = Left (UnsupportedStatement e) go e@(NaturalPlus {}) = Left (UnsupportedStatement e) go e@(NaturalTimes {}) = Left (UnsupportedStatement e) go e@(Integer ) = Left (UnsupportedStatement e) diff --git a/dhall-json/src/Dhall/JSON.hs b/dhall-json/src/Dhall/JSON.hs index 563326fc9..cec063eb5 100644 --- a/dhall-json/src/Dhall/JSON.hs +++ b/dhall-json/src/Dhall/JSON.hs @@ -832,6 +832,12 @@ convertToHomogeneousMaps (Conversion {..}) e0 = loop (Core.normalize e0) Core.NaturalSubtract -> Core.NaturalSubtract + Core.NaturalEqual -> + Core.NaturalEqual + + Core.NaturalLessThan -> + Core.NaturalLessThan + Core.NaturalPlus a b -> Core.NaturalPlus a' b' where diff --git a/dhall/src/Dhall/Binary.hs b/dhall/src/Dhall/Binary.hs index ebe05cddc..39dba1868 100644 --- a/dhall/src/Dhall/Binary.hs +++ b/dhall/src/Dhall/Binary.hs @@ -169,10 +169,12 @@ decodeExpressionInternal decodeEmbed = go | sb == "Text/replace" -> return TextReplace 13 | sb == "Integer/clamp" -> return IntegerClamp | sb == "Natural/build" -> return NaturalBuild + | sb == "Natural/equal" -> return NaturalEqual | sb == "TimeZone/show" -> return TimeZoneShow 14 | sb == "Integer/negate" -> return IntegerNegate | sb == "Natural/isZero" -> return NaturalIsZero 16 | sb == "Integer/toDouble" -> return IntegerToDouble + | sb == "Natural/lessThan" -> return NaturalLessThan | sb == "Natural/subtract" -> return NaturalSubtract 17 | sb == "Natural/toInteger" -> return NaturalToInteger _ -> die ("Unrecognized built-in: " <> show sb) @@ -708,6 +710,12 @@ encodeExpressionInternal encodeEmbed = go NaturalSubtract -> Encoding.encodeUtf8ByteArray "Natural/subtract" + NaturalEqual -> + Encoding.encodeUtf8ByteArray "Natural/equal" + + NaturalLessThan -> + Encoding.encodeUtf8ByteArray "Natural/lessThan" + IntegerToDouble -> Encoding.encodeUtf8ByteArray "Integer/toDouble" diff --git a/dhall/src/Dhall/Diff.hs b/dhall/src/Dhall/Diff.hs index 46f332b78..c265f1f18 100644 --- a/dhall/src/Dhall/Diff.hs +++ b/dhall/src/Dhall/Diff.hs @@ -1244,6 +1244,18 @@ diffPrimitiveExpression l@NaturalSubtract r = mismatch l r diffPrimitiveExpression l r@NaturalSubtract = mismatch l r +diffPrimitiveExpression NaturalEqual NaturalEqual = + "…" +diffPrimitiveExpression l@NaturalEqual r = + mismatch l r +diffPrimitiveExpression l r@NaturalEqual = + mismatch l r +diffPrimitiveExpression NaturalLessThan NaturalLessThan = + "…" +diffPrimitiveExpression l@NaturalLessThan r = + mismatch l r +diffPrimitiveExpression l r@NaturalLessThan = + mismatch l r diffPrimitiveExpression Integer Integer = "…" diffPrimitiveExpression l@Integer r = diff --git a/dhall/src/Dhall/Eval.hs b/dhall/src/Dhall/Eval.hs index 73ba65b7a..82f4b4a45 100644 --- a/dhall/src/Dhall/Eval.hs +++ b/dhall/src/Dhall/Eval.hs @@ -188,6 +188,8 @@ data Val a | VNaturalToInteger !(Val a) | VNaturalShow !(Val a) | VNaturalSubtract !(Val a) !(Val a) + | VNaturalEqual !(Val a) !(Val a) + | VNaturalLessThan !(Val a) !(Val a) | VNaturalPlus !(Val a) !(Val a) | VNaturalTimes !(Val a) !(Val a) @@ -577,6 +579,22 @@ eval !env t0 = VNaturalLit 0 -> VNaturalLit 0 y | conv env x y -> VNaturalLit 0 y -> VNaturalSubtract x y + NaturalEqual -> VPrim $ \case + VNaturalLit x -> VPrim $ \case + VNaturalLit y -> VBoolLit (x == y) + y -> VNaturalEqual (VNaturalLit x) y + x -> VPrim $ \case + VNaturalLit y -> VNaturalEqual x (VNaturalLit y) + y | conv env x y -> VBoolLit True + y -> VNaturalEqual x y + NaturalLessThan -> VPrim $ \case + VNaturalLit x -> VPrim $ \case + VNaturalLit y -> VBoolLit (x < y) + y -> VNaturalLessThan (VNaturalLit x) y + x -> VPrim $ \case + VNaturalLit y -> VNaturalLessThan x (VNaturalLit y) + y | conv env x y -> VBoolLit False + y -> VNaturalLessThan x y NaturalPlus t u -> vNaturalPlus (eval env t) (eval env u) NaturalTimes t u -> @@ -1017,6 +1035,10 @@ conv !env t0 t0' = conv env t t' (VNaturalSubtract x y, VNaturalSubtract x' y') -> conv env x x' && conv env y y' + (VNaturalEqual x y, VNaturalEqual x' y') -> + conv env x x' && conv env y y' + (VNaturalLessThan x y, VNaturalLessThan x' y') -> + conv env x x' && conv env y y' (VNaturalPlus t u, VNaturalPlus t' u') -> conv env t t' && conv env u u' (VNaturalTimes t u, VNaturalTimes t' u') -> @@ -1241,6 +1263,10 @@ quote !env !t0 = NaturalPlus (quote env t) (quote env u) VNaturalTimes t u -> NaturalTimes (quote env t) (quote env u) + VNaturalEqual x y -> + NaturalEqual `qApp` x `qApp` y + VNaturalLessThan x y -> + NaturalLessThan `qApp` x `qApp` y VNaturalSubtract x y -> NaturalSubtract `qApp` x `qApp` y VInteger -> @@ -1448,6 +1474,10 @@ alphaNormalize = goEnv EmptyNames NaturalShow NaturalSubtract -> NaturalSubtract + NaturalEqual -> + NaturalEqual + NaturalLessThan -> + NaturalLessThan NaturalPlus t u -> NaturalPlus (go t) (go u) NaturalTimes t u -> diff --git a/dhall/src/Dhall/Normalize.hs b/dhall/src/Dhall/Normalize.hs index c51377dfd..208890a83 100644 --- a/dhall/src/Dhall/Normalize.hs +++ b/dhall/src/Dhall/Normalize.hs @@ -235,6 +235,8 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0) App NaturalToInteger (NaturalLit n) -> pure (IntegerLit (toInteger n)) App NaturalShow (NaturalLit n) -> pure (TextLit (Chunks [] (Text.pack (show n)))) + App (App NaturalEqual (NaturalLit x)) (NaturalLit y) -> pure (BoolLit (x == y)) + App (App NaturalLessThan (NaturalLit x)) (NaturalLit y) -> pure (BoolLit (x < y)) App (App NaturalSubtract (NaturalLit x)) (NaturalLit y) -- Use an `Integer` for the subtraction, due to the -- following issue: @@ -460,6 +462,8 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0) NaturalToInteger -> pure NaturalToInteger NaturalShow -> pure NaturalShow NaturalSubtract -> pure NaturalSubtract + NaturalEqual -> pure NaturalEqual + NaturalLessThan -> pure NaturalLessThan NaturalPlus x y -> decide <$> loop x <*> loop y where decide (NaturalLit 0) r = r @@ -806,6 +810,8 @@ isNormalized e0 = loop (Syntax.denote e0) App NaturalEven (NaturalLit _) -> False App NaturalOdd (NaturalLit _) -> False App NaturalShow (NaturalLit _) -> False + App (App NaturalEqual (NaturalLit _)) (NaturalLit _) -> False + App (App NaturalLessThan (NaturalLit _)) (NaturalLit _) -> False App DateShow (DateLiteral _) -> False App TimeShow (TimeLiteral _ _) -> False App TimeZoneShow (TimeZoneLiteral _) -> False @@ -813,6 +819,9 @@ isNormalized e0 = loop (Syntax.denote e0) App (App NaturalSubtract (NaturalLit 0)) _ -> False App (App NaturalSubtract _) (NaturalLit 0) -> False App (App NaturalSubtract x) y -> not (Eval.judgmentallyEqual x y) + App (App NaturalEqual (NaturalLit _)) (NaturalLit _) -> False + App (App NaturalEqual x) y -> not (Eval.judgmentallyEqual x y) + App (App NaturalLessThan x) y -> not (Eval.judgmentallyEqual x y) App NaturalToInteger (NaturalLit _) -> False App IntegerNegate (IntegerLit _) -> False App IntegerClamp (IntegerLit _) -> False @@ -874,6 +883,8 @@ isNormalized e0 = loop (Syntax.denote e0) NaturalOdd -> True NaturalShow -> True NaturalSubtract -> True + NaturalEqual -> True + NaturalLessThan -> True NaturalToInteger -> True NaturalPlus x y -> loop x && loop y && decide x y where diff --git a/dhall/src/Dhall/Parser/Expression.hs b/dhall/src/Dhall/Parser/Expression.hs index 0f75be90a..d57b9e41a 100644 --- a/dhall/src/Dhall/Parser/Expression.hs +++ b/dhall/src/Dhall/Parser/Expression.hs @@ -706,6 +706,8 @@ parsers embedded = Parsers{..} , NaturalEven <$ _NaturalEven , NaturalOdd <$ _NaturalOdd , NaturalSubtract <$ _NaturalSubtract + , NaturalEqual <$ _NaturalEqual + , NaturalLessThan <$ _NaturalLessThan , NaturalToInteger <$ _NaturalToInteger , NaturalShow <$ _NaturalShow , Natural <$ _Natural diff --git a/dhall/src/Dhall/Parser/Token.hs b/dhall/src/Dhall/Parser/Token.hs index 84167e41b..0c4d44d67 100644 --- a/dhall/src/Dhall/Parser/Token.hs +++ b/dhall/src/Dhall/Parser/Token.hs @@ -59,6 +59,8 @@ module Dhall.Parser.Token ( _NaturalToInteger, _NaturalShow, _NaturalSubtract, + _NaturalEqual, + _NaturalLessThan, _IntegerClamp, _IntegerNegate, _IntegerShow, @@ -1048,6 +1050,20 @@ _NaturalShow = builtin "Natural/show" _NaturalSubtract :: Parser () _NaturalSubtract = builtin "Natural/subtract" +{-| Parse the @Natural/lessThan@ built-in + + This corresponds to the @Natural-lessThan@ rule from the official grammar +-} +_NaturalLessThan :: Parser () +_NaturalLessThan = builtin "Natural/lessThan" + +{-| Parse the @Natural/equal@ built-in + + This corresponds to the @Natural-equal@ rule from the official grammar +-} +_NaturalEqual :: Parser () +_NaturalEqual = builtin "Natural/equal" + {-| Parse the @Integer/clamp@ built-in This corresponds to the @Integer-clamp@ rule from the official grammar diff --git a/dhall/src/Dhall/Pretty/Internal.hs b/dhall/src/Dhall/Pretty/Internal.hs index fdd545d3c..85387c473 100644 --- a/dhall/src/Dhall/Pretty/Internal.hs +++ b/dhall/src/Dhall/Pretty/Internal.hs @@ -1336,6 +1336,10 @@ prettyPrinters characterSet = builtin "Natural/show" prettyPrimitiveExpression NaturalSubtract = builtin "Natural/subtract" + prettyPrimitiveExpression NaturalEqual = + builtin "Natural/equal" + prettyPrimitiveExpression NaturalLessThan = + builtin "Natural/lessThan" prettyPrimitiveExpression Integer = builtin "Integer" prettyPrimitiveExpression IntegerClamp = diff --git a/dhall/src/Dhall/Syntax/Expr.hs b/dhall/src/Dhall/Syntax/Expr.hs index 660e1ba05..40bb6254c 100644 --- a/dhall/src/Dhall/Syntax/Expr.hs +++ b/dhall/src/Dhall/Syntax/Expr.hs @@ -114,6 +114,10 @@ data Expr s a | NaturalShow -- | > NaturalSubtract ~ Natural/subtract | NaturalSubtract + -- | > NaturalEqual ~ Natural/equal + | NaturalEqual + -- | > NaturalLessThan ~ Natural/lessThan + | NaturalLessThan -- | > NaturalPlus x y ~ x + y | NaturalPlus (Expr s a) (Expr s a) -- | > NaturalTimes x y ~ x * y diff --git a/dhall/src/Dhall/Syntax/Operations.hs b/dhall/src/Dhall/Syntax/Operations.hs index 8d68c37b6..17e16d56e 100644 --- a/dhall/src/Dhall/Syntax/Operations.hs +++ b/dhall/src/Dhall/Syntax/Operations.hs @@ -95,6 +95,8 @@ unsafeSubExpressions _ NaturalOdd = pure NaturalOdd unsafeSubExpressions _ NaturalToInteger = pure NaturalToInteger unsafeSubExpressions _ NaturalShow = pure NaturalShow unsafeSubExpressions _ NaturalSubtract = pure NaturalSubtract +unsafeSubExpressions _ NaturalEqual = pure NaturalEqual +unsafeSubExpressions _ NaturalLessThan = pure NaturalLessThan unsafeSubExpressions f (NaturalPlus a b) = NaturalPlus <$> f a <*> f b unsafeSubExpressions f (NaturalTimes a b) = NaturalTimes <$> f a <*> f b unsafeSubExpressions _ Integer = pure Integer @@ -242,6 +244,8 @@ reservedIdentifiers = reservedKeywords <> , "Natural/toInteger" , "Natural/show" , "Natural/subtract" + , "Natural/equal" + , "Natural/lessThan" , "Integer" , "Integer/clamp" , "Integer/negate" diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 68829e4e3..ef2fc60b7 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -482,6 +482,12 @@ infer typer = loop NaturalSubtract -> return (VNatural ~> VNatural ~> VNatural) + NaturalEqual -> + return (VNatural ~> VNatural ~> VBool) + + NaturalLessThan -> + return (VNatural ~> VNatural ~> VBool) + NaturalPlus l r -> do tl' <- loop ctx l diff --git a/dhall/tests/Dhall/Test/Normalization.hs b/dhall/tests/Dhall/Test/Normalization.hs index 32b9b16f2..3b2d2b6d6 100644 --- a/dhall/tests/Dhall/Test/Normalization.hs +++ b/dhall/tests/Dhall/Test/Normalization.hs @@ -69,6 +69,8 @@ customization = Tasty.testGroup "customization" [ simpleCustomization , nestedReduction + , naturalEqualTest + , naturalLessThanTest ] simpleCustomization :: TestTree @@ -141,6 +143,79 @@ alphaNormalizationTest prefix = do Tasty.HUnit.assertEqual message expectedNormalized actualNormalized +naturalEqualTest :: TestTree +naturalEqualTest = Tasty.HUnit.testCase "Natural/equal" $ do + let tyCtx = + Context.insert + "Natural/equal" + (Pi mempty "_" Natural (Pi mempty "_" Natural Bool)) + Context.empty + + valCtx e = + case e of + App (App (Var (V "Natural/equal" 0)) (NaturalLit x)) (NaturalLit y) -> + pure (Just (BoolLit (x == y))) + _ -> + pure Nothing + + -- Test equal numbers + e1 <- Test.Util.codeWith tyCtx "Natural/equal 5 5" + Test.Util.assertNormalizesToWith valCtx e1 "True" + + -- Test unequal numbers + e2 <- Test.Util.codeWith tyCtx "Natural/equal 5 7" + Test.Util.assertNormalizesToWith valCtx e2 "False" + + -- Test with zero + e3 <- Test.Util.codeWith tyCtx "Natural/equal 0 0" + Test.Util.assertNormalizesToWith valCtx e3 "True" + + -- Test with larger numbers + e4 <- Test.Util.codeWith tyCtx "Natural/equal 42 42" + Test.Util.assertNormalizesToWith valCtx e4 "True" + + -- Test partial application (should not reduce) + e5 <- Test.Util.codeWith tyCtx "Natural/equal 3" + Test.Util.assertNormalizesToWith valCtx e5 "Natural/equal 3" + +naturalLessThanTest :: TestTree +naturalLessThanTest = Tasty.HUnit.testCase "Natural/lessThan" $ do + let tyCtx = + Context.insert + "Natural/lessThan" + (Pi mempty "_" Natural (Pi mempty "_" Natural Bool)) + Context.empty + + valCtx e = + case e of + App (App (Var (V "Natural/lessThan" 0)) (NaturalLit x)) (NaturalLit y) -> + pure (Just (BoolLit (x < y))) + _ -> + pure Nothing + + -- Test less than + e1 <- Test.Util.codeWith tyCtx "Natural/lessThan 5 7" + Test.Util.assertNormalizesToWith valCtx e1 "True" + + -- Test not less than + e2 <- Test.Util.codeWith tyCtx "Natural/lessThan 7 5" + Test.Util.assertNormalizesToWith valCtx e2 "False" + + -- Test equal numbers + e3 <- Test.Util.codeWith tyCtx "Natural/lessThan 5 5" + Test.Util.assertNormalizesToWith valCtx e3 "False" + + -- Test with zero + e4 <- Test.Util.codeWith tyCtx "Natural/lessThan 0 1" + Test.Util.assertNormalizesToWith valCtx e4 "True" + + e5 <- Test.Util.codeWith tyCtx "Natural/lessThan 1 0" + Test.Util.assertNormalizesToWith valCtx e5 "False" + + -- Test partial application (should not reduce) + e6 <- Test.Util.codeWith tyCtx "Natural/lessThan 3" + Test.Util.assertNormalizesToWith valCtx e6 "Natural/lessThan 3" + {- Unit tests don't type-check, so we only verify that they normalize to the expected output -} diff --git a/dhall/tests/Dhall/Test/QuickCheck.hs b/dhall/tests/Dhall/Test/QuickCheck.hs index b73156be3..ba4433d71 100644 --- a/dhall/tests/Dhall/Test/QuickCheck.hs +++ b/dhall/tests/Dhall/Test/QuickCheck.hs @@ -370,6 +370,8 @@ instance (Arbitrary s, Arbitrary a) => Arbitrary (Expr s a) where % (1 :: W "NaturalToInteger") % (1 :: W "NaturalShow") % (1 :: W "NaturalSubtract") + % (1 :: W "NaturalEqual") + % (1 :: W "NaturalLessThan") % (1 :: W "NaturalPlus") % (1 :: W "NaturalTimes") % (1 :: W "Integer")