c9936a6 · Idris-dev · git.iko.soy

CONTRIBUTORS+1

compare with master

unifiedsplit

@@ -34,6 +34,7 @@ Brent Yorgey

34Brian Koropoff

35Brian McKenna

36Bryn Keller

37+Caleb Case

37Calvin Beck

38Calvin Beck

38Carsten König

39Carsten König

39Carter Charbonneau

40Carter Charbonneau

libs/base/Data/Vect.idr+8

@@ -634,6 +634,14 @@ mapElem : {xs : Vect k t} -> {f : t -> u} -> Elem x xs -> Elem (f x) (map f xs)

634mapElem Here = Here

635mapElem (There e) = There (mapElem e)

636

637+||| Remove the element at the given position.

638+|||

639+||| @xs The vector to be removed from

640+||| @p A proof that the element to be removed is in the vector

641+dropElem : (xs : Vect (S k) t) -> (p : Elem x xs) -> Vect k t

642+dropElem (x :: ys) Here = ys

643+dropElem {k = (S k)} (x :: ys) (There later) = x :: dropElem ys later

644+

637-- Some convenience functions for testing lengths

645-- Some convenience functions for testing lengths

638

646

639||| If the given Vect is the required length, return a Vect with that

647||| If the given Vect is the required length, return a Vect with that

libs/base/base.ipkg+39−44

@@ -1,48 +1,43 @@

1package base

2

3opts = "--nobasepkgs --total --no-elim-deprecation-warnings --partial-eval -i ../prelude"

4−modules = System,

5

4

6− Debug.Error, Debug.Trace,

5+modules = Control.Arrow

7−

6+ , Control.Catchable

8− System.Info,

7+ , Control.Category

9−

8+ , Control.IOExcept

10− Language.Reflection.Utils,

9+ , Control.Isomorphism

11−

10+ , Control.Monad.Identity

12− Syntax.PreorderReasoning,

11+ , Control.Monad.Reader

13−

12+ , Control.Monad.RWS

14− Data.Morphisms,

13+ , Control.Monad.State

14+ , Control.Monad.Trans

15+ , Control.Monad.Writer

15− Data.Bits,

16+ , Data.Bits

16− Data.Mod2,

17− Data.Fin,

17+ , Data.Buffer

18− Data.Vect,

19− Data.Vect.Views,

20− Data.Vect.Quantifiers,

21− Data.HVect,

22− Data.Complex,

18+ , Data.Complex

23− Data.Erased,

19+ , Data.Erased

20+ , Data.Fin

21+ , Data.HVect

24− Data.IORef,

22+ , Data.IORef

23+ , Data.List

25− Data.List,

24+ , Data.List.Quantifiers

26− Data.List.Views,

25+ , Data.List.Views

27− Data.List.Quantifiers,

26+ , Data.Mod2

27+ , Data.Morphisms

28− Data.Nat.Views,

28+ , Data.Nat.Views

29− Data.Primitives.Views,

29+ , Data.Primitives.Views

30− Data.String.Views,

31− Data.So,

30+ , Data.So

32− Data.String,

31+ , Data.String

33− Data.Buffer,

32+ , Data.String.Views

34−

33+ , Data.Vect

35− Control.Isomorphism,

34+ , Data.Vect.Quantifiers

36− Control.Monad.Identity,

35+ , Data.Vect.Views

37− Control.Monad.RWS,

36+ , Debug.Error

38− Control.Monad.Trans,

37+ , Debug.Trace

39− Control.Monad.State,

38+ , Language.Reflection.Utils

40− Control.Monad.Writer,

39+ , Syntax.PreorderReasoning

41− Control.Monad.Reader,

40+ , System

42− Control.Category,

41+ , System.Concurrency.Channels

43− Control.Arrow,

44− Control.Catchable,

45− Control.IOExcept,

46−

47− System.Concurrency.Raw,

42+ , System.Concurrency.Raw

48− System.Concurrency.Channels

43+ , System.Info

libs/contrib/Data/String.idr → libs/contrib/Data/String/Extra.idrrenamed+1−1

@@ -1,4 +1,4 @@

1−module Data.String

1+module Data.String.Extra

2

3infixl 5 +>

4infixr 5 <+

libs/contrib/contrib.ipkg+55−43

@@ -1,47 +1,59 @@

1package contrib

2

3opts = "--nobasepkgs --partial-eval --total -i ../prelude -i ../base"

4−modules = CFFI, CFFI.Types, CFFI.Memory,

5

4

5+modules = CFFI

6+ , CFFI.Memory

7+ , CFFI.Types

6− Control.Algebra,

