bb013f0 · Idris-dev · git.iko.soy

CHANGELOG+18−13

compare with master

unifiedsplit

@@ -23,6 +23,12 @@ New in 0.9.17:

23 an extra argument of type TTName. This allows more understandable

24 dynamic errors in DSL code and more readable code generation results.

25* DSL notation can now be applied with $

26+* Added FFI_Export type which allows Idris functions to be exportoed and

27+ called from foreign code

28+* Instances can now have documentation strings.

29+* Type providers can have documentation strings.

30+* Unification errors now (where possible) contain information about provenance

31+ of a type

26

32

27New in 0.9.16:

33New in 0.9.16:

28--------------

34--------------

@@ -60,7 +66,7 @@ New in 0.9.15:

60 solved automatically.

66 solved automatically.

61* More efficient representation of proof state, leading to faster elaboration

67* More efficient representation of proof state, leading to faster elaboration

62 of large expressions.

68 of large expressions.

63−* EXPERIMENTAL Implementation of uniqueness types

69+* EXPERIMENTAL Implementation of uniqueness types

64* Unary negation now desugars to "negate", which is a method of the Neg type class.

70* Unary negation now desugars to "negate", which is a method of the Neg type class.

65 This allows instances of Num that can't be negative, like Nat, and it makes correct

71 This allows instances of Num that can't be negative, like Nat, and it makes correct

66 IEEE Float operations easier to encode. Additionally, unary negation is now available

72 IEEE Float operations easier to encode. Additionally, unary negation is now available

@@ -74,12 +80,12 @@ New in 0.9.15:

74 library (see #1516)

80 library (see #1516)

75* Terms in `code blocks` inside of documentation strings are now parsed and

81* Terms in `code blocks` inside of documentation strings are now parsed and

76 type checked. If this succeeds, they are rendered in full color in

82 type checked. If this succeeds, they are rendered in full color in

77− documentation lookups, and with semantic highlighting for IDEs.

83+ documentation lookups, and with semantic highlighting for IDEs.

78* Fenced code blocks in docs defined with the "example" attribute are rendered

84* Fenced code blocks in docs defined with the "example" attribute are rendered

79 as code examples.

85 as code examples.

80* Fenced code blocks declared to be Idris code that fail to parse or type check now

86* Fenced code blocks declared to be Idris code that fail to parse or type check now

81 provide error messages to IDE clients.

87 provide error messages to IDE clients.

82−* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient

88+* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient

83 Engine style)

89 Engine style)

84

90

85New in 0.9.14:

91New in 0.9.14:

@@ -156,7 +162,7 @@ New in 0.9.12:

156 ||| @ n the first number (examined by the function)

162 ||| @ n the first number (examined by the function)

157 ||| @ m the second number (not examined)

163 ||| @ m the second number (not examined)

158 plus (n, m : Nat) -> Nat

164 plus (n, m : Nat) -> Nat

159−* Allow the auto-solve behaviour in the prover to be disabled, for easier

165+* Allow the auto-solve behaviour in the prover to be disabled, for easier

160 debugging of proof automation. Use ":set autosolve" and ":unset autosolve".

166 debugging of proof automation. Use ":set autosolve" and ":unset autosolve".

161* Updated 'effects' library

167* Updated 'effects' library

162* New :apropos command at REPL to search documentation, names, and types

168* New :apropos command at REPL to search documentation, names, and types

@@ -186,7 +192,7 @@ New in 0.9.11:

186 write "with Vect [1,2,3]" at the REPL instead of "the (Vect _ _) [1,2,3]",

192 write "with Vect [1,2,3]" at the REPL instead of "the (Vect _ _) [1,2,3]",

187 because the Vect constructors are defined in a namespace called Vect.

193 because the Vect constructors are defined in a namespace called Vect.

188* assert_smaller internal function, which marks an expression as smaller than

194* assert_smaller internal function, which marks an expression as smaller than

189− a pattern for use in totality checking.

195+ a pattern for use in totality checking.

190 e.g. "assert_smaller (x :: xs) (f xs)" asserts that "f xs" will always be

196 e.g. "assert_smaller (x :: xs) (f xs)" asserts that "f xs" will always be

191 structurally smaller than "(x :: xs)"

197 structurally smaller than "(x :: xs)"

192* assert_total internal function, which marks a subexpression as assumed to

198* assert_total internal function, which marks a subexpression as assumed to

@@ -211,7 +217,7 @@ New in 0.9.10:

211 types may now depend on earlier methods.

217 types may now depend on earlier methods.

212* More flexible class instance resolution, so that function types and lambda

218* More flexible class instance resolution, so that function types and lambda

213 expressions can be made instances of a type class.

219 expressions can be made instances of a type class.

214−* Add !expr notation for implicit binding of intermediate results in

220+* Add !expr notation for implicit binding of intermediate results in

215 monadic/do/etc expressions.

221 monadic/do/etc expressions.

216* Extend Effects package to cope with possibly failing operations, using

222* Extend Effects package to cope with possibly failing operations, using

217 "if_valid", "if_error", etc.

223 "if_valid", "if_error", etc.

@@ -336,7 +342,7 @@ User visible changes:

336Internal changes:

342Internal changes:

337

343

338* Separate inlining methods at compile-time and run-time

344* Separate inlining methods at compile-time and run-time

339−* Fixed nested parameters blocks

345+* Fixed nested parameters blocks

340* Improve efficiency of elaborator by:

346* Improve efficiency of elaborator by:

341 - only normalising when necessary

347 - only normalising when necessary

342 - reducing backtracking with resolving ambiguities

348 - reducing backtracking with resolving ambiguities

@@ -417,7 +423,7 @@ User visible changes:

417Internal changes:

423Internal changes:

418

424

419* Some type class resolution fixes

425* Some type class resolution fixes

420−* Several minor bug fixes

426+* Several minor bug fixes

421* Performance improvements in resolving overloading and type classes

427* Performance improvements in resolving overloading and type classes

422

428

423New in 0.9.1:

429New in 0.9.1:

@@ -465,11 +471,10 @@ Complete rewrite. User visible changes:

465Internal changes:

471Internal changes:

466

472

467* Everything :-)

473* Everything :-)

468−* All definitions (functions, classes and instances) are elaborated to top

474+* All definitions (functions, classes and instances) are elaborated to top

469− level, fully explicit, data declarations and pattern matching definitions,

475+ level, fully explicit, data declarations and pattern matching definitions,

470− which are verified by a minimal type checker.

476+ which are verified by a minimal type checker.

471

477

472This is the first release of a complete reimplementation. There will be bugs.

478This is the first release of a complete reimplementation. There will be bugs.

473−If you find any, please do not hesitate to contact Edwin Brady

479+If you find any, please do not hesitate to contact Edwin Brady

474(ecb10@st-andrews.ac.uk).

480(ecb10@st-andrews.ac.uk).

475−

CONTRIBUTORS+1

@@ -28,6 +28,7 @@ Tom Prince

28raichoo

29Philip Rasmussen

30Reynir Reynisson

31+Adam Sandberg Eriksson

31Seo Sanghyeon

32Seo Sanghyeon

32Benjamin Saunders

33Benjamin Saunders

33Alexander Shabalin

34Alexander Shabalin

codegen/idris-c/Main.hs+7−2

@@ -10,10 +10,12 @@ import IRTS.CodegenC

10

11import System.Environment

12import System.Exit

13+import Control.Monad

13

14

14import Paths_idris

15import Paths_idris

15

16

16data Opts = Opts { inputs :: [FilePath],

17data Opts = Opts { inputs :: [FilePath],

18+ interface :: Bool,

17 output :: FilePath }

19 output :: FilePath }

18

20

19showUsage = do putStrLn "Usage: idris-c <ibc-files> [-o <output-file>]"

21showUsage = do putStrLn "Usage: idris-c <ibc-files> [-o <output-file>]"

@@ -21,16 +23,19 @@ showUsage = do putStrLn "Usage: idris-c <ibc-files> [-o <output-file>]"

21

23

22getOpts :: IO Opts

24getOpts :: IO Opts

23getOpts = do xs <- getArgs

25getOpts = do xs <- getArgs

24− return $ process (Opts [] "a.out") xs

26+ return $ process (Opts [] False "a.out") xs

25 where

27 where

26 process opts ("-o":o:xs) = process (opts { output = o }) xs

28 process opts ("-o":o:xs) = process (opts { output = o }) xs

29+ process opts ("--interface":xs) = process (opts { interface = True }) xs

27 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

30 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

28 process opts [] = opts

31 process opts [] = opts

29

32

30c_main :: Opts -> Idris ()

33c_main :: Opts -> Idris ()

31c_main opts = do elabPrims

34c_main opts = do elabPrims

32 loadInputs (inputs opts) Nothing

35 loadInputs (inputs opts) Nothing

36+ mainProg <- if interface opts

33− mainProg <- elabMain

37+ then liftM Just elabMain

38+ else return Nothing

34 ir <- compile (Via "c") (output opts) mainProg

39 ir <- compile (Via "c") (output opts) mainProg

35 runIO $ codegenC ir

40 runIO $ codegenC ir

36

41

codegen/idris-javascript/Main.hs+1−1

@@ -32,7 +32,7 @@ jsMain :: Opts -> Idris ()

32jsMain opts = do elabPrims

33 loadInputs (inputs opts) Nothing

34 mainProg <- elabMain

35− ir <- compile (Via "javascript") (output opts) mainProg

35+ ir <- compile (Via "javascript") (output opts) (Just mainProg)

36 runIO $ codegenJavaScript ir

37

38main :: IO ()

codegen/idris-node/Main.hs+1−1

@@ -32,7 +32,7 @@ jsMain :: Opts -> Idris ()

32jsMain opts = do elabPrims

33 loadInputs (inputs opts) Nothing

34 mainProg <- elabMain

35− ir <- compile (Via "node") (output opts) mainProg

35+ ir <- compile (Via "node") (output opts) (Just mainProg)

36 runIO $ codegenNode ir

37

38main :: IO ()

idris.cabal+16

@@ -394,6 +394,10 @@ Extra-source-files:

