Add truncated Natural subtraction

2 files changed, 11 insertions, 0 deletions

diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 3e45240..395cf28 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -47,6 +47,16 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
             )),
             _ => Err(()),
         },
+        (NaturalSubtract, [a, b, r..]) => {
+            match (&*a.as_value(), &*b.as_value()) {
+                (NaturalLit(a), NaturalLit(b)) => {
+                    Ok((r, NaturalLit(if b > a { b - a } else { 0 })))
+                }
+                (NaturalLit(0), b) => Ok((r, b.clone())),
+                (_, NaturalLit(0)) => Ok((r, NaturalLit(0))),
+                _ => Err(()),
+            }
+        }
         (IntegerShow, [n, r..]) => match &*n.as_value() {
             IntegerLit(n) => {
                 let s = if *n < 0 {
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 4b3a03f..2e4642c 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -212,6 +212,7 @@ fn type_of_builtin(b: Builtin) -> Expr<X, X> {
         ),
         NaturalToInteger => dhall::expr!(Natural -> Integer),
         NaturalShow => dhall::expr!(Natural -> Text),
+        NaturalSubtract => dhall::expr!(Natural -> Natural -> Natural),
 
         IntegerToDouble => dhall::expr!(Integer -> Double),
         IntegerShow => dhall::expr!(Integer -> Text),