summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/phase/normalize.rs10
-rw-r--r--dhall/src/phase/typecheck.rs1
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),