394 test/ffi005/*.idr

395 test/ffi005/run

396 test/ffi005/expected

397+ test/ffi006/*.idr

398+ test/ffi006/*.c

399+ test/ffi006/run

400+ test/ffi006/expected

397

401

398 test/idrisdoc001/run

402 test/idrisdoc001/run

399 test/idrisdoc001/expected

403 test/idrisdoc001/expected

@@ -607,6 +611,17 @@ Extra-source-files:

607 test/unique003/*.idr

611 test/unique003/*.idr

608 test/unique003/expected

612 test/unique003/expected

609

613

614+ test/docs001/run

615+ test/docs001/input

616+ test/docs001/*.idr

617+ test/docs001/expected

618+ test/docs002/run

619+ test/docs002/input

620+ test/docs002/*.idr

621+ test/docs002/expected

622+

623+

624+

610source-repository head

625source-repository head

611 type: git

626 type: git

612 location: git://github.com/idris-lang/Idris-dev.git

627 location: git://github.com/idris-lang/Idris-dev.git

@@ -723,6 +738,7 @@ Library

723 , IRTS.CodegenC

738 , IRTS.CodegenC

724 , IRTS.CodegenCommon

739 , IRTS.CodegenCommon

725 , IRTS.CodegenJavaScript

740 , IRTS.CodegenJavaScript

741+ , IRTS.Exports

726 , IRTS.JavaScript.AST

742 , IRTS.JavaScript.AST

727 , IRTS.Compiler

743 , IRTS.Compiler

728 , IRTS.Defunctionalise

744 , IRTS.Defunctionalise

libs/base/Data/Fin.idr+39−9

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

1module Data.Fin

2

3%default total

4+%access public

4

5

5||| Numbers strictly less than some bound. The name comes from "finite sets".

6||| Numbers strictly less than some bound. The name comes from "finite sets".

6|||

7|||

@@ -144,18 +145,47 @@ fromInteger {n} x {prf} with (integerToFin x n)

144

145

145%language ErrorReflection

146%language ErrorReflection

146

147

148+||| Attempt to convert a reflected (fromInteger n) to a Nat

149+total private

150+getNat' : TT -> Maybe TT

151+getNat' `(fromInteger ~(TConst (BI c)) : Nat) = Just $ quote (the Nat (fromInteger c))

152+getNat' _ = Nothing

153+

154+||| Attempt to convert a reflected (fromInteger n) to a Nat. Return

155+||| the original term on failure.

156+total private

157+getNat : TT -> TT

158+getNat tm = maybe tm id $ getNat' tm

159+

160+total private

161+mkFinIntegerErr : TT -> TT -> List ErrorReportPart -> Maybe (List ErrorReportPart)

162+mkFinIntegerErr lit finSize subErr

163+ = Just [ TextPart "When using", TermPart lit

164+ , TextPart "as a literal for a"

165+ , TermPart `(Fin ~(getNat finSize))

166+ , SubReport subErr

167+ ]

147total

168total

148finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)

169finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)

170+finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(TConst c) ~m)) err xs y)

171+ = mkFinIntegerErr (TConst c) m

172+ [ TermPart (TConst c)

173+ , TextPart "is not strictly less than"

174+ , TermPart (getNat m)

175+ ]

176+finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(P Bound n t) ~m)) err xs y)

177+ = mkFinIntegerErr (P Bound n t) m

178+ [ TextPart "Could not show that", TermPart (P Bound n t)

179+ , TextPart "is less than", TermPart (getNat m)

180+ , TextPart "because", TermPart (P Bound n t)

181+ , TextPart "is a bound variable instead of a constant"

182+ , TermPart (TConst (AType (ATInt ITBig)))

183+ ]

149finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)

184finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)

150− = Just [ TextPart "When using", TermPart n

185+ = mkFinIntegerErr n m

151− , TextPart "as a literal for a"

152− , TermPart `(Fin ~m)

153− , SubReport [ TextPart "Could not show that"

186+ [ TextPart "Could not show that" , TermPart n

154− , TermPart n

155− , TextPart "is less than"

187+ , TextPart "is less than" , TermPart (getNat m)

156− , TermPart m

157− ]

158− ]

188+ ]

159finFromIntegerErrors _ = Nothing

189finFromIntegerErrors _ = Nothing

160

190

161%error_handlers Data.Fin.fromInteger prf finFromIntegerErrors

191%error_handlers Data.Fin.fromInteger prf finFromIntegerErrors

libs/base/Data/VectType.idr+5−4

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

1−module Data.VectType

1+module Data.VectType

2

3import Data.Fin

4

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

6%default total

7

8namespace Vect {

9−

9+

10infixr 7 ::

11

12%elim data Vect : Nat -> Type -> Type where

@@ -531,6 +531,8 @@ instance Applicative (Vect k) where

531

532 fs <*> vs = zipWith apply fs vs

533

534+||| This monad is different from the List monad, (>>=)

535+||| uses the diagonal.

534instance Monad (Vect n) where

536instance Monad (Vect n) where

535 m >>= f = diag (map f m)

537 m >>= f = diag (map f m)

536

538

@@ -539,7 +541,7 @@ instance Traversable (Vect n) where

539 traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]

541 traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]

540

542

541--------------------------------------------------------------------------------

543--------------------------------------------------------------------------------

542−-- Show

544+-- Show

543--------------------------------------------------------------------------------

545--------------------------------------------------------------------------------

544

546

545instance Show a => Show (Vect n a) where

547instance Show a => Show (Vect n a) where

@@ -595,4 +597,3 @@ instance DecEq a => DecEq (Vect n a) where

595

597

596-- For the primitives, we have to cheat because we don't have access to their

598-- For the primitives, we have to cheat because we don't have access to their

597-- internal implementations.

599-- internal implementations.

598−

libs/prelude/IO.idr+53−4

@@ -21,7 +21,9 @@ abstract WorldRes : Type -> Type

21WorldRes x = x

22

23record FFI : Type where

24− MkFFI : (ffi_types : Type -> Type) -> (ffi_fn : Type) -> FFI

24+ MkFFI : (ffi_types : Type -> Type) ->

25+ (ffi_fn : Type) ->

26+ (ffi_data : Type) -> FFI

25

27

26abstract

28abstract

27data IO' : (lang : FFI) -> Type -> Type where

29data IO' : (lang : FFI) -> Type -> Type where

@@ -89,8 +91,12 @@ io_return x = MkIO (\w => prim_io_return x)

89liftPrimIO : (World -> PrimIO a) -> IO' l a

91liftPrimIO : (World -> PrimIO a) -> IO' l a

90liftPrimIO = MkIO

92liftPrimIO = MkIO

91

93

94+call__IO : IO' l a -> PrimIO a

95+call__IO (MkIO f) = f (TheWorld prim__TheWorld)

96+

97+-- Concrete type makes it easier to elaborate at top level

92run__IO : IO' l () -> PrimIO ()

98run__IO : IO' l () -> PrimIO ()

93−run__IO (MkIO f) = f (TheWorld prim__TheWorld)

99+run__IO f = call__IO f

94

100

95unsafePerformIO : IO' ffi a -> a

101unsafePerformIO : IO' ffi a -> a

96unsafePerformIO (MkIO f) = unsafePerformPrimIO

102unsafePerformIO (MkIO f) = unsafePerformPrimIO

@@ -143,7 +149,7 @@ data C_Types : Type -> Type where

143 C_IntT : C_IntTypes i -> C_Types i

149 C_IntT : C_IntTypes i -> C_Types i

144

150

145FFI_C : FFI

151FFI_C : FFI

146−FFI_C = MkFFI C_Types String

152+FFI_C = MkFFI C_Types String String

147

153

148IO : Type -> Type

154IO : Type -> Type

149IO = IO' FFI_C

155IO = IO' FFI_C

@@ -194,8 +200,51 @@ mutual

194%used MkJsFn x

200%used MkJsFn x

195

201

196FFI_JS : FFI

202FFI_JS : FFI

197−FFI_JS = MkFFI JS_Types String

203+FFI_JS = MkFFI JS_Types String String

198

204

199JS_IO : Type -> Type

205JS_IO : Type -> Type

200JS_IO = IO' FFI_JS

206JS_IO = IO' FFI_JS

201

207

208+

209+--------- Foreign Exports

210+

211+namespace FFI_Export

212+-- It's just like Data.List.Elem, but we don't need all the other stuff

213+-- that comes with it, just a proof that a data type is defined.

214+ data DataDefined : Type -> List (Type, s) -> s -> Type where

215+ DHere : DataDefined x ((x, t) :: xs) t

216+ DThere : DataDefined x xs t -> DataDefined x (y :: xs) t

217+

218+ data FFI_Base : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where

219+ FFI_ExpType : {n : ffi_data f} -> (def : DataDefined t xs n) -> FFI_Base f xs t

220+ FFI_Prim : (prim : ffi_types f t) -> FFI_Base f xs t

221+

222+ %used FFI_ExpType n

223+ %used FFI_ExpType def

224+ %used FFI_Prim prim

225+

226+ data FFI_Exportable : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where

227+ FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO t)

228+ FFI_Fun : (b : FFI_Base f xs s) -> (a : FFI_Exportable f xs t) -> FFI_Exportable f xs (s -> t)

229+ FFI_Ret : (b : FFI_Base f xs t) -> FFI_Exportable f xs t

230+

231+ %used FFI_IO b

232+ %used FFI_Fun b

233+ %used FFI_Fun a

234+ %used FFI_Ret b

235+

236+ data FFI_Export : (f : FFI) -> String -> List (Type, ffi_data f) -> Type where

237+ Data : (x : Type) -> (n : ffi_data f) ->

238+ (es : FFI_Export f h ((x, n) :: xs)) -> FFI_Export f h xs

239+ Fun : (fn : t) -> (n : ffi_fn f) -> {auto prf : FFI_Exportable f xs t} ->

240+ (es : FFI_Export f h xs) -> FFI_Export f h xs

241+ End : FFI_Export f h xs

242+

243+%used Data x

244+%used Data n

245+%used Data es

246+%used Fun fn

247+%used Fun n

248+%used Fun es

249+%used Fun prf

250+

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

@@ -195,6 +195,7 @@ instance Num Nat where

195instance MinBound Nat where

196 minBound = Z

197

198+||| Casts negative `Integers` to 0.

198instance Cast Integer Nat where

199instance Cast Integer Nat where

199 cast = fromInteger

200 cast = fromInteger

200

201

@@ -250,6 +251,7 @@ instance BoundedJoinSemilattice Nat where

250 bottom = Z

251 bottom = Z

251

252

253

254+||| Casts negative `Ints` to 0.

253instance Cast Int Nat where

255instance Cast Int Nat where

254 cast i = fromInteger (cast i)

256 cast i = fromInteger (cast i)

255

257

@@ -333,7 +335,7 @@ lcm x y = divNat (x * y) (gcd x y)

333

335

334

336

335--------------------------------------------------------------------------------

337--------------------------------------------------------------------------------

336−-- An informative comparison view

338+-- An informative comparison view

337--------------------------------------------------------------------------------

339--------------------------------------------------------------------------------

338data CmpNat : Nat -> Nat -> Type where

340data CmpNat : Nat -> Nat -> Type where

339 CmpLT : (y : _) -> CmpNat x (x + S y)

341 CmpLT : (y : _) -> CmpNat x (x + S y)

rts/idris_rts.c+14

@@ -63,6 +63,20 @@ VM* init_vm(int stack_size, size_t heap_size,

63 return vm;

64}

65

66+VM* idris_vm() {

67+ VM* vm = init_vm(4096000, 4096000, 1);

68+ init_threadkeys();

69+ init_threaddata(vm);

70+ init_gmpalloc();

71+ init_nullaries();

72+

73+ return vm;

74+}

75+

76+void close_vm(VM* vm) {

77+ terminate(vm);

78+}

79+

66void init_threadkeys() {

80void init_threadkeys() {

67#ifdef HAS_PTHREAD

81#ifdef HAS_PTHREAD

68 pthread_key_create(&vm_key, (void*)free_key);

82 pthread_key_create(&vm_key, (void*)free_key);

rts/idris_rts.h+5

@@ -125,6 +125,11 @@ void init_threaddata(VM *vm);

125// Clean up a VM once it's no longer needed

126Stats terminate(VM* vm);

127

128+// Create a new VM, set up everything with sensible defaults (use when

129+// calling Idris from C)

130+VM* idris_vm();

131+void close_vm(VM* vm);

132+

128// Set up key for thread-local data - called once from idris_main

133// Set up key for thread-local data - called once from idris_main

129void init_threadkeys();

134void init_threadkeys();

130

135

src/IRTS/CodegenC.hs+124−17

@@ -24,15 +24,19 @@ import Control.Monad

24import Debug.Trace

25

26codegenC :: CodeGenerator

27−codegenC ci = codegenC' (simpleDecls ci)

27+codegenC ci = do codegenC' (simpleDecls ci)

28− (outputFile ci)

28+ (outputFile ci)

29− (outputType ci)

29+ (outputType ci)

30− (includes ci)

30+ (includes ci)

31− (compileObjs ci)

31+ (compileObjs ci)

32− (map mkLib (compileLibs ci) ++

32+ (map mkLib (compileLibs ci) ++

33− map incdir (importDirs ci))

33+ map incdir (importDirs ci))

34− (compilerFlags ci)

34+ (compilerFlags ci)

35+ (exportDecls ci)

36+ (interfaces ci)

35− (debugLevel ci)

37+ (debugLevel ci)

38+ when (interfaces ci) $

39+ codegenH (exportDecls ci)

36

40

37 where mkLib l = "-l" ++ l

41 where mkLib l = "-l" ++ l

38 incdir i = "-I" ++ i

42 incdir i = "-I" ++ i

@@ -44,17 +48,20 @@ codegenC' :: [(Name, SDecl)] ->

44 [String] -> -- extra object files

48 [String] -> -- extra object files

45 [String] -> -- extra compiler flags (libraries)

49 [String] -> -- extra compiler flags (libraries)

46 [String] -> -- extra compiler flags (anything)

50 [String] -> -- extra compiler flags (anything)

51+ [ExportIFace] ->

52+ Bool -> -- interfaces too (so make a .o instead)

47 DbgLevel ->

53 DbgLevel ->

48 IO ()

54 IO ()

49−codegenC' defs out exec incs objs libs flags dbg

55+codegenC' defs out exec incs objs libs flags exports iface dbg

50 = do -- print defs

56 = do -- print defs

51 let bc = map toBC defs

57 let bc = map toBC defs

52 let h = concatMap toDecl (map fst bc)

58 let h = concatMap toDecl (map fst bc)

53 let cc = concatMap (uncurry toC) bc

59 let cc = concatMap (uncurry toC) bc

60+ let hi = concatMap ifaceC (concatMap getExp exports)

54 d <- getDataDir

61 d <- getDataDir

55 mprog <- readFile (d </> "rts" </> "idris_main" <.> "c")

62 mprog <- readFile (d </> "rts" </> "idris_main" <.> "c")

56 let cout = headers incs ++ debug dbg ++ h ++ cc ++

63 let cout = headers incs ++ debug dbg ++ h ++ cc ++

57− (if (exec == Executable) then mprog else "")

64+ (if (exec == Executable) then mprog else hi)

58 case exec of

65 case exec of

59 MavenProject -> putStrLn ("FAILURE: output type not supported")

66 MavenProject -> putStrLn ("FAILURE: output type not supported")

60 Raw -> writeFile out cout

67 Raw -> writeFile out cout

@@ -67,21 +74,23 @@ codegenC' defs out exec incs objs libs flags dbg

67 libFlags <- getLibFlags

74 libFlags <- getLibFlags

68 incFlags <- getIncFlags

75 incFlags <- getIncFlags

69 let args = [gccDbg dbg] ++

76 let args = [gccDbg dbg] ++

70− gccFlags ++

77+ gccFlags iface ++

71 -- # Any flags defined here which alter the RTS API must also be added to config.mk

78 -- # Any flags defined here which alter the RTS API must also be added to config.mk

72 ["-DHAS_PTHREAD", "-DIDRIS_ENABLE_STATS", "-msse2",

79 ["-DHAS_PTHREAD", "-DIDRIS_ENABLE_STATS", "-msse2",

73 "-I."] ++ objs ++ ["-x", "c"] ++

80 "-I."] ++ objs ++ ["-x", "c"] ++

74 (if (exec == Executable) then [] else ["-c"]) ++

81 (if (exec == Executable) then [] else ["-c"]) ++

75 [tmpn] ++

82 [tmpn] ++

76− concatMap words libFlags ++

83+ (if not iface then concatMap words libFlags else []) ++

77 concatMap words incFlags ++

84 concatMap words incFlags ++

78− concatMap words libs ++

85+ (if not iface then concatMap words libs else []) ++

79 concatMap words flags ++

86 concatMap words flags ++

80 ["-o", out]

87 ["-o", out]

81−-- putStrLn gcc

88+-- putStrLn (show args)

82 exit <- rawSystem comp args

89 exit <- rawSystem comp args

83 when (exit /= ExitSuccess) $

90 when (exit /= ExitSuccess) $

84 putStrLn ("FAILURE: " ++ show comp ++ " " ++ show args)

91 putStrLn ("FAILURE: " ++ show comp ++ " " ++ show args)

92+ where

93+ getExp (Export _ _ exp) = exp

85

94

86headers xs =

95headers xs =

87 concatMap

96 concatMap

@@ -93,7 +102,8 @@ debug _ = ""

93

102

94-- We're using signed integers now. Make sure we get consistent semantics

103-- We're using signed integers now. Make sure we get consistent semantics

95-- out of them from gcc. See e.g. http://thiemonagel.de/2010/01/signed-integer-overflow/

104-- out of them from gcc. See e.g. http://thiemonagel.de/2010/01/signed-integer-overflow/

105+gccFlags i = if i then ["-fwrapv"]

96−gccFlags = ["-fwrapv", "-fno-strict-overflow"]

106+ else ["-fwrapv", "-fno-strict-overflow"]

97

107

98gccDbg DEBUG = "-g"

108gccDbg DEBUG = "-g"

99gccDbg TRACE = "-O2"

109gccDbg TRACE = "-O2"

@@ -311,7 +321,7 @@ toFType (FApp c [_,ity])

311 | c == sUN "C_IntT" = FArith (toAType ity)

321 | c == sUN "C_IntT" = FArith (toAType ity)

312toFType (FApp c [_])

322toFType (FApp c [_])

313 | c == sUN "C_Any" = FAny

323 | c == sUN "C_Any" = FAny

314−toFType t = error (show t ++ " not defined in toFType")

324+toFType t = FAny

315

325

316c_irts (FArith (ATInt ITNative)) l x = l ++ "MKINT((i_int)(" ++ x ++ "))"

326c_irts (FArith (ATInt ITNative)) l x = l ++ "MKINT((i_int)(" ++ x ++ "))"

317c_irts (FArith (ATInt ITChar)) l x = c_irts (FArith (ATInt ITNative)) l x

327c_irts (FArith (ATInt ITChar)) l x = c_irts (FArith (ATInt ITNative)) l x

@@ -561,3 +571,100 @@ doOp _ op args = error "doOp of (" ++ show op ++ ") not implemented, arguments (

561

571

562flUnOp :: String -> String -> String

572flUnOp :: String -> String -> String

563flUnOp name val = "MKFLOAT(vm, " ++ name ++ "(GETFLOAT(" ++ val ++ ")))"

573flUnOp name val = "MKFLOAT(vm, " ++ name ++ "(GETFLOAT(" ++ val ++ ")))"

574+

575+-------------------- Interface file generation

576+

577+-- First, the wrappers in the C file

578+

579+ifaceC :: Export -> String

580+ifaceC (ExportData n) = "typedef VAL " ++ cdesc n ++ ";\n"

581+ifaceC (ExportFun n cn ret args)

582+ = ctype ret ++ " " ++ cdesc cn ++

583+ "(VM* vm" ++ showArgs (zip argNames args) ++ ") {\n"

584+ ++ mkBody n (zip argNames args) ret ++ "}\n\n"

585+ where showArgs [] = ""

586+ showArgs ((n, t) : ts) = ", " ++ ctype t ++ " " ++ n ++

587+ showArgs ts

588+

589+ argNames = zipWith (++) (repeat "arg") (map show [0..])

590+

591+mkBody n as t = indent 1 ++ "INITFRAME;\n" ++

592+ indent 1 ++ "RESERVE(" ++ show (max (length as) 3) ++ ");\n" ++

593+ push 0 as ++ call n ++ retval t

594+ where push i [] = ""

595+ push i ((n, t) : ts) = indent 1 ++ c_irts (toFType t)

596+ ("TOP(" ++ show i ++ ") = ") n

597+ ++ ";\n" ++ push (i + 1) ts

598+

599+ call _ = indent 1 ++ "STOREOLD;\n" ++

600+ indent 1 ++ "BASETOP(0);\n" ++

601+ indent 1 ++ "ADDTOP(" ++ show (length as) ++ ");\n" ++

602+ indent 1 ++ "CALL(" ++ cname n ++ ");\n"

603+

604+ retval (FIO t)

605+ = indent 1 ++ "TOP(0) = NULL;\n" ++

606+ indent 1 ++ "TOP(1) = NULL;\n" ++

607+ indent 1 ++ "TOP(2) = RVAL;\n" ++

608+ indent 1 ++ "STOREOLD;\n" ++

609+ indent 1 ++ "BASETOP(0);\n" ++

610+ indent 1 ++ "ADDTOP(3);\n" ++

611+ indent 1 ++ "CALL(" ++ cname (sUN "call__IO") ++ ");\n" ++

612+ retval t

613+ retval t = indent 1 ++ "return " ++ irts_c (toFType t) "RVAL" ++ ";\n"

614+

615+ctype (FCon c)

616+ | c == sUN "C_Str" = "char*"

617+ | c == sUN "C_Float" = "float"

618+ | c == sUN "C_Ptr" = "void*"

619+ | c == sUN "C_MPtr" = "void*"

620+ | c == sUN "C_Unit" = "void"

621+ctype (FApp c [_,ity])

622+ | c == sUN "C_IntT" = carith ity

623+ctype (FApp c [_])

624+ | c == sUN "C_Any" = "VAL"

625+ctype (FStr s) = s

626+ctype FUnknown = "void*"

627+ctype (FIO t) = ctype t

628+ctype t = error "Can't happen: Not a valid interface type " ++ show t

629+

630+carith (FCon i)

631+ | i == sUN "C_IntChar" = "char"

632+ | i == sUN "C_IntNative" = "int"

633+carith t = error "Can't happen: Not an exportable arithmetic type"

634+

635+cdesc (FStr s) = s

636+cdesc s = error "Can't happen: Not a valid C name"

637+

638+-- Then, the header files

639+

640+codegenH :: [ExportIFace] -> IO ()

641+codegenH es = mapM_ writeIFace es

642+

643+writeIFace :: ExportIFace -> IO ()

644+writeIFace (Export ffic hdr exps)

645+ | ffic == sUN "FFI_C"

646+ = do let hfile = "#ifndef " ++ hdr_guard hdr ++ "\n" ++

647+ "#define " ++ hdr_guard hdr ++ "\n\n" ++

648+ "#include <idris_rts.h>\n\n" ++

649+ concatMap hdr_export exps ++ "\n" ++

650+ "#endif\n\n"

651+ writeFile hdr hfile

652+ | otherwise = return ()

653+

654+hdr_guard x = "__" ++ map hchar x

655+ where hchar x | isAlphaNum x = toUpper x

656+ hchar _ = '_'

657+

658+hdr_export :: Export -> String

659+hdr_export (ExportData n) = "typedef VAL " ++ cdesc n ++ ";\n"

660+hdr_export (ExportFun n cn ret args)

661+ = ctype ret ++ " " ++ cdesc cn ++

662+ "(VM* vm" ++ showArgs (zip argNames args) ++ ");\n"

663+ where showArgs [] = ""

664+ showArgs ((n, t) : ts) = ", " ++ ctype t ++ " " ++ n ++

665+ showArgs ts

666+

667+ argNames = zipWith (++) (repeat "arg") (map show [0..])

668+

669+

670+

src/IRTS/CodegenCommon.hs+3−1

@@ -33,7 +33,9 @@ data CodegenInfo = CodegenInfo { outputFile :: String,

33 debugLevel :: DbgLevel,

34 simpleDecls :: [(Name, SDecl)],

35 defunDecls :: [(Name, DDecl)],

36− liftDecls :: [(Name, LDecl)]

36+ liftDecls :: [(Name, LDecl)],

37+ interfaces :: Bool,

38+ exportDecls :: [ExportIFace]

37 }

39 }

38

40

39type CodeGenerator = CodegenInfo -> IO ()

41type CodeGenerator = CodegenInfo -> IO ()

src/IRTS/Compiler.hs+21−11

@@ -11,6 +11,7 @@ import IRTS.CodegenC

11import IRTS.DumpBC

12import IRTS.CodegenJavaScript

13import IRTS.Inliner

14+import IRTS.Exports

14

15

15import Idris.AbsSyntax

16import Idris.AbsSyntax

16import Idris.AbsSyntaxTree

17import Idris.AbsSyntaxTree

@@ -45,20 +46,30 @@ import System.FilePath ((</>), addTrailingPathSeparator)

45

46

46-- | Given a 'main' term to compiler, return the IRs which can be used to

47-- | Given a 'main' term to compiler, return the IRs which can be used to

47-- generate code.

48-- generate code.

48−compile :: Codegen -> FilePath -> Term -> Idris CodegenInfo

49+compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo

49−compile codegen f tm

50+compile codegen f mtm

50 = do checkMVs -- check for undefined metavariables

51 = do checkMVs -- check for undefined metavariables

51 checkTotality -- refuse to compile if there are totality problems

52 checkTotality -- refuse to compile if there are totality problems

53+ exports <- findExports

54+

52− reachableNames <- performUsageAnalysis

55+ reachableNames <- performUsageAnalysis (getExpNames exports)

56+ maindef <- case mtm of

57+ Nothing -> return []

53− maindef <- irMain tm

58+ Just tm -> do md <- irMain tm

54− iLOG $ "MAIN: " ++ show maindef

59+ iLOG $ "MAIN: " ++ show md

60+ return [(sMN 0 "runMain", md)]

55 objs <- getObjectFiles codegen

61 objs <- getObjectFiles codegen

56 libs <- getLibs codegen

62 libs <- getLibs codegen

57 flags <- getFlags codegen

63 flags <- getFlags codegen

58 hdrs <- getHdrs codegen

64 hdrs <- getHdrs codegen

59 impdirs <- allImportDirs

65 impdirs <- allImportDirs

60− defsIn <- mkDecls tm reachableNames

66+ defsIn <- mkDecls reachableNames

67+ -- if no 'main term' given, generate interface files

68+ let iface = case mtm of

69+ Nothing -> True

70+ Just _ -> False

71+

61− let defs = defsIn ++ [(sMN 0 "runMain", maindef)]

72+ let defs = defsIn ++ maindef

62 -- iputStrLn $ showSep "\n" (map show defs)

73 -- iputStrLn $ showSep "\n" (map show defs)

63 -- Inlined top level LDecl made here

74 -- Inlined top level LDecl made here

64 let defsInlined = inlineAll defs

75 let defsInlined = inlineAll defs

@@ -89,12 +100,11 @@ compile codegen f tm

89 triple <- Idris.AbsSyntax.targetTriple

100 triple <- Idris.AbsSyntax.targetTriple

90 cpu <- Idris.AbsSyntax.targetCPU

101 cpu <- Idris.AbsSyntax.targetCPU

91 iLOG "Building output"

102 iLOG "Building output"

92−

93 case checked of

103 case checked of

94 OK c -> do return $ CodegenInfo f outty triple cpu

104 OK c -> do return $ CodegenInfo f outty triple cpu

95 hdrs impdirs objs libs flags

105 hdrs impdirs objs libs flags

96 NONE c (toAlist defuns)

106 NONE c (toAlist defuns)

97− tagged

107+ tagged iface exports

98-- runIO $ case codegen of

108-- runIO $ case codegen of

99-- ViaC -> codegenC cginfo

109-- ViaC -> codegenC cginfo

100-- ViaJava -> codegenJava cginfo

110-- ViaJava -> codegenJava cginfo

@@ -133,8 +143,8 @@ irMain tm = do

133 i <- irTerm M.empty [] tm

143 i <- irTerm M.empty [] tm

134 return $ LFun [] (sMN 0 "runMain") [] (LForce i)

144 return $ LFun [] (sMN 0 "runMain") [] (LForce i)

135

145

136−mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]

146+mkDecls :: [Name] -> Idris [(Name, LDecl)]

137−mkDecls t used

147+mkDecls used

138 = do i <- getIState

148 = do i <- getIState

139 let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)

149 let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)

140 decls <- mapM build ds

150 decls <- mapM build ds

src/IRTS/Exports.hsnew file+110

@@ -0,0 +1,110 @@

1+{-# LANGUAGE PatternGuards #-}

2+module IRTS.Exports(findExports, getExpNames) where

3+

4+import Idris.AbsSyntax

5+import Idris.Core.TT

6+import Idris.Core.CaseTree

7+import Idris.Core.Evaluate

8+import Idris.Error

9+import IRTS.Lang

10+

11+import Data.Maybe

12+

13+findExports :: Idris [ExportIFace]

14+findExports = do exps <- getExports

15+ es <- mapM toIFace exps

16+ logLvl 2 $ "Exporting " ++ show es

17+ return es

18+

19+getExpNames :: [ExportIFace] -> [Name]

20+getExpNames = concatMap expNames

21+

22+expNames :: ExportIFace -> [Name]

23+expNames (Export _ _ es) = mapMaybe fnames es

24+ where fnames (ExportData _) = Nothing

25+ fnames (ExportFun n _ _ _) = Just n

26+

27+toIFace :: Name -> Idris ExportIFace

28+toIFace n = do i <- getIState

29+ let ctxt = tt_ctxt i

30+ def <- case lookupDefExact n ctxt of

31+ Just (CaseOp _ _ _ _ _ cs)

32+ -> getExpList (snd (cases_compiletime cs))

33+ Nothing -> ifail "Can't happen [toIFace]"

34+ case lookupTyExact n ctxt of

35+ Just ty -> toIFaceTyVal ty def

36+ Nothing -> ifail "Can't happen [toIFace]"

37+ where

38+ getExpList (STerm t) = return t

39+ getExpList _ = ifail "Badly formed export list"

40+

41+toIFaceTyVal :: Type -> Term -> Idris ExportIFace

42+toIFaceTyVal ty tm

43+ | (P _ exp _, [P _ ffi _, Constant (Str hdr), _]) <- unApply ty

44+ = do tm' <- toIFaceVal tm

45+ return $ Export ffi hdr tm'

46+

47+toIFaceVal :: Term -> Idris [Export]

48+toIFaceVal tm

49+ | (P _ end _, _) <- unApply tm,

50+ end == sNS (sUN "End") ["FFI_Export"] = return []

51+ | (P _ fun _, [_,_,_,_,(P _ fn _),extnm,prf,rest]) <- unApply tm,

52+ fun == sNS (sUN "Fun") ["FFI_Export"]

53+ = do rest' <- toIFaceVal rest

54+ return $

55+ ExportFun fn (toFDesc extnm) (toFDescRet prf) (toFDescArgs prf)

56+ : rest'

57+ | (P _ dat _, [_,_,_,_,d,rest]) <- unApply tm,

58+ dat == sNS (sUN "Data") ["FFI_Export"]

59+ = do rest' <- toIFaceVal rest

60+ return $ ExportData (toFDesc d) : rest'

61+ | otherwise = ifail $ "Badly formed export list " ++ show tm

62+

63+toFDesc :: Term -> FDesc

64+toFDesc (Constant (Str str)) = FStr str

65+toFDesc tm

66+ | (P _ n _, []) <- unApply tm = FCon (deNS n)

67+ | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDesc as)

68+toFDesc _ = FUnknown

69+

70+toFDescRet :: Term -> FDesc

71+toFDescRet tm

72+ | (P _ ret _, [_,_,_,b]) <- unApply tm,

73+ ret == sNS (sUN "FFI_Ret") ["FFI_Export"]

74+ = toFDescBase b

75+ | (P _ io _, [_,_,_,b]) <- unApply tm,

76+ io == sNS (sUN "FFI_IO") ["FFI_Export"]

77+ = FIO $ toFDescBase b

78+ | (P _ fun _, [_,_,_,_,_,t]) <- unApply tm,

79+ fun == sNS (sUN "FFI_Fun") ["FFI_Export"]

80+ = toFDescRet t

81+ | otherwise = error "Badly formed export proof"

82+

83+toFDescBase :: Term -> FDesc

84+toFDescBase tm

85+ | (P _ prim _, [_, _, _, pdesc]) <- unApply tm,

86+ prim == sNS (sUN "FFI_Prim") ["FFI_Export"]

87+ = toFDescPrim pdesc

88+ | (P _ prim _, [_, _, _, ddesc, _]) <- unApply tm,

89+ prim == sNS (sUN "FFI_ExpType") ["FFI_Export"]

90+ = toFDescPrim ddesc

91+ | otherwise = error "Badly formed export type"

92+

93+toFDescArgs :: Term -> [FDesc]

94+toFDescArgs tm

95+ | (P _ fun _, [_,_,_,_,b,t]) <- unApply tm,

96+ fun == sNS (sUN "FFI_Fun") ["FFI_Export"]

97+ = toFDescBase b : toFDescArgs t

98+ | otherwise = []

99+

100+toFDescPrim (Constant (Str str)) = FStr str

101+toFDescPrim tm

102+ | (P _ n _, []) <- unApply tm = FCon (deNS n)

103+ | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDescPrim as)

104+toFDescPrim _ = FUnknown

105+

106+deNS (NS n _) = n

107+deNS n = n

108+

109+

110+

src/IRTS/Lang.hs+14−1

@@ -29,7 +29,7 @@ data LExp = LV LVar

29 Int Name [LExp]

30 | LCase CaseType LExp [LAlt]

31 | LConst Const

32− | LForeign FDesc -- Function descriptor

32+ | LForeign FDesc -- Function descriptor (usually name as string)

33 FDesc -- Return type descriptor

34 [(FDesc, LExp)] -- first LExp is the FFI type description

35 | LOp PrimFn [LExp]

@@ -40,9 +40,22 @@ data LExp = LV LVar

40data FDesc = FCon Name

41 | FStr String

42 | FUnknown

43+ | FIO FDesc

43 | FApp Name [FDesc]

44 | FApp Name [FDesc]

44 deriving (Show, Eq)

45 deriving (Show, Eq)

45

46

47+data Export = ExportData FDesc -- Exported data descriptor (usually string)

48+ | ExportFun Name -- Idris name

49+ FDesc -- Exported function descriptor

50+ FDesc -- Return type descriptor

51+ [FDesc] -- Argument types

52+ deriving (Show, Eq)

53+

54+data ExportIFace = Export Name -- FFI descriptor

55+ String -- interface file

56+ [Export]

57+ deriving (Show, Eq)

58+

46-- Primitive operators. Backends are not *required* to implement all

59-- Primitive operators. Backends are not *required* to implement all

47-- of these, but should report an error if they are unable

60-- of these, but should report an error if they are unable

48

61

src/Idris/AbsSyntax.hs+27−17

@@ -96,7 +96,7 @@ addHdr :: Codegen -> String -> Idris ()

96addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }

97

98addImported :: Bool -> FilePath -> Idris ()

99−addImported pub f

99+addImported pub f

100 = do i <- getIState

101 putIState $ i { idris_imported = nub $ (f, pub) : idris_imported i }

102

@@ -129,22 +129,30 @@ addErasureUsage :: Name -> Int -> Idris ()

129addErasureUsage n i = do ist <- getIState

130 putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }

131

132+addExport :: Name -> Idris ()

133+addExport n = do ist <- getIState

134+ putIState $ ist { idris_exports = n : idris_exports ist }

135+

132addUsedName :: FC -> Name -> Name -> Idris ()

136addUsedName :: FC -> Name -> Name -> Idris ()

133−addUsedName fc n arg

137+addUsedName fc n arg

134 = do ist <- getIState

138 = do ist <- getIState

135 case lookupTyName n (tt_ctxt ist) of

139 case lookupTyName n (tt_ctxt ist) of

136− [(_, ty)] -> addUsage 0 ty

140+ [(n', ty)] -> addUsage n' 0 ty

137 [] -> throwError (At fc (NoSuchVariable n))

141 [] -> throwError (At fc (NoSuchVariable n))

138 xs -> throwError (At fc (CantResolveAlts (map fst xs)))

142 xs -> throwError (At fc (CantResolveAlts (map fst xs)))

139− where addUsage i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))

143+ where addUsage n i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))

140− addErasureUsage n i

144+ addErasureUsage n i

141− | otherwise = addUsage (i + 1) sc

145+ | otherwise = addUsage n (i + 1) sc

142− addUsage _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))

146+ addUsage _ _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))

143

147

144getErasureUsage :: Idris [(Name, Int)]

148getErasureUsage :: Idris [(Name, Int)]

145getErasureUsage = do ist <- getIState;

149getErasureUsage = do ist <- getIState;

146 return (idris_erasureUsed ist)

150 return (idris_erasureUsed ist)

147

151

152+getExports :: Idris [Name]

153+getExports = do ist <- getIState

154+ return (idris_exports ist)

155+

148totcheck :: (FC, Name) -> Idris ()

156totcheck :: (FC, Name) -> Idris ()

149totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

157totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

150

158

@@ -260,7 +268,7 @@ addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts

260

268

261 where errWhen True

269 where errWhen True

262 = throwError (At fc

270 = throwError (At fc

263− (CantUnify False x y (Msg "") [] 0))

271+ (CantUnify False (x, Nothing) (y, Nothing) (Msg "") [] 0))

264 errWhen False = return ()

272 errWhen False = return ()

265

273

266isTyInferred :: Name -> Idris Bool

274isTyInferred :: Name -> Idris Bool

@@ -1074,8 +1082,8 @@ expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs decls)

1074 (map (mapsnd (expandParams dec ps ns [])) params)

1082 (map (mapsnd (expandParams dec ps ns [])) params)

1075 pDocs

1083 pDocs

1076 (map (expandParamsD rhs ist dec ps ns) decls)

1084 (map (expandParamsD rhs ist dec ps ns) decls)

1077−expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)

1085+expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n params ty cn decls)

1078− = PInstance info f

1086+ = PInstance doc argDocs info f

1079 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

1087 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

1080 n

1088 n

1081 (map (expandParams dec ps ns []) params)

1089 (map (expandParams dec ps ns []) params)

@@ -1292,8 +1300,10 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

1292 getImps (Bind n (Pi _ t _) sc) imps

1300 getImps (Bind n (Pi _ t _) sc) imps

1293 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

1301 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

1294 where

1302 where

1303+ argInfo n (Imp opt _ _ _) Placeholder

1304+ = (True, PImp 0 True opt n Placeholder)

1295 argInfo n (Imp opt _ _ _) t'

1305 argInfo n (Imp opt _ _ _) t'

1296− = (True, PImp (getPriority i t') True opt n t')

1306+ = (False, PImp (getPriority i t') True opt n t')

1297 argInfo n (Exp opt _ _) t'

1307 argInfo n (Exp opt _ _) t'

1298 = (InaccessibleArg `elem` opt,

1308 = (InaccessibleArg `elem` opt,

1299 PExp (getPriority i t') opt n t')

1309 PExp (getPriority i t') opt n t')

@@ -1542,7 +1552,7 @@ addImpl' inpat env infns ist ptm

1542 PLam fc n ty' sc'

1552 PLam fc n ty' sc'

1543 _ -> ai qq env ds (PLam fc (sMN 0 "lamp") ty

1553 _ -> ai qq env ds (PLam fc (sMN 0 "lamp") ty

1544 (PCase fc (PRef fc (sMN 0 "lamp") )

1554 (PCase fc (PRef fc (sMN 0 "lamp") )

1545− [(PRef fc n, sc)]))

1555+ [(PRef fc n, sc)]))

1546 ai qq env ds (PLet fc n ty val sc)

1556 ai qq env ds (PLet fc n ty val sc)

1547 = case lookupDef n (tt_ctxt ist) of

1557 = case lookupDef n (tt_ctxt ist) of

1548 [] -> let ty' = ai qq env ds ty

1558 [] -> let ty' = ai qq env ds ty

@@ -1716,7 +1726,7 @@ stripLinear i tm = evalState (sl tm) [] where

1716 sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')

1726 sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')

1717 sl (PDPair fc p l t r) = do l' <- sl l

1727 sl (PDPair fc p l t r) = do l' <- sl l

1718 t' <- sl t

1728 t' <- sl t

1719− r' <- sl r

1729+ r' <- sl r

1720 return (PDPair fc p l' t' r')

1730 return (PDPair fc p l' t' r')

1721 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var

1731 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var

1722 args' <- mapM slA args

1732 args' <- mapM slA args

@@ -1915,11 +1925,11 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1915 match (PHidden x) (PHidden y)

1925 match (PHidden x) (PHidden y)

1916 | RightOK xs <- match x y = return xs -- to collect variables

1926 | RightOK xs <- match x y = return xs -- to collect variables

1917 | otherwise = return [] -- Otherwise hidden things are unmatchable

1927 | otherwise = return [] -- Otherwise hidden things are unmatchable

1918− match (PHidden x) y

1928+ match (PHidden x) y

1919− | RightOK xs <- match x y = return xs

1929+ | RightOK xs <- match x y = return xs

1920 | otherwise = return []

1930 | otherwise = return []

1921− match x (PHidden y)

1931+ match x (PHidden y)

1922− | RightOK xs <- match x y = return xs

1932+ | RightOK xs <- match x y = return xs

1923 | otherwise = return []

1933 | otherwise = return []

1924 match (PUnifyLog x) y = match' x y

1934 match (PUnifyLog x) y = match' x y

1925 match x (PUnifyLog y) = match' x y

1935 match x (PUnifyLog y) = match' x y

src/Idris/AbsSyntaxTree.hs+35−28

@@ -57,7 +57,7 @@ data ElabInfo = EInfo { params :: [(Name, PTerm)],

57 liftname :: Name -> Name,

58 namespace :: Maybe [String],

59 elabFC :: Maybe FC,

60− rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->

60+ rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->

61 Idris () }

62

63toplevel :: ElabInfo

@@ -225,7 +225,8 @@ data IState = IState {

225 idris_callswho :: Maybe (M.Map Name [Name]),

226 idris_repl_defs :: [Name], -- ^ List of names that were defined in the repl, and can be re-/un-defined

227 elab_stack :: [Name], -- ^ Stack of names currently being elaborated

228− idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)

228+ idris_symbols :: M.Map Name Name, -- ^ Symbol table (preserves sharing of names)

229+ idris_exports :: [Name] -- ^ Functions with ExportList

229 }

230 }

230

231

231-- Required for parsers library, and therefore trifecta

232-- Required for parsers library, and therefore trifecta

@@ -297,6 +298,7 @@ data IBCWrite = IBCFix FixDecl

297 | IBCParsedRegion FC

298 | IBCParsedRegion FC

298 | IBCModDocs Name -- ^ The name is the special name used to track module docs

299 | IBCModDocs Name -- ^ The name is the special name used to track module docs

299 | IBCUsage (Name, Int)

300 | IBCUsage (Name, Int)

301+ | IBCExport Name

300 deriving Show

302 deriving Show

301

303

302-- | The initial state for the compiler

304-- | The initial state for the compiler

@@ -309,7 +311,7 @@ idrisInit = IState initContext [] []

309 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

311 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

310 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

312 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

311 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

313 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

312− AutomaticWidth S.empty [] Nothing Nothing [] [] M.empty

314+ AutomaticWidth S.empty [] Nothing Nothing [] [] M.empty []

313

315

314-- | The monad for the main REPL - reading and processing files and updating

316-- | The monad for the main REPL - reading and processing files and updating

315-- global state (hence the IO inner monad).

317-- global state (hence the IO inner monad).

@@ -419,6 +421,7 @@ data Opt = Filename String

419 | NoREPL

421 | NoREPL

420 | OLogging Int

422 | OLogging Int

421 | Output String

423 | Output String

424+ | Interface

422 | TypeCase

425 | TypeCase

423 | TypeInType

426 | TypeInType

424 | DefaultTotal

427 | DefaultTotal

@@ -598,19 +601,24 @@ data PDecl' t

598 [PDecl' t] -- declarations

601 [PDecl' t] -- declarations

599 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

602 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

600 -- class name, parameters, method declarations

603 -- class name, parameters, method declarations

604+ | PInstance

605+ (Docstring (Either Err PTerm)) -- Instance docs

606+ [(Name, Docstring (Either Err PTerm))] -- Parameter docs

607+ SyntaxInfo

601− | PInstance SyntaxInfo FC [(Name, t)] -- constraints

608+ FC [(Name, t)] -- constraints

602− Name -- class

609+ Name -- class

603− [t] -- parameters

610+ [t] -- parameters

604− t -- full instance type

611+ t -- full instance type

605− (Maybe Name) -- explicit name

612+ (Maybe Name) -- explicit name

606− [PDecl' t]

613+ [PDecl' t]

607− -- ^ Instance declaration: arguments are syntax info, source location, constraints,

614+ -- ^ Instance declaration: arguments are documentation, syntax info, source

615+ -- location, constraints, class name, parameters, full instance

608− -- class name, parameters, full instance type, optional explicit name, and definitions

616+ -- type, optional explicit name, and definitions

609 | PDSL Name (DSL' t) -- ^ DSL declaration

617 | PDSL Name (DSL' t) -- ^ DSL declaration

610 | PSyntax FC Syntax -- ^ Syntax definition

618 | PSyntax FC Syntax -- ^ Syntax definition

611 | PMutual FC [PDecl' t] -- ^ Mutual block

619 | PMutual FC [PDecl' t] -- ^ Mutual block

612 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.

620 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.

613− | PProvider SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term

621+ | PProvider (Docstring (Either Err PTerm)) SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term

614 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If

622 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If

615 -- bool is True, lhs and rhs must be convertible

623 -- bool is True, lhs and rhs must be convertible

616 deriving Functor

624 deriving Functor

@@ -685,7 +693,7 @@ declared (PParams _ _ ds) = concatMap declared ds

685declared (PNamespace _ ds) = concatMap declared ds

693declared (PNamespace _ ds) = concatMap declared ds

686declared (PRecord _ _ _ n _ _ _ c _) = [n, c]

694declared (PRecord _ _ _ n _ _ _ c _) = [n, c]

687declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms

695declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms

688−declared (PInstance _ _ _ _ _ _ _ _) = []

696+declared (PInstance _ _ _ _ _ _ _ _ _ _) = []

689declared (PDSL n _) = [n]

697declared (PDSL n _) = [n]

690declared (PSyntax _ _) = []

698declared (PSyntax _ _) = []

691declared (PMutual _ ds) = concatMap declared ds

699declared (PMutual _ ds) = concatMap declared ds

@@ -704,7 +712,7 @@ tldeclared (PParams _ _ ds) = []

704tldeclared (PMutual _ ds) = concatMap tldeclared ds

712tldeclared (PMutual _ ds) = concatMap tldeclared ds

705tldeclared (PNamespace _ ds) = concatMap tldeclared ds

713tldeclared (PNamespace _ ds) = concatMap tldeclared ds

706tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms

714tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms

707−tldeclared (PInstance _ _ _ _ _ _ _ _) = []

715+tldeclared (PInstance _ _ _ _ _ _ _ _ _ _) = []

708tldeclared _ = []

716tldeclared _ = []

709

717

710defined :: PDecl -> [Name]

718defined :: PDecl -> [Name]

@@ -720,7 +728,7 @@ defined (PParams _ _ ds) = concatMap defined ds

720defined (PNamespace _ ds) = concatMap defined ds

728defined (PNamespace _ ds) = concatMap defined ds

721defined (PRecord _ _ _ n _ _ _ c _) = [n, c]

729defined (PRecord _ _ _ n _ _ _ c _) = [n, c]

722defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms

730defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms

723−defined (PInstance _ _ _ _ _ _ _ _) = []

731+defined (PInstance _ _ _ _ _ _ _ _ _ _) = []

724defined (PDSL n _) = [n]

732defined (PDSL n _) = [n]

725defined (PSyntax _ _) = []

733defined (PSyntax _ _) = []

726defined (PMutual _ ds) = concatMap defined ds

734defined (PMutual _ ds) = concatMap defined ds

@@ -775,7 +783,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

775 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)

783 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)

776 | PHidden PTerm -- ^ Irrelevant or hidden pattern

784 | PHidden PTerm -- ^ Irrelevant or hidden pattern

777 | PType -- ^ 'Type' type

785 | PType -- ^ 'Type' type

778− | PUniverse Universe -- ^ Some universe

786+ | PUniverse Universe -- ^ Some universe

779 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions

787 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions

780 | PConstant Const -- ^ Builtin types

788 | PConstant Const -- ^ Builtin types

781 | Placeholder -- ^ Underscore

789 | Placeholder -- ^ Underscore

@@ -1110,7 +1118,7 @@ data SSymbol = Keyword Name

1110 | Expr Name

1118 | Expr Name

1111 | SimpleExpr Name

1119 | SimpleExpr Name

1112 deriving (Show, Eq)

1120 deriving (Show, Eq)

1113−

1121+

1114

1122

1115{-!

1123{-!

1116deriving instance Binary SSymbol

1124deriving instance Binary SSymbol

@@ -1385,7 +1393,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1385 where

1393 where

1386 startPrec = 0

1394 startPrec = 0

1387 funcAppPrec = 10

1395 funcAppPrec = 10

1388−

1396+

1389 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1397 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1390 prettySe p bnd (PQuote r) =

1398 prettySe p bnd (PQuote r) =

1391 text "![" <> pretty r <> text "]"

1399 text "![" <> pretty r <> text "]"

@@ -1448,7 +1456,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1448 [x] -> group (opName True <$> group (prettySe startPrec bnd (getTm x)))

1456 [x] -> group (opName True <$> group (prettySe startPrec bnd (getTm x)))

1449 [l,r] -> let precedence = maybe (startPrec - 1) prec f

1457 [l,r] -> let precedence = maybe (startPrec - 1) prec f

1450 in bracket p precedence $ inFix (getTm l) (getTm r)

1458 in bracket p precedence $ inFix (getTm l) (getTm r)

1451− (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->

1459+ (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->

1452 bracket p funcAppPrec $

1460 bracket p funcAppPrec $

1453 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>

1461 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>

1454 align (group (vsep (map (prettyArgS bnd) rest)))

1462 align (group (vsep (map (prettyArgS bnd) rest)))

@@ -1464,7 +1472,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1464 Just (Infixr p') -> p'

1472 Just (Infixr p') -> p'

1465 Just f' -> prec f' + 1

1473 Just f' -> prec f' + 1

1466 inFix l r = align . group $

1474 inFix l r = align . group $

1467− (prettySe left bnd l <+> opName False) <$>

1475+ (prettySe left bnd l <+> opName False) <$>

1468 group (prettySe right bnd r)

1476 group (prettySe right bnd r)

1469 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo

1477 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo

1470 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1478 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

@@ -1483,7 +1491,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1483 align $ kwd "case" <+> prettySe startPrec bnd scr <+> kwd "of" <$>

1491 align $ kwd "case" <+> prettySe startPrec bnd scr <+> kwd "of" <$>

1484 indent 2 (vsep (map ppcase cases))

1492 indent 2 (vsep (map ppcase cases))

1485 where

1493 where

1486− ppcase (l, r) = let prettyCase = prettySe startPrec

1494+ ppcase (l, r) = let prettyCase = prettySe startPrec

1487 ([(n, False) | n <- vars l] ++ bnd)

1495 ([(n, False) | n <- vars l] ++ bnd)

1488 in nest nestingSize $

1496 in nest nestingSize $

1489 prettyCase l <+> text "=>" <+> prettyCase r

1497 prettyCase l <+> text "=>" <+> prettyCase r

@@ -1554,7 +1562,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1554 prettyAs =

1562 prettyAs =

1555 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as

1563 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as

1556 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"

1564 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"

1557− prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)

1565+ prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)

1558 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))

1566 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))

1559 -- XXX: add pretty for tactics

1567 -- XXX: add pretty for tactics

1560 prettySe p bnd (PProof ts) =

1568 prettySe p bnd (PProof ts) =

@@ -1720,7 +1728,7 @@ showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <>

1720showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1728showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1721showDeclImp o (PClass _ _ _ cs n ps _ ds)

1729showDeclImp o (PClass _ _ _ cs n ps _ ds)

1722 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

1730 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

1723−showDeclImp o (PInstance _ _ cs n _ t _ ds)

1731+showDeclImp o (PInstance _ _ _ _ cs n _ t _ ds)

1724 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

1732 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

1725showDeclImp _ _ = text "..."

1733showDeclImp _ _ = text "..."

1726-- showDeclImp (PImport o) = "import " ++ o

1734-- showDeclImp (PImport o) = "import " ++ o

@@ -1896,16 +1904,16 @@ implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

1896implicitNamesIn uvars ist tm = nub $ ni [] tm

1904implicitNamesIn uvars ist tm = nub $ ni [] tm

1897 where

1905 where

1898 ni env (PRef _ n)

1906 ni env (PRef _ n)

1899− | not (n `elem` env)

1907+ | not (n `elem` env)

1900 = case lookupTy n (tt_ctxt ist) of

1908 = case lookupTy n (tt_ctxt ist) of

1901 [] -> [n]

1909 [] -> [n]

1902 _ -> if n `elem` uvars then [n] else []

1910 _ -> if n `elem` uvars then [n] else []

1903− ni env (PApp _ f@(PRef _ n) as)

1911+ ni env (PApp _ f@(PRef _ n) as)

1904 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)

1912 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)

1905 | otherwise = concatMap (ni env) (map getTm as)

1913 | otherwise = concatMap (ni env) (map getTm as)

1906 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1914 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1907 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1915 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1908− ni env (PCase _ c os) = ni env c ++

1916+ ni env (PCase _ c os) = ni env c ++

1909 -- names in 'os', not counting the names bound in the cases

1917 -- names in 'os', not counting the names bound in the cases

1910 (nub (concatMap (ni env) (map snd os))

1918 (nub (concatMap (ni env) (map snd os))

1911 \\ nub (concatMap (ni env) (map fst os)))

1919 \\ nub (concatMap (ni env) (map fst os)))

@@ -1935,7 +1943,7 @@ namesIn uvars ist tm = nub $ ni [] tm

1935 _ -> if n `elem` (map fst uvars) then [n] else []

1943 _ -> if n `elem` (map fst uvars) then [n] else []

1936 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1944 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1937 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1945 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1938− ni env (PCase _ c os) = ni env c ++

1946+ ni env (PCase _ c os) = ni env c ++

1939 -- names in 'os', not counting the names bound in the cases

1947 -- names in 'os', not counting the names bound in the cases

1940 (nub (concatMap (ni env) (map snd os))

1948 (nub (concatMap (ni env) (map snd os))

1941 \\ nub (concatMap (ni env) (map fst os)))

1949 \\ nub (concatMap (ni env) (map fst os)))

@@ -1994,4 +2002,3 @@ getErasureInfo ist n =

1994 case lookupCtxtExact n (idris_optimisation ist) of

2002 case lookupCtxtExact n (idris_optimisation ist) of

1995 Just (Optimise inacc detagg) -> map fst inacc

2003 Just (Optimise inacc detagg) -> map fst inacc

1996 Nothing -> []

2004 Nothing -> []

1997−

src/Idris/CmdOptions.hs+1

@@ -83,6 +83,7 @@ parseFlags = many $

83 <|> flag' NoREPL (long "check" <> help "Typecheck only, don't start the REPL")

84 <|> (Output <$> strOption (short 'o' <> long "output" <> metavar "FILE" <> help "Specify output file"))

85 -- <|> flag' TypeCase (long "typecase")

86+ <|> flag' Interface (long "interface" <> help "Generate interface files from ExportLists")

86 <|> flag' TypeInType (long "typeintype")

87 <|> flag' TypeInType (long "typeintype")

87 <|> flag' DefaultTotal (long "total" <> help "Require functions to be total by default")

88 <|> flag' DefaultTotal (long "total" <> help "Require functions to be total by default")

88 <|> flag' DefaultPartial (long "partial")

89 <|> flag' DefaultPartial (long "partial")

src/Idris/Core/Binary.hs+12

@@ -23,6 +23,18 @@ instance Binary ErrorReportPart where

23 3 -> fmap SubReport get

24 _ -> error "Corrupted binary data for ErrorReportPart"

25

26+instance Binary Provenance where

27+ put ExpectedType = putWord8 0

28+ put (SourceTerm t) = do putWord8 1

29+ put t

30+

31+ get = do i <- getWord8

32+ case i of

33+ 0 -> return ExpectedType

34+ 1 -> do x1 <- get

35+ return (SourceTerm x1)

36+ _ -> error "Corrupted binary data for Provenance"

37+

26instance Binary a => Binary (Err' a) where

38instance Binary a => Binary (Err' a) where

27 put (Msg str) = do putWord8 0

39 put (Msg str) = do putWord8 0

28 put str

40 put str

src/Idris/Core/Constraints.hs+2−1

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

8import Control.Arrow

9import Control.Monad.RWS

10import Control.Monad.State

11+import qualified Data.Set as S

11import Data.List

12import Data.List

12import Data.Maybe

13import Data.Maybe

13import qualified Data.Map.Strict as M

14import qualified Data.Map.Strict as M

@@ -19,7 +20,7 @@ ucheck :: [(UConstraint, FC)] -> TC ()

19ucheck cs = acyclic rels (map fst (M.toList rels))

20ucheck cs = acyclic rels (map fst (M.toList rels))

20 where lhs (ULT l _) = l

21 where lhs (ULT l _) = l

21 lhs (ULE l _) = l

22 lhs (ULE l _) = l

22− cs' = nub cs

23+ cs' = S.toList (S.fromList cs)

23 rels = mkRels cs' M.empty

24 rels = mkRels cs' M.empty

24

25

25type Relations = M.Map UExp [(UConstraint, FC)]

26type Relations = M.Map UExp [(UConstraint, FC)]

src/Idris/Core/DeepSeq.hs+4

@@ -43,6 +43,10 @@ instance NFData Raw where

43instance NFData FC where

44 rnf (FC x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

45

46+instance NFData Provenance where

47+ rnf ExpectedType = ()

48+ rnf (SourceTerm x1) = rnf x1 `seq` ()

49+

46instance NFData Err where

50instance NFData Err where

47 rnf (Msg x1) = rnf x1 `seq` ()

51 rnf (Msg x1) = rnf x1 `seq` ()

48 rnf (InternalMsg x1) = rnf x1 `seq` ()

52 rnf (InternalMsg x1) = rnf x1 `seq` ()

src/Idris/Core/Elaborate.hs+3−2

@@ -727,10 +727,11 @@ no_errors tac err

727 if (length ps' > length ps) then

728 case reverse ps' of

729 ((x, y, _, env, inerr, while, _) : _) ->

730+ let (xp, yp) = getProvenance inerr

730− let env' = map (\(x, b) -> (x, binderTy b)) env in

731+ env' = map (\(x, b) -> (x, binderTy b)) env in

731 lift $ tfail $

732 lift $ tfail $

732 case err of

733 case err of

733− Nothing -> CantUnify False x y inerr env' 0

734+ Nothing -> CantUnify False (x, xp) (y, yp) inerr env' 0

734 Just e -> e

735 Just e -> e

735 else return $! ()

736 else return $! ()

736

737

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

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

9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

10 addDatatype, addCasedef, simplifyCasedef, addOperator,

11 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

12− lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

12+ lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

13 mapDefCtxt,

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

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

@@ -1007,7 +1007,10 @@ isTCDict n ctxt

1007 _ -> False

1008

1009lookupP :: Name -> Context -> [Term]

1010−lookupP n ctxt

1010+lookupP = lookupP_all False

1011+

1012+lookupP_all :: Bool -> Name -> Context -> [Term]

1013+lookupP_all all n ctxt

1011 = do def <- lookupCtxt n (definitions ctxt)

1014 = do def <- lookupCtxt n (definitions ctxt)

1012 p <- case def of

1015 p <- case def of

1013 (Function ty tm, a, _, _) -> return (P Ref n ty, a)

1016 (Function ty tm, a, _, _) -> return (P Ref n ty, a)

@@ -1015,7 +1018,7 @@ lookupP n ctxt

1015 (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n ty, a)

1018 (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n ty, a)

1016 (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)

1019 (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)

1017 case snd p of

1020 case snd p of

1018− Hidden -> []

1021+ Hidden -> if all then return (fst p) else []

1019 _ -> return (fst p)

1022 _ -> return (fst p)

1020

1023

1021lookupDefExact :: Name -> Context -> Maybe Def

1024lookupDefExact :: Name -> Context -> Maybe Def

src/Idris/Core/ProofState.hs+32−21

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

6

7module Idris.Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,

8 Tactic(..), Goal(..), processTactic, nowElaboratingPS, doneElaboratingAppPS,

9− doneElaboratingArgPS, dropGiven, keepGiven) where

9+ doneElaboratingArgPS, dropGiven, keepGiven, getProvenance) where

10

11import Idris.Core.Typecheck

12import Idris.Core.Evaluate

@@ -154,9 +154,11 @@ holeName i = sMN i "hole"

154qshow :: Fails -> String

155qshow fs = show (map (\ (x, y, hs, _, _, _, t) -> (t, x, y, hs)) fs)

156

157−match_unify' :: Context -> Env -> TT Name -> TT Name ->

157+match_unify' :: Context -> Env ->

158+ (TT Name, Maybe Provenance) ->

159+ (TT Name, Maybe Provenance) ->

158 StateT TState TC [(Name, TT Name)]

160 StateT TState TC [(Name, TT Name)]

159−match_unify' ctxt env topx topy =

161+match_unify' ctxt env (topx, xfrom) (topy, yfrom) =

160 do ps <- get

162 do ps <- get

161 let while = while_elaborating ps

163 let while = while_elaborating ps

162 let dont = dontunify ps

164 let dont = dontunify ps

@@ -168,7 +170,7 @@ match_unify' ctxt env topx topy =

168 ++ "\n"

170 ++ "\n"

169 ++ "\n" ++ show (getProofTerm (pterm ps)) ++ "\n\n"

171 ++ "\n" ++ show (getProofTerm (pterm ps)) ++ "\n\n"

170 ) $

172 ) $

171− case match_unify ctxt env topx topy inj (holes ps) while of

173+ case match_unify ctxt env (topx, xfrom) (topy, yfrom) inj (holes ps) while of

172 OK u -> traceWhen (unifylog ps)

174 OK u -> traceWhen (unifylog ps)

173 ("Matched " ++ show u) $

175 ("Matched " ++ show u) $

174 do let (h, ns) = unified ps

176 do let (h, ns) = unified ps

@@ -196,14 +198,16 @@ mergeSolutions env ns = merge [] ns

196 = do ps <- get

198 = do ps <- get

197 let probs = problems ps

199 let probs = problems ps

198 put (ps { problems = probs ++ [(t,t',True,env,

200 put (ps { problems = probs ++ [(t,t',True,env,

199− CantUnify True t t' (Msg "") (errEnv env) 0,

201+ CantUnify True (t, Nothing) (t', Nothing) (Msg "") (errEnv env) 0,

200 [], Unify)] })

202 [], Unify)] })

201 merge acc ns

203 merge acc ns

202 | otherwise = merge ((n, t): acc) ns

204 | otherwise = merge ((n, t): acc) ns

203

205

204−unify' :: Context -> Env -> TT Name -> TT Name ->

206+unify' :: Context -> Env ->

207+ (TT Name, Maybe Provenance) ->

208+ (TT Name, Maybe Provenance) ->

205 StateT TState TC [(Name, TT Name)]

209 StateT TState TC [(Name, TT Name)]

206−unify' ctxt env topx topy =

210+unify' ctxt env (topx, xfrom) (topy, yfrom) =

207 do ps <- get

211 do ps <- get

208 let while = while_elaborating ps

212 let while = while_elaborating ps

209 let dont = dontunify ps

213 let dont = dontunify ps

@@ -216,7 +220,7 @@ unify' ctxt env topx topy =

216 "\nHoles: " ++ show (holes ps)

220 "\nHoles: " ++ show (holes ps)

217 ++ "\nInjective: " ++ show (injective ps)

221 ++ "\nInjective: " ++ show (injective ps)

218 ++ "\n") $

222 ++ "\n") $

219− lift $ unify ctxt env topx topy inj (holes ps)

223+ lift $ unify ctxt env (topx, xfrom) (topy, yfrom) inj (holes ps)

220 (map fst (notunified ps)) while

224 (map fst (notunified ps)) while

221 let notu = filter (\ (n, t) -> case t of

225 let notu = filter (\ (n, t) -> case t of

222-- P _ _ _ -> False

226-- P _ _ _ -> False

@@ -456,7 +460,7 @@ regret ctxt env (Bind x (Hole t) _)

456unifyGoal :: Raw -> RunTactic

460unifyGoal :: Raw -> RunTactic

457unifyGoal tm ctxt env h@(Bind x b sc) =

461unifyGoal tm ctxt env h@(Bind x b sc) =

458 do (tmv, _) <- lift $ check ctxt env tm

462 do (tmv, _) <- lift $ check ctxt env tm

459− ns' <- unify' ctxt env (binderTy b) tmv

463+ ns' <- unify' ctxt env (binderTy b, Nothing) (tmv, Nothing)

460 return h

464 return h

461

465

462exact :: Raw -> RunTactic

466exact :: Raw -> RunTactic

@@ -473,7 +477,8 @@ fill guess ctxt env (Bind x (Hole ty) sc) =

473 do (val, valty) <- lift $ check ctxt env guess

477 do (val, valty) <- lift $ check ctxt env guess

474-- let valtyn = normalise ctxt env valty

478-- let valtyn = normalise ctxt env valty

475-- let tyn = normalise ctxt env ty

479-- let tyn = normalise ctxt env ty

476− ns <- unify' ctxt env valty ty

480+ ns <- unify' ctxt env (valty, Just $ SourceTerm val)

481+ (ty, Just ExpectedType)

477 ps <- get

482 ps <- get

478 let (uh, uns) = unified ps

483 let (uh, uns) = unified ps

479-- put (ps { unified = (uh, uns ++ ns) })

484-- put (ps { unified = (uh, uns ++ ns) })

@@ -488,7 +493,7 @@ match_fill guess ctxt env (Bind x (Hole ty) sc) =

488 do (val, valty) <- lift $ check ctxt env guess

493 do (val, valty) <- lift $ check ctxt env guess

489-- let valtyn = normalise ctxt env valty

494-- let valtyn = normalise ctxt env valty

490-- let tyn = normalise ctxt env ty

495-- let tyn = normalise ctxt env ty

491− ns <- match_unify' ctxt env valty ty

496+ ns <- match_unify' ctxt env (valty, Nothing) (ty, Nothing)

492 ps <- get

497 ps <- get

493 let (uh, uns) = unified ps

498 let (uh, uns) = unified ps

494-- put (ps { unified = (uh, uns ++ ns) })

499-- put (ps { unified = (uh, uns ++ ns) })

@@ -506,7 +511,7 @@ complete_fill :: RunTactic

506complete_fill ctxt env (Bind x (Guess ty val) sc) =

511complete_fill ctxt env (Bind x (Guess ty val) sc) =

507 do let guess = forget val

512 do let guess = forget val

508 (val', valty) <- lift $ check ctxt env guess

513 (val', valty) <- lift $ check ctxt env guess

509− ns <- unify' ctxt env valty ty

514+ ns <- unify' ctxt env (valty, Nothing) (ty, Nothing)

510 ps <- get

515 ps <- get

511 let (uh, uns) = unified ps

516 let (uh, uns) = unified ps

512-- put (ps { unified = (uh, uns ++ ns) })

517-- put (ps { unified = (uh, uns ++ ns) })

@@ -524,7 +529,7 @@ solve ctxt env (Bind x (Guess ty val) sc)

524 dropdots <-

529 dropdots <-

525 case lookup x (notunified ps) of

530 case lookup x (notunified ps) of

526 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $

531 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $

527− do match_unify' ctxt env tm val

532+ do match_unify' ctxt env (tm, Nothing) (val, Nothing)

528 return [x]

533 return [x]

529 _ -> return []

534 _ -> return []

530 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $

535 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $

@@ -567,7 +572,7 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

567-- ns <- lift $ unify ctxt env tyv t'

572-- ns <- lift $ unify ctxt env tyv t'

568 case t' of

573 case t' of

569 Bind y (Pi _ s _) t -> let t' = subst y (P Bound n s) t in

574 Bind y (Pi _ s _) t -> let t' = subst y (P Bound n s) t in

570− do ns <- unify' ctxt env s tyv

575+ do ns <- unify' ctxt env (s, Nothing) (tyv, Nothing)

571 ps <- get

576 ps <- get

572 let (uh, uns) = unified ps

577 let (uh, uns) = unified ps

573-- put (ps { unified = (uh, uns ++ ns) })

578-- put (ps { unified = (uh, uns ++ ns) })

@@ -593,8 +598,8 @@ intro n ctxt env _ = fail "Can't introduce here."

593forall :: Name -> Maybe ImplicitInfo -> Raw -> RunTactic

598forall :: Name -> Maybe ImplicitInfo -> Raw -> RunTactic

594forall n impl ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

599forall n impl ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

595 do (tyv, tyt) <- lift $ check ctxt env ty

600 do (tyv, tyt) <- lift $ check ctxt env ty

596− unify' ctxt env tyt (TType (UVar 0))

601+ unify' ctxt env (tyt, Nothing) (TType (UVar 0), Nothing)

597− unify' ctxt env t (TType (UVar 0))

602+ unify' ctxt env (t, Nothing) (TType (UVar 0), Nothing)

598 return $ Bind n (Pi impl tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))

603 return $ Bind n (Pi impl tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))

599forall n impl ty ctxt env _ = fail "Can't pi bind here"

604forall n impl ty ctxt env _ = fail "Can't pi bind here"

600

605

@@ -822,8 +827,8 @@ updateError ns (At f e) = At f (updateError ns e)

822updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)

827updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)

823updateError ns (ElaboratingArg f a env e)

828updateError ns (ElaboratingArg f a env e)

824 = ElaboratingArg f a env (updateError ns e)

829 = ElaboratingArg f a env (updateError ns e)

825−updateError ns (CantUnify b l r e xs sc)

830+updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)

826− = CantUnify b (updateSolvedTerm ns l) (updateSolvedTerm ns r) (updateError ns e) xs sc

831+ = CantUnify b (updateSolvedTerm ns l, lp) (updateSolvedTerm ns r, rp) (updateError ns e) xs sc

827updateError ns e = e

832updateError ns e = e

828

833

829solveInProblems x val [] = []

834solveInProblems x val [] = []

@@ -837,7 +842,7 @@ mergeNotunified env holes ns = mnu ns [] [] where

837 mnu ((n, t):ns) ns_acc ps_acc

842 mnu ((n, t):ns) ns_acc ps_acc

838 | Just t' <- lookup n ns, t /= t'

843 | Just t' <- lookup n ns, t /= t'

839 = mnu ns ((n,t') : ns_acc)

844 = mnu ns ((n,t') : ns_acc)

840− ((t,t',True, env,CantUnify True t t' (Msg "") [] 0, [],Match) : ps_acc)

845+ ((t,t',True, env,CantUnify True (t, Nothing) (t', Nothing) (Msg "") [] 0, [],Match) : ps_acc)

841 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc

846 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc

842

847

843updateNotunified [] nu = nu

848updateNotunified [] nu = nu

@@ -846,6 +851,10 @@ updateNotunified ns nu = up nu where

846 up ((n, t) : nus) = let t' = updateSolvedTerm ns t in

851 up ((n, t) : nus) = let t' = updateSolvedTerm ns t in

847 ((n, t') : up nus)

852 ((n, t') : up nus)

848

853

854+getProvenance :: Err -> (Maybe Provenance, Maybe Provenance)

855+getProvenance (CantUnify _ (_, lp) (_, rp) _ _ _) = (lp, rp)

856+getProvenance _ = (Nothing, Nothing)

857+

849updateProblems :: ProofState -> [(Name, TT Name)] -> Fails

858updateProblems :: ProofState -> [(Name, TT Name)] -> Fails

850 -> ([(Name, TT Name)], Fails)

859 -> ([(Name, TT Name)], Fails)

851-- updateProblems ctxt [] ps inj holes = ([], ps)

860-- updateProblems ctxt [] ps inj holes = ([], ps)

@@ -860,11 +869,12 @@ updateProblems ps updates probs = up updates probs where

860 up ns (prob@(x, y, ready, env, err, while, um) : ps) =

869 up ns (prob@(x, y, ready, env, err, while, um) : ps) =

861 let (x', newx) = updateSolvedTerm' ns x

870 let (x', newx) = updateSolvedTerm' ns x

862 (y', newy) = updateSolvedTerm' ns y

871 (y', newy) = updateSolvedTerm' ns y

872+ (lp, rp) = getProvenance err

863 err' = updateError ns err

873 err' = updateError ns err

864 env' = updateEnv ns env in

874 env' = updateEnv ns env in

865 if newx || newy || ready ||

875 if newx || newy || ready ||

866 any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then

876 any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then

867− case unify ctxt env' x' y' inj hs usupp while of

877+ case unify ctxt env' (x', lp) (y', rp) inj hs usupp while of

868 OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v)) $

878 OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v)) $

869 up (ns ++ v) ps

879 up (ns ++ v) ps

870 e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $

880 e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $

@@ -887,9 +897,10 @@ matchProblems all ps updates probs = up updates probs where

887 | all || um == Match =

897 | all || um == Match =

888 let x' = updateSolvedTerm ns x

898 let x' = updateSolvedTerm ns x

889 y' = updateSolvedTerm ns y

899 y' = updateSolvedTerm ns y

900+ (lp, rp) = getProvenance err

890 err' = updateError ns err

901 err' = updateError ns err

891 env' = updateEnv ns env in

902 env' = updateEnv ns env in

892− case match_unify ctxt env' x' y' inj hs while of

903+ case match_unify ctxt env' (x', lp) (y', rp) inj hs while of

893 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

904 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

894 up (ns ++ v) ps

905 up (ns ++ v) ps

895 _ -> let (ns', ps') = up ns ps in

906 _ -> let (ns', ps') = up ns ps in

src/Idris/Core/TT.hs+15−5

@@ -53,7 +53,7 @@ data FC = FC { fc_fname :: String, -- ^ Filename

53 fc_start :: (Int, Int), -- ^ Line and column numbers for the start of the location span

54 fc_end :: (Int, Int) -- ^ Line and column numbers for the end of the location span

55 }

56− deriving (Data, Typeable)

56+ deriving (Data, Typeable, Ord)

57

58-- | Ignore source location equality (so deriving classes do not compare FCs)

59instance Eq FC where

@@ -120,12 +120,22 @@ data ErrorReportPart = TextPart String

120-- Please remember to keep Err synchronised with

121-- Language.Reflection.Errors.Err in the stdlib!

122

123+data Provenance = ExpectedType

124+ | SourceTerm Term

125+ deriving (Show, Eq, Data, Typeable)

126+{-!

127+deriving instance NFData Err

128+deriving instance Binary Err

129+!-}

130+

123-- | Idris errors. Used as exceptions in the compiler, but reported to users

131-- | Idris errors. Used as exceptions in the compiler, but reported to users

124-- if they reach the top level.

132-- if they reach the top level.

125data Err' t

133data Err' t

126 = Msg String

134 = Msg String

127 | InternalMsg String

135 | InternalMsg String

136+ | CantUnify Bool (t, Maybe Provenance) -- Expected type, provenance

137+ (t, Maybe Provenance) -- Actual type, provenance

128− | CantUnify Bool t t (Err' t) [(Name, t)] Int

138+ (Err' t) [(Name, t)] Int

129 -- Int is 'score' - how much we did unify

139 -- Int is 'score' - how much we did unify

130 -- Bool indicates recoverability, True indicates more info may make

140 -- Bool indicates recoverability, True indicates more info may make

131 -- unification succeed

141 -- unification succeed

@@ -211,7 +221,7 @@ instance Sized ErrorReportPart where

211instance Sized Err where

221instance Sized Err where

212 size (Msg msg) = length msg

222 size (Msg msg) = length msg

213 size (InternalMsg msg) = length msg

223 size (InternalMsg msg) = length msg

214− size (CantUnify _ left right err _ score) = size left + size right + size err

224+ size (CantUnify _ left right err _ score) = size (fst left) + size (fst right) + size err

215 size (InfiniteUnify _ right _) = size right

225 size (InfiniteUnify _ right _) = size right

216 size (CantConvert left right _) = size left + size right

226 size (CantConvert left right _) = size left + size right

217 size (UnifyScope _ _ right _) = size right

227 size (UnifyScope _ _ right _) = size right

@@ -263,7 +273,7 @@ instance Show Err where

263

273

264instance Pretty Err OutputAnnotation where

274instance Pretty Err OutputAnnotation where

265 pretty (Msg m) = text m

275 pretty (Msg m) = text m

266− pretty (CantUnify _ l r e _ i) =

276+ pretty (CantUnify _ (l, _) (r, _) e _ i) =

267 text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r <+>

277 text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r <+>

268 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

278 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

269 pretty (ProviderError msg) = text msg

279 pretty (ProviderError msg) = text msg

@@ -783,7 +793,7 @@ instance Show UExp where

783-- | Universe constraints

793-- | Universe constraints

784data UConstraint = ULT UExp UExp -- ^ Strictly less than

794data UConstraint = ULT UExp UExp -- ^ Strictly less than

785 | ULE UExp UExp -- ^ Less than or equal to

795 | ULE UExp UExp -- ^ Less than or equal to

786− deriving Eq

796+ deriving (Eq, Ord)

787

797

788instance Show UConstraint where

798instance Show UConstraint where

789 show (ULT x y) = show x ++ " < " ++ show y

799 show (ULT x y) = show x ++ " < " ++ show y

src/Idris/Core/Typecheck.hs+4−1

@@ -81,7 +81,10 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

81 Env -> Raw -> StateT UCs TC (Term, Type)

82 chk u env (Var n)

83 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

84+ -- If we're elaborating, we don't want the private names; if we're

85+ -- checking an already elaborated term, we do

86+ | (P nt n' ty : _) <- lookupP_all (not holes) n ctxt

84− | (P nt n' ty : _) <- lookupP n ctxt = return (P nt n' ty, ty)

87+ = return (P nt n' ty, ty)

85 | otherwise = do lift $ tfail $ NoSuchVariable n

88 | otherwise = do lift $ tfail $ NoSuchVariable n

86 chk u env ap@(RApp f a)

89 chk u env ap@(RApp f a)

87 = do (fv, fty) <- chk u env f

90 = do (fv, fty) <- chk u env f

src/Idris/Core/Unify.hs+29−21

@@ -51,7 +51,7 @@ data UResult a = UOK a

51 | UFail Err

52

53-- | Smart constructor for unification errors that takes into account the FailContext

54−cantUnify :: [FailContext] -> Bool -> t -> t -> (Err' t) -> [(Name, t)] -> Int -> Err' t

54+cantUnify :: [FailContext] -> Bool -> (t, Maybe Provenance) -> (t, Maybe Provenance) -> (Err' t) -> [(Name, t)] -> Int -> Err' t

55cantUnify [] r t1 t2 e ctxt i = CantUnify r t1 t2 e ctxt i

56cantUnify (FailContext fc f x : prev) r t1 t2 e ctxt i =

57 At fc (ElaboratingArg f x

@@ -61,13 +61,15 @@ cantUnify (FailContext fc f x : prev) r t1 t2 e ctxt i =

61-- Solve metavariables by matching terms against each other

62-- Not really unification, of course!

63

64−match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] -> [FailContext] ->

64+match_unify :: Context -> Env ->

65+ (TT Name, Maybe Provenance) ->

66+ (TT Name, Maybe Provenance) -> [Name] -> [Name] -> [FailContext] ->

65 TC [(Name, TT Name)]

67 TC [(Name, TT Name)]

66−match_unify ctxt env topx topy inj holes from =

68+match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

67 case runStateT (un [] (renameBindersTm env topx)

69 case runStateT (un [] (renameBindersTm env topx)

68 (renameBindersTm env topy)) (UI 0 []) of

70 (renameBindersTm env topy)) (UI 0 []) of

69 OK (v, UI _ []) ->

71 OK (v, UI _ []) ->

70− do v' <- trimSolutions topx topy from env v

72+ do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v

71 return (map (renameBinders env) v')

73 return (map (renameBinders env) v')

72 res ->

74 res ->

73 let topxn = renameBindersTm env (normalise ctxt env topx)

75 let topxn = renameBindersTm env (normalise ctxt env topx)

@@ -75,14 +77,14 @@ match_unify ctxt env topx topy inj holes from =

75 case runStateT (un [] topxn topyn)

77 case runStateT (un [] topxn topyn)

76 (UI 0 []) of

78 (UI 0 []) of

77 OK (v, UI _ fails) ->

79 OK (v, UI _ fails) ->

78− do v' <- trimSolutions topx topy from env v

80+ do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v

79 return (map (renameBinders env) v')

81 return (map (renameBinders env) v')

80 Error e ->

82 Error e ->

81 -- just normalise the term we're matching against

83 -- just normalise the term we're matching against

82 case runStateT (un [] topxn topy)

84 case runStateT (un [] topxn topy)

83 (UI 0 []) of

85 (UI 0 []) of

84 OK (v, UI _ fails) ->

86 OK (v, UI _ fails) ->

85− do v' <- trimSolutions topx topy from env v

87+ do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v

86 return (map (renameBinders env) v')

88 return (map (renameBinders env) v')

87 _ -> tfail e

89 _ -> tfail e

88 where

90 where

@@ -143,7 +145,7 @@ match_unify ctxt env topx topy inj holes from =

143 let r = recoverable (normalise ctxt env x)

145 let r = recoverable (normalise ctxt env x)

144 (normalise ctxt env y)

146 (normalise ctxt env y)

145 let err = cantUnify from r

147 let err = cantUnify from r

146− topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

148+ (topx, xfrom) (topy, yfrom) (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s

147 if (not r) then lift $ tfail err

149 if (not r) then lift $ tfail err

148 else do put (UI s ((x, y, True, env, err, from, Match) : f))

150 else do put (UI s ((x, y, True, env, err, from, Match) : f))

149 lift $ tfail err

151 lift $ tfail err

@@ -157,8 +159,9 @@ match_unify ctxt env topx topy inj holes from =

157 uB bnames x y = do UI s f <- get

159 uB bnames x y = do UI s f <- get

158 let r = recoverable (normalise ctxt env (binderTy x))

160 let r = recoverable (normalise ctxt env (binderTy x))

159 (normalise ctxt env (binderTy y))

161 (normalise ctxt env (binderTy y))

160− let err = cantUnify from r topx topy

162+ let err = cantUnify from r (topx, xfrom) (topy, yfrom)

163+ (CantUnify r (binderTy x, Nothing)

161− (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

164+ (binderTy y, Nothing) (Msg "") (errEnv env) s)

162 (errEnv env) s

165 (errEnv env) s

163 put (UI s ((binderTy x, binderTy y,

166 put (UI s ((binderTy x, binderTy y,

164 False,

167 False,

@@ -179,7 +182,8 @@ match_unify ctxt env topx topy inj holes from =

179 let r = recoverable (normalise ctxt env x)

182 let r = recoverable (normalise ctxt env x)

180 (normalise ctxt env y)

183 (normalise ctxt env y)

181 let err = cantUnify from r

184 let err = cantUnify from r

185+ (topx, xfrom) (topy, yfrom)

182− topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

186+ (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s

183 put (UI s ((x, y, True, env, err, from, Match) : f))

187 put (UI s ((x, y, True, env, err, from, Match) : f))

184 lift $ tfail err

188 lift $ tfail err

185 combine bnames as [] = return as

189 combine bnames as [] = return as

@@ -241,7 +245,7 @@ renameBindersTm env tm = uniqueBinders (map fst env) tm

241 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)

245 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)

242 explicitHole t = t

246 explicitHole t = t

243

247

244−trimSolutions topx topy from env topns = followSols [] (dropPairs topns)

248+trimSolutions (topx, xfrom) (topy, yfrom) from env topns = followSols [] (dropPairs topns)

245 where dropPairs [] = []

249 where dropPairs [] = []

246 dropPairs (n@(x, P _ x' _) : ns)

250 dropPairs (n@(x, P _ x' _) : ns)

247 | x == x' = dropPairs ns

251 | x == x' = dropPairs ns

@@ -258,7 +262,7 @@ trimSolutions topx topy from env topns = followSols [] (dropPairs topns)

258 = do vs' <- case t' of

262 = do vs' <- case t' of

259 P _ tn _ ->

263 P _ tn _ ->

260 if (n, tn) `elem` vs then -- cycle

264 if (n, tn) `elem` vs then -- cycle

261− tfail (cantUnify from False topx topy

265+ tfail (cantUnify from False (topx, xfrom) (topy, yfrom)

262 (Msg "") (errEnv env) 0)

266 (Msg "") (errEnv env) 0)

263 else return ((n, tn) : vs)

267 else return ((n, tn) : vs)

264 _ -> return vs

268 _ -> return vs

@@ -280,16 +284,18 @@ hasv (App f a) = hasv f || hasv a

280hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

284hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

281hasv _ = False

285hasv _ = False

282

286

283−unify :: Context -> Env -> TT Name -> TT Name ->

287+unify :: Context -> Env ->

288+ (TT Name, Maybe Provenance) ->

289+ (TT Name, Maybe Provenance) ->

284 [Name] -> [Name] -> [Name] -> [FailContext] ->

290 [Name] -> [Name] -> [Name] -> [FailContext] ->

285 TC ([(Name, TT Name)], Fails)

291 TC ([(Name, TT Name)], Fails)

286−unify ctxt env topx topy inj holes usersupp from =

292+unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

287-- traceWhen (hasv topx || hasv topy)

293-- traceWhen (hasv topx || hasv topy)

288-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $

294-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $

289 -- don't bother if topx and topy are different at the head

295 -- don't bother if topx and topy are different at the head

290 case runStateT (un False [] (renameBindersTm env topx)

296 case runStateT (un False [] (renameBindersTm env topx)

291 (renameBindersTm env topy)) (UI 0 []) of

297 (renameBindersTm env topy)) (UI 0 []) of

292− OK (v, UI _ []) -> do v' <- trimSolutions topx topy from env v

298+ OK (v, UI _ []) -> do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v

293 return (map (renameBinders env) v', [])

299 return (map (renameBinders env) v', [])

294 res ->

300 res ->

295 let topxn = renameBindersTm env (normalise ctxt env topx)

301 let topxn = renameBindersTm env (normalise ctxt env topx)

@@ -298,7 +304,7 @@ unify ctxt env topx topy inj holes usersupp from =

298 case runStateT (un False [] topxn topyn)

304 case runStateT (un False [] topxn topyn)

299 (UI 0 []) of

305 (UI 0 []) of

300 OK (v, UI _ fails) ->

306 OK (v, UI _ fails) ->

301− do v' <- trimSolutions topx topy from env v

307+ do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v

302 return (map (renameBinders env) v', reverse fails)

308 return (map (renameBinders env) v', reverse fails)

303-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

309-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

304 Error e -> tfail e

310 Error e -> tfail e

@@ -470,7 +476,7 @@ unify ctxt env topx topy inj holes usersupp from =

470 let r = recoverable (normalise ctxt env x)

476 let r = recoverable (normalise ctxt env x)

471 (normalise ctxt env y)

477 (normalise ctxt env y)

472 let err = cantUnify from r

478 let err = cantUnify from r

473− topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

479+ (topx, xfrom) (topy, yfrom) (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s

474 if (not r) then lift $ tfail err

480 if (not r) then lift $ tfail err

475 else do put (UI s ((x, y, True, env, err, from, Unify) : f))

481 else do put (UI s ((x, y, True, env, err, from, Unify) : f))

476 return [] -- lift $ tfail err

482 return [] -- lift $ tfail err

@@ -569,7 +575,8 @@ unify ctxt env topx topy inj holes usersupp from =

569 = do UI s f <- get

575 = do UI s f <- get

570 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

576 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

571 let err = cantUnify from r

577 let err = cantUnify from r

578+ (topx, xfrom) (topy, yfrom)

572− topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

579+ (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s

573 put (UI s ((topx, topy, True, env, err, from, Unify) : f))

580 put (UI s ((topx, topy, True, env, err, from, Unify) : f))

574 return []

581 return []

575

582

@@ -577,7 +584,8 @@ unify ctxt env topx topy inj holes usersupp from =

577 unifyFail x y = do UI s f <- get

584 unifyFail x y = do UI s f <- get

578 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

585 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

579 let err = cantUnify from r

586 let err = cantUnify from r

587+ (topx, xfrom) (topy, yfrom)

580− topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

588+ (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s

581 put (UI s ((topx, topy, True, env, err, from, Unify) : f))

589 put (UI s ((topx, topy, True, env, err, from, Unify) : f))

582 lift $ tfail err

590 lift $ tfail err

583

591

@@ -599,8 +607,8 @@ unify ctxt env topx topy inj holes usersupp from =

599 uB bnames x y = do UI s f <- get

607 uB bnames x y = do UI s f <- get

600 let r = recoverable (normalise ctxt env (binderTy x))

608 let r = recoverable (normalise ctxt env (binderTy x))

601 (normalise ctxt env (binderTy y))

609 (normalise ctxt env (binderTy y))

602− let err = cantUnify from r topx topy

610+ let err = cantUnify from r (topx, xfrom) (topy, yfrom)

603− (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

611+ (CantUnify r (binderTy x, Nothing) (binderTy y, Nothing) (Msg "") (errEnv env) s)

604 (errEnv env) s

612 (errEnv env) s

605 put (UI s ((binderTy x, binderTy y,

613 put (UI s ((binderTy x, binderTy y,

606 False,

614 False,

src/Idris/DeepSeq.hs+7−7

@@ -153,17 +153,20 @@ instance (NFData t) => NFData (PDecl' t) where

153 = rnf x1 `seq`

154 rnf x2 `seq`

155 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

156− rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8)

156+ rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

157 = rnf x1 `seq`

158 rnf x2 `seq`

159 rnf x3 `seq`

160+ rnf x4 `seq`

161+ rnf x5 `seq`

162+ rnf x6 `seq`

160− rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

163+ rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()

161 rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

164 rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

162 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

165 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

163 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

166 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

164 rnf (PDirective x1) = ()

167 rnf (PDirective x1) = ()

165− rnf (PProvider x1 x2 x3 x4)

168+ rnf (PProvider x1 x2 x3 x4 x5)

166− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

169+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

167 rnf (PTransform x1 x2 x3 x4)

170 rnf (PTransform x1 x2 x3 x4)

168 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

171 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

169

172

@@ -357,6 +360,3 @@ instance NFData SyntaxInfo where

357 rnf x4 `seq`

360 rnf x4 `seq`

358 rnf x5 `seq`

361 rnf x5 `seq`

359 rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

362 rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

360−

361−

362−

src/Idris/Delaborate.hs+17−4

@@ -194,6 +194,11 @@ pprintTerm ist = pprintTerm' ist []

194pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

195pprintTerm' ist bnd tm = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) tm

196

197+pprintProv :: IState -> [(Name, Term)] -> Provenance -> Doc OutputAnnotation

198+pprintProv i e ExpectedType = text "Expected type"

199+pprintProv i e (SourceTerm tm)

200+ = text "Type of " <> pprintTerm' i (zip (map fst e) (repeat False)) (delab i tm)

201+

197pprintErr :: IState -> Err -> Doc OutputAnnotation

202pprintErr :: IState -> Err -> Doc OutputAnnotation

198pprintErr i err = pprintErr' i (fmap (errReverse i) err)

203pprintErr i err = pprintErr' i (fmap (errReverse i) err)

199

204

@@ -203,20 +208,28 @@ pprintErr' i (InternalMsg s) =

203 text "This is probably a bug, or a missing error message.",

208 text "This is probably a bug, or a missing error message.",

204 text ("Please consider reporting at " ++ bugaddr)

209 text ("Please consider reporting at " ++ bugaddr)

205 ]

210 ]

206−pprintErr' i (CantUnify _ x_in y_in e sc s) =

211+pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =

207 let (x_ns, y_ns, nms) = renameMNs x_in y_in

212 let (x_ns, y_ns, nms) = renameMNs x_in y_in

208 (x, y) = addImplicitDiffs (delab i x_ns) (delab i y_ns) in

213 (x, y) = addImplicitDiffs (delab i x_ns) (delab i y_ns) in

209 text "Can't unify" <> indented (annTm x_ns

214 text "Can't unify" <> indented (annTm x_ns

210 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc

215 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc

211− ++ zip nms (repeat False)) x)) <$>

216+ ++ zip nms (repeat False)) x))

217+ <> case xprov of

218+ Nothing -> empty

219+ Just t -> text " (" <> pprintProv i sc t <> text ")"

220+ <$>

212 text "with" <> indented (annTm y_ns

221 text "with" <> indented (annTm y_ns

213 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc

222 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc

214− ++ zip nms (repeat False)) y)) <>

223+ ++ zip nms (repeat False)) y))

224+ <> case yprov of

225+ Nothing -> empty

226+ Just t -> text " (" <> pprintProv i sc t <> text ")"

227+ <>

215 case e of

228 case e of

216 Msg "" -> empty

229 Msg "" -> empty

217 -- if the specific error is the same as the one we just printed,

230 -- if the specific error is the same as the one we just printed,

218 -- there's no need to print it

231 -- there's no need to print it

219− CantUnify _ x_in' y_in' _ _ _ | x_in == x_in' && y_in == y_in' -> empty

232+ CantUnify _ (x_in', _) (y_in',_) _ _ _ | x_in == x_in' && y_in == y_in' -> empty

220 _ -> line <> line <> text "Specifically:" <>

233 _ -> line <> line <> text "Specifically:" <>

221 indented (pprintErr' i e) <>

234 indented (pprintErr' i e) <>

222 if (opt_errContext (idris_options i)) then showSc i sc else empty

235 if (opt_errContext (idris_options i)) then showSc i sc else empty

src/Idris/Docs.hs+50−12

@@ -32,7 +32,8 @@ data Docs' d = FunDoc (FunDoc' d)

32 | ClassDoc Name d -- class docs

33 [FunDoc' d] -- method docs

34 [(Name, Maybe d)] -- parameters and their docstrings

35− [PTerm] -- instances

35+ [(PTerm, (d, [(Name, d)]))] -- instances

36+ [PTerm] -- subclasses

36 [PTerm] -- superclasses

37 [PTerm] -- superclasses

37 | ModDoc [String] -- Module name

38 | ModDoc [String] -- Module name

38 d

39 d

@@ -88,7 +89,7 @@ pprintDocs ist (DataDoc t args)

88 if null args then text "No constructors."

89 if null args then text "No constructors."

89 else nest 4 (text "Constructors:" <> line <>

90 else nest 4 (text "Constructors:" <> line <>

90 vsep (map (pprintFD ist) args))

91 vsep (map (pprintFD ist) args))

91−pprintDocs ist (ClassDoc n doc meths params instances superclasses)

92+pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)

92 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>

93 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>

93 if nullDocstring doc

94 if nullDocstring doc

94 then empty

95 then empty

@@ -100,8 +101,8 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

100 vsep (map (pprintFD ist) meths))

101 vsep (map (pprintFD ist) meths))

101 <$>

102 <$>

102 nest 4 (text "Instances:" <$>

103 nest 4 (text "Instances:" <$>

103− vsep (if null instances' then [text "<no instances>"]

104+ vsep (if null instances then [text "<no instances>"]

104− else map dumpInstance instances'))

105+ else map pprintInstance instances))

105 <>

106 <>

106 (if null subclasses then empty

107 (if null subclasses then empty

107 else line <$> nest 4 (text "Subclasses:" <$>

108 else line <$> nest 4 (text "Subclasses:" <$>

@@ -118,6 +119,30 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

118 ppo = ppOptionIst ist

119 ppo = ppOptionIst ist

119 infixes = idris_infixes ist

120 infixes = idris_infixes ist

120

121

122+ pprintInstance (term, (doc, argDocs)) =

123+ nest 4 (dumpInstance term <>

124+ (if nullDocstring doc

125+ then empty

126+ else line <>

127+ renderDocstring

128+ (renderDocTerm

129+ (pprintDelab ist)

130+ (normaliseAll (tt_ctxt ist) []))

131+ doc) <>

132+ if null argDocs

133+ then empty

134+ else line <> vsep (map (prettyInstanceParam (map fst argDocs)) argDocs))

135+

136+ prettyInstanceParam params (name, doc) =

137+ if nullDocstring doc

138+ then empty

139+ else prettyName True False (zip params (repeat False)) name <+>

140+ showDoc ist doc

141+

142+-- if any (isJust . snd) params

143+-- then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)

144+-- else hsep (punctuate comma (map (prettyName True False params' . fst) params))

145+

121 dumpInstance :: PTerm -> Doc OutputAnnotation

146 dumpInstance :: PTerm -> Doc OutputAnnotation

122 dumpInstance = pprintPTerm ppo params' [] infixes

147 dumpInstance = pprintPTerm ppo params' [] infixes

123

148

@@ -140,11 +165,10 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

140 isSubclass (PPi _ _ _ pt) = isSubclass pt

165 isSubclass (PPi _ _ _ pt) = isSubclass pt

141 isSubclass _ = False

166 isSubclass _ = False

142

167

143− (subclasses, instances') = partition isSubclass instances

168+ prettyParameters =

144−

145− prettyParameters = if any (isJust . snd) params

169+ if any (isJust . snd) params

146− then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)

170+ then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)

147− else hsep (punctuate comma (map (prettyName True False params' . fst) params))

171+ else hsep (punctuate comma (map (prettyName True False params' . fst) params))

148

172

149pprintDocs ist (ModDoc mod docs)

173pprintDocs ist (ModDoc mod docs)

150 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>

174 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>

@@ -186,14 +210,28 @@ docClass n ci

186 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

210 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

187 docstr = maybe emptyDocstring fst docStrings

211 docstr = maybe emptyDocstring fst docStrings

188 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd))) (class_params ci)

212 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd))) (class_params ci)

213+ instanceDocs = map (fromMaybe (emptyDocstring, []) .

214+ listToMaybe .

215+ flip lookupCtxt (idris_docstrings i))

216+ (class_instances ci)

189− instances = map (delabTy i) (class_instances ci)

217+ instances = zip (map (delabTy i) (class_instances ci)) instanceDocs

218+ (subclasses, instances') = partition (isSubclass . fst) instances

190 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

219 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

191 mdocs <- mapM (docFun . fst) (class_methods ci)

220 mdocs <- mapM (docFun . fst) (class_methods ci)

221+ return $ ClassDoc

192− return $ ClassDoc n docstr mdocs params instances superclasses

222+ n docstr mdocs params

223+ instances' (map fst subclasses) superclasses

193 where

224 where

194− getDInst (PInstance _ _ _ _ _ t _ _) = Just t

225+ getDInst (PInstance _ _ _ _ _ _ _ t _ _) = Just t

195 getDInst _ = Nothing

226 getDInst _ = Nothing

196

227

228+ isSubclass (PPi (Constraint _ _) _ (PApp _ _ args) (PApp _ (PRef _ nm) args'))

229+ = nm == n && map getTm args == map getTm args'

230+ isSubclass (PPi _ _ _ pt)

231+ = isSubclass pt

232+ isSubclass _

233+ = False

234+

197docFun :: Name -> Idris FunDoc

235docFun :: Name -> Idris FunDoc

198docFun n

236docFun n

199 = do i <- getIState

237 = do i <- getIState

src/Idris/Elab/Class.hs+7−9

@@ -109,8 +109,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

109 mdec x = x

110

111 -- TODO: probably should normalise

112− checkDefaultSuperclassInstance :: PDecl -> Idris ()

112+ checkDefaultSuperclassInstance :: PDecl -> Idris ()

113− checkDefaultSuperclassInstance (PInstance _ fc cs n ps _ _ _)

113+ checkDefaultSuperclassInstance (PInstance _ _ _ fc cs n ps _ _ _)

114 = do when (not $ null cs) . tclift

115 $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))

116 i <- getIState

@@ -120,11 +120,11 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

120 $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))

121 return ()

122

123− impbind :: [(Name, PTerm)] -> PTerm -> PTerm

123+ impbind :: [(Name, PTerm)] -> PTerm -> PTerm

124 impbind [] x = x

125 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)

126

127− conbind :: [(Name, PTerm)] -> PTerm -> PTerm

127+ conbind :: [(Name, PTerm)] -> PTerm -> PTerm

128 conbind ((c, ty) : ns) x = PPi constraint c ty (conbind ns x)

129 conbind [] x = x

130

@@ -133,7 +133,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

133 = do t' <- implicit' info syn allmeths n t

134 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

135 return ( (n, (toExp (map fst ps) Exp t')),

136− (n, (doc, o, (toExp (map fst ps)

136+ (n, (doc, o, (toExp (map fst ps)

137 (\ l s p -> Imp l s p Nothing) t'))),

138 (n, (syn, o, t) ) )

139 tdecl _ _ = ifail "Not allowed in a class declaration"

@@ -155,7 +155,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

155

156 tydecl (PTy _ _ _ _ _ _ _) = True

157 tydecl _ = False

158− instdecl (PInstance _ _ _ _ _ _ _ _) = True

158+ instdecl (PInstance _ _ _ _ _ _ _ _ _ _) = True

159 instdecl _ = False

160 clause (PClauses _ _ _ _) = True

161 clause _ = False

@@ -221,7 +221,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

221

222 insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)

223 = PPi p n ty (insertConstraint c sc)

224− insertConstraint c sc = PPi (constraint { pstatic = Static })

224+ insertConstraint c sc = PPi (constraint { pstatic = Static })

225 (sMN 0 "class") c sc

226

227 -- make arguments explicit and don't bind class parameters

@@ -230,5 +230,3 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

230 | otherwise = PPi (e l s p) n ty (toExp ns e sc)

231 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

232 toExp ns e sc = sc

233−

234−

src/Idris/Elab/Clause.hs+3−3

@@ -464,7 +464,7 @@ checkPossible info fc tcgen fname lhs_in

464 Error err -> if tcgen then return (recoverable ctxt err)

465 else return (validCase ctxt err ||

466 recoverable ctxt err)

467− where validCase ctxt (CantUnify _ topx topy e _ _)

467+ where validCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)

468 = let topx' = normalise ctxt [] topx

469 topy' = normalise ctxt [] topy in

470 not (sameFam topx' topy' || not (validCase ctxt e))

@@ -474,7 +474,7 @@ checkPossible info fc tcgen fname lhs_in

474 validCase ctxt (ElaboratingArg _ _ _ e) = validCase ctxt e

475 validCase ctxt _ = True

476

477− recoverable ctxt (CantUnify r topx topy e _ _)

477+ recoverable ctxt (CantUnify r (topx, _) (topy, _) e _ _)

478 = let topx' = normalise ctxt [] topx

479 topy' = normalise ctxt [] topy in

480 checkRec topx' topy'

@@ -704,7 +704,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

704 OK (_, cs) -> do addConstraints fc cs

705 logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs

706 return ()

707− Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))

707+ Error e -> ierror (At fc (CantUnify False (clhsty, Nothing) (crhsty, Nothing) e [] 0))

708 i <- getIState

709 checkInferred fc (delab' i crhs True True) rhs

710 -- if the function is declared '%error_reverse', or its type,

src/Idris/Elab/Instance.hs+7−5

@@ -51,6 +51,8 @@ import Data.List.Split (splitOn)

51import Util.Pretty(pretty, text)

52

53elabInstance :: ElabInfo -> SyntaxInfo ->

54+ Docstring (Either Err PTerm) ->

55+ [(Name, Docstring (Either Err PTerm))] ->

54 ElabWhat -> -- phase

56 ElabWhat -> -- phase

55 FC -> [(Name, PTerm)] -> -- constraints

57 FC -> [(Name, PTerm)] -> -- constraints

56 Name -> -- the class

58 Name -> -- the class

@@ -58,7 +60,7 @@ elabInstance :: ElabInfo -> SyntaxInfo ->

58 PTerm -> -- full instance type

60 PTerm -> -- full instance type

59 Maybe Name -> -- explicit name

61 Maybe Name -> -- explicit name

60 [PDecl] -> Idris ()

62 [PDecl] -> Idris ()

61−elabInstance info syn what fc cs n ps t expn ds = do

63+elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

62 i <- getIState

64 i <- getIState

63 (n, ci) <- case lookupCtxtName n (idris_classes i) of

65 (n, ci) <- case lookupCtxtName n (idris_classes i) of

64 [c] -> return c

66 [c] -> return c

@@ -69,7 +71,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

69 let iname = mkiname n (namespace info) ps expn

71 let iname = mkiname n (namespace info) ps expn

70 let emptyclass = null (class_methods ci)

72 let emptyclass = null (class_methods ci)

71 when (what /= EDefns || (null ds && not emptyclass)) $ do

73 when (what /= EDefns || (null ds && not emptyclass)) $ do

72− nty <- elabType' True info syn emptyDocstring [] fc [] iname t

74+ nty <- elabType' True info syn doc argDocs fc [] iname t

73 -- if the instance type matches any of the instances we have already,

75 -- if the instance type matches any of the instances we have already,

74 -- and it's not a named instance, then it's overlapping, so report an error

76 -- and it's not a named instance, then it's overlapping, so report an error

75 case expn of

77 case expn of

@@ -147,10 +149,10 @@ elabInstance info syn what fc cs n ps t expn ds = do

147 Just m -> sNS (SN (sInstanceN n' (map show ps'))) m

149 Just m -> sNS (SN (sInstanceN n' (map show ps'))) m

148 Just nm -> nm

150 Just nm -> nm

149

151

150− substInstance ips pnames (PInstance syn _ cs n ps t expn ds)

152+ substInstance ips pnames (PInstance doc argDocs syn _ cs n ps t expn ds)

151− = PInstance syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

153+ = PInstance doc argDocs syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

152

154

153− isOverlapping i (PInstance syn _ _ n ps t expn _)

155+ isOverlapping i (PInstance doc argDocs syn _ _ n ps t expn _)

154 = case lookupCtxtName n (idris_classes i) of

156 = case lookupCtxtName n (idris_classes i) of

155 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in

157 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in

156 case lookupTy iname (tt_ctxt i) of

158 case lookupTy iname (tt_ctxt i) of

src/Idris/Elab/Provider.hs+4−5

@@ -52,8 +52,8 @@ import Data.List.Split (splitOn)

52import Util.Pretty(pretty, text)

53

54-- | Elaborate a type provider

55−elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()

55+elabProvider :: Docstring (Either Err PTerm) -> ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()

56−elabProvider info syn fc what n

56+elabProvider doc info syn fc what n

57 = do i <- getIState

58 -- Ensure that the experimental extension is enabled

59 unless (TypeProviders `elem` idris_language_extensions i) $

@@ -93,12 +93,12 @@ elabProvider info syn fc what n

93 Provide tm

94 | ProvTerm ty _ <- what ->

95 do -- Finally add a top-level definition of the provided term

96− elabType info syn emptyDocstring [] fc [] n ty

96+ elabType info syn doc [] fc [] n ty

97 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

98 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

99 | ProvPostulate _ <- what ->

100 do -- Add the postulate

101− elabPostulate info syn (fmap (const (Left $ Msg "")) . parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)

101+ elabPostulate info syn doc fc [] n (delab i tm)

102 logLvl 3 $ "Elaborated provided postulate " ++ show n

103 | otherwise ->

104 ierror . Msg $ "Attempted to provide a postulate where a term was expected."

@@ -120,4 +120,3 @@ elabProvider info syn fc what n

120 case converts ctxt [] (providerOf tp) prov of

121 OK _ -> True

122 _ -> False

123−

src/Idris/Elab/Transform.hs+2−2

@@ -81,12 +81,12 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

81 -- Types must always convert

82 case converts ctxt [] clhs_ty crhs_ty of

83 OK _ -> return ()

84− Error e -> ierror (At fc (CantUnify False clhs_tm crhs_tm e [] 0))

84+ Error e -> ierror (At fc (CantUnify False (clhs_tm, Nothing) (crhs_tm, Nothing) e [] 0))

85 -- In safe mode, values must convert (Thinks: This is probably not

86 -- useful as is, perhaps it should require a proof of equality instead)

87 when safe $ case converts ctxt [] clhs_tm crhs_tm of

88 OK _ -> return ()

89− Error e -> ierror (At fc (CantUnify False clhs_tm crhs_tm e [] 0))

89+ Error e -> ierror (At fc (CantUnify False (clhs_tm, Nothing) (crhs_tm, Nothing) e [] 0))

90

91 case unApply (depat clhs_tm) of

92 (P _ tfname _, _) -> do addTrans tfname (clhs_tm, crhs_tm)

src/Idris/Elab/Type.hs+9−1

@@ -90,7 +90,7 @@ buildType info syn fc opts n ty' = do

90 let (inaccData, impls) = unzip $ getUnboundImplicits i cty ty

91 let inacc = inaccessibleImps 0 cty inaccData

92 logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc ++

93− " from " ++ show (cty, ty)

93+ " from " ++ show cty ++ "\n" ++ showTmImpls ty

94

95 putIState $ i { idris_implicits = addDef n impls (idris_implicits i) }

96 logLvl 3 ("Implicit " ++ show n ++ " " ++ show impls)

@@ -181,6 +181,12 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

181 addIBC (IBCErrorHandler n)

182 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"

183 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."

184+ -- if it's an export list type, make a note of it

185+ case (unApply usety) of

186+ (P _ ut _, _)

187+ | ut == ffiexport -> do addIBC (IBCExport n)

188+ addExport n

189+ _ -> return ()

184 return usety

190 return usety

185 where

191 where

186 -- for making an internalapp, we only want the explicit ones, and don't

192 -- for making an internalapp, we only want the explicit ones, and don't

@@ -191,6 +197,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

191 | otherwise = mergeTy sc sc'

197 | otherwise = mergeTy sc sc'

192 mergeTy _ sc = sc

198 mergeTy _ sc = sc

193

199

200+ ffiexport = sNS (sUN "FFI_Export") ["FFI_Export"]

201+

194 err = txt "Err"

202 err = txt "Err"

195 maybe = txt "Maybe"

203 maybe = txt "Maybe"

196 lst = txt "List"

204 lst = txt "List"

src/Idris/ElabDecls.hs+6−7

@@ -200,11 +200,11 @@ elabDecl' what info (PMutual f ps)

200 where isDataDecl (PData _ _ _ _ _ _) = True

201 isDataDecl _ = False

202

203− setMutData ns n

203+ setMutData ns n

204 = do i <- getIState

205 case lookupCtxt n (idris_datatypes i) of

206 [x] -> do let x' = x { mutual_types = ns }

207− putIState $ i { idris_datatypes

207+ putIState $ i { idris_datatypes

208 = addDef n x' (idris_datatypes i) }

209 _ -> return ()

210

@@ -233,9 +233,9 @@ elabDecl' what info (PClass doc s f cs n ps pdocs ds)

233 | what /= EDefns

234 = do iLOG $ "Elaborating class " ++ show n

235 elabClass info (s { syn_params = [] }) doc f cs n ps pdocs ds

236−elabDecl' what info (PInstance s f cs n ps t expn ds)

236+elabDecl' what info (PInstance doc argDocs s f cs n ps t expn ds)

237 = do iLOG $ "Elaborating instance " ++ show n

238− elabInstance info s what f cs n ps t expn ds

238+ elabInstance info s doc argDocs what f cs n ps t expn ds

239elabDecl' what info (PRecord doc s f tyn ty opts cdoc cn cty)

240 | what /= ETypes

241 = do iLOG $ "Elaborating record " ++ show tyn

@@ -249,12 +249,11 @@ elabDecl' _ info (PDSL n dsl)

249 addIBC (IBCDSL n)

250elabDecl' what info (PDirective i)

251 | what /= EDefns = i

252−elabDecl' what info (PProvider syn fc provWhat n)

252+elabDecl' what info (PProvider doc syn fc provWhat n)

253 | what /= EDefns

254 = do iLOG $ "Elaborating type provider " ++ show n

255− elabProvider info syn fc provWhat n

255+ elabProvider doc info syn fc provWhat n

256elabDecl' what info (PTransform fc safety old new)

257 = do elabTransform info fc safety old new

258 return ()

259elabDecl' _ _ _ = return () -- skipped this time

260−

src/Idris/ElabTerm.hs+3−3

@@ -268,10 +268,10 @@ elab ist info emode opts fn tm

268 pimp (sUN "a") Placeholder True,

269 pexp ct])) True

270

271− forceErr env (CantUnify _ t t' _ _ _)

271+ forceErr env (CantUnify _ (t,_) (t',_) _ _ _)

272 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

273 ht == txt "Lazy'" = True

274− forceErr env (CantUnify _ t t' _ _ _)

274+ forceErr env (CantUnify _ (t,_) (t',_) _ _ _)

275 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),

276 ht == txt "Lazy'" = True

277 forceErr env (InfiniteUnify _ t _)

@@ -2553,7 +2553,7 @@ reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT")

2553reflectErr :: Err -> Raw

2554reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]

2555reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]

2556−reflectErr (CantUnify b t1 t2 e ctxt i) =

2556+reflectErr (CantUnify b (t1,_) (t2,_) e ctxt i) =

2557 raw_apply (Var $ reflErrName "CantUnify")

2558 [ rawBool b

2559 , reflect t1

src/Idris/Erasure.hs+19−15

@@ -65,12 +65,12 @@ type Vars = Map Name VarInfo

65

66-- Perform usage analysis, write the relevant information in the internal

67-- structures, returning the list of reachable names.

68−performUsageAnalysis :: Idris [Name]

68+performUsageAnalysis :: [Name] -> Idris [Name]

69−performUsageAnalysis = do

69+performUsageAnalysis roots = do

70 ctx <- tt_ctxt <$> getIState

71− mainName <- getMainName <$> getIState

71+ startNames <- getStartNames <$> getIState

72

73− case mainName of

73+ case startNames of

74 Left reason -> return [] -- no main -> not compiling -> reachability irrelevant

75 Right main -> do

76 ci <- idris_classes <$> getIState

@@ -106,11 +106,14 @@ performUsageAnalysis = do

106

107 return $ S.toList reachableNames

108 where

109− getMainName :: IState -> Either Err Name

109+ getStartNames :: IState -> Either Err [Name]

110+ getStartNames ist

110− getMainName ist = case lookupCtxtName n (idris_implicits ist) of

111+ = case lookupCtxtName n (idris_implicits ist) of

111− [(n', _)] -> Right n'

112+ [(n', _)] -> Right (n' : roots)

113+ [] -> if null roots

112− [] -> Left (NoSuchVariable n)

114+ then Left (NoSuchVariable n)

115+ else Right roots

113− more -> Left (CantResolveAlts (map fst more))

116+ more -> Left (CantResolveAlts (map fst more))

114 where

117 where

115 n = sNS (sUN "main") ["Main"]

118 n = sNS (sUN "main") ["Main"]

116

119

@@ -171,9 +174,9 @@ forwardChain deps

171

174

172-- Build the dependency graph,

175-- Build the dependency graph,

173-- starting the depth-first search from a list of Names.

176-- starting the depth-first search from a list of Names.

174−buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> Context -> Name -> Deps

177+buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> Context -> [Name] -> Deps

175−buildDepMap ci used ctx mainName = addPostulates used $

178+buildDepMap ci used ctx startNames = addPostulates used $

176− dfs S.empty M.empty [mainName]

179+ dfs S.empty M.empty startNames

177 where

180 where

178 -- mark the result of Main.main as used with the empty assumption

181 -- mark the result of Main.main as used with the empty assumption

179 addPostulates :: [(Name, Int)] -> Deps -> Deps

182 addPostulates :: [(Name, Int)] -> Deps -> Deps

@@ -191,10 +194,11 @@ buildDepMap ci used ctx mainName = addPostulates used $

191

194

192 postulates used =

195 postulates used =

193 [ [] ==> concat

196 [ [] ==> concat

194− -- These two, Main.main and run__IO, are always evaluated

197+ -- Main.main ( + export lists) and run__IO, are always evaluated

195 -- but they elude analysis since they come from the seed term.

198 -- but they elude analysis since they come from the seed term.

196− [ [(mainName, Result)]

199+ [(map (\n -> (n, Result)) startNames)

197− , [(sUN "run__IO", Result), (sUN "run__IO", Arg 1)]

200+ ,[(sUN "run__IO", Result), (sUN "run__IO", Arg 1)]

201+ ,[(sUN "call__IO", Result), (sUN "call__IO", Arg 2)]

198

202

199 -- Explicit usage declarations from a %used pragma

203 -- Explicit usage declarations from a %used pragma

200 , map (\(n, i) -> (n, Arg i)) used

204 , map (\(n, i) -> (n, Arg i)) used

src/Idris/IBC.hs+53−37

@@ -80,7 +80,8 @@ data IBCFile = IBCFile { ver :: Word8,

80 ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))],

81 ibc_postulates :: ![Name],

82 ibc_parsedSpan :: !(Maybe FC),

83− ibc_usage :: ![(Name, Int)]

83+ ibc_usage :: ![(Name, Int)],

84+ ibc_exports :: ![Name]

84 }

85 }

85 deriving Show

86 deriving Show

86{-!

87{-!

@@ -88,11 +89,11 @@ deriving instance Binary IBCFile

88!-}

89!-}

89

90

90initIBC :: IBCFile

91initIBC :: IBCFile

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

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

92

93

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

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

94 -> FilePath -> Idris ()

95 -> FilePath -> Idris ()

95−loadIBC reexport fp

96+loadIBC reexport fp

96 = do imps <- getImported

97 = do imps <- getImported

97 let redo = case lookup fp imps of

98 let redo = case lookup fp imps of

98 Nothing -> True

99 Nothing -> True

@@ -193,7 +194,7 @@ ibc i (IBCLib tgt n) f = return f { ibc_libs = (tgt, n) : ibc_libs f }

193ibc i (IBCCGFlag tgt n) f = return f { ibc_cgflags = (tgt, n) : ibc_cgflags f }

194ibc i (IBCCGFlag tgt n) f = return f { ibc_cgflags = (tgt, n) : ibc_cgflags f }

194ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }

195ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }

195ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }

196ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }

196−ibc i (IBCDef n) f

197+ibc i (IBCDef n) f

197 = do f' <- case lookupDefExact n (tt_ctxt i) of

198 = do f' <- case lookupDefExact n (tt_ctxt i) of

198 Just v -> return f { ibc_defs = (n,v) : ibc_defs f }

199 Just v -> return f { ibc_defs = (n,v) : ibc_defs f }

199 _ -> ifail "IBC write failed"

200 _ -> ifail "IBC write failed"

@@ -233,17 +234,18 @@ ibc i (IBCModDocs n) f = case lookupCtxtExact n (idris_moduledocs i) of

233 Just v -> return f { ibc_moduledocs = (n,v) : ibc_moduledocs f }

234 Just v -> return f { ibc_moduledocs = (n,v) : ibc_moduledocs f }

234 _ -> ifail "IBC write failed"

235 _ -> ifail "IBC write failed"

235ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f }

236ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f }

237+ibc i (IBCExport n) f = return f { ibc_exports = n : ibc_exports f }

236

238

237process :: Bool -- ^ Reexporting

239process :: Bool -- ^ Reexporting

238 -> IBCFile -> FilePath -> Idris ()

240 -> IBCFile -> FilePath -> Idris ()

239process reexp i fn

241process reexp i fn

240− | ver i /= ibcVersion

242+ | ver i /= ibcVersion

241 = do iLOG "ibc out of date"

243 = do iLOG "ibc out of date"

242 let e = if ver i < ibcVersion then " an earlier " else " a later "

244 let e = if ver i < ibcVersion then " an earlier " else " a later "

243 ifail $ "Incompatible ibc version.\nThis library was built with"

245 ifail $ "Incompatible ibc version.\nThis library was built with"

244 ++ e ++ "version of Idris.\n" ++

246 ++ e ++ "version of Idris.\n" ++

245 "Please clean and rebuild."

247 "Please clean and rebuild."

246−

248+

247 --- please rebuild"

249 --- please rebuild"

248 | otherwise =

250 | otherwise =

249 do srcok <- runIO $ doesFileExist (sourcefile i)

251 do srcok <- runIO $ doesFileExist (sourcefile i)

@@ -290,6 +292,7 @@ process reexp i fn

290 pPostulates $ force (ibc_postulates i)

292 pPostulates $ force (ibc_postulates i)

291 pParsedSpan $ force (ibc_parsedSpan i)

293 pParsedSpan $ force (ibc_parsedSpan i)

292 pUsage $ force (ibc_usage i)

294 pUsage $ force (ibc_usage i)

295+ pExports $ force (ibc_exports i)

293

296

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

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

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

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

@@ -311,12 +314,16 @@ pUsage :: [(Name, Int)] -> Idris ()

311pUsage ns = do ist <- getIState

314pUsage ns = do ist <- getIState

312 putIState ist { idris_erasureUsed = ns ++ idris_erasureUsed ist }

315 putIState ist { idris_erasureUsed = ns ++ idris_erasureUsed ist }

313

316

317+pExports :: [Name] -> Idris ()

318+pExports ns = do ist <- getIState

319+ putIState ist { idris_exports = ns ++ idris_exports ist }

320+

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

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

315pImportDirs fs = mapM_ addImportDir fs

322pImportDirs fs = mapM_ addImportDir fs

316

323

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

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

318pImports fs

325pImports fs

319− = do mapM_ (\(re, f) ->

326+ = do mapM_ (\(re, f) ->

320 do i <- getIState

327 do i <- getIState

321 ibcsd <- valIBCSubDir i

328 ibcsd <- valIBCSubDir i

322 ids <- allImportDirs

329 ids <- allImportDirs

@@ -420,20 +427,20 @@ pHdrs :: [(Codegen, String)] -> Idris ()

420pHdrs hs = mapM_ (uncurry addHdr) hs

427pHdrs hs = mapM_ (uncurry addHdr) hs

421

428

422pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()

429pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()

423−pPatdefs ds

430+pPatdefs ds

424− = mapM_ (\ (n, d) ->

431+ = mapM_ (\ (n, d) ->

425 do i <- getIState

432 do i <- getIState

426 putIState (i { idris_patdefs = addDef n (force d) (idris_patdefs i) }))

433 putIState (i { idris_patdefs = addDef n (force d) (idris_patdefs i) }))

427 ds

434 ds

428

435

429pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()

436pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()

430−pDefs reexp syms ds

437+pDefs reexp syms ds

431 = mapM_ (\ (n, d) ->

438 = mapM_ (\ (n, d) ->

432 do d' <- updateDef d

439 do d' <- updateDef d

433 case d' of

440 case d' of

434− TyDecl _ _ -> return ()

441+ TyDecl _ _ -> return ()

435 _ -> do iLOG $ "SOLVING " ++ show n

442 _ -> do iLOG $ "SOLVING " ++ show n

436− solveDeferred n

443+ solveDeferred n

437 i <- getIState

444 i <- getIState

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

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

439 putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })

446 putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })

@@ -502,8 +509,8 @@ pMDocs ds = mapM_ addMDocStr ds

502

509

503pAccess :: Bool -- ^ Reexporting?

510pAccess :: Bool -- ^ Reexporting?

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

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

505−pAccess reexp ds

512+pAccess reexp ds

506− = mapM_ (\ (n, a_in) ->

513+ = mapM_ (\ (n, a_in) ->

507 do let a = if reexp then a_in else Hidden

514 do let a = if reexp then a_in else Hidden

508 logLvl 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a

515 logLvl 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a

509 i <- getIState

516 i <- getIState

@@ -561,7 +568,7 @@ pFunctionErrorHandlers ((fn, arg, handler):ns) = do addFunctionErrorHandlers fn

561

568

562pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()

569pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()

563pMetavars ns = do i <- getIState

570pMetavars ns = do i <- getIState

564− putIState $ i { idris_metavars = Data.List.reverse ns

571+ putIState $ i { idris_metavars = Data.List.reverse ns

565 ++ idris_metavars i }

572 ++ idris_metavars i }

566

573

567----- For Cheapskate and docstrings

574----- For Cheapskate and docstrings

@@ -855,7 +862,7 @@ safeToEnum :: (Enum a, Bounded a, Integral int) => String -> int -> a

855safeToEnum label x' = result

862safeToEnum label x' = result

856 where

863 where

857 x = fromIntegral x'

864 x = fromIntegral x'

858− result

865+ result

859 | x < fromEnum (minBound `asTypeOf` result)

866 | x < fromEnum (minBound `asTypeOf` result)

860 || x > fromEnum (maxBound `asTypeOf` result)

867 || x > fromEnum (maxBound `asTypeOf` result)

861 = error $ label ++ ": corrupted binary representation in IBC"

868 = error $ label ++ ": corrupted binary representation in IBC"

@@ -927,7 +934,7 @@ instance Binary MetaInformation where

927 _ -> error "Corrupted binary data for MetaInformation"

934 _ -> error "Corrupted binary data for MetaInformation"

928

935

929instance Binary IBCFile where

936instance Binary IBCFile where

930− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42)

937+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43)

931 = {-# SCC "putIBCFile" #-}

938 = {-# SCC "putIBCFile" #-}

932 do put x1

939 do put x1

933 put x2

940 put x2

@@ -971,6 +978,7 @@ instance Binary IBCFile where

971 put x40

978 put x40

972 put x41

979 put x41

973 put x42

980 put x42

981+ put x43

974

982

975 get

983 get

976 = do x1 <- get

984 = do x1 <- get

@@ -1016,7 +1024,8 @@ instance Binary IBCFile where

1016 x40 <- get

1024 x40 <- get

1017 x41 <- get

1025 x41 <- get

1018 x42 <- get

1026 x42 <- get

1027+ x43 <- get

1019− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42)

1028+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43)

1020 else return (initIBC { ver = x1 })

1029 else return (initIBC { ver = x1 })

1021

1030

1022instance Binary DataOpt where

1031instance Binary DataOpt where

@@ -1239,15 +1248,18 @@ instance (Binary t) => Binary (PDecl' t) where

1239 put x6

1248 put x6

1240 put x7

1249 put x7

1241 put x8

1250 put x8

1242− PInstance x1 x2 x3 x4 x5 x6 x7 x8 -> do putWord8 8

1251+ PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

1252+ do putWord8 8

1243− put x1

1253+ put x1

1244− put x2

1254+ put x2

1245− put x3

1255+ put x3

1246− put x4

1256+ put x4

1247− put x5

1257+ put x5

1248− put x6

1258+ put x6

1249− put x7

1259+ put x7

1250− put x8

1260+ put x8

1261+ put x9

1262+ put x10

1251 PDSL x1 x2 -> do putWord8 9

1263 PDSL x1 x2 -> do putWord8 9

1252 put x1

1264 put x1

1253 put x2

1265 put x2

@@ -1270,16 +1282,18 @@ instance (Binary t) => Binary (PDecl' t) where

1270 put x1

1282 put x1

1271 put x2

1283 put x2

1272 PDirective x1 -> error "Cannot serialize PDirective"

1284 PDirective x1 -> error "Cannot serialize PDirective"

1273− PProvider x1 x2 x3 x4 -> do putWord8 15

1285+ PProvider x1 x2 x3 x4 x5 ->

1286+ do putWord8 15

1274− put x1

1287+ put x1

1275− put x2

1288+ put x2

1276− put x3

1289+ put x3

1277− put x4

1290+ put x4

1291+ put x5

1278 PTransform x1 x2 x3 x4 -> do putWord8 16

1292 PTransform x1 x2 x3 x4 -> do putWord8 16

1279 put x1

1293 put x1

1280 put x2

1294 put x2

1281 put x3

1295 put x3

1282− put x4

1296+ put x4

1283 get

1297 get

1284 = do i <- getWord8

1298 = do i <- getWord8

1285 case i of

1299 case i of

@@ -1341,7 +1355,9 @@ instance (Binary t) => Binary (PDecl' t) where

1341 x6 <- get

1355 x6 <- get

1342 x7 <- get

1356 x7 <- get

1343 x8 <- get

1357 x8 <- get

1358+ x9 <- get

1359+ x10 <- get

1344− return (PInstance x1 x2 x3 x4 x5 x6 x7 x8)

1360+ return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

1345 9 -> do x1 <- get

1361 9 -> do x1 <- get

1346 x2 <- get

1362 x2 <- get

1347 return (PDSL x1 x2)

1363 return (PDSL x1 x2)

@@ -1367,7 +1383,8 @@ instance (Binary t) => Binary (PDecl' t) where

1367 x2 <- get

1383 x2 <- get

1368 x3 <- get

1384 x3 <- get

1369 x4 <- get

1385 x4 <- get

1386+ x5 <- get

1370− return (PProvider x1 x2 x3 x4)

1387+ return (PProvider x1 x2 x3 x4 x5)

1371 16 -> do x1 <- get

1388 16 -> do x1 <- get

1372 x2 <- get

1389 x2 <- get

1373 x3 <- get

1390 x3 <- get

@@ -2189,4 +2206,3 @@ instance Binary Codegen where

2189 return (Via x1)

2206 return (Via x1)

2190 1 -> return Bytecode

2207 1 -> return Bytecode

2191 _ -> error "Corrupted binary data for Codegen"

2208 _ -> error "Corrupted binary data for Codegen"

2192−

src/Idris/IdrisDoc.hs+5−5

@@ -168,7 +168,7 @@ removeOrphans list =

168 in filter ((`S.notMember` children) . (\(n, _, _) -> n)) list

169

170 where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds

171− names (Just (ClassDoc _ _ fds _ _ _)) = map (\(FD n _ _ _ _) -> n) fds

171+ names (Just (ClassDoc _ _ fds _ _ _ _)) = map (\(FD n _ _ _ _) -> n) fds

172 names _ = []

173

174-- | Whether a Name names something which should be documented

@@ -219,7 +219,7 @@ referredNss (n, Just d, _) =

219

220 where getFunDocs (FunDoc f) = [f]

221 getFunDocs (DataDoc f fs) = f:fs

222− getFunDocs (ClassDoc _ _ fs _ _ _) = fs

222+ getFunDocs (ClassDoc _ _ fs _ _ _ _) = fs

223 types (FD _ _ args t _) = t:(map second args)

224 second (_, x, _, _) = x

225

@@ -417,7 +417,7 @@ createIndex nss out =

417 BS2.hPut h $ renderHtml $ wrapper Nothing $ do

418 H.h1 $ "Namespaces"

419 H.ul ! class_ "names" $ do

420− let path ns = "docs" </> genRelNsPath ns "html"

420+ let path ns = "docs" </> genRelNsPath ns "html"

421 item ns = do let n = toHtml $ nsName2Str ns

422 link = toValue $ path ns

423 H.li $ H.a ! href link ! class_ "code" $ n

@@ -439,7 +439,7 @@ createNsDoc :: IState -- ^ Needed to determine the types of names

439createNsDoc ist ns content out =

440 do let tpath = out </> "docs" </> (genRelNsPath ns "html")

441 dir = takeDirectory tpath

442− file = takeFileName tpath

442+ file = takeFileName tpath

443 haveDocs (_, Just d, _) = [d]

444 haveDocs _ = []

445 -- We cannot do anything without a Doc

@@ -575,7 +575,7 @@ createOtherDoc :: IState -- ^ Needed to determine the types of names

575 -> H.Html -- ^ Resulting HTML

576createOtherDoc ist (FunDoc fd) = createFunDoc ist fd

577

578−createOtherDoc ist (ClassDoc n docstring fds _ _ _) = do

578+createOtherDoc ist (ClassDoc n docstring fds _ _ _ _) = do

579 H.dt ! (A.id $ toValue $ show n) $ do

580 H.span ! class_ "word" $ do "class"; nbsp

581 H.span ! class_ "name type"

src/Idris/ParseHelpers.hs+2−2

@@ -587,7 +587,7 @@ collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

587collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

588collect (PClass doc f s cs n ps pdocs ds : ds')

589 = PClass doc f s cs n ps pdocs (collect ds) : collect ds'

590−collect (PInstance f s cs n ps t en ds : ds')

590+collect (PInstance doc argDocs f s cs n ps t en ds : ds')

591− = PInstance f s cs n ps t en (collect ds) : collect ds'

591+ = PInstance doc argDocs f s cs n ps t en (collect ds) : collect ds'

592collect (d : ds) = d : collect ds

593collect [] = []

src/Idris/Parser.hs+56−44

@@ -9,7 +9,7 @@ module Idris.Parser(module Idris.Parser,

9import Prelude hiding (pi)

10

11import Text.Trifecta.Delta

12−import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)

12+import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace, Err)

13import Text.Parser.LookAhead

14import Text.Parser.Expression

15import qualified Text.Parser.Token as Tok

@@ -87,7 +87,7 @@ import System.IO

87{- | Parses module definition

88

89@

90− ModuleHeader ::= 'module' Identifier_t ';'?;

90+ ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;

91@

92-}

93moduleHeader :: IdrisParser (Maybe (Docstring ()), [String])

@@ -291,7 +291,7 @@ syntaxRule syn

291

292 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :

293 mkSimple es

294− -- Can't parse a full expression followed by operator like characters due to ambiguity

294+ -- Can't parse a full expression followed by operator like characters due to ambiguity

295 mkSimple' (Expr e : Symbol s : es)

296 | takeWhile (`elem` opChars) ts /= "" && ts `notElem` invalidOperators = SimpleExpr e : Symbol s : mkSimple' es

297 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s

@@ -348,13 +348,9 @@ fnDecl' :: SyntaxInfo -> IdrisParser PDecl

348fnDecl' syn = checkFixity $

349 do (doc, argDocs, fc, opts', n, acc) <- try (do

350 pushIndent

351− (doc, argDocs) <- option noDocs docComment

351+ (doc, argDocs) <- docstring syn

352 ist <- get

353− let doc' = annotCode (tryFullExpr syn ist) doc

354− argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

355− | (n, d) <- argDocs ]

356−

357− initOpts = if default_total ist

353+ let initOpts = if default_total ist

358 then [TotalFn]

354 then [TotalFn]

359 else []

355 else []

360 opts <- fnOpts initOpts

356 opts <- fnOpts initOpts

@@ -364,7 +360,7 @@ fnDecl' syn = checkFixity $

364 let n = expandNS syn n_in

360 let n = expandNS syn n_in

365 fc <- getFC

361 fc <- getFC

366 lchar ':'

362 lchar ':'

367− return (doc', argDocs', fc, opts', n, acc))

363+ return (doc, argDocs, fc, opts', n, acc))

368 ty <- typeExpr (allowImp syn)

364 ty <- typeExpr (allowImp syn)

369 terminator

365 terminator

370 addAcc n acc

366 addAcc n acc

@@ -459,12 +455,10 @@ Postulate ::=

459@

455@

460-}

456-}

461postulate :: SyntaxInfo -> IdrisParser PDecl

457postulate :: SyntaxInfo -> IdrisParser PDecl

462−postulate syn = do doc <- try $ do (doc, _) <- option noDocs docComment

458+postulate syn = do doc <- try $ do (doc, _) <- docstring syn

463− ist <- get

464− let doc' = annotCode (tryFullExpr syn ist) doc

465 pushIndent

459 pushIndent

466 reserved "postulate"

460 reserved "postulate"

467− return doc'

461+ return doc

468 ist <- get

462 ist <- get

469 let initOpts = if default_total ist

463 let initOpts = if default_total ist

470 then [TotalFn]

464 then [TotalFn]

@@ -587,7 +581,7 @@ ClassBlock ::=

587classBlock :: SyntaxInfo -> IdrisParser [PDecl]

581classBlock :: SyntaxInfo -> IdrisParser [PDecl]

588classBlock syn = do reserved "where"

582classBlock syn = do reserved "where"

589 openBlock

583 openBlock

590− ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)

584+ ds <- many (notEndBlock >> instance_ syn <|> fnDecl syn)

591 closeBlock

585 closeBlock

592 return (concat ds)

586 return (concat ds)

593 <?> "class block"

587 <?> "class block"

@@ -608,15 +602,14 @@ Class ::=

608@

602@

609-}

603-}

610class_ :: SyntaxInfo -> IdrisParser [PDecl]

604class_ :: SyntaxInfo -> IdrisParser [PDecl]

611−class_ syn = do (doc, argDocs, acc) <- try (do

605+class_ syn = do (doc, argDocs, acc)

612− (doc, argDocs) <- option noDocs docComment

606+ <- try (do (doc, argDocs) <- docstring syn

613− ist <- get

614− let doc' = annotCode (tryFullExpr syn ist) doc

615− argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

616− | (n, d) <- argDocs ]

617− acc <- optional accessibility

607+ acc <- optional accessibility

618− return (doc', argDocs', acc))

608+ reserved "class"

609+ return (doc, argDocs, acc))

610+ fc <- getFC

619− reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName

611+ cons <- constraintList syn

612+ n_in <- fnName

620 let n = expandNS syn n_in

613 let n = expandNS syn n_in

621 cs <- many carg

614 cs <- many carg

622 ds <- option [] (classBlock syn)

615 ds <- option [] (classBlock syn)

@@ -634,7 +627,7 @@ class_ syn = do (doc, argDocs, acc) <- try (do

634

627

635@

628@

636 Instance ::=

629 Instance ::=

637− 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?

630+ DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?

638 ;

631 ;

639@

632@

640

633

@@ -643,7 +636,9 @@ InstanceName ::= '[' Name ']';

643@

636@

644-}

637-}

645instance_ :: SyntaxInfo -> IdrisParser [PDecl]

638instance_ :: SyntaxInfo -> IdrisParser [PDecl]

639+instance_ syn = do (doc, argDocs)

646−instance_ syn = do reserved "instance"; fc <- getFC

640+ <- try (docstring syn <* reserved "instance")

641+ fc <- getFC

647 en <- optional instanceName

642 en <- optional instanceName

648 cs <- constraintList syn

643 cs <- constraintList syn

649 cn <- fnName

644 cn <- fnName

@@ -651,7 +646,7 @@ instance_ syn = do reserved "instance"; fc <- getFC

651 let sc = PApp fc (PRef fc cn) (map pexp args)

646 let sc = PApp fc (PRef fc cn) (map pexp args)

652 let t = bindList (PPi constraint) cs sc

647 let t = bindList (PPi constraint) cs sc

653 ds <- option [] (instanceBlock syn)

648 ds <- option [] (instanceBlock syn)

654− return [PInstance syn fc cs cn args t en ds]

649+ return [PInstance doc argDocs syn fc cs cn args t en ds]

655 <?> "instance declaration"

650 <?> "instance declaration"

656 where instanceName :: IdrisParser Name

651 where instanceName :: IdrisParser Name

657 instanceName = do lchar '['; n_in <- fnName; lchar ']'

652 instanceName = do lchar '['; n_in <- fnName; lchar ']'

@@ -660,6 +655,18 @@ instance_ syn = do reserved "instance"; fc <- getFC

660 <?> "instance name"

655 <?> "instance name"

661

656

662

657

658+-- | Parse a docstring

659+docstring :: SyntaxInfo

660+ -> IdrisParser (Docstring (Either Err PTerm),

661+ [(Name,Docstring (Either Err PTerm))])

662+docstring syn = do (doc, argDocs) <- option noDocs docComment

663+ ist <- get

664+ let doc' = annotCode (tryFullExpr syn ist) doc

665+ argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

666+ | (n, d) <- argDocs ]

667+ return (doc', argDocs')

668+

669+

663{- | Parses a using declaration list

670{- | Parses a using declaration list

664

671

665@

672@

@@ -1101,25 +1108,30 @@ totality

1101{- | Parses a type provider

1108{- | Parses a type provider

1102

1109

1103@

1110@

1104−Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;

1111+Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;

1105ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'

1112ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'

1106@

1113@

1107 -}

1114 -}

1108provider :: SyntaxInfo -> IdrisParser [PDecl]

1115provider :: SyntaxInfo -> IdrisParser [PDecl]

1116+provider syn = do doc <- try (do (doc, _) <- docstring syn

1117+ lchar '%'

1109−provider syn = do try (lchar '%' *> reserved "provide");

1118+ reserved "provide"

1119+ return doc)

1110− provideTerm <|> providePostulate

1120+ provideTerm doc <|> providePostulate doc

1111 <?> "type provider"

1121 <?> "type provider"

1122+ where provideTerm doc =

1112− where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1123+ do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1113− fc <- getFC

1124+ fc <- getFC

1114− reserved "with"

1125+ reserved "with"

1115− e <- expr syn <?> "provider expression"

1126+ e <- expr syn <?> "provider expression"

1116− return [PProvider syn fc (ProvTerm t e) n]

1127+ return [PProvider doc syn fc (ProvTerm t e) n]

1128+ providePostulate doc =

1117− providePostulate = do reserved "postulate"

1129+ do reserved "postulate"

1118− n <- fnName

1130+ n <- fnName

1119− fc <- getFC

1131+ fc <- getFC

1120− reserved "with"

1132+ reserved "with"

1121− e <- expr syn <?> "provider expression"

1133+ e <- expr syn <?> "provider expression"

1122− return [PProvider syn fc (ProvPostulate e) n]

1134+ return [PProvider doc syn fc (ProvPostulate e) n]

1123

1135

1124{- | Parses a transform

1136{- | Parses a transform

1125

1137

@@ -1403,9 +1415,9 @@ loadSource lidr f toline

1403 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)

1415 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)

1404 toMutual x = let r = PMutual (fileFC "single mutual") [x] in

1416 toMutual x = let r = PMutual (fileFC "single mutual") [x] in

1405 case x of

1417 case x of

1406− PClauses _ _ _ _ -> r

1418+ PClauses{} -> r

1407− PClass _ _ _ _ _ _ _ _ -> r

1419+ PClass{} -> r

1408− PInstance _ _ _ _ _ _ _ _ -> r

1420+ PInstance{} -> r

1409 _ -> x

1421 _ -> x

1410

1422

1411 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()

1423 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()

src/Idris/Prover.hs+1−1

@@ -83,7 +83,7 @@ prove opt ctxt lit n ty

83 "Expected type:" ++ show ty)

84 case converts ctxt [] ty pty of

85 OK _ -> return ()

86− Error e -> ierror (CantUnify False ty pty e [] 0)

86+ Error e -> ierror (CantUnify False (ty, Nothing) (pty, Nothing) e [] 0)

87 ptm' <- applyOpts ptm

88 ei <- getErasureInfo `fmap` getIState

89 updateContext (addCasedef n ei (CaseInfo True True False) False (STerm Erased) True False

src/Idris/REPL.hs+16−9

@@ -54,6 +54,7 @@ import Idris.Core.Constraints

54

55import IRTS.Compiler

56import IRTS.CodegenCommon

57+import IRTS.Exports

57import IRTS.System

58import IRTS.System

58

59

59import Control.Category

60import Control.Category

@@ -810,8 +811,8 @@ process fn (NewDefn decls) = do

810 fixClauses :: PDecl' t -> PDecl' t

811 fixClauses :: PDecl' t -> PDecl' t

811 fixClauses (PClauses fc opts _ css@(clause:cs)) =

812 fixClauses (PClauses fc opts _ css@(clause:cs)) =

812 PClauses fc opts (getClauseName clause) css

813 PClauses fc opts (getClauseName clause) css

813− fixClauses (PInstance syn fc constraints cls parms ty instName decls) =

814+ fixClauses (PInstance doc argDocs syn fc constraints cls parms ty instName decls) =

814− PInstance syn fc constraints cls parms ty instName (map fixClauses decls)

815+ PInstance doc argDocs syn fc constraints cls parms ty instName (map fixClauses decls)

815 fixClauses decl = decl

816 fixClauses decl = decl

816

817

817process fn (Undefine names) = undefine names

818process fn (Undefine names) = undefine names

@@ -968,7 +969,7 @@ process fn (DebugUnify l r)

968 = do (ltm, _) <- elabVal recinfo ERHS l

969 = do (ltm, _) <- elabVal recinfo ERHS l

969 (rtm, _) <- elabVal recinfo ERHS r

970 (rtm, _) <- elabVal recinfo ERHS r

970 ctxt <- getContext

971 ctxt <- getContext

971− case unify ctxt [] ltm rtm [] [] [] [] of

972+ case unify ctxt [] (ltm, Nothing) (rtm, Nothing) [] [] [] [] of

972 OK ans -> iputStrLn (show ans)

973 OK ans -> iputStrLn (show ans)

973 Error e -> iputStrLn (show e)

974 Error e -> iputStrLn (show e)

974

975

@@ -1110,7 +1111,7 @@ process fn Execute

1110 t <- codegen

1111 t <- codegen

1111 -- gcc adds .exe when it builds windows programs

1112 -- gcc adds .exe when it builds windows programs

1112 progName <- return $ if isWindows then tmpn ++ ".exe" else tmpn

1113 progName <- return $ if isWindows then tmpn ++ ".exe" else tmpn

1113− ir <- compile t tmpn m

1114+ ir <- compile t tmpn (Just m)

1114 runIO $ generate t (fst (head (idris_imported ist))) ir

1115 runIO $ generate t (fst (head (idris_imported ist))) ir

1115 case idris_outputmode ist of

1116 case idris_outputmode ist of

1116 RawOutput h -> do runIO $ rawSystem progName []

1117 RawOutput h -> do runIO $ rawSystem progName []

@@ -1122,9 +1123,13 @@ process fn Execute

1122process fn (Compile codegen f)

1123process fn (Compile codegen f)

1123 | map toLower (takeExtension f) `elem` [".idr", ".lidr", ".idc"] =

1124 | map toLower (takeExtension f) `elem` [".idr", ".lidr", ".idc"] =

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

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

1126+ | otherwise = do opts <- getCmdLine

1127+ let iface = Interface `elem` opts

1128+ m <- if iface then return Nothing else

1125− | otherwise = do (m, _) <- elabVal recinfo ERHS

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

1126− (PApp fc (PRef fc (sUN "run__IO"))

1130+ (PApp fc (PRef fc (sUN "run__IO"))

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

1131+ [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

1132+ return (Just m')

1128 ir <- compile codegen f m

1133 ir <- compile codegen f m

1129 i <- getIState

1134 i <- getIState

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

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

@@ -1418,9 +1423,10 @@ loadInputs inputs toline -- furthest line to read in input source files

1418 ist <- getIState

1423 ist <- getIState

1419 putIState (ist { idris_tyinfodata = tidata,

1424 putIState (ist { idris_tyinfodata = tidata,

1420 idris_patdefs = patdefs })

1425 idris_patdefs = patdefs })

1426+ exports <- findExports

1421

1427

1422 case opt getOutput opts of

1428 case opt getOutput opts of

1423− [] -> performUsageAnalysis -- interactive

1429+ [] -> performUsageAnalysis (getExpNames exports) -- interactive

1424 _ -> return [] -- batch, will be checked by the compiler

1430 _ -> return [] -- batch, will be checked by the compiler

1425

1431

1426 return (map fst ifiles))

1432 return (map fst ifiles))

@@ -1515,7 +1521,8 @@ idrisMain opts =

1515 xs -> last xs

1521 xs -> last xs

1516 setOptLevel optimise

1522 setOptLevel optimise

1517 let outty = case opt getOutputTy opts of

1523 let outty = case opt getOutputTy opts of

1524+ [] -> if Interface `elem` opts then

1518− [] -> Executable

1525+ Object else Executable

1519 xs -> last xs

1526 xs -> last xs

1520 let cgn = case opt getCodegen opts of

1527 let cgn = case opt getCodegen opts of

1521 [] -> Via "c"

1528 [] -> Via "c"

src/Idris/TypeSearch.hs+4−2

@@ -278,7 +278,7 @@ inArgTys = map . first . second

278

279typeclassUnify :: Ctxt ClassInfo -> Context -> Type -> Type -> Maybe [(Name, Type)]

280typeclassUnify classInfo ctxt ty tyTry = do

281− res <- tcToMaybe $ match_unify ctxt [] ty retTy [] theHoles []

281+ res <- tcToMaybe $ match_unify ctxt [] (ty, Nothing) (retTy, Nothing) [] theHoles []

282 guard $ null (theHoles \\ map fst res)

283 let argTys' = map (second $ foldr (.) id [ subst n t | (n, t) <- res ]) tcArgs

284 return argTys'

@@ -424,7 +424,9 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

424 unifyQueue state [] = return state

425 unifyQueue state ((ty1, ty2) : queue) = do

426 --trace ("go: \n" ++ show state) True `seq` return ()

427− res <- tcToMaybe $ match_unify ctxt [ (n, Pi Nothing ty (TType (UVar 0))) | (n, ty) <- holes state] ty1 ty2 [] (map fst $ holes state) []

427+ res <- tcToMaybe $ match_unify ctxt [ (n, Pi Nothing ty (TType (UVar 0))) | (n, ty) <- holes state]

428+ (ty1, Nothing)

429+ (ty2, Nothing) [] (map fst $ holes state) []

428 (state', queueAdditions) <- resolveUnis res state

430 (state', queueAdditions) <- resolveUnis res state

429 guard $ scoreCriterion (score state')

431 guard $ scoreCriterion (score state')

430 unifyQueue state' (queue ++ queueAdditions)

432 unifyQueue state' (queue ++ queueAdditions)

test/Makefile+1−7

@@ -7,14 +7,8 @@ test: $(TESTS)

7%.test:

8 @perl ./runtest.pl $(patsubst %.test,%,$@)

9

10−test_java:

11− @perl ./runtest.pl without primitives004 --codegen Java

12−

13test_js:

10test_js:

14− @perl ./runtest.pl without sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 effects003 buffer001 basic007 basic011 primitives004 --codegen node

11+ @perl ./runtest.pl without sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 effects003 buffer001 basic007 basic011 primitives004 ffi006 --codegen node

15−

16−test_llvm:

17− @perl ./runtest.pl without primitives003 primitives004 sugar004 io003 buffer001 --codegen llvm

18

12

19update:

13update:

20 /usr/bin/env perl ./runtest.pl all -u

14 /usr/bin/env perl ./runtest.pl all -u

test/basic006/expected+2−2

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

1test020a.idr:16:18:When elaborating right hand side of foo:

2When elaborating an application of function Prelude.List.reverse:

3 Can't unify

4− Vect n a

4+ Vect n a (Type of xs)

5 with

6− List a

6+ List a (Expected type)

7[3, 2, 1]

8"Number 42"

test/docs001/docs001.idrnew file+20

@@ -0,0 +1,20 @@

1+||| class

2+||| @ t a type

3+class C (t : Type) where

4+ ||| member of class

5+ m : t

6+

7+||| type

8+data A = B

9+

10+||| type 2

11+data D a b = E

12+

13+||| instance of class

14+instance C A where

15+ m = B

16+

17+||| another instance of class

18+||| @ a parameter type

19+instance C (D a b) where

20+ m = E

test/docs001/expectednew file+18

@@ -0,0 +1,18 @@

1+Type checking ./docs001.idr

2+*docs001> Type class C

3+ class

4+

5+Parameters:

6+ t -- a type

7+

8+Methods:

9+ m : C t => t

10+ member of class

11+

12+Instances:

13+ C A

14+ instance of class

15+ C (D a b)

16+ another instance of class

17+ a -- parameter type

18+*docs001> Bye bye

test/docs001/inputnew file+1

@@ -0,0 +1 @@

1+:doc C

test/docs001/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --nobanner --nocolor docs001.idr < input

3+rm *.ibc

test/docs002/docs002.idrnew file+20

@@ -0,0 +1,20 @@

1+module Main

2+

3+-- Simple test case for type provider documentation.

4+

5+import Providers

6+

7+%language TypeProviders

8+

9+getType : Int -> IO (Provider Type)

10+getType 0 = return (Provide Int)

11+getType _ = return (Provide Bool)

12+

13+||| Some documentation

14+%provide (T1 : Type) with getType 0

15+

16+||| Some other documentation

17+%provide (T2 : Type) with getType 1

18+

19+||| Some provided postulate

20+%provide postulate T3 with getType 0

test/docs002/expectednew file+11

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

1+Type checking ./docs002.idr

2+*docs002> T1 : Type

3+ Some documentation

4+

5+*docs002> T2 : Type

6+ Some other documentation

7+

8+*docs002> T3 : Int

9+ Some provided postulate

10+

11+*docs002> Bye bye

test/docs002/inputnew file+3

@@ -0,0 +1,3 @@

1+:doc T1

2+:doc T2

3+:doc T3

test/docs002/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --nobanner --nocolor docs002.idr < input

3+rm *.ibc

test/error005/error005.idr+7

@@ -18,3 +18,10 @@ ok n = 1

18

19notOk : (n : Nat) -> Fin (plus 2 n)

20notOk n = 2

21+

22+b0rken : Integer -> Fin 3

23+b0rken n = fromInteger n

24+

25+x : Fin 4

26+x = the (Fin 4) 5

27+

test/error005/expected+12−4

@@ -1,12 +1,20 @@

1error005.idr:13:1:When elaborating right hand side of two:

2When elaborating argument prf to function Data.Fin.fromInteger:

3 When using 2 as a literal for a Fin 2

4− Could not show that 2 is less than 2

4+ 2 is not strictly less than 2

5error005.idr:16:1:When elaborating right hand side of hahaha:

6When elaborating argument prf to function Data.Fin.fromInteger:

7 When using 0 as a literal for a Fin n

8− Could not show that 0 is less than n

8+ 0 is not strictly less than n

9−error005.idr:21:1:When elaborating right hand side of notOk:

9+error005.idr:22:1:When elaborating right hand side of notOk:

10When elaborating argument prf to function Data.Fin.fromInteger:

11 When using 2 as a literal for a Fin (S (S n))

12+ 2 is not strictly less than S (S n)

13+error005.idr:23:24:When elaborating right hand side of b0rken:

14+When elaborating argument prf to function Data.Fin.fromInteger:

15+ When using n as a literal for a Fin 3

12− Could not show that 2 is less than S (S n)

16+ Could not show that n is less than 3 because n is a bound variable instead of a constant Integer

17+error005.idr:28:1:When elaborating right hand side of x:

18+When elaborating argument prf to function Data.Fin.fromInteger:

19+ When using 5 as a literal for a Fin 4

20+ 5 is not strictly less than 4

test/ffi006/expectednew file+2

@@ -0,0 +1,2 @@

1+Ready to show...

2+[10, 20, 30, 40]

test/ffi006/ffi006.cnew file+14

@@ -0,0 +1,14 @@

1+#include "testHdr.h"

2+

3+int main() {

4+

5+ VM* vm = idris_vm();

6+

7+ ListInt x = cons(vm, 10, cons(vm, 20, nil(vm)));

8+ ListInt y = cons(vm, 30, cons(vm, 40, nil(vm)));

9+ ListInt z = addLists(vm, x, y);

10+

11+ printf("%s\n", showList(vm, z));

12+

13+ close_vm(vm);

14+}

test/ffi006/ffi006.idrnew file+30

@@ -0,0 +1,30 @@

1+import Data.List

2+

3+addLists : List Int -> List Int -> List Int

4+addLists xs ys = xs ++ ys

5+

6+nil : List Int

7+nil = []

8+

9+cons : Int -> List Int -> List Int

10+cons x xs = x :: xs

11+

12+show' : List Int -> IO String

13+show' xs = do putStrLn "Ready to show..."

14+ return (show xs)

15+

16+testList : FFI_Export FFI_C "testHdr.h" []

17+testList = Data (List Int) "ListInt" $

18+ Data (List Nat) "ListNat" $

19+ Fun addLists "addLists" $

20+ Fun nil "nil" $

21+ Fun cons "cons" $

22+ Data Nat "Nat" $

23+ Fun Strings.length "lengthS" $

24+ Fun show' "showList" $

25+ End

26+

27+-- main : IO ()

28+-- main = do s <- show' 42

29+-- putStrLn s

30+

test/ffi006/runnew file+5

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

1+#!/usr/bin/env bash

2+idris $@ ffi006.idr --interface -o ffi006.o

3+cc ffi006.c ffi006.o `idris --include` `idris --link` -o ffi006

4+./ffi006

5+rm -f ffi006 *.ibc *.o *.h

test/proof002/expected+2−2

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

1Reflect.idr:208:38:When elaborating right hand side of testReflect1:

2When elaborating an application of function Reflect.getJust:

3 Can't unify

4− IsJust (Just x1)

4+ IsJust (Just x1) (Type of ItIsJust)

5 with

6− IsJust (prove (getProof x))

6+ IsJust (prove (getProof x)) (Expected type)

7

8 Specifically:

9 Can't unify

test/reg007/expected+2−2

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

1reg007.lidr:8:1:A.n is already defined

2reg007.lidr:12:11:When elaborating right hand side of hurrah:

3Can't unify

4− n = lala

4+ n = lala (Type of isSame)

5with

6− 0 = 1

6+ 0 = 1 (Expected type)

7

8Specifically:

9 Can't unify

test/reg023/expected+2−2

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

1reg023.idr:7:5:When elaborating right hand side of bad:

2Can't unify

3− [94mNat[0m

3+ [94mNat[0m (Type of [91m0[0m)

4with

5− [92mf[0m [94mNat[0m

5+ [92mf[0m [94mNat[0m (Expected type)

test/reg044/expected+2−2

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

1reg044.idr:4:4:When elaborating right hand side of Main.pf:

2Can't unify

3− [95mb[0m [94m=[0m [95mb[0m

3+ [95mb[0m [94m=[0m [95mb[0m (Type of [91mRefl[0m)

4with

5− [95ma[0m [94m=[0m [95mb[0m

5+ [95ma[0m [94m=[0m [95mb[0m (Expected type)

6

7Specifically:

8 Can't unify

test/tutorial006/expected+4−4

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

1tutorial006a.idr:5:23:When elaborating right hand side of vapp:

2When elaborating argument [95mxs[0m to constructor [91mData.VectType.Vect.::[0m:

3 Can't unify

4− [94mVect[0m ([95mn[0m [92m+[0m [95mn[0m) [95ma[0m

4+ [94mVect[0m ([95mn[0m [92m+[0m [95mn[0m) [95ma[0m (Type of vapp _ _)

5 with

6− [94mVect[0m ([92mplus[0m [95mn[0m [95mm[0m) [95ma[0m

6+ [94mVect[0m ([92mplus[0m [95mn[0m [95mm[0m) [95ma[0m (Expected type)

7

8 Specifically:

9 Can't unify

@@ -12,9 +12,9 @@ When elaborating argument [95mxs[0m to constructor [91mData.VectType.Vect.::

12 [92mplus[0m [95mn[0m [95mm[0m

13tutorial006b.idr:10:10:When elaborating right hand side of with block in Main.parity:

14Can't unify

15− [94mParity[0m ([92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m))

15+ [94mParity[0m ([92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m)) (Type of [91meven[0m)

16with

17− [94mParity[0m ([91mS[0m ([91mS[0m ([92mplus[0m [95mj[0m [95mj[0m)))

17+ [94mParity[0m ([91mS[0m ([91mS[0m ([92mplus[0m [95mj[0m [95mj[0m))) (Expected type)

18

19Specifically:

20 Can't unify