git.iko.soy/Idris-dev
on master help sign in
Improve implementation of toIntNat

Converting via Integer means that it's constant time rather than linear, because Integer and Nat have the same representation at run time

commit3c31a7ef860932c95b8db8d9d03e05a4f1d19d02 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 17 Jun 2017, 23:01 (9 years ago) parent7b1a31a
3 files changed+4−8
compare with master
unifiedsplit
CHANGELOG.md+1−2 libs/prelude/Prelude/Cast.idr+1−1 libs/prelude/Prelude/Nat.idr+2−5
CHANGELOG.md+1−2
@@ -4,8 +4,7 @@
44+ New JavaScript code generator that uses an higher level intermediate
55 representation.
66
7−+ Various optimizations of the novel JavaScript code generator to make
8− its results fast.
7++ Various optimizations of the new JavaScript code generator.
98
109+ Names are now annotated with their representations over the IDE
1110 protocol, which allows IDEs to provide commands that work on special
libs/prelude/Prelude/Cast.idr+1−1
@@ -7,7 +7,7 @@ import public Builtins
77
88||| Interface for transforming an instance of a data type to another type.
99interface Cast from to where
10− ||| Perform a cast operation.
10+ ||| Perform a (potentially lossy!) cast operation.
1111 |||
1212 ||| @orig The original type.
1313 cast : (orig : from) -> to
libs/prelude/Prelude/Nat.idr+2−5
@@ -191,13 +191,10 @@ maximum Z m = m
191191maximum (S n) Z = S n
192192maximum (S n) (S m) = S (maximum n m)
193193
194−||| Tail recursive cast Nat to Int
194+||| Cast Nat to Int
195195||| Note that this can overflow
196196toIntNat : Nat -> Int
197−toIntNat n = toIntNat' n 0 where
198− toIntNat' : Nat -> Int -> Int
199− toIntNat' Z x = x
200− toIntNat' (S n) x = toIntNat' n (x + 1)
197+toIntNat n = prim__truncBigInt_Int (toIntegerNat n)
201198
202199(-) : (m : Nat) -> (n : Nat) -> {auto smaller : LTE n m} -> Nat
203200(-) m n {smaller} = minus m n