a14e4ed · Idris-dev · git.iko.soy

CHANGELOG+12

compare with master

unifiedsplit

@@ -1,3 +1,15 @@

1+New in 0.11:

2+============

3+

4+* The export rules have been simplified. Now:

5+ - 'private' means that the definition is not exported at all

6+ - 'export' means that the top level type is exported, but not the

7+ definition. In the case of 'data', this means the type constructor is

8+ exported but not the data constructors.

9+ - 'public export' means that the entire definition is exported.

10+* By default, names are 'private'. This can be altered with an %access

11+ directive as before.

12+

1New in 0.10:

13New in 0.10:

2============

14============

3

15

libs/base/Control/Catchable.idr+2

@@ -2,6 +2,8 @@ module Control.Catchable

2

3import Control.IOExcept

4

5+%access public

6+

5interface Catchable (m : Type -> Type) t where

7interface Catchable (m : Type -> Type) t where

6 throw : t -> m a

8 throw : t -> m a

7 catch : m a -> (t -> m a) -> m a

9 catch : m a -> (t -> m a) -> m a

libs/base/Control/IOExcept.idr+2

@@ -1,5 +1,7 @@

1module Control.IOExcept

2

3+%access public

4+

3-- An IO monad with exception handling

5-- An IO monad with exception handling

4

6

5record IOExcept' (f:FFI) err a where

7record IOExcept' (f:FFI) err a where

libs/base/Control/Isomorphism.idr+1

@@ -4,6 +4,7 @@ import Syntax.PreorderReasoning

4import Data.Fin

5

6%default total

7+%access public

7

8

8||| An isomorphism between two types

9||| An isomorphism between two types

9data Iso : Type -> Type -> Type where

10data Iso : Type -> Type -> Type where

libs/base/Control/Monad/Identity.idr+2

@@ -1,5 +1,7 @@

1module Control.Monad.Identity

2

3+%access public

4+

3public record Identity (a : Type) where

5public record Identity (a : Type) where

4 constructor Id

6 constructor Id

5 runIdentity : a

7 runIdentity : a

libs/base/Control/Monad/Trans.idr+2

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

1module Control.Monad.Trans

2

3+%access public

4+

3interface MonadTrans (t : (Type -> Type) -> Type -> Type) where

5interface MonadTrans (t : (Type -> Type) -> Type -> Type) where

4 lift : Monad m => m a -> t m a

6 lift : Monad m => m a -> t m a

libs/base/Data/Complex.idr+2

@@ -5,6 +5,8 @@

5

6module Data.Complex

7

8+%access public

9+

8------------------------------ Rectangular form

10------------------------------ Rectangular form

9

11

10infix 6 :+

12infix 6 :+

libs/base/Data/List/Quantifiers.idr+2

@@ -2,6 +2,8 @@ module Data.List.Quantifiers

2

3import Data.List

4

5+%access public

6+

5||| A proof that some element of a list satisfies some property

7||| A proof that some element of a list satisfies some property

6|||

8|||

7||| @ P the property to be satsified

9||| @ P the property to be satsified

libs/base/Data/So.idr+1

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

1module Data.So

2

3%default total

4+%access public

4

5

5||| Ensure that some run-time Boolean test has been performed.

6||| Ensure that some run-time Boolean test has been performed.

6|||

7|||

libs/base/Data/Vect/Quantifiers.idr+2

@@ -2,6 +2,8 @@ module Data.Vect.Quantifiers

2

3import Data.Vect

4

5+%access public

6+

5||| A proof that some element of a vector satisfies some property

7||| A proof that some element of a vector satisfies some property

6|||

8|||

7||| @ P the property to be satsified

9||| @ P the property to be satsified

libs/base/Debug/Error.idr+1−1

@@ -7,7 +7,7 @@ import System

7|||

8||| @ loc The source location to display for the error

9||| @ message The error to print

10−partial

10+partial abstract

11error : {default (%runElab sourceLocation) loc : SourceLocation} ->

12 (message : String) ->

13 a

libs/base/Debug/Trace.idr+1

@@ -3,6 +3,7 @@ module Debug.Trace

3||| Print a message for debugging purposes as a side effect

4||| @ msg what to print

5||| @ result the final result

6+abstract

6trace : (msg : String) -> (result : a) -> a

7trace : (msg : String) -> (result : a) -> a

7trace x val = unsafePerformIO {ffi=FFI_C} (do putStrLn x; return val)

8trace x val = unsafePerformIO {ffi=FFI_C} (do putStrLn x; return val)

8

9

libs/base/Language/Reflection/Utils.idr+2

@@ -4,6 +4,8 @@ import Language.Reflection

4import Language.Reflection.Elab

5import Language.Reflection.Errors

6

7+%access public

8+

7--------------------------------------------------------

9--------------------------------------------------------

8-- Tactic construction conveniences

10-- Tactic construction conveniences

9--------------------------------------------------------

11--------------------------------------------------------

libs/base/Syntax/PreorderReasoning.idr+2

@@ -1,5 +1,7 @@

1module Syntax.PreorderReasoning

2

3+%access public

4+

3-- QED is first to get the precedence to work out. It's just Refl with an explicit argument.

5-- QED is first to get the precedence to work out. It's just Refl with an explicit argument.

4syntax [expr] "QED" = qed expr

6syntax [expr] "QED" = qed expr

