git.iko.soy/Idris-dev
on master help sign in
Initial reorganization into contrib
commitdb5b385e13075c3678f86bba9285a4be529d7ce3 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 17 Mar 2015, 00:17 (12 years ago) parent6d768bb
14 files changed+78−13
compare with master
unifiedsplit
libs/Makefile+10−5 libs/base/base.ipkg+5−8 libs/base/Data/Buffer.idr → libs/contrib/Data/Buffer.idr libs/base/Data/Fun.idr → libs/contrib/Data/Fun.idr libs/base/Data/Rel.idr → libs/contrib/Data/Rel.idr libs/base/Data/SortedMap.idr → libs/contrib/Data/SortedMap.idr libs/contrib/Data/SortedSet.idr+28 libs/base/Decidable/Decidable.idr → libs/contrib/Decidable/Decidable.idr libs/base/Decidable/Order.idr → libs/contrib/Decidable/Order.idr libs/contrib/Makefile+24 libs/base/Network/Cgi.idr → libs/contrib/Network/Cgi.idr libs/base/System/Concurrency/Process.idr → libs/contrib/System/Concurrency/Process.idr libs/base/System/Concurrency/Raw.idr → libs/contrib/System/Concurrency/Raw.idr libs/contrib/contrib.ipkg+11
libs/Makefile+10−5
@@ -1,28 +1,33 @@
11build:
22 $(MAKE) -C prelude build
33 $(MAKE) -C base build
4+ $(MAKE) -C contrib build
45 $(MAKE) -C effects build
56
67
78install:
89 $(MAKE) -C prelude install
910 $(MAKE) -C base install
11+ $(MAKE) -C contrib install
1012 $(MAKE) -C effects install
1113
1214clean:
1315 $(MAKE) -C prelude clean
1416 $(MAKE) -C base clean
17+ $(MAKE) -C contrib clean
1518 $(MAKE) -C effects clean
1619
1720doc:
18− $(MAKE) -C prelude doc
19− $(MAKE) -C base doc
20− $(MAKE) -C effects doc
21+ $(MAKE) -C prelude doc
22+ $(MAKE) -C base doc
23+ $(MAKE) -C contrib doc
24+ $(MAKE) -C effects doc
2125
2226doc_clean:
2327 $(MAKE) -C prelude doc_clean
24− $(MAKE) -C base doc_clean
25− $(MAKE) -C effects doc_clean
28+ $(MAKE) -C base doc_clean
29+ $(MAKE) -C contrib doc_clean
30+ $(MAKE) -C effects doc_clean
2631
2732
2833.PHONY: build install clean doc doc_clean
libs/base/base.ipkg+5−8
@@ -3,13 +3,10 @@ package base
33opts = "--nobasepkgs --total -i ../prelude"
44modules = System,
55
6− Network.Cgi, Network.Socket,
6+ Network.Socket,
77 Debug.Error, Debug.Trace,
88
99 System.Info,
10− System.Concurrency.Raw, System.Concurrency.Process,
11−
12− Decidable.Decidable, Decidable.Order,
1310
1411 Providers,
1512
@@ -20,11 +17,11 @@ modules = System,
2017 Data.Morphisms,
2118 Data.Bits, Data.Mod2,
2219 Data.ZZ, Data.Sign,
23− Data.SortedMap, Data.SortedSet, Data.BoundedList,
24− Data.Fin, Data.Vect, Data.VectType,
20+ Data.BoundedList,
21+ Data.Fin, Data.Vect, Data.VectType,
2522 Data.HVect, Data.Vect.Quantifiers,
26− Data.Floats, Data.Complex, Data.Heap, Data.Fun,
27− Data.Rel, Data.Buffer, Data.Erased,
23+ Data.Floats, Data.Complex, Data.Heap,
24+ Data.Erased,
2825 Data.List, Data.Hash, Data.Matrix,
2926 Data.So,
3027
libs/base/Data/Buffer.idr → libs/contrib/Data/Buffer.idrrenamed

The content is the same.

libs/base/Data/Fun.idr → libs/contrib/Data/Fun.idrrenamed

The content is the same.

libs/base/Data/Rel.idr → libs/contrib/Data/Rel.idrrenamed

The content is the same.

libs/base/Data/SortedMap.idr → libs/contrib/Data/SortedMap.idrrenamed

The content is the same.

libs/contrib/Data/SortedSet.idrnew file+28
@@ -0,0 +1,28 @@
1+module Data.SortedSet
2+
3+import Data.SortedMap
4+
5+-- TODO: add intersection, union, difference
6+
7+data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())
8+
9+empty : SortedSet k
10+empty = SetWrapper Data.SortedMap.empty
11+
12+insert : Ord k => k -> SortedSet k -> SortedSet k
13+insert k (SetWrapper m) = SetWrapper (Data.SortedMap.insert k () m)
14+
15+delete : Ord k => k -> SortedSet k -> SortedSet k
16+delete k (SetWrapper m) = SetWrapper (Data.SortedMap.delete k m)
17+
18+contains : Ord k => k -> SortedSet k -> Bool
19+contains k (SetWrapper m) = isJust (Data.SortedMap.lookup k m)
20+
21+fromList : Ord k => List k -> SortedSet k
22+fromList l = SetWrapper (Data.SortedMap.fromList (map (\i => (i, ())) l))
23+
24+toList : SortedSet k -> List k
25+toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)
26+
27+instance Foldable SortedSet where
28+ foldr f e xs = foldr f e (Data.SortedSet.toList xs)
libs/base/Decidable/Decidable.idr → libs/contrib/Decidable/Decidable.idrrenamed

The content is the same.

libs/base/Decidable/Order.idr → libs/contrib/Decidable/Order.idrrenamed

The content is the same.

libs/contrib/Makefilenew file+24
@@ -0,0 +1,24 @@
1+IDRIS := idris
2+PKG := contrib
3+
4+build:
5+ $(IDRIS) --build ${PKG}.ipkg
6+
7+install:
8+ $(IDRIS) --install ${PKG}.ipkg
9+
10+clean:
11+ $(IDRIS) --clean ${PKG}.ipkg
12+
13+rebuild: clean build
14+
15+doc:
16+ ${IDRIS} --mkdoc ${PKG}.ipkg
17+
18+doc_clean:
19+ rm -rf ${PKG}_doc
20+
21+linecount:
22+ find . -name '*.idr' | xargs wc -l
23+
24+.PHONY: build install clean rebuild linecount
libs/base/Network/Cgi.idr → libs/contrib/Network/Cgi.idrrenamed

The content is the same.

libs/base/System/Concurrency/Process.idr → libs/contrib/System/Concurrency/Process.idrrenamed

The content is the same.

libs/base/System/Concurrency/Raw.idr → libs/contrib/System/Concurrency/Raw.idrrenamed

The content is the same.

libs/contrib/contrib.ipkgnew file+11
@@ -0,0 +1,11 @@
1+package contrib
2+
3+opts = "--nobaselibs --total -i ../prelude -i ../base"
4+modules = Data.Fun, Data.Rel, Data.Buffer,
5+ Data.SortedMap, Data.SortedSet,
6+
7+ Decidable.Decidable, Decidable.Order,
8+
9+ Network.Cgi,
10+
11+ System.Concurrency.Process, System.Concurrency.Raw