ba6f0ef · Idris-dev · git.iko.soy

idris.cabal+6−1

compare with master

unifiedsplit

@@ -68,6 +68,11 @@ Extra-source-files:

68

69 libs/Makefile

70

71+ libs/prelude/prelude.ipkg

72+ libs/prelude/Prelude/*.idr

73+ libs/prelude/Makefile

74+ libs/prelude/*.idr

75+

71 libs/base/base.ipkg

76 libs/base/base.ipkg

72 libs/base/*.idr

77 libs/base/*.idr

73 libs/base/Control/*.idr

78 libs/base/Control/*.idr

@@ -80,9 +85,9 @@ Extra-source-files:

80 libs/base/Language/Reflection/*.idr

85 libs/base/Language/Reflection/*.idr

81 libs/base/Makefile

86 libs/base/Makefile

82 libs/base/Network/*.idr

87 libs/base/Network/*.idr

83− libs/base/Prelude/*.idr

84 libs/base/System/Concurrency/*.idr

88 libs/base/System/Concurrency/*.idr

85

89

90+

86 libs/effects/Makefile

91 libs/effects/Makefile

87 libs/effects/effects.ipkg

92 libs/effects/effects.ipkg

88 libs/effects/Effect/*.idr

93 libs/effects/Effect/*.idr

libs/Makefile+3

@@ -1,15 +1,18 @@

1build: .PHONY

2+ make -C prelude build

2 make -C base build

3 make -C base build

3 make -C effects build

4 make -C effects build

4 make -C javascript build

5 make -C javascript build

5

6

7

7install: .PHONY

8install: .PHONY

9+ make -C prelude install

8 make -C base install

10 make -C base install

9 make -C effects install

11 make -C effects install

10 make -C javascript install

12 make -C javascript install

11

13

12clean: .PHONY

14clean: .PHONY

15+ make -C prelude clean

13 make -C base clean

16 make -C base clean

14 make -C effects clean

17 make -C effects clean

15 make -C javascript clean

18 make -C javascript clean

libs/base/Prelude/Heap.idr → libs/base/Data/Heap.idrrenamed+2−9

@@ -3,14 +3,7 @@

3-- ``Fun with binary heap trees'', Chris Okasaki, Fun of programming, 2003.

4--------------------------------------------------------------------------------

5

6−module Prelude.Heap

6+module Data.Heap

7−

8−import Builtins

9−

10−import Prelude

11−import Prelude.Algebra

12−import Prelude.List

13−import Prelude.Nat

14

7

15%access public

8%access public

16

9

@@ -112,7 +105,7 @@ fromList : Ord a => List a -> MaxiphobicHeap a

112fromList = foldr insert empty

105fromList = foldr insert empty

113

106

114sort : Ord a => List a -> List a

107sort : Ord a => List a -> List a

115−sort = Prelude.Heap.toList . Prelude.Heap.fromList

108+sort = Heap.toList . Heap.fromList

116

109

117--------------------------------------------------------------------------------

110--------------------------------------------------------------------------------

118-- Class instances

111-- Class instances

libs/base/base.ipkg+3−9

@@ -1,13 +1,7 @@

1package base

2

3−opts = "--noprelude --total"

3+opts = "--total"

4−modules = Builtins, Prelude, IO, System,

4+modules = System,

5−

6− Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,

7− Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,

8− Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,

9− Prelude.Heap, Prelude.Functor, Prelude.Foldable,

10− Prelude.Traversable, Prelude.Bits, Prelude.Stream,

11

5

12 Network.Cgi,

6 Network.Cgi,

13 Debug.Trace,

7 Debug.Trace,

@@ -27,7 +21,7 @@ modules = Builtins, Prelude, IO, System,

27 Data.ZZ, Data.Sign,

21 Data.ZZ, Data.Sign,

28 Data.SortedMap, Data.SortedSet, Data.BoundedList,

22 Data.SortedMap, Data.SortedSet, Data.BoundedList,

29 Data.Vect, Data.HVect, Data.Vect.Quantifiers,

23 Data.Vect, Data.HVect, Data.Vect.Quantifiers,

30− Data.Floats, Data.Complex,

24+ Data.Floats, Data.Complex, Data.Heap,

31

25

32 Control.Monad.Identity,

26 Control.Monad.Identity,

33 Control.Monad.RWS,

27 Control.Monad.RWS,

libs/base/Builtins.idr → libs/prelude/Builtins.idrrenamed

The content is the same.

libs/base/IO.idr → libs/prelude/IO.idrrenamed

The content is the same.

libs/base/Prelude.idr → libs/prelude/Prelude.idrrenamed

The content is the same.

libs/base/Prelude/Algebra.idr → libs/prelude/Prelude/Algebra.idrrenamed

The content is the same.

libs/base/Prelude/Applicative.idr → libs/prelude/Prelude/Applicative.idrrenamed

The content is the same.

libs/base/Prelude/Bits.idr → libs/prelude/Prelude/Bits.idrrenamed

The content is the same.

libs/base/Prelude/Cast.idr → libs/prelude/Prelude/Cast.idrrenamed

The content is the same.

libs/base/Prelude/Chars.idr → libs/prelude/Prelude/Chars.idrrenamed

The content is the same.

libs/base/Prelude/Either.idr → libs/prelude/Prelude/Either.idrrenamed

The content is the same.

libs/base/Prelude/Fin.idr → libs/prelude/Prelude/Fin.idrrenamed

The content is the same.

libs/base/Prelude/Foldable.idr → libs/prelude/Prelude/Foldable.idrrenamed

The content is the same.

libs/base/Prelude/Functor.idr → libs/prelude/Prelude/Functor.idrrenamed

The content is the same.

libs/base/Prelude/List.idr → libs/prelude/Prelude/List.idrrenamed

The content is the same.

libs/base/Prelude/Maybe.idr → libs/prelude/Prelude/Maybe.idrrenamed

The content is the same.

libs/base/Prelude/Monad.idr → libs/prelude/Prelude/Monad.idrrenamed

The content is the same.

libs/base/Prelude/Nat.idr → libs/prelude/Prelude/Nat.idrrenamed

The content is the same.

libs/base/Prelude/Stream.idr → libs/prelude/Prelude/Stream.idrrenamed

The content is the same.

libs/base/Prelude/Strings.idr → libs/prelude/Prelude/Strings.idrrenamed

The content is the same.

libs/base/Prelude/Traversable.idr → libs/prelude/Prelude/Traversable.idrrenamed

The content is the same.

libs/base/Prelude/Vect.idr → libs/prelude/Prelude/Vect.idrrenamed

The content is the same.

libs/prelude/prelude.ipkgnew file+11

@@ -0,0 +1,11 @@

1+package prelude

2+

3+opts = "--noprelude --total"

4+modules = Builtins, Prelude, IO,

5+

6+ Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,

7+ Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,

8+ Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,

9+ Prelude.Functor, Prelude.Foldable,

10+ Prelude.Traversable, Prelude.Bits, Prelude.Stream

11+

src/Idris/REPL.hs+1

@@ -1125,6 +1125,7 @@ idrisMain opts =

1125 setImportDirs importdirs

1126

1127 addPkgDir "base"

1128+ addPkgDir "prelude"

1128 mapM_ addPkgDir pkgdirs

1129 mapM_ addPkgDir pkgdirs

1129 elabPrims

1130 elabPrims

1130 when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"

1131 when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"