git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
commitc9936a61f9f62ae6e7445d779cad68817210b329 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 19 Oct 2017, 09:52 (9 years ago) parentff9e9facc7ff93
13 files changed+154−118
compare with master
unifiedsplit
CONTRIBUTORS+1 libs/base/Data/Vect.idr+8 libs/base/base.ipkg+39−44 libs/contrib/Data/String.idr → libs/contrib/Data/String/Extra.idr+1−1 libs/contrib/contrib.ipkg+55−43 libs/effects/effects.ipkg+11−12 libs/prelude/Prelude/Nat.idr+3 libs/prelude/prelude.ipkg+33−13 libs/pruviloj/pruviloj.ipkg+2−1 src/Idris/Core/ProofState.hs−1 src/Idris/Elab/Type.hs−1 src/Idris/Elab/Utils.hs−1 src/Util/DynamicLinker.hs+1−1
CONTRIBUTORS+1
@@ -34,6 +34,7 @@ Brent Yorgey
3434Brian Koropoff
3535Brian McKenna
3636Bryn Keller
37+Caleb Case
3738Calvin Beck
3839Carsten König
3940Carter 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)
634634mapElem Here = Here
635635mapElem (There e) = There (mapElem e)
636636
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+
637645-- Some convenience functions for testing lengths
638646
639647||| If the given Vect is the required length, return a Vect with that
libs/base/base.ipkg+39−44
@@ -1,48 +1,43 @@
11package base
22
33opts = "--nobasepkgs --total --no-elim-deprecation-warnings --partial-eval -i ../prelude"
4−modules = System,
54
6− Debug.Error, Debug.Trace,
7−
8− System.Info,
9−
10− Language.Reflection.Utils,
11−
12− Syntax.PreorderReasoning,
13−
14− Data.Morphisms,
15− Data.Bits,
16− Data.Mod2,
17− Data.Fin,
18− Data.Vect,
19− Data.Vect.Views,
20− Data.Vect.Quantifiers,
21− Data.HVect,
22− Data.Complex,
23− Data.Erased,
24− Data.IORef,
25− Data.List,
26− Data.List.Views,
27− Data.List.Quantifiers,
28− Data.Nat.Views,
29− Data.Primitives.Views,
30− Data.String.Views,
31− Data.So,
32− Data.String,
33− Data.Buffer,
34−
35− Control.Isomorphism,
36− Control.Monad.Identity,
37− Control.Monad.RWS,
38− Control.Monad.Trans,
39− Control.Monad.State,
40− Control.Monad.Writer,
41− Control.Monad.Reader,
42− Control.Category,
43− Control.Arrow,
44− Control.Catchable,
45− Control.IOExcept,
46−
47− System.Concurrency.Raw,
48− System.Concurrency.Channels
5+modules = Control.Arrow
6+ , Control.Catchable
7+ , Control.Category
8+ , Control.IOExcept
9+ , Control.Isomorphism
10+ , Control.Monad.Identity
11+ , Control.Monad.Reader
12+ , Control.Monad.RWS
13+ , Control.Monad.State
14+ , Control.Monad.Trans
15+ , Control.Monad.Writer
16+ , Data.Bits
17+ , Data.Buffer
18+ , Data.Complex
19+ , Data.Erased
20+ , Data.Fin
21+ , Data.HVect
22+ , Data.IORef
23+ , Data.List
24+ , Data.List.Quantifiers
25+ , Data.List.Views
26+ , Data.Mod2
27+ , Data.Morphisms
28+ , Data.Nat.Views
29+ , Data.Primitives.Views
30+ , Data.So
31+ , Data.String
32+ , Data.String.Views
33+ , Data.Vect
34+ , Data.Vect.Quantifiers
35+ , Data.Vect.Views
36+ , Debug.Error
37+ , Debug.Trace
38+ , Language.Reflection.Utils
39+ , Syntax.PreorderReasoning
40+ , System
41+ , System.Concurrency.Channels
42+ , System.Concurrency.Raw
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
22
33infixl 5 +>
44infixr 5 <+
libs/contrib/contrib.ipkg+55−43
@@ -1,47 +1,59 @@
11package contrib
22
33opts = "--nobasepkgs --partial-eval --total -i ../prelude -i ../base"
4−modules = CFFI, CFFI.Types, CFFI.Memory,
54
6− Control.Algebra,
7− Control.Algebra.Lattice, Control.Algebra.VectorSpace,
8− Control.Algebra.NumericImplementations,
9− Control.Isomorphism.Primitives,
10− Control.Partial,
11− Control.Pipeline,
12− Control.ST, Control.ST.ImplicitCall, Control.ST.Exception, Control.ST.Random,
13−
14− Interfaces.Correlative,
15− Interfaces.Verified,
16−
17− Data.Fun, Data.Rel,
18− Data.Hash,
19− Data.Matrix, Data.Matrix.Algebraic, Data.Matrix.Numeric,
20− Data.Nat.DivMod, Data.Nat.DivMod.IteratedSubtraction,
21− Data.ZZ, Data.Sign,
22− Data.BoundedList,
23− Data.Heap,
24− Data.SortedMap, Data.SortedSet,
25− Data.CoList, Data.Storable,
26− Data.List.Zipper,
27− Data.Pairs.Implicit,
28− Data.Combinators, Data.Combinators.Applicative, Data.Combinators.Arrow,
29− Data.IOArray,
30−
31− Decidable.Decidable, Decidable.Order,
32−
33− Network.Cgi, Network.Socket.Data, Network.Socket.Raw, Network.Socket,
34−
35− System.Concurrency.Process,
36−
37− Text.Lexer, Text.Parser,
38−
39− Text.PrettyPrint.WL,
40− Text.PrettyPrint.WL.Core,
41− Text.PrettyPrint.WL.Characters,
42− Text.PrettyPrint.WL.Combinators,
43−
44− Text.Literate,
45−
46− Data.Fin.Extra,
47− Data.Stream.Extra
5+modules = CFFI
6+ , CFFI.Memory
7+ , CFFI.Types
8+ , Control.Algebra
9+ , Control.Algebra.Lattice
10+ , Control.Algebra.NumericImplementations
11+ , Control.Algebra.VectorSpace
12+ , Control.Isomorphism.Primitives
13+ , Control.Partial
14+ , Control.Pipeline
15+ , Control.ST
16+ , Control.ST.Exception
17+ , Control.ST.ImplicitCall
18+ , Control.ST.Random
19+ , Data.BoundedList
20+ , Data.CoList
21+ , Data.Combinators
22+ , Data.Combinators.Applicative
23+ , Data.Combinators.Arrow
24+ , Data.Fin.Extra
25+ , Data.Fun
26+ , Data.Hash
27+ , Data.Heap
28+ , Data.IOArray
29+ , Data.List.Zipper
30+ , Data.Matrix
31+ , Data.Matrix.Algebraic
32+ , Data.Matrix.Numeric
33+ , Data.Nat.DivMod
34+ , Data.Nat.DivMod.IteratedSubtraction
35+ , Data.Pairs.Implicit
36+ , Data.Rel
37+ , Data.Sign
38+ , Data.SortedMap
39+ , Data.SortedSet
40+ , Data.Storable
41+ , Data.Stream.Extra
42+ , Data.String.Extra
43+ , Data.ZZ
44+ , Decidable.Decidable
45+ , Decidable.Order
46+ , Interfaces.Correlative
47+ , Interfaces.Verified
48+ , Network.Cgi
49+ , Network.Socket
50+ , Network.Socket.Data
51+ , Network.Socket.Raw
52+ , System.Concurrency.Process
53+ , Text.Lexer
54+ , Text.Literate
55+ , Text.Parser
56+ , Text.PrettyPrint.WL
57+ , Text.PrettyPrint.WL.Characters
58+ , Text.PrettyPrint.WL.Combinators
59+ , Text.PrettyPrint.WL.Core
libs/effects/effects.ipkg+11−12
@@ -1,21 +1,20 @@
11package effects
22
3−opts = "--nobasepkgs --partial-eval --typeintype -i ../prelude -i ../base"
4−
5−modules = Effects
6− , Effect.Default
7− , Effect.Monad
3+opts = "--nobasepkgs --partial-eval --typeintype -i ../prelude -i ../base"
84
5+modules = Effect.Default
96 , Effect.Exception
107 , 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
1214 , Effect.Random
13− , Effect.StdIO
1415 , Effect.Select
15− , Effect.Memory
16+ , Effect.State
17+ , Effect.StdIO
1618 , Effect.System
1719 , Effect.Trans
18− , Effect.Logging.Level
19− , Effect.Logging.Default
20− , Effect.Logging.Category
21− , Effect.Perf
20+ , Effects
libs/prelude/Prelude/Nat.idr+3
@@ -25,6 +25,9 @@ import Prelude.Uninhabited
2525
2626Uninhabited (Z = S n) where
2727 uninhabited Refl impossible
28+
29+Uninhabited (S n = Z) where
30+ uninhabited Refl impossible
2831
2932--------------------------------------------------------------------------------
3033-- Syntactic tests
libs/prelude/prelude.ipkg+33−13
@@ -1,17 +1,37 @@
11package prelude
22
33opts = "--nobuiltins --total --no-elim-deprecation-warnings --partial-eval"
4−modules = Builtins, Prelude, IO,
54
6− Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,
7− Prelude.Interfaces, Prelude.Nat, Prelude.List,
8− Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,
9− Prelude.Strings, Prelude.Chars, Prelude.Show, Prelude.Functor,
10− Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
11− Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,
12− Prelude.Interactive, Prelude.File, Prelude.Doubles,
13− Prelude.WellFounded,
14−
15− Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,
16−
17− Decidable.Equality
5+modules = Builtins
6+ , Decidable.Equality
7+ , IO
8+ , Language.Reflection
9+ , Language.Reflection.Elab
10+ , Language.Reflection.Errors
11+ , Prelude
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
25+ , Prelude.Interfaces
26+ , Prelude.List
27+ , Prelude.Maybe
28+ , Prelude.Monad
29+ , Prelude.Nat
30+ , Prelude.Pairs
31+ , Prelude.Providers
32+ , Prelude.Show
33+ , Prelude.Stream
34+ , Prelude.Strings
35+ , Prelude.Traversable
36+ , Prelude.Uninhabited
37+ , Prelude.WellFounded
libs/pruviloj/pruviloj.ipkg+2−1
@@ -1,6 +1,7 @@
11package pruviloj
22
3−opts = "--nobasepkgs --partial-eval -i ../prelude -i ../base"
3+opts = "--nobasepkgs --partial-eval -i ../prelude -i ../base"
4+
45modules = Pruviloj
56 , Pruviloj.Core
67 , Pruviloj.Derive.DecEq
src/Idris/Core/ProofState.hs−1
@@ -31,7 +31,6 @@ import Util.Pretty hiding (fill)
3131import Control.Arrow ((***))
3232import Control.Monad.State.Strict
3333import Data.List
34−import Debug.Trace
3534
3635data ProofState = PS { thname :: Name,
3736 holes :: [Name], -- ^ holes still to be solved
src/Idris/Elab/Type.hs−1
@@ -16,7 +16,6 @@ import Idris.ASTUtils
1616import Idris.Core.Elaborate hiding (Tactic(..))
1717import Idris.Core.Evaluate
1818import Idris.Core.TT
19−import Idris.Core.WHNF
2019import Idris.Docstrings (Docstring)
2120import Idris.Elab.Term
2221import Idris.Elab.Utils
src/Idris/Elab/Utils.hs−1
@@ -26,7 +26,6 @@ import Control.Monad.State
2626import Data.List
2727import qualified Data.Map as Map
2828import Data.Maybe
29−import Debug.Trace
3029
3130recheckC = recheckC_borrowing False True []
3231
src/Util/DynamicLinker.hs+1−1
@@ -21,7 +21,7 @@ import System.FilePath.Windows ((</>))
2121import System.Win32.DLL
2222import System.Win32.Types
2323#else
24−import Control.Exception (IOException, throwIO, try)
24+import Control.Exception (IOException, try)
2525import Foreign.Ptr (FunPtr, nullFunPtr, nullPtr)
2626#ifdef linux_HOST_OS
2727import Data.Array (bounds, inRange, (!))