git.iko.soy/Idris-dev
on master help sign in
More library rearranging
commit0d4d8db36591af2c8e5a053720f0c02a042c80cc authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 19 Mar 2015, 16:04 (12 years ago) parentf4554eb
7 files changed+14−10
compare with master
unifiedsplit
libs/base/base.ipkg+2−4 libs/base/Control/Isomorphism/Primitives.idr → libs/contrib/Control/Isomorphism/Primitives.idr libs/base/Data/Heap.idr → libs/contrib/Data/Heap.idr libs/contrib/contrib.ipkg+5−3 libs/prelude/Prelude.idr+1−1 libs/base/Providers.idr → libs/prelude/Prelude/Providers.idr+5−1 libs/prelude/prelude.ipkg+1−1
libs/base/base.ipkg+2−4
@@ -7,8 +7,6 @@ modules = System,
77
88 System.Info,
99
10− Providers,
11−
1210 Language.Reflection.Utils,
1311
1412 Syntax.PreorderReasoning,
@@ -19,12 +17,12 @@ modules = System,
1917 Data.BoundedList,
2018 Data.Fin, Data.Vect, Data.VectType,
2119 Data.HVect, Data.Vect.Quantifiers,
22− Data.Floats, Data.Complex, Data.Heap,
20+ Data.Floats, Data.Complex,
2321 Data.Erased,
2422 Data.List, Data.Hash, Data.Matrix,
2523 Data.So,
2624
27− Control.Isomorphism, Control.Isomorphism.Primitives,
25+ Control.Isomorphism,
2826 Control.Monad.Identity,
2927 Control.Monad.RWS,
3028 Control.Monad.Trans,
libs/base/Control/Isomorphism/Primitives.idr → libs/contrib/Control/Isomorphism/Primitives.idrrenamed

The content is the same.

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

The content is the same.

libs/contrib/contrib.ipkg+5−3
@@ -1,11 +1,13 @@
11package contrib
22
3−opts = "--nobaselibs --total -i ../prelude -i ../base"
4−modules = Data.Fun, Data.Rel, Data.Buffer,
3+opts = "--nobasepkgs --total -i ../prelude -i ../base"
4+modules = Control.Isomorphism.Primitives,
5+ Data.Fun, Data.Rel, Data.Buffer,
6+ Data.Heap,
57 Data.SortedMap, Data.SortedSet,
68
79 Decidable.Decidable, Decidable.Order,
810
9− Network.Cgi, Network.Socket
11+ Network.Cgi, Network.Socket,
1012
1113 System.Concurrency.Process
libs/prelude/Prelude.idr+1−1
@@ -23,7 +23,7 @@ import public Prelude.Bits
2323import public Prelude.Uninhabited
2424import public Prelude.Pairs
2525import public Prelude.Stream
26−
26+import public Prelude.Providers
2727import public Decidable.Equality
2828import public Language.Reflection
2929import public Language.Reflection.Errors
libs/base/Providers.idr → libs/prelude/Prelude/Providers.idrrenamed+5−1
@@ -1,4 +1,8 @@
1−module Providers
1+module Prelude.Providers
2+
3+import Prelude.Functor
4+import Prelude.Applicative
5+import Prelude.Monad
26
37||| Type providers must build one of these in an IO computation.
48public
libs/prelude/prelude.ipkg+1−1
@@ -8,7 +8,7 @@ modules = Builtins, Prelude, IO,
88 Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,
99 Prelude.Strings, Prelude.Chars, Prelude.Functor,
1010 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
11− Prelude.Uninhabited, Prelude.Pairs,
11+ Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,
1212
1313 Language.Reflection, Language.Reflection.Errors, Language.Reflection.Tactical,
1414