5-- foo ={ prf }= bar ={ prf' }= fnord QED

7-- foo ={ prf }= bar ={ prf' }= fnord QED

libs/base/System/Concurrency/Raw.idr+2

@@ -6,6 +6,8 @@ module System.Concurrency.Raw

6

7import System

8

9+%access abstract

10+

9||| Send a message of any type to the thread with the given thread id

11||| Send a message of any type to the thread with the given thread id

10||| Returns 1 if the message was sent successfully, 0 otherwise

12||| Returns 1 if the message was sent successfully, 0 otherwise

11sendToThread : (thread_id : Ptr) -> a -> IO Int

13sendToThread : (thread_id : Ptr) -> a -> IO Int

libs/base/System/Info.idr+3

@@ -1,13 +1,16 @@

1module System.Info

2

3||| The Idris backend in use

4+abstract

4backend : String

5backend : String

5backend = prim__systemInfo 0

6backend = prim__systemInfo 0

6

7

7||| The operating system in use.

8||| The operating system in use.

9+abstract

8os : String

10os : String

9os = prim__systemInfo 1

11os = prim__systemInfo 1

10

12

11||| The triple this program was targeted for

13||| The triple this program was targeted for

14+abstract

12targetTriple : String

15targetTriple : String

13targetTriple = prim__systemInfo 2

16targetTriple = prim__systemInfo 2

libs/contrib/Classes/Verified.idr+2

@@ -4,6 +4,8 @@ import Control.Algebra

4import Control.Algebra.Lattice

5import Control.Algebra.VectorSpace

6

7+%access public

8+

7-- Due to these being basically unused and difficult to implement,

9-- Due to these being basically unused and difficult to implement,

8-- they're in contrib for a bit. Once a design is found that lets them

10-- they're in contrib for a bit. Once a design is found that lets them

9-- be implemented for a number of implementations, and we get those

11-- be implemented for a number of implementations, and we get those

libs/contrib/Control/Algebra.idr+1

@@ -3,6 +3,7 @@ module Control.Algebra

3infixl 6 <->

4infixl 7 <.>

5

6+%access public

6

7

7||| Sets equipped with a single binary operation that is associative, along with

8||| Sets equipped with a single binary operation that is associative, along with

8||| a neutral element for that binary operation and inverses for all elements.

9||| a neutral element for that binary operation and inverses for all elements.

libs/contrib/Control/Algebra/Lattice.idr+1

@@ -3,6 +3,7 @@ module Control.Algebra.Lattice

3import Control.Algebra

4import Data.Heap

5

6+%access public

6

7

7||| Sets equipped with a binary operation that is commutative, associative and

8||| Sets equipped with a binary operation that is commutative, associative and

8||| idempotent. Must satisfy the following laws:

9||| idempotent. Must satisfy the following laws:

libs/contrib/Control/Algebra/NumericInstances.idr+1

@@ -7,6 +7,7 @@ import Control.Algebra.VectorSpace

7import Data.Complex

8import Data.ZZ

9

10+%access public

10

11

11Semigroup Integer where

12Semigroup Integer where

12 (<+>) = (+)

13 (<+>) = (+)

libs/contrib/Control/Algebra/VectorSpace.idr+2

@@ -2,6 +2,8 @@ module Control.Algebra.VectorSpace

2

3import Control.Algebra

4

5+%access public

6+

5infixl 5 <#>

7infixl 5 <#>

6infixr 2 <||>

8infixr 2 <||>

7

9

libs/contrib/Control/Partial.idr+1−1

@@ -7,7 +7,7 @@ module Control.Partial

7||| @ p the predicate to wait for

8||| @ f the function to repeatedly apply

9||| @ v the starting value

10−partial

10+partial abstract

11until : (p : a -> Bool) -> (f : a -> a) -> (v : a) -> a

12until p f v with (p v)

13 | False = until p f (f v)

libs/contrib/Control/WellFounded.idr+1−1

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

6module Control.WellFounded

7

8%default total

9−

9+%access public

10

11||| Accessibility: some element `x` is accessible if all `y` such that

12||| `rel y x` are themselves accessible.

libs/contrib/Data/Fun.idr+1

@@ -3,6 +3,7 @@ module Data.Fun

3import public Data.Vect

4

5%default total

6+%access public

6

7

7||| Build an n-ary function type from a Vect of Types and a result type

8||| Build an n-ary function type from a Vect of Types and a result type

8Fun : Vect n Type -> Type -> Type

9Fun : Vect n Type -> Type -> Type

libs/contrib/Data/Matrix.idr+1

@@ -5,6 +5,7 @@ module Data.Matrix

5import public Data.Vect

6

7%default total

8+%access public

8

9

9||| Matrix with n rows and m columns

10||| Matrix with n rows and m columns

10Matrix : Nat -> Nat -> Type -> Type

11Matrix : Nat -> Nat -> Type -> Type

libs/contrib/Data/Matrix/Algebraic.idr+1−1

@@ -9,7 +9,7 @@ import public Control.Algebra.NumericInstances

9

10import public Data.Matrix

11

12−

12+%access public

13%default total

14

15infixr 2 <:> -- vector inner product

libs/contrib/Data/Matrix/Numeric.idr+1

@@ -5,6 +5,7 @@ module Data.Matrix.Numeric

5import public Data.Matrix

6

7%default total

8+%access public

8

9

9infixr 2 <:> -- vector inner product

10infixr 2 <:> -- vector inner product

10infixr 2 >< -- vector outer product

11infixr 2 >< -- vector outer product

libs/contrib/Data/Nat/DivMod.idr+1

@@ -2,6 +2,7 @@

2module Data.Nat.DivMod

3

4%default total

5+%access public

5

6

6||| The result of euclidean division of natural numbers

7||| The result of euclidean division of natural numbers

7|||

8|||

libs/contrib/Data/Rel.idr+1

@@ -2,6 +2,7 @@ module Data.Rel

2

3import Data.Fun

4

5+%access public

5

6

6||| Build an n-ary relation type from a Vect of Types

7||| Build an n-ary relation type from a Vect of Types

7Rel : Vect n Type -> Type

8Rel : Vect n Type -> Type

libs/contrib/Data/Sign.idr+2

@@ -1,5 +1,7 @@

1module Data.Sign

2

3+%access public

4+

3||| A representation of signs for signed datatypes such as `ZZ`

5||| A representation of signs for signed datatypes such as `ZZ`

4data Sign = Plus | Zero | Minus

6data Sign = Plus | Zero | Minus

5

7

libs/contrib/contrib.ipkg+2

@@ -7,7 +7,9 @@ modules = Control.Algebra,

7 Control.Isomorphism.Primitives,

8 Control.Partial,

9 Control.WellFounded,

10+

10 Classes.Verified,

11 Classes.Verified,

12+

11 Data.Fun, Data.Rel,

13 Data.Fun, Data.Rel,

12 Data.Hash,

14 Data.Hash,

13 Data.Matrix, Data.Matrix.Algebraic, Data.Matrix.Numeric,

15 Data.Matrix, Data.Matrix.Algebraic, Data.Matrix.Numeric,

libs/effects/Effect/Default.idr+2

@@ -2,6 +2,8 @@ module Effect.Default

2

3import Data.Vect

4

5+%access public

6+

5interface Default a where

7interface Default a where

6 default : a

8 default : a

7

9

libs/effects/Effect/Exception.idr+2

@@ -4,6 +4,8 @@ import Effects

4import System

5import Control.IOExcept

6

7+%access public

8+

7data Exception : Type -> Effect where

9data Exception : Type -> Effect where

8 Raise : a -> sig (Exception a) b

10 Raise : a -> sig (Exception a) b

9

11

libs/effects/Effect/File.idr+1

@@ -4,6 +4,7 @@ module Effect.File

4import Effects

5import Control.IOExcept

6

7+%access public

7

8

8||| A Dependent type to describe File Handles. File handles are

9||| A Dependent type to describe File Handles. File handles are

9||| parameterised with the current state of the file: Closed; Open for

10||| parameterised with the current state of the file: Closed; Open for

libs/effects/Effect/Monad.idr+2

@@ -2,6 +2,8 @@ module Effect.Monad

2

3import Effects

4

5+%access public

6+

5data MonadEffT : List EFFECT -> (Type -> Type) -> Type -> Type where

7data MonadEffT : List EFFECT -> (Type -> Type) -> Type -> Type where

6 MkMonadEffT : EffM m a xs (\v => xs) -> MonadEffT xs m a

8 MkMonadEffT : EffM m a xs (\v => xs) -> MonadEffT xs m a

7

9

libs/effects/Effect/Random.idr+2

@@ -3,6 +3,8 @@ module Effect.Random

3import Effects

4import Data.Vect

5

6+%access public

7+

6data Random : Effect where

8data Random : Effect where

7 GetRandom : sig Random Integer Integer

9 GetRandom : sig Random Integer Integer

8 SetSeed : Integer -> sig Random () Integer

10 SetSeed : Integer -> sig Random () Integer

libs/effects/Effect/Select.idr+2

@@ -2,6 +2,8 @@ module Effect.Select

2

3import Effects

4

5+%access public

6+

5data Selection : Effect where

7data Selection : Effect where

6 Select : List a -> sig Selection a ()

8 Select : List a -> sig Selection a ()

7

9

libs/effects/Effect/StdIO.idr+2

@@ -3,6 +3,8 @@ module Effect.StdIO

3import Effects

4import Control.IOExcept

5

6+%access public

7+

6-------------------------------------------------------------

8-------------------------------------------------------------

7-- IO effects internals

9-- IO effects internals

8-------------------------------------------------------------

10-------------------------------------------------------------

libs/effects/Effect/System.idr+2

@@ -7,6 +7,8 @@ import Effects

7import System

8import Control.IOExcept

9

10+%access public

11+

10data System : Effect where

12data System : Effect where

11 Args : sig System (List String)

13 Args : sig System (List String)

12 Time : sig System Integer

14 Time : sig System Integer

libs/prelude/Decidable/Equality.idr+2

@@ -9,6 +9,8 @@ import Prelude.List

9import Prelude.Nat

10import Prelude.Maybe

11

12+%access public

13+

12--------------------------------------------------------------------------------

14--------------------------------------------------------------------------------

13-- Utility lemmas

15-- Utility lemmas

14--------------------------------------------------------------------------------

16--------------------------------------------------------------------------------

libs/prelude/Language/Reflection/Elab.idr+2

@@ -16,6 +16,8 @@ import Prelude.Monad

16import Prelude.Nat

17import Language.Reflection

18

19+%access public

20+

19data Fixity = Infixl Nat | Infixr Nat | Infix Nat | Prefix Nat

21data Fixity = Infixl Nat | Infixr Nat | Infix Nat | Prefix Nat

20

22

21||| Erasure annotations reflect Idris's idea of what is intended to be

23||| Erasure annotations reflect Idris's idea of what is intended to be

libs/prelude/Language/Reflection/Errors.idr+2

@@ -8,6 +8,8 @@ import Prelude.Bool

8import Prelude.List

9import Prelude.Maybe

10

11+%access public

12+

11data Err = Msg String

13data Err = Msg String

12 | InternalMsg String

14 | InternalMsg String

13 | CantUnify Bool TT TT Err (List (TTName, TT)) Int

15 | CantUnify Bool TT TT Err (List (TTName, TT)) Int

libs/prelude/Prelude/Applicative.idr+2

@@ -8,6 +8,8 @@ import Prelude.Interfaces

8import Prelude.Foldable

9import Prelude.Functor

10

11+%access public

12+

11---- Applicative functors/Idioms

13---- Applicative functors/Idioms

12

14

13infixl 2 <*>

15infixl 2 <*>

libs/prelude/Prelude/Basics.idr+3−1

@@ -1,7 +1,9 @@

1module Prelude.Basics

2

3import Builtins

4−

4+

5+%access public

6+

5Not : Type -> Type

7Not : Type -> Type

6Not a = a -> Void

8Not a = a -> Void

7

9

libs/prelude/Prelude/Bool.idr+2

@@ -4,6 +4,8 @@ import Builtins

4

5import Prelude.Uninhabited

6

7+%access public

8+

7||| Boolean Data Type

9||| Boolean Data Type

8%case data Bool = False | True

10%case data Bool = False | True

9

11

libs/prelude/Prelude/Cast.idr+2

@@ -3,6 +3,8 @@ module Prelude.Cast

3import Prelude.Bool

4import public Builtins

5

6+%access public

7+

6||| Interface for transforming an instance of a data type to another type.

8||| Interface for transforming an instance of a data type to another type.

7interface Cast from to where

9interface Cast from to where

8 ||| Perform a cast operation.

10 ||| Perform a cast operation.

libs/prelude/Prelude/Chars.idr+2

@@ -7,6 +7,8 @@ import Prelude.List

7import Prelude.Cast

8import Builtins

9

10+%access public

11+

10||| Convert the number to its ASCII equivalent.

12||| Convert the number to its ASCII equivalent.

11chr : Int -> Char

13chr : Int -> Char

12chr x = if (x >= 0 && x < 0x110000)

14chr x = if (x >= 0 && x < 0x110000)

libs/prelude/Prelude/Either.idr+2

@@ -8,6 +8,8 @@ import Prelude.Interfaces

8import Prelude.Maybe

9import Prelude.List

10

11+%access public

12+

11||| A sum type

13||| A sum type

12%elim data Either : (a, b : Type) -> Type where

14%elim data Either : (a, b : Type) -> Type where

13 ||| One possibility of the sum, conventionally used to represent errors

15 ||| One possibility of the sum, conventionally used to represent errors

libs/prelude/Prelude/Functor.idr+2

@@ -2,6 +2,8 @@ module Prelude.Functor

2

3import Prelude.Basics

4

5+%access public

6+

5||| Functors allow a uniform action over a parameterised type.

7||| Functors allow a uniform action over a parameterised type.

6||| @ f a parameterised type

8||| @ f a parameterised type

7interface Functor (f : Type -> Type) where

9interface Functor (f : Type -> Type) where

libs/prelude/Prelude/Interfaces.idr+2

@@ -4,6 +4,8 @@ import Builtins

4import Prelude.Basics

5import Prelude.Bool

6

7+%access public

8+

7-- Numerical Operator Precedence

9-- Numerical Operator Precedence

8infixl 5 ==, /=

10infixl 5 ==, /=

9infixl 6 <, <=, >, >=

11infixl 6 <, <=, >, >=

libs/prelude/Prelude/Providers.idr+2

@@ -4,6 +4,8 @@ import Prelude.Functor

4import Prelude.Applicative

5import Prelude.Monad

6

7+%access public

8+

7||| Type providers must build one of these in an IO computation.

9||| Type providers must build one of these in an IO computation.

8public

10public

9data Provider : (a : Type) -> Type where

11data Provider : (a : Type) -> Type where

libs/prelude/Prelude/Show.idr+2

@@ -14,6 +14,8 @@ import Prelude.Either

14import Prelude.Nat

15import Prelude.Strings

16

17+%access public

18+

17%default total

19%default total

18

20

19||| The precedence of an Idris operator or syntactic context.

21||| The precedence of an Idris operator or syntactic context.

libs/prelude/Prelude/Strings.idr+2

@@ -17,6 +17,8 @@ import Prelude.Nat

17import Prelude.Monad

18import Decidable.Equality

19

20+%access public

21+

20partial

22partial

21foldr1 : (a -> a -> a) -> List a -> a

23foldr1 : (a -> a -> a) -> List a -> a

22foldr1 _ [x] = x

24foldr1 _ [x] = x

libs/prelude/Prelude/Traversable.idr+2

@@ -7,6 +7,8 @@ import Prelude.Applicative

7import Prelude.Foldable

8import Prelude.Functor

9

10+%access public

11+

10traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()

12traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()

11traverse_ f = foldr ((*>) . f) (pure ())

13traverse_ f = foldr ((*>) . f) (pure ())

12

14

libs/prelude/Prelude/Uninhabited.idr+2

@@ -5,6 +5,8 @@ module Prelude.Uninhabited

5

6import Builtins

7

8+%access public

9+

8||| A canonical proof that some type is empty

10||| A canonical proof that some type is empty

9interface Uninhabited t where

11interface Uninhabited t where

10 ||| If I have a t, I've had a contradiction

12 ||| If I have a t, I've had a contradiction

libs/pruviloj/Pruviloj/Core.idr+2

@@ -5,6 +5,8 @@ module Pruviloj.Core

5

6import Language.Reflection.Utils

7

8+%access public

9+

8||| Run something for effects, throwing away the return value

10||| Run something for effects, throwing away the return value

9ignore : Functor f => f a -> f ()

11ignore : Functor f => f a -> f ()

10ignore x = map (const ()) x

12ignore x = map (const ()) x

libs/pruviloj/Pruviloj/Internals.idr+2

@@ -7,6 +7,8 @@ import Pruviloj.Renamers

7

8import Data.Vect

9

10+%access public

11+

10||| Get the name of a reflected type constructor argument.

12||| Get the name of a reflected type constructor argument.

11tyConArgName : TyConArg -> TTName

13tyConArgName : TyConArg -> TTName

12tyConArgName (TyConParameter a) = name a

14tyConArgName (TyConParameter a) = name a

libs/pruviloj/Pruviloj/Internals/TyConInfo.idr+1−1

@@ -6,7 +6,7 @@ import Pruviloj.Renamers

6

7import Language.Reflection.Utils

8

9−

9+%access public

10

11||| A representation of a type constructor in which all argument names

12||| are made unique and they are separated into params and then

libs/pruviloj/Pruviloj/Renamers.idr+2

@@ -2,6 +2,8 @@ module Pruviloj.Renamers

2

3import Language.Reflection.Utils

4

5+%access public

6+

5||| A renamer keeps track of names to be substituted

7||| A renamer keeps track of names to be substituted

6Renamer : Type

8Renamer : Type

7Renamer = TTName -> Maybe TTName

9Renamer = TTName -> Maybe TTName

src/Idris/Core/Evaluate.hs+3−5

@@ -12,7 +12,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

12 addDatatype, addCasedef, simplifyCasedef, addOperator,

13 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

14 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

15− mapDefCtxt,

15+ mapDefCtxt,

16 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,

17 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

18 isUniverse) where

@@ -253,12 +253,10 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

253 ev ntimes (n:stk) True env tm

254 [(Function _ tm, Public)] ->

255 ev ntimes (n:stk) True env tm

256− [(Function _ tm, Hidden)] ->

257− ev ntimes (n:stk) True env tm

258 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty

256 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty

259 return $ VP nt n vty

257 return $ VP nt n vty

260 [(CaseOp ci _ _ _ _ cd, acc)]

258 [(CaseOp ci _ _ _ _ cd, acc)]

261− | (acc /= Frozen || sUN "assert_total" `elem` stk) &&

259+ | (acc == Public || sUN "assert_total" `elem` stk) &&

262 null (fst (cases_totcheck cd)) -> -- unoptimised version

260 null (fst (cases_totcheck cd)) -> -- unoptimised version

263 let (ns, tree) = getCases cd in

261 let (ns, tree) = getCases cd in

264 if blockSimplify ci n stk

262 if blockSimplify ci n stk

@@ -376,7 +374,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

376 do let val = lookupDefAcc n (spec || atRepl) ctxt

374 do let val = lookupDefAcc n (spec || atRepl) ctxt

377 case val of

375 case val of

378 [(CaseOp ci _ _ _ _ cd, acc)]

376 [(CaseOp ci _ _ _ _ cd, acc)]

379− | acc /= Frozen || sUN "assert_total" `elem` stk ->

377+ | acc == Public || sUN "assert_total" `elem` stk ->

380 -- unoptimised version

378 -- unoptimised version

381 let (ns, tree) = getCases cd in

379 let (ns, tree) = getCases cd in

382 if blockSimplify ci n stk

380 if blockSimplify ci n stk

src/Idris/Elab/Term.hs+3−1

@@ -2476,8 +2476,10 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

2476 OK hs -> return hs

2477

2478 -- Normalize error handler terms to produce the new messages

2479+ -- Need to use 'normaliseAll' since we have to reduce private

2480+ -- names in error handlers too

2479 ctxt <- getContext

2481 ctxt <- getContext

2480− let results = map (normalise ctxt []) (map fst handlers)

2482+ let results = map (normaliseAll ctxt []) (map fst handlers)

2481 logElab 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))

