From b05418463ddf47780b0b0c3258ff9574c50196da Mon Sep 17 00:00:00 2001 From: Nikita Volkov Date: Fri, 1 May 2026 14:13:13 +0300 Subject: [PATCH 1/2] Add Natural/equal primitive --- dhall-bash/src/Dhall/Bash.hs | 1 + dhall-json/src/Dhall/JSON.hs | 3 +++ dhall/src/Dhall/Binary.hs | 4 +++ dhall/src/Dhall/Diff.hs | 6 +++++ dhall/src/Dhall/Eval.hs | 15 +++++++++++ dhall/src/Dhall/Normalize.hs | 6 +++++ dhall/src/Dhall/Parser/Expression.hs | 1 + dhall/src/Dhall/Parser/Token.hs | 8 ++++++ dhall/src/Dhall/Pretty/Internal.hs | 2 ++ dhall/src/Dhall/Syntax/Expr.hs | 2 ++ dhall/src/Dhall/Syntax/Operations.hs | 2 ++ dhall/src/Dhall/TypeCheck.hs | 3 +++ dhall/tests/Dhall/Test/Normalization.hs | 36 +++++++++++++++++++++++++ dhall/tests/Dhall/Test/QuickCheck.hs | 1 + 14 files changed, 90 insertions(+) diff --git a/dhall-bash/src/Dhall/Bash.hs b/dhall-bash/src/Dhall/Bash.hs index 756c5532d..c0af246f7 100644 --- a/dhall-bash/src/Dhall/Bash.hs +++ b/dhall-bash/src/Dhall/Bash.hs @@ -303,6 +303,7 @@ 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@(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..5ca3307a5 100644 --- a/dhall-json/src/Dhall/JSON.hs +++ b/dhall-json/src/Dhall/JSON.hs @@ -832,6 +832,9 @@ convertToHomogeneousMaps (Conversion {..}) e0 = loop (Core.normalize e0) Core.NaturalSubtract -> Core.NaturalSubtract + Core.NaturalEqual -> + Core.NaturalEqual + 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..be63008b2 100644 --- a/dhall/src/Dhall/Binary.hs +++ b/dhall/src/Dhall/Binary.hs @@ -169,6 +169,7 @@ 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 @@ -708,6 +709,9 @@ encodeExpressionInternal encodeEmbed = go NaturalSubtract -> Encoding.encodeUtf8ByteArray "Natural/subtract" + NaturalEqual -> + Encoding.encodeUtf8ByteArray "Natural/equal" + IntegerToDouble -> Encoding.encodeUtf8ByteArray "Integer/toDouble" diff --git a/dhall/src/Dhall/Diff.hs b/dhall/src/Dhall/Diff.hs index 46f332b78..a5b31d5bb 100644 --- a/dhall/src/Dhall/Diff.hs +++ b/dhall/src/Dhall/Diff.hs @@ -1244,6 +1244,12 @@ 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 Integer Integer = "…" diffPrimitiveExpression l@Integer r = diff --git a/dhall/src/Dhall/Eval.hs b/dhall/src/Dhall/Eval.hs index 73ba65b7a..a70bf83bc 100644 --- a/dhall/src/Dhall/Eval.hs +++ b/dhall/src/Dhall/Eval.hs @@ -188,6 +188,7 @@ data Val a | VNaturalToInteger !(Val a) | VNaturalShow !(Val a) | VNaturalSubtract !(Val a) !(Val a) + | VNaturalEqual !(Val a) !(Val a) | VNaturalPlus !(Val a) !(Val a) | VNaturalTimes !(Val a) !(Val a) @@ -577,6 +578,14 @@ 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 NaturalPlus t u -> vNaturalPlus (eval env t) (eval env u) NaturalTimes t u -> @@ -1017,6 +1026,8 @@ 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' (VNaturalPlus t u, VNaturalPlus t' u') -> conv env t t' && conv env u u' (VNaturalTimes t u, VNaturalTimes t' u') -> @@ -1241,6 +1252,8 @@ 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 VNaturalSubtract x y -> NaturalSubtract `qApp` x `qApp` y VInteger -> @@ -1448,6 +1461,8 @@ alphaNormalize = goEnv EmptyNames NaturalShow NaturalSubtract -> NaturalSubtract + NaturalEqual -> + NaturalEqual 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..ca6dc3712 100644 --- a/dhall/src/Dhall/Normalize.hs +++ b/dhall/src/Dhall/Normalize.hs @@ -235,6 +235,7 @@ 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 NaturalSubtract (NaturalLit x)) (NaturalLit y) -- Use an `Integer` for the subtraction, due to the -- following issue: @@ -460,6 +461,7 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0) NaturalToInteger -> pure NaturalToInteger NaturalShow -> pure NaturalShow NaturalSubtract -> pure NaturalSubtract + NaturalEqual -> pure NaturalEqual NaturalPlus x y -> decide <$> loop x <*> loop y where decide (NaturalLit 0) r = r @@ -806,6 +808,7 @@ 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 DateShow (DateLiteral _) -> False App TimeShow (TimeLiteral _ _) -> False App TimeZoneShow (TimeZoneLiteral _) -> False @@ -813,6 +816,8 @@ 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 NaturalToInteger (NaturalLit _) -> False App IntegerNegate (IntegerLit _) -> False App IntegerClamp (IntegerLit _) -> False @@ -874,6 +879,7 @@ isNormalized e0 = loop (Syntax.denote e0) NaturalOdd -> True NaturalShow -> True NaturalSubtract -> True + NaturalEqual -> 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..d496023fa 100644 --- a/dhall/src/Dhall/Parser/Expression.hs +++ b/dhall/src/Dhall/Parser/Expression.hs @@ -706,6 +706,7 @@ parsers embedded = Parsers{..} , NaturalEven <$ _NaturalEven , NaturalOdd <$ _NaturalOdd , NaturalSubtract <$ _NaturalSubtract + , NaturalEqual <$ _NaturalEqual , NaturalToInteger <$ _NaturalToInteger , NaturalShow <$ _NaturalShow , Natural <$ _Natural diff --git a/dhall/src/Dhall/Parser/Token.hs b/dhall/src/Dhall/Parser/Token.hs index 84167e41b..8aebfab66 100644 --- a/dhall/src/Dhall/Parser/Token.hs +++ b/dhall/src/Dhall/Parser/Token.hs @@ -59,6 +59,7 @@ module Dhall.Parser.Token ( _NaturalToInteger, _NaturalShow, _NaturalSubtract, + _NaturalEqual, _IntegerClamp, _IntegerNegate, _IntegerShow, @@ -1048,6 +1049,13 @@ _NaturalShow = builtin "Natural/show" _NaturalSubtract :: Parser () _NaturalSubtract = builtin "Natural/subtract" +{-| 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..952cf7461 100644 --- a/dhall/src/Dhall/Pretty/Internal.hs +++ b/dhall/src/Dhall/Pretty/Internal.hs @@ -1336,6 +1336,8 @@ prettyPrinters characterSet = builtin "Natural/show" prettyPrimitiveExpression NaturalSubtract = builtin "Natural/subtract" + prettyPrimitiveExpression NaturalEqual = + builtin "Natural/equal" prettyPrimitiveExpression Integer = builtin "Integer" prettyPrimitiveExpression IntegerClamp = diff --git a/dhall/src/Dhall/Syntax/Expr.hs b/dhall/src/Dhall/Syntax/Expr.hs index 660e1ba05..aa9ff73bb 100644 --- a/dhall/src/Dhall/Syntax/Expr.hs +++ b/dhall/src/Dhall/Syntax/Expr.hs @@ -114,6 +114,8 @@ data Expr s a | NaturalShow -- | > NaturalSubtract ~ Natural/subtract | NaturalSubtract + -- | > NaturalEqual ~ Natural/equal + | NaturalEqual -- | > 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..c23daa097 100644 --- a/dhall/src/Dhall/Syntax/Operations.hs +++ b/dhall/src/Dhall/Syntax/Operations.hs @@ -95,6 +95,7 @@ unsafeSubExpressions _ NaturalOdd = pure NaturalOdd unsafeSubExpressions _ NaturalToInteger = pure NaturalToInteger unsafeSubExpressions _ NaturalShow = pure NaturalShow unsafeSubExpressions _ NaturalSubtract = pure NaturalSubtract +unsafeSubExpressions _ NaturalEqual = pure NaturalEqual 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 +243,7 @@ reservedIdentifiers = reservedKeywords <> , "Natural/toInteger" , "Natural/show" , "Natural/subtract" + , "Natural/equal" , "Integer" , "Integer/clamp" , "Integer/negate" diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 68829e4e3..635d2162b 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -482,6 +482,9 @@ infer typer = loop NaturalSubtract -> return (VNatural ~> VNatural ~> VNatural) + NaturalEqual -> + 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..2cd3b4b43 100644 --- a/dhall/tests/Dhall/Test/Normalization.hs +++ b/dhall/tests/Dhall/Test/Normalization.hs @@ -69,6 +69,7 @@ customization = Tasty.testGroup "customization" [ simpleCustomization , nestedReduction + , naturalEqualTest ] simpleCustomization :: TestTree @@ -141,6 +142,41 @@ 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" + {- 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..1b8d51072 100644 --- a/dhall/tests/Dhall/Test/QuickCheck.hs +++ b/dhall/tests/Dhall/Test/QuickCheck.hs @@ -370,6 +370,7 @@ instance (Arbitrary s, Arbitrary a) => Arbitrary (Expr s a) where % (1 :: W "NaturalToInteger") % (1 :: W "NaturalShow") % (1 :: W "NaturalSubtract") + % (1 :: W "NaturalEqual") % (1 :: W "NaturalPlus") % (1 :: W "NaturalTimes") % (1 :: W "Integer") From d63f2b1faab78f2b16974be9108ba537f48bff40 Mon Sep 17 00:00:00 2001 From: Nikita Volkov Date: Sat, 2 May 2026 00:08:13 +0300 Subject: [PATCH 2/2] Implement Natural/lessThan --- dhall-bash/src/Dhall/Bash.hs | 1 + dhall-json/src/Dhall/JSON.hs | 3 ++ dhall/src/Dhall/Binary.hs | 4 +++ dhall/src/Dhall/Diff.hs | 6 ++++ dhall/src/Dhall/Eval.hs | 15 ++++++++++ dhall/src/Dhall/Normalize.hs | 5 ++++ dhall/src/Dhall/Parser/Expression.hs | 1 + dhall/src/Dhall/Parser/Token.hs | 8 +++++ dhall/src/Dhall/Pretty/Internal.hs | 2 ++ dhall/src/Dhall/Syntax/Expr.hs | 2 ++ dhall/src/Dhall/Syntax/Operations.hs | 2 ++ dhall/src/Dhall/TypeCheck.hs | 3 ++ dhall/tests/Dhall/Test/Normalization.hs | 39 +++++++++++++++++++++++++ dhall/tests/Dhall/Test/QuickCheck.hs | 1 + 14 files changed, 92 insertions(+) diff --git a/dhall-bash/src/Dhall/Bash.hs b/dhall-bash/src/Dhall/Bash.hs index c0af246f7..5c69977d4 100644 --- a/dhall-bash/src/Dhall/Bash.hs +++ b/dhall-bash/src/Dhall/Bash.hs @@ -304,6 +304,7 @@ dhallToStatement expr0 var0 = go (Dhall.Core.normalize expr0) 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 5ca3307a5..cec063eb5 100644 --- a/dhall-json/src/Dhall/JSON.hs +++ b/dhall-json/src/Dhall/JSON.hs @@ -835,6 +835,9 @@ convertToHomogeneousMaps (Conversion {..}) e0 = loop (Core.normalize e0) 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 be63008b2..39dba1868 100644 --- a/dhall/src/Dhall/Binary.hs +++ b/dhall/src/Dhall/Binary.hs @@ -174,6 +174,7 @@ decodeExpressionInternal decodeEmbed = go 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) @@ -712,6 +713,9 @@ encodeExpressionInternal encodeEmbed = go 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 a5b31d5bb..c265f1f18 100644 --- a/dhall/src/Dhall/Diff.hs +++ b/dhall/src/Dhall/Diff.hs @@ -1250,6 +1250,12 @@ 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 a70bf83bc..82f4b4a45 100644 --- a/dhall/src/Dhall/Eval.hs +++ b/dhall/src/Dhall/Eval.hs @@ -189,6 +189,7 @@ data 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) @@ -586,6 +587,14 @@ eval !env t0 = 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 -> @@ -1028,6 +1037,8 @@ conv !env t0 t0' = 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') -> @@ -1254,6 +1265,8 @@ quote !env !t0 = 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 -> @@ -1463,6 +1476,8 @@ alphaNormalize = goEnv EmptyNames 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 ca6dc3712..208890a83 100644 --- a/dhall/src/Dhall/Normalize.hs +++ b/dhall/src/Dhall/Normalize.hs @@ -236,6 +236,7 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0) 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: @@ -462,6 +463,7 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0) 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 @@ -809,6 +811,7 @@ isNormalized e0 = loop (Syntax.denote e0) 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 @@ -818,6 +821,7 @@ isNormalized e0 = loop (Syntax.denote e0) 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 @@ -880,6 +884,7 @@ isNormalized e0 = loop (Syntax.denote e0) 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 d496023fa..d57b9e41a 100644 --- a/dhall/src/Dhall/Parser/Expression.hs +++ b/dhall/src/Dhall/Parser/Expression.hs @@ -707,6 +707,7 @@ parsers embedded = Parsers{..} , 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 8aebfab66..0c4d44d67 100644 --- a/dhall/src/Dhall/Parser/Token.hs +++ b/dhall/src/Dhall/Parser/Token.hs @@ -60,6 +60,7 @@ module Dhall.Parser.Token ( _NaturalShow, _NaturalSubtract, _NaturalEqual, + _NaturalLessThan, _IntegerClamp, _IntegerNegate, _IntegerShow, @@ -1049,6 +1050,13 @@ _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 diff --git a/dhall/src/Dhall/Pretty/Internal.hs b/dhall/src/Dhall/Pretty/Internal.hs index 952cf7461..85387c473 100644 --- a/dhall/src/Dhall/Pretty/Internal.hs +++ b/dhall/src/Dhall/Pretty/Internal.hs @@ -1338,6 +1338,8 @@ prettyPrinters characterSet = 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 aa9ff73bb..40bb6254c 100644 --- a/dhall/src/Dhall/Syntax/Expr.hs +++ b/dhall/src/Dhall/Syntax/Expr.hs @@ -116,6 +116,8 @@ data Expr s a | 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 c23daa097..17e16d56e 100644 --- a/dhall/src/Dhall/Syntax/Operations.hs +++ b/dhall/src/Dhall/Syntax/Operations.hs @@ -96,6 +96,7 @@ 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 @@ -244,6 +245,7 @@ reservedIdentifiers = reservedKeywords <> , "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 635d2162b..ef2fc60b7 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -485,6 +485,9 @@ infer typer = loop 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 2cd3b4b43..3b2d2b6d6 100644 --- a/dhall/tests/Dhall/Test/Normalization.hs +++ b/dhall/tests/Dhall/Test/Normalization.hs @@ -70,6 +70,7 @@ customization = [ simpleCustomization , nestedReduction , naturalEqualTest + , naturalLessThanTest ] simpleCustomization :: TestTree @@ -177,6 +178,44 @@ naturalEqualTest = Tasty.HUnit.testCase "Natural/equal" $ do 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 1b8d51072..ba4433d71 100644 --- a/dhall/tests/Dhall/Test/QuickCheck.hs +++ b/dhall/tests/Dhall/Test/QuickCheck.hs @@ -371,6 +371,7 @@ instance (Arbitrary s, Arbitrary a) => Arbitrary (Expr s a) where % (1 :: W "NaturalShow") % (1 :: W "NaturalSubtract") % (1 :: W "NaturalEqual") + % (1 :: W "NaturalLessThan") % (1 :: W "NaturalPlus") % (1 :: W "NaturalTimes") % (1 :: W "Integer")