git.iko.soy/Idris-dev
on master help sign in
Beginnings of generic machine integer support
5734ddfBenjamin Saunders
lib/Prelude.idr+1
compare with master
unifiedsplit
@@ -6,6 +6,7 @@ import IO
6import Prelude.Cast
6import Prelude.Cast
7import Prelude.Nat
7import Prelude.Nat
8import Prelude.Fin
8import Prelude.Fin
9+import Prelude.Modular
9import Prelude.List
10import Prelude.List
10import Prelude.Maybe
11import Prelude.Maybe
11import Prelude.Monad
12import Prelude.Monad
lib/Prelude/Bits.idrnew file+58
@@ -0,0 +1,58 @@
1+module Bits
2+
3+%default total
4+
5+log2ceil : Nat -> Nat
6+log2ceil n = let x = log2 n in
7+ if x == log2 (n-1)
8+ then x+1
9+ else x
10+
11+Bits : Nat -> Type
12+Bits x with (log2ceil x)
13+ | (S (S (S (S (S (S _)))))) = Bits64
14+ | (S (S (S (S (S O))))) = Bits32
15+ | (S (S (S (S O)))) = Bits16
16+ | _ = Bits8
17+
18+intToBits : {n: Nat} -> Int -> Bits n
19+intToBits {n=n} x with (Bits n)
20+ | Bits8 = prim__intToB8 x
21+ | Bits16 = prim__intToB16 x
22+ | Bits32 = prim__intToB32 x
23+ | Bits64 = prim__intToB64 x
24+
25+bitsAdd : {n : Nat} -> Bits n -> Bits n -> Bits n
26+bitsAdd {n=m} x y with (Bits m)
27+ | Bits8 = prim__addB8 x y
28+ | Bits16 = prim__addB16 x y
29+ | Bits32 = prim__addB32 x y
30+ | Bits64 = prim__addB64 x y
31+
32+bitsSub : {n : Nat} -> Bits n -> Bits n -> Bits n
33+bitsSub {n=m} x y with (Bits m)
34+ | Bits8 = prim__subB8 x y
35+ | Bits16 = prim__subB16 x y
36+ | Bits32 = prim__subB32 x y
37+ | Bits64 = prim__subB64 x y
38+
39+bitsMul : {n : Nat} -> Bits n -> Bits n -> Bits n
40+bitsMul {n=m} x y with (Bits m)
41+ | Bits8 = prim__mulB8 x y
42+ | Bits16 = prim__mulB16 x y
43+ | Bits32 = prim__mulB32 x y
44+ | Bits64 = prim__mulB64 x y
45+
46+bitsSDiv : {n : Nat} -> Bits n -> Bits n -> Bits n
47+bitsSDiv {n=m} x y with (Bits m)
48+ | Bits8 = prim__sdivB8 x y
49+ | Bits16 = prim__sdivB16 x y
50+ | Bits32 = prim__sdivB32 x y
51+ | Bits64 = prim__sdivB64 x y
52+
53+bitsUDiv : {n : Nat} -> Bits n -> Bits n -> Bits n
54+bitsUDiv {n=m} x y with (Bits m)
55+ | Bits8 = prim__udivB8 x y
56+ | Bits16 = prim__udivB16 x y
57+ | Bits32 = prim__udivB32 x y
58+ | Bits64 = prim__udivB64 x y
lib/Prelude/Modular.idrnew file+26
@@ -0,0 +1,26 @@
1+module Modular
2+import Prelude.Bits
3+
4+%default total
5+
6+data Modulo : Nat -> Type where
7+ MkModulo : {n : Nat} -> Bits (log2 (2*n)) -> Modulo (S n)
8+
9+modAdd : Modulo n -> Modulo n -> Modulo n
10+modAdd (MkModulo x) (MkModulo y) = MkModulo (bitsAdd x y)
11+
12+modSub : Modulo n -> Modulo n -> Modulo n
13+modSub (MkModulo x) (MkModulo y) = MkModulo (bitsSub x y)
14+
15+modMul : Modulo n -> Modulo n -> Modulo n
16+modMul (MkModulo x) (MkModulo y) = MkModulo (bitsMul x y)
17+
18+modDiv : Modulo n -> Modulo n -> Modulo n
19+modDiv (MkModulo x) (MkModulo y) = MkModulo (bitsUDiv x y)
20+
21+instance Num (Modulo (S n)) where
22+ (+) = modAdd
23+ (-) = modSub
24+ (*) = modMul
25+ abs = id
26+ fromInteger x = MkModulo (intToBits x)
lib/base.ipkg+2−1
@@ -6,7 +6,8 @@ modules = Builtins, Prelude, IO, System,
6 Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,
6 Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,
7 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
7 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
8 Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,
8 Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,
9− Prelude.Heap, Prelude.Complex, Prelude.Functor,
9+ Prelude.Heap, Prelude.Complex, Prelude.Functor, Prelude.Modular,
10+ Prelude.Bits
10
11
11 Network.Cgi,
12 Network.Cgi,
12 Debug.Trace,
13 Debug.Trace,