git.iko.soy/Idris-dev
on master help sign in
Split numeric instances of algebraic classes into their own module
2b258dbBlackBrane
libs/contrib/Control/Algebra/NumericInstances.idrnew file+104
compare with master
unifiedsplit
@@ -0,0 +1,104 @@
1+module Control.Algebra.NumericInstances
2+
3+import Control.Algebra
4+import Data.Complex
5+import Data.ZZ
6+
7+
8+instance Semigroup Integer where
9+ (<+>) = (+)
10+
11+instance Monoid Integer where
12+ neutral = 0
13+
14+instance Group Integer where
15+ inverse = (* -1)
16+
17+instance AbelianGroup Integer
18+
19+instance Ring Integer where
20+ (<.>) = (*)
21+
22+instance RingWithUnity Integer where
23+ unity = 1
24+
25+
26+instance Semigroup Int where
27+ (<+>) = (+)
28+
29+instance Monoid Int where
30+ neutral = 0
31+
32+instance Group Int where
33+ inverse = (* -1)
34+
35+instance AbelianGroup Int
36+
37+instance Ring Int where
38+ (<.>) = (*)
39+
40+instance RingWithUnity Int where
41+ unity = 1
42+
43+
44+instance Semigroup Float where
45+ (<+>) = (+)
46+
47+instance Monoid Float where
48+ neutral = 0
49+
50+instance Group Float where
51+ inverse = (* -1)
52+
53+instance AbelianGroup Float
54+
55+instance Ring Float where
56+ (<.>) = (*)
57+
58+instance RingWithUnity Float where
59+ unity = 1
60+
61+instance Field Float where
62+ inverseM f _ = 1 / f
63+
64+
65+instance Semigroup Nat where
66+ (<+>) = (+)
67+
68+instance Monoid Nat where
69+ neutral = 0
70+
71+instance Semigroup ZZ where
72+ (<+>) = (+)
73+
74+instance Monoid ZZ where
75+ neutral = 0
76+
77+instance Group ZZ where
78+ inverse = (* -1)
79+
80+instance AbelianGroup ZZ
81+
82+instance Ring ZZ where
83+ (<.>) = (*)
84+
85+instance RingWithUnity ZZ where
86+ unity = 1
87+
88+
89+instance Semigroup a => Semigroup (Complex a) where
90+ (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
91+
92+instance Monoid a => Monoid (Complex a) where
93+ neutral = (neutral :+ neutral)
94+
95+instance Group a => Group (Complex a) where
96+ inverse (r :+ i) = (inverse r :+ inverse i)
97+
98+instance Ring a => AbelianGroup (Complex a) where {}
99+
100+instance Ring a => Ring (Complex a) where
101+ (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)
102+
103+instance RingWithUnity a => RingWithUnity (Complex a) where
104+ unity = (unity :+ neutral)
libs/contrib/Data/Matrix.idr+4−104
@@ -1,6 +1,8 @@
1module Data.Matrix
1module Data.Matrix
2
2
3+import Control.Algebra
4+import Control.Algebra.VectorSpace
3−import Control.Algebra
5+import public Control.Algebra.NumericInstances
4
6
5import Data.Complex
7import Data.Complex
6import Data.ZZ
8import Data.ZZ
@@ -40,8 +42,7 @@ instance Ring a => Ring (Vect n a) where
40instance RingWithUnity a => RingWithUnity (Vect n a) where
42instance RingWithUnity a => RingWithUnity (Vect n a) where
41 unity {n} = replicate n unity
43 unity {n} = replicate n unity
42
44
43−instance Field a => Field (Vect n a) where
45+--instance Field a => Field (Vect n a) where
44− inverseM = map inverseM
45
46
46instance RingWithUnity a => Module a (Vect n a) where
47instance RingWithUnity a => Module a (Vect n a) where
47 (<#>) r v = map (r <.>) v
48 (<#>) r v = map (r <.>) v
@@ -147,104 +148,3 @@ Id {d} = map (\n => basis n) $ allN d
147
148
148-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes
149-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes
149
150
150−-----------------------------------------------------------------------
151−-- Numberic data types as rings
152−-----------------------------------------------------------------------
153−
154−instance Semigroup Integer where
155− (<+>) = (+)
156−
157−instance Monoid Integer where
158− neutral = 0
159−
160−instance Group Integer where
161− inverse = (* -1)
162−
163−instance AbelianGroup Integer
164−
165−instance Ring Integer where
166− (<.>) = (*)
167−
168−instance RingWithUnity Integer where
169− unity = 1
170−
171−
172−instance Semigroup Int where
173− (<+>) = (+)
174−
175−instance Monoid Int where
176− neutral = 0
177−
178−instance Group Int where
179− inverse = (* -1)
180−
181−instance AbelianGroup Int
182−
183−instance Ring Int where
184− (<.>) = (*)
185−
186−instance RingWithUnity Int where
187− unity = 1
188−
189−
190−instance Semigroup Float where
191− (<+>) = (+)
192−
193−instance Monoid Float where
194− neutral = 0
195−
196−instance Group Float where
197− inverse = (* -1)
198−
199−instance AbelianGroup Float
200−
201−instance Ring Float where
202− (<.>) = (*)
203−
204−instance RingWithUnity Float where
205− unity = 1
206−
207−instance Field Float where
208− inverseM f = 1 / f
209−
210−
211−instance Semigroup Nat where
212− (<+>) = (+)
213−
214−instance Monoid Nat where
215− neutral = 0
216−
217−instance Semigroup ZZ where
218− (<+>) = (+)
219−
220−instance Monoid ZZ where
221− neutral = 0
222−
223−instance Group ZZ where
224− inverse = (* -1)
225−
226−instance AbelianGroup ZZ
227−
228−instance Ring ZZ where
229− (<.>) = (*)
230−
231−instance RingWithUnity ZZ where
232− unity = 1
233−
234−
235−instance Semigroup a => Semigroup (Complex a) where
236− (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
237−
238−instance Monoid a => Monoid (Complex a) where
239− neutral = (neutral :+ neutral)
240−
241−instance Group a => Group (Complex a) where
242− inverse (r :+ i) = (inverse r :+ inverse i)
243−
244−instance Ring a => AbelianGroup (Complex a) where {}
245−
246−instance Ring a => Ring (Complex a) where
247− (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)
248−
249−instance RingWithUnity a => RingWithUnity (Complex a) where
250− unity = (unity :+ neutral)
libs/contrib/contrib.ipkg+1
@@ -3,6 +3,7 @@ package contrib
3opts = "--nobasepkgs --total -i ../prelude -i ../base"
3opts = "--nobasepkgs --total -i ../prelude -i ../base"
4modules = Control.Algebra,
4modules = Control.Algebra,
5 Control.Algebra.Lattice, Control.Algebra.VectorSpace,
5 Control.Algebra.Lattice, Control.Algebra.VectorSpace,
6+ Control.Algebra.NumericInstances,
6 Control.Isomorphism.Primitives,
7 Control.Isomorphism.Primitives,
7 Control.WellFounded,
8 Control.WellFounded,
8 Classes.Verified,
9 Classes.Verified,