2483 logElab 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))

2482

2484

2483 -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent

2485 -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent

src/Idris/IBC.hs+43−30

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

3

4module Idris.IBC (loadIBC, loadPkgIndex,

5 writeIBC, writePkgIndex,

6− hasValidIBCVersion) where

6+ hasValidIBCVersion, IBCPhase(..)) where

7

8import Idris.Core.Evaluate

9import Idris.Core.TT

@@ -40,13 +40,14 @@ import System.Directory

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 130

43+ibcVersion = 131

44

45-- When IBC is being loaded - we'll load different things (and omit different

46-- structures/definitions) depending on which phase we're in

47data IBCPhase = IBC_Building -- ^ when building the module tree

48− | IBC_REPL -- ^ when loading modules for the REPL

48+ | IBC_REPL Bool -- ^ when loading modules for the REPL

49− | IBC_IDE -- ^ when running in IDE mode

49+ -- Bool = True for top level module

50+ deriving (Show, Eq)

50

51

51data IBCFile = IBCFile { ver :: Word16,

52data IBCFile = IBCFile { ver :: Word16,

52 sourcefile :: FilePath,

53 sourcefile :: FilePath,

@@ -69,13 +70,10 @@ data IBCFile = IBCFile { ver :: Word16,

69 ibc_cgflags :: ![(Codegen, String)],

70 ibc_cgflags :: ![(Codegen, String)],

70 ibc_dynamic_libs :: ![String],

71 ibc_dynamic_libs :: ![String],

71 ibc_hdrs :: ![(Codegen, String)],

72 ibc_hdrs :: ![(Codegen, String)],

72− ibc_access :: ![(Name, Accessibility)],

73− ibc_total :: ![(Name, Totality)],

74 ibc_totcheckfail :: ![(FC, String)],

73 ibc_totcheckfail :: ![(FC, String)],

75 ibc_flags :: ![(Name, [FnOpt])],

74 ibc_flags :: ![(Name, [FnOpt])],

76 ibc_fninfo :: ![(Name, FnInfo)],

75 ibc_fninfo :: ![(Name, FnInfo)],

77 ibc_cg :: ![(Name, CGInfo)],

76 ibc_cg :: ![(Name, CGInfo)],

78− ibc_defs :: ![(Name, Def)],

79 ibc_docstrings :: ![(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))],

77 ibc_docstrings :: ![(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))],

80 ibc_moduledocs :: ![(Name, Docstring D.DocTerm)],

78 ibc_moduledocs :: ![(Name, Docstring D.DocTerm)],

81 ibc_transforms :: ![(Name, (Term, Term))],

79 ibc_transforms :: ![(Name, (Term, Term))],

@@ -94,7 +92,10 @@ data IBCFile = IBCFile { ver :: Word16,

94 ibc_usage :: ![(Name, Int)],

92 ibc_usage :: ![(Name, Int)],

95 ibc_exports :: ![Name],

93 ibc_exports :: ![Name],

96 ibc_autohints :: ![(Name, Name)],

94 ibc_autohints :: ![(Name, Name)],

97− ibc_deprecated :: ![(Name, String)]

95+ ibc_deprecated :: ![(Name, String)],

96+ ibc_defs :: ![(Name, Def)],

97+ ibc_total :: ![(Name, Totality)],

98+ ibc_access :: ![(Name, Accessibility)]

98 }

99 }