8+ , Control.Algebra

7− Control.Algebra.Lattice, Control.Algebra.VectorSpace,

9+ , Control.Algebra.Lattice

8− Control.Algebra.NumericImplementations,

10+ , Control.Algebra.NumericImplementations

11+ , Control.Algebra.VectorSpace

9− Control.Isomorphism.Primitives,

12+ , Control.Isomorphism.Primitives

10− Control.Partial,

13+ , Control.Partial

11− Control.Pipeline,

14+ , Control.Pipeline

15+ , Control.ST

16+ , Control.ST.Exception

12− Control.ST, Control.ST.ImplicitCall, Control.ST.Exception, Control.ST.Random,

17+ , Control.ST.ImplicitCall

13−

18+ , Control.ST.Random

14− Interfaces.Correlative,

19+ , Data.BoundedList

15− Interfaces.Verified,

20+ , Data.CoList

16−

21+ , Data.Combinators

22+ , Data.Combinators.Applicative

23+ , Data.Combinators.Arrow

24+ , Data.Fin.Extra

17− Data.Fun, Data.Rel,

25+ , Data.Fun

18− Data.Hash,

26+ , Data.Hash

27+ , Data.Heap

28+ , Data.IOArray

29+ , Data.List.Zipper

30+ , Data.Matrix

19− Data.Matrix, Data.Matrix.Algebraic, Data.Matrix.Numeric,

31+ , Data.Matrix.Algebraic

32+ , Data.Matrix.Numeric

33+ , Data.Nat.DivMod

20− Data.Nat.DivMod, Data.Nat.DivMod.IteratedSubtraction,

34+ , Data.Nat.DivMod.IteratedSubtraction

35+ , Data.Pairs.Implicit

36+ , Data.Rel

21− Data.ZZ, Data.Sign,

37+ , Data.Sign

22− Data.BoundedList,

23− Data.Heap,

24− Data.SortedMap, Data.SortedSet,

38+ , Data.SortedMap

39+ , Data.SortedSet

25− Data.CoList, Data.Storable,

40+ , Data.Storable

26− Data.List.Zipper,

41+ , Data.Stream.Extra

27− Data.Pairs.Implicit,

42+ , Data.String.Extra

28− Data.Combinators, Data.Combinators.Applicative, Data.Combinators.Arrow,

43+ , Data.ZZ

29− Data.IOArray,

30−

31− Decidable.Decidable, Decidable.Order,

44+ , Decidable.Decidable

32−

45+ , Decidable.Order

46+ , Interfaces.Correlative

47+ , Interfaces.Verified

48+ , Network.Cgi

49+ , Network.Socket

50+ , Network.Socket.Data

33− Network.Cgi, Network.Socket.Data, Network.Socket.Raw, Network.Socket,

51+ , Network.Socket.Raw

34−

35− System.Concurrency.Process,

52+ , System.Concurrency.Process

36−

53+ , Text.Lexer

54+ , Text.Literate

37− Text.Lexer, Text.Parser,

55+ , Text.Parser

38−

39− Text.PrettyPrint.WL,

40− Text.PrettyPrint.WL.Core,

56+ , Text.PrettyPrint.WL

41− Text.PrettyPrint.WL.Characters,

57+ , Text.PrettyPrint.WL.Characters

42− Text.PrettyPrint.WL.Combinators,

58+ , Text.PrettyPrint.WL.Combinators

43−

59+ , Text.PrettyPrint.WL.Core

44− Text.Literate,

45−

46− Data.Fin.Extra,

47− Data.Stream.Extra

libs/effects/effects.ipkg+11−12

@@ -1,21 +1,20 @@

1package effects

2

3−opts = "--nobasepkgs --partial-eval --typeintype -i ../prelude -i ../base"

3+opts = "--nobasepkgs --partial-eval --typeintype -i ../prelude -i ../base"

4−

5−modules = Effects

6− , Effect.Default

7− , Effect.Monad

8

4

5+modules = Effect.Default

9 , Effect.Exception

6 , Effect.Exception

10 , Effect.File

7 , Effect.File

11− , Effect.State

8+ , Effect.Logging.Category

9+ , Effect.Logging.Default

10+ , Effect.Logging.Level

11+ , Effect.Memory

12+ , Effect.Monad

13+ , Effect.Perf

12 , Effect.Random

14 , Effect.Random

13− , Effect.StdIO

14 , Effect.Select

15 , Effect.Select

15− , Effect.Memory

16+ , Effect.State

17+ , Effect.StdIO

16 , Effect.System

18 , Effect.System

17 , Effect.Trans

19 , Effect.Trans

