ba6f0ef · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Separate base into base and prelude

Everything in prelude will be imported automatically, unless given the --noprelude option. The idea is that what counts as "Idris" is the compiler plus the Standard Prelude. Other libraries (base, effects, etc) are still part of the distribution, but not necessarily standard.

commitba6f0ef10086f1d316dedc11164330fecb979d01 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 21 Nov 2013, 13:40 (13 years ago) parent873e824

26 files changed+26−19

compare with master

unifiedsplit

idris.cabal+6−1

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

6868

6969 libs/Makefile

7070

71+ libs/prelude/prelude.ipkg

72+ libs/prelude/Prelude/*.idr

73+ libs/prelude/Makefile

74+ libs/prelude/*.idr

75+

7176 libs/base/base.ipkg

7277 libs/base/*.idr

7378 libs/base/Control/*.idr

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

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

8186 libs/base/Makefile

8287 libs/base/Network/*.idr

83− libs/base/Prelude/*.idr

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

8589

90+

8691 libs/effects/Makefile

8792 libs/effects/effects.ipkg

8893 libs/effects/Effect/*.idr

libs/Makefile+3

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

11build: .PHONY

2+ make -C prelude build

23 make -C base build

34 make -C effects build

45 make -C javascript build

78install: .PHONY

9+ make -C prelude install

810 make -C base install

911 make -C effects install

1012 make -C javascript install

1113

1214clean: .PHONY

15+ make -C prelude clean

1316 make -C base clean

1417 make -C effects clean

1518 make -C javascript clean

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

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

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

44--------------------------------------------------------------------------------

6−module Prelude.Heap

7−

8−import Builtins

9−

10−import Prelude

11−import Prelude.Algebra

12−import Prelude.List

13−import Prelude.Nat

6+module Data.Heap

147

158%access public

169

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

112105fromList = foldr insert empty

113106

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

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

108+sort = Heap.toList . Heap.fromList

116109

117110--------------------------------------------------------------------------------

118111-- Class instances

libs/base/base.ipkg+3−9

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

11package base

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

4−modules = Builtins, Prelude, IO, 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,

3+opts = "--total"

4+modules = System,

115

126 Network.Cgi,

137 Debug.Trace,

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

2721 Data.ZZ, Data.Sign,

2822 Data.SortedMap, Data.SortedSet, Data.BoundedList,

2923 Data.Vect, Data.HVect, Data.Vect.Quantifiers,

30− Data.Floats, Data.Complex,

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

3125

3226 Control.Monad.Identity,

3327 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

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

4+modules = Builtins, Prelude, IO,

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 =

11251125 setImportDirs importdirs

11261126

11271127 addPkgDir "base"

1128+ addPkgDir "prelude"

11281129 mapM_ addPkgDir pkgdirs

11291130 elabPrims

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