99 deriving Show

100 deriving Show

100{-!

101{-!

@@ -102,7 +103,7 @@ deriving instance Binary IBCFile

102!-}

103!-}

103

104

104initIBC :: IBCFile

105initIBC :: IBCFile

105−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] []

106+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] []

106

107

107hasValidIBCVersion :: FilePath -> Idris Bool

108hasValidIBCVersion :: FilePath -> Idris Bool

108hasValidIBCVersion fp = do

109hasValidIBCVersion fp = do

@@ -113,8 +114,9 @@ hasValidIBCVersion fp = do

113 return (ver == ibcVersion)

114 return (ver == ibcVersion)

114

115

115loadIBC :: Bool -- ^ True = reexport, False = make everything private

116loadIBC :: Bool -- ^ True = reexport, False = make everything private

117+ -> IBCPhase

116 -> FilePath -> Idris ()

118 -> FilePath -> Idris ()

117−loadIBC reexport fp

119+loadIBC reexport phase fp

118 = do imps <- getImported

120 = do imps <- getImported

119 let redo = case lookup fp imps of

121 let redo = case lookup fp imps of

120 Nothing -> True

122 Nothing -> True

@@ -125,7 +127,7 @@ loadIBC reexport fp

125 case toArchiveOrFail archiveFile of

