db5b385 · Idris-dev · git.iko.soy

libs/Makefile+10−5

compare with master

unifiedsplit

@@ -1,28 +1,33 @@

1build:

2 $(MAKE) -C prelude build

3 $(MAKE) -C base build

4+ $(MAKE) -C contrib build

4 $(MAKE) -C effects build

5 $(MAKE) -C effects build

5

6

7

7install:

8install:

8 $(MAKE) -C prelude install

9 $(MAKE) -C prelude install

9 $(MAKE) -C base install

10 $(MAKE) -C base install

11+ $(MAKE) -C contrib install

10 $(MAKE) -C effects install

12 $(MAKE) -C effects install

11

13

12clean:

14clean:

13 $(MAKE) -C prelude clean

15 $(MAKE) -C prelude clean

14 $(MAKE) -C base clean

16 $(MAKE) -C base clean

17+ $(MAKE) -C contrib clean

15 $(MAKE) -C effects clean

18 $(MAKE) -C effects clean

16

19

17doc:

20doc:

18− $(MAKE) -C prelude doc

21+ $(MAKE) -C prelude doc

19− $(MAKE) -C base doc

22+ $(MAKE) -C base doc

23+ $(MAKE) -C contrib doc

20− $(MAKE) -C effects doc

24+ $(MAKE) -C effects doc

21

25

22doc_clean:

26doc_clean:

23 $(MAKE) -C prelude doc_clean

27 $(MAKE) -C prelude doc_clean

24− $(MAKE) -C base doc_clean

28+ $(MAKE) -C base doc_clean

29+ $(MAKE) -C contrib doc_clean

25− $(MAKE) -C effects doc_clean

30+ $(MAKE) -C effects doc_clean

26

31

27

32

28.PHONY: build install clean doc doc_clean

33.PHONY: build install clean doc doc_clean

libs/base/base.ipkg+5−8

@@ -3,13 +3,10 @@ package base

3opts = "--nobasepkgs --total -i ../prelude"

4modules = System,

5

6− Network.Cgi, Network.Socket,

6+ Network.Socket,

7 Debug.Error, Debug.Trace,

8

9 System.Info,

10− System.Concurrency.Raw, System.Concurrency.Process,

11−

12− Decidable.Decidable, Decidable.Order,

13

10

14 Providers,

11 Providers,

15

12

@@ -20,11 +17,11 @@ modules = System,

20 Data.Morphisms,

17 Data.Morphisms,

21 Data.Bits, Data.Mod2,

18 Data.Bits, Data.Mod2,

22 Data.ZZ, Data.Sign,

19 Data.ZZ, Data.Sign,

23− Data.SortedMap, Data.SortedSet, Data.BoundedList,

20+ Data.BoundedList,

24− Data.Fin, Data.Vect, Data.VectType,

21+ Data.Fin, Data.Vect, Data.VectType,

25 Data.HVect, Data.Vect.Quantifiers,

22 Data.HVect, Data.Vect.Quantifiers,

26− Data.Floats, Data.Complex, Data.Heap, Data.Fun,

23+ Data.Floats, Data.Complex, Data.Heap,

27− Data.Rel, Data.Buffer, Data.Erased,

24+ Data.Erased,

28 Data.List, Data.Hash, Data.Matrix,

25 Data.List, Data.Hash, Data.Matrix,

29 Data.So,

26 Data.So,

30

27

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