summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
m---------dhall-lang0
-rw-r--r--dhall/src/phase/normalize.rs10
-rw-r--r--dhall/src/phase/typecheck.rs1
-rw-r--r--dhall_generated_parser/src/dhall.pest.visibility1
-rw-r--r--dhall_syntax/src/core/expr.rs1
-rw-r--r--dhall_syntax/src/parser.rs1
-rw-r--r--dhall_syntax/src/printer.rs1
7 files changed, 15 insertions, 0 deletions
diff --git a/dhall-lang b/dhall-lang
-Subproject f692f70bafa0322da5d9c4b535b2d323a9c5ac6
+Subproject c7082d910d956bcedfdc51daae989659a2db67b
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",