git.iko.soy/Idris-dev
on master help sign in
Improve implementation of toIntNat
3c31a7eEdwin Brady
CHANGELOG.md+1−2
compare with master
unifiedsplit
@@ -4,8 +4,7 @@
4+ New JavaScript code generator that uses an higher level intermediate
4+ New JavaScript code generator that uses an higher level intermediate
5 representation.
5 representation.
6
6
7−+ Various optimizations of the novel JavaScript code generator to make
7++ Various optimizations of the new JavaScript code generator.
8− its results fast.
9
8
10+ Names are now annotated with their representations over the IDE
9+ Names are now annotated with their representations over the IDE
11 protocol, which allows IDEs to provide commands that work on special
10 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
7
7
8||| Interface for transforming an instance of a data type to another type.
8||| Interface for transforming an instance of a data type to another type.
9interface Cast from to where
9interface Cast from to where
10− ||| Perform a cast operation.
10+ ||| Perform a (potentially lossy!) cast operation.
11 |||
11 |||
12 ||| @orig The original type.
12 ||| @orig The original type.
13 cast : (orig : from) -> to
13 cast : (orig : from) -> to
libs/prelude/Prelude/Nat.idr+2−5
@@ -191,13 +191,10 @@ maximum Z m = m
191maximum (S n) Z = S n
191maximum (S n) Z = S n
192maximum (S n) (S m) = S (maximum n m)
192maximum (S n) (S m) = S (maximum n m)
193
193
194−||| Tail recursive cast Nat to Int
194+||| Cast Nat to Int
195||| Note that this can overflow
195||| Note that this can overflow
196toIntNat : Nat -> Int
196toIntNat : Nat -> Int
197−toIntNat n = toIntNat' n 0 where
197+toIntNat n = prim__truncBigInt_Int (toIntegerNat n)
198− toIntNat' : Nat -> Int -> Int
199− toIntNat' Z x = x
200− toIntNat' (S n) x = toIntNat' n (x + 1)
201
198
202(-) : (m : Nat) -> (n : Nat) -> {auto smaller : LTE n m} -> Nat
199(-) : (m : Nat) -> (n : Nat) -> {auto smaller : LTE n m} -> Nat
203(-) m n {smaller} = minus m n
200(-) m n {smaller} = minus m n