diff --git a/dhall-bash/src/Dhall/Bash.hs b/dhall-bash/src/Dhall/Bash.hs index a87a995..2add515 100644 --- a/dhall-bash/src/Dhall/Bash.hs +++ b/dhall-bash/src/Dhall/Bash.hs @@ -296,6 +296,7 @@ dhallToStatement expr0 var0 = go (Dhall.Core.normalize expr0) go e@(NaturalOdd ) = Left (UnsupportedStatement e) go e@(NaturalToInteger) = Left (UnsupportedStatement e) go e@(NaturalShow ) = Left (UnsupportedStatement e) + go e@(NaturalSubtract ) = 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 c088ea5..1baea1e 100644 --- a/dhall-json/src/Dhall/JSON.hs +++ b/dhall-json/src/Dhall/JSON.hs @@ -639,6 +639,9 @@ convertToHomogeneousMaps (Conversion {..}) e0 = loop (Core.normalize e0) Core.NaturalShow -> Core.NaturalShow + Core.NaturalSubtract -> + Core.NaturalSubtract + Core.NaturalPlus a b -> Core.NaturalPlus a' b' where diff --git a/dhall-nix/src/Dhall/Nix.hs b/dhall-nix/src/Dhall/Nix.hs index ee7cd24..1bfd76a 100644 --- a/dhall-nix/src/Dhall/Nix.hs +++ b/dhall-nix/src/Dhall/Nix.hs @@ -300,6 +300,14 @@ dhallToNix e = loop (Dhall.Core.normalize e) return (Fix (NLet [e5] e8)) loop NaturalShow = do return "toString" + loop NaturalSubtract = do + let e0 = NamedVar ["z"] (Fix (NBinary NMinus "y" "x")) Nix.nullPos + let e1 = Fix (NBinary NLt "z" (Fix (NConstant (NInt 0)))) + let e2 = Fix (NConstant (NInt 0)) + let e3 = "z" + let e4 = Fix (NIf e1 e2 e3) + let e5 = Fix (NLet [e0] e4) + return (Fix (NAbs "x" (Fix (NAbs "y" e5)))) loop NaturalToInteger = do return (Fix (NAbs "n" "n")) loop (NaturalPlus a b) = do diff --git a/dhall/dhall-lang b/dhall/dhall-lang index f692f70..c7082d9 160000 --- a/dhall/dhall-lang +++ b/dhall/dhall-lang @@ -1 +1 @@ -Subproject commit f692f70bafa0322da5d9c4b535b2d323a9c5ac61 +Subproject commit c7082d910d956bcedfdc51daae989659a2db67bd diff --git a/dhall/src/Dhall/Binary.hs b/dhall/src/Dhall/Binary.hs index ca99edb..d8793cb 100644 --- a/dhall/src/Dhall/Binary.hs +++ b/dhall/src/Dhall/Binary.hs @@ -122,6 +122,8 @@ instance ToTerm a => ToTerm (Expr X a) where TString "Natural/toInteger" encode NaturalShow = TString "Natural/show" + encode NaturalSubtract = + TString "Natural/subtract" encode IntegerToDouble = TString "Integer/toDouble" encode IntegerShow = @@ -482,6 +484,8 @@ instance FromTerm a => FromTerm (Expr s a) where return NaturalToInteger decode (TString "Natural/show") = return NaturalShow + decode (TString "Natural/subtract") = + return NaturalSubtract decode (TString "Integer/toDouble") = return IntegerToDouble decode (TString "Integer/show") = diff --git a/dhall/src/Dhall/Core.hs b/dhall/src/Dhall/Core.hs index 1c6962e..ac40805 100644 --- a/dhall/src/Dhall/Core.hs +++ b/dhall/src/Dhall/Core.hs @@ -405,6 +405,8 @@ data Expr s a | NaturalToInteger -- | > NaturalShow ~ Natural/show | NaturalShow + -- | > NaturalSubtract ~ Natural/subtract + | NaturalSubtract -- | > NaturalPlus x y ~ x + y | NaturalPlus (Expr s a) (Expr s a) -- | > NaturalTimes x y ~ x * y @@ -525,6 +527,7 @@ instance Functor (Expr s) where fmap _ NaturalOdd = NaturalOdd fmap _ NaturalToInteger = NaturalToInteger fmap _ NaturalShow = NaturalShow + fmap _ NaturalSubtract = NaturalSubtract fmap f (NaturalPlus e1 e2) = NaturalPlus (fmap f e1) (fmap f e2) fmap f (NaturalTimes e1 e2) = NaturalTimes (fmap f e1) (fmap f e2) fmap _ Integer = Integer @@ -601,6 +604,7 @@ instance Monad (Expr s) where NaturalOdd >>= _ = NaturalOdd NaturalToInteger >>= _ = NaturalToInteger NaturalShow >>= _ = NaturalShow + NaturalSubtract >>= _ = NaturalSubtract NaturalPlus a b >>= k = NaturalPlus (a >>= k) (b >>= k) NaturalTimes a b >>= k = NaturalTimes (a >>= k) (b >>= k) Integer >>= _ = Integer @@ -667,6 +671,7 @@ instance Bifunctor Expr where first _ NaturalOdd = NaturalOdd first _ NaturalToInteger = NaturalToInteger first _ NaturalShow = NaturalShow + first _ NaturalSubtract = NaturalSubtract first k (NaturalPlus a b ) = NaturalPlus (first k a) (first k b) first k (NaturalTimes a b ) = NaturalTimes (first k a) (first k b) first _ Integer = Integer @@ -901,6 +906,7 @@ shift _ _ NaturalEven = NaturalEven shift _ _ NaturalOdd = NaturalOdd shift _ _ NaturalToInteger = NaturalToInteger shift _ _ NaturalShow = NaturalShow +shift _ _ NaturalSubtract = NaturalSubtract shift d v (NaturalPlus a b) = NaturalPlus a' b' where a' = shift d v a @@ -1076,6 +1082,7 @@ subst _ _ NaturalEven = NaturalEven subst _ _ NaturalOdd = NaturalOdd subst _ _ NaturalToInteger = NaturalToInteger subst _ _ NaturalShow = NaturalShow +subst _ _ NaturalSubtract = NaturalSubtract subst x e (NaturalPlus a b) = NaturalPlus a' b' where a' = subst x e a @@ -1250,6 +1257,7 @@ denote NaturalEven = NaturalEven denote NaturalOdd = NaturalOdd denote NaturalToInteger = NaturalToInteger denote NaturalShow = NaturalShow +denote NaturalSubtract = NaturalSubtract denote (NaturalPlus a b ) = NaturalPlus (denote a) (denote b) denote (NaturalTimes a b ) = NaturalTimes (denote a) (denote b) denote Integer = Integer @@ -1400,6 +1408,11 @@ normalizeWithM ctx e0 = loop (denote e0) App NaturalToInteger (NaturalLit n) -> pure (IntegerLit (toInteger n)) App NaturalShow (NaturalLit n) -> pure (TextLit (Chunks [] (Data.Text.pack (show n)))) + App (App NaturalSubtract (NaturalLit x)) (NaturalLit y) + | y >= x -> pure (NaturalLit (subtract x y)) + | otherwise -> pure (NaturalLit 0) + App (App NaturalSubtract (NaturalLit 0)) y -> pure y + App (App NaturalSubtract _) (NaturalLit 0) -> pure (NaturalLit 0) App IntegerShow (IntegerLit n) | 0 <= n -> pure (TextLit (Chunks [] ("+" <> Data.Text.pack (show n)))) | otherwise -> pure (TextLit (Chunks [] (Data.Text.pack (show n)))) @@ -1554,6 +1567,7 @@ normalizeWithM ctx e0 = loop (denote e0) NaturalOdd -> pure NaturalOdd NaturalToInteger -> pure NaturalToInteger NaturalShow -> pure NaturalShow + NaturalSubtract -> pure NaturalSubtract NaturalPlus x y -> decide <$> loop x <*> loop y where decide (NaturalLit 0) r = r @@ -1823,6 +1837,9 @@ isNormalized e0 = loop (denote e0) App NaturalEven (NaturalLit _) -> False App NaturalOdd (NaturalLit _) -> False App NaturalShow (NaturalLit _) -> False + App (App NaturalSubtract (NaturalLit _)) (NaturalLit _) -> False + App (App NaturalSubtract (NaturalLit 0)) _ -> False + App (App NaturalSubtract _) (NaturalLit 0) -> False App NaturalToInteger (NaturalLit _) -> False App IntegerShow (IntegerLit _) -> False App IntegerToDouble (IntegerLit _) -> False @@ -1881,6 +1898,7 @@ isNormalized e0 = loop (denote e0) NaturalEven -> True NaturalOdd -> True NaturalShow -> True + NaturalSubtract -> True NaturalToInteger -> True NaturalPlus x y -> loop x && loop y && decide x y where @@ -2047,6 +2065,7 @@ reservedIdentifiers = , "Natural/odd" , "Natural/toInteger" , "Natural/show" + , "Natural/subtract" , "Integer" , "Integer/show" , "Integer/toDouble" @@ -2099,6 +2118,7 @@ subExpressions _ NaturalEven = pure NaturalEven subExpressions _ NaturalOdd = pure NaturalOdd subExpressions _ NaturalToInteger = pure NaturalToInteger subExpressions _ NaturalShow = pure NaturalShow +subExpressions _ NaturalSubtract = pure NaturalSubtract subExpressions f (NaturalPlus a b) = NaturalPlus <$> f a <*> f b subExpressions f (NaturalTimes a b) = NaturalTimes <$> f a <*> f b subExpressions _ Integer = pure Integer diff --git a/dhall/src/Dhall/Diff.hs b/dhall/src/Dhall/Diff.hs index 11d866e..4e7eca4 100644 --- a/dhall/src/Dhall/Diff.hs +++ b/dhall/src/Dhall/Diff.hs @@ -1070,6 +1070,12 @@ diffPrimitiveExpression l@NaturalShow r = mismatch l r diffPrimitiveExpression l r@NaturalShow = mismatch l r +diffPrimitiveExpression NaturalSubtract NaturalSubtract = + "…" +diffPrimitiveExpression l@NaturalSubtract r = + mismatch l r +diffPrimitiveExpression l r@NaturalSubtract = + 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 5d6f19f..33d7d72 100644 --- a/dhall/src/Dhall/Eval.hs +++ b/dhall/src/Dhall/Eval.hs @@ -173,6 +173,7 @@ data Val a | VNaturalOdd !(Val a) | VNaturalToInteger !(Val a) | VNaturalShow !(Val a) + | VNaturalSubtract !(Val a) !(Val a) | VNaturalPlus !(Val a) !(Val a) | VNaturalTimes !(Val a) !(Val a) @@ -413,6 +414,14 @@ eval !env t = n -> VNaturalToInteger n NaturalShow -> VPrim $ \case VNaturalLit n -> VTextLit (VChunks [] (Data.Text.pack (show n))) n -> VNaturalShow n + NaturalSubtract -> VPrim $ \x -> VPrim $ \y -> + case (x,y) of + (VNaturalLit x, VNaturalLit y) + | y >= x -> VNaturalLit (subtract x y) + | otherwise -> VNaturalLit 0 + (VNaturalLit 0, y) -> y + (x, VNaturalLit 0) -> VNaturalLit 0 + (x, y) -> VNaturalSubtract x y NaturalPlus t u -> vNaturalPlus (evalE t) (evalE u) NaturalTimes t u -> case (evalE t, evalE u) of (VNaturalLit 1, u ) -> u @@ -662,14 +671,15 @@ conv !env t t' = (VNaturalFold t _ u v, VNaturalFold t' _ u' v') -> convE t t' && convE u u' && convE v v' - (VNaturalBuild t , VNaturalBuild t') -> convE t t' - (VNaturalIsZero t , VNaturalIsZero t') -> convE t t' - (VNaturalEven t , VNaturalEven t') -> convE t t' - (VNaturalOdd t , VNaturalOdd t') -> convE t t' - (VNaturalToInteger t , VNaturalToInteger t') -> convE t t' - (VNaturalShow t , VNaturalShow t') -> convE t t' - (VNaturalPlus t u , VNaturalPlus t' u') -> convE t t' && convE u u' - (VNaturalTimes t u , VNaturalTimes t' u') -> convE t t' && convE u u' + (VNaturalBuild t , VNaturalBuild t') -> convE t t' + (VNaturalIsZero t , VNaturalIsZero t') -> convE t t' + (VNaturalEven t , VNaturalEven t') -> convE t t' + (VNaturalOdd t , VNaturalOdd t') -> convE t t' + (VNaturalToInteger t , VNaturalToInteger t') -> convE t t' + (VNaturalShow t , VNaturalShow t') -> convE t t' + (VNaturalSubtract x y , VNaturalSubtract x' y') -> convE x x' && convE y y' + (VNaturalPlus t u , VNaturalPlus t' u') -> convE t t' && convE u u' + (VNaturalTimes t u , VNaturalTimes t' u') -> convE t t' && convE u u' (VInteger , VInteger) -> True (VIntegerLit t , VIntegerLit t') -> t == t' @@ -807,6 +817,7 @@ quote !env !t = VNaturalShow t -> NaturalShow `qApp` t VNaturalPlus t u -> NaturalPlus (quoteE t) (quoteE u) VNaturalTimes t u -> NaturalTimes (quoteE t) (quoteE u) + VNaturalSubtract x y -> NaturalSubtract `qApp` x `qApp` y VInteger -> Integer VIntegerLit n -> IntegerLit n @@ -922,6 +933,7 @@ alphaNormalize = goEnv NEmpty where NaturalOdd -> NaturalOdd NaturalToInteger -> NaturalToInteger NaturalShow -> NaturalShow + NaturalSubtract -> NaturalSubtract NaturalPlus t u -> NaturalPlus (go t) (go u) NaturalTimes t u -> NaturalTimes (go t) (go u) Integer -> Integer diff --git a/dhall/src/Dhall/Import.hs b/dhall/src/Dhall/Import.hs index 233203d..4532e50 100644 --- a/dhall/src/Dhall/Import.hs +++ b/dhall/src/Dhall/Import.hs @@ -924,6 +924,7 @@ loadWith expr₀ = case expr₀ of NaturalOdd -> pure NaturalOdd NaturalToInteger -> pure NaturalToInteger NaturalShow -> pure NaturalShow + NaturalSubtract -> pure NaturalSubtract NaturalPlus a b -> NaturalPlus <$> loadWith a <*> loadWith b NaturalTimes a b -> NaturalTimes <$> loadWith a <*> loadWith b Integer -> pure Integer diff --git a/dhall/src/Dhall/Parser/Expression.hs b/dhall/src/Dhall/Parser/Expression.hs index 53a8f21..44d02bb 100644 --- a/dhall/src/Dhall/Parser/Expression.hs +++ b/dhall/src/Dhall/Parser/Expression.hs @@ -356,7 +356,7 @@ parsers embedded = Parsers {..} , NaturalIsZero <$ _NaturalIsZero , NaturalEven <$ _NaturalEven , NaturalOdd <$ _NaturalOdd - , NaturalToInteger <$ _NaturalToInteger + , NaturalSubtract <$ _NaturalSubtract , NaturalToInteger <$ _NaturalToInteger , NaturalShow <$ _NaturalShow , Natural <$ _Natural diff --git a/dhall/src/Dhall/Parser/Token.hs b/dhall/src/Dhall/Parser/Token.hs index 0b241e2..6ab027c 100644 --- a/dhall/src/Dhall/Parser/Token.hs +++ b/dhall/src/Dhall/Parser/Token.hs @@ -39,6 +39,7 @@ module Dhall.Parser.Token ( _NaturalOdd, _NaturalToInteger, _NaturalShow, + _NaturalSubtract, _IntegerShow, _IntegerToDouble, _DoubleShow, @@ -625,6 +626,9 @@ _NaturalToInteger = reserved "Natural/toInteger" _NaturalShow :: Parser () _NaturalShow = reserved "Natural/show" +_NaturalSubtract :: Parser () +_NaturalSubtract = reserved "Natural/subtract" + _IntegerShow :: Parser () _IntegerShow = reserved "Integer/show" diff --git a/dhall/src/Dhall/Pretty/Internal.hs b/dhall/src/Dhall/Pretty/Internal.hs index 5b389a1..9f994cf 100644 --- a/dhall/src/Dhall/Pretty/Internal.hs +++ b/dhall/src/Dhall/Pretty/Internal.hs @@ -798,6 +798,8 @@ prettyCharacterSet characterSet expression = builtin "Natural/toInteger" prettyPrimitiveExpression NaturalShow = builtin "Natural/show" + prettyPrimitiveExpression NaturalSubtract = + builtin "Natural/subtract" prettyPrimitiveExpression Integer = builtin "Integer" prettyPrimitiveExpression IntegerShow = diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index a981c50..bbd73fd 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -306,6 +306,8 @@ typeWithA tpa = loop return (Pi "_" Natural Integer) loop _ NaturalShow = do return (Pi "_" Natural Text) + loop _ NaturalSubtract = do + return (Pi "_" Natural (Pi "_" Natural Natural)) loop ctx e@(NaturalPlus l r) = do tl <- fmap Dhall.Core.normalize (loop ctx l) case tl of diff --git a/dhall/tests/Dhall/Test/QuickCheck.hs b/dhall/tests/Dhall/Test/QuickCheck.hs index 64ce938..298d9e4 100644 --- a/dhall/tests/Dhall/Test/QuickCheck.hs +++ b/dhall/tests/Dhall/Test/QuickCheck.hs @@ -203,6 +203,7 @@ instance (Arbitrary s, Arbitrary a) => Arbitrary (Expr s a) where , ( 1, lift0 NaturalShow) , ( 1, lift2 NaturalPlus) , ( 1, lift2 NaturalTimes) + , ( 1, lift0 NaturalSubtract) , ( 1, lift0 Integer) , ( 7, fmap IntegerLit integer) , ( 1, lift0 IntegerShow)