diff options
| author | Nadrieril | 2019-12-23 21:59:47 +0000 |
|---|---|---|
| committer | Nadrieril | 2019-12-23 21:59:47 +0000 |
| commit | 0e928ebde4ab8b662499eb716f366b97479c75fc (patch) | |
| tree | 80e836e2a76ed70718ee31ab01e95b67fc59f248 /dhall/src/semantics/phase | |
| parent | cb2097ed82c7aa23f555cb27a7e27a32863de09a (diff) | |
Add two new Integer builtins
Diffstat (limited to 'dhall/src/semantics/phase')
| -rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 11 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/typecheck.rs | 3 |
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), |