18− , Effect.Logging.Level

20+ , Effects

19− , Effect.Logging.Default

20− , Effect.Logging.Category

21− , Effect.Perf

libs/prelude/Prelude/Nat.idr+3

@@ -25,6 +25,9 @@ import Prelude.Uninhabited

25

26Uninhabited (Z = S n) where

27 uninhabited Refl impossible

28+

29+Uninhabited (S n = Z) where

30+ uninhabited Refl impossible

28

31

29--------------------------------------------------------------------------------

32--------------------------------------------------------------------------------

30-- Syntactic tests

33-- Syntactic tests

libs/prelude/prelude.ipkg+33−13

@@ -1,17 +1,37 @@

1package prelude

2

3opts = "--nobuiltins --total --no-elim-deprecation-warnings --partial-eval"

4−modules = Builtins, Prelude, IO,

5

4

5+modules = Builtins

6+ , Decidable.Equality

7+ , IO

8+ , Language.Reflection

9+ , Language.Reflection.Elab

10+ , Language.Reflection.Errors

11+ , Prelude

6− Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,

12+ , Prelude.Algebra

13+ , Prelude.Applicative

14+ , Prelude.Basics

15+ , Prelude.Bits

16+ , Prelude.Bool

17+ , Prelude.Cast

18+ , Prelude.Chars

19+ , Prelude.Doubles

20+ , Prelude.Either

21+ , Prelude.File

22+ , Prelude.Foldable

23+ , Prelude.Functor

24+ , Prelude.Interactive

7− Prelude.Interfaces, Prelude.Nat, Prelude.List,

25+ , Prelude.Interfaces

8− Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,

26+ , Prelude.List

27+ , Prelude.Maybe

28+ , Prelude.Monad

29+ , Prelude.Nat

30+ , Prelude.Pairs

31+ , Prelude.Providers

32+ , Prelude.Show

33+ , Prelude.Stream

9− Prelude.Strings, Prelude.Chars, Prelude.Show, Prelude.Functor,

34+ , Prelude.Strings

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

35+ , Prelude.Traversable

11− Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,

36+ , Prelude.Uninhabited

12− Prelude.Interactive, Prelude.File, Prelude.Doubles,

13− Prelude.WellFounded,

37+ , Prelude.WellFounded

14−

15− Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,

16−

17− Decidable.Equality

libs/pruviloj/pruviloj.ipkg+2−1

@@ -1,6 +1,7 @@

1package pruviloj

2

3−opts = "--nobasepkgs --partial-eval -i ../prelude -i ../base"

3+opts = "--nobasepkgs --partial-eval -i ../prelude -i ../base"

4+

4modules = Pruviloj

5modules = Pruviloj

5 , Pruviloj.Core

6 , Pruviloj.Core

6 , Pruviloj.Derive.DecEq

7 , Pruviloj.Derive.DecEq

src/Idris/Core/ProofState.hs−1

@@ -31,7 +31,6 @@ import Util.Pretty hiding (fill)

31import Control.Arrow ((***))

32import Control.Monad.State.Strict

33import Data.List

34−import Debug.Trace

35

34

36data ProofState = PS { thname :: Name,

35data ProofState = PS { thname :: Name,

37 holes :: [Name], -- ^ holes still to be solved

36 holes :: [Name], -- ^ holes still to be solved

src/Idris/Elab/Type.hs−1

@@ -16,7 +16,6 @@ import Idris.ASTUtils

16import Idris.Core.Elaborate hiding (Tactic(..))

17import Idris.Core.Evaluate

18import Idris.Core.TT

19−import Idris.Core.WHNF

20import Idris.Docstrings (Docstring)

19import Idris.Docstrings (Docstring)

21import Idris.Elab.Term

20import Idris.Elab.Term

22import Idris.Elab.Utils

21import Idris.Elab.Utils

src/Idris/Elab/Utils.hs−1

@@ -26,7 +26,6 @@ import Control.Monad.State

26import Data.List

27import qualified Data.Map as Map

28import Data.Maybe

29−import Debug.Trace

30

29

31recheckC = recheckC_borrowing False True []

30recheckC = recheckC_borrowing False True []

32

31

src/Util/DynamicLinker.hs+1−1

@@ -21,7 +21,7 @@ import System.FilePath.Windows ((</>))

21import System.Win32.DLL

22import System.Win32.Types

23#else

24−import Control.Exception (IOException, throwIO, try)

24+import Control.Exception (IOException, try)

25import Foreign.Ptr (FunPtr, nullFunPtr, nullPtr)

26#ifdef linux_HOST_OS

27import Data.Array (bounds, inRange, (!))