127 case toArchiveOrFail archiveFile of

126 Left _ -> ifail $ fp ++ " isn't loadable, it may have an old ibc format.\n"

128 Left _ -> ifail $ fp ++ " isn't loadable, it may have an old ibc format.\n"

127 ++ "Please clean and rebuild it."

129 ++ "Please clean and rebuild it."

128− Right archive -> do process reexport archive fp

130+ Right archive -> do process reexport phase archive fp

129 addImported reexport fp

131 addImported reexport fp

130-- dumpTT

132-- dumpTT

131

133

@@ -134,7 +136,7 @@ loadPkgIndex :: String -> Idris ()

134loadPkgIndex pkg = do ddir <- runIO $ getIdrisLibDir

136loadPkgIndex pkg = do ddir <- runIO $ getIdrisLibDir

135 addImportDir (ddir </> pkg)

137 addImportDir (ddir </> pkg)

136 fp <- findPkgIndex pkg

138 fp <- findPkgIndex pkg

137− loadIBC True fp

139+ loadIBC True IBC_Building fp

138

140

139

141

140makeEntry :: (Binary b) => String -> [b] -> Maybe Entry

142makeEntry :: (Binary b) => String -> [b] -> Maybe Entry

@@ -164,13 +166,10 @@ entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),

164 makeEntry "ibc_cgflags" (ibc_cgflags i),

166 makeEntry "ibc_cgflags" (ibc_cgflags i),

165 makeEntry "ibc_dynamic_libs" (ibc_dynamic_libs i),

167 makeEntry "ibc_dynamic_libs" (ibc_dynamic_libs i),

166 makeEntry "ibc_hdrs" (ibc_hdrs i),

168 makeEntry "ibc_hdrs" (ibc_hdrs i),

167− makeEntry "ibc_access" (ibc_access i),

168− makeEntry "ibc_total" (ibc_total i),

169 makeEntry "ibc_totcheckfail" (ibc_totcheckfail i),

170 makeEntry "ibc_flags" (ibc_flags i),

171 makeEntry "ibc_fninfo" (ibc_fninfo i),

172 makeEntry "ibc_cg" (ibc_cg i),

173− makeEntry "ibc_defs" (ibc_defs i),

174 makeEntry "ibc_docstrings" (ibc_docstrings i),

173 makeEntry "ibc_docstrings" (ibc_docstrings i),

175 makeEntry "ibc_moduledocs" (ibc_moduledocs i),

174 makeEntry "ibc_moduledocs" (ibc_moduledocs i),

176 makeEntry "ibc_transforms" (ibc_transforms i),

175 makeEntry "ibc_transforms" (ibc_transforms i),

@@ -189,7 +188,10 @@ entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),

189 makeEntry "ibc_usage" (ibc_usage i),

188 makeEntry "ibc_usage" (ibc_usage i),

190 makeEntry "ibc_exports" (ibc_exports i),

189 makeEntry "ibc_exports" (ibc_exports i),

191 makeEntry "ibc_autohints" (ibc_autohints i),

190 makeEntry "ibc_autohints" (ibc_autohints i),

192− makeEntry "ibc_deprecated" (ibc_deprecated i)]

191+ makeEntry "ibc_deprecated" (ibc_deprecated i),

192+ makeEntry "ibc_defs" (ibc_defs i),

193+ makeEntry "ibc_total" (ibc_total i),

194+ makeEntry "ibc_access" (ibc_access i)]

193

195

194writeArchive :: FilePath -> IBCFile -> Idris ()

196writeArchive :: FilePath -> IBCFile -> Idris ()

195writeArchive fp i = do let a = L.foldl (\x y -> addEntryToArchive y x) emptyArchive (entries i)

197writeArchive fp i = do let a = L.foldl (\x y -> addEntryToArchive y x) emptyArchive (entries i)

@@ -323,8 +325,9 @@ getEntry alt f a = case findEntryByPath f a of

323 Just e -> return $! (force . decode . fromEntry) e

325 Just e -> return $! (force . decode . fromEntry) e

324

326

325process :: Bool -- ^ Reexporting

327process :: Bool -- ^ Reexporting

328+ -> IBCPhase

326 -> Archive -> FilePath -> Idris ()

329 -> Archive -> FilePath -> Idris ()

327−process reexp i fn = do

330+process reexp phase i fn = do

328 ver <- getEntry 0 "ver" i

331 ver <- getEntry 0 "ver" i

329 when (ver /= ibcVersion) $ do

332 when (ver /= ibcVersion) $ do

330 logIBC 1 "ibc out of date"

333 logIBC 1 "ibc out of date"

@@ -336,7 +339,7 @@ process reexp i fn = do

336 srcok <- runIO $ doesFileExist source

339 srcok <- runIO $ doesFileExist source

337 when srcok $ timestampOlder source fn

340 when srcok $ timestampOlder source fn

338 pImportDirs =<< getEntry [] "ibc_importdirs" i

341 pImportDirs =<< getEntry [] "ibc_importdirs" i

339− pImports reexp =<< getEntry [] "ibc_imports" i

342+ pImports reexp phase =<< getEntry [] "ibc_imports" i

340 pImps =<< getEntry [] "ibc_implicits" i

343 pImps =<< getEntry [] "ibc_implicits" i

341 pFixes =<< getEntry [] "ibc_fixes" i

344 pFixes =<< getEntry [] "ibc_fixes" i

342 pStatics =<< getEntry [] "ibc_statics" i

345 pStatics =<< getEntry [] "ibc_statics" i

@@ -353,12 +356,9 @@ process reexp i fn = do

353 pCGFlags =<< getEntry [] "ibc_cgflags" i

356 pCGFlags =<< getEntry [] "ibc_cgflags" i

354 pDyLibs =<< getEntry [] "ibc_dynamic_libs" i

357 pDyLibs =<< getEntry [] "ibc_dynamic_libs" i

355 pHdrs =<< getEntry [] "ibc_hdrs" i

358 pHdrs =<< getEntry [] "ibc_hdrs" i

356− pDefs reexp =<< getEntry [] "ibc_defs" i

357 pPatdefs =<< getEntry [] "ibc_patdefs" i

359 pPatdefs =<< getEntry [] "ibc_patdefs" i

358− pAccess reexp =<< getEntry [] "ibc_access" i

359 pFlags =<< getEntry [] "ibc_flags" i

360 pFlags =<< getEntry [] "ibc_flags" i

360 pFnInfo =<< getEntry [] "ibc_fninfo" i

361 pFnInfo =<< getEntry [] "ibc_fninfo" i

361− pTotal =<< getEntry [] "ibc_total" i

362 pTotCheckErr =<< getEntry [] "ibc_totcheckfail" i

363 pCG =<< getEntry [] "ibc_cg" i

364 pDocs =<< getEntry [] "ibc_docstrings" i

@@ -379,6 +379,9 @@ process reexp i fn = do

379 pExports =<< getEntry [] "ibc_exports" i

380 pAutoHints =<< getEntry [] "ibc_autohints" i

381 pDeprecate =<< getEntry [] "ibc_deprecated" i

382+ pDefs reexp =<< getEntry [] "ibc_defs" i

383+ pTotal =<< getEntry [] "ibc_total" i

384+ pAccess reexp phase =<< getEntry [] "ibc_access" i

382

385

383timestampOlder :: FilePath -> FilePath -> Idris ()

386timestampOlder :: FilePath -> FilePath -> Idris ()

384timestampOlder src ibc = do srct <- runIO $ getModificationTime src

387timestampOlder src ibc = do srct <- runIO $ getModificationTime src

@@ -412,8 +415,8 @@ pDeprecate ns = mapM_ (\(n,reason) -> addDeprecated n reason) ns

