bb013f0 · Idris-dev · git.iko.soy

CHANGELOG+18−13

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

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

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

2525* 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

2632

2733New in 0.9.16:

2834--------------

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

6066 solved automatically.

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

6268 of large expressions.

63−* EXPERIMENTAL Implementation of uniqueness types

69+* EXPERIMENTAL Implementation of uniqueness types

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

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

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

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

7480 library (see #1516)

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

7682 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.

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

7985 as code examples.

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

8187 provide error messages to IDE clients.

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

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

8389 Engine style)

8490

8591New in 0.9.14:

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

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

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

158164 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

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

161167* Updated 'effects' library

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

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

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

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

188194* 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.

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

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

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

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

211217 types may now depend on earlier methods.

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

213219 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

215221 monadic/do/etc expressions.

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

217223 "if_valid", "if_error", etc.

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

336342Internal changes:

337343

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

339−* Fixed nested parameters blocks

345+* Fixed nested parameters blocks

340346* Improve efficiency of elaborator by:

341347 - only normalising when necessary

342348 - reducing backtracking with resolving ambiguities

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

417423Internal changes:

418424

419425* Some type class resolution fixes

420−* Several minor bug fixes

426+* Several minor bug fixes

421427* Performance improvements in resolving overloading and type classes

422428

423429New in 0.9.1:

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

465471Internal changes:

466472

467473* Everything :-)

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

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

470− which are verified by a minimal type checker.

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

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

476+ which are verified by a minimal type checker.

471477

472478This 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

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

475−

CONTRIBUTORS+1

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

2828raichoo

2929Philip Rasmussen

3030Reynir Reynisson

31+Adam Sandberg Eriksson

3132Seo Sanghyeon

3233Benjamin Saunders

3334Alexander Shabalin

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

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

1010

1111import System.Environment

1212import System.Exit

13+import Control.Monad

1314

1415import Paths_idris

1516

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

18+ interface :: Bool,

1719 output :: FilePath }

1820

1921showUsage = 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>]"

2123

2224getOpts :: IO Opts

2325getOpts = do xs <- getArgs

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

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

2527 where

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

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

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

2831 process opts [] = opts

2932

3033c_main :: Opts -> Idris ()

3134c_main opts = do elabPrims

3235 loadInputs (inputs opts) Nothing

33− mainProg <- elabMain

36+ mainProg <- if interface opts

37+ then liftM Just elabMain

38+ else return Nothing

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

3540 runIO $ codegenC ir

3641

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

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

3232jsMain opts = do elabPrims

3333 loadInputs (inputs opts) Nothing

3434 mainProg <- elabMain

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

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

3636 runIO $ codegenJavaScript ir

3737

3838main :: IO ()

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

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

3232jsMain opts = do elabPrims

3333 loadInputs (inputs opts) Nothing

3434 mainProg <- elabMain

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

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

3636 runIO $ codegenNode ir

3737

3838main :: IO ()

idris.cabal+16

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

