Add Natural/equal and Natural/lessThan primitives

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)

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

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"
 

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 =

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 ->

dhall/src/Dhall/Normalize.hs

@@ -235,6 +235,8 @@
                     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 @@
           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,13 +810,18 @@
           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
           App (App NaturalSubtract (NaturalLit _)) (NaturalLit _) -> False
           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 @@
       NaturalOdd -> True
       NaturalShow -> True
       NaturalSubtract -> True
+      NaturalEqual -> True
+      NaturalLessThan -> True
       NaturalToInteger -> True
       NaturalPlus x y -> loop x && loop y && decide x y
         where

dhall/src/Dhall/Parser/Expression.hs

@@ -8,8 +8,8 @@
 -- | Parsing Dhall expressions.
 module Dhall.Parser.Expression where
 
 import Control.Applicative     (Alternative (..), liftA2, optional)
 import Data.Foldable           (foldl')
 import Data.List.NonEmpty      (NonEmpty (..))
 import Data.Text               (Text)
 import Dhall.Src               (Src (..))
@@ -706,6 +706,8 @@
                             , NaturalEven      <$ _NaturalEven
                             , NaturalOdd       <$ _NaturalOdd
                             , NaturalSubtract  <$ _NaturalSubtract
+                            , NaturalEqual     <$ _NaturalEqual
+                            , NaturalLessThan  <$ _NaturalLessThan
                             , NaturalToInteger <$ _NaturalToInteger
                             , NaturalShow      <$ _NaturalShow
                             , Natural          <$ _Natural

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

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 =

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

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"

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
 

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
 -}

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")