412pImportDirs :: [FilePath] -> Idris ()

415pImportDirs :: [FilePath] -> Idris ()

413pImportDirs fs = mapM_ addImportDir fs

416pImportDirs fs = mapM_ addImportDir fs

414

417

415−pImports :: Bool -> [(Bool, FilePath)] -> Idris ()

418+pImports :: Bool -> IBCPhase -> [(Bool, FilePath)] -> Idris ()

416−pImports reexp fs

419+pImports reexp phase fs

417 = do mapM_ (\(re, f) ->

420 = do mapM_ (\(re, f) ->

418 do i <- getIState

421 do i <- getIState

419 ibcsd <- valIBCSubDir i

422 ibcsd <- valIBCSubDir i

@@ -422,6 +425,9 @@ pImports reexp fs

422-- if (f `elem` imported i)

425-- if (f `elem` imported i)

423-- then logLvl 1 $ "Already read " ++ f

426-- then logLvl 1 $ "Already read " ++ f

424 putIState (i { imported = f : imported i })

427 putIState (i { imported = f : imported i })

428+ let phase' = case phase of

429+ IBC_REPL _ -> IBC_REPL False

430+ p -> p

425 case fp of

431 case fp of

426 LIDR fn -> do

432 LIDR fn -> do

427 logIBC 1 $ "Failed at " ++ fn

433 logIBC 1 $ "Failed at " ++ fn

@@ -429,7 +435,7 @@ pImports reexp fs

429 IDR fn -> do

435 IDR fn -> do

430 logIBC 1 $ "Failed at " ++ fn

436 logIBC 1 $ "Failed at " ++ fn

431 ifail "Must be an ibc"

437 ifail "Must be an ibc"

432− IBC fn src -> loadIBC (reexp && re) fn)

438+ IBC fn src -> loadIBC (reexp && re) phase' fn)

433 fs

439 fs

434

440

435pImps :: [(Name, [PArg])] -> Idris ()

441pImps :: [(Name, [PArg])] -> Idris ()

@@ -528,10 +534,7 @@ pDefs reexp ds

528 _ -> do logIBC 1 $ "SOLVING " ++ show n

534 _ -> do logIBC 1 $ "SOLVING " ++ show n

529 solveDeferred n

535 solveDeferred n

530 updateIState (\i -> i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })

536 updateIState (\i -> i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })

531−-- logLvl 1 $ "Added " ++ show (n, d')

537+ ) ds

532− if (not reexp) then do logIBC 1 $ "Not exporting " ++ show n

533− setAccessibility n Hidden

534− else logIBC 1 $ "Exporting " ++ show n) ds

535 where

538 where

536 updateDef (CaseOp c t args o s cd)

539 updateDef (CaseOp c t args o s cd)

537 = do o' <- mapM updateOrig o

540 = do o' <- mapM updateOrig o

@@ -599,12 +602,22 @@ pMDocs ds = mapM_ (\ (n, d) -> updateIState (\i ->

599 i { idris_moduledocs = addDef n d (idris_moduledocs i) })) ds

602 i { idris_moduledocs = addDef n d (idris_moduledocs i) })) ds

600

603

601pAccess :: Bool -- ^ Reexporting?

604pAccess :: Bool -- ^ Reexporting?

605+ -> IBCPhase

602 -> [(Name, Accessibility)] -> Idris ()

606 -> [(Name, Accessibility)] -> Idris ()

603−pAccess reexp ds

607+pAccess reexp phase ds

604 = mapM_ (\ (n, a_in) ->

608 = mapM_ (\ (n, a_in) ->

605 do let a = if reexp then a_in else Hidden

609 do let a = if reexp then a_in else Hidden

606 logIBC 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a

610 logIBC 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a

607− updateIState (\i -> i { tt_ctxt = setAccess n a (tt_ctxt i) })) ds

611+ updateIState (\i -> i { tt_ctxt = setAccess n a (tt_ctxt i) })

612+

613+ if (not reexp) then do logIBC 1 $ "Not exporting " ++ show n

614+ setAccessibility n Hidden

615+ else logIBC 1 $ "Exporting " ++ show n

616+ -- Everything should be available at the REPL from

617+ -- things imported publicly

618+ when (phase == IBC_REPL True) $

619+ setAccessibility n Public

620+ ) ds

608

621

609pFlags :: [(Name, [FnOpt])] -> Idris ()

622pFlags :: [(Name, [FnOpt])] -> Idris ()

610pFlags ds = mapM_ (\ (n, a) -> setFlags n a) ds

623pFlags ds = mapM_ (\ (n, a) -> setFlags n a) ds

src/Idris/Parser.hs+13−14

@@ -1565,17 +1565,17 @@ parseProg syn fname input mrk

