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/src/phase/normalize.rs | 10 ++++++++++ dhall/src/phase/typecheck.rs | 1 + 2 files changed, 11 insertions(+) (limited to 'dhall/src/phase') 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) -> 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 { ), 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), -- cgit v1.2.3