394394 test/ffi005/*.idr

395395 test/ffi005/run

396396 test/ffi005/expected

397+ test/ffi006/*.idr

398+ test/ffi006/*.c

399+ test/ffi006/run

400+ test/ffi006/expected

397401

398402 test/idrisdoc001/run

399403 test/idrisdoc001/expected

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

607611 test/unique003/*.idr

608612 test/unique003/expected

609613

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+

610625source-repository head

611626 type: git

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

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

723738 , IRTS.CodegenC

724739 , IRTS.CodegenCommon

725740 , IRTS.CodegenJavaScript

741+ , IRTS.Exports

726742 , IRTS.JavaScript.AST

727743 , IRTS.Compiler

728744 , IRTS.Defunctionalise

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

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

11module Data.Fin

22

33%default total

4+%access public

45

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

67|||

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

144145

145146%language ErrorReflection

146147

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+ ]

147168total

148169finFromIntegerErrors : 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+ ]

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

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

151− , TextPart "as a literal for a"

152− , TermPart `(Fin ~m)

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

154− , TermPart n

155− , TextPart "is less than"

156− , TermPart m

157− ]

158− ]

185+ = mkFinIntegerErr n m

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

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

188+ ]

159189finFromIntegerErrors _ = Nothing

160190

161191%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

22

33import Data.Fin

44

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

66%default total

77

88namespace Vect {

9−

9+

1010infixr 7 ::

1111

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

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

531531

532532 fs <*> vs = zipWith apply fs vs

533533

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

535+||| uses the diagonal.

534536instance Monad (Vect n) where

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

536538

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

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

540542

541543--------------------------------------------------------------------------------

542−-- Show

544+-- Show

543545--------------------------------------------------------------------------------

544546

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

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

595597

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

597599-- internal implementations.

598−

libs/prelude/IO.idr+53−4

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

2121WorldRes x = x

2222

2323record 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

2527

2628abstract

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

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

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

9092liftPrimIO = MkIO

9193

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

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

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

99+run__IO f = call__IO f

94100

95101unsafePerformIO : IO' ffi a -> a

96102unsafePerformIO (MkIO f) = unsafePerformPrimIO

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

143149 C_IntT : C_IntTypes i -> C_Types i

144150

145151FFI_C : FFI

146−FFI_C = MkFFI C_Types String

152+FFI_C = MkFFI C_Types String String

147153

148154IO : Type -> Type

149155IO = IO' FFI_C

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

194200%used MkJsFn x

195201

196202FFI_JS : FFI

197−FFI_JS = MkFFI JS_Types String

203+FFI_JS = MkFFI JS_Types String String

198204

199205JS_IO : Type -> Type

200206JS_IO = IO' FFI_JS

201207

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

195195instance MinBound Nat where

196196 minBound = Z

197197

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

198199instance Cast Integer Nat where

199200 cast = fromInteger

200201

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

250251 bottom = Z

251252

252253

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

253255instance Cast Int Nat where

254256 cast i = fromInteger (cast i)

255257

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

333335

334336

335337--------------------------------------------------------------------------------

336−-- An informative comparison view

338+-- An informative comparison view

337339--------------------------------------------------------------------------------

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

339341 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,

6363 return vm;

6464}

6565

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+

6680void init_threadkeys() {

6781#ifdef HAS_PTHREAD

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

rts/idris_rts.h+5

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

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

126126Stats terminate(VM* vm);

127127

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+

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

129134void init_threadkeys();

130135

src/IRTS/CodegenC.hs+124−17

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

2424import Debug.Trace

2525

2626codegenC :: CodeGenerator

27−codegenC ci = codegenC' (simpleDecls ci)

28− (outputFile ci)

29− (outputType ci)

30− (includes ci)

31− (compileObjs ci)

32− (map mkLib (compileLibs ci) ++

33− map incdir (importDirs ci))

34− (compilerFlags ci)

35− (debugLevel ci)

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

28+ (outputFile ci)

29+ (outputType ci)

30+ (includes ci)

31+ (compileObjs ci)

32+ (map mkLib (compileLibs ci) ++

33+ map incdir (importDirs ci))

34+ (compilerFlags ci)

35+ (exportDecls ci)

36+ (interfaces ci)

37+ (debugLevel ci)

38+ when (interfaces ci) $

39+ codegenH (exportDecls ci)

3640

3741 where mkLib l = "-l" ++ l

3842 incdir i = "-I" ++ i

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

4448 [String] -> -- extra object files

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

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

51+ [ExportIFace] ->

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

4753 DbgLevel ->

4854 IO ()

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

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

5056 = do -- print defs

5157 let bc = map toBC defs

5258 let h = concatMap toDecl (map fst bc)

5359 let cc = concatMap (uncurry toC) bc

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

5461 d <- getDataDir

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

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

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

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

5865 case exec of

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

6067 Raw -> writeFile out cout

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

6774 libFlags <- getLibFlags

6875 incFlags <- getIncFlags

6976 let args = [gccDbg dbg] ++

70− gccFlags ++

77+ gccFlags iface ++

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

7279 ["-DHAS_PTHREAD", "-DIDRIS_ENABLE_STATS", "-msse2",

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

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

7582 [tmpn] ++

76− concatMap words libFlags ++

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

7784 concatMap words incFlags ++

78− concatMap words libs ++

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

7986 concatMap words flags ++

8087 ["-o", out]

81−-- putStrLn gcc

88+-- putStrLn (show args)

8289 exit <- rawSystem comp args

8390 when (exit /= ExitSuccess) $

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

92+ where

93+ getExp (Export _ _ exp) = exp

8594

8695headers xs =

8796 concatMap

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

93102

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

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

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

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

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

97107

98108gccDbg DEBUG = "-g"

99109gccDbg TRACE = "-O2"

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

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

312322toFType (FApp c [_])

313323 | c == sUN "C_Any" = FAny

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

324+toFType t = FAny

315325

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

317327c_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 (

561571

562572flUnOp :: String -> String -> String

563573flUnOp 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,

3333 debugLevel :: DbgLevel,

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

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

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

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

37+ interfaces :: Bool,

38+ exportDecls :: [ExportIFace]

3739 }

3840

3941type CodeGenerator = CodegenInfo -> IO ()

src/IRTS/Compiler.hs+21−11

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

1111import IRTS.DumpBC

1212import IRTS.CodegenJavaScript

1313import IRTS.Inliner

14+import IRTS.Exports

1415

1516import Idris.AbsSyntax

1617import Idris.AbsSyntaxTree

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

4546

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

4748-- generate code.

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

49−compile codegen f tm

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

50+compile codegen f mtm

5051 = do checkMVs -- check for undefined metavariables

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

52− reachableNames <- performUsageAnalysis

53− maindef <- irMain tm

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

53+ exports <- findExports

54+

55+ reachableNames <- performUsageAnalysis (getExpNames exports)

56+ maindef <- case mtm of

57+ Nothing -> return []

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

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

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

5561 objs <- getObjectFiles codegen

5662 libs <- getLibs codegen

5763 flags <- getFlags codegen

5864 hdrs <- getHdrs codegen

5965 impdirs <- allImportDirs

60− defsIn <- mkDecls tm reachableNames

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

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+

72+ let defs = defsIn ++ maindef

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

6374 -- Inlined top level LDecl made here

6475 let defsInlined = inlineAll defs

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

89100 triple <- Idris.AbsSyntax.targetTriple

90101 cpu <- Idris.AbsSyntax.targetCPU

91102 iLOG "Building output"

92−

93103 case checked of

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

95105 hdrs impdirs objs libs flags

96106 NONE c (toAlist defuns)

97− tagged

107+ tagged iface exports

98108-- runIO $ case codegen of

99109-- ViaC -> codegenC cginfo

100110-- ViaJava -> codegenJava cginfo

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

133143 i <- irTerm M.empty [] tm

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

135145

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

137−mkDecls t used

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

147+mkDecls used

138148 = do i <- getIState

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

140150 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

2929 Int Name [LExp]

3030 | LCase CaseType LExp [LAlt]

3131 | LConst Const

32− | LForeign FDesc -- Function descriptor

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

3333 FDesc -- Return type descriptor

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

3535 | LOp PrimFn [LExp]

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

4040data FDesc = FCon Name

4141 | FStr String

4242 | FUnknown

43+ | FIO FDesc

4344 | FApp Name [FDesc]

4445 deriving (Show, Eq)

4546

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+

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

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

4861

src/Idris/AbsSyntax.hs+27−17

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

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

9797

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

99−addImported pub f

99+addImported pub f

100100 = do i <- getIState

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

102102

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

129129addErasureUsage n i = do ist <- getIState

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

131131

132+addExport :: Name -> Idris ()

133+addExport n = do ist <- getIState

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

135+

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

133−addUsedName fc n arg

137+addUsedName fc n arg

134138 = do ist <- getIState

135139 case lookupTyName n (tt_ctxt ist) of

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

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

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

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

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

140− addErasureUsage n i

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

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

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

144+ addErasureUsage n i

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

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

143147

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

145149getErasureUsage = do ist <- getIState;

146150 return (idris_erasureUsed ist)

147151

152+getExports :: Idris [Name]

153+getExports = do ist <- getIState

154+ return (idris_exports ist)

155+

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

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

150158

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

260268

261269 where errWhen True

262270 = throwError (At fc

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

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

264272 errWhen False = return ()

265273

266274isTyInferred :: Name -> Idris Bool

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

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

10751083 pDocs

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

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

1078− = PInstance info f

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

1086+ = PInstance doc argDocs info f

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

10801088 n

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

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

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

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

12941302 where

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

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

12951305 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')

12971307 argInfo n (Exp opt _ _) t'

12981308 = (InaccessibleArg `elem` opt,

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

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

15421552 PLam fc n ty' sc'

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

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

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

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

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

15471557 = case lookupDef n (tt_ctxt ist) of

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

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

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

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

17181728 t' <- sl t

1719− r' <- sl r

1729+ r' <- sl r

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

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

17221732 args' <- mapM slA args

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

19151925 match (PHidden x) (PHidden y)

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

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

1918− match (PHidden x) y

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

1928+ match (PHidden x) y

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

19201930 | otherwise = return []

1921− match x (PHidden y)

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

1931+ match x (PHidden y)

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

19231933 | otherwise = return []

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

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

src/Idris/AbsSyntaxTree.hs+35−28

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

5757 liftname :: Name -> Name,

5858 namespace :: Maybe [String],

5959 elabFC :: Maybe FC,

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

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

6161 Idris () }

6262

6363toplevel :: ElabInfo

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

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

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

227227 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

229230 }

230231

231232-- Required for parsers library, and therefore trifecta

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

297298 | IBCParsedRegion FC

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

299300 | IBCUsage (Name, Int)

301+ | IBCExport Name

300302 deriving Show

301303

302304-- | The initial state for the compiler

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

309311 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

310312 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

311313 (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 []

313315

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

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

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

419421 | NoREPL

420422 | OLogging Int

421423 | Output String

424+ | Interface

422425 | TypeCase

423426 | TypeInType

424427 | DefaultTotal

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

598601 [PDecl' t] -- declarations

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

600603 -- class name, parameters, method declarations

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

602− Name -- class

603− [t] -- parameters

604− t -- full instance type

605− (Maybe Name) -- explicit name

606− [PDecl' t]

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

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

604+ | PInstance

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

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

607+ SyntaxInfo

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

609+ Name -- class

610+ [t] -- parameters

611+ t -- full instance type

612+ (Maybe Name) -- explicit name

613+ [PDecl' t]

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

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

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

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

610618 | PSyntax FC Syntax -- ^ Syntax definition

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

612620 | 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

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

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

616624 deriving Functor

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

685693declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

689697declared (PDSL n _) = [n]

690698declared (PSyntax _ _) = []

691699declared (PMutual _ ds) = concatMap declared ds

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

704712tldeclared (PMutual _ ds) = concatMap tldeclared ds

705713tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

708716tldeclared _ = []

709717

710718defined :: PDecl -> [Name]

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

720728defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

724732defined (PDSL n _) = [n]

725733defined (PSyntax _ _) = []

726734defined (PMutual _ ds) = concatMap defined ds

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

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

776784 | PHidden PTerm -- ^ Irrelevant or hidden pattern

777785 | PType -- ^ 'Type' type

778− | PUniverse Universe -- ^ Some universe

786+ | PUniverse Universe -- ^ Some universe

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

780788 | PConstant Const -- ^ Builtin types

781789 | Placeholder -- ^ Underscore

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

11101118 | Expr Name

11111119 | SimpleExpr Name

11121120 deriving (Show, Eq)

1113−

1121+

11141122

11151123{-!

11161124deriving instance Binary SSymbol

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

13851393 where

13861394 startPrec = 0

13871395 funcAppPrec = 10

1388−

1396+

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

13901398 prettySe p bnd (PQuote r) =

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

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

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

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

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

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

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

14521460 bracket p funcAppPrec $

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

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

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

14641472 Just (Infixr p') -> p'

14651473 Just f' -> prec f' + 1

14661474 inFix l r = align . group $

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

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

14681476 group (prettySe right bnd r)

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

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

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

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

14841492 indent 2 (vsep (map ppcase cases))

14851493 where

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

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

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

14881496 in nest nestingSize $

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

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

15541562 prettyAs =

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

15561564 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)

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

15591567 -- XXX: add pretty for tactics

15601568 prettySe p bnd (PProof ts) =

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

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

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

17221730 = 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)

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

17251733showDeclImp _ _ = text "..."

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

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

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

18971905 where

18981906 ni env (PRef _ n)

1899− | not (n `elem` env)

1907+ | not (n `elem` env)

19001908 = case lookupTy n (tt_ctxt ist) of

19011909 [] -> [n]

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

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

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

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

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

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

19071915 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 ++

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

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

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

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

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

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

19371945 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 ++

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

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

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

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

19942002 case lookupCtxtExact n (idris_optimisation ist) of

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

19962004 Nothing -> []

1997−

src/Idris/CmdOptions.hs+1

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

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

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

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

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

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

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

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

src/Idris/Core/Binary.hs+12

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

2323 3 -> fmap SubReport get

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

2525

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+

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

2739 put (Msg str) = do putWord8 0

2840 put str

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

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

88import Control.Arrow

99import Control.Monad.RWS

1010import Control.Monad.State

11+import qualified Data.Set as S

1112import Data.List

1213import Data.Maybe

1314import qualified Data.Map.Strict as M

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

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

2021 where lhs (ULT l _) = l

2122 lhs (ULE l _) = l

22− cs' = nub cs

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

2324 rels = mkRels cs' M.empty

2425

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

src/Idris/Core/DeepSeq.hs+4

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

4343instance NFData FC where

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

4545

46+instance NFData Provenance where

47+ rnf ExpectedType = ()

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

49+

4650instance NFData Err where

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

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

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

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

727727 if (length ps' > length ps) then

728728 case reverse ps' of

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

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

730+ let (xp, yp) = getProvenance inerr

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

731732 lift $ tfail $

732733 case err of

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

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

734735 Just e -> e

735736 else return $! ()

736737

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

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

99 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

1010 addDatatype, addCasedef, simplifyCasedef, addOperator,

1111 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

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

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

1313 mapDefCtxt,

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

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

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

10071007 _ -> False

10081008

10091009lookupP :: 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

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

10121015 p <- case def of

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

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

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

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

10171020 case snd p of

1018− Hidden -> []

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

10191022 _ -> return (fst p)

10201023

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

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

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

66

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

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

9− doneElaboratingArgPS, dropGiven, keepGiven) where

9+ doneElaboratingArgPS, dropGiven, keepGiven, getProvenance) where

1010

1111import Idris.Core.Typecheck

1212import Idris.Core.Evaluate

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

154154qshow :: Fails -> String

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

156156

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

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

158+ (TT Name, Maybe Provenance) ->

159+ (TT Name, Maybe Provenance) ->

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

159−match_unify' ctxt env topx topy =

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

160162 do ps <- get

161163 let while = while_elaborating ps

162164 let dont = dontunify ps

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

168170 ++ "\n"

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

170172 ) $

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

172174 OK u -> traceWhen (unifylog ps)

173175 ("Matched " ++ show u) $

174176 do let (h, ns) = unified ps

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

196198 = do ps <- get

197199 let probs = problems ps

198200 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,

200202 [], Unify)] })

201203 merge acc ns

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

203205

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

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

207+ (TT Name, Maybe Provenance) ->

208+ (TT Name, Maybe Provenance) ->

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

206−unify' ctxt env topx topy =

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

207211 do ps <- get

208212 let while = while_elaborating ps

209213 let dont = dontunify ps

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

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

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

218222 ++ "\n") $

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

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

220224 (map fst (notunified ps)) while

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

222226-- P _ _ _ -> False

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

456460unifyGoal :: Raw -> RunTactic

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

458462 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)

460464 return h

461465

462466exact :: Raw -> RunTactic

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

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

474478-- let valtyn = normalise ctxt env valty

475479-- 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)

477482 ps <- get

478483 let (uh, uns) = unified ps

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

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

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

489494-- let valtyn = normalise ctxt env valty

490495-- let tyn = normalise ctxt env ty

491− ns <- match_unify' ctxt env valty ty

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

492497 ps <- get

493498 let (uh, uns) = unified ps

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

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

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

507512 do let guess = forget val

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

509− ns <- unify' ctxt env valty ty

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

510515 ps <- get

511516 let (uh, uns) = unified ps

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

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

524529 dropdots <-

525530 case lookup x (notunified ps) of

526531 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)

528533 return [x]

529534 _ -> return []

530535 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' =

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

568573 case t' of

569574 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)

571576 ps <- get

572577 let (uh, uns) = unified ps

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

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

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

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

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

596− unify' ctxt env tyt (TType (UVar 0))

597− unify' ctxt env t (TType (UVar 0))

601+ unify' ctxt env (tyt, Nothing) (TType (UVar 0), Nothing)

602+ unify' ctxt env (t, Nothing) (TType (UVar 0), Nothing)

598603 return $ Bind n (Pi impl tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))

599604forall n impl ty ctxt env _ = fail "Can't pi bind here"

600605

@@ -822,8 +827,8 @@ updateError ns (At f e) = At f (updateError ns e)

822827updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)

823828updateError ns (ElaboratingArg f a env e)

824829 = ElaboratingArg f a env (updateError ns e)

825−updateError ns (CantUnify b l r e xs sc)

826− = CantUnify b (updateSolvedTerm ns l) (updateSolvedTerm ns r) (updateError ns e) xs sc

830+updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)

831+ = CantUnify b (updateSolvedTerm ns l, lp) (updateSolvedTerm ns r, rp) (updateError ns e) xs sc

827832updateError ns e = e

828833

829834solveInProblems x val [] = []

@@ -837,7 +842,7 @@ mergeNotunified env holes ns = mnu ns [] [] where

837842 mnu ((n, t):ns) ns_acc ps_acc

838843 | Just t' <- lookup n ns, t /= t'

839844 = 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)

841846 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc

842847

843848updateNotunified [] nu = nu

@@ -846,6 +851,10 @@ updateNotunified ns nu = up nu where

846851 up ((n, t) : nus) = let t' = updateSolvedTerm ns t in

847852 ((n, t') : up nus)

848853

854+getProvenance :: Err -> (Maybe Provenance, Maybe Provenance)

855+getProvenance (CantUnify _ (_, lp) (_, rp) _ _ _) = (lp, rp)

856+getProvenance _ = (Nothing, Nothing)

857+

849858updateProblems :: ProofState -> [(Name, TT Name)] -> Fails

850859 -> ([(Name, TT Name)], Fails)

851860-- updateProblems ctxt [] ps inj holes = ([], ps)

@@ -860,11 +869,12 @@ updateProblems ps updates probs = up updates probs where

860869 up ns (prob@(x, y, ready, env, err, while, um) : ps) =

861870 let (x', newx) = updateSolvedTerm' ns x

862871 (y', newy) = updateSolvedTerm' ns y

872+ (lp, rp) = getProvenance err

863873 err' = updateError ns err

864874 env' = updateEnv ns env in

865875 if newx || newy || ready ||

866876 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

868878 OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v)) $

869879 up (ns ++ v) ps

870880 e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $

@@ -887,9 +897,10 @@ matchProblems all ps updates probs = up updates probs where

887897 | all || um == Match =

888898 let x' = updateSolvedTerm ns x

889899 y' = updateSolvedTerm ns y

900+ (lp, rp) = getProvenance err

890901 err' = updateError ns err

891902 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

893904 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

894905 up (ns ++ v) ps

895906 _ -> 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

5353 fc_start :: (Int, Int), -- ^ Line and column numbers for the start of the location span

5454 fc_end :: (Int, Int) -- ^ Line and column numbers for the end of the location span

5555 }

56− deriving (Data, Typeable)

56+ deriving (Data, Typeable, Ord)

5757

5858-- | Ignore source location equality (so deriving classes do not compare FCs)

5959instance Eq FC where

@@ -120,12 +120,22 @@ data ErrorReportPart = TextPart String

120120-- Please remember to keep Err synchronised with

121121-- Language.Reflection.Errors.Err in the stdlib!

122122

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+

123131-- | Idris errors. Used as exceptions in the compiler, but reported to users

124132-- if they reach the top level.

125133data Err' t

126134 = Msg String

127135 | InternalMsg String

128− | CantUnify Bool t t (Err' t) [(Name, t)] Int

136+ | CantUnify Bool (t, Maybe Provenance) -- Expected type, provenance

137+ (t, Maybe Provenance) -- Actual type, provenance

138+ (Err' t) [(Name, t)] Int

129139 -- Int is 'score' - how much we did unify

130140 -- Bool indicates recoverability, True indicates more info may make

131141 -- unification succeed

@@ -211,7 +221,7 @@ instance Sized ErrorReportPart where

211221instance Sized Err where

212222 size (Msg msg) = length msg

213223 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

215225 size (InfiniteUnify _ right _) = size right

216226 size (CantConvert left right _) = size left + size right

217227 size (UnifyScope _ _ right _) = size right

@@ -263,7 +273,7 @@ instance Show Err where

263273

264274instance Pretty Err OutputAnnotation where

265275 pretty (Msg m) = text m

266− pretty (CantUnify _ l r e _ i) =

276+ pretty (CantUnify _ (l, _) (r, _) e _ i) =

267277 text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r <+>

268278 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

269279 pretty (ProviderError msg) = text msg

@@ -783,7 +793,7 @@ instance Show UExp where

783793-- | Universe constraints

784794data UConstraint = ULT UExp UExp -- ^ Strictly less than

785795 | ULE UExp UExp -- ^ Less than or equal to

786− deriving Eq

796+ deriving (Eq, Ord)

787797

788798instance Show UConstraint where

789799 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

8181 Env -> Raw -> StateT UCs TC (Term, Type)

8282 chk u env (Var n)

8383 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

84− | (P nt n' ty : _) <- lookupP n ctxt = return (P nt 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

87+ = return (P nt n' ty, ty)

8588 | otherwise = do lift $ tfail $ NoSuchVariable n

8689 chk u env ap@(RApp f a)

8790 = do (fv, fty) <- chk u env f

src/Idris/Core/Unify.hs+29−21

@@ -51,7 +51,7 @@ data UResult a = UOK a

5151 | UFail Err

5252

5353-- | 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

5555cantUnify [] r t1 t2 e ctxt i = CantUnify r t1 t2 e ctxt i

5656cantUnify (FailContext fc f x : prev) r t1 t2 e ctxt i =

5757 At fc (ElaboratingArg f x

@@ -61,13 +61,15 @@ cantUnify (FailContext fc f x : prev) r t1 t2 e ctxt i =

6161-- Solve metavariables by matching terms against each other

6262-- Not really unification, of course!

6363

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] ->

6567 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 =

6769 case runStateT (un [] (renameBindersTm env topx)

6870 (renameBindersTm env topy)) (UI 0 []) of

6971 OK (v, UI _ []) ->

70− do v' <- trimSolutions topx topy from env v

72+ do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v

7173 return (map (renameBinders env) v')

7274 res ->

7375 let topxn = renameBindersTm env (normalise ctxt env topx)

@@ -75,14 +77,14 @@ match_unify ctxt env topx topy inj holes from =

7577 case runStateT (un [] topxn topyn)

7678 (UI 0 []) of

7779 OK (v, UI _ fails) ->

78− do v' <- trimSolutions topx topy from env v

80+ do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v

7981 return (map (renameBinders env) v')

8082 Error e ->

8183 -- just normalise the term we're matching against

8284 case runStateT (un [] topxn topy)

8385 (UI 0 []) of

8486 OK (v, UI _ fails) ->

85− do v' <- trimSolutions topx topy from env v

87+ do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v

8688 return (map (renameBinders env) v')

8789 _ -> tfail e

8890 where

@@ -143,7 +145,7 @@ match_unify ctxt env topx topy inj holes from =

143145 let r = recoverable (normalise ctxt env x)

144146 (normalise ctxt env y)

145147 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

147149 if (not r) then lift $ tfail err

148150 else do put (UI s ((x, y, True, env, err, from, Match) : f))

149151 lift $ tfail err

@@ -157,8 +159,9 @@ match_unify ctxt env topx topy inj holes from =

157159 uB bnames x y = do UI s f <- get

158160 let r = recoverable (normalise ctxt env (binderTy x))

159161 (normalise ctxt env (binderTy y))

160− let err = cantUnify from r topx topy

161− (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

162+ let err = cantUnify from r (topx, xfrom) (topy, yfrom)

163+ (CantUnify r (binderTy x, Nothing)

164+ (binderTy y, Nothing) (Msg "") (errEnv env) s)

162165 (errEnv env) s

163166 put (UI s ((binderTy x, binderTy y,

164167 False,

@@ -179,7 +182,8 @@ match_unify ctxt env topx topy inj holes from =

179182 let r = recoverable (normalise ctxt env x)

180183 (normalise ctxt env y)

181184 let err = cantUnify from r

182− topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

185+ (topx, xfrom) (topy, yfrom)

186+ (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s

183187 put (UI s ((x, y, True, env, err, from, Match) : f))

184188 lift $ tfail err

185189 combine bnames as [] = return as

@@ -241,7 +245,7 @@ renameBindersTm env tm = uniqueBinders (map fst env) tm

241245 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)

242246 explicitHole t = t

243247

244−trimSolutions topx topy from env topns = followSols [] (dropPairs topns)

248+trimSolutions (topx, xfrom) (topy, yfrom) from env topns = followSols [] (dropPairs topns)

245249 where dropPairs [] = []

246250 dropPairs (n@(x, P _ x' _) : ns)

247251 | x == x' = dropPairs ns

@@ -258,7 +262,7 @@ trimSolutions topx topy from env topns = followSols [] (dropPairs topns)

258262 = do vs' <- case t' of

259263 P _ tn _ ->

260264 if (n, tn) `elem` vs then -- cycle

261− tfail (cantUnify from False topx topy

265+ tfail (cantUnify from False (topx, xfrom) (topy, yfrom)

262266 (Msg "") (errEnv env) 0)

263267 else return ((n, tn) : vs)

264268 _ -> return vs

@@ -280,16 +284,18 @@ hasv (App f a) = hasv f || hasv a

280284hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

281285hasv _ = False

282286

283−unify :: Context -> Env -> TT Name -> TT Name ->

287+unify :: Context -> Env ->

288+ (TT Name, Maybe Provenance) ->

289+ (TT Name, Maybe Provenance) ->

284290 [Name] -> [Name] -> [Name] -> [FailContext] ->

285291 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 =

287293-- traceWhen (hasv topx || hasv topy)

288294-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $

289295 -- don't bother if topx and topy are different at the head

290296 case runStateT (un False [] (renameBindersTm env topx)

291297 (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

293299 return (map (renameBinders env) v', [])

294300 res ->

295301 let topxn = renameBindersTm env (normalise ctxt env topx)

@@ -298,7 +304,7 @@ unify ctxt env topx topy inj holes usersupp from =

298304 case runStateT (un False [] topxn topyn)

299305 (UI 0 []) of

300306 OK (v, UI _ fails) ->

301− do v' <- trimSolutions topx topy from env v

307+ do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v

302308 return (map (renameBinders env) v', reverse fails)

303309-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

304310 Error e -> tfail e

@@ -470,7 +476,7 @@ unify ctxt env topx topy inj holes usersupp from =

470476 let r = recoverable (normalise ctxt env x)

471477 (normalise ctxt env y)

472478 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

474480 if (not r) then lift $ tfail err

475481 else do put (UI s ((x, y, True, env, err, from, Unify) : f))

476482 return [] -- lift $ tfail err

@@ -569,7 +575,8 @@ unify ctxt env topx topy inj holes usersupp from =

569575 = do UI s f <- get

570576 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

571577 let err = cantUnify from r

572− topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

578+ (topx, xfrom) (topy, yfrom)

579+ (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s

573580 put (UI s ((topx, topy, True, env, err, from, Unify) : f))

574581 return []

575582

@@ -577,7 +584,8 @@ unify ctxt env topx topy inj holes usersupp from =

577584 unifyFail x y = do UI s f <- get

578585 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

579586 let err = cantUnify from r

580− topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

587+ (topx, xfrom) (topy, yfrom)

588+ (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s

581589 put (UI s ((topx, topy, True, env, err, from, Unify) : f))

582590 lift $ tfail err

583591

@@ -599,8 +607,8 @@ unify ctxt env topx topy inj holes usersupp from =

599607 uB bnames x y = do UI s f <- get

600608 let r = recoverable (normalise ctxt env (binderTy x))

601609 (normalise ctxt env (binderTy y))

602− let err = cantUnify from r topx topy

603− (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

610+ let err = cantUnify from r (topx, xfrom) (topy, yfrom)

611+ (CantUnify r (binderTy x, Nothing) (binderTy y, Nothing) (Msg "") (errEnv env) s)

604612 (errEnv env) s

605613 put (UI s ((binderTy x, binderTy y,

606614 False,

src/Idris/DeepSeq.hs+7−7

@@ -153,17 +153,20 @@ instance (NFData t) => NFData (PDecl' t) where

153153 = rnf x1 `seq`

154154 rnf x2 `seq`

155155 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)

157157 = rnf x1 `seq`

158158 rnf x2 `seq`

159159 rnf x3 `seq`

160− rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

160+ rnf x4 `seq`

161+ rnf x5 `seq`

162+ rnf x6 `seq`

163+ rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()

161164 rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

162165 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

163166 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

164167 rnf (PDirective x1) = ()

165− rnf (PProvider x1 x2 x3 x4)

166− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

168+ rnf (PProvider x1 x2 x3 x4 x5)

169+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

167170 rnf (PTransform x1 x2 x3 x4)

168171 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

169172

@@ -357,6 +360,3 @@ instance NFData SyntaxInfo where

357360 rnf x4 `seq`

358361 rnf x5 `seq`

359362 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 []

194194pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

195195pprintTerm' ist bnd tm = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) tm

196196

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+

197202pprintErr :: IState -> Err -> Doc OutputAnnotation

198203pprintErr i err = pprintErr' i (fmap (errReverse i) err)

199204

@@ -203,20 +208,28 @@ pprintErr' i (InternalMsg s) =

203208 text "This is probably a bug, or a missing error message.",

204209 text ("Please consider reporting at " ++ bugaddr)

205210 ]

206−pprintErr' i (CantUnify _ x_in y_in e sc s) =

211+pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =

207212 let (x_ns, y_ns, nms) = renameMNs x_in y_in

208213 (x, y) = addImplicitDiffs (delab i x_ns) (delab i y_ns) in

209214 text "Can't unify" <> indented (annTm x_ns

210215 (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+ <$>

212221 text "with" <> indented (annTm y_ns

213222 (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+ <>

215228 case e of

216229 Msg "" -> empty

217230 -- if the specific error is the same as the one we just printed,

218231 -- 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

220233 _ -> line <> line <> text "Specifically:" <>

221234 indented (pprintErr' i e) <>

222235 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)

3232 | ClassDoc Name d -- class docs

3333 [FunDoc' d] -- method docs

3434 [(Name, Maybe d)] -- parameters and their docstrings

35− [PTerm] -- instances

35+ [(PTerm, (d, [(Name, d)]))] -- instances

36+ [PTerm] -- subclasses

3637 [PTerm] -- superclasses

3738 | ModDoc [String] -- Module name

3839 d

@@ -88,7 +89,7 @@ pprintDocs ist (DataDoc t args)

8889 if null args then text "No constructors."

8990 else nest 4 (text "Constructors:" <> line <>

9091 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)

9293 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>

9394 if nullDocstring doc

9495 then empty

@@ -100,8 +101,8 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

100101 vsep (map (pprintFD ist) meths))

101102 <$>

102103 nest 4 (text "Instances:" <$>

103− vsep (if null instances' then [text "<no instances>"]

104− else map dumpInstance instances'))

104+ vsep (if null instances then [text "<no instances>"]

105+ else map pprintInstance instances))

105106 <>

106107 (if null subclasses then empty

107108 else line <$> nest 4 (text "Subclasses:" <$>

@@ -118,6 +119,30 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

118119 ppo = ppOptionIst ist

119120 infixes = idris_infixes ist

120121

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+

121146 dumpInstance :: PTerm -> Doc OutputAnnotation

122147 dumpInstance = pprintPTerm ppo params' [] infixes

123148

@@ -140,11 +165,10 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

140165 isSubclass (PPi _ _ _ pt) = isSubclass pt

141166 isSubclass _ = False

142167

143− (subclasses, instances') = partition isSubclass instances

144−

145− prettyParameters = if any (isJust . snd) params

146− 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))

168+ prettyParameters =

169+ if any (isJust . snd) params

170+ then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)

171+ else hsep (punctuate comma (map (prettyName True False params' . fst) params))

148172

149173pprintDocs ist (ModDoc mod docs)

150174 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>

@@ -186,14 +210,28 @@ docClass n ci

186210 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

187211 docstr = maybe emptyDocstring fst docStrings

188212 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd))) (class_params ci)

189− instances = map (delabTy i) (class_instances ci)

213+ instanceDocs = map (fromMaybe (emptyDocstring, []) .

214+ listToMaybe .

215+ flip lookupCtxt (idris_docstrings i))

216+ (class_instances ci)

217+ instances = zip (map (delabTy i) (class_instances ci)) instanceDocs

218+ (subclasses, instances') = partition (isSubclass . fst) instances

190219 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

191220 mdocs <- mapM (docFun . fst) (class_methods ci)

192− return $ ClassDoc n docstr mdocs params instances superclasses

221+ return $ ClassDoc

222+ n docstr mdocs params

223+ instances' (map fst subclasses) superclasses

193224 where

194− getDInst (PInstance _ _ _ _ _ t _ _) = Just t

225+ getDInst (PInstance _ _ _ _ _ _ _ t _ _) = Just t

195226 getDInst _ = Nothing

196227

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+

197235docFun :: Name -> Idris FunDoc

198236docFun n

199237 = 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

109109 mdec x = x

110110

111111 -- TODO: probably should normalise

112− checkDefaultSuperclassInstance :: PDecl -> Idris ()

113− checkDefaultSuperclassInstance (PInstance _ fc cs n ps _ _ _)

112+ checkDefaultSuperclassInstance :: PDecl -> Idris ()

113+ checkDefaultSuperclassInstance (PInstance _ _ _ fc cs n ps _ _ _)

114114 = do when (not $ null cs) . tclift

115115 $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))

116116 i <- getIState

@@ -120,11 +120,11 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

120120 $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))

121121 return ()

122122

123− impbind :: [(Name, PTerm)] -> PTerm -> PTerm

123+ impbind :: [(Name, PTerm)] -> PTerm -> PTerm

124124 impbind [] x = x

125125 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)

126126

127− conbind :: [(Name, PTerm)] -> PTerm -> PTerm

127+ conbind :: [(Name, PTerm)] -> PTerm -> PTerm

128128 conbind ((c, ty) : ns) x = PPi constraint c ty (conbind ns x)

129129 conbind [] x = x

130130

@@ -133,7 +133,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

133133 = do t' <- implicit' info syn allmeths n t

134134 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

135135 return ( (n, (toExp (map fst ps) Exp t')),

136− (n, (doc, o, (toExp (map fst ps)

136+ (n, (doc, o, (toExp (map fst ps)

137137 (\ l s p -> Imp l s p Nothing) t'))),

138138 (n, (syn, o, t) ) )

139139 tdecl _ _ = ifail "Not allowed in a class declaration"

@@ -155,7 +155,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

155155

156156 tydecl (PTy _ _ _ _ _ _ _) = True

157157 tydecl _ = False

158− instdecl (PInstance _ _ _ _ _ _ _ _) = True

158+ instdecl (PInstance _ _ _ _ _ _ _ _ _ _) = True

159159 instdecl _ = False

160160 clause (PClauses _ _ _ _) = True

161161 clause _ = False

@@ -221,7 +221,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

221221

222222 insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)

223223 = PPi p n ty (insertConstraint c sc)

224− insertConstraint c sc = PPi (constraint { pstatic = Static })

224+ insertConstraint c sc = PPi (constraint { pstatic = Static })

225225 (sMN 0 "class") c sc

226226

227227 -- make arguments explicit and don't bind class parameters

@@ -230,5 +230,3 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

230230 | otherwise = PPi (e l s p) n ty (toExp ns e sc)

231231 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

232232 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

464464 Error err -> if tcgen then return (recoverable ctxt err)

465465 else return (validCase ctxt err ||

466466 recoverable ctxt err)

467− where validCase ctxt (CantUnify _ topx topy e _ _)

467+ where validCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)

468468 = let topx' = normalise ctxt [] topx

469469 topy' = normalise ctxt [] topy in

470470 not (sameFam topx' topy' || not (validCase ctxt e))

@@ -474,7 +474,7 @@ checkPossible info fc tcgen fname lhs_in

474474 validCase ctxt (ElaboratingArg _ _ _ e) = validCase ctxt e

475475 validCase ctxt _ = True

476476

477− recoverable ctxt (CantUnify r topx topy e _ _)

477+ recoverable ctxt (CantUnify r (topx, _) (topy, _) e _ _)

478478 = let topx' = normalise ctxt [] topx

479479 topy' = normalise ctxt [] topy in

480480 checkRec topx' topy'

@@ -704,7 +704,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

704704 OK (_, cs) -> do addConstraints fc cs

705705 logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs

706706 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))

708708 i <- getIState

709709 checkInferred fc (delab' i crhs True True) rhs

710710 -- 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)

5151import Util.Pretty(pretty, text)

5252

5353elabInstance :: ElabInfo -> SyntaxInfo ->

54+ Docstring (Either Err PTerm) ->

55+ [(Name, Docstring (Either Err PTerm))] ->

5456 ElabWhat -> -- phase

5557 FC -> [(Name, PTerm)] -> -- constraints

5658 Name -> -- the class

@@ -58,7 +60,7 @@ elabInstance :: ElabInfo -> SyntaxInfo ->

5860 PTerm -> -- full instance type

5961 Maybe Name -> -- explicit name

6062 [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

6264 i <- getIState

6365 (n, ci) <- case lookupCtxtName n (idris_classes i) of

6466 [c] -> return c

@@ -69,7 +71,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

6971 let iname = mkiname n (namespace info) ps expn

7072 let emptyclass = null (class_methods ci)

7173 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

7375 -- if the instance type matches any of the instances we have already,

7476 -- and it's not a named instance, then it's overlapping, so report an error

7577 case expn of

@@ -147,10 +149,10 @@ elabInstance info syn what fc cs n ps t expn ds = do

147149 Just m -> sNS (SN (sInstanceN n' (map show ps'))) m

148150 Just nm -> nm

149151

150− substInstance ips pnames (PInstance syn _ cs n ps t expn ds)

151− = PInstance syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

152+ substInstance ips pnames (PInstance doc argDocs syn _ cs n ps t expn ds)

153+ = PInstance doc argDocs syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

152154

153− isOverlapping i (PInstance syn _ _ n ps t expn _)

155+ isOverlapping i (PInstance doc argDocs syn _ _ n ps t expn _)

154156 = case lookupCtxtName n (idris_classes i) of

155157 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in

156158 case lookupTy iname (tt_ctxt i) of

src/Idris/Elab/Provider.hs+4−5

@@ -52,8 +52,8 @@ import Data.List.Split (splitOn)

5252import Util.Pretty(pretty, text)

5353

5454-- | Elaborate a type provider

55−elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()

56−elabProvider info syn fc what n

55+elabProvider :: Docstring (Either Err PTerm) -> ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()

56+elabProvider doc info syn fc what n

5757 = do i <- getIState

5858 -- Ensure that the experimental extension is enabled

5959 unless (TypeProviders `elem` idris_language_extensions i) $

@@ -93,12 +93,12 @@ elabProvider info syn fc what n

9393 Provide tm

9494 | ProvTerm ty _ <- what ->

9595 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

9797 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

9898 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

9999 | ProvPostulate _ <- what ->

100100 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)

102102 logLvl 3 $ "Elaborated provided postulate " ++ show n

103103 | otherwise ->

104104 ierror . Msg $ "Attempted to provide a postulate where a term was expected."

@@ -120,4 +120,3 @@ elabProvider info syn fc what n

120120 case converts ctxt [] (providerOf tp) prov of

121121 OK _ -> True

122122 _ -> False

123−

src/Idris/Elab/Transform.hs+2−2

@@ -81,12 +81,12 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

8181 -- Types must always convert

8282 case converts ctxt [] clhs_ty crhs_ty of

8383 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))

8585 -- In safe mode, values must convert (Thinks: This is probably not

8686 -- useful as is, perhaps it should require a proof of equality instead)

8787 when safe $ case converts ctxt [] clhs_tm crhs_tm of

8888 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))

9090

9191 case unApply (depat clhs_tm) of

9292 (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

9090 let (inaccData, impls) = unzip $ getUnboundImplicits i cty ty

9191 let inacc = inaccessibleImps 0 cty inaccData

9292 logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc ++

93− " from " ++ show (cty, ty)

93+ " from " ++ show cty ++ "\n" ++ showTmImpls ty

9494

9595 putIState $ i { idris_implicits = addDef n impls (idris_implicits i) }

9696 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

181181 addIBC (IBCErrorHandler n)

182182 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"

183183 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 ()

184190 return usety

185191 where

186192 -- 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

191197 | otherwise = mergeTy sc sc'

192198 mergeTy _ sc = sc

193199

200+ ffiexport = sNS (sUN "FFI_Export") ["FFI_Export"]

201+

194202 err = txt "Err"

195203 maybe = txt "Maybe"

196204 lst = txt "List"

src/Idris/ElabDecls.hs+6−7

@@ -200,11 +200,11 @@ elabDecl' what info (PMutual f ps)

200200 where isDataDecl (PData _ _ _ _ _ _) = True

201201 isDataDecl _ = False

202202

203− setMutData ns n

203+ setMutData ns n

204204 = do i <- getIState

205205 case lookupCtxt n (idris_datatypes i) of

206206 [x] -> do let x' = x { mutual_types = ns }

207− putIState $ i { idris_datatypes

207+ putIState $ i { idris_datatypes

208208 = addDef n x' (idris_datatypes i) }

209209 _ -> return ()

210210

@@ -233,9 +233,9 @@ elabDecl' what info (PClass doc s f cs n ps pdocs ds)

233233 | what /= EDefns

234234 = do iLOG $ "Elaborating class " ++ show n

235235 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)

237237 = 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

239239elabDecl' what info (PRecord doc s f tyn ty opts cdoc cn cty)

240240 | what /= ETypes

241241 = do iLOG $ "Elaborating record " ++ show tyn

@@ -249,12 +249,11 @@ elabDecl' _ info (PDSL n dsl)

249249 addIBC (IBCDSL n)

250250elabDecl' what info (PDirective i)

251251 | what /= EDefns = i

252−elabDecl' what info (PProvider syn fc provWhat n)

252+elabDecl' what info (PProvider doc syn fc provWhat n)

253253 | what /= EDefns

254254 = do iLOG $ "Elaborating type provider " ++ show n

255− elabProvider info syn fc provWhat n

255+ elabProvider doc info syn fc provWhat n

256256elabDecl' what info (PTransform fc safety old new)

257257 = do elabTransform info fc safety old new

258258 return ()

259259elabDecl' _ _ _ = return () -- skipped this time

260−

src/Idris/ElabTerm.hs+3−3

@@ -268,10 +268,10 @@ elab ist info emode opts fn tm

268268 pimp (sUN "a") Placeholder True,

269269 pexp ct])) True

270270

271− forceErr env (CantUnify _ t t' _ _ _)

271+ forceErr env (CantUnify _ (t,_) (t',_) _ _ _)

272272 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

273273 ht == txt "Lazy'" = True

274− forceErr env (CantUnify _ t t' _ _ _)

274+ forceErr env (CantUnify _ (t,_) (t',_) _ _ _)

275275 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),

276276 ht == txt "Lazy'" = True

277277 forceErr env (InfiniteUnify _ t _)

@@ -2553,7 +2553,7 @@ reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT")

25532553reflectErr :: Err -> Raw

25542554reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]

25552555reflectErr (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) =

25572557 raw_apply (Var $ reflErrName "CantUnify")

25582558 [ rawBool b

25592559 , reflect t1

src/Idris/Erasure.hs+19−15

@@ -65,12 +65,12 @@ type Vars = Map Name VarInfo

6565

6666-- Perform usage analysis, write the relevant information in the internal

6767-- structures, returning the list of reachable names.

68−performUsageAnalysis :: Idris [Name]

69−performUsageAnalysis = do

68+performUsageAnalysis :: [Name] -> Idris [Name]

69+performUsageAnalysis roots = do

7070 ctx <- tt_ctxt <$> getIState

71− mainName <- getMainName <$> getIState

71+ startNames <- getStartNames <$> getIState

7272

73− case mainName of

73+ case startNames of

7474 Left reason -> return [] -- no main -> not compiling -> reachability irrelevant

7575 Right main -> do

7676 ci <- idris_classes <$> getIState

@@ -106,11 +106,14 @@ performUsageAnalysis = do

106106

107107 return $ S.toList reachableNames

108108 where

109− getMainName :: IState -> Either Err Name

110− getMainName ist = case lookupCtxtName n (idris_implicits ist) of

111− [(n', _)] -> Right n'

112− [] -> Left (NoSuchVariable n)

113− more -> Left (CantResolveAlts (map fst more))

109+ getStartNames :: IState -> Either Err [Name]

110+ getStartNames ist

111+ = case lookupCtxtName n (idris_implicits ist) of

112+ [(n', _)] -> Right (n' : roots)

113+ [] -> if null roots

114+ then Left (NoSuchVariable n)

115+ else Right roots

116+ more -> Left (CantResolveAlts (map fst more))

114117 where

115118 n = sNS (sUN "main") ["Main"]

116119

@@ -171,9 +174,9 @@ forwardChain deps

171174

172175-- Build the dependency graph,

173176-- starting the depth-first search from a list of Names.

174−buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> Context -> Name -> Deps

175−buildDepMap ci used ctx mainName = addPostulates used $

176− dfs S.empty M.empty [mainName]

177+buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> Context -> [Name] -> Deps

178+buildDepMap ci used ctx startNames = addPostulates used $

179+ dfs S.empty M.empty startNames

177180 where

178181 -- mark the result of Main.main as used with the empty assumption

179182 addPostulates :: [(Name, Int)] -> Deps -> Deps

@@ -191,10 +194,11 @@ buildDepMap ci used ctx mainName = addPostulates used $

191194

192195 postulates used =

193196 [ [] ==> concat

194− -- These two, Main.main and run__IO, are always evaluated

197+ -- Main.main ( + export lists) and run__IO, are always evaluated

195198 -- but they elude analysis since they come from the seed term.

196− [ [(mainName, Result)]

197− , [(sUN "run__IO", Result), (sUN "run__IO", Arg 1)]

199+ [(map (\n -> (n, Result)) startNames)

200+ ,[(sUN "run__IO", Result), (sUN "run__IO", Arg 1)]

201+ ,[(sUN "call__IO", Result), (sUN "call__IO", Arg 2)]

198202

199203 -- Explicit usage declarations from a %used pragma

200204 , map (\(n, i) -> (n, Arg i)) used

src/Idris/IBC.hs+53−37

@@ -80,7 +80,8 @@ data IBCFile = IBCFile { ver :: Word8,

8080 ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))],

8181 ibc_postulates :: ![Name],

8282 ibc_parsedSpan :: !(Maybe FC),

83− ibc_usage :: ![(Name, Int)]

83+ ibc_usage :: ![(Name, Int)],

84+ ibc_exports :: ![Name]

8485 }

8586 deriving Show

8687{-!

@@ -88,11 +89,11 @@ deriving instance Binary IBCFile

8889!-}

8990

9091initIBC :: IBCFile

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

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

9293

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

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

9495 -> FilePath -> Idris ()

95−loadIBC reexport fp

96+loadIBC reexport fp

9697 = do imps <- getImported

9798 let redo = case lookup fp imps of

9899 Nothing -> True

@@ -193,7 +194,7 @@ ibc i (IBCLib tgt n) f = return f { ibc_libs = (tgt, n) : ibc_libs f }

193194ibc i (IBCCGFlag tgt n) f = return f { ibc_cgflags = (tgt, n) : ibc_cgflags f }

194195ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }

195196ibc 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

197198 = do f' <- case lookupDefExact n (tt_ctxt i) of

198199 Just v -> return f { ibc_defs = (n,v) : ibc_defs f }

199200 _ -> ifail "IBC write failed"

@@ -233,17 +234,18 @@ ibc i (IBCModDocs n) f = case lookupCtxtExact n (idris_moduledocs i) of

233234 Just v -> return f { ibc_moduledocs = (n,v) : ibc_moduledocs f }

234235 _ -> ifail "IBC write failed"

235236ibc 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 }

236238

237239process :: Bool -- ^ Reexporting

238240 -> IBCFile -> FilePath -> Idris ()

239241process reexp i fn

240− | ver i /= ibcVersion

242+ | ver i /= ibcVersion

241243 = do iLOG "ibc out of date"

242244 let e = if ver i < ibcVersion then " an earlier " else " a later "

243245 ifail $ "Incompatible ibc version.\nThis library was built with"

244246 ++ e ++ "version of Idris.\n" ++

245247 "Please clean and rebuild."

246−

248+

247249 --- please rebuild"

248250 | otherwise =

249251 do srcok <- runIO $ doesFileExist (sourcefile i)

@@ -290,6 +292,7 @@ process reexp i fn

290292 pPostulates $ force (ibc_postulates i)

291293 pParsedSpan $ force (ibc_parsedSpan i)

292294 pUsage $ force (ibc_usage i)

295+ pExports $ force (ibc_exports i)

293296

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

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

@@ -311,12 +314,16 @@ pUsage :: [(Name, Int)] -> Idris ()

311314pUsage ns = do ist <- getIState

312315 putIState ist { idris_erasureUsed = ns ++ idris_erasureUsed ist }

313316

317+pExports :: [Name] -> Idris ()

318+pExports ns = do ist <- getIState

319+ putIState ist { idris_exports = ns ++ idris_exports ist }

320+

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

315322pImportDirs fs = mapM_ addImportDir fs

316323

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

318325pImports fs

319− = do mapM_ (\(re, f) ->

326+ = do mapM_ (\(re, f) ->

320327 do i <- getIState

321328 ibcsd <- valIBCSubDir i

322329 ids <- allImportDirs

@@ -420,20 +427,20 @@ pHdrs :: [(Codegen, String)] -> Idris ()

420427pHdrs hs = mapM_ (uncurry addHdr) hs

421428

422429pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()

423−pPatdefs ds

424− = mapM_ (\ (n, d) ->

430+pPatdefs ds

431+ = mapM_ (\ (n, d) ->

425432 do i <- getIState

426433 putIState (i { idris_patdefs = addDef n (force d) (idris_patdefs i) }))

427434 ds

428435

429436pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()

430−pDefs reexp syms ds

437+pDefs reexp syms ds

431438 = mapM_ (\ (n, d) ->

432439 do d' <- updateDef d

433440 case d' of

434− TyDecl _ _ -> return ()

441+ TyDecl _ _ -> return ()

435442 _ -> do iLOG $ "SOLVING " ++ show n

436− solveDeferred n

443+ solveDeferred n

437444 i <- getIState

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

439446 putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })

@@ -502,8 +509,8 @@ pMDocs ds = mapM_ addMDocStr ds

502509

503510pAccess :: Bool -- ^ Reexporting?

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

505−pAccess reexp ds

506− = mapM_ (\ (n, a_in) ->

512+pAccess reexp ds

513+ = mapM_ (\ (n, a_in) ->

507514 do let a = if reexp then a_in else Hidden

508515 logLvl 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a

509516 i <- getIState

@@ -561,7 +568,7 @@ pFunctionErrorHandlers ((fn, arg, handler):ns) = do addFunctionErrorHandlers fn

561568

562569pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()

563570pMetavars ns = do i <- getIState

564− putIState $ i { idris_metavars = Data.List.reverse ns

571+ putIState $ i { idris_metavars = Data.List.reverse ns

565572 ++ idris_metavars i }

566573

567574----- For Cheapskate and docstrings

@@ -855,7 +862,7 @@ safeToEnum :: (Enum a, Bounded a, Integral int) => String -> int -> a

855862safeToEnum label x' = result

856863 where

857864 x = fromIntegral x'

858− result

865+ result

859866 | x < fromEnum (minBound `asTypeOf` result)

860867 || x > fromEnum (maxBound `asTypeOf` result)

861868 = error $ label ++ ": corrupted binary representation in IBC"

@@ -927,7 +934,7 @@ instance Binary MetaInformation where

927934 _ -> error "Corrupted binary data for MetaInformation"

928935

929936instance 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)

931938 = {-# SCC "putIBCFile" #-}

932939 do put x1

933940 put x2

@@ -971,6 +978,7 @@ instance Binary IBCFile where

971978 put x40

972979 put x41

973980 put x42

981+ put x43

974982

975983 get

976984 = do x1 <- get

@@ -1016,7 +1024,8 @@ instance Binary IBCFile where

10161024 x40 <- get

10171025 x41 <- get

10181026 x42 <- 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)

1027+ x43 <- get

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)

10201029 else return (initIBC { ver = x1 })

10211030

10221031instance Binary DataOpt where

@@ -1239,15 +1248,18 @@ instance (Binary t) => Binary (PDecl' t) where

12391248 put x6

12401249 put x7

12411250 put x8

1242− PInstance x1 x2 x3 x4 x5 x6 x7 x8 -> do putWord8 8

1243− put x1

1244− put x2

1245− put x3

1246− put x4

1247− put x5

1248− put x6

1249− put x7

1250− put x8

1251+ PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

1252+ do putWord8 8

1253+ put x1

1254+ put x2

1255+ put x3

1256+ put x4

1257+ put x5

1258+ put x6

1259+ put x7

1260+ put x8

1261+ put x9

1262+ put x10

12511263 PDSL x1 x2 -> do putWord8 9

12521264 put x1

12531265 put x2

@@ -1270,16 +1282,18 @@ instance (Binary t) => Binary (PDecl' t) where

12701282 put x1

12711283 put x2

12721284 PDirective x1 -> error "Cannot serialize PDirective"

1273− PProvider x1 x2 x3 x4 -> do putWord8 15

1274− put x1

1275− put x2

1276− put x3

1277− put x4

1285+ PProvider x1 x2 x3 x4 x5 ->

1286+ do putWord8 15

1287+ put x1

1288+ put x2

1289+ put x3

1290+ put x4

1291+ put x5

12781292 PTransform x1 x2 x3 x4 -> do putWord8 16

12791293 put x1

12801294 put x2

12811295 put x3

1282− put x4

1296+ put x4

12831297 get

12841298 = do i <- getWord8

12851299 case i of

@@ -1341,7 +1355,9 @@ instance (Binary t) => Binary (PDecl' t) where

13411355 x6 <- get

13421356 x7 <- get

13431357 x8 <- get

1344− return (PInstance x1 x2 x3 x4 x5 x6 x7 x8)

1358+ x9 <- get

1359+ x10 <- get

1360+ return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

13451361 9 -> do x1 <- get

13461362 x2 <- get

13471363 return (PDSL x1 x2)

@@ -1367,7 +1383,8 @@ instance (Binary t) => Binary (PDecl' t) where

13671383 x2 <- get

13681384 x3 <- get

13691385 x4 <- get

1370− return (PProvider x1 x2 x3 x4)

1386+ x5 <- get

1387+ return (PProvider x1 x2 x3 x4 x5)

13711388 16 -> do x1 <- get

13721389 x2 <- get

13731390 x3 <- get

@@ -2189,4 +2206,3 @@ instance Binary Codegen where

21892206 return (Via x1)

21902207 1 -> return Bytecode

21912208 _ -> error "Corrupted binary data for Codegen"

2192−

src/Idris/IdrisDoc.hs+5−5

@@ -168,7 +168,7 @@ removeOrphans list =

168168 in filter ((`S.notMember` children) . (\(n, _, _) -> n)) list

169169

170170 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

172172 names _ = []

173173

174174-- | Whether a Name names something which should be documented

@@ -219,7 +219,7 @@ referredNss (n, Just d, _) =

219219

220220 where getFunDocs (FunDoc f) = [f]

221221 getFunDocs (DataDoc f fs) = f:fs

222− getFunDocs (ClassDoc _ _ fs _ _ _) = fs

222+ getFunDocs (ClassDoc _ _ fs _ _ _ _) = fs

223223 types (FD _ _ args t _) = t:(map second args)

224224 second (_, x, _, _) = x

225225

@@ -417,7 +417,7 @@ createIndex nss out =

417417 BS2.hPut h $ renderHtml $ wrapper Nothing $ do

418418 H.h1 $ "Namespaces"

419419 H.ul ! class_ "names" $ do

420− let path ns = "docs" </> genRelNsPath ns "html"

420+ let path ns = "docs" </> genRelNsPath ns "html"

421421 item ns = do let n = toHtml $ nsName2Str ns

422422 link = toValue $ path ns

423423 H.li $ H.a ! href link ! class_ "code" $ n

@@ -439,7 +439,7 @@ createNsDoc :: IState -- ^ Needed to determine the types of names

439439createNsDoc ist ns content out =

440440 do let tpath = out </> "docs" </> (genRelNsPath ns "html")

441441 dir = takeDirectory tpath

442− file = takeFileName tpath

442+ file = takeFileName tpath

443443 haveDocs (_, Just d, _) = [d]

444444 haveDocs _ = []

445445 -- We cannot do anything without a Doc

@@ -575,7 +575,7 @@ createOtherDoc :: IState -- ^ Needed to determine the types of names

575575 -> H.Html -- ^ Resulting HTML

576576createOtherDoc ist (FunDoc fd) = createFunDoc ist fd

577577

578−createOtherDoc ist (ClassDoc n docstring fds _ _ _) = do

578+createOtherDoc ist (ClassDoc n docstring fds _ _ _ _) = do

579579 H.dt ! (A.id $ toValue $ show n) $ do

580580 H.span ! class_ "word" $ do "class"; nbsp

581581 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

587587collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

588588collect (PClass doc f s cs n ps pdocs ds : ds')

589589 = PClass doc f s cs n ps pdocs (collect ds) : collect ds'

590−collect (PInstance f s cs n ps t en ds : ds')

591− = PInstance f s cs n ps t en (collect ds) : collect ds'

590+collect (PInstance doc argDocs f s cs n ps t en ds : ds')

591+ = PInstance doc argDocs f s cs n ps t en (collect ds) : collect ds'

592592collect (d : ds) = d : collect ds

593593collect [] = []

src/Idris/Parser.hs+56−44

@@ -9,7 +9,7 @@ module Idris.Parser(module Idris.Parser,

99import Prelude hiding (pi)

1010

1111import 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)

1313import Text.Parser.LookAhead

1414import Text.Parser.Expression

1515import qualified Text.Parser.Token as Tok

@@ -87,7 +87,7 @@ import System.IO

8787{- | Parses module definition

8888

8989@

90− ModuleHeader ::= 'module' Identifier_t ';'?;

90+ ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;

9191@

9292-}

9393moduleHeader :: IdrisParser (Maybe (Docstring ()), [String])

@@ -291,7 +291,7 @@ syntaxRule syn

291291

292292 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :

293293 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

295295 mkSimple' (Expr e : Symbol s : es)

296296 | takeWhile (`elem` opChars) ts /= "" && ts `notElem` invalidOperators = SimpleExpr e : Symbol s : mkSimple' es

297297 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s

@@ -348,13 +348,9 @@ fnDecl' :: SyntaxInfo -> IdrisParser PDecl

348348fnDecl' syn = checkFixity $

349349 do (doc, argDocs, fc, opts', n, acc) <- try (do

350350 pushIndent

351− (doc, argDocs) <- option noDocs docComment

351+ (doc, argDocs) <- docstring syn

352352 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

358354 then [TotalFn]

359355 else []

360356 opts <- fnOpts initOpts

@@ -364,7 +360,7 @@ fnDecl' syn = checkFixity $

364360 let n = expandNS syn n_in

365361 fc <- getFC

366362 lchar ':'

367− return (doc', argDocs', fc, opts', n, acc))

363+ return (doc, argDocs, fc, opts', n, acc))

368364 ty <- typeExpr (allowImp syn)

369365 terminator

370366 addAcc n acc

@@ -459,12 +455,10 @@ Postulate ::=

459455@

460456-}

461457postulate :: SyntaxInfo -> IdrisParser PDecl

462−postulate syn = do doc <- try $ do (doc, _) <- option noDocs docComment

463− ist <- get

464− let doc' = annotCode (tryFullExpr syn ist) doc

458+postulate syn = do doc <- try $ do (doc, _) <- docstring syn

465459 pushIndent

466460 reserved "postulate"

467− return doc'

461+ return doc

468462 ist <- get

469463 let initOpts = if default_total ist

470464 then [TotalFn]

@@ -587,7 +581,7 @@ ClassBlock ::=

587581classBlock :: SyntaxInfo -> IdrisParser [PDecl]

588582classBlock syn = do reserved "where"

589583 openBlock

590− ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)

584+ ds <- many (notEndBlock >> instance_ syn <|> fnDecl syn)

591585 closeBlock

592586 return (concat ds)

593587 <?> "class block"

@@ -608,15 +602,14 @@ Class ::=

608602@

609603-}

610604class_ :: SyntaxInfo -> IdrisParser [PDecl]

611−class_ syn = do (doc, argDocs, acc) <- try (do

612− (doc, argDocs) <- option noDocs docComment

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

618− return (doc', argDocs', acc))

619− reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName

605+class_ syn = do (doc, argDocs, acc)

606+ <- try (do (doc, argDocs) <- docstring syn

607+ acc <- optional accessibility

608+ reserved "class"

609+ return (doc, argDocs, acc))

610+ fc <- getFC

611+ cons <- constraintList syn

612+ n_in <- fnName

620613 let n = expandNS syn n_in

621614 cs <- many carg

622615 ds <- option [] (classBlock syn)

@@ -634,7 +627,7 @@ class_ syn = do (doc, argDocs, acc) <- try (do

634627

635628@

636629 Instance ::=

637− 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?

630+ DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?

638631 ;

639632@

640633

@@ -643,7 +636,9 @@ InstanceName ::= '[' Name ']';

643636@

644637-}

645638instance_ :: SyntaxInfo -> IdrisParser [PDecl]

646−instance_ syn = do reserved "instance"; fc <- getFC

639+instance_ syn = do (doc, argDocs)

640+ <- try (docstring syn <* reserved "instance")

641+ fc <- getFC

647642 en <- optional instanceName

648643 cs <- constraintList syn

649644 cn <- fnName

@@ -651,7 +646,7 @@ instance_ syn = do reserved "instance"; fc <- getFC

651646 let sc = PApp fc (PRef fc cn) (map pexp args)

652647 let t = bindList (PPi constraint) cs sc

653648 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]

655650 <?> "instance declaration"

656651 where instanceName :: IdrisParser Name

657652 instanceName = do lchar '['; n_in <- fnName; lchar ']'

@@ -660,6 +655,18 @@ instance_ syn = do reserved "instance"; fc <- getFC

660655 <?> "instance name"

661656

662657

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+

663670{- | Parses a using declaration list

664671

665672@

@@ -1101,25 +1108,30 @@ totality

11011108{- | Parses a type provider

11021109

11031110@

1104−Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;

1111+Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;

11051112ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'

11061113@

11071114 -}

11081115provider :: SyntaxInfo -> IdrisParser [PDecl]

1109−provider syn = do try (lchar '%' *> reserved "provide");

1110− provideTerm <|> providePostulate

1116+provider syn = do doc <- try (do (doc, _) <- docstring syn

1117+ lchar '%'

1118+ reserved "provide"

1119+ return doc)

1120+ provideTerm doc <|> providePostulate doc

11111121 <?> "type provider"

1112− where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1113− fc <- getFC

1114− reserved "with"

1115− e <- expr syn <?> "provider expression"

1116− return [PProvider syn fc (ProvTerm t e) n]

1117− providePostulate = do reserved "postulate"

1118− n <- fnName

1119− fc <- getFC

1120− reserved "with"

1121− e <- expr syn <?> "provider expression"

1122− return [PProvider syn fc (ProvPostulate e) n]

1122+ where provideTerm doc =

1123+ do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1124+ fc <- getFC

1125+ reserved "with"

1126+ e <- expr syn <?> "provider expression"

1127+ return [PProvider doc syn fc (ProvTerm t e) n]

1128+ providePostulate doc =

1129+ do reserved "postulate"

1130+ n <- fnName

1131+ fc <- getFC

1132+ reserved "with"

1133+ e <- expr syn <?> "provider expression"

1134+ return [PProvider doc syn fc (ProvPostulate e) n]

11231135

11241136{- | Parses a transform

11251137

@@ -1403,9 +1415,9 @@ loadSource lidr f toline

14031415 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)

14041416 toMutual x = let r = PMutual (fileFC "single mutual") [x] in

14051417 case x of

1406− PClauses _ _ _ _ -> r

1407− PClass _ _ _ _ _ _ _ _ -> r

1408− PInstance _ _ _ _ _ _ _ _ -> r

1418+ PClauses{} -> r

1419+ PClass{} -> r

1420+ PInstance{} -> r

14091421 _ -> x

14101422

14111423 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()

src/Idris/Prover.hs+1−1

@@ -83,7 +83,7 @@ prove opt ctxt lit n ty

8383 "Expected type:" ++ show ty)

8484 case converts ctxt [] ty pty of

8585 OK _ -> return ()

86− Error e -> ierror (CantUnify False ty pty e [] 0)

86+ Error e -> ierror (CantUnify False (ty, Nothing) (pty, Nothing) e [] 0)

8787 ptm' <- applyOpts ptm

8888 ei <- getErasureInfo `fmap` getIState

8989 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

5454

5555import IRTS.Compiler

5656import IRTS.CodegenCommon

57+import IRTS.Exports

5758import IRTS.System

5859

5960import Control.Category

@@ -810,8 +811,8 @@ process fn (NewDefn decls) = do

810811 fixClauses :: PDecl' t -> PDecl' t

811812 fixClauses (PClauses fc opts _ css@(clause:cs)) =

812813 PClauses fc opts (getClauseName clause) css

813− fixClauses (PInstance syn fc constraints cls parms ty instName decls) =

814− PInstance syn fc constraints cls parms ty instName (map fixClauses decls)

814+ fixClauses (PInstance doc argDocs syn fc constraints cls parms ty instName decls) =

815+ PInstance doc argDocs syn fc constraints cls parms ty instName (map fixClauses decls)

815816 fixClauses decl = decl

816817

817818process fn (Undefine names) = undefine names

@@ -968,7 +969,7 @@ process fn (DebugUnify l r)

968969 = do (ltm, _) <- elabVal recinfo ERHS l

969970 (rtm, _) <- elabVal recinfo ERHS r

970971 ctxt <- getContext

971− case unify ctxt [] ltm rtm [] [] [] [] of

972+ case unify ctxt [] (ltm, Nothing) (rtm, Nothing) [] [] [] [] of

972973 OK ans -> iputStrLn (show ans)

973974 Error e -> iputStrLn (show e)

974975

@@ -1110,7 +1111,7 @@ process fn Execute

11101111 t <- codegen

11111112 -- gcc adds .exe when it builds windows programs

11121113 progName <- return $ if isWindows then tmpn ++ ".exe" else tmpn

1113− ir <- compile t tmpn m

1114+ ir <- compile t tmpn (Just m)

11141115 runIO $ generate t (fst (head (idris_imported ist))) ir

11151116 case idris_outputmode ist of

11161117 RawOutput h -> do runIO $ rawSystem progName []

@@ -1122,9 +1123,13 @@ process fn Execute

11221123process fn (Compile codegen f)

11231124 | map toLower (takeExtension f) `elem` [".idr", ".lidr", ".idc"] =

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

1125− | otherwise = do (m, _) <- elabVal recinfo ERHS

1126− (PApp fc (PRef fc (sUN "run__IO"))

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

1126+ | otherwise = do opts <- getCmdLine

1127+ let iface = Interface `elem` opts

1128+ m <- if iface then return Nothing else

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

1130+ (PApp fc (PRef fc (sUN "run__IO"))

1131+ [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

1132+ return (Just m')

11281133 ir <- compile codegen f m

11291134 i <- getIState

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

@@ -1418,9 +1423,10 @@ loadInputs inputs toline -- furthest line to read in input source files

14181423 ist <- getIState

14191424 putIState (ist { idris_tyinfodata = tidata,

14201425 idris_patdefs = patdefs })

1426+ exports <- findExports

14211427

14221428 case opt getOutput opts of

1423− [] -> performUsageAnalysis -- interactive

1429+ [] -> performUsageAnalysis (getExpNames exports) -- interactive

14241430 _ -> return [] -- batch, will be checked by the compiler

14251431

14261432 return (map fst ifiles))

@@ -1515,7 +1521,8 @@ idrisMain opts =

15151521 xs -> last xs

15161522 setOptLevel optimise

15171523 let outty = case opt getOutputTy opts of

1518− [] -> Executable

1524+ [] -> if Interface `elem` opts then

1525+ Object else Executable

15191526 xs -> last xs

15201527 let cgn = case opt getCodegen opts of

15211528 [] -> Via "c"

src/Idris/TypeSearch.hs+4−2

@@ -278,7 +278,7 @@ inArgTys = map . first . second

278278

279279typeclassUnify :: Ctxt ClassInfo -> Context -> Type -> Type -> Maybe [(Name, Type)]

280280typeclassUnify 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 []

282282 guard $ null (theHoles \\ map fst res)

283283 let argTys' = map (second $ foldr (.) id [ subst n t | (n, t) <- res ]) tcArgs

284284 return argTys'

@@ -424,7 +424,9 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

424424 unifyQueue state [] = return state

425425 unifyQueue state ((ty1, ty2) : queue) = do

426426 --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) []

428430 (state', queueAdditions) <- resolveUnis res state

429431 guard $ scoreCriterion (score state')

430432 unifyQueue state' (queue ++ queueAdditions)

test/Makefile+1−7

@@ -7,14 +7,8 @@ test: $(TESTS)

77%.test:

88 @perl ./runtest.pl $(patsubst %.test,%,$@)

99

10−test_java:

11− @perl ./runtest.pl without primitives004 --codegen Java

12−

1310test_js:

14− @perl ./runtest.pl without sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 effects003 buffer001 basic007 basic011 primitives004 --codegen node

15−

16−test_llvm:

17− @perl ./runtest.pl without primitives003 primitives004 sugar004 io003 buffer001 --codegen llvm

11+ @perl ./runtest.pl without sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 effects003 buffer001 basic007 basic011 primitives004 ffi006 --codegen node

1812

1913update:

2014 /usr/bin/env perl ./runtest.pl all -u

test/basic006/expected+2−2

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

11test020a.idr:16:18:When elaborating right hand side of foo:

22When elaborating an application of function Prelude.List.reverse:

33 Can't unify

4− Vect n a

4+ Vect n a (Type of xs)

55 with

6− List a

6+ List a (Expected type)

77[3, 2, 1]

88"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

1818

1919notOk : (n : Nat) -> Fin (plus 2 n)

2020notOk 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 @@

11error005.idr:13:1:When elaborating right hand side of two:

22When elaborating argument prf to function Data.Fin.fromInteger:

33 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

55error005.idr:16:1:When elaborating right hand side of hahaha:

66When elaborating argument prf to function Data.Fin.fromInteger:

77 When using 0 as a literal for a Fin n

8− Could not show that 0 is less than n

9−error005.idr:21:1:When elaborating right hand side of notOk:

8+ 0 is not strictly less than n

9+error005.idr:22:1:When elaborating right hand side of notOk:

1010When elaborating argument prf to function Data.Fin.fromInteger:

1111 When using 2 as a literal for a Fin (S (S n))

12− Could not show that 2 is less than 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

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 @@

11Reflect.idr:208:38:When elaborating right hand side of testReflect1:

22When elaborating an application of function Reflect.getJust:

33 Can't unify

4− IsJust (Just x1)

4+ IsJust (Just x1) (Type of ItIsJust)

55 with

6− IsJust (prove (getProof x))

6+ IsJust (prove (getProof x)) (Expected type)

77

88 Specifically:

99 Can't unify

test/reg007/expected+2−2

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

11reg007.lidr:8:1:A.n is already defined

22reg007.lidr:12:11:When elaborating right hand side of hurrah:

33Can't unify

4− n = lala

4+ n = lala (Type of isSame)

55with

6− 0 = 1

6+ 0 = 1 (Expected type)

77

88Specifically:

99 Can't unify

test/reg023/expected+2−2

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

11reg023.idr:7:5:When elaborating right hand side of bad:

22Can't unify

3− [94mNat[0m

3+ [94mNat[0m (Type of [91m0[0m)

44with

5− [92mf[0m [94mNat[0m

5+ [92mf[0m [94mNat[0m (Expected type)

test/reg044/expected+2−2

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

11reg044.idr:4:4:When elaborating right hand side of Main.pf:

22Can't unify

3− [95mb[0m [94m=[0m [95mb[0m

3+ [95mb[0m [94m=[0m [95mb[0m (Type of [91mRefl[0m)

44with

5− [95ma[0m [94m=[0m [95mb[0m

5+ [95ma[0m [94m=[0m [95mb[0m (Expected type)

66

77Specifically:

88 Can't unify

test/tutorial006/expected+4−4

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

11tutorial006a.idr:5:23:When elaborating right hand side of vapp:

22When elaborating argument [95mxs[0m to constructor [91mData.VectType.Vect.::[0m:

33 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 _ _)

55 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)

77

88 Specifically:

99 Can't unify

@@ -12,9 +12,9 @@ When elaborating argument [95mxs[0m to constructor [91mData.VectType.Vect.::

1212 [92mplus[0m [95mn[0m [95mm[0m

1313tutorial006b.idr:10:10:When elaborating right hand side of with block in Main.parity:

1414Can'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)

1616with

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)

1818

1919Specifically:

2020 Can't unify