summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/phase
diff options
context:
space:
mode:
authorNadrieril2019-12-23 21:59:47 +0000
committerNadrieril2019-12-23 21:59:47 +0000
commit0e928ebde4ab8b662499eb716f366b97479c75fc (patch)
tree80e836e2a76ed70718ee31ab01e95b67fc59f248 /dhall/src/semantics/phase
parentcb2097ed82c7aa23f555cb27a7e27a32863de09a (diff)
Add two new Integer builtins
Diffstat (limited to 'dhall/src/semantics/phase')
-rw-r--r--dhall/src/semantics/phase/normalize.rs11
-rw-r--r--dhall/src/semantics/phase/typecheck.rs3
2 files changed, 14 insertions, 0 deletions
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 6258ae8..5a0f566 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -1,4 +1,5 @@
use std::collections::HashMap;
+use std::convert::TryInto;
use crate::semantics::core::value::Value;
use crate::semantics::core::value::ValueKind;
@@ -141,6 +142,16 @@ pub(crate) fn apply_builtin(
}
_ => Ret::DoneAsIs,
},
+ (IntegerNegate, [n]) => match &*n.as_whnf() {
+ IntegerLit(n) => Ret::ValueKind(IntegerLit(-n)),
+ _ => Ret::DoneAsIs,
+ },
+ (IntegerClamp, [n]) => match &*n.as_whnf() {
+ IntegerLit(n) => {
+ Ret::ValueKind(NaturalLit((*n).try_into().unwrap_or(0)))
+ }
+ _ => Ret::DoneAsIs,
+ },
(DoubleShow, [n]) => {
match &*n.as_whnf() {
DoubleLit(n) => Ret::ValueKind(TextLit(vec![
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index c9834e1..7ea4951 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -235,6 +235,9 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
IntegerToDouble => make_type!(Integer -> Double),
IntegerShow => make_type!(Integer -> Text),
+ IntegerNegate => make_type!(Integer -> Integer),
+ IntegerClamp => make_type!(Integer -> Natural),
+
DoubleShow => make_type!(Double -> Text),
TextShow => make_type!(Text -> Text),