Simplify Natural/subtract when its arguments are equivalent (#1220)

…as standardized in https://github.com/dhall-lang/dhall-lang/pull/685.
This commit is contained in:
Simon Jakobi 2019-08-08 04:39:21 +02:00 committed by mergify[bot]
parent ecb5814f59
commit 97f0ff8552
2 changed files with 3 additions and 0 deletions

View File

@ -1439,6 +1439,7 @@ normalizeWithM ctx e0 = loop (denote e0)
| otherwise -> pure (NaturalLit 0)
App (App NaturalSubtract (NaturalLit 0)) y -> pure y
App (App NaturalSubtract _) (NaturalLit 0) -> pure (NaturalLit 0)
App (App NaturalSubtract x) y | judgmentallyEqual x y -> 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))))
@ -1877,6 +1878,7 @@ isNormalized e0 = loop (denote e0)
App (App NaturalSubtract (NaturalLit _)) (NaturalLit _) -> False
App (App NaturalSubtract (NaturalLit 0)) _ -> False
App (App NaturalSubtract _) (NaturalLit 0) -> False
App (App NaturalSubtract x) y -> not (judgmentallyEqual x y)
App NaturalToInteger (NaturalLit _) -> False
App IntegerShow (IntegerLit _) -> False
App IntegerToDouble (IntegerLit _) -> False

View File

@ -427,6 +427,7 @@ eval !env t =
x ->
VPrim $ \case
VNaturalLit 0 -> VNaturalLit 0
y | conv env x y -> VNaturalLit 0
y -> VNaturalSubtract x y
NaturalPlus t u -> vNaturalPlus (evalE t) (evalE u)
NaturalTimes t u -> case (evalE t, evalE u) of