aca1148 · Idris-dev · git.iko.soy

CHANGELOG+28−13

@@ -8,6 +8,22 @@ New in 0.9.17:

88* Quasiquotation supports the generation of Language.Reflection.Raw terms

99 in addition to Language.Reflection.TT. Types are used for disambiguation,

1010 defaulting to TT at the REPL.

11+* Library operators have been renamed for consistency with Haskell. In

12+ particular, Applicative.(<$>) is now Applicative.(<*>) and (<$>) is

13+ now an alias for Functor.map. Correspondingly, ($>) and (<$) have

14+ been renamed to (<*) and (*>). The cascading effects of this rename

15+ are that Algebra.(<*>) has been renamed to Algebra.(<.>) and

16+ Matrix.(<.>) is now Matrix.(<:>).

17+* Binding forms in DSL notation are now given an extra argument: a

18+ reflected representation of the name that the user chose.

19+ Specifically, the rewritten lambda, pi, and let binders will now get

20+ an extra argument of type TTName. This allows more understandable

21+ dynamic errors in DSL code and more readable code generation results.

22+* DSL notation can now be applied with $

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

24+ called from foreign code

25+* Instances can now have documentation strings.

26+* Type providers can have documentation strings.

1127

1228New in 0.9.16:

1329--------------

@@ -45,7 +61,7 @@ New in 0.9.15:

4561 solved automatically.

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

4763 of large expressions.

48−* EXPERIMENTAL Implementation of uniqueness types

64+* EXPERIMENTAL Implementation of uniqueness types

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

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

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

@@ -59,12 +75,12 @@ New in 0.9.15:

5975 library (see #1516)

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

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

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

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

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

6480 as code examples.

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

6682 provide error messages to IDE clients.

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

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

6884 Engine style)

6985

7086New in 0.9.14:

@@ -141,7 +157,7 @@ New in 0.9.12:

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

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

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

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

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

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

146162* Updated 'effects' library

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

@@ -171,7 +187,7 @@ New in 0.9.11:

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

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

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

174− a pattern for use in totality checking.

190+ a pattern for use in totality checking.

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

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

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

@@ -196,7 +212,7 @@ New in 0.9.10:

196212 types may now depend on earlier methods.

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

198214 expressions can be made instances of a type class.

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

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

200216 monadic/do/etc expressions.

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

202218 "if_valid", "if_error", etc.

@@ -321,7 +337,7 @@ User visible changes:

321337Internal changes:

322338

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

324−* Fixed nested parameters blocks

340+* Fixed nested parameters blocks

325341* Improve efficiency of elaborator by:

326342 - only normalising when necessary

327343 - reducing backtracking with resolving ambiguities

@@ -402,7 +418,7 @@ User visible changes:

402418Internal changes:

403419

404420* Some type class resolution fixes

405−* Several minor bug fixes

421+* Several minor bug fixes

406422* Performance improvements in resolving overloading and type classes

407423

408424New in 0.9.1:

@@ -450,11 +466,10 @@ Complete rewrite. User visible changes:

450466Internal changes:

451467

452468* Everything :-)

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

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

455− which are verified by a minimal type checker.

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

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

471+ which are verified by a minimal type checker.

456472

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

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

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

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

460−

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

contribs/lib/SQLite3/Sqlite3.idr+1−1

@@ -48,7 +48,7 @@ instance Functor DB where

4848

4949instance Applicative DB where

5050 pure = MkDB . return . Right

