diff options
| m--------- | dhall-lang | 0 | ||||
| -rw-r--r-- | dhall/src/phase/normalize.rs | 10 | ||||
| -rw-r--r-- | dhall/src/phase/typecheck.rs | 1 | ||||
| -rw-r--r-- | dhall_generated_parser/src/dhall.pest.visibility | 1 | ||||
| -rw-r--r-- | dhall_syntax/src/core/expr.rs | 1 | ||||
| -rw-r--r-- | dhall_syntax/src/parser.rs | 1 | ||||
| -rw-r--r-- | dhall_syntax/src/printer.rs | 1 |
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", |