summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-12-23 21:59:47 +0000
committerNadrieril2019-12-23 21:59:47 +0000
commit0e928ebde4ab8b662499eb716f366b97479c75fc (patch)
tree80e836e2a76ed70718ee31ab01e95b67fc59f248
parentcb2097ed82c7aa23f555cb27a7e27a32863de09a (diff)
Add two new Integer builtins
m---------dhall-lang0
-rw-r--r--dhall/src/semantics/phase/normalize.rs11
-rw-r--r--dhall/src/semantics/phase/typecheck.rs3
-rw-r--r--dhall/src/syntax/ast/expr.rs2
-rw-r--r--dhall/src/syntax/text/parser.rs2
-rw-r--r--dhall/src/syntax/text/printer.rs2
6 files changed, 20 insertions, 0 deletions
diff --git a/dhall-lang b/dhall-lang
-Subproject 89bbf42f9fd3e9e09f0a15aac9a23d309e50b15
+Subproject ee120309828f8a18b3267d192e3030add2a718e
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),
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index fe49448..68cb524 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -79,6 +79,8 @@ pub enum Builtin {
NaturalSubtract,
IntegerToDouble,
IntegerShow,
+ IntegerNegate,
+ IntegerClamp,
DoubleShow,
ListBuild,
ListFold,
diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs
index fe34aee..d9e5c3b 100644
--- a/dhall/src/syntax/text/parser.rs
+++ b/dhall/src/syntax/text/parser.rs
@@ -57,6 +57,8 @@ impl crate::syntax::Builtin {
"Natural/subtract" => Some(NaturalSubtract),
"Integer/toDouble" => Some(IntegerToDouble),
"Integer/show" => Some(IntegerShow),
+ "Integer/negate" => Some(IntegerNegate),
+ "Integer/clamp" => Some(IntegerClamp),
"Double/show" => Some(DoubleShow),
"List/build" => Some(ListBuild),
"List/fold" => Some(ListFold),
diff --git a/dhall/src/syntax/text/printer.rs b/dhall/src/syntax/text/printer.rs
index 626ab1c..96f4c2a 100644
--- a/dhall/src/syntax/text/printer.rs
+++ b/dhall/src/syntax/text/printer.rs
@@ -468,6 +468,8 @@ impl Display for Builtin {
NaturalShow => "Natural/show",
NaturalSubtract => "Natural/subtract",
IntegerToDouble => "Integer/toDouble",
+ IntegerNegate => "Integer/negate",
+ IntegerClamp => "Integer/clamp",
IntegerShow => "Integer/show",
DoubleShow => "Double/show",
ListBuild => "List/build",