51− (MkDB f) <$> (MkDB x) = MkDB (do f' <- f

51+ (MkDB f) <*> (MkDB x) = MkDB (do f' <- f

5252 case f' of

5353 Left err => return (Left err)

5454 Right op => x >>= (return . map op))

contribs/lib/SimpleParser/SimpleParser.idr+1−1

@@ -30,7 +30,7 @@ instance Functor Parser where

3030

3131instance Applicative Parser where

3232 pure v = P (\inp => Right (v, inp))

33− a <$> b = P (\inp => do (f, rest) <- parse a inp

33+ a <*> b = P (\inp => do (f, rest) <- parse a inp

3434 (x, rest') <- parse b rest

3535 pure ((f x), rest'))

3636

idris.cabal+19

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

@@ -548,6 +552,9 @@ Extra-source-files:

548552 test/sugar005/*.idr

549553 test/sugar005/expected

550554

555+ test/tactics001/run

556+ test/tactics001/*.idr

557+ test/tactics001/expected

551558

552559 test/totality001/run

553560 test/totality001/*.idr

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

604611 test/unique003/*.idr

605612 test/unique003/expected

606613

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+

607625source-repository head

608626 type: git

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

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

720738 , IRTS.CodegenC

721739 , IRTS.CodegenCommon

722740 , IRTS.CodegenJavaScript

741+ , IRTS.Exports

723742 , IRTS.JavaScript.AST

724743 , IRTS.Compiler

725744 , IRTS.Defunctionalise

libs/base/Control/Arrow.idr+1−1

@@ -95,7 +95,7 @@ instance Arrow a => Functor (ArrowMonad a) where

9595

9696instance Arrow a => Applicative (ArrowMonad a) where

9797 pure x = MkArrowMonad $ arrow $ \_ => x

98− (MkArrowMonad f) <$> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)

98+ (MkArrowMonad f) <*> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)

9999

100100instance ArrowApply a => Monad (ArrowMonad a) where

101101 (MkArrowMonad m) >>= f =

libs/base/Control/IOExcept.idr+2−2

@@ -10,8 +10,8 @@ instance Functor (IOExcept e) where

1010

1111instance Applicative (IOExcept e) where

1212 pure x = ioM (pure (pure x))

13− (ioM f) <$> (ioM a) = ioM (do f' <- f; a' <- a

14− return (f' <$> a'))

13+ (ioM f) <*> (ioM a) = ioM (do f' <- f; a' <- a

14+ return (f' <*> a'))

1515

1616instance Monad (IOExcept e) where

1717 (ioM x) >>= k = ioM (do x' <- x;

libs/base/Control/Monad/Identity.idr+1−1

@@ -14,7 +14,7 @@ instance Functor Identity where

1414instance Applicative Identity where

1515 pure x = Id x

1616

17− (Id f) <$> (Id g) = Id (f g)

17+ (Id f) <*> (Id g) = Id (f g)

1818

1919instance Monad Identity where

2020 (Id x) >>= k = k x

libs/base/Control/Monad/RWS.idr+1−1

@@ -25,7 +25,7 @@ instance Monad m => Functor (RWST r w s m) where

2525

2626instance (Monoid w, Monad m) => Applicative (RWST r w s m) where

2727 pure a = MkRWST $ \_,s => return (a, s, neutral)

28− (MkRWST f) <$> (MkRWST v) = MkRWST $ \r,s => do (a, s', w) <- v r s

28+ (MkRWST f) <*> (MkRWST v) = MkRWST $ \r,s => do (a, s', w) <- v r s

2929 (fn, ss, w') <- f r s

3030 return (fn a, ss, w <+> w)

3131

libs/base/Control/Monad/Reader.idr+1−1

@@ -32,7 +32,7 @@ instance Functor f => Functor (ReaderT r f) where

3232

3333instance Applicative m => Applicative (ReaderT r m) where

3434 pure = liftReaderT . pure

35− (RD f) <$> (RD v) = RD $ \r => f r <$> v r

35+ (RD f) <*> (RD v) = RD $ \r => f r <*> v r

3636

3737instance Alternative m => Alternative (ReaderT r m) where

3838 empty = liftReaderT empty

libs/base/Control/Monad/State.idr+1−1

@@ -29,7 +29,7 @@ instance Functor f => Functor (StateT s f) where

2929instance Monad f => Applicative (StateT s f) where

3030 pure x = ST (\st => pure (x, st))

3131

32− (ST f) <$> (ST a) = ST (\st => do (g, r) <- f st

32+ (ST f) <*> (ST a) = ST (\st => do (g, r) <- f st

3333 (b, t) <- a r

3434 return (g b, t))

3535

libs/base/Control/Monad/Writer.idr+1−1

@@ -31,7 +31,7 @@ instance Functor f => Functor (WriterT w f) where

3131

3232instance (Monoid w, Applicative m) => Applicative (WriterT w m) where

3333 pure a = WR $ pure (a, neutral)

34− (WR f) <$> (WR v) = WR $ liftA2 merge f v where

34+ (WR f) <*> (WR v) = WR $ liftA2 merge f v where

3535 merge (fn, w) (a, w') = (fn a, w <+> w')

3636

3737instance (Monoid w, Alternative m) => Alternative (WriterT w m) where

libs/base/Data/Erased.idr+1−1

@@ -16,7 +16,7 @@ instance Functor Erased where

1616

1717instance Applicative Erased where

1818 pure = Erase

19− (<$>) (Erase f) (Erase x) = Erase (f x)

19+ (<*>) (Erase f) (Erase x) = Erase (f x)

2020

2121instance Monad Erased where

2222 (>>=) (Erase x) f = f x

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/Matrix.idr+29−29

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

77

88%default total

99

10−infixr 2 <.> -- vector inner product

10+infixr 2 <:> -- vector inner product

1111infixr 2 >< -- vector outer product

1212infixr 2 <<>> -- matrix commutator

1313infixr 2 >><< -- matrix anticommutator

1414infixl 3 <\> -- row times a matrix

1515infixr 4 </> -- matrix times a column

16−infixr 5 <> -- matrix multiplication

16+infixr 5 <> -- matrix multiplication

1717infixr 7 \&\ -- vector tensor product

1818infixr 7 <&> -- matrix tensor product

1919

@@ -26,14 +26,14 @@ instance Semigroup a => Semigroup (Vect n a) where

2626

2727instance Monoid a => Monoid (Vect n a) where

2828 neutral {n} = replicate n neutral

29−

29+

3030instance Group a => Group (Vect n a) where

3131 inverse = map inverse

3232

3333instance AbelianGroup a => AbelianGroup (Vect n a) where {}

3434

3535instance Ring a => Ring (Vect n a) where

36− (<*>) v w = zipWith (<*>) v w

36+ (<.>) v w = zipWith (<.>) v w

3737

3838instance RingWithUnity a => RingWithUnity (Vect n a) where

3939 unity {n} = replicate n unity

@@ -42,7 +42,7 @@ instance Field a => Field (Vect n a) where

4242 inverseM = map inverseM

4343

4444instance RingWithUnity a => Module a (Vect n a) where

45− (<#>) r v = map (r <*>) v

45+ (<#>) r v = map (r <.>) v

4646

4747instance RingWithUnity a => Module a (Vect n (Vect l a)) where

4848 (<#>) r m = map (r <#>) m

@@ -53,12 +53,12 @@ instance RingWithUnity a => Module a (Vect n (Vect l a)) where

5353-----------------------------------------------------------------------

5454

5555||| Inner product of ring vectors

56−(<.>) : Ring a => Vect n a -> Vect n a -> a

57−(<.>) w v = foldr (<+>) neutral (zipWith (<*>) w v)

56+(<:>) : Ring a => Vect n a -> Vect n a -> a

57+(<:>) w v = foldr (<+>) neutral (zipWith (<.>) w v)

5858

5959||| Tensor multiply (⊗) ring vectors

6060(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a

61−(\&\) {n} {m} v w = zipWith (<*>) (oextend m v) (orep n w) where

61+(\&\) {n} {m} v w = zipWith (<.>) (oextend m v) (orep n w) where

6262 orep : (n : Nat) -> Vect m a -> Vect (n * m) a

6363 orep n v = concat $ replicate n v

6464 oextend : (n : Nat) -> Vect k a -> Vect (k * n) a

@@ -90,15 +90,15 @@ indices f1 f2 m = index f2 (index f1 m)

9090

9191||| Matrix times a column vector

9292(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a

93−(</>) m v = map (v <.>) m

93+(</>) m v = map (v <:>) m

9494

9595||| Matrix times a row vector

9696(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a

97−(<\>) r m = map (r <.>) $ transpose m

97+(<\>) r m = map (r <:>) $ transpose m

9898

9999||| Matrix multiplication

100−(<>) : Ring a => Matrix n k a ->

101− Matrix k m a ->

100+(<>) : Ring a => Matrix n k a ->

101+ Matrix k m a ->

102102 Matrix n m a

103103(<>) m1 m2 = map (<\> m2) m1

104104

@@ -110,11 +110,11 @@ indices f1 f2 m = index f2 (index f1 m)

110110 stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a

111111 stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2

112112

113−||| Cast a vector from a standard Vect to a proper n x 1 matrix

113+||| Cast a vector from a standard Vect to a proper n x 1 matrix

114114col : Vect n a -> Matrix n 1 a

115115col v = map (\x => [x]) v

116116

117−||| Cast a row from a standard Vect to a proper 1 x n matrix

117+||| Cast a row from a standard Vect to a proper 1 x n matrix

118118row : Vect n a -> Matrix 1 n a

119119row r = [r]

120120

@@ -157,11 +157,11 @@ instance Monoid Integer where

157157

158158instance Group Integer where

159159 inverse = (* -1)

160−

160+

161161instance AbelianGroup Integer

162162

163−instance Ring Integer where

164− (<*>) = (*)

163+instance Ring Integer where

164+ (<.>) = (*)

165165

166166instance RingWithUnity Integer where

167167 unity = 1

@@ -175,11 +175,11 @@ instance Monoid Int where

175175

176176instance Group Int where

177177 inverse = (* -1)

178−

178+

179179instance AbelianGroup Int

180180

181−instance Ring Int where

182− (<*>) = (*)

181+instance Ring Int where

182+ (<.>) = (*)

183183

184184instance RingWithUnity Int where

185185 unity = 1

@@ -193,11 +193,11 @@ instance Monoid Float where

193193

194194instance Group Float where

195195 inverse = (* -1)

196−

196+

197197instance AbelianGroup Float

198198

199−instance Ring Float where

200− (<*>) = (*)

199+instance Ring Float where

200+ (<.>) = (*)

201201

202202instance RingWithUnity Float where

203203 unity = 1

@@ -211,7 +211,7 @@ instance Semigroup Nat where

211211

212212instance Monoid Nat where

213213 neutral = 0

214−

214+

215215instance VerifiedSemigroup Nat where

216216 semigroupOpIsAssociative = plusAssociative

217217

@@ -228,12 +228,12 @@ instance Monoid ZZ where

228228

229229instance Group ZZ where

230230 inverse = (* -1)

231−

231+

232232instance AbelianGroup ZZ

233233

234−instance Ring ZZ where

235− (<*>) = (*)

236−

234+instance Ring ZZ where

235+ (<.>) = (*)

236+

237237instance RingWithUnity ZZ where

238238 unity = 1

239239

@@ -250,7 +250,7 @@ instance Group a => Group (Complex a) where

250250instance Ring a => AbelianGroup (Complex a) where {}

251251

252252instance Ring a => Ring (Complex a) where

253− (<*>) (a :+ b) (c :+ d) = (a <*> c <-> b <*> d) :+ (a <*> d <+> b <*> c)

253+ (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)

254254

255255instance RingWithUnity a => RingWithUnity (Complex a) where

256256 unity = (unity :+ neutral)

libs/base/Data/Morphisms.idr+1−1

@@ -25,7 +25,7 @@ instance Functor (Morphism r) where

2525

2626instance Applicative (Morphism r) where

2727 pure a = Mor $ const a

28− (Mor f) <$> (Mor a) = Mor $ \r => f r $ a r

28+ (Mor f) <*> (Mor a) = Mor $ \r => f r $ a r

2929

3030instance Monad (Morphism r) where

3131 (Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r

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

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

@@ -529,8 +529,10 @@ transpose (x :: xs) = zipWith (::) x (transpose xs)

529529instance Applicative (Vect k) where

530530 pure = replicate _

531531

532− fs <$> vs = zipWith apply fs vs

532+ 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/base/Network/Cgi.idr+1−1

@@ -47,7 +47,7 @@ instance Functor CGI where

4747instance Applicative CGI where

4848 pure v = MkCGI (\s => return (v, s))

4949

50− (MkCGI a) <$> (MkCGI b) = MkCGI (\s => do (f, i) <- a s

50+ (MkCGI a) <*> (MkCGI b) = MkCGI (\s => do (f, i) <- a s

5151 (c, j) <- b i

5252 return (f c, j))

5353

libs/base/Providers.idr+3−3

@@ -17,9 +17,9 @@ instance Functor Provider where

1717 map f (Error err) = Error err

1818

1919instance Applicative Provider where

20− (Provide f) <$> (Provide x) = Provide (f x)

21− (Provide f) <$> (Error err) = Error err

22− (Error err) <$> _ = Error err

20+ (Provide f) <*> (Provide x) = Provide (f x)

21+ (Provide f) <*> (Error err) = Error err

22+ (Error err) <*> _ = Error err

2323 pure = Provide

2424

2525instance Monad Provider where

libs/base/System/Concurrency/Process.idr+1−1

@@ -19,7 +19,7 @@ instance Functor (Process msg) where

1919

2020instance Applicative (Process msg) where

2121 pure = Lift . return

22− (Lift f) <$> (Lift a) = Lift (f <$> a)

22+ (Lift f) <*> (Lift a) = Lift (f <*> a)

2323

2424instance Monad (Process msg) where

2525 (Lift io) >>= k = Lift (do x <- io

libs/effects/Effect/Memory.idr+12−12

@@ -24,11 +24,11 @@ data RawMemory : Effect where

2424 (size : Nat) ->

2525 So (offset + size <= i) ->

2626 RawMemory (Vect size Bits8)

27− (MemoryChunk n i) (\v => MemoryChunk n i)

27+ (MemoryChunk n i) (\v => MemoryChunk n i)

2828 Poke : (offset : Nat) ->

2929 (Vect size Bits8) ->

3030 So (offset <= i && offset + size <= n) ->

31− RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))

31+ RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))

3232 Move : (src : MemoryChunk src_size src_init) ->

3333 (dst_offset : Nat) ->

3434 (src_offset : Nat) ->

@@ -36,8 +36,8 @@ data RawMemory : Effect where

3636 So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

3737 So (src_offset + size <= src_init) ->

3838 RawMemory () (MemoryChunk dst_size dst_init)

39− (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))

40− GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)

39+ (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))

40+ GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)

4141

4242private

4343do_malloc : Nat -> IOExcept String Ptr

@@ -84,9 +84,9 @@ instance Handler RawMemory (IOExcept String) where

8484 = do ptr <- do_malloc n

8585 k () (CH ptr)

8686 handle {-{res = MemoryChunk _ offset}-} (CH ptr) (Initialize {i} c size _) k

87− = ioe_lift (do_memset ptr i c size) $> k () (CH ptr)

87+ = ioe_lift (do_memset ptr i c size) *> k () (CH ptr)

8888 handle (CH ptr) (Free) k

89− = ioe_lift (do_free ptr) $> k () ()

89+ = ioe_lift (do_free ptr) *> k () ()

9090 handle (CH ptr) (Peek offset size _) k

9191 = do res <- ioe_lift (do_peek ptr offset size)

9292 k res (CH ptr)

@@ -102,7 +102,7 @@ instance Handler RawMemory (IOExcept String) where

102102RAW_MEMORY : Type -> EFFECT

103103RAW_MEMORY t = MkEff t RawMemory

104104

105−allocate : (n : Nat) ->

105+allocate : (n : Nat) ->

106106 Eff () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])

107107allocate size = call $ Allocate size

108108

@@ -111,7 +111,7 @@ initialize : {i : Nat} ->

111111 Bits8 ->

112112 (size : Nat) ->

113113 So (i + size <= n) ->

114− Eff () [RAW_MEMORY (MemoryChunk n i)]

114+ Eff () [RAW_MEMORY (MemoryChunk n i)]

115115 (\v => [RAW_MEMORY (MemoryChunk n (i + size))])

116116initialize c size prf = call $ Initialize c size prf

117117

@@ -122,7 +122,7 @@ peek : {i : Nat} ->

122122 (offset : Nat) ->

123123 (size : Nat) ->

124124 So (offset + size <= i) ->

125− { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)

125+ { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)

126126peek offset size prf = call $ Peek offset size prf

127127

128128poke : {n : Nat} ->

@@ -130,12 +130,12 @@ poke : {n : Nat} ->

130130 (offset : Nat) ->

131131 Vect size Bits8 ->

132132 So (offset <= i && offset + size <= n) ->

133− Eff () [RAW_MEMORY (MemoryChunk n i)]

133+ Eff () [RAW_MEMORY (MemoryChunk n i)]

134134 (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])

135135poke offset content prf = call $ Poke offset content prf

136136

137137private

138−getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff (MemoryChunk n i)

138+getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff (MemoryChunk n i)

139139getRawPtr = call $ GetRawPtr

140140

141141private

@@ -173,5 +173,5 @@ move : {dst_size : Nat} ->

173173move dst_offset src_offset size dst_bounds src_bounds

174174 = do src_ptr <- Src :- getRawPtr

175175 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds

176− return ()

176+ return ()

177177

libs/effects/Effect/Monad.idr+1−1

@@ -11,7 +11,7 @@ using (xs : List EFFECT, m : Type -> Type)

1111

1212 instance Applicative (\a => EffM m a xs (\v => xs)) where

1313 pure = value

14− (<$>) f a = do f' <- f

14+ (<*>) f a = do f' <- f

1515 a' <- a

1616 value (f' a')

1717

libs/effects/Effect/StdIO.idr+11−4

@@ -9,8 +9,8 @@ import Control.IOExcept

99

1010||| The internal representation of StdIO effects

1111data StdIO : Effect where

12− PutStr : String -> { () } StdIO ()

13− GetStr : { () } StdIO String

12+ PutStr : String -> { () } StdIO ()

13+ GetStr : { () } StdIO String

1414 PutCh : Char -> { () } StdIO ()

1515 GetCh : { () } StdIO Char

1616

@@ -22,13 +22,13 @@ data StdIO : Effect where

2222instance Handler StdIO IO where

2323 handle () (PutStr s) k = do putStr s; k () ()

2424 handle () GetStr k = do x <- getLine; k x ()

25− handle () (PutCh c) k = do putChar c; k () ()

25+ handle () (PutCh c) k = do putChar c; k () ()

2626 handle () GetCh k = do x <- getChar; k x ()

2727

2828instance Handler StdIO (IOExcept a) where

2929 handle () (PutStr s) k = do ioe_lift $ putStr s; k () ()

3030 handle () GetStr k = do x <- ioe_lift $ getLine; k x ()

31− handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()

31+ handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()

3232 handle () GetCh k = do x <- ioe_lift $ getChar; k x ()

3333

3434-------------------------------------------------------------

@@ -58,3 +58,10 @@ getStr = call $ GetStr

5858getChar : { [STDIO] } Eff Char

5959getChar = call $ GetCh

6060

61+||| Given a parameter `a` 'show' `a` to standard output.

62+print : Show a => a -> { [STDIO] } Eff ()

63+print a = putStr (show a)

64+

65+||| Given a parameter `a` 'show' `a` to a standard output, terminating with a newline

66+printLn : Show a => a -> { [STDIO] } Eff ()

67+printLn a = putStrLn (show a)

libs/effects/Effects.idr+3−3

@@ -174,7 +174,7 @@ return x = value x

174174

175175-- ------------------------------------------------------ [ for idiom brackets ]

176176

177−infixl 2 <$>

177+infixl 2 <*>

178178

179179pure : a -> Eff a xs (\v => xs)

180180pure = value

@@ -182,9 +182,9 @@ pure = value

182182pureM : (val : a) -> Eff a (xs val) xs

183183pureM = value

184184

185−(<$>) : Eff (a -> b) xs (\v => xs) ->

185+(<*>) : Eff (a -> b) xs (\v => xs) ->

186186 Eff a xs (\v => xs) -> Eff b xs (\v => xs)

187−(<$>) prog v = do fn <- prog

187+(<*>) prog v = do fn <- prog

188188 arg <- v

189189 return (fn arg)

190190

libs/oldeffects/Effect/Monad.idr+1−1

@@ -11,7 +11,7 @@ using (xs : List EFFECT, m : Type -> Type)

1111

1212 instance Applicative (\a => EffM m a xs (\v => xs)) where

1313 pure = value

14− (<$>) f a = do f' <- f

14+ (<*>) f a = do f' <- f

1515 a' <- a

1616 value (f' a')

1717

libs/oldeffects/Effects.idr+3−3

@@ -185,16 +185,16 @@ return x = value x

185185

186186-- ------------------------------------------------------ [ for idiom brackets ]

187187

188−infixl 2 <$>

188+infixl 2 <*>

189189

190190pure : a -> Eff m a xs (\v => xs)

191191pure = value

192192

193193syntax pureM [val] = with_val val (pure ())

194194

195−(<$>) : Eff m (a -> b) xs (\v => xs) ->

195+(<*>) : Eff m (a -> b) xs (\v => xs) ->

196196 Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)

197−(<$>) prog v = do fn <- prog

197+(<*>) prog v = do fn <- prog

198198 arg <- v

199199 return (fn arg)

200200

libs/prelude/IO.idr+56−3

@@ -23,11 +23,17 @@ WorldRes x = x

2323record FFI where

2424 ffi_types : Type -> Type

2525 ffi_fn : Type

26+ ffi_data : Type

2627 constructor MkFFI

28+

2729{-

2830record FFI : Type where

2931 MkFFI : (ffi_types : Type -> Type) -> (ffi_fn : Type) -> FFI

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

33+ (ffi_fn : Type) ->

34+ (ffi_data : Type) -> FFI

3035-}

36+

3137abstract

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

3339 MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a

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

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

95101liftPrimIO = MkIO

96102

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

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

105+

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

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

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

108+run__IO f = call__IO f

99109

100110unsafePerformIO : IO' ffi a -> a

101111unsafePerformIO (MkIO f) = unsafePerformPrimIO

@@ -148,7 +158,7 @@ data C_Types : Type -> Type where

148158 C_IntT : C_IntTypes i -> C_Types i

149159

150160FFI_C : FFI

151−FFI_C = MkFFI C_Types String

161+FFI_C = MkFFI C_Types String String

152162

153163IO : Type -> Type

154164IO = IO' FFI_C

@@ -199,8 +209,51 @@ mutual

199209%used MkJsFn x

200210

201211FFI_JS : FFI

202−FFI_JS = MkFFI JS_Types String

212+FFI_JS = MkFFI JS_Types String String

203213

204214JS_IO : Type -> Type

205215JS_IO = IO' FFI_JS

206216

217+

218+--------- Foreign Exports

219+

220+namespace FFI_Export

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

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

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

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

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

226+

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

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

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

230+

231+ %used FFI_ExpType n

232+ %used FFI_ExpType def

233+ %used FFI_Prim prim

234+

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

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

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

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

239+

240+ %used FFI_IO b

241+ %used FFI_Fun b

242+ %used FFI_Fun a

243+ %used FFI_Ret b

244+

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

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

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

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

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

250+ End : FFI_Export f h xs

251+

252+%used Data x

253+%used Data n

254+%used Data es

255+%used Fun fn

256+%used Fun n

257+%used Fun es

258+%used Fun prf

259+

libs/prelude/Language/Reflection.idr+181−33

@@ -267,108 +267,193 @@ data Tactic =

267267%name Tactic tac, tac'

268268

269269

270−||| Things with a canonical representation in the TT datatype.

270+||| Things with a canonical representation as a reflected term.

271271|||

272272||| This type class is intended to be used during proof automation and the

273273||| construction of custom tactics.

274274|||

275275||| @ a the type to be quoted

276−class Quotable a where

276+||| @ t the type to quote it to (typically `TT` or `Raw`)

277+class Quotable a t where

277278 ||| A representation of the type `a`.

278279 |||

279280 ||| This is to enable quoting polymorphic datatypes

280− quotedTy : TT

281+ quotedTy : t

281282

282283 ||| Quote a particular element of `a`.

283284 |||

284285 ||| Each equation should look something like ```quote (Foo x y) = `(Foo ~(quote x) ~(quote y))```

285− quote : a -> TT

286+ quote : a -> t

286287

287−instance Quotable Nat where

288+instance Quotable Nat TT where

288289 quotedTy = `(Nat)

289290

290291 quote Z = `(Z)

291292 quote (S k) = `(S ~(quote k))

292293

293−instance Quotable Int where

294+instance Quotable Nat Raw where

295+ quotedTy = `(Nat)

296+

297+ quote Z = `(Z)

298+ quote (S k) = `(S ~(quote k))

299+

300+instance Quotable Int TT where

294301 quotedTy = `(Int)

295302 quote x = TConst (I x)

296303

297−instance Quotable Float where

304+instance Quotable Int Raw where

305+ quotedTy = `(Int)

306+ quote x = RConstant (I x)

307+

308+instance Quotable Float TT where

298309 quotedTy = `(Float)

299310 quote x = TConst (Fl x)

300311

301−instance Quotable Char where

312+instance Quotable Float Raw where

313+ quotedTy = `(Float)

314+ quote x = RConstant (Fl x)

315+

316+instance Quotable Char TT where

302317 quotedTy = `(Char)

303318 quote x = TConst (Ch x)

304319

305−instance Quotable Bits8 where

320+instance Quotable Char Raw where

321+ quotedTy = `(Char)

322+ quote x = RConstant (Ch x)

323+

324+instance Quotable Bits8 TT where

306325 quotedTy = `(Bits8)

307326 quote x = TConst (B8 x)

308327

309−instance Quotable Bits16 where

328+instance Quotable Bits8 Raw where

329+ quotedTy = `(Bits8)

330+ quote x = RConstant (B8 x)

331+

332+instance Quotable Bits16 TT where

310333 quotedTy = `(Bits16)

311334 quote x = TConst (B16 x)

312335

313−instance Quotable Bits32 where

336+instance Quotable Bits16 Raw where

337+ quotedTy = `(Bits16)

338+ quote x = RConstant (B16 x)

339+

340+instance Quotable Bits32 TT where

314341 quotedTy = `(Bits32)

315342 quote x = TConst (B32 x)

316343

317−instance Quotable Bits64 where

344+instance Quotable Bits32 Raw where

345+ quotedTy = `(Bits32)

346+ quote x = RConstant (B32 x)

347+

348+instance Quotable Bits64 TT where

318349 quotedTy = `(Bits64)

319350 quote x = TConst (B64 x)

320351

321−instance Quotable Integer where

352+instance Quotable Bits64 Raw where

353+ quotedTy = `(Bits64)

354+ quote x = RConstant (B64 x)

355+

356+instance Quotable Integer TT where

322357 quotedTy = `(Integer)

323358 quote x = TConst (BI x)

324359

325−instance Quotable Bits8x16 where

360+instance Quotable Integer Raw where

361+ quotedTy = `(Integer)

362+ quote x = RConstant (BI x)

363+

364+instance Quotable Bits8x16 TT where

326365 quotedTy = `(Bits8x16)

327366 quote x = TConst (B8V x)

328367

329−instance Quotable Bits16x8 where

368+instance Quotable Bits8x16 Raw where

369+ quotedTy = `(Bits8x16)

370+ quote x = RConstant (B8V x)

371+

372+instance Quotable Bits16x8 TT where

330373 quotedTy = `(Bits16x8)

331374 quote x = TConst (B16V x)

332375

333−instance Quotable Bits32x4 where

376+instance Quotable Bits16x8 Raw where

377+ quotedTy = `(Bits16x8)

378+ quote x = RConstant (B16V x)

379+

380+instance Quotable Bits32x4 TT where

334381 quotedTy = `(Bits32x4)

335382 quote x = TConst (B32V x)

336383

337−instance Quotable Bits64x2 where

384+instance Quotable Bits32x4 Raw where

385+ quotedTy = `(Bits32x4)

386+ quote x = RConstant (B32V x)

387+

388+instance Quotable Bits64x2 TT where

338389 quotedTy = `(Bits64x2)

339390 quote x = TConst (B64V x)

340391

341−instance Quotable String where

392+instance Quotable Bits64x2 Raw where

393+ quotedTy = `(Bits64x2)

394+ quote x = RConstant (B64V x)

395+

396+instance Quotable String TT where

342397 quotedTy = `(String)

343398 quote x = TConst (Str x)

344399

345−instance Quotable NameType where

400+instance Quotable String Raw where

401+ quotedTy = `(String)

402+ quote x = RConstant (Str x)

403+

404+instance Quotable NameType TT where

346405 quotedTy = `(NameType)

347406 quote Bound = `(Bound)

348407 quote Ref = `(Ref)

349408 quote (DCon x y) = `(DCon ~(quote x) ~(quote y))

350409 quote (TCon x y) = `(TCon ~(quote x) ~(quote y))

351410

352−instance Quotable a => Quotable (List a) where

411+instance Quotable NameType Raw where

412+ quotedTy = `(NameType)

413+ quote Bound = `(Bound)

414+ quote Ref = `(Ref)

415+ quote (DCon x y) = `(DCon ~(quote {t=Raw} x) ~(quote {t=Raw} y))

416+ quote (TCon x y) = `(TCon ~(quote {t=Raw} x) ~(quote {t=Raw} y))

417+

418+instance Quotable a TT => Quotable (List a) TT where

353419 quotedTy = `(List ~(quotedTy {a=a}))

354420 quote [] = `(List.Nil {a=~quotedTy})

355421 quote (x :: xs) = `(List.(::) {a=~quotedTy} ~(quote x) ~(quote xs))

356422

357−instance Quotable TTName where

423+instance Quotable a Raw => Quotable (List a) Raw where

424+ quotedTy = `(List ~(quotedTy {a=a}))

425+ quote [] = `(List.Nil {a=~quotedTy})

426+ quote (x :: xs) = `(List.(::) {a=~quotedTy} ~(quote x) ~(quote xs))

427+

428+instance Quotable TTName TT where

358429 quotedTy = `(TTName)

359430 quote (UN x) = `(UN ~(quote x))

360431 quote (NS n xs) = `(NS ~(quote n) ~(quote xs))

361432 quote (MN x y) = `(MN ~(quote x) ~(quote y))

362433 quote NErased = `(NErased)

363434

364−instance Quotable NativeTy where

435+instance Quotable TTName Raw where

436+ quotedTy = `(TTName)

437+ quote (UN x) = `(UN ~(quote {t=Raw} x))

438+ quote (NS n xs) = `(NS ~(quote {t=Raw} n) ~(quote {t=Raw} xs))

439+ quote (MN x y) = `(MN ~(quote {t=Raw} x) ~(quote {t=Raw} y))

440+ quote NErased = `(NErased)

441+

442+instance Quotable NativeTy TT where

443+ quotedTy = `(NativeTy)

444+ quote IT8 = `(Reflection.IT8)

445+ quote IT16 = `(Reflection.IT16)

446+ quote IT32 = `(Reflection.IT32)

447+ quote IT64 = `(Reflection.IT64)

448+

449+instance Quotable NativeTy Raw where

365450 quotedTy = `(NativeTy)

366451 quote IT8 = `(Reflection.IT8)

367452 quote IT16 = `(Reflection.IT16)

368453 quote IT32 = `(Reflection.IT32)

369454 quote IT64 = `(Reflection.IT64)

370455

371−instance Quotable Reflection.IntTy where

456+instance Quotable Reflection.IntTy TT where

372457 quotedTy = `(Reflection.IntTy)

373458 quote (ITFixed x) = `(ITFixed ~(quote x))

374459 quote ITNative = `(Reflection.ITNative)

@@ -376,12 +461,25 @@ instance Quotable Reflection.IntTy where

376461 quote ITChar = `(Reflection.ITChar)

377462 quote (ITVec x y) = `(ITVec ~(quote x) ~(quote y))

378463

379−instance Quotable ArithTy where

464+instance Quotable Reflection.IntTy Raw where

465+ quotedTy = `(Reflection.IntTy)

466+ quote (ITFixed x) = `(ITFixed ~(quote {t=Raw} x))

467+ quote ITNative = `(Reflection.ITNative)

468+ quote ITBig = `(ITBig)

469+ quote ITChar = `(Reflection.ITChar)

470+ quote (ITVec x y) = `(ITVec ~(quote {t=Raw} x) ~(quote {t=Raw} y))

471+

472+instance Quotable ArithTy TT where

380473 quotedTy = `(ArithTy)

381474 quote (ATInt x) = `(ATInt ~(quote x))

382475 quote ATFloat = `(ATFloat)

383476

384−instance Quotable Const where

477+instance Quotable ArithTy Raw where

478+ quotedTy = `(ArithTy)

479+ quote (ATInt x) = `(ATInt ~(quote {t=Raw} x))

480+ quote ATFloat = `(ATFloat)

481+

482+instance Quotable Const TT where

385483 quotedTy = `(Const)

386484 quote (I x) = `(I ~(quote x))

387485 quote (BI x) = `(BI ~(quote x))

@@ -406,19 +504,55 @@ instance Quotable Const where

406504 quote WorldType = `(WorldType)

407505 quote TheWorld = `(TheWorld)

408506

409−instance Quotable TTUExp where

507+instance Quotable Const Raw where

508+ quotedTy = `(Const)

509+ quote (I x) = `(I ~(quote {t=Raw} x))

510+ quote (BI x) = `(BI ~(quote {t=Raw} x))

511+ quote (Fl x) = `(Fl ~(quote {t=Raw} x))

512+ quote (Ch x) = `(Ch ~(quote {t=Raw} x))

513+ quote (Str x) = `(Str ~(quote {t=Raw} x))

514+ quote (B8 x) = `(B8 ~(quote {t=Raw} x))

515+ quote (B16 x) = `(B16 ~(quote {t=Raw} x))

516+ quote (B32 x) = `(B32 ~(quote {t=Raw} x))

517+ quote (B64 x) = `(B64 ~(quote {t=Raw} x))

518+ quote (B8V xs) = `(B8V ~(quote {t=Raw} xs))

519+ quote (B16V xs) = `(B16V ~(quote {t=Raw} xs))

520+ quote (B32V xs) = `(B32V ~(quote {t=Raw} xs))

521+ quote (B64V xs) = `(B64V ~(quote {t=Raw} xs))

522+ quote (AType x) = `(AType ~(quote {t=Raw} x))

523+ quote StrType = `(StrType)

524+ quote PtrType = `(PtrType)

525+ quote ManagedPtrType = `(ManagedPtrType)

526+ quote BufferType = `(BufferType)

527+ quote VoidType = `(VoidType)

528+ quote Forgot = `(Forgot)

529+ quote WorldType = `(WorldType)

530+ quote TheWorld = `(TheWorld)

531+

532+instance Quotable TTUExp TT where

410533 quotedTy = `(TTUExp)

411534 quote (UVar x) = `(UVar ~(quote x))

412535 quote (UVal x) = `(UVal ~(quote x))

413536

414−instance Quotable Universe where

537+instance Quotable TTUExp Raw where

538+ quotedTy = `(TTUExp)

539+ quote (UVar x) = `(UVar ~(quote {t=Raw} x))

540+ quote (UVal x) = `(UVal ~(quote {t=Raw} x))

541+

542+instance Quotable Universe TT where

543+ quotedTy = `(Universe)

544+ quote Reflection.NullType = `(NullType)

545+ quote Reflection.UniqueType = `(UniqueType)

546+ quote Reflection.AllTypes = `(AllTypes)

547+

548+instance Quotable Universe Raw where

415549 quotedTy = `(Universe)

416550 quote Reflection.NullType = `(NullType)

417551 quote Reflection.UniqueType = `(UniqueType)

418552 quote Reflection.AllTypes = `(AllTypes)

419553

420554mutual

421− instance Quotable TT where

555+ instance Quotable TT TT where

422556 quotedTy = `(TT)

423557 quote (P nt n tm) = `(P ~(quote nt) ~(quote n) ~(quote tm))

424558 quote (V x) = `(V ~(quote x))

@@ -431,7 +565,7 @@ mutual

431565 quote (TType uexp) = `(TType ~(quote uexp))

432566 quote (UType u) = `(UType ~(quote u))

433567

434− instance Quotable (Binder TT) where

568+ instance Quotable (Binder TT) TT where

435569 quotedTy = `(Binder TT)

436570 quote (Lam x) = `(Lam {a=TT} ~(assert_total (quote x)))

437571 quote (Pi x k) = `(Pi {a=TT} ~(assert_total (quote x))

@@ -448,7 +582,7 @@ mutual

448582 quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))

449583

450584

451−instance Quotable ErrorReportPart where

585+instance Quotable ErrorReportPart TT where

452586 quotedTy = `(ErrorReportPart)

453587 quote (TextPart x) = `(TextPart ~(quote x))

454588 quote (NamePart n) = `(NamePart ~(quote n))

@@ -476,15 +610,15 @@ mutual

476610 quoteRawBinder (PVar x) = `(PVar {a=Raw} ~(quoteRaw x))

477611 quoteRawBinder (PVTy x) = `(PVTy {a=Raw} ~(quoteRaw x))

478612

479−instance Quotable Raw where

613+instance Quotable Raw TT where

480614 quotedTy = `(Raw)

481615 quote = quoteRaw

482616

483−instance Quotable (Binder Raw) where

617+instance Quotable (Binder Raw) TT where

484618 quotedTy = `(Binder Raw)

485619 quote = quoteRawBinder

486620

487−instance Quotable Tactic where

621+instance Quotable Tactic TT where

488622 quotedTy = `(Tactic)

489623 quote (Try tac tac') = `(Try ~(quote tac) ~(quote tac'))

490624 quote (GoalType x tac) = `(GoalType ~(quote x) ~(quote tac))

@@ -514,3 +648,17 @@ instance Quotable Tactic where

514648 quote (Fail xs) = `(Fail ~(quote xs))

515649 quote SourceFC = `(SourceFC)

516650

651+

652+instance Quotable SourceLocation TT where

653+ quotedTy = `(SourceLocation)

654+ quote (FileLoc fn (sl, sc) (el, ec)) =

655+ `(FileLoc ~(quote fn)

656+ (~(quote sl), ~(quote sc))

657+ (~(quote el), ~(quote ec)))

658+

659+instance Quotable SourceLocation Raw where

660+ quotedTy = `(SourceLocation)

661+ quote (FileLoc fn (sl, sc) (el, ec)) =

662+ `(FileLoc ~(quote {t=Raw} fn)

663+ (~(quote {t=Raw} sl), ~(quote {t=Raw} sc))

664+ (~(quote {t=Raw} el), ~(quote {t=Raw} ec)))

libs/prelude/Language/Reflection/Errors.idr+1−1

@@ -29,7 +29,7 @@ data Err = Msg String

2929 | NoTypeDecl TTName

3030 | NotInjective TT TT TT

3131 | CantResolve TT

32− | CantResolveAlts (List String)

32+ | CantResolveAlts (List TTName)

3333 | IncompleteTerm TT

3434 | UniverseError

3535 | ProgramLineComment

libs/prelude/Language/Reflection/Tactical.idr+22−1

@@ -22,6 +22,8 @@ data Tactical : Type -> Type where

2222 prim__Holes : Tactical (List TTName)

2323 prim__Guess : Tactical (Maybe TT)

2424

25+ prim__SourceLocation : Tactical SourceLocation

26+

2527 prim__Forget : TT -> Tactical Raw

2628

2729 prim__Gensym : String -> Tactical TTName

@@ -32,7 +34,10 @@ data Tactical : Type -> Type where

3234 prim__Unfocus : TTName -> Tactical ()

3335 prim__Attack : Tactical ()

3436

37+ prim__Rewrite : Raw -> Tactical ()

38+

3539 prim__Claim : TTName -> Raw -> Tactical ()

40+ prim__Intro : Maybe TTName -> Tactical ()

3641

3742-------------

3843-- Public API

@@ -44,7 +49,7 @@ instance Functor Tactical where

4449

4550instance Applicative Tactical where

4651 pure x = prim__PureTactical x

47− f <$> x = prim__BindTactical f $ \g =>

52+ f <*> x = prim__BindTactical f $ \g =>

4853 prim__BindTactical x $ \y =>

4954 prim__PureTactical $ g y

5055

@@ -93,3 +98,19 @@ attack = prim__Attack

9398

9499claim : TTName -> Raw -> Tactical ()

95100claim n ty = prim__Claim n ty

101+

102+intro : Maybe TTName -> Tactical ()

103+intro n = prim__Intro n

104+

105+||| Find out the present source context for the tactic script

106+getSourceLocation : Tactical SourceLocation

107+getSourceLocation = prim__SourceLocation

108+

109+||| Attempt to solve the current goal with the source code location

110+sourceLocation : Tactical ()

111+sourceLocation = do loc <- getSourceLocation

112+ fill (quote loc)

113+ solve

114+

115+rewriteWith : Raw -> Tactical ()

116+rewriteWith rule = prim__Rewrite rule

libs/prelude/Prelude.idr+8−8

@@ -249,31 +249,31 @@ instance Functor (Either e) where

249249instance Applicative PrimIO where

250250 pure = prim_io_return

251251

252− am <$> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))

252+ am <*> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))

253253

254254instance Applicative (IO' ffi) where

255255 pure x = io_return x

256− f <$> a = io_bind f (\f' =>

256+ f <*> a = io_bind f (\f' =>

257257 io_bind a (\a' =>

258258 io_return (f' a')))

259259

260260instance Applicative Maybe where

261261 pure = Just

262262

263− (Just f) <$> (Just a) = Just (f a)

264− _ <$> _ = Nothing

263+ (Just f) <*> (Just a) = Just (f a)

264+ _ <*> _ = Nothing

265265

266266instance Applicative (Either e) where

267267 pure = Right

268268

269− (Left a) <$> _ = Left a

270− (Right f) <$> (Right r) = Right (f r)

271− (Right _) <$> (Left l) = Left l

269+ (Left a) <*> _ = Left a

270+ (Right f) <*> (Right r) = Right (f r)

271+ (Right _) <*> (Left l) = Left l

272272

273273instance Applicative List where

274274 pure x = [x]

275275

276− fs <$> vs = concatMap (\f => map f vs) fs

276+ fs <*> vs = concatMap (\f => map f vs) fs

277277

278278---- Alternative instances

279279

libs/prelude/Prelude/Algebra.idr+37−37

@@ -5,7 +5,7 @@ import Builtins

55-- XXX: change?

66infixl 6 <->

77infixl 6 <+>

8−infixl 6 <*>

8+infixl 6 <.>

99infixl 5 <#>

1010

1111%access public

@@ -96,18 +96,18 @@ class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where

9696||| + Inverse for `<+>`:

9797||| forall a, a <+> inverse a == neutral

9898||| forall a, inverse a <+> a == neutral

99−||| + Associativity of `<*>`:

100−||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c

101−||| + Distributivity of `<*>` and `<->`:

102−||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)

103−||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)

99+||| + Associativity of `<.>`:

100+||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c

101+||| + Distributivity of `<.>` and `<->`:

102+||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)

103+||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)

104104class AbelianGroup a => Ring a where

105− (<*>) : a -> a -> a

105+ (<.>) : a -> a -> a

106106

107107class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

108− total ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r

109− total ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)

110− total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (c <*> r)

108+ total ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r

109+ total ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)

110+ total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)

111111

112112||| Sets equipped with two binary operations, one associative and commutative

113113||| supplied with a neutral element, and the other associative supplied with a

@@ -124,20 +124,20 @@ class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

124124||| + Inverse for `<+>`:

125125||| forall a, a <+> inverse a == neutral

126126||| forall a, inverse a <+> a == neutral

127−||| + Associativity of `<*>`:

128−||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c

129−||| + Neutral for `<*>`:

130−||| forall a, a <*> unity == a

131−||| forall a, unity <*> a == a

132−||| + Distributivity of `<*>` and `<->`:

133−||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)

134−||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)

127+||| + Associativity of `<.>`:

128+||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c

129+||| + Neutral for `<.>`:

130+||| forall a, a <.> unity == a

131+||| forall a, unity <.> a == a

132+||| + Distributivity of `<.>` and `<->`:

133+||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)

134+||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)

135135class Ring a => RingWithUnity a where

136136 unity : a

137137

138138class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where

139− total ringWithUnityIsUnityL : (l : a) -> l <*> unity = l

140− total ringWithUnityIsUnityR : (r : a) -> unity <*> r = r

139+ total ringWithUnityIsUnityL : (l : a) -> l <.> unity = l

140+ total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r

141141

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

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

@@ -281,31 +281,31 @@ class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, Verif

281281||| + Inverse for `<+>`:

282282||| forall a, a <+> inverse a == neutral

283283||| forall a, inverse a <+> a == neutral

284−||| + Associativity of `<*>`:

285−||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c

286−||| + Unity for `<*>`:

287−||| forall a, a <*> unity == a

288−||| forall a, unity <*> a == a

289−||| + InverseM of `<*>`:

290−||| forall a, a <*> inverseM a == unity

291−||| forall a, inverseM a <*> a == unity

292−||| + Distributivity of `<*>` and `<->`:

293−||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)

294−||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)

284+||| + Associativity of `<.>`:

285+||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c

286+||| + Unity for `<.>`:

287+||| forall a, a <.> unity == a

288+||| forall a, unity <.> a == a

289+||| + InverseM of `<.>`:

290+||| forall a, a <.> inverseM a == unity

291+||| forall a, inverseM a <.> a == unity

292+||| + Distributivity of `<.>` and `<->`:

293+||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)

294+||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)

295295class RingWithUnity a => Field a where

296296 inverseM : a -> a

297297

298298class (VerifiedRing a, Field a) => VerifiedField a where

299− total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity

300− total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity

299+ total fieldInverseIsInverseL : (l : a) -> l <.> inverseM l = unity

300+ total fieldInverseIsInverseR : (r : a) -> inverseM r <.> r = unity

301301

302302||| A module over a ring is an additive abelian group of 'vectors' endowed with a

303−||| scale operation multiplying vectors by ring elements, and distributivity laws

304−||| relating the scale operation to both ring addition and module addition.

303+||| scale operation multiplying vectors by ring elements, and distributivity laws

304+||| relating the scale operation to both ring addition and module addition.

305305||| Must satisfy the following laws:

306306|||

307307||| + Compatibility of scalar multiplication with ring multiplication:

308−||| forall a b v, a <#> (b <#> v) = (a <*> b) <#> v

308+||| forall a b v, a <#> (b <#> v) = (a <.> b) <#> v

309309||| + Ring unity is the identity element of scalar multiplication:

310310||| forall v, unity <#> v = v

311311||| + Distributivity of `<#>` and `<+>`:

@@ -315,7 +315,7 @@ class (RingWithUnity a, AbelianGroup b) => Module a b where

315315 (<#>) : a -> b -> b

316316

317317class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where

318− total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <*> y) <#> v

318+ total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v

319319 total moduleScalarUnityIsUnity : (v : b) -> unity <#> v = v

320320 total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)

321321 total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)

libs/prelude/Prelude/Applicative.idr+17−17

@@ -9,46 +9,46 @@ import Prelude.Functor

99

1010---- Applicative functors/Idioms

1111

12−infixl 2 <$>

12+infixl 2 <*>

1313

1414class Functor f => Applicative (f : Type -> Type) where

1515 pure : a -> f a

16− (<$>) : f (a -> b) -> f a -> f b

16+ (<*>) : f (a -> b) -> f a -> f b

1717

1818instance Applicative id where

1919 pure a = a

20− f <$> a = f a

20+ f <*> a = f a

2121

2222class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where

2323 applicativeMap : (x : f a) -> (g : a -> b) ->

24− map g x = pure g <$> x

25− applicativeIdentity : (x : f a) -> pure id <$> x = x

24+ map g x = pure g <*> x

25+ applicativeIdentity : (x : f a) -> pure id <*> x = x

2626 applicativeComposition : (x : f a) -> (g1 : f (a -> b)) -> (g2 : f (b -> c)) ->

27− ((pure (.) <$> g2) <$> g1) <$> x = g2 <$> (g1 <$> x)

27+ ((pure (.) <*> g2) <*> g1) <*> x = g2 <*> (g1 <*> x)

2828 applicativeHomomorphism : (x : a) -> (g : a -> b) ->

29− (<$>) {f} (pure g) (pure x) = pure {f} (g x)

29+ (<*>) {f} (pure g) (pure x) = pure {f} (g x)

3030 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->

31− g <$> pure x = pure (\g' : a -> b => g' x) <$> g

31+ g <*> pure x = pure (\g' : a -> b => g' x) <*> g

3232

33−infixl 2 <$

34−(<$) : Applicative f => f a -> f b -> f a

35−a <$ b = map const a <$> b

33+infixl 2 <*

34+(<*) : Applicative f => f a -> f b -> f a

35+a <* b = map const a <*> b

3636

37−infixl 2 $>

38−($>) : Applicative f => f a -> f b -> f b

39−a $> b = map (const id) a <$> b

37+infixl 2 *>

38+(*>) : Applicative f => f a -> f b -> f b

39+a *> b = map (const id) a <*> b

4040

4141||| Lift a function to an applicative

4242liftA : Applicative f => (a -> b) -> f a -> f b

43−liftA f a = pure f <$> a

43+liftA f a = pure f <*> a

4444

4545||| Lift a two-argument function to an applicative

4646liftA2 : Applicative f => (a -> b -> c) -> f a -> f b -> f c

47−liftA2 f a b = (map f a) <$> b

47+liftA2 f a b = (map f a) <*> b

4848

4949||| Lift a three-argument function to an applicative

5050liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d

51−liftA3 f a b c = (map f a) <$> b <$> c

51+liftA3 f a b c = (map f a) <*> b <*> c

5252

5353infixl 3 <|>

5454class Applicative f => Alternative (f : Type -> Type) where

libs/prelude/Prelude/Functor.idr+8

@@ -10,6 +10,14 @@ class Functor (f : Type -> Type) where

1010 ||| @ m the morphism

1111 map : (m : a -> b) -> f a -> f b

1212

13+infixl 4 <$>

14+

15+||| An infix alias for `map`: the action of a functor on morphisms.

16+||| @ f the functor

17+||| @ m the morphism

18+(<$>) : Functor f => (m : a -> b) -> f a -> f b

19+m <$> x = map m x

20+

1321class Functor f => VerifiedFunctor (f : Type -> Type) where

1422 functorIdentity : {a : Type} -> (x : f a) -> map id x = id x

1523 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->

libs/prelude/Prelude/Monad.idr+1−1

@@ -16,7 +16,7 @@ class Applicative m => Monad (m : Type -> Type) where

1616

1717class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where

1818 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->

19− mf <$> mx = mf >>= \f =>

19+ mf <*> mx = mf >>= \f =>

2020 mx >>= \x =>

2121 pure (f x)

2222 monadLeftIdentity : (x : a) -> (f : a -> m b) -> return x >>= f = f x

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

@@ -267,6 +268,7 @@ instance BoundedJoinSemilattice Nat where

267268 bottom = Z

268269

269270

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

270272instance Cast Int Nat where

271273 cast i = fromInteger (cast i)

272274

@@ -350,7 +352,7 @@ lcm x y = divNat (x * y) (gcd x y)

350352

351353

352354--------------------------------------------------------------------------------

353−-- An informative comparison view

355+-- An informative comparison view

354356--------------------------------------------------------------------------------

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

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

libs/prelude/Prelude/Stream.idr+1−1

@@ -111,7 +111,7 @@ scanr f (x :: xs) = f x (foldr f xs) :: scanr f xs

111111

112112instance Applicative Stream where

113113 pure = repeat

114− (<$>) = zipWith apply

114+ (<*>) = zipWith apply

115115

116116instance Monad Stream where

117117 s >>= f = diag (map f s)

libs/prelude/Prelude/Traversable.idr+2−2

@@ -8,10 +8,10 @@ import Prelude.Foldable

88import Prelude.Functor

99

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

11−traverse_ f = foldr (($>) . f) (pure ())

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

1212

1313sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()

14−sequence_ = foldr ($>) (pure ())

14+sequence_ = foldr (*>) (pure ())

1515

1616for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()

1717for_ = flip traverse_

rts/idris_gc.c+4−8

@@ -17,7 +17,6 @@ VAL copy(VM* vm, VAL x) {

1717 } else {

1818 allocCon(cl, vm, CTAG(x), ar, 1);

1919 for(i = 0; i < ar; ++i) {

20− // *argptr = copy(vm, *((VAL*)(x->info.c.args)+i)); // recursive version

2120 cl->info.c.args[i] = x->info.c.args[i];

2221 }

2322 }

@@ -90,9 +89,7 @@ void cheney(VM *vm) {

9089 case CON:

9190 ar = ARITY(heap_item);

9291 for(i = 0; i < ar; ++i) {

93− // printf("Copying %d %p\n", heap_item->info.c.tag, *argptr);

9492 VAL newptr = copy(vm, heap_item->info.c.args[i]);

95− // printf("Got %p\t\t%p %p\n", newptr, scan, vm->heap_next);

9693 heap_item->info.c.args[i] = newptr;

9794 }

9895 break;

@@ -111,7 +108,6 @@ void cheney(VM *vm) {

111108void idris_gc(VM* vm) {

112109 HEAP_CHECK(vm)

113110 STATS_ENTER_GC(vm->stats, vm->heap.size)

114− // printf("Collecting\n");

115111

116112 if (vm->heap.old != NULL)

117113 free(vm->heap.old);

@@ -162,13 +158,13 @@ void idris_gc(VM* vm) {

162158

163159void idris_gcInfo(VM* vm, int doGC) {

164160 printf("Stack: <BOT %p> <TOP %p>\n", vm->valstack, vm->valstack_top);

165− printf("Final heap size %d\n", (int)(vm->heap.size));

166− printf("Final heap use %d\n", (int)(vm->heap.next - vm->heap.heap));

161+ printf("Final heap size %zd\n", vm->heap.size);

162+ printf("Final heap use %zd\n", vm->heap.next - vm->heap.heap);

167163 if (doGC) { idris_gc(vm); }

168− printf("Final heap use after GC %d\n", (int)(vm->heap.next - vm->heap.heap));

164+ printf("Final heap use after GC %zd\n", vm->heap.next - vm->heap.heap);

169165#ifdef IDRIS_ENABLE_STATS

170166 printf("Total allocations %" PRIu64 "\n", vm->stats.allocations);

171167#endif

172− printf("Number of collections %d\n", vm->stats.collections);

168+ printf("Number of collections %" PRIu32 "\n", vm->stats.collections);

173169

174170}

rts/idris_heap.c+2−2

@@ -10,8 +10,8 @@ void alloc_heap(Heap * h, size_t heap_size)

1010 char * mem = malloc(heap_size);

1111 if (mem == NULL) {

1212 fprintf(stderr,

13− "RTS ERROR: Unable to allocate heap. Requested %d bytes.\n",

14− (int)heap_size);

13+ "RTS ERROR: Unable to allocate heap. Requested %zd bytes.\n",

14+ heap_size);

1515 exit(EXIT_FAILURE);

1616 }

1717

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+6−1

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

@@ -162,7 +167,7 @@ typedef void(*func)(VM*, VAL*);

162167#define SETTY(x,t) (x)->ty = (((x)->ty & 0xffff0000) | (t))

163168

164169#define GETHEAP(x) ((x)->ty >> 16)

165−#define SETHEAP(x,y) (x)->ty = (((x)->ty & 0x0000ffff) | ((t) << 16))

170+#define SETHEAP(x,y) (x)->ty = (((x)->ty & 0x0000ffff) | ((y) << 16))

166171

167172// Integers, floats and operators

168173

rts/idris_stats.h+2−1

@@ -3,9 +3,10 @@

33

44#ifdef IDRIS_ENABLE_STATS

55#include <time.h>

6+#endif

7+

68#include <inttypes.h>

79#include <stdint.h>

8−#endif

910

1011

1112// TODO: measure user time, exclusive/inclusive stats

samples/interp.idr+2−2

@@ -37,8 +37,8 @@ using (G : Vect n Ty)

3737 index_first = stop

3838 index_next = pop

3939

40− (<$>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

41− (<$>) = \f, a => App f a

40+ (<*>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

41+ (<*>) = \f, a => App f a

4242

4343 pure : Expr G a -> Expr G a

4444 pure = id

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+26−16

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

@@ -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+39−30

@@ -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).

@@ -336,6 +338,8 @@ data Codegen = Via String

336338deriving instance NFData Codegen

337339!-}

338340

341+data HowMuchDocs = FullDocs | OverviewDocs

342+

339343-- | REPL commands

340344data Command = Quit

341345 | Help

@@ -343,7 +347,7 @@ data Command = Quit

343347 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.

344348 | Undefine [Name]

345349 | Check PTerm

346− | DocStr (Either Name Const)

350+ | DocStr (Either Name Const) HowMuchDocs

347351 | TotCheck Name

348352 | Reload

349353 | Load FilePath (Maybe Int) -- up to maximum line number

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

417421 | NoREPL

418422 | OLogging Int

419423 | Output String

424+ | Interface

420425 | TypeCase

421426 | TypeInType

422427 | DefaultTotal

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

596601 [PDecl' t] -- declarations

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

598603 -- class name, parameters, method declarations

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

600− Name -- class

601− [t] -- parameters

602− t -- full instance type

603− (Maybe Name) -- explicit name

604− [PDecl' t]

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

606− -- 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

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

608618 | PSyntax FC Syntax -- ^ Syntax definition

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

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

611− | 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

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

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

614624 deriving Functor

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

683693declared (PNamespace _ ds) = concatMap declared ds

684694declared (PRecord _ _ _ n _ _ _ (Just c) _ _) = [n, c]

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

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

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

687697declared (PDSL n _) = [n]

688698declared (PSyntax _ _) = []

689699declared (PMutual _ ds) = concatMap declared ds

@@ -703,7 +713,7 @@ tldeclared (PParams _ _ ds) = []

703713tldeclared (PMutual _ ds) = concatMap tldeclared ds

704714tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

707717tldeclared _ = []

708718

709719defined :: PDecl -> [Name]

@@ -719,7 +729,7 @@ defined (PParams _ _ ds) = concatMap defined ds

719729defined (PNamespace _ ds) = concatMap defined ds

720730defined (PRecord _ _ _ n _ _ _ (Just c) _ _) = [n, c]

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

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

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

723733defined (PDSL n _) = [n]

724734defined (PSyntax _ _) = []

725735defined (PMutual _ ds) = concatMap defined ds

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

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

775785 | PHidden PTerm -- ^ Irrelevant or hidden pattern

776786 | PType -- ^ 'Type' type

777− | PUniverse Universe -- ^ Some universe

787+ | PUniverse Universe -- ^ Some universe

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

779789 | PConstant Const -- ^ Builtin types

780790 | Placeholder -- ^ Underscore

@@ -1109,7 +1119,7 @@ data SSymbol = Keyword Name

11091119 | Expr Name

11101120 | SimpleExpr Name

11111121 deriving (Show, Eq)

1112−

1122+

11131123

11141124{-!

11151125deriving instance Binary SSymbol

@@ -1158,7 +1168,7 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules

11581168

11591169initDSL = DSL (PRef f (sUN ">>="))

11601170 (PRef f (sUN "return"))

1161− (PRef f (sUN "<$>"))

1171+ (PRef f (sUN "<*>"))

11621172 (PRef f (sUN "pure"))

11631173 Nothing

11641174 Nothing

@@ -1384,7 +1394,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

13841394 where

13851395 startPrec = 0

13861396 funcAppPrec = 10

1387−

1397+

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

13891399 prettySe p bnd (PQuote r) =

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

@@ -1447,7 +1457,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

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

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

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

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

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

14511461 bracket p funcAppPrec $

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

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

@@ -1463,7 +1473,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

14631473 Just (Infixr p') -> p'

14641474 Just f' -> prec f' + 1

14651475 inFix l r = align . group $

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

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

14671477 group (prettySe right bnd r)

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

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

@@ -1482,7 +1492,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

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

14831493 indent 2 (vsep (map ppcase cases))

14841494 where

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

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

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

14871497 in nest nestingSize $

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

@@ -1553,7 +1563,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

15531563 prettyAs =

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

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

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

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

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

15581568 -- XXX: add pretty for tactics

15591569 prettySe p bnd (PProof ts) =

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

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

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

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

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

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

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

17301740showDeclImp _ _ = text "..."

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

@@ -1901,16 +1911,16 @@ implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

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

19021912 where

19031913 ni env (PRef _ n)

1904− | not (n `elem` env)

1914+ | not (n `elem` env)

19051915 = case lookupTy n (tt_ctxt ist) of

19061916 [] -> [n]

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

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

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

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

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

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

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

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

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

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

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

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

@@ -1940,7 +1950,7 @@ namesIn uvars ist tm = nub $ ni [] tm

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

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

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

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

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

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

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

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

@@ -1999,4 +2009,3 @@ getErasureInfo ist n =

19992009 case lookupCtxtExact n (idris_optimisation ist) of

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

20012011 Nothing -> []

2002−

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/Elaborate.hs−7

@@ -28,13 +28,6 @@ import Debug.Trace

2828

2929import Util.Pretty hiding (fill)

3030

31−-- I don't really want this here, but it's useful for the test shell

32−data Command = Theorem Name Raw

33− | Eval Raw

34− | Quit

35− | Print Name

36− | Tac (Elab ())

37−

3831data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))

3932 deriving Show

4033

src/Idris/DSL.hs+40−8

@@ -2,6 +2,8 @@

22

33module Idris.DSL where

44

5+import Data.Generics.Uniplate.Data (transform)

6+

57import Idris.AbsSyntax

68

79import Idris.Core.TT

@@ -13,25 +15,55 @@ import Debug.Trace

1315debindApp :: SyntaxInfo -> PTerm -> PTerm

1416debindApp syn t = debind (dsl_bind (dsl_info syn)) t

1517

18+dslify :: SyntaxInfo -> IState -> PTerm -> PTerm

19+dslify syn i = transform dslifyApp

20+ where

21+ dslifyApp (PApp fc (PRef _ f) [a])

22+ | [d] <- lookupCtxt f (idris_dsls i)

23+ = desugar (syn { dsl_info = d }) i (getTm a)

24+ dslifyApp t = t

25+

1626desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

17−desugar syn i t = let t' = expandDo (dsl_info syn) t in

18− t' -- addImpl i t'

27+desugar syn i t = let t' = expandDo (dsl_info syn) t

28+ in dslify syn i t'

29+

30+mkTTName :: FC -> Name -> PTerm

31+mkTTName fc n =

32+ let mkList fc [] = PRef fc (sNS (sUN "Nil") ["List", "Prelude"])

33+ mkList fc (x:xs) = PApp fc (PRef fc (sNS (sUN "::") ["List", "Prelude"]))

34+ [ pexp (stringC x)

35+ , pexp (mkList fc xs)]

36+ stringC = PConstant . Str . str

37+ intC = PConstant . I

38+ reflm n = sNS (sUN n) ["Reflection", "Language"]

39+ in case n of

40+ UN nm -> PApp fc (PRef fc (reflm "UN")) [ pexp (stringC nm)]

41+ NS nm ns -> PApp fc (PRef fc (reflm "NS")) [ pexp (mkTTName fc nm)

42+ , pexp (mkList fc ns)]

43+ MN i nm -> PApp fc (PRef fc (reflm "MN")) [ pexp (intC i)

44+ , pexp (stringC nm)]

45+ otherwise -> PRef fc $ reflm "NErased"

1946

2047expandDo :: DSL -> PTerm -> PTerm

2148expandDo dsl (PLam fc n ty tm)

2249 | Just lam <- dsl_lambda dsl

23− = let sc = PApp fc lam [pexp (var dsl n tm 0)] in

24− expandDo dsl sc

50+ = let sc = PApp fc lam [ pexp (mkTTName fc n)

51+ , pexp (var dsl n tm 0)]

52+ in expandDo dsl sc

2553expandDo dsl (PLam fc n ty tm) = PLam fc n (expandDo dsl ty) (expandDo dsl tm)

2654expandDo dsl (PLet fc n ty v tm)

2755 | Just letb <- dsl_let dsl

28− = let sc = PApp (fileFC "(dsl)") letb [pexp v, pexp (var dsl n tm 0)] in

29− expandDo dsl sc

56+ = let sc = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)

57+ , pexp v

58+ , pexp (var dsl n tm 0)]

59+ in expandDo dsl sc

3060expandDo dsl (PLet fc n ty v tm) = PLet fc n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)

3161expandDo dsl (PPi p n ty tm)

3262 | Just pi <- dsl_pi dsl

33− = let sc = PApp (fileFC "(dsl)") pi [pexp ty, pexp (var dsl n tm 0)] in

34− expandDo dsl sc

63+ = let sc = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)

64+ , pexp ty

65+ , pexp (var dsl n tm 0)]

66+ in expandDo dsl sc

3567expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

3668expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

3769 (map (fmap (expandDo dsl)) args)

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/Docs.hs+89−39

@@ -1,12 +1,12 @@

1−{-# LANGUAGE PatternGuards #-}

2−module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc(..), Docs (..)) where

1+{-# LANGUAGE DeriveFunctor, PatternGuards #-}

2+module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc, FunDoc'(..), Docs, Docs'(..)) where

33

44import Idris.AbsSyntax

55import Idris.AbsSyntaxTree

66import Idris.Delaborate

77import Idris.Core.TT

88import Idris.Core.Evaluate

9−import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, renderDocstring, DocTerm, renderDocTerm)

9+import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, renderDocstring, DocTerm, renderDocTerm, overview)

1010

1111import Util.Pretty

1212

@@ -18,21 +18,28 @@ import qualified Data.Text as T

1818--

1919-- Issue #1573 on the Issue tracker.

2020-- https://github.com/idris-lang/Idris-dev/issues/1573

21−data FunDoc = FD Name (Docstring DocTerm)

22− [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))] -- args: name, ty, implicit, docs

23− PTerm -- function type

24− (Maybe Fixity)

25−

26−data Docs = FunDoc FunDoc

27− | DataDoc FunDoc -- type constructor docs

28− [FunDoc] -- data constructor docs

29− | ClassDoc Name (Docstring DocTerm)-- class docs

30− [FunDoc] -- method docs

31− [(Name, Maybe (Docstring DocTerm))] -- parameters and their docstrings

32− [PTerm] -- instances

33− [PTerm] -- superclasses

34− | ModDoc [String] -- Module name

35− (Docstring DocTerm)

21+data FunDoc' d = FD Name d

22+ [(Name, PTerm, Plicity, Maybe d)] -- args: name, ty, implicit, docs

23+ PTerm -- function type

24+ (Maybe Fixity)

25+ deriving Functor

26+

27+type FunDoc = FunDoc' (Docstring DocTerm)

28+

29+data Docs' d = FunDoc (FunDoc' d)

30+ | DataDoc (FunDoc' d) -- type constructor docs

31+ [FunDoc' d] -- data constructor docs

32+ | ClassDoc Name d -- class docs

33+ [FunDoc' d] -- method docs

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

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

36+ [PTerm] -- subclasses

37+ [PTerm] -- superclasses

38+ | ModDoc [String] -- Module name

39+ d

40+ deriving Functor

41+

42+type Docs = Docs' (Docstring DocTerm)

3643

3744showDoc ist d

3845 | nullDocstring d = empty

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

8289 if null args then text "No constructors."

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

8491 vsep (map (pprintFD ist) args))

85−pprintDocs ist (ClassDoc n doc meths params instances superclasses)

92+pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)

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

8794 if nullDocstring doc

8895 then empty

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

94101 vsep (map (pprintFD ist) meths))

95102 <$>

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

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

98− else map dumpInstance instances'))

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

105+ else map pprintInstance instances))

99106 <>

100107 (if null subclasses then empty

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

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

112119 ppo = ppOptionIst ist

113120 infixes = idris_infixes ist

114121

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+

115146 dumpInstance :: PTerm -> Doc OutputAnnotation

116147 dumpInstance = pprintPTerm ppo params' [] infixes

117148

@@ -134,33 +165,38 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

134165 isSubclass (PPi _ _ _ pt) = isSubclass pt

135166 isSubclass _ = False

136167

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

138−

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

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

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

142172

143173pprintDocs ist (ModDoc mod docs)

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

145175 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) docs

146176

177+-- | Determine a truncation function depending how much docs the user

178+-- wants to see

179+howMuch FullDocs = id

180+howMuch OverviewDocs = overview

181+

147182-- | Given a fully-qualified, disambiguated name, construct the

148183-- documentation object for it

149−getDocs :: Name -> Idris Docs

150−getDocs n@(NS n' ns) | n' == modDocName

184+getDocs :: Name -> HowMuchDocs -> Idris Docs

185+getDocs n@(NS n' ns) w | n' == modDocName

151186 = do i <- getIState

152187 case lookupCtxtExact n (idris_moduledocs i) of

153− Just doc -> return $ ModDoc (reverse (map T.unpack ns)) doc

188+ Just doc -> return . ModDoc (reverse (map T.unpack ns)) $ howMuch w doc

154189 Nothing -> fail $ "Module docs for " ++ show (reverse (map T.unpack ns)) ++

155190 " do not exist! This shouldn't have happened and is a bug."

156−getDocs n

191+getDocs n w

157192 = do i <- getIState

158− case lookupCtxt n (idris_classes i) of

159− [ci] -> docClass n ci

160− _ -> case lookupCtxt n (idris_datatypes i) of

161− [ti] -> docData n ti

162− _ -> do fd <- docFun n

163− return (FunDoc fd)

193+ docs <- case lookupCtxt n (idris_classes i) of

194+ [ci] -> docClass n ci

195+ _ -> case lookupCtxt n (idris_datatypes i) of

196+ [ti] -> docData n ti

197+ _ -> do fd <- docFun n

198+ return (FunDoc fd)

199+ return $ fmap (howMuch w) docs

164200

165201docData :: Name -> TypeInfo -> Idris Docs

166202docData n ti

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

174210 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

175211 docstr = maybe emptyDocstring fst docStrings

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

177− 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

178219 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

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

180− return $ ClassDoc n docstr mdocs params instances superclasses

221+ return $ ClassDoc

222+ n docstr mdocs params

223+ instances' (map fst subclasses) superclasses

181224 where

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

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

183226 getDInst _ = Nothing

184227

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+

185235docFun :: Name -> Idris FunDoc

186236docFun n

187237 = 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/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/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 args 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+41−24

@@ -1066,7 +1066,7 @@ elab ist info emode opts fn tm

10661066 delayElab $ do focus h

10671067 dotterm

10681068 elab' ina fc t

1069− elab' ina _ (PRunTactics fc tm) =

1069+ elab' ina fc (PRunTactics fc' tm) =

10701070 do attack

10711071 n <- getNameFrom (sMN 0 "tacticScript")

10721072 n' <- getNameFrom (sMN 0 "tacticExpr")

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

10751075 movelast n

10761076 letbind n' scriptTy (Var n)

10771077 focus n

1078− elab' ina (Just fc) tm

1078+ elab' ina (Just fc') tm

10791079 env <- get_env

10801080 ctxt <- get_context

1081− runTactical fc ctxt env (P Bound n' Erased)

1081+ runTactical (maybe fc' id fc) ctxt env (P Bound n' Erased)

10821082 solve

10831083 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

10841084

@@ -1508,7 +1508,7 @@ case_ ind autoSolve ist fn tm = do

15081508runTactical :: FC -> Context -> Env -> Term -> ElabD ()

15091509runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

15101510 where

1511− eval = normaliseAll ctxt env

1511+ eval = normaliseAll ctxt env . finalise

15121512 tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]

15131513 returnUnit = fmap fst $ get_type_val (Var unitCon)

15141514

@@ -1540,6 +1540,9 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

15401540 else fmap fst . get_type_val $

15411541 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))

15421542 (Var (reflm "TT"))

1543+ | n == tacN "prim__SourceLocation", [] <- args

1544+ = fmap fst . get_type_val $

1545+ reflectFC fc

15431546 | n == tacN "prim__Env", [] <- args

15441547 = do env <- get_env

15451548 fmap fst . get_type_val $ reflectEnv env

@@ -1547,7 +1550,7 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

15471550 = do parts <- reifyReportParts (eval errs)

15481551 lift . tfail $ ReflectionError [parts] (Msg "")

15491552 | n == tacN "prim__PureTactical", [_a, tm] <- args

1550− = return tm

1553+ = return tm

15511554 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args

15521555 = do let first' = eval first

15531556 res <- runTacTm first'

@@ -1575,6 +1578,10 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

15751578 | n == tacN "prim__Attack", [] <- args

15761579 = do attack

15771580 returnUnit

1581+ | n == tacN "prim__Rewrite", [rule] <- args

1582+ = do r <- reifyRaw rule

1583+ rewrite r

1584+ returnUnit

15781585 | n == tacN "prim__Focus", [what] <- args

15791586 = do n' <- reifyTTName what

15801587 focus n'

@@ -1583,6 +1590,12 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

15831590 = do n' <- reifyTTName what

15841591 movelast n'

15851592 returnUnit

1593+ | n == tacN "prim__Intro", [mn] <- args

1594+ = do n <- case fromTTMaybe mn of

1595+ Nothing -> return Nothing

1596+ Just name -> fmap Just $ reifyTTName name

1597+ intro n

1598+ returnUnit

15861599 runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x

15871600

15881601-- Running tactics directly

@@ -1829,22 +1842,7 @@ runTac autoSolve ist perhapsFC fn tac

18291842 case perhapsFC of

18301843 Nothing -> lift . tfail $ Msg "There is no source location available."

18311844 Just fc ->

1832− do let intTy = RConstant (AType (ATInt ITNative))

1833− fill $ raw_apply (Var (reflm "FileLoc"))

1834− [ RConstant (Str (fc_fname fc))

1835− , raw_apply (Var pairCon) $

1836− [intTy, intTy] ++

1837− map (RConstant . I)

1838− [ fst (fc_start fc)

1839− , snd (fc_start fc)

1840− ]

1841− , raw_apply (Var pairCon) $

1842− [intTy, intTy] ++

1843− map (RConstant . I)

1844− [ fst (fc_end fc)

1845− , snd (fc_end fc)

1846− ]

1847− ]

1845+ do fill $ reflectFC fc

18481846 solve

18491847 runT x = fail $ "Not implemented " ++ show x

18501848

@@ -1966,7 +1964,7 @@ reifyRaw t@(App _ _)

19661964 | (P _ f _, args) <- unApply t = reifyRawApp f args

19671965reifyRaw t@(P _ n _)

19681966 | n == reflm "RType" = return $ RType

1969−reifyRaw t = fail ("Unknown reflection raw term: " ++ show t)

1967+reifyRaw t = fail ("Unknown reflection raw term in reifyRaw: " ++ show t)

19701968

19711969reifyRawApp :: Name -> [Term] -> ElabD Raw

19721970reifyRawApp t [n]

@@ -1982,7 +1980,7 @@ reifyRawApp t [t']

19821980 | t == reflm "RForce" = liftM RForce (reifyRaw t')

19831981reifyRawApp t [c]

19841982 | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)

1985−reifyRawApp t args = fail ("Unknown reflection raw term: " ++ show (t, args))

1983+reifyRawApp t args = fail ("Unknown reflection raw term in reifyRawApp: " ++ show (t, args))

19861984

19871985reifyTTName :: Term -> ElabD Name

19881986reifyTTName t

@@ -2602,7 +2600,7 @@ reflectErr (NotInjective t1 t2 t3) =

26022600reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

26032601reflectErr (CantResolveAlts ss) =

26042602 raw_apply (Var $ reflErrName "CantResolveAlts")

2605− [rawList (Var $ (sUN "String")) (map Var ss)]

2603+ [rawList (Var $ reflm "TTName") (map reflectName ss)]

26062604reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

26072605reflectErr UniverseError = Var $ reflErrName "UniverseError"

26082606reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

@@ -2617,6 +2615,25 @@ reflectErr (LoadingFailed str err) =

26172615 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]

26182616reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]

26192617

2618+-- | Reflect a file context

2619+reflectFC :: FC -> Raw

2620+reflectFC fc = raw_apply (Var (reflm "FileLoc"))

2621+ [ RConstant (Str (fc_fname fc))

2622+ , raw_apply (Var pairCon) $

2623+ [intTy, intTy] ++

2624+ map (RConstant . I)

2625+ [ fst (fc_start fc)

2626+ , snd (fc_start fc)

2627+ ]

2628+ , raw_apply (Var pairCon) $

2629+ [intTy, intTy] ++

2630+ map (RConstant . I)

2631+ [ fst (fc_end fc)

2632+ , snd (fc_end fc)

2633+ ]

2634+ ]

2635+ where intTy = RConstant (AType (ATInt ITNative))

2636+

26202637elaboratingArgErr :: [(Name, Name)] -> Err -> Err

26212638elaboratingArgErr [] err = err

26222639elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)

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+54−38

@@ -37,7 +37,7 @@ import Codec.Compression.Zlib (compress)

3737import Util.Zlib (decompressEither)

3838

3939ibcVersion :: Word8

40−ibcVersion = 98

40+ibcVersion = 99

4141

4242data IBCFile = IBCFile { ver :: Word8,

4343 sourcefile :: FilePath,

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

@@ -1240,15 +1249,18 @@ instance (Binary t) => Binary (PDecl' t) where

12401249 put x6

12411250 put x7

12421251 put x8

1243− PInstance x1 x2 x3 x4 x5 x6 x7 x8 -> do putWord8 8

1244− put x1

1245− put x2

1246− put x3

1247− put x4

1248− put x5

1249− put x6

1250− put x7

1251− put x8

1252+ PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

1253+ do putWord8 8

1254+ put x1

1255+ put x2

1256+ put x3

1257+ put x4

1258+ put x5

1259+ put x6

1260+ put x7

1261+ put x8

1262+ put x9

1263+ put x10

12521264 PDSL x1 x2 -> do putWord8 9

12531265 put x1

12541266 put x2

@@ -1271,16 +1283,18 @@ instance (Binary t) => Binary (PDecl' t) where

12711283 put x1

12721284 put x2

12731285 PDirective x1 -> error "Cannot serialize PDirective"

1274− PProvider x1 x2 x3 x4 -> do putWord8 15

1275− put x1

1276− put x2

1277− put x3

1278− put x4

1286+ PProvider x1 x2 x3 x4 x5 ->

1287+ do putWord8 15

1288+ put x1

1289+ put x2

1290+ put x3

1291+ put x4

1292+ put x5

12791293 PTransform x1 x2 x3 x4 -> do putWord8 16

12801294 put x1

12811295 put x2

12821296 put x3

1283− put x4

1297+ put x4

12841298 get

12851299 = do i <- getWord8

12861300 case i of

@@ -1343,7 +1357,9 @@ instance (Binary t) => Binary (PDecl' t) where

13431357 x6 <- get

13441358 x7 <- get

13451359 x8 <- get

1346− return (PInstance x1 x2 x3 x4 x5 x6 x7 x8)

1360+ x9 <- get

1361+ x10 <- get

1362+ return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

13471363 9 -> do x1 <- get

13481364 x2 <- get

13491365 return (PDSL x1 x2)

@@ -1369,7 +1385,8 @@ instance (Binary t) => Binary (PDecl' t) where

13691385 x2 <- get

13701386 x3 <- get

13711387 x4 <- get

1372− return (PProvider x1 x2 x3 x4)

1388+ x5 <- get

1389+ return (PProvider x1 x2 x3 x4 x5)

13731390 16 -> do x1 <- get

13741391 x2 <- get

13751392 x3 <- get

@@ -2191,4 +2208,3 @@ instance Binary Codegen where

21912208 return (Via x1)

21922209 1 -> return Bytecode

21932210 _ -> error "Corrupted binary data for Codegen"

2194−

src/Idris/IdeMode.hs+8−3

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

22

33{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}

44

5−module Idris.IdeMode(parseMessage, convSExp, IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar) where

5+module Idris.IdeMode(parseMessage, convSExp, WhatDocs(..), IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar) where

66

77import Text.Printf

88import Numeric

@@ -206,6 +206,8 @@ parseSExp = parseString pSExp (Directed (UTF8.fromString "(unknown)") 0 0 0 0)

206206

207207data Opt = ShowImpl | ErrContext deriving Show

208208

209+data WhatDocs = Overview | Full

210+

209211data IdeModeCommand = REPLCompletions String

210212 | Interpret String

211213 | TypeOf String

@@ -217,7 +219,7 @@ data IdeModeCommand = REPLCompletions String

217219 | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth

218220 | MakeLemma Int String

219221 | LoadFile String (Maybe Int)

220− | DocsFor String

222+ | DocsFor String WhatDocs

221223 | Apropos String

222224 | GetOpts

223225 | SetOpt Opt Bool

@@ -258,7 +260,10 @@ sexpToCommand (SexpList (SymbolAtom "proof-search" : IntegerAtom line : StringAt

258260 _ -> Nothing)

259261sexpToCommand (SexpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom name]) = Just (MakeLemma (fromInteger line) name)

260262sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint] Nothing)

261−sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)

263+sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name Full)

264+sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name, SymbolAtom s])

265+ | Just w <- lookup s opts = Just (DocsFor name w)

266+ where opts = [("overview", Overview), ("full", Full)]

262267sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)

263268sexpToCommand (SymbolAtom "get-options") = Just GetOpts

264269sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])

src/Idris/IdrisDoc.hs+6−6

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

@@ -273,7 +273,7 @@ loadDocs :: IState -- ^ IState to extract infomation from

273273 -> Name -- ^ Name to load Docs for

274274 -> IO (Maybe Docs)

275275loadDocs ist n

276− | mayHaveDocs n = do docs <- runExceptT $ evalStateT (getDocs n) ist

276+ | mayHaveDocs n = do docs <- runExceptT $ evalStateT (getDocs n FullDocs) ist

277277 case docs of Right d -> return (Just d)

278278 Left _ -> return Nothing

279279 | otherwise = return Nothing

@@ -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/Imports.hs+22−6

@@ -44,7 +44,7 @@ ibcPath ibcsd use_ibcsd fp = let (d_fp, n_fp) = splitFileName fp

4444

4545ibcPathWithFallback :: FilePath -> FilePath -> IO FilePath

4646ibcPathWithFallback ibcsd fp = do let ibcp = ibcPath ibcsd True fp

47− ibc <- doesFileExist ibcp

47+ ibc <- doesFileExist' ibcp

4848 return (if ibc

4949 then ibcp

5050 else ibcPath ibcsd False fp)

@@ -58,9 +58,9 @@ findImport (d:ds) ibcsd fp = do let fp_full = d </> fp

5858 ibcp <- runIO $ ibcPathWithFallback ibcsd fp_full

5959 let idrp = srcPath fp_full

6060 let lidrp = lsrcPath fp_full

61− ibc <- runIO $ doesFileExist ibcp

62− idr <- runIO $ doesFileExist idrp

63− lidr <- runIO $ doesFileExist lidrp

61+ ibc <- runIO $ doesFileExist' ibcp

62+ idr <- runIO $ doesFileExist' idrp

63+ lidr <- runIO $ doesFileExist' lidrp

6464-- when idr $ putStrLn $ idrp ++ " ok"

6565-- when lidr $ putStrLn $ lidrp ++ " ok"

6666-- when ibc $ putStrLn $ ibcp ++ " ok"

@@ -78,7 +78,7 @@ findImport (d:ds) ibcsd fp = do let fp_full = d </> fp

7878findInPath :: [FilePath] -> FilePath -> IO FilePath

7979findInPath [] fp = fail $ "Can't find file " ++ fp

8080findInPath (d:ds) fp = do let p = d </> fp

81− e <- doesFileExist p

81+ e <- doesFileExist' p

8282 if e then return p else findInPath ds fp

8383

8484findPkgIndex :: String -> Idris FilePath

@@ -94,10 +94,26 @@ installedPackages = do

9494 where

9595 allFilesInDir base fp = do

9696 let fullpath = base </> fp

97− isDir <- doesDirectoryExist fullpath

97+ isDir <- doesDirectoryExist' fullpath

9898 if isDir

9999 then fmap concat (mapM (allFilesInDir fullpath) =<< dirContents fullpath)

100100 else return [fp]

101101 dirContents = fmap (filter (not . (`elem` [".", ".."]))) . getDirectoryContents

102102 goodDir idir d = any (".ibc" `isSuffixOf`) <$> allFilesInDir idir d

103103

104+

105+-- Case sensitive file existence check for Mac OS X.

106+doesFileExist' :: FilePath -> IO Bool

107+doesFileExist' = caseSensitive doesFileExist

108+

109+-- Case sensitive directory existence check for Mac OS X.

110+doesDirectoryExist' :: FilePath -> IO Bool

111+doesDirectoryExist' = caseSensitive doesDirectoryExist

112+

113+caseSensitive :: (FilePath -> IO Bool) -> FilePath -> IO Bool

114+caseSensitive existsCheck name =

115+ do exists <- existsCheck name

116+ if exists

117+ then do contents <- getDirectoryContents (takeDirectory name)

118+ return $ (takeFileName name) `elem` contents

119+ else return False

src/Idris/ParseExpr.hs+4−8

@@ -554,14 +554,8 @@ app syn = do f <- simpleExpr syn

554554 args <- many (do notEndApp; arg syn)

555555 case args of

556556 [] -> return f

557− _ -> return (dslify i (PApp fc f args)))

557+ _ -> return (PApp fc f args))

558558 <?> "function application"

559− where

560− dslify :: IState -> PTerm -> PTerm

561− dslify i (PApp fc (PRef _ f) [a])

562− | [d] <- lookupCtxt f (idris_dsls i)

563− = desugar (syn { dsl_info = d }) i (getTm a)

564− dslify i t = t

565559

566560{-| Parses a function argument

567561@

@@ -878,7 +872,9 @@ pi syn =

878872 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)) <|> (do

879873 try (lchar '{' *> reserved "default")

880874 when (st == Static) $ fail "default tactic constraints can not be static"

881− script <- simpleExpr syn

875+ ist <- get

876+ script' <- simpleExpr syn

877+ let script = debindApp syn . desugar syn ist $ script'

882878 xt <- typeDeclList syn

883879 lchar '}'

884880 symbol "->"

src/Idris/ParseHelpers.hs+11−4

@@ -119,7 +119,7 @@ singleLineComment :: MonadicParsing m => m ()

119119singleLineComment = (string "--" *>

120120 many (satisfy (not . isEol)) *>

121121 eol *> pure ())

122− <?> "single-line comment"

122+ <?> ""

123123

124124{- | Consumes a multi-line comment

125125

@@ -321,10 +321,17 @@ opChars = ":!#$%&*+./<=>?@\\^|-~"

321321operatorLetter :: MonadicParsing m => m Char

322322operatorLetter = oneOf opChars

323323

324+

325+commentMarkers :: [String]

326+commentMarkers = [ "--", "|||" ]

327+

328+invalidOperators :: [String]

329+invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!"]

330+

324331-- | Parses an operator

325332operator :: MonadicParsing m => m String

326333operator = do op <- token . some $ operatorLetter

327− when (op `elem` [":", "=>", "->", "<-", "=", "?=", "|"]) $

334+ when (op `elem` (invalidOperators ++ commentMarkers)) $

328335 fail $ op ++ " is not a valid operator"

329336 return op

330337

@@ -580,7 +587,7 @@ collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

580587collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

581588collect (PClass doc f s cs n ps pdocs ds : ds')

582589 = PClass doc f s cs n ps pdocs (collect ds) : collect ds'

583−collect (PInstance f s cs n ps t en ds : ds')

584− = 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'

585592collect (d : ds) = d : collect ds

586593collect [] = []

src/Idris/ParseOps.hs+9−1

@@ -37,7 +37,8 @@ table fixes

3737 toTable (reverse fixes) ++

3838 [[backtick],

3939 [binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],

40− [binary "=" (\fc x y -> PEq fc Placeholder Placeholder x y) AssocLeft]]

40+ [binary "=" (\fc x y -> PEq fc Placeholder Placeholder x y) AssocLeft],

41+ [nofixityoperator]]

4142 where

4243 flatten :: PTerm -> PTerm -- flatten application

4344 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

@@ -80,6 +81,13 @@ backtick = Infix (do indentPropHolds gtProp

8081 fc <- getFC

8182 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone

8283

84+-- | Operator without fixity (throws an error)

85+nofixityoperator :: Operator IdrisParser PTerm

86+nofixityoperator = Infix (do indentPropHolds gtProp

87+ op <- try operator

88+ unexpected $ "Operator without known fixity: " ++ op) AssocNone

89+

90+

8391{- | Parses an operator in function position i.e. enclosed by `()', with an

8492 optional namespace

8593

src/Idris/Parser.hs+59−43

@@ -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,6 +291,10 @@ 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

295+ mkSimple' (Expr e : Symbol s : es)

296+ | takeWhile (`elem` opChars) ts /= "" && ts `notElem` invalidOperators = SimpleExpr e : Symbol s : mkSimple' es

297+ where ts = dropWhile isSpace . dropWhileEnd isSpace $ s

294298 mkSimple' (e : es) = e : mkSimple' es

295299 mkSimple' [] = []

296300

@@ -344,13 +348,9 @@ fnDecl' :: SyntaxInfo -> IdrisParser PDecl

344348fnDecl' syn = checkFixity $

345349 do (doc, argDocs, fc, opts', n, acc) <- try (do

346350 pushIndent

347− (doc, argDocs) <- option noDocs docComment

351+ (doc, argDocs) <- docstring syn

348352 ist <- get

349− let doc' = annotCode (tryFullExpr syn ist) doc

350− argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

351− | (n, d) <- argDocs ]

352−

353− initOpts = if default_total ist

353+ let initOpts = if default_total ist

354354 then [TotalFn]

355355 else []

356356 opts <- fnOpts initOpts

@@ -360,7 +360,7 @@ fnDecl' syn = checkFixity $

360360 let n = expandNS syn n_in

361361 fc <- getFC

362362 lchar ':'

363− return (doc', argDocs', fc, opts', n, acc))

363+ return (doc, argDocs, fc, opts', n, acc))

364364 ty <- typeExpr (allowImp syn)

365365 terminator

366366 addAcc n acc

@@ -455,12 +455,10 @@ Postulate ::=

455455@

456456-}

457457postulate :: SyntaxInfo -> IdrisParser PDecl

458−postulate syn = do doc <- try $ do (doc, _) <- option noDocs docComment

459− ist <- get

460− let doc' = annotCode (tryFullExpr syn ist) doc

458+postulate syn = do doc <- try $ do (doc, _) <- docstring syn

461459 pushIndent

462460 reserved "postulate"

463− return doc'

461+ return doc

464462 ist <- get

465463 let initOpts = if default_total ist

466464 then [TotalFn]

@@ -583,7 +581,7 @@ ClassBlock ::=

583581classBlock :: SyntaxInfo -> IdrisParser [PDecl]

584582classBlock syn = do reserved "where"

585583 openBlock

586− ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)

584+ ds <- many (notEndBlock >> instance_ syn <|> fnDecl syn)

587585 closeBlock

588586 return (concat ds)

589587 <?> "class block"

@@ -604,15 +602,14 @@ Class ::=

604602@

605603-}

606604class_ :: SyntaxInfo -> IdrisParser [PDecl]

607−class_ syn = do (doc, argDocs, acc) <- try (do

608− (doc, argDocs) <- option noDocs docComment

609− ist <- get

610− let doc' = annotCode (tryFullExpr syn ist) doc

611− argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

612− | (n, d) <- argDocs ]

613− acc <- optional accessibility

614− return (doc', argDocs', acc))

615− 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

616613 let n = expandNS syn n_in

617614 cs <- many carg

618615 ds <- option [] (classBlock syn)

@@ -630,7 +627,7 @@ class_ syn = do (doc, argDocs, acc) <- try (do

630627

631628@

632629 Instance ::=

633− 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?

630+ DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?

634631 ;

635632@

636633

@@ -639,7 +636,9 @@ InstanceName ::= '[' Name ']';

639636@

640637-}

641638instance_ :: SyntaxInfo -> IdrisParser [PDecl]

642−instance_ syn = do reserved "instance"; fc <- getFC

639+instance_ syn = do (doc, argDocs)

640+ <- try (docstring syn <* reserved "instance")

641+ fc <- getFC

643642 en <- optional instanceName

644643 cs <- constraintList syn

645644 cn <- fnName

@@ -647,7 +646,7 @@ instance_ syn = do reserved "instance"; fc <- getFC

647646 let sc = PApp fc (PRef fc cn) (map pexp args)

648647 let t = bindList (PPi constraint) cs sc

649648 ds <- option [] (instanceBlock syn)

650− return [PInstance syn fc cs cn args t en ds]

649+ return [PInstance doc argDocs syn fc cs cn args t en ds]

651650 <?> "instance declaration"

652651 where instanceName :: IdrisParser Name

653652 instanceName = do lchar '['; n_in <- fnName; lchar ']'

@@ -656,6 +655,18 @@ instance_ syn = do reserved "instance"; fc <- getFC

656655 <?> "instance name"

657656

658657

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+

659670{- | Parses a using declaration list

660671

661672@

@@ -1097,25 +1108,30 @@ totality

10971108{- | Parses a type provider

10981109

10991110@

1100−Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;

1111+Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;

11011112ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'

11021113@

11031114 -}

11041115provider :: SyntaxInfo -> IdrisParser [PDecl]

1105−provider syn = do try (lchar '%' *> reserved "provide");

1106− 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

11071121 <?> "type provider"

1108− where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1109− fc <- getFC

1110− reserved "with"

1111− e <- expr syn <?> "provider expression"

1112− return [PProvider syn fc (ProvTerm t e) n]

1113− providePostulate = do reserved "postulate"

1114− n <- fnName

1115− fc <- getFC

1116− reserved "with"

1117− e <- expr syn <?> "provider expression"

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

11191135

11201136{- | Parses a transform

11211137

@@ -1399,9 +1415,9 @@ loadSource lidr f toline

13991415 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)

14001416 toMutual x = let r = PMutual (fileFC "single mutual") [x] in

14011417 case x of

1402− PClauses _ _ _ _ -> r

1403− PClass _ _ _ _ _ _ _ _ -> r

1404− PInstance _ _ _ _ _ _ _ _ -> r

1418+ PClauses{} -> r

1419+ PClass{} -> r

1420+ PInstance{} -> r

14051421 _ -> x

14061422

14071423 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()

src/Idris/ProofSearch.hs+1−1

@@ -138,7 +138,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

138138 True)

139139 -- if all else fails, make a new metavariable

140140 (if fromProver

141− then cantSolveGoal

141+ then fail "cantSolveGoal"

142142 else do attack; defer [] nroot; solve) True) True

143143

144144 getFn d Nothing = []

src/Idris/Prover.hs+2−2

@@ -202,7 +202,7 @@ receiveInput h e =

202202 receiveInput h e

203203 Just (IdeMode.Interpret cmd) -> return (Just cmd)

204204 Just (IdeMode.TypeOf str) -> return (Just (":t " ++ str))

205− Just (IdeMode.DocsFor str) -> return (Just (":doc " ++ str))

205+ Just (IdeMode.DocsFor str _) -> return (Just (":doc " ++ str))

206206 _ -> return Nothing

207207

208208ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])

@@ -336,7 +336,7 @@ ploop fn d prompt prf e h

336336 return (False, e, False, prf,

337337 Right $ iRenderResult (vsep toShow)))

338338 (\err -> do putIState ist ; ierror err)

339− where showDoc ist (n, d) = do doc <- getDocs n

339+ where showDoc ist (n, d) = do doc <- getDocs n FullDocs

340340 return $ pprintDocs ist doc

341341 docStr (Right c) = do ist <- getIState

342342 return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c))

src/Idris/REPL.hs+27−16

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

@@ -344,13 +345,15 @@ runIdeModeCommand h id orig fn mods (IdeMode.TypeOf name) =

344345 Left err -> iPrintError err

345346 Right n -> process "(idemode)"

346347 (Check (PRef (FC "(idemode)" (0,0) (0,0)) n))

347−runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name) =

348+runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name w) =

348349 case parseConst orig name of

349− Success c -> process "(idemode)" (DocStr (Right c))

350+ Success c -> process "(idemode)" (DocStr (Right c) (howMuch w))

350351 Failure _ ->

351352 case splitName name of

352353 Left err -> iPrintError err

353− Right n -> process "(idemode)" (DocStr (Left n))

354+ Right n -> process "(idemode)" (DocStr (Left n) (howMuch w))

355+ where howMuch IdeMode.Overview = OverviewDocs

356+ howMuch IdeMode.Full = FullDocs

354357runIdeModeCommand h id orig fn mods (IdeMode.CaseSplit line name) =

355358 process fn (CaseSplitAt False line (sUN name))

356359runIdeModeCommand h id orig fn mods (IdeMode.AddClause line name) =

@@ -553,7 +556,7 @@ idemodeProcess fn (Undefine n) = process fn (Undefine n)

553556idemodeProcess fn (ExecVal t) = process fn (ExecVal t)

554557idemodeProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))

555558idemodeProcess fn (Check t) = process fn (Check t)

556−idemodeProcess fn (DocStr n) = process fn (DocStr n)

559+idemodeProcess fn (DocStr n w) = process fn (DocStr n w)

557560idemodeProcess fn Universes = process fn Universes

558561idemodeProcess fn (Defn n) = do process fn (Defn n)

559562 iPrintResult ""

@@ -808,8 +811,8 @@ process fn (NewDefn decls) = do

808811 fixClauses :: PDecl' t -> PDecl' t

809812 fixClauses (PClauses fc opts _ css@(clause:cs)) =

810813 PClauses fc opts (getClauseName clause) css

811− fixClauses (PInstance syn fc constraints cls parms ty instName decls) =

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

813816 fixClauses decl = decl

814817

815818process fn (Undefine names) = undefine names

@@ -905,21 +908,23 @@ process fn (Check t)

905908 _ -> iPrintTermWithType (pprintDelab ist tm)

906909 (pprintDelab ist ty)

907910

908−process fn (DocStr (Left n))

911+process fn (DocStr (Left n) w)

909912 = do ist <- getIState

910913 let docs = lookupCtxtName n (idris_docstrings ist) ++

911− map (\(n,d)-> (n, (d,[]))) (lookupCtxtName (modDocN n) (idris_moduledocs ist))

914+ map (\(n,d)-> (n, (d, [])))

915+ (lookupCtxtName (modDocN n) (idris_moduledocs ist))

912916 case docs of

913917 [] -> iPrintError $ "No documentation for " ++ show n

914918 ns -> do toShow <- mapM (showDoc ist) ns

915919 iRenderResult (vsep toShow)

916− where showDoc ist (n, d) = do doc <- getDocs n

920+ where showDoc ist (n, d) = do doc <- getDocs n w

917921 return $ pprintDocs ist doc

922+

918923 modDocN (NS (UN n) ns) = NS modDocName (n:ns)

919924 modDocN (UN n) = NS modDocName [n]

920925 modDocN _ = sMN 1 "NotFoundForSure"

921926

922−process fn (DocStr (Right c))

927+process fn (DocStr (Right c) _) -- constants only have overviews

923928 = do ist <- getIState

924929 iRenderResult $ pprintConstDocs ist c (constDocs c)

925930

@@ -1106,7 +1111,7 @@ process fn Execute

11061111 t <- codegen

11071112 -- gcc adds .exe when it builds windows programs

11081113 progName <- return $ if isWindows then tmpn ++ ".exe" else tmpn

1109− ir <- compile t tmpn m

1114+ ir <- compile t tmpn (Just m)

11101115 runIO $ generate t (fst (head (idris_imported ist))) ir

11111116 case idris_outputmode ist of

11121117 RawOutput h -> do runIO $ rawSystem progName []

@@ -1118,9 +1123,13 @@ process fn Execute

11181123process fn (Compile codegen f)

11191124 | map toLower (takeExtension f) `elem` [".idr", ".lidr", ".idc"] =

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

1121− | otherwise = do (m, _) <- elabVal recinfo ERHS

1122− (PApp fc (PRef fc (sUN "run__IO"))

1123− [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')

11241133 ir <- compile codegen f m

11251134 i <- getIState

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

@@ -1414,9 +1423,10 @@ loadInputs inputs toline -- furthest line to read in input source files

14141423 ist <- getIState

14151424 putIState (ist { idris_tyinfodata = tidata,

14161425 idris_patdefs = patdefs })

1426+ exports <- findExports

14171427

14181428 case opt getOutput opts of

1419− [] -> performUsageAnalysis -- interactive

1429+ [] -> performUsageAnalysis (getExpNames exports) -- interactive

14201430 _ -> return [] -- batch, will be checked by the compiler

14211431

14221432 return (map fst ifiles))

@@ -1511,7 +1521,8 @@ idrisMain opts =

15111521 xs -> last xs

15121522 setOptLevel optimise

15131523 let outty = case opt getOutputTy opts of

1514− [] -> Executable

1524+ [] -> if Interface `elem` opts then

1525+ Object else Executable

15151526 xs -> last xs

15161527 let cgn = case opt getCodegen opts of

15171528 [] -> Via "c"

src/Idris/REPLParser.hs+2−2

@@ -258,9 +258,9 @@ cmd_doc name = do

258258 let constant = do

259259 c <- P.constant

260260 eof

261− return $ Right (DocStr (Right c))

261+ return $ Right (DocStr (Right c) FullDocs)

262262

263− let fnName = fnNameArg (\n -> DocStr (Left n)) name

263+ let fnName = fnNameArg (\n -> DocStr (Left n) FullDocs) name

264264

265265 try constant <|> fnName

266266

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/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/dsl001/test001.idr+4−1

@@ -35,8 +35,11 @@ using (G : Vect n Ty)

3535 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

3636 Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b

3737

38+ lam_ : TTName -> Expr (a :: G) t -> Expr G (TyFun a t)

39+ lam_ _ = Lam

40+

3841 dsl expr

39− lambda = Lam

42+ lambda = lam_

4043 variable = Var

4144 index_first = stop

4245 index_next = pop

test/dsl002/Resimp.idr+6−1

@@ -156,6 +156,11 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)

156156 = interp env v (\env', v' => do n <- v'

157157 interp env' (f n) k)

158158

159+ let_ : _ -> Creator (interpTy a) ->

160+ Res (a :: gam) (Val () :: gam') (R t) ->

161+ Res gam gam' (R t)

162+ let_ _ = Let

163+

159164-- run : {static} Res [] [] (R t) -> IO t

160165-- run prog = interp [] prog (\env, res => res)

161166

@@ -163,7 +168,7 @@ syntax run [prog] = interp [] prog (\env, res => res)

163168

164169dsl res

165170 variable = id

166− let = Let

171+ let = let_

167172 index_first = stop

168173 index_next = pop

169174

test/dsl003/DSLPi.idr+8−2

@@ -5,8 +5,11 @@ import Data.Vect

55

66data Ty = BOOL | INT | UNIT | ARR Ty Ty

77

8+arr_ : _ -> Ty -> Ty -> Ty

9+arr_ _ = ARR

10+

811dsl simple_type

9− pi = ARR

12+ pi = arr_

1013

1114test1 : simple_type (BOOL -> INT -> UNIT) = BOOL `ARR` (INT `ARR` UNIT)

1215test1 = Refl

@@ -25,8 +28,11 @@ using (vars : Vect n Ty)

2528 implicit exprSpec : Expr vars BOOL -> Spec vars

2629 exprSpec = ItHolds

2730

31+ forall_ : _ -> (t : Ty) -> Spec (t :: vars) -> Spec vars

32+ forall_ _ = ForAll

33+

2834dsl specs

29− pi = ForAll

35+ pi = forall_

3036 variable = Var

3137 index_first = FZ

3238 index_next = FS

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/reg027/reg027.idr+1−1

@@ -14,7 +14,7 @@ instance Functor IntFn where -- (\x => Int -> x) where

1414

1515instance Applicative (\x => Int -> x) where

1616 pure v = \x => v

17− (<$>) f a = \x => f x (a x)

17+ (<*>) f a = \x => f x (a x)

1818

1919instance Monad IntFn where

2020 f >>= k = \x => k (f x) x

test/reg041/ott.idr+1−1

@@ -37,6 +37,6 @@ EQ two False two False = one

3737EQ (pi s t) f (pi s' t') g = pi s $ \x => pi s' $ \y => EQ s x s' y ~> EQ (t x) (f x) (t' y) (g y)

3838EQ _ _ _ _ = zero

3939

40−example : <| id == id in (two ~> two) |>

40+example : <| (id == id in (two ~> two)) |>

4141example = ?prf

4242

test/reg050/expected+9−28

@@ -1,29 +1,10 @@

1−badbangop.idr:16:1:When elaborating right hand side of opUse:

2−When elaborating an application of function Prelude.Monad.>>=:

3− Can't unify

4− List Integer

5− with

6− argTy -> retTy

7−

8− Specifically:

9− Can't unify

10− List

11− with

12− \{uv0} => argTy -> uv

13−./baddoublebang.idr:6:26: error: not

14− a terminator, expected: "$",

15− "$>", "&&", "*", "+", "++", "-",

16− "->", ".", "/", "/=", "::", ";",

17− "<", "<#>", "<$", "<$>", "<*>",

18− "<+>", "<->", "<<", "<=", "<|>",

19− "=", "==", ">", ">=", ">>",

20− ">>=", "\\\\", "`", "in", "||",

21− "~=~",

22− ambiguous use of a left-associative operator,

23− ambiguous use of a non-associative operator,

24− ambiguous use of a right-associative operator,

25− end of input, function argument,

26− matching application expression,

27− single-line comment

1+./badbangop.idr:7:1: error: ! is

2+ not a valid

3+ operator, expected: space

4+(!) : List a -> Nat -> Maybe a

5+^

6+./baddoublebang.idr:6:28: error: unexpected

7+ Operator without known fixity:

8+ !!, expected: space

289doubleBang mmn = do pure !!mmn

29− ^

10+ ^

test/reg053/four.idr+1−1

@@ -5,5 +5,5 @@ data FourFunctor y = Four y y y y

55traverseFourFunctor : Applicative f ->

66 (x -> f b) -> FourFunctor x -> f (FourFunctor b)

77traverseFourFunctor constr f (Four w x y z)

8− = pure Four <$> (f w) <$> (f x) <$> (f y) <$> (f z)

8+ = pure Four <*> (f w) <*> (f x) <*> (f y) <*> (f z)

99

test/sourceLocation001/SourceLoc.idr+3−1

@@ -54,6 +54,8 @@ using (ctxt : Vect n Ty)

5454 run (App f x) env = !(run f env) !(run x env)

5555 run (Die {loc}) _ = Left loc

5656

57+ lam_ : _ -> Tm (t::ctxt) t' -> Tm ctxt (Arr t t')

58+ lam_ _ = Lam

5759

5860exec : Tm [] t -> IO ()

5961exec tm = case run tm [] of

@@ -64,7 +66,7 @@ dsl lang

6466 variable = Var

6567 index_first = FZ

6668 index_next = FS

67− lambda = Lam

69+ lambda = lam_

6870

6971testTerm1 : Tm [] (Arr U U)

7072testTerm1 = lang (\x=>Die)

test/sourceLocation001/expected+2−2

@@ -3,9 +3,9 @@ FileLoc "SourceLoc.idr" (16, 11) (16, 11)

33Testing using inline tactics

44FileLoc "SourceLoc.idr" (20, 17) (20, 17)

55Testing using metavariable with later definition

6−FileLoc "SourceLoc.idr" (96, 16) (96, 16)

6+FileLoc "SourceLoc.idr" (98, 16) (98, 16)

77-----------------------

88Success!

9−Error at FileLoc "SourceLoc.idr" (70, 23) (70, 23)

9+Error at FileLoc "SourceLoc.idr" (72, 23) (72, 23)

1010Success!

1111Success!

test/sugar001/test007.idr+1−1

@@ -19,7 +19,7 @@ instance Functor Eval where

1919instance Applicative Eval where

2020 pure x = MkEval (\e => Just x)

2121

22− (<$>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where

22+ (<*>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where

2323 appAux : Maybe (a -> b) -> Maybe a -> Maybe b

2424 appAux (Just fx) (Just gx) = Just (fx gx)

2525 appAux _ _ = Nothing

test/tactics001/Tactics.idrnew file+27

@@ -0,0 +1,27 @@

1+module Tactics

2+

3+import Language.Reflection.Tactical

4+

5+%default total

6+

7+-- Test that basic proofs with new-style tactics work

8+

9+||| Construct a Refl at some particular type for some particular term

10+||| @ t the type

11+||| @ x the term for equality to be reflexive at

12+refl : (t, x : Raw) -> Raw

13+refl t x = RApp (RApp (Var (UN "Refl")) t) x

14+

15+plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n

16+plusZeroRightNeutralNew Z = Refl

17+plusZeroRightNeutralNew (S k) =

18+ %runTactics (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k"))

19+ fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))

20+ solve)

21+

22+plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k)

23+plusSuccRightSuccNew Z k = Refl

24+plusSuccRightSuccNew (S j) k =

25+ %runTactics (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))

26+ fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))

27+ solve)

test/tactics001/expectednew file

No changes to the content.

test/tactics001/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ --check Tactics.idr

3+rm -f *.ibc

test/tutorial003/tutorial003.idr+1−1

@@ -19,7 +19,7 @@ instance Functor Eval where

1919instance Applicative Eval where

2020 pure x = MkEval (\e => Just x)

2121

22− (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where

22+ (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where

2323 app : Maybe (a -> b) -> Maybe a -> Maybe b

2424 app (Just fx) (Just gx) = Just (fx gx)

2525 app _ _ = Nothing