From 51c4f79fe092191d670ffa2f9098693079dbc1be Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 7 Aug 2019 21:18:11 +0200
Subject: Add truncated Natural subtraction

---
 dhall-lang                                       |  2 +-
 dhall/src/phase/normalize.rs                     | 10 ++++++++++
 dhall/src/phase/typecheck.rs                     |  1 +
 dhall_generated_parser/src/dhall.pest.visibility |  1 +
 dhall_syntax/src/core/expr.rs                    |  1 +
 dhall_syntax/src/parser.rs                       |  1 +
 dhall_syntax/src/printer.rs                      |  1 +
 7 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/dhall-lang b/dhall-lang
index f692f70..c7082d9 160000
--- a/dhall-lang
+++ b/dhall-lang
@@ -1 +1 @@
-Subproject commit f692f70bafa0322da5d9c4b535b2d323a9c5ac61
+Subproject commit c7082d910d956bcedfdc51daae989659a2db67bd
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),
diff --git a/dhall_generated_parser/src/dhall.pest.visibility b/dhall_generated_parser/src/dhall.pest.visibility
index dd54578..de6dc8d 100644
--- a/dhall_generated_parser/src/dhall.pest.visibility
+++ b/dhall_generated_parser/src/dhall.pest.visibility
@@ -71,6 +71,7 @@ Location
 # Natural_show
 # Integer_toDouble
 # Integer_show
+# Natural_subtract
 # Double_show
 # List_build
 # List_fold
diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs
index aab4b6a..b293357 100644
--- a/dhall_syntax/src/core/expr.rs
+++ b/dhall_syntax/src/core/expr.rs
@@ -119,6 +119,7 @@ pub enum Builtin {
     NaturalOdd,
     NaturalToInteger,
     NaturalShow,
+    NaturalSubtract,
     IntegerToDouble,
     IntegerShow,
     DoubleShow,
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index a7f419a..72dfcdd 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -80,6 +80,7 @@ impl crate::Builtin {
             "Natural/odd" => Some(NaturalOdd),
             "Natural/toInteger" => Some(NaturalToInteger),
             "Natural/show" => Some(NaturalShow),
+            "Natural/subtract" => Some(NaturalSubtract),
             "Integer/toDouble" => Some(IntegerToDouble),
             "Integer/show" => Some(IntegerShow),
             "Double/show" => Some(DoubleShow),
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index db688bd..1d6c113 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -449,6 +449,7 @@ impl Display for Builtin {
             NaturalOdd => "Natural/odd",
             NaturalToInteger => "Natural/toInteger",
             NaturalShow => "Natural/show",
+            NaturalSubtract => "Natural/subtract",
             IntegerToDouble => "Integer/toDouble",
             IntegerShow => "Integer/show",
             DoubleShow => "Double/show",
-- 
cgit v1.2.3