1565 return (ds, i')

1566

1567{- | Load idris module and show error if something wrong happens -}

1568−loadModule :: FilePath -> Idris (Maybe String)

1568+loadModule :: FilePath -> IBCPhase -> Idris (Maybe String)

1569−loadModule f

1569+loadModule f phase

1570− = idrisCatch (loadModule' f)

1570+ = idrisCatch (loadModule' f phase)

1571 (\e -> do setErrSpan (getErrSpan e)

1572 ist <- getIState

1573 iWarn (getErrSpan e) $ pprintErr ist e

1574 return Nothing)

1575

1576{- | Load idris module -}

1577−loadModule' :: FilePath -> Idris (Maybe String)

1577+loadModule' :: FilePath -> IBCPhase -> Idris (Maybe String)

1578−loadModule' f

1578+loadModule' f phase

1579 = do i <- getIState

1580 let file = takeWhile (/= ' ') f

1581 ibcsd <- valIBCSubDir i

@@ -1589,7 +1589,7 @@ loadModule' f

1589 IDR fn -> loadSource False fn Nothing

1590 LIDR fn -> loadSource True fn Nothing

1591 IBC fn src ->

1592− idrisCatch (loadIBC True fn)

1592+ idrisCatch (loadIBC True phase fn)

1593 (\c -> do logParser 1 $ fn ++ " failed " ++ pshow i c

1594 case src of

1595 IDR sfn -> loadSource False sfn Nothing

@@ -1597,18 +1597,18 @@ loadModule' f

1597 return $ Just file

1598

1599{- | Load idris code from file -}

1600−loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()

1600+loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()

1601−loadFromIFile reexp i@(IBC fn src) maxline

1601+loadFromIFile reexp phase i@(IBC fn src) maxline

1602 = do logParser 1 $ "Skipping " ++ getSrcFile i

1603− idrisCatch (loadIBC reexp fn)

1603+ idrisCatch (loadIBC reexp phase fn)

1604 (\err -> ierror $ LoadingFailed fn err)

1605 where

1606 getSrcFile (IDR fn) = fn

1607 getSrcFile (LIDR fn) = fn

1608 getSrcFile (IBC f src) = getSrcFile src

1609

1610−loadFromIFile _ (IDR fn) maxline = loadSource' False fn maxline

1610+loadFromIFile _ _ (IDR fn) maxline = loadSource' False fn maxline

1611−loadFromIFile _ (LIDR fn) maxline = loadSource' True fn maxline

1611+loadFromIFile _ _ (LIDR fn) maxline = loadSource' True fn maxline

1612

1613{-| Load idris source code and show error if something wrong happens -}

1614loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()

@@ -1639,7 +1639,7 @@ loadSource lidr f toline

1639 LIDR fn -> ifail $ "No ibc for " ++ f

1640 IDR fn -> ifail $ "No ibc for " ++ f

1641 IBC fn src ->

1642− do loadIBC True fn

1642+ do loadIBC True IBC_Building fn

1643 let srcFn = case src of

1644 IDR fn -> Just fn

1645 LIDR fn -> Just fn

@@ -1803,8 +1803,7 @@ addHides :: [(Name, Maybe Accessibility)] -> Idris ()

1803addHides xs = do i <- getIState

1804 let defh = default_access i

1805 let (hs, as) = partition isNothing xs

1806− unless (null as) $

1807− mapM_ doHide

1806+ mapM_ doHide

1808 (map (\ (n, _) -> (n, defh)) hs ++

1807 (map (\ (n, _) -> (n, defh)) hs ++

1809 map (\ (n, Just a) -> (n, a)) as)

1808 map (\ (n, Just a) -> (n, a)) as)

1810 where isNothing (_, Nothing) = True

1809 where isNothing (_, Nothing) = True

src/Idris/REPL.hs+18−13

@@ -12,6 +12,7 @@ import Idris.REPLParser

12import Idris.ElabDecls

13import Idris.Erasure

14import Idris.Error

15+import Idris.IBC

15import Idris.ErrReverse

16import Idris.ErrReverse

16import Idris.Delaborate

17import Idris.Delaborate

17import Idris.Docstrings (Docstring, overview, renderDocstring, renderDocTerm)

18import Idris.Docstrings (Docstring, overview, renderDocstring, renderDocTerm)

@@ -735,7 +736,7 @@ processInput cmd orig inputs efile

735 return (Just mod)

736 return (Just mod)

736 Success (Right (ModImport f)) ->

737 Success (Right (ModImport f)) ->

737 do clearErr

738 do clearErr

738− fmod <- loadModule f

739+ fmod <- loadModule f (IBC_REPL True)

739 return (Just (inputs ++ maybe [] (:[]) fmod))

740 return (Just (inputs ++ maybe [] (:[]) fmod))

740 Success (Right Edit) -> do -- takeMVar stvar

741 Success (Right Edit) -> do -- takeMVar stvar

741 edit efile orig

742 edit efile orig

@@ -817,7 +818,7 @@ process fn Warranty = iPrintResult warranty

817process fn (ChangeDirectory f)

818process fn (ChangeDirectory f)

818 = do runIO $ setCurrentDirectory f

819 = do runIO $ setCurrentDirectory f

819 return ()

820 return ()

820−process fn (ModImport f) = do fmod <- loadModule f

821+process fn (ModImport f) = do fmod <- loadModule f (IBC_REPL True)

821 case fmod of

822 case fmod of

822 Just pr -> isetPrompt pr

823 Just pr -> isetPrompt pr

823 Nothing -> iPrintError $ "Can't find import " ++ f

824 Nothing -> iPrintError $ "Can't find import " ++ f

@@ -1089,7 +1090,7 @@ process fn (DebugInfo n)

1089 when (not (null di)) $ iputStrLn (show di)

1090 when (not (null di)) $ iputStrLn (show di)

1090 let imps = lookupCtxt n (idris_implicits i)

1091 let imps = lookupCtxt n (idris_implicits i)

1091 when (not (null imps)) $ iputStrLn (show imps)

1092 when (not (null imps)) $ iputStrLn (show imps)

1092− let d = lookupDef n (tt_ctxt i)

1093+ let d = lookupDefAcc n False (tt_ctxt i)

1093 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))

1094 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))

1094 let cg = lookupCtxtName n (idris_callgraph i)

1095 let cg = lookupCtxtName n (idris_callgraph i)

1095 i <- getIState

1096 i <- getIState

@@ -1238,12 +1239,15 @@ process fn (Compile codegen f)

1238 iPrintError $ "Invalid filename for compiler output \"" ++ f ++"\""

1239 iPrintError $ "Invalid filename for compiler output \"" ++ f ++"\""

1239 | otherwise = do opts <- getCmdLine

1240 | otherwise = do opts <- getCmdLine

1240 let iface = Interface `elem` opts

1241 let iface = Interface `elem` opts

1242+ let mainname = sNS (sUN "main") ["Main"]

1243+

1241 m <- if iface then return Nothing else

1244 m <- if iface then return Nothing else

1242 do (m', _) <- elabVal recinfo ERHS

1245 do (m', _) <- elabVal recinfo ERHS

1243 (PApp fc (PRef fc [] (sUN "run__IO"))

1246 (PApp fc (PRef fc [] (sUN "run__IO"))

1244− [pexp $ PRef fc [] (sNS (sUN "main") ["Main"])])

1247+ [pexp $ PRef fc [] mainname])

1245 return (Just m')

1248 return (Just m')

1246 ir <- compile codegen f m

1249 ir <- compile codegen f m

1250+

1247 i <- getIState

1251 i <- getIState

1248 runIO $ generate codegen (fst (head (idris_imported i))) ir

1252 runIO $ generate codegen (fst (head (idris_imported i))) ir

1249 where fc = fileFC "main"

1253 where fc = fileFC "main"

@@ -1559,7 +1563,7 @@ loadInputs inputs toline -- furthest line to read in input source files

1559 logParser 1 ("MODULE TREE : " ++ show modTree)

1563 logParser 1 ("MODULE TREE : " ++ show modTree)

1560 logParser 1 ("RELOAD: " ++ show ifiles)

1564 logParser 1 ("RELOAD: " ++ show ifiles)

1561 when (not (all ibc ifiles) || loadCode) $

1565 when (not (all ibc ifiles) || loadCode) $

1562− tryLoad False (filter (not . ibc) ifiles)

1566+ tryLoad False IBC_Building (filter (not . ibc) ifiles)

1563 -- return the files that need rechecking

1567 -- return the files that need rechecking

1564 return (input, ifiles))

1568 return (input, ifiles))

1565 ninputs

1569 ninputs

@@ -1570,7 +1574,8 @@ loadInputs inputs toline -- furthest line to read in input source files

1570 Nothing ->

1574 Nothing ->

1571 do putIState $!! ist { idris_tyinfodata = tidata }

1575 do putIState $!! ist { idris_tyinfodata = tidata }

1572 ibcfiles <- mapM findNewIBC (nub (concat (map snd ifiles)))

1576 ibcfiles <- mapM findNewIBC (nub (concat (map snd ifiles)))

1577+-- logLvl 0 $ "Loading from " ++ show ibcfiles

1573− tryLoad True (mapMaybe id ibcfiles)

1578+ tryLoad True (IBC_REPL True) (mapMaybe id ibcfiles)

1574 _ -> return ()

1579 _ -> return ()

1575 exports <- findExports

1580 exports <- findExports

1576

1581

@@ -1590,9 +1595,9 @@ loadInputs inputs toline -- furthest line to read in input source files

1590 iWarn emptyFC $ pprintErr i e

1595 iWarn emptyFC $ pprintErr i e

1591 return [])

1596 return [])

1592 where -- load all files, stop if any fail

1597 where -- load all files, stop if any fail

1593− tryLoad :: Bool -> [IFileType] -> Idris ()

1598+ tryLoad :: Bool -> IBCPhase -> [IFileType] -> Idris ()

1594− tryLoad keepstate [] = warnTotality >> return ()

1599+ tryLoad keepstate phase [] = warnTotality >> return ()

1595− tryLoad keepstate (f : fs)

1600+ tryLoad keepstate phase (f : fs)

1596 = do ist <- getIState

1601 = do ist <- getIState

1597 let maxline

1602 let maxline

1598 = case toline of

1603 = case toline of

@@ -1605,7 +1610,7 @@ loadInputs inputs toline -- furthest line to read in input source files

1605 then Just l

1610 then Just l

1606 else Nothing

1611 else Nothing

1607 _ -> Nothing

1612 _ -> Nothing

1608− loadFromIFile True f maxline

1613+ loadFromIFile True phase f maxline

1609 inew <- getIState

1614 inew <- getIState

1610 -- FIXME: Save these in IBC to avoid this hack! Need to

1615 -- FIXME: Save these in IBC to avoid this hack! Need to

1611 -- preserve it all from source inputs

1616 -- preserve it all from source inputs

@@ -1623,7 +1628,7 @@ loadInputs inputs toline -- furthest line to read in input source files

1623 ist <- getIState

1628 ist <- getIState

1624 putIState $!! ist { idris_tyinfodata = tidata,

1629 putIState $!! ist { idris_tyinfodata = tidata,

1625 idris_patdefs = patdefs }

1630 idris_patdefs = patdefs }

1626− tryLoad keepstate fs

1631+ tryLoad keepstate phase fs

1627

1632

1628 ibc (IBC _ _) = True

1633 ibc (IBC _ _) = True

1629 ibc _ = False

1634 ibc _ = False

@@ -1727,10 +1732,10 @@ idrisMain opts =

1727 addPkgDir "base"

1732 addPkgDir "base"

1728 mapM_ addPkgDir pkgdirs

1733 mapM_ addPkgDir pkgdirs

1729 elabPrims

1734 elabPrims

1730− when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins"

1735+ when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins" (IBC_REPL True)

1731 addAutoImport "Builtins"

1736 addAutoImport "Builtins"

1732 return ()

1737 return ()

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

1738+ when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude" (IBC_REPL True)

1734 addAutoImport "Prelude"

1739 addAutoImport "Prelude"

1735 return ()

1740 return ()

1736 when (runrepl && not idesl) initScript

1741 when (runrepl && not idesl) initScript

src/Pkg/Package.hs+1−1

@@ -142,7 +142,7 @@ documentPkg fp =

142 setCurrentDirectory pkgDir

143 let run l = runExceptT . execStateT l

144 load [] = return ()

145− load (f:fs) = do loadModule f; load fs

145+ load (f:fs) = do loadModule f IBC_Building; load fs

146 loader = do idrisMain opts; addImportDir (sourcedir pkgdesc); load fs

147 idrisInstance <- run loader idrisInit

148 setCurrentDirectory cd

test/basic009/A.idr+1

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

1module A

2

3+public

3num : Nat

4num : Nat

4num = 0

5num = 0

test/basic009/B/C.idr+1

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

1module B.C

2

3+public

3num : Nat

4num : Nat

4num = 1

5num = 1

test/dsl002/Resimp.idr+2

@@ -3,6 +3,8 @@ module Resimp

3import public Data.Vect

4import public Data.Fin

5

6+%access public

7+

6-- IO operations which read a resource

8-- IO operations which read a resource

7data Reader : Type -> Type where

9data Reader : Type -> Type where

8 MkReader : IO a -> Reader a

10 MkReader : IO a -> Reader a

test/effects003/VectMissing.idr+1

@@ -6,6 +6,7 @@ import Data.Vect

6implementation Uninhabited (Elem x []) where

7 uninhabited Here impossible

8

9+abstract

9shrink : (xs : Vect (S n) a) -> Elem x xs -> Vect n a

10shrink : (xs : Vect (S n) a) -> Elem x xs -> Vect n a

10shrink (x :: ys) Here = ys

11shrink (x :: ys) Here = ys

11shrink (y :: []) (There p) = absurd p

12shrink (y :: []) (There p) = absurd p

test/idrisdoc002/TestFunctions.idr+2−1

@@ -1,5 +1,6 @@

1module TestFunctions

2

3||| Test function

4+public

4test : ()

5test : ()

5−test = ()

6+test = ()

test/idrisdoc003/TestDatatypes.idr+2−1

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

1module TestDatatypes

2

3||| This is another test

4+public

4data Test : Type where

5data Test : Type where

5 ||| Test constructor

6 ||| Test constructor

6− ATest : Test

7+ ATest : Test

test/idrisdoc004/TestTypeclasses.idr+1

@@ -3,6 +3,7 @@ module TestTypeclasses

3||| This is a test

4|||

5||| @ a Test arg

6+public

6interface Test a where

7interface Test a where

7 ||| Test function

8 ||| Test function

8 test : a -> Int

9 test : a -> Int

test/idrisdoc005/TestTracing.idr+2−1

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

1module TestTracing

2

3+public

3test : Bool

4test : Bool

4−test = True

5+test = True

test/idrisdoc006/A/fully/Qualified/NAME.idr+2−2

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

1module A.fully.Qualified.NAME

2

3||| This is another test

4−data Test : Type where

4+public data Test : Type where

5 ||| Test constructor

6− ATest : Test

6+ ATest : Test

test/idrisdoc006/B.idr+2−1

@@ -1,5 +1,6 @@

1module B

2

3||| Test function

4+public

4test : ()

5test : ()

5−test = ()

6+test = ()

test/idrisdoc009/Test.idr+2

@@ -23,6 +23,8 @@

23module Test

24import Data.Complex

25

26+%access public

27+

26myplus : Nat -> Nat -> Nat

28myplus : Nat -> Nat -> Nat

27myplus Z j = j

29myplus Z j = j

28myplus (S k) j = S (myplus k j)

30myplus (S k) j = S (myplus k j)

test/literate001/Lit.lidr+2−2

@@ -2,12 +2,12 @@

2

3Test some string primitives while we're at it

4

5−> st : String

5+> abstract st : String

6> st = "abcdefg"

7

8Literate main program

9

10−> main : IO ()

10+> abstract main : IO ()

11> main = do { putStrLn (show (strHead st))

12> putStrLn (show (strIndex st 3))

13> putStrLn (strCons 'z' st)

test/proof002/Reflect.idr+1

@@ -2,6 +2,7 @@ module Reflect

2

3import Decidable.Equality

4

5+%access public

5%default total

6%default total

6

7

7using (xs : List a, ys : List a, G : List (List a))

8using (xs : List a, ys : List a, G : List (List a))

test/proof002/expected+3−3

@@ -1,8 +1,8 @@

1−Reflect.idr:173:21-26:

1+Reflect.idr:174:21-26:

2This style of tactic proof is deprecated. See %runElab for the replacement.

3−Reflect.idr:182:21-26:

3+Reflect.idr:183:21-26:

4This style of tactic proof is deprecated. See %runElab for the replacement.

5−Reflect.idr:190:15-20:

5+Reflect.idr:191:15-20:

6This style of tactic proof is deprecated. See %runElab for the replacement.

7test030a.idr:12:26-14:1:

8When checking right hand side of testReflect1 with expected type

test/proof003/Parity.idr+2

@@ -1,5 +1,7 @@

1module Parity

2

3+%access public

4+

3data Parity : Nat -> Type where

5data Parity : Nat -> Type where

4 Even : {n : Nat} -> Parity (n + n)

6 Even : {n : Nat} -> Parity (n + n)

5 Odd : {n : Nat} -> Parity (S (n + n))

7 Odd : {n : Nat} -> Parity (S (n + n))

test/proof003/expected+2−2

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

1−Parity.idr:15:18-23:

1+Parity.idr:17:18-23:

2This style of tactic proof is deprecated. See %runElab for the replacement.

3−Parity.idr:22:18-23:

3+Parity.idr:24:18-23:

4This style of tactic proof is deprecated. See %runElab for the replacement.

5test015.idr:88:15-20:

6This style of tactic proof is deprecated. See %runElab for the replacement.

test/reg007/A.lidr+1−1

@@ -1,5 +1,5 @@

1> module A

2

3−> n : Nat

3+> public n : Nat

4> n = ?lala

5