aca1148 · Idris-dev · git.iko.soy

CHANGELOG+28−13

compare with master

unifiedsplit

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

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

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

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

11

27

12New in 0.9.16:

28New in 0.9.16:

13--------------

29--------------

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

45 solved automatically.

61 solved automatically.

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

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

47 of large expressions.

63 of large expressions.

48−* EXPERIMENTAL Implementation of uniqueness types

64+* EXPERIMENTAL Implementation of uniqueness types

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

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

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

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

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

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

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

59 library (see #1516)

75 library (see #1516)

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

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

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

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

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

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

64 as code examples.

80 as code examples.

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

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

66 provide error messages to IDE clients.

82 provide error messages to IDE clients.

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

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

68 Engine style)

84 Engine style)

69

85

70New in 0.9.14:

86New in 0.9.14:

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

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

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

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

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

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

159 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

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

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

146* Updated 'effects' library

162* Updated 'effects' library

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

196 types may now depend on earlier methods.

212 types may now depend on earlier methods.

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

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

198 expressions can be made instances of a type class.

214 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

200 monadic/do/etc expressions.

216 monadic/do/etc expressions.

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

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

202 "if_valid", "if_error", etc.

218 "if_valid", "if_error", etc.

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

321Internal changes:

337Internal changes:

322

338

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

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

324−* Fixed nested parameters blocks

340+* Fixed nested parameters blocks

325* Improve efficiency of elaborator by:

341* Improve efficiency of elaborator by:

326 - only normalising when necessary

342 - only normalising when necessary

327 - reducing backtracking with resolving ambiguities

343 - reducing backtracking with resolving ambiguities

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

402Internal changes:

418Internal changes:

403

419

404* Some type class resolution fixes

420* Some type class resolution fixes

405−* Several minor bug fixes

421+* Several minor bug fixes

406* Performance improvements in resolving overloading and type classes

422* Performance improvements in resolving overloading and type classes

407

423

408New in 0.9.1:

424New in 0.9.1:

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

450Internal changes:

466Internal changes:

451

467

452* Everything :-)

468* Everything :-)

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

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

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

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

455− which are verified by a minimal type checker.

471+ which are verified by a minimal type checker.

456

472

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

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

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

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

460−

CONTRIBUTORS+1

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

28raichoo

29Philip Rasmussen

30Reynir Reynisson

31+Adam Sandberg Eriksson

31Seo Sanghyeon

32Seo Sanghyeon

32Benjamin Saunders

33Benjamin Saunders

33Alexander Shabalin

34Alexander Shabalin

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

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

10

11import System.Environment

12import System.Exit

13+import Control.Monad

13

14

14import Paths_idris

15import Paths_idris

15

16

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

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

18+ interface :: Bool,

17 output :: FilePath }

19 output :: FilePath }

18

20

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

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

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

21

23

22getOpts :: IO Opts

24getOpts :: IO Opts

23getOpts = do xs <- getArgs

25getOpts = do xs <- getArgs

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

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

25 where

27 where

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

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

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

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

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

28 process opts [] = opts

31 process opts [] = opts

29

32

30c_main :: Opts -> Idris ()

33c_main :: Opts -> Idris ()

31c_main opts = do elabPrims

34c_main opts = do elabPrims

32 loadInputs (inputs opts) Nothing

35 loadInputs (inputs opts) Nothing

36+ mainProg <- if interface opts

33− mainProg <- elabMain

37+ then liftM Just elabMain

38+ else return Nothing

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

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

35 runIO $ codegenC ir

40 runIO $ codegenC ir

36

41

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

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

32jsMain opts = do elabPrims

33 loadInputs (inputs opts) Nothing

34 mainProg <- elabMain

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

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

36 runIO $ codegenJavaScript ir

37

38main :: IO ()

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

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

32jsMain opts = do elabPrims

33 loadInputs (inputs opts) Nothing

34 mainProg <- elabMain

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

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

36 runIO $ codegenNode ir

37

38main :: IO ()

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

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

48

49instance Applicative DB where

50 pure = MkDB . return . Right

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

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

52 case f' of

53 Left err => return (Left err)

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

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

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

30

31instance Applicative Parser where

32 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

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

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

36

idris.cabal+19

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

394 test/ffi005/*.idr

395 test/ffi005/run

396 test/ffi005/expected

397+ test/ffi006/*.idr

398+ test/ffi006/*.c

399+ test/ffi006/run

400+ test/ffi006/expected

397

401

398 test/idrisdoc001/run

402 test/idrisdoc001/run

399 test/idrisdoc001/expected

403 test/idrisdoc001/expected

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

548 test/sugar005/*.idr

552 test/sugar005/*.idr

549 test/sugar005/expected

553 test/sugar005/expected

550

554

555+ test/tactics001/run

556+ test/tactics001/*.idr

557+ test/tactics001/expected

551

558

552 test/totality001/run

559 test/totality001/run

553 test/totality001/*.idr

560 test/totality001/*.idr

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

604 test/unique003/*.idr

611 test/unique003/*.idr

605 test/unique003/expected

612 test/unique003/expected

606

613

614+ test/docs001/run

615+ test/docs001/input

616+ test/docs001/*.idr

617+ test/docs001/expected

618+ test/docs002/run

619+ test/docs002/input

620+ test/docs002/*.idr

621+ test/docs002/expected

622+

623+

624+

607source-repository head

625source-repository head

608 type: git

626 type: git

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

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

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

720 , IRTS.CodegenC

738 , IRTS.CodegenC

721 , IRTS.CodegenCommon

739 , IRTS.CodegenCommon

722 , IRTS.CodegenJavaScript

740 , IRTS.CodegenJavaScript

741+ , IRTS.Exports

723 , IRTS.JavaScript.AST

742 , IRTS.JavaScript.AST

724 , IRTS.Compiler

743 , IRTS.Compiler

725 , IRTS.Defunctionalise

744 , IRTS.Defunctionalise

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

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

95

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

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

99

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

101 (MkArrowMonad m) >>= f =

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

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

10

11instance Applicative (IOExcept e) where

12 pure x = ioM (pure (pure x))

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

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

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

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

15

16instance Monad (IOExcept e) where

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

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

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

14instance Applicative Identity where

15 pure x = Id x

16

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

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

18

19instance Monad Identity where

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

25

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

27 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

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

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

31

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

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

32

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

34 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

36

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

38 empty = liftReaderT empty

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

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

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

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

31

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

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

33 (b, t) <- a r

34 return (g b, t))

35

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

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

31

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

33 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

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

36

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

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

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

16

17instance Applicative Erased where

18 pure = Erase

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

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

20

21instance Monad Erased where

22 (>>=) (Erase x) f = f x

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

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

1module Data.Fin

2

3%default total

4+%access public

4

5

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

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

6|||

7|||

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

144

145

145%language ErrorReflection

146%language ErrorReflection

146

147

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

149+total private

150+getNat' : TT -> Maybe TT

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

152+getNat' _ = Nothing

153+

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

155+||| the original term on failure.

156+total private

157+getNat : TT -> TT

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

159+

160+total private

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

162+mkFinIntegerErr lit finSize subErr

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

164+ , TextPart "as a literal for a"

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

166+ , SubReport subErr

167+ ]

147total

168total

148finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)

169finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)

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

171+ = mkFinIntegerErr (TConst c) m

172+ [ TermPart (TConst c)

173+ , TextPart "is not strictly less than"

174+ , TermPart (getNat m)

175+ ]

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

177+ = mkFinIntegerErr (P Bound n t) m

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

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

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

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

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

183+ ]

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

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

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

185+ = mkFinIntegerErr n m

151− , TextPart "as a literal for a"

152− , TermPart `(Fin ~m)

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

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

154− , TermPart n

155− , TextPart "is less than"

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

156− , TermPart m

157− ]

158− ]

188+ ]

159finFromIntegerErrors _ = Nothing

189finFromIntegerErrors _ = Nothing

160

190

161%error_handlers Data.Fin.fromInteger prf finFromIntegerErrors

191%error_handlers Data.Fin.fromInteger prf finFromIntegerErrors

libs/base/Data/Matrix.idr+29−29

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

7

8%default total

9

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

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

11infixr 2 >< -- vector outer product

12infixr 2 <<>> -- matrix commutator

13infixr 2 >><< -- matrix anticommutator

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

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

16−infixr 5 <> -- matrix multiplication

16+infixr 5 <> -- matrix multiplication

17infixr 7 \&\ -- vector tensor product

18infixr 7 <&> -- matrix tensor product

19

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

26

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

28 neutral {n} = replicate n neutral

29−

29+

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

31 inverse = map inverse

32

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

34

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

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

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

37

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

39 unity {n} = replicate n unity

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

42 inverseM = map inverseM

43

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

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

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

46

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

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

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

53-----------------------------------------------------------------------

54

55||| Inner product of ring vectors

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

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

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

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

58

59||| Tensor multiply (⊗) ring vectors

60(\&\) : 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

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

63 orep n v = concat $ replicate n v

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

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

90

91||| Matrix times a column vector

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

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

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

94

95||| Matrix times a row vector

96(<\>) : 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

98

99||| Matrix multiplication

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

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

101− Matrix k m a ->

101+ Matrix k m a ->

102 Matrix n m a

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

104

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

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

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

112

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

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

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

116

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

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

119row r = [r]

120

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

157

158instance Group Integer where

159 inverse = (* -1)

160−

160+

161instance AbelianGroup Integer

162

163−instance Ring Integer where

163+instance Ring Integer where

164− (<*>) = (*)

164+ (<.>) = (*)

165

166instance RingWithUnity Integer where

167 unity = 1

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

175

176instance Group Int where

177 inverse = (* -1)

178−

178+

179instance AbelianGroup Int

180

181−instance Ring Int where

181+instance Ring Int where

182− (<*>) = (*)

182+ (<.>) = (*)

183

184instance RingWithUnity Int where

185 unity = 1

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

193

194instance Group Float where

195 inverse = (* -1)

196−

196+

197instance AbelianGroup Float

198

199−instance Ring Float where

199+instance Ring Float where

200− (<*>) = (*)

200+ (<.>) = (*)

201

202instance RingWithUnity Float where

203 unity = 1

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

211

212instance Monoid Nat where

213 neutral = 0

214−

214+

215instance VerifiedSemigroup Nat where

216 semigroupOpIsAssociative = plusAssociative

217

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

228

229instance Group ZZ where

230 inverse = (* -1)

231−

231+

232instance AbelianGroup ZZ

233

234−instance Ring ZZ where

234+instance Ring ZZ where

235− (<*>) = (*)

235+ (<.>) = (*)

236−

236+

237instance RingWithUnity ZZ where

238 unity = 1

239

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

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

251

252instance 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)

254

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

256 unity = (unity :+ neutral)

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

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

25

26instance Applicative (Morphism r) where

27 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

29

30instance Monad (Morphism r) where

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

2

3import Data.Fin

4

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

6%default total

7

8namespace Vect {

9−

9+

10infixr 7 ::

11

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

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

529instance Applicative (Vect k) where

530 pure = replicate _

531

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

532+ fs <*> vs = zipWith apply fs vs

533

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

535+||| uses the diagonal.

534instance Monad (Vect n) where

536instance Monad (Vect n) where

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

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

536

538

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

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

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

540

542

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

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

542−-- Show

544+-- Show

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

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

544

546

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

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

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

595

597

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

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

597-- internal implementations.

599-- internal implementations.

598−

libs/base/Network/Cgi.idr+1−1

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

47instance Applicative CGI where

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

49

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

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

51 (c, j) <- b i

52 return (f c, j))

53

libs/base/Providers.idr+3−3

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

17 map f (Error err) = Error err

18

19instance Applicative Provider where

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

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

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

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

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

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

23 pure = Provide

24

25instance Monad Provider where

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

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

19

20instance Applicative (Process msg) where

21 pure = Lift . return

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

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

23

24instance Monad (Process msg) where

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

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

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

24 (size : Nat) ->

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

26 RawMemory (Vect size Bits8)

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

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

28 Poke : (offset : Nat) ->

29 (Vect size Bits8) ->

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

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

33 (dst_offset : Nat) ->

34 (src_offset : Nat) ->

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

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

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

38 RawMemory () (MemoryChunk dst_size dst_init)

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

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

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

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

41

42private

43do_malloc : Nat -> IOExcept String Ptr

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

84 = do ptr <- do_malloc n

85 k () (CH ptr)

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

88 handle (CH ptr) (Free) k

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

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

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

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

92 k res (CH ptr)

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

102RAW_MEMORY : Type -> EFFECT

103RAW_MEMORY t = MkEff t RawMemory

104

105−allocate : (n : Nat) ->

105+allocate : (n : Nat) ->

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

107allocate size = call $ Allocate size

108

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

111 Bits8 ->

112 (size : Nat) ->

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

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

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

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

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

117

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

122 (offset : Nat) ->

123 (size : Nat) ->

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

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

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

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

127

128poke : {n : Nat} ->

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

130 (offset : Nat) ->

131 Vect size Bits8 ->

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

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

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

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

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

136

137private

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

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

139getRawPtr = call $ GetRawPtr

140

141private

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

173move dst_offset src_offset size dst_bounds src_bounds

174 = do src_ptr <- Src :- getRawPtr

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

176− return ()

176+ return ()

177

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

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

11

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

13 pure = value

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

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

15 a' <- a

16 value (f' a')

17

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

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

9

10||| The internal representation of StdIO effects

11data StdIO : Effect where

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

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

13− GetStr : { () } StdIO String

13+ GetStr : { () } StdIO String

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

15 GetCh : { () } StdIO Char

16

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

22instance Handler StdIO IO where

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

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

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

27

28instance Handler StdIO (IOExcept a) where

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

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

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

33

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

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

58getChar : { [STDIO] } Eff Char

59getChar = call $ GetCh

60

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

174

175-- ------------------------------------------------------ [ for idiom brackets ]

176

177−infixl 2 <$>

177+infixl 2 <*>

178

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

180pure = value

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

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

183pureM = value

184

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

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

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

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

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

188 arg <- v

189 return (fn arg)

190

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

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

11

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

13 pure = value

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

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

15 a' <- a

16 value (f' a')

17

libs/oldeffects/Effects.idr+3−3

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

185

186-- ------------------------------------------------------ [ for idiom brackets ]

187

188−infixl 2 <$>

188+infixl 2 <*>

189

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

191pure = value

192

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

194

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

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

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

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

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

198 arg <- v

199 return (fn arg)

200

libs/prelude/IO.idr+56−3

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

23record FFI where

24 ffi_types : Type -> Type

25 ffi_fn : Type

26+ ffi_data : Type

26 constructor MkFFI

27 constructor MkFFI

28+

27{-

29{-

28record FFI : Type where

30record FFI : Type where

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

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

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

33+ (ffi_fn : Type) ->

34+ (ffi_data : Type) -> FFI

30-}

35-}

36+

31abstract

37abstract

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

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

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

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

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

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

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

95liftPrimIO = MkIO

101liftPrimIO = MkIO

96

102

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

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

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

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

108+run__IO f = call__IO f

99

109

100unsafePerformIO : IO' ffi a -> a

110unsafePerformIO : IO' ffi a -> a

101unsafePerformIO (MkIO f) = unsafePerformPrimIO

111unsafePerformIO (MkIO f) = unsafePerformPrimIO

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

148 C_IntT : C_IntTypes i -> C_Types i

158 C_IntT : C_IntTypes i -> C_Types i

149

159

150FFI_C : FFI

160FFI_C : FFI

151−FFI_C = MkFFI C_Types String

161+FFI_C = MkFFI C_Types String String

152

162

153IO : Type -> Type

163IO : Type -> Type

154IO = IO' FFI_C

164IO = IO' FFI_C

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

199%used MkJsFn x

209%used MkJsFn x

200

210

201FFI_JS : FFI

211FFI_JS : FFI

202−FFI_JS = MkFFI JS_Types String

212+FFI_JS = MkFFI JS_Types String String

203

213

204JS_IO : Type -> Type

214JS_IO : Type -> Type

205JS_IO = IO' FFI_JS

215JS_IO = IO' FFI_JS

206

216

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 =

267%name Tactic tac, tac'

268

269

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

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

271|||

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

273||| construction of custom tactics.

274|||

275||| @ a the type to be quoted

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

276−class Quotable a where

277+class Quotable a t where

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

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

278 |||

279 |||

279 ||| This is to enable quoting polymorphic datatypes

280 ||| This is to enable quoting polymorphic datatypes

280− quotedTy : TT

281+ quotedTy : t

281

282

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

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

283 |||

284 |||

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

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

285− quote : a -> TT

286+ quote : a -> t

286

287

287−instance Quotable Nat where

288+instance Quotable Nat TT where

288 quotedTy = `(Nat)

289 quotedTy = `(Nat)

289

290

290 quote Z = `(Z)

291 quote Z = `(Z)

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

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

292

293

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

294 quotedTy = `(Int)

301 quotedTy = `(Int)

295 quote x = TConst (I x)

302 quote x = TConst (I x)

296

303

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

298 quotedTy = `(Float)

309 quotedTy = `(Float)

299 quote x = TConst (Fl x)

310 quote x = TConst (Fl x)

300

311

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

302 quotedTy = `(Char)

317 quotedTy = `(Char)

303 quote x = TConst (Ch x)

318 quote x = TConst (Ch x)

304

319

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

306 quotedTy = `(Bits8)

325 quotedTy = `(Bits8)

307 quote x = TConst (B8 x)

326 quote x = TConst (B8 x)

308

327

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

310 quotedTy = `(Bits16)

333 quotedTy = `(Bits16)

311 quote x = TConst (B16 x)

334 quote x = TConst (B16 x)

312

335

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

314 quotedTy = `(Bits32)

341 quotedTy = `(Bits32)

315 quote x = TConst (B32 x)

342 quote x = TConst (B32 x)

316

343

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

318 quotedTy = `(Bits64)

349 quotedTy = `(Bits64)

319 quote x = TConst (B64 x)

350 quote x = TConst (B64 x)

320

351

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

322 quotedTy = `(Integer)

357 quotedTy = `(Integer)

323 quote x = TConst (BI x)

358 quote x = TConst (BI x)

324

359

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

326 quotedTy = `(Bits8x16)

365 quotedTy = `(Bits8x16)

327 quote x = TConst (B8V x)

366 quote x = TConst (B8V x)

328

367

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

330 quotedTy = `(Bits16x8)

373 quotedTy = `(Bits16x8)

331 quote x = TConst (B16V x)

374 quote x = TConst (B16V x)

332

375

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

334 quotedTy = `(Bits32x4)

381 quotedTy = `(Bits32x4)

335 quote x = TConst (B32V x)

382 quote x = TConst (B32V x)

336

383

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

338 quotedTy = `(Bits64x2)

389 quotedTy = `(Bits64x2)

339 quote x = TConst (B64V x)

390 quote x = TConst (B64V x)

340

391

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

342 quotedTy = `(String)

397 quotedTy = `(String)

343 quote x = TConst (Str x)

398 quote x = TConst (Str x)

344

399

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

346 quotedTy = `(NameType)

405 quotedTy = `(NameType)

347 quote Bound = `(Bound)

406 quote Bound = `(Bound)

348 quote Ref = `(Ref)

407 quote Ref = `(Ref)

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

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

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

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

351

410

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+

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

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

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

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

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

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

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

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

356

422

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

358 quotedTy = `(TTName)

429 quotedTy = `(TTName)

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

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

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

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

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

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

362 quote NErased = `(NErased)

433 quote NErased = `(NErased)

363

434

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

365 quotedTy = `(NativeTy)

450 quotedTy = `(NativeTy)

366 quote IT8 = `(Reflection.IT8)

451 quote IT8 = `(Reflection.IT8)

367 quote IT16 = `(Reflection.IT16)

452 quote IT16 = `(Reflection.IT16)

368 quote IT32 = `(Reflection.IT32)

453 quote IT32 = `(Reflection.IT32)

369 quote IT64 = `(Reflection.IT64)

454 quote IT64 = `(Reflection.IT64)

370

455

371−instance Quotable Reflection.IntTy where

456+instance Quotable Reflection.IntTy TT where

372 quotedTy = `(Reflection.IntTy)

457 quotedTy = `(Reflection.IntTy)

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

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

374 quote ITNative = `(Reflection.ITNative)

459 quote ITNative = `(Reflection.ITNative)

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

376 quote ITChar = `(Reflection.ITChar)

461 quote ITChar = `(Reflection.ITChar)

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

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

378

463

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

380 quotedTy = `(ArithTy)

473 quotedTy = `(ArithTy)

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

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

382 quote ATFloat = `(ATFloat)

475 quote ATFloat = `(ATFloat)

383

476

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

385 quotedTy = `(Const)

483 quotedTy = `(Const)

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

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

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

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

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

406 quote WorldType = `(WorldType)

504 quote WorldType = `(WorldType)

407 quote TheWorld = `(TheWorld)

505 quote TheWorld = `(TheWorld)

408

506

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

410 quotedTy = `(TTUExp)

533 quotedTy = `(TTUExp)

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

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

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

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

413

536

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

415 quotedTy = `(Universe)

549 quotedTy = `(Universe)

416 quote Reflection.NullType = `(NullType)

550 quote Reflection.NullType = `(NullType)

417 quote Reflection.UniqueType = `(UniqueType)

551 quote Reflection.UniqueType = `(UniqueType)

418 quote Reflection.AllTypes = `(AllTypes)

552 quote Reflection.AllTypes = `(AllTypes)

419

553

420mutual

554mutual

421− instance Quotable TT where

555+ instance Quotable TT TT where

422 quotedTy = `(TT)

556 quotedTy = `(TT)

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

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

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

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

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

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

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

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

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

433

567

434− instance Quotable (Binder TT) where

568+ instance Quotable (Binder TT) TT where

435 quotedTy = `(Binder TT)

569 quotedTy = `(Binder TT)

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

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

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

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

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

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

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

449

583

450

584

451−instance Quotable ErrorReportPart where

585+instance Quotable ErrorReportPart TT where

452 quotedTy = `(ErrorReportPart)

586 quotedTy = `(ErrorReportPart)

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

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

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

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

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

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

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

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

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

478

612

479−instance Quotable Raw where

613+instance Quotable Raw TT where

480 quotedTy = `(Raw)

614 quotedTy = `(Raw)

481 quote = quoteRaw

615 quote = quoteRaw

482

616

483−instance Quotable (Binder Raw) where

617+instance Quotable (Binder Raw) TT where

484 quotedTy = `(Binder Raw)

618 quotedTy = `(Binder Raw)

485 quote = quoteRawBinder

619 quote = quoteRawBinder

486

620

487−instance Quotable Tactic where

621+instance Quotable Tactic TT where

488 quotedTy = `(Tactic)

622 quotedTy = `(Tactic)

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

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

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

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

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

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

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

515 quote SourceFC = `(SourceFC)

649 quote SourceFC = `(SourceFC)

516

650

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

29 | NoTypeDecl TTName

30 | NotInjective TT TT TT

31 | CantResolve TT

32− | CantResolveAlts (List String)

32+ | CantResolveAlts (List TTName)

33 | IncompleteTerm TT

34 | UniverseError

35 | ProgramLineComment

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

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

22 prim__Holes : Tactical (List TTName)

23 prim__Guess : Tactical (Maybe TT)

24

25+ prim__SourceLocation : Tactical SourceLocation

26+

25 prim__Forget : TT -> Tactical Raw

27 prim__Forget : TT -> Tactical Raw

26

28

27 prim__Gensym : String -> Tactical TTName

29 prim__Gensym : String -> Tactical TTName

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

32 prim__Unfocus : TTName -> Tactical ()

34 prim__Unfocus : TTName -> Tactical ()

33 prim__Attack : Tactical ()

35 prim__Attack : Tactical ()

34

36

37+ prim__Rewrite : Raw -> Tactical ()

38+

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

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

40+ prim__Intro : Maybe TTName -> Tactical ()

36

41

37-------------

42-------------

38-- Public API

43-- Public API

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

44

49

45instance Applicative Tactical where

50instance Applicative Tactical where

46 pure x = prim__PureTactical x

51 pure x = prim__PureTactical x

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

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

48 prim__BindTactical x $ \y =>

53 prim__BindTactical x $ \y =>

49 prim__PureTactical $ g y

54 prim__PureTactical $ g y

50

55

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

93

98

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

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

95claim n ty = prim__Claim n ty

100claim 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

249instance Applicative PrimIO where

250 pure = prim_io_return

251

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

253

254instance Applicative (IO' ffi) where

255 pure x = io_return x

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

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

257 io_bind a (\a' =>

258 io_return (f' a')))

259

260instance Applicative Maybe where

261 pure = Just

262

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

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

264− _ <$> _ = Nothing

264+ _ <*> _ = Nothing

265

266instance Applicative (Either e) where

267 pure = Right

268

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

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

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

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

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

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

272

273instance Applicative List where

274 pure x = [x]

275

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

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

277

278---- Alternative instances

279

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

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

5-- XXX: change?

6infixl 6 <->

7infixl 6 <+>

8−infixl 6 <*>

8+infixl 6 <.>

9infixl 5 <#>

10

11%access public

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

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

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

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

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

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

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

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

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

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

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

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

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

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

104class AbelianGroup a => Ring a where

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

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

106

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

108− total ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> 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)

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)

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

111

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

135class Ring a => RingWithUnity a where

136 unity : a

137

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

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

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

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

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

141

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

295class RingWithUnity a => Field a where

296 inverseM : a -> a

297

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

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

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

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

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

301

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

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

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

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

305||| Must satisfy the following laws:

306|||

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

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

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

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

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

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

316

317class (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

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

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

321 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

9

10---- Applicative functors/Idioms

11

12−infixl 2 <$>

12+infixl 2 <*>

13

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

15 pure : a -> f a

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

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

17

18instance Applicative id where

19 pure a = a

20− f <$> a = f a

20+ f <*> a = f a

21

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

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

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

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

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

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

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

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

30 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

32

33−infixl 2 <$

33+infixl 2 <*

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

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

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

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

36

37−infixl 2 $>

37+infixl 2 *>

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

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

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

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

40

41||| Lift a function to an applicative

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

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

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

44

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

46liftA2 : 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

48

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

50liftA3 : 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

52

53infixl 3 <|>

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

libs/prelude/Prelude/Functor.idr+8

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

10 ||| @ m the morphism

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

12

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+

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

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

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

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

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

23 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

16

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

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

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

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

20 mx >>= \x =>

21 pure (f x)

22 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

195instance MinBound Nat where

196 minBound = Z

197

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

198instance Cast Integer Nat where

199instance Cast Integer Nat where

199 cast = fromInteger

200 cast = fromInteger

200

201

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

267 bottom = Z

268 bottom = Z

268

269

270

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

270instance Cast Int Nat where

272instance Cast Int Nat where

271 cast i = fromInteger (cast i)

273 cast i = fromInteger (cast i)

272

274

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

350

352

351

353

352--------------------------------------------------------------------------------

354--------------------------------------------------------------------------------

353−-- An informative comparison view

355+-- An informative comparison view

354--------------------------------------------------------------------------------

356--------------------------------------------------------------------------------

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

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

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

358 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

111

112instance Applicative Stream where

113 pure = repeat

114− (<$>) = zipWith apply

114+ (<*>) = zipWith apply

115

116instance Monad Stream where

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

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

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

8import Prelude.Functor

9

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

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

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

12

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

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

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

15

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

17for_ = flip traverse_

rts/idris_gc.c+4−8

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

17 } else {

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

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

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

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

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

22 }

21 }

23 }

22 }

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

90 case CON:

89 case CON:

91 ar = ARITY(heap_item);

90 ar = ARITY(heap_item);

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

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

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

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

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

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

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

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

97 }

94 }

98 break;

95 break;

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

111void idris_gc(VM* vm) {

108void idris_gc(VM* vm) {

112 HEAP_CHECK(vm)

109 HEAP_CHECK(vm)

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

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

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

115

111

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

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

117 free(vm->heap.old);

113 free(vm->heap.old);

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

162

158

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

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

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

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

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

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

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

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

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

163 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);

169#ifdef IDRIS_ENABLE_STATS

165#ifdef IDRIS_ENABLE_STATS

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

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

171#endif

167#endif

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

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

173

169

174}

170}

rts/idris_heap.c+2−2

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

10 char * mem = malloc(heap_size);

11 if (mem == NULL) {

12 fprintf(stderr,

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

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

14− (int)heap_size);

14+ heap_size);

15 exit(EXIT_FAILURE);

16 }

17

rts/idris_rts.c+14

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

63 return vm;

64}

65

66+VM* idris_vm() {

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

68+ init_threadkeys();

69+ init_threaddata(vm);

70+ init_gmpalloc();

71+ init_nullaries();

72+

73+ return vm;

74+}

75+

76+void close_vm(VM* vm) {

77+ terminate(vm);

78+}

79+

66void init_threadkeys() {

80void init_threadkeys() {

67#ifdef HAS_PTHREAD

81#ifdef HAS_PTHREAD

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

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

rts/idris_rts.h+6−1

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

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

126Stats terminate(VM* vm);

127

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

129+// calling Idris from C)

130+VM* idris_vm();

131+void close_vm(VM* vm);

132+

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

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

129void init_threadkeys();

134void init_threadkeys();

130

135

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

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

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

163

168

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

169#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))

166

171

167// Integers, floats and operators

172// Integers, floats and operators

168

173

rts/idris_stats.h+2−1

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

3

4#ifdef IDRIS_ENABLE_STATS

5#include <time.h>

6+#endif

7+

6#include <inttypes.h>

8#include <inttypes.h>

7#include <stdint.h>

9#include <stdint.h>

8−#endif

9

10

11

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

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

samples/interp.idr+2−2

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

37 index_first = stop

38 index_next = pop

39

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

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

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

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

42

43 pure : Expr G a -> Expr G a

44 pure = id

src/IRTS/CodegenC.hs+124−17

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

24import Debug.Trace

25

26codegenC :: CodeGenerator

27−codegenC ci = codegenC' (simpleDecls ci)

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

28− (outputFile ci)

28+ (outputFile ci)

29− (outputType ci)

29+ (outputType ci)

30− (includes ci)

30+ (includes ci)

31− (compileObjs ci)

31+ (compileObjs ci)

32− (map mkLib (compileLibs ci) ++

32+ (map mkLib (compileLibs ci) ++

33− map incdir (importDirs ci))

33+ map incdir (importDirs ci))

34− (compilerFlags ci)

34+ (compilerFlags ci)

35+ (exportDecls ci)

36+ (interfaces ci)

35− (debugLevel ci)

37+ (debugLevel ci)

38+ when (interfaces ci) $

39+ codegenH (exportDecls ci)

36

40

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

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

38 incdir i = "-I" ++ i

42 incdir i = "-I" ++ i

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

44 [String] -> -- extra object files

48 [String] -> -- extra object files

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

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

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

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

51+ [ExportIFace] ->

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

47 DbgLevel ->

53 DbgLevel ->

48 IO ()

54 IO ()

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

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

50 = do -- print defs

56 = do -- print defs

51 let bc = map toBC defs

57 let bc = map toBC defs

52 let h = concatMap toDecl (map fst bc)

58 let h = concatMap toDecl (map fst bc)

53 let cc = concatMap (uncurry toC) bc

59 let cc = concatMap (uncurry toC) bc

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

54 d <- getDataDir

61 d <- getDataDir

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

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

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

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

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

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

58 case exec of

65 case exec of

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

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

60 Raw -> writeFile out cout

67 Raw -> writeFile out cout

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

67 libFlags <- getLibFlags

74 libFlags <- getLibFlags

68 incFlags <- getIncFlags

75 incFlags <- getIncFlags

69 let args = [gccDbg dbg] ++

76 let args = [gccDbg dbg] ++

70− gccFlags ++

77+ gccFlags iface ++

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

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

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

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

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

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

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

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

75 [tmpn] ++

82 [tmpn] ++

76− concatMap words libFlags ++

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

77 concatMap words incFlags ++

84 concatMap words incFlags ++

78− concatMap words libs ++

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

79 concatMap words flags ++

86 concatMap words flags ++

80 ["-o", out]

87 ["-o", out]

81−-- putStrLn gcc

88+-- putStrLn (show args)

82 exit <- rawSystem comp args

89 exit <- rawSystem comp args

83 when (exit /= ExitSuccess) $

90 when (exit /= ExitSuccess) $

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

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

92+ where

93+ getExp (Export _ _ exp) = exp

85

94

86headers xs =

95headers xs =

87 concatMap

96 concatMap

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

93

102

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

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

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

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

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

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

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

97

107

98gccDbg DEBUG = "-g"

108gccDbg DEBUG = "-g"

99gccDbg TRACE = "-O2"

109gccDbg TRACE = "-O2"

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

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

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

312toFType (FApp c [_])

322toFType (FApp c [_])

313 | c == sUN "C_Any" = FAny

323 | c == sUN "C_Any" = FAny

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

324+toFType t = FAny

315

325

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

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

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

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

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

561

571

562flUnOp :: String -> String -> String

572flUnOp :: String -> String -> String

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

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

574+

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

576+

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

578+

579+ifaceC :: Export -> String

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

581+ifaceC (ExportFun n cn ret args)

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

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

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

585+ where showArgs [] = ""

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

587+ showArgs ts

588+

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

590+

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

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

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

594+ where push i [] = ""

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

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

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

598+

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

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

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

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

603+

604+ retval (FIO t)

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

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

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

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

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

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

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

612+ retval t

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

614+

615+ctype (FCon c)

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

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

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

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

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

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

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

623+ctype (FApp c [_])

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

625+ctype (FStr s) = s

626+ctype FUnknown = "void*"

627+ctype (FIO t) = ctype t

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

629+

630+carith (FCon i)

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

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

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

634+

635+cdesc (FStr s) = s

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

637+

638+-- Then, the header files

639+

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

641+codegenH es = mapM_ writeIFace es

642+

643+writeIFace :: ExportIFace -> IO ()

644+writeIFace (Export ffic hdr exps)

645+ | ffic == sUN "FFI_C"

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

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

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

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

650+ "#endif\n\n"

651+ writeFile hdr hfile

652+ | otherwise = return ()

653+

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

655+ where hchar x | isAlphaNum x = toUpper x

656+ hchar _ = '_'

657+

658+hdr_export :: Export -> String

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

660+hdr_export (ExportFun n cn ret args)

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

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

663+ where showArgs [] = ""

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

665+ showArgs ts

666+

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

668+

669+

670+

src/IRTS/CodegenCommon.hs+3−1

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

33 debugLevel :: DbgLevel,

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

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

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

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

37+ interfaces :: Bool,

38+ exportDecls :: [ExportIFace]

37 }

39 }

38

40

39type CodeGenerator = CodegenInfo -> IO ()

41type CodeGenerator = CodegenInfo -> IO ()

src/IRTS/Compiler.hs+21−11

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

11import IRTS.DumpBC

12import IRTS.CodegenJavaScript

13import IRTS.Inliner

14+import IRTS.Exports

14

15

15import Idris.AbsSyntax

16import Idris.AbsSyntax

16import Idris.AbsSyntaxTree

17import Idris.AbsSyntaxTree

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

45

46

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

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

47-- generate code.

48-- generate code.

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

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

49−compile codegen f tm

50+compile codegen f mtm

50 = do checkMVs -- check for undefined metavariables

51 = do checkMVs -- check for undefined metavariables

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

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

53+ exports <- findExports

54+

52− reachableNames <- performUsageAnalysis

55+ reachableNames <- performUsageAnalysis (getExpNames exports)

56+ maindef <- case mtm of

57+ Nothing -> return []

53− maindef <- irMain tm

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

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

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

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

55 objs <- getObjectFiles codegen

61 objs <- getObjectFiles codegen

56 libs <- getLibs codegen

62 libs <- getLibs codegen

57 flags <- getFlags codegen

63 flags <- getFlags codegen

58 hdrs <- getHdrs codegen

64 hdrs <- getHdrs codegen

59 impdirs <- allImportDirs

65 impdirs <- allImportDirs

60− defsIn <- mkDecls tm reachableNames

66+ defsIn <- mkDecls reachableNames

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

68+ let iface = case mtm of

69+ Nothing -> True

70+ Just _ -> False

71+

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

72+ let defs = defsIn ++ maindef

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

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

63 -- Inlined top level LDecl made here

74 -- Inlined top level LDecl made here

64 let defsInlined = inlineAll defs

75 let defsInlined = inlineAll defs

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

89 triple <- Idris.AbsSyntax.targetTriple

100 triple <- Idris.AbsSyntax.targetTriple

90 cpu <- Idris.AbsSyntax.targetCPU

101 cpu <- Idris.AbsSyntax.targetCPU

91 iLOG "Building output"

102 iLOG "Building output"

92−

93 case checked of

103 case checked of

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

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

95 hdrs impdirs objs libs flags

105 hdrs impdirs objs libs flags

96 NONE c (toAlist defuns)

106 NONE c (toAlist defuns)

97− tagged

107+ tagged iface exports

98-- runIO $ case codegen of

108-- runIO $ case codegen of

99-- ViaC -> codegenC cginfo

109-- ViaC -> codegenC cginfo

100-- ViaJava -> codegenJava cginfo

110-- ViaJava -> codegenJava cginfo

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

133 i <- irTerm M.empty [] tm

143 i <- irTerm M.empty [] tm

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

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

135

145

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

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

137−mkDecls t used

147+mkDecls used

138 = do i <- getIState

148 = do i <- getIState

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

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

140 decls <- mapM build ds

150 decls <- mapM build ds

src/IRTS/Exports.hsnew file+110

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

1+{-# LANGUAGE PatternGuards #-}

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

3+

4+import Idris.AbsSyntax

5+import Idris.Core.TT

6+import Idris.Core.CaseTree

7+import Idris.Core.Evaluate

8+import Idris.Error

9+import IRTS.Lang

10+

11+import Data.Maybe

12+

13+findExports :: Idris [ExportIFace]

14+findExports = do exps <- getExports

15+ es <- mapM toIFace exps

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

17+ return es

18+

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

20+getExpNames = concatMap expNames

21+

22+expNames :: ExportIFace -> [Name]

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

24+ where fnames (ExportData _) = Nothing

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

26+

27+toIFace :: Name -> Idris ExportIFace

28+toIFace n = do i <- getIState

29+ let ctxt = tt_ctxt i

30+ def <- case lookupDefExact n ctxt of

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

32+ -> getExpList (snd (cases_compiletime cs))

33+ Nothing -> ifail "Can't happen [toIFace]"

34+ case lookupTyExact n ctxt of

35+ Just ty -> toIFaceTyVal ty def

36+ Nothing -> ifail "Can't happen [toIFace]"

37+ where

38+ getExpList (STerm t) = return t

39+ getExpList _ = ifail "Badly formed export list"

40+

41+toIFaceTyVal :: Type -> Term -> Idris ExportIFace

42+toIFaceTyVal ty tm

43+ | (P _ exp _, [P _ ffi _, Constant (Str hdr), _]) <- unApply ty

44+ = do tm' <- toIFaceVal tm

45+ return $ Export ffi hdr tm'

46+

47+toIFaceVal :: Term -> Idris [Export]

48+toIFaceVal tm

49+ | (P _ end _, _) <- unApply tm,

50+ end == sNS (sUN "End") ["FFI_Export"] = return []

51+ | (P _ fun _, [_,_,_,_,(P _ fn _),extnm,prf,rest]) <- unApply tm,

52+ fun == sNS (sUN "Fun") ["FFI_Export"]

53+ = do rest' <- toIFaceVal rest

54+ return $

55+ ExportFun fn (toFDesc extnm) (toFDescRet prf) (toFDescArgs prf)

56+ : rest'

57+ | (P _ dat _, [_,_,_,_,d,rest]) <- unApply tm,

58+ dat == sNS (sUN "Data") ["FFI_Export"]

59+ = do rest' <- toIFaceVal rest

60+ return $ ExportData (toFDesc d) : rest'

61+ | otherwise = ifail $ "Badly formed export list " ++ show tm

62+

63+toFDesc :: Term -> FDesc

64+toFDesc (Constant (Str str)) = FStr str

65+toFDesc tm

66+ | (P _ n _, []) <- unApply tm = FCon (deNS n)

67+ | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDesc as)

68+toFDesc _ = FUnknown

69+

70+toFDescRet :: Term -> FDesc

71+toFDescRet tm

72+ | (P _ ret _, [_,_,_,b]) <- unApply tm,

73+ ret == sNS (sUN "FFI_Ret") ["FFI_Export"]

74+ = toFDescBase b

75+ | (P _ io _, [_,_,_,b]) <- unApply tm,

76+ io == sNS (sUN "FFI_IO") ["FFI_Export"]

77+ = FIO $ toFDescBase b

78+ | (P _ fun _, [_,_,_,_,_,t]) <- unApply tm,

79+ fun == sNS (sUN "FFI_Fun") ["FFI_Export"]

80+ = toFDescRet t

81+ | otherwise = error "Badly formed export proof"

82+

83+toFDescBase :: Term -> FDesc

84+toFDescBase tm

85+ | (P _ prim _, [_, _, _, pdesc]) <- unApply tm,

86+ prim == sNS (sUN "FFI_Prim") ["FFI_Export"]

87+ = toFDescPrim pdesc

88+ | (P _ prim _, [_, _, _, ddesc, _]) <- unApply tm,

89+ prim == sNS (sUN "FFI_ExpType") ["FFI_Export"]

90+ = toFDescPrim ddesc

91+ | otherwise = error "Badly formed export type"

92+

93+toFDescArgs :: Term -> [FDesc]

94+toFDescArgs tm

95+ | (P _ fun _, [_,_,_,_,b,t]) <- unApply tm,

96+ fun == sNS (sUN "FFI_Fun") ["FFI_Export"]

97+ = toFDescBase b : toFDescArgs t

98+ | otherwise = []

99+

100+toFDescPrim (Constant (Str str)) = FStr str

101+toFDescPrim tm

102+ | (P _ n _, []) <- unApply tm = FCon (deNS n)

103+ | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDescPrim as)

104+toFDescPrim _ = FUnknown

105+

106+deNS (NS n _) = n

107+deNS n = n

108+

109+

110+

src/IRTS/Lang.hs+14−1

@@ -29,7 +29,7 @@ data LExp = LV LVar

29 Int Name [LExp]

30 | LCase CaseType LExp [LAlt]

31 | LConst Const

32− | LForeign FDesc -- Function descriptor

32+ | LForeign FDesc -- Function descriptor (usually name as string)

33 FDesc -- Return type descriptor

34 [(FDesc, LExp)] -- first LExp is the FFI type description

35 | LOp PrimFn [LExp]

@@ -40,9 +40,22 @@ data LExp = LV LVar

40data FDesc = FCon Name

41 | FStr String

42 | FUnknown

43+ | FIO FDesc

43 | FApp Name [FDesc]

44 | FApp Name [FDesc]

44 deriving (Show, Eq)

45 deriving (Show, Eq)

45

46

47+data Export = ExportData FDesc -- Exported data descriptor (usually string)

48+ | ExportFun Name -- Idris name

49+ FDesc -- Exported function descriptor

50+ FDesc -- Return type descriptor

51+ [FDesc] -- Argument types

52+ deriving (Show, Eq)

53+

54+data ExportIFace = Export Name -- FFI descriptor

55+ String -- interface file

56+ [Export]

57+ deriving (Show, Eq)

58+

46-- Primitive operators. Backends are not *required* to implement all

59-- Primitive operators. Backends are not *required* to implement all

47-- of these, but should report an error if they are unable

60-- of these, but should report an error if they are unable

48

61

src/Idris/AbsSyntax.hs+26−16

@@ -96,7 +96,7 @@ addHdr :: Codegen -> String -> Idris ()

96addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }

97

98addImported :: Bool -> FilePath -> Idris ()

99−addImported pub f

99+addImported pub f

100 = do i <- getIState

101 putIState $ i { idris_imported = nub $ (f, pub) : idris_imported i }

102

@@ -129,22 +129,30 @@ addErasureUsage :: Name -> Int -> Idris ()

129addErasureUsage n i = do ist <- getIState

130 putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }

131

132+addExport :: Name -> Idris ()

133+addExport n = do ist <- getIState

134+ putIState $ ist { idris_exports = n : idris_exports ist }

135+

132addUsedName :: FC -> Name -> Name -> Idris ()

136addUsedName :: FC -> Name -> Name -> Idris ()

133−addUsedName fc n arg

137+addUsedName fc n arg

134 = do ist <- getIState

138 = do ist <- getIState

135 case lookupTyName n (tt_ctxt ist) of

139 case lookupTyName n (tt_ctxt ist) of

136− [(_, ty)] -> addUsage 0 ty

140+ [(n', ty)] -> addUsage n' 0 ty

137 [] -> throwError (At fc (NoSuchVariable n))

141 [] -> throwError (At fc (NoSuchVariable n))

138 xs -> throwError (At fc (CantResolveAlts (map fst xs)))

142 xs -> throwError (At fc (CantResolveAlts (map fst xs)))

139− where addUsage i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))

143+ where addUsage n i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))

140− addErasureUsage n i

144+ addErasureUsage n i

141− | otherwise = addUsage (i + 1) sc

145+ | otherwise = addUsage n (i + 1) sc

142− addUsage _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))

146+ addUsage _ _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))

143

147

144getErasureUsage :: Idris [(Name, Int)]

148getErasureUsage :: Idris [(Name, Int)]

145getErasureUsage = do ist <- getIState;

149getErasureUsage = do ist <- getIState;

146 return (idris_erasureUsed ist)

150 return (idris_erasureUsed ist)

147

151

152+getExports :: Idris [Name]

153+getExports = do ist <- getIState

154+ return (idris_exports ist)

155+

148totcheck :: (FC, Name) -> Idris ()

156totcheck :: (FC, Name) -> Idris ()

149totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

157totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

150

158

@@ -1074,8 +1082,8 @@ expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs decls)

1074 (map (mapsnd (expandParams dec ps ns [])) params)

1082 (map (mapsnd (expandParams dec ps ns [])) params)

1075 pDocs

1083 pDocs

1076 (map (expandParamsD rhs ist dec ps ns) decls)

1084 (map (expandParamsD rhs ist dec ps ns) decls)

1077−expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)

1085+expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n params ty cn decls)

1078− = PInstance info f

1086+ = PInstance doc argDocs info f

1079 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

1087 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

1080 n

1088 n

1081 (map (expandParams dec ps ns []) params)

1089 (map (expandParams dec ps ns []) params)

@@ -1292,8 +1300,10 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

1292 getImps (Bind n (Pi _ t _) sc) imps

1300 getImps (Bind n (Pi _ t _) sc) imps

1293 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

1301 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

1294 where

1302 where

1303+ argInfo n (Imp opt _ _ _) Placeholder

1304+ = (True, PImp 0 True opt n Placeholder)

1295 argInfo n (Imp opt _ _ _) t'

1305 argInfo n (Imp opt _ _ _) t'

1296− = (True, PImp (getPriority i t') True opt n t')

1306+ = (False, PImp (getPriority i t') True opt n t')

1297 argInfo n (Exp opt _ _) t'

1307 argInfo n (Exp opt _ _) t'

1298 = (InaccessibleArg `elem` opt,

1308 = (InaccessibleArg `elem` opt,

1299 PExp (getPriority i t') opt n t')

1309 PExp (getPriority i t') opt n t')

@@ -1542,7 +1552,7 @@ addImpl' inpat env infns ist ptm

1542 PLam fc n ty' sc'

1552 PLam fc n ty' sc'

1543 _ -> ai qq env ds (PLam fc (sMN 0 "lamp") ty

1553 _ -> ai qq env ds (PLam fc (sMN 0 "lamp") ty

1544 (PCase fc (PRef fc (sMN 0 "lamp") )

1554 (PCase fc (PRef fc (sMN 0 "lamp") )

1545− [(PRef fc n, sc)]))

1555+ [(PRef fc n, sc)]))

1546 ai qq env ds (PLet fc n ty val sc)

1556 ai qq env ds (PLet fc n ty val sc)

1547 = case lookupDef n (tt_ctxt ist) of

1557 = case lookupDef n (tt_ctxt ist) of

1548 [] -> let ty' = ai qq env ds ty

1558 [] -> let ty' = ai qq env ds ty

@@ -1716,7 +1726,7 @@ stripLinear i tm = evalState (sl tm) [] where

1716 sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')

1726 sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')

1717 sl (PDPair fc p l t r) = do l' <- sl l

1727 sl (PDPair fc p l t r) = do l' <- sl l

1718 t' <- sl t

1728 t' <- sl t

1719− r' <- sl r

1729+ r' <- sl r

1720 return (PDPair fc p l' t' r')

1730 return (PDPair fc p l' t' r')

1721 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var

1731 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var

1722 args' <- mapM slA args

1732 args' <- mapM slA args

@@ -1915,11 +1925,11 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1915 match (PHidden x) (PHidden y)

1925 match (PHidden x) (PHidden y)

1916 | RightOK xs <- match x y = return xs -- to collect variables

1926 | RightOK xs <- match x y = return xs -- to collect variables

1917 | otherwise = return [] -- Otherwise hidden things are unmatchable

1927 | otherwise = return [] -- Otherwise hidden things are unmatchable

1918− match (PHidden x) y

1928+ match (PHidden x) y

1919− | RightOK xs <- match x y = return xs

1929+ | RightOK xs <- match x y = return xs

1920 | otherwise = return []

1930 | otherwise = return []

1921− match x (PHidden y)

1931+ match x (PHidden y)

1922− | RightOK xs <- match x y = return xs

1932+ | RightOK xs <- match x y = return xs

1923 | otherwise = return []

1933 | otherwise = return []

1924 match (PUnifyLog x) y = match' x y

1934 match (PUnifyLog x) y = match' x y

1925 match x (PUnifyLog y) = match' x y

1935 match x (PUnifyLog y) = match' x y

src/Idris/AbsSyntaxTree.hs+39−30

@@ -57,7 +57,7 @@ data ElabInfo = EInfo { params :: [(Name, PTerm)],

57 liftname :: Name -> Name,

58 namespace :: Maybe [String],

59 elabFC :: Maybe FC,

60− rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->

60+ rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->

61 Idris () }

62

63toplevel :: ElabInfo

@@ -225,7 +225,8 @@ data IState = IState {

225 idris_callswho :: Maybe (M.Map Name [Name]),

226 idris_repl_defs :: [Name], -- ^ List of names that were defined in the repl, and can be re-/un-defined

227 elab_stack :: [Name], -- ^ Stack of names currently being elaborated

228− idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)

228+ idris_symbols :: M.Map Name Name, -- ^ Symbol table (preserves sharing of names)

229+ idris_exports :: [Name] -- ^ Functions with ExportList

229 }

230 }

230

231

231-- Required for parsers library, and therefore trifecta

232-- Required for parsers library, and therefore trifecta

@@ -297,6 +298,7 @@ data IBCWrite = IBCFix FixDecl

297 | IBCParsedRegion FC

298 | IBCParsedRegion FC

298 | IBCModDocs Name -- ^ The name is the special name used to track module docs

299 | IBCModDocs Name -- ^ The name is the special name used to track module docs

299 | IBCUsage (Name, Int)

300 | IBCUsage (Name, Int)

301+ | IBCExport Name

300 deriving Show

302 deriving Show

301

303

302-- | The initial state for the compiler

304-- | The initial state for the compiler

@@ -309,7 +311,7 @@ idrisInit = IState initContext [] []

309 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

311 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

310 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

312 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

311 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

313 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

312− AutomaticWidth S.empty [] Nothing Nothing [] [] M.empty

314+ AutomaticWidth S.empty [] Nothing Nothing [] [] M.empty []

313

315

314-- | The monad for the main REPL - reading and processing files and updating

316-- | The monad for the main REPL - reading and processing files and updating

315-- global state (hence the IO inner monad).

317-- global state (hence the IO inner monad).

@@ -336,6 +338,8 @@ data Codegen = Via String

336deriving instance NFData Codegen

338deriving instance NFData Codegen

337!-}

339!-}

338

340

341+data HowMuchDocs = FullDocs | OverviewDocs

342+

339-- | REPL commands

343-- | REPL commands

340data Command = Quit

344data Command = Quit

341 | Help

345 | Help

@@ -343,7 +347,7 @@ data Command = Quit

343 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.

347 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.

344 | Undefine [Name]

348 | Undefine [Name]

345 | Check PTerm

349 | Check PTerm

346− | DocStr (Either Name Const)

350+ | DocStr (Either Name Const) HowMuchDocs

347 | TotCheck Name

351 | TotCheck Name

348 | Reload

352 | Reload

349 | Load FilePath (Maybe Int) -- up to maximum line number

353 | Load FilePath (Maybe Int) -- up to maximum line number

@@ -417,6 +421,7 @@ data Opt = Filename String

417 | NoREPL

421 | NoREPL

418 | OLogging Int

422 | OLogging Int

419 | Output String

423 | Output String

424+ | Interface

420 | TypeCase

425 | TypeCase

421 | TypeInType

426 | TypeInType

422 | DefaultTotal

427 | DefaultTotal

@@ -596,19 +601,24 @@ data PDecl' t

596 [PDecl' t] -- declarations

601 [PDecl' t] -- declarations

597 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

602 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

598 -- class name, parameters, method declarations

603 -- class name, parameters, method declarations

604+ | PInstance

605+ (Docstring (Either Err PTerm)) -- Instance docs

606+ [(Name, Docstring (Either Err PTerm))] -- Parameter docs

607+ SyntaxInfo

599− | PInstance SyntaxInfo FC [(Name, t)] -- constraints

608+ FC [(Name, t)] -- constraints

600− Name -- class

609+ Name -- class

601− [t] -- parameters

610+ [t] -- parameters

602− t -- full instance type

611+ t -- full instance type

603− (Maybe Name) -- explicit name

612+ (Maybe Name) -- explicit name

604− [PDecl' t]

613+ [PDecl' t]

605− -- ^ Instance declaration: arguments are syntax info, source location, constraints,

614+ -- ^ Instance declaration: arguments are documentation, syntax info, source

615+ -- location, constraints, class name, parameters, full instance

606− -- class name, parameters, full instance type, optional explicit name, and definitions

616+ -- type, optional explicit name, and definitions

607 | PDSL Name (DSL' t) -- ^ DSL declaration

617 | PDSL Name (DSL' t) -- ^ DSL declaration

608 | PSyntax FC Syntax -- ^ Syntax definition

618 | PSyntax FC Syntax -- ^ Syntax definition

609 | PMutual FC [PDecl' t] -- ^ Mutual block

619 | PMutual FC [PDecl' t] -- ^ Mutual block

610 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.

620 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.

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

612 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If

622 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If

613 -- bool is True, lhs and rhs must be convertible

623 -- bool is True, lhs and rhs must be convertible

614 deriving Functor

624 deriving Functor

@@ -683,7 +693,7 @@ declared (PParams _ _ ds) = concatMap declared ds

683declared (PNamespace _ ds) = concatMap declared ds

693declared (PNamespace _ ds) = concatMap declared ds

684declared (PRecord _ _ _ n _ _ _ (Just c) _ _) = [n, c]

694declared (PRecord _ _ _ n _ _ _ (Just c) _ _) = [n, c]

685declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms

695declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms

686−declared (PInstance _ _ _ _ _ _ _ _) = []

696+declared (PInstance _ _ _ _ _ _ _ _ _ _) = []

687declared (PDSL n _) = [n]

697declared (PDSL n _) = [n]

688declared (PSyntax _ _) = []

698declared (PSyntax _ _) = []

689declared (PMutual _ ds) = concatMap declared ds

699declared (PMutual _ ds) = concatMap declared ds

@@ -703,7 +713,7 @@ tldeclared (PParams _ _ ds) = []

703tldeclared (PMutual _ ds) = concatMap tldeclared ds

713tldeclared (PMutual _ ds) = concatMap tldeclared ds

704tldeclared (PNamespace _ ds) = concatMap tldeclared ds

714tldeclared (PNamespace _ ds) = concatMap tldeclared ds

705tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms

715tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms

706−tldeclared (PInstance _ _ _ _ _ _ _ _) = []

716+tldeclared (PInstance _ _ _ _ _ _ _ _ _ _) = []

707tldeclared _ = []

717tldeclared _ = []

708

718

709defined :: PDecl -> [Name]

719defined :: PDecl -> [Name]

@@ -719,7 +729,7 @@ defined (PParams _ _ ds) = concatMap defined ds

719defined (PNamespace _ ds) = concatMap defined ds

729defined (PNamespace _ ds) = concatMap defined ds

720defined (PRecord _ _ _ n _ _ _ (Just c) _ _) = [n, c]

730defined (PRecord _ _ _ n _ _ _ (Just c) _ _) = [n, c]

721defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms

731defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms

722−defined (PInstance _ _ _ _ _ _ _ _) = []

732+defined (PInstance _ _ _ _ _ _ _ _ _ _) = []

723defined (PDSL n _) = [n]

733defined (PDSL n _) = [n]

724defined (PSyntax _ _) = []

734defined (PSyntax _ _) = []

725defined (PMutual _ ds) = concatMap defined ds

735defined (PMutual _ ds) = concatMap defined ds

@@ -774,7 +784,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

774 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)

784 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)

775 | PHidden PTerm -- ^ Irrelevant or hidden pattern

785 | PHidden PTerm -- ^ Irrelevant or hidden pattern

776 | PType -- ^ 'Type' type

786 | PType -- ^ 'Type' type

777− | PUniverse Universe -- ^ Some universe

787+ | PUniverse Universe -- ^ Some universe

778 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions

788 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions

779 | PConstant Const -- ^ Builtin types

789 | PConstant Const -- ^ Builtin types

780 | Placeholder -- ^ Underscore

790 | Placeholder -- ^ Underscore

@@ -1109,7 +1119,7 @@ data SSymbol = Keyword Name

1109 | Expr Name

1119 | Expr Name

1110 | SimpleExpr Name

1120 | SimpleExpr Name

1111 deriving (Show, Eq)

1121 deriving (Show, Eq)

1112−

1122+

1113

1123

1114{-!

1124{-!

1115deriving instance Binary SSymbol

1125deriving instance Binary SSymbol

@@ -1158,7 +1168,7 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules

1158

1168

1159initDSL = DSL (PRef f (sUN ">>="))

1169initDSL = DSL (PRef f (sUN ">>="))

1160 (PRef f (sUN "return"))

1170 (PRef f (sUN "return"))

1161− (PRef f (sUN "<$>"))

1171+ (PRef f (sUN "<*>"))

1162 (PRef f (sUN "pure"))

1172 (PRef f (sUN "pure"))

1163 Nothing

1173 Nothing

1164 Nothing

1174 Nothing

@@ -1384,7 +1394,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1384 where

1394 where

1385 startPrec = 0

1395 startPrec = 0

1386 funcAppPrec = 10

1396 funcAppPrec = 10

1387−

1397+

1388 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1398 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1389 prettySe p bnd (PQuote r) =

1399 prettySe p bnd (PQuote r) =

1390 text "![" <> pretty r <> text "]"

1400 text "![" <> pretty r <> text "]"

@@ -1447,7 +1457,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1447 [x] -> group (opName True <$> group (prettySe startPrec bnd (getTm x)))

1457 [x] -> group (opName True <$> group (prettySe startPrec bnd (getTm x)))

1448 [l,r] -> let precedence = maybe (startPrec - 1) prec f

1458 [l,r] -> let precedence = maybe (startPrec - 1) prec f

1449 in bracket p precedence $ inFix (getTm l) (getTm r)

1459 in bracket p precedence $ inFix (getTm l) (getTm r)

1450− (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->

1460+ (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->

1451 bracket p funcAppPrec $

1461 bracket p funcAppPrec $

1452 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>

1462 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>

1453 align (group (vsep (map (prettyArgS bnd) rest)))

1463 align (group (vsep (map (prettyArgS bnd) rest)))

@@ -1463,7 +1473,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1463 Just (Infixr p') -> p'

1473 Just (Infixr p') -> p'

1464 Just f' -> prec f' + 1

1474 Just f' -> prec f' + 1

1465 inFix l r = align . group $

1475 inFix l r = align . group $

1466− (prettySe left bnd l <+> opName False) <$>

1476+ (prettySe left bnd l <+> opName False) <$>

1467 group (prettySe right bnd r)

1477 group (prettySe right bnd r)

1468 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo

1478 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo

1469 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1479 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

@@ -1482,7 +1492,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1482 align $ kwd "case" <+> prettySe startPrec bnd scr <+> kwd "of" <$>

1492 align $ kwd "case" <+> prettySe startPrec bnd scr <+> kwd "of" <$>

1483 indent 2 (vsep (map ppcase cases))

1493 indent 2 (vsep (map ppcase cases))

1484 where

1494 where

1485− ppcase (l, r) = let prettyCase = prettySe startPrec

1495+ ppcase (l, r) = let prettyCase = prettySe startPrec

1486 ([(n, False) | n <- vars l] ++ bnd)

1496 ([(n, False) | n <- vars l] ++ bnd)

1487 in nest nestingSize $

1497 in nest nestingSize $

1488 prettyCase l <+> text "=>" <+> prettyCase r

1498 prettyCase l <+> text "=>" <+> prettyCase r

@@ -1553,7 +1563,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1553 prettyAs =

1563 prettyAs =

1554 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as

1564 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as

1555 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"

1565 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)

1557 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))

1567 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))

1558 -- XXX: add pretty for tactics

1568 -- XXX: add pretty for tactics

1559 prettySe p bnd (PProof ts) =

1569 prettySe p bnd (PProof ts) =

@@ -1725,7 +1735,7 @@ showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <>

1725showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1735showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1726showDeclImp o (PClass _ _ _ cs n ps _ ds)

1736showDeclImp o (PClass _ _ _ cs n ps _ ds)

1727 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

1737 = 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)

1729 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

1739 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

1730showDeclImp _ _ = text "..."

1740showDeclImp _ _ = text "..."

1731-- showDeclImp (PImport o) = "import " ++ o

1741-- showDeclImp (PImport o) = "import " ++ o

@@ -1901,16 +1911,16 @@ implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

1901implicitNamesIn uvars ist tm = nub $ ni [] tm

1911implicitNamesIn uvars ist tm = nub $ ni [] tm

1902 where

1912 where

1903 ni env (PRef _ n)

1913 ni env (PRef _ n)

1904− | not (n `elem` env)

1914+ | not (n `elem` env)

1905 = case lookupTy n (tt_ctxt ist) of

1915 = case lookupTy n (tt_ctxt ist) of

1906 [] -> [n]

1916 [] -> [n]

1907 _ -> if n `elem` uvars then [n] else []

1917 _ -> if n `elem` uvars then [n] else []

1908− ni env (PApp _ f@(PRef _ n) as)

1918+ ni env (PApp _ f@(PRef _ n) as)

1909 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)

1919 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)

1910 | otherwise = concatMap (ni env) (map getTm as)

1920 | otherwise = concatMap (ni env) (map getTm as)

1911 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1921 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1912 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1922 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 ++

1914 -- names in 'os', not counting the names bound in the cases

1924 -- names in 'os', not counting the names bound in the cases

1915 (nub (concatMap (ni env) (map snd os))

1925 (nub (concatMap (ni env) (map snd os))

1916 \\ nub (concatMap (ni env) (map fst os)))

1926 \\ nub (concatMap (ni env) (map fst os)))

@@ -1940,7 +1950,7 @@ namesIn uvars ist tm = nub $ ni [] tm

1940 _ -> if n `elem` (map fst uvars) then [n] else []

1950 _ -> if n `elem` (map fst uvars) then [n] else []

1941 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1951 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1942 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1952 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 ++

1944 -- names in 'os', not counting the names bound in the cases

1954 -- names in 'os', not counting the names bound in the cases

1945 (nub (concatMap (ni env) (map snd os))

1955 (nub (concatMap (ni env) (map snd os))

1946 \\ nub (concatMap (ni env) (map fst os)))

1956 \\ nub (concatMap (ni env) (map fst os)))

@@ -1999,4 +2009,3 @@ getErasureInfo ist n =

1999 case lookupCtxtExact n (idris_optimisation ist) of

2009 case lookupCtxtExact n (idris_optimisation ist) of

2000 Just (Optimise inacc detagg) -> map fst inacc

2010 Just (Optimise inacc detagg) -> map fst inacc

2001 Nothing -> []

2011 Nothing -> []

2002−

src/Idris/CmdOptions.hs+1

@@ -83,6 +83,7 @@ parseFlags = many $

83 <|> flag' NoREPL (long "check" <> help "Typecheck only, don't start the REPL")

84 <|> (Output <$> strOption (short 'o' <> long "output" <> metavar "FILE" <> help "Specify output file"))

85 -- <|> flag' TypeCase (long "typecase")

86+ <|> flag' Interface (long "interface" <> help "Generate interface files from ExportLists")

86 <|> flag' TypeInType (long "typeintype")

87 <|> flag' TypeInType (long "typeintype")

87 <|> flag' DefaultTotal (long "total" <> help "Require functions to be total by default")

88 <|> flag' DefaultTotal (long "total" <> help "Require functions to be total by default")

88 <|> flag' DefaultPartial (long "partial")

89 <|> flag' DefaultPartial (long "partial")

src/Idris/Core/Elaborate.hs−7

@@ -28,13 +28,6 @@ import Debug.Trace

28

29import Util.Pretty hiding (fill)

30

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−

38data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))

31data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))

39 deriving Show

32 deriving Show

40

33

src/Idris/DSL.hs+40−8

@@ -2,6 +2,8 @@

2

3module Idris.DSL where

4

5+import Data.Generics.Uniplate.Data (transform)

6+

5import Idris.AbsSyntax

7import Idris.AbsSyntax

6

8

7import Idris.Core.TT

9import Idris.Core.TT

@@ -13,25 +15,55 @@ import Debug.Trace

13debindApp :: SyntaxInfo -> PTerm -> PTerm

15debindApp :: SyntaxInfo -> PTerm -> PTerm

14debindApp syn t = debind (dsl_bind (dsl_info syn)) t

16debindApp syn t = debind (dsl_bind (dsl_info syn)) t

15

17

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+

16desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

26desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

17−desugar syn i t = let t' = expandDo (dsl_info syn) t in

27+desugar syn i t = let t' = expandDo (dsl_info syn) t

18− t' -- addImpl i 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"

19

46

20expandDo :: DSL -> PTerm -> PTerm

47expandDo :: DSL -> PTerm -> PTerm

21expandDo dsl (PLam fc n ty tm)

48expandDo dsl (PLam fc n ty tm)

22 | Just lam <- dsl_lambda dsl

49 | Just lam <- dsl_lambda dsl

50+ = let sc = PApp fc lam [ pexp (mkTTName fc n)

23− = let sc = PApp fc lam [pexp (var dsl n tm 0)] in

51+ , pexp (var dsl n tm 0)]

24− expandDo dsl sc

52+ in expandDo dsl sc

25expandDo dsl (PLam fc n ty tm) = PLam fc n (expandDo dsl ty) (expandDo dsl tm)

53expandDo dsl (PLam fc n ty tm) = PLam fc n (expandDo dsl ty) (expandDo dsl tm)

26expandDo dsl (PLet fc n ty v tm)

54expandDo dsl (PLet fc n ty v tm)

27 | Just letb <- dsl_let dsl

55 | Just letb <- dsl_let dsl

28− = let sc = PApp (fileFC "(dsl)") letb [pexp v, pexp (var dsl n tm 0)] in

56+ = let sc = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)

57+ , pexp v

58+ , pexp (var dsl n tm 0)]

29− expandDo dsl sc

59+ in expandDo dsl sc

30expandDo dsl (PLet fc n ty v tm) = PLet fc n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)

60expandDo dsl (PLet fc n ty v tm) = PLet fc n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)

31expandDo dsl (PPi p n ty tm)

61expandDo dsl (PPi p n ty tm)

32 | Just pi <- dsl_pi dsl

62 | Just pi <- dsl_pi dsl

63+ = let sc = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)

64+ , pexp ty

33− = let sc = PApp (fileFC "(dsl)") pi [pexp ty, pexp (var dsl n tm 0)] in

65+ , pexp (var dsl n tm 0)]

34− expandDo dsl sc

66+ in expandDo dsl sc

35expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

67expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

36expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

68expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

37 (map (fmap (expandDo dsl)) args)

69 (map (fmap (expandDo dsl)) args)

src/Idris/DeepSeq.hs+7−7

@@ -153,17 +153,20 @@ instance (NFData t) => NFData (PDecl' t) where

153 = rnf x1 `seq`

154 rnf x2 `seq`

155 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

156− rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8)

156+ rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

157 = rnf x1 `seq`

158 rnf x2 `seq`

159 rnf x3 `seq`

160+ rnf x4 `seq`

161+ rnf x5 `seq`

162+ rnf x6 `seq`

160− rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

163+ rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()

161 rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

164 rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

162 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

165 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

163 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

166 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

164 rnf (PDirective x1) = ()

167 rnf (PDirective x1) = ()

165− rnf (PProvider x1 x2 x3 x4)

168+ rnf (PProvider x1 x2 x3 x4 x5)

166− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

169+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

167 rnf (PTransform x1 x2 x3 x4)

170 rnf (PTransform x1 x2 x3 x4)

168 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

171 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

169

172

@@ -357,6 +360,3 @@ instance NFData SyntaxInfo where

357 rnf x4 `seq`

360 rnf x4 `seq`

358 rnf x5 `seq`

361 rnf x5 `seq`

359 rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

362 rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

360−

361−

362−

src/Idris/Docs.hs+89−39

@@ -1,12 +1,12 @@

1−{-# LANGUAGE PatternGuards #-}

1+{-# LANGUAGE DeriveFunctor, PatternGuards #-}

2−module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc(..), Docs (..)) where

2+module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc, FunDoc'(..), Docs, Docs'(..)) where

3

4import Idris.AbsSyntax

5import Idris.AbsSyntaxTree

6import Idris.Delaborate

7import Idris.Core.TT

8import 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)

10

11import Util.Pretty

12

@@ -18,21 +18,28 @@ import qualified Data.Text as T

18--

19-- Issue #1573 on the Issue tracker.

20-- https://github.com/idris-lang/Idris-dev/issues/1573

21−data FunDoc = FD Name (Docstring DocTerm)

21+data FunDoc' d = FD Name d

22− [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))] -- args: name, ty, implicit, docs

22+ [(Name, PTerm, Plicity, Maybe d)] -- args: name, ty, implicit, docs

23− PTerm -- function type

23+ PTerm -- function type

24− (Maybe Fixity)

24+ (Maybe Fixity)

25−

25+ deriving Functor

26+

27+type FunDoc = FunDoc' (Docstring DocTerm)

28+

26−data Docs = FunDoc FunDoc

29+data Docs' d = FunDoc (FunDoc' d)

27− | DataDoc FunDoc -- type constructor docs

30+ | DataDoc (FunDoc' d) -- type constructor docs

28− [FunDoc] -- data constructor docs

31+ [FunDoc' d] -- data constructor docs

29− | ClassDoc Name (Docstring DocTerm)-- class docs

32+ | ClassDoc Name d -- class docs

30− [FunDoc] -- method docs

33+ [FunDoc' d] -- method docs

31− [(Name, Maybe (Docstring DocTerm))] -- parameters and their docstrings

34+ [(Name, Maybe d)] -- parameters and their docstrings

32− [PTerm] -- instances

35+ [(PTerm, (d, [(Name, d)]))] -- instances

36+ [PTerm] -- subclasses

33− [PTerm] -- superclasses

37+ [PTerm] -- superclasses

34− | ModDoc [String] -- Module name

38+ | ModDoc [String] -- Module name

39+ d

40+ deriving Functor

41+

35− (Docstring DocTerm)

42+type Docs = Docs' (Docstring DocTerm)

36

43

37showDoc ist d

44showDoc ist d

38 | nullDocstring d = empty

45 | nullDocstring d = empty

@@ -82,7 +89,7 @@ pprintDocs ist (DataDoc t args)

82 if null args then text "No constructors."

89 if null args then text "No constructors."

83 else nest 4 (text "Constructors:" <> line <>

90 else nest 4 (text "Constructors:" <> line <>

84 vsep (map (pprintFD ist) args))

91 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)

86 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>

93 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>

87 if nullDocstring doc

94 if nullDocstring doc

88 then empty

95 then empty

@@ -94,8 +101,8 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

94 vsep (map (pprintFD ist) meths))

101 vsep (map (pprintFD ist) meths))

95 <$>

102 <$>

96 nest 4 (text "Instances:" <$>

103 nest 4 (text "Instances:" <$>

97− vsep (if null instances' then [text "<no instances>"]

104+ vsep (if null instances then [text "<no instances>"]

98− else map dumpInstance instances'))

105+ else map pprintInstance instances))

99 <>

106 <>

100 (if null subclasses then empty

107 (if null subclasses then empty

101 else line <$> nest 4 (text "Subclasses:" <$>

108 else line <$> nest 4 (text "Subclasses:" <$>

@@ -112,6 +119,30 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

112 ppo = ppOptionIst ist

119 ppo = ppOptionIst ist

113 infixes = idris_infixes ist

120 infixes = idris_infixes ist

114

121

122+ pprintInstance (term, (doc, argDocs)) =

123+ nest 4 (dumpInstance term <>

124+ (if nullDocstring doc

125+ then empty

126+ else line <>

127+ renderDocstring

128+ (renderDocTerm

129+ (pprintDelab ist)

130+ (normaliseAll (tt_ctxt ist) []))

131+ doc) <>

132+ if null argDocs

133+ then empty

134+ else line <> vsep (map (prettyInstanceParam (map fst argDocs)) argDocs))

135+

136+ prettyInstanceParam params (name, doc) =

137+ if nullDocstring doc

138+ then empty

139+ else prettyName True False (zip params (repeat False)) name <+>

140+ showDoc ist doc

141+

142+-- if any (isJust . snd) params

143+-- then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)

144+-- else hsep (punctuate comma (map (prettyName True False params' . fst) params))

145+

115 dumpInstance :: PTerm -> Doc OutputAnnotation

146 dumpInstance :: PTerm -> Doc OutputAnnotation

116 dumpInstance = pprintPTerm ppo params' [] infixes

147 dumpInstance = pprintPTerm ppo params' [] infixes

117

148

@@ -134,33 +165,38 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

134 isSubclass (PPi _ _ _ pt) = isSubclass pt

165 isSubclass (PPi _ _ _ pt) = isSubclass pt

135 isSubclass _ = False

166 isSubclass _ = False

136

167

137− (subclasses, instances') = partition isSubclass instances

168+ prettyParameters =

138−

139− prettyParameters = if any (isJust . snd) params

169+ if any (isJust . snd) params

140− then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)

170+ then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)

141− else hsep (punctuate comma (map (prettyName True False params' . fst) params))

171+ else hsep (punctuate comma (map (prettyName True False params' . fst) params))

142

172

143pprintDocs ist (ModDoc mod docs)

173pprintDocs ist (ModDoc mod docs)

144 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>

174 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>

145 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) docs

175 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) docs

146

176

177+-- | Determine a truncation function depending how much docs the user

178+-- wants to see

179+howMuch FullDocs = id

180+howMuch OverviewDocs = overview

181+

147-- | Given a fully-qualified, disambiguated name, construct the

182-- | Given a fully-qualified, disambiguated name, construct the

148-- documentation object for it

183-- documentation object for it

149−getDocs :: Name -> Idris Docs

184+getDocs :: Name -> HowMuchDocs -> Idris Docs

150−getDocs n@(NS n' ns) | n' == modDocName

185+getDocs n@(NS n' ns) w | n' == modDocName

151 = do i <- getIState

186 = do i <- getIState

152 case lookupCtxtExact n (idris_moduledocs i) of

187 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

154 Nothing -> fail $ "Module docs for " ++ show (reverse (map T.unpack ns)) ++

189 Nothing -> fail $ "Module docs for " ++ show (reverse (map T.unpack ns)) ++

155 " do not exist! This shouldn't have happened and is a bug."

190 " do not exist! This shouldn't have happened and is a bug."

156−getDocs n

191+getDocs n w

157 = do i <- getIState

192 = do i <- getIState

158− case lookupCtxt n (idris_classes i) of

193+ docs <- case lookupCtxt n (idris_classes i) of

159− [ci] -> docClass n ci

194+ [ci] -> docClass n ci

160− _ -> case lookupCtxt n (idris_datatypes i) of

195+ _ -> case lookupCtxt n (idris_datatypes i) of

161− [ti] -> docData n ti

196+ [ti] -> docData n ti

162− _ -> do fd <- docFun n

197+ _ -> do fd <- docFun n

163− return (FunDoc fd)

198+ return (FunDoc fd)

199+ return $ fmap (howMuch w) docs

164

200

165docData :: Name -> TypeInfo -> Idris Docs

201docData :: Name -> TypeInfo -> Idris Docs

166docData n ti

202docData n ti

@@ -174,14 +210,28 @@ docClass n ci

174 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

210 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

175 docstr = maybe emptyDocstring fst docStrings

211 docstr = maybe emptyDocstring fst docStrings

176 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd))) (class_params ci)

212 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd))) (class_params ci)

213+ instanceDocs = map (fromMaybe (emptyDocstring, []) .

214+ listToMaybe .

215+ flip lookupCtxt (idris_docstrings i))

216+ (class_instances ci)

177− instances = map (delabTy i) (class_instances ci)

217+ instances = zip (map (delabTy i) (class_instances ci)) instanceDocs

218+ (subclasses, instances') = partition (isSubclass . fst) instances

178 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

219 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

179 mdocs <- mapM (docFun . fst) (class_methods ci)

220 mdocs <- mapM (docFun . fst) (class_methods ci)

221+ return $ ClassDoc

180− return $ ClassDoc n docstr mdocs params instances superclasses

222+ n docstr mdocs params

223+ instances' (map fst subclasses) superclasses

181 where

224 where

182− getDInst (PInstance _ _ _ _ _ t _ _) = Just t

225+ getDInst (PInstance _ _ _ _ _ _ _ t _ _) = Just t

183 getDInst _ = Nothing

226 getDInst _ = Nothing

184

227

228+ isSubclass (PPi (Constraint _ _) _ (PApp _ _ args) (PApp _ (PRef _ nm) args'))

229+ = nm == n && map getTm args == map getTm args'

230+ isSubclass (PPi _ _ _ pt)

231+ = isSubclass pt

232+ isSubclass _

233+ = False

234+

185docFun :: Name -> Idris FunDoc

235docFun :: Name -> Idris FunDoc

186docFun n

236docFun n

187 = do i <- getIState

237 = do i <- getIState

src/Idris/Elab/Class.hs+7−9

@@ -109,8 +109,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

109 mdec x = x

110

111 -- TODO: probably should normalise

112− checkDefaultSuperclassInstance :: PDecl -> Idris ()

112+ checkDefaultSuperclassInstance :: PDecl -> Idris ()

113− checkDefaultSuperclassInstance (PInstance _ fc cs n ps _ _ _)

113+ checkDefaultSuperclassInstance (PInstance _ _ _ fc cs n ps _ _ _)

114 = do when (not $ null cs) . tclift

115 $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))

116 i <- getIState

@@ -120,11 +120,11 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

120 $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))

121 return ()

122

123− impbind :: [(Name, PTerm)] -> PTerm -> PTerm

123+ impbind :: [(Name, PTerm)] -> PTerm -> PTerm

124 impbind [] x = x

125 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)

126

127− conbind :: [(Name, PTerm)] -> PTerm -> PTerm

127+ conbind :: [(Name, PTerm)] -> PTerm -> PTerm

128 conbind ((c, ty) : ns) x = PPi constraint c ty (conbind ns x)

129 conbind [] x = x

130

@@ -133,7 +133,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

133 = do t' <- implicit' info syn allmeths n t

134 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

135 return ( (n, (toExp (map fst ps) Exp t')),

136− (n, (doc, o, (toExp (map fst ps)

136+ (n, (doc, o, (toExp (map fst ps)

137 (\ l s p -> Imp l s p Nothing) t'))),

138 (n, (syn, o, t) ) )

139 tdecl _ _ = ifail "Not allowed in a class declaration"

@@ -155,7 +155,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

155

156 tydecl (PTy _ _ _ _ _ _ _) = True

157 tydecl _ = False

158− instdecl (PInstance _ _ _ _ _ _ _ _) = True

158+ instdecl (PInstance _ _ _ _ _ _ _ _ _ _) = True

159 instdecl _ = False

160 clause (PClauses _ _ _ _) = True

161 clause _ = False

@@ -221,7 +221,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

221

222 insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)

223 = PPi p n ty (insertConstraint c sc)

224− insertConstraint c sc = PPi (constraint { pstatic = Static })

224+ insertConstraint c sc = PPi (constraint { pstatic = Static })

225 (sMN 0 "class") c sc

226

227 -- make arguments explicit and don't bind class parameters

@@ -230,5 +230,3 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

230 | otherwise = PPi (e l s p) n ty (toExp ns e sc)

231 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

232 toExp ns e sc = sc

233−

234−

src/Idris/Elab/Instance.hs+7−5

@@ -51,6 +51,8 @@ import Data.List.Split (splitOn)

51import Util.Pretty(pretty, text)

52

53elabInstance :: ElabInfo -> SyntaxInfo ->

54+ Docstring (Either Err PTerm) ->

55+ [(Name, Docstring (Either Err PTerm))] ->

54 ElabWhat -> -- phase

56 ElabWhat -> -- phase

55 FC -> [(Name, PTerm)] -> -- constraints

57 FC -> [(Name, PTerm)] -> -- constraints

56 Name -> -- the class

58 Name -> -- the class

@@ -58,7 +60,7 @@ elabInstance :: ElabInfo -> SyntaxInfo ->

58 PTerm -> -- full instance type

60 PTerm -> -- full instance type

59 Maybe Name -> -- explicit name

61 Maybe Name -> -- explicit name

60 [PDecl] -> Idris ()

62 [PDecl] -> Idris ()

61−elabInstance info syn what fc cs n ps t expn ds = do

63+elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

62 i <- getIState

64 i <- getIState

63 (n, ci) <- case lookupCtxtName n (idris_classes i) of

65 (n, ci) <- case lookupCtxtName n (idris_classes i) of

64 [c] -> return c

66 [c] -> return c

@@ -69,7 +71,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

69 let iname = mkiname n (namespace info) ps expn

71 let iname = mkiname n (namespace info) ps expn

70 let emptyclass = null (class_methods ci)

72 let emptyclass = null (class_methods ci)

71 when (what /= EDefns || (null ds && not emptyclass)) $ do

73 when (what /= EDefns || (null ds && not emptyclass)) $ do

72− nty <- elabType' True info syn emptyDocstring [] fc [] iname t

74+ nty <- elabType' True info syn doc argDocs fc [] iname t

73 -- if the instance type matches any of the instances we have already,

75 -- if the instance type matches any of the instances we have already,

74 -- and it's not a named instance, then it's overlapping, so report an error

76 -- and it's not a named instance, then it's overlapping, so report an error

75 case expn of

77 case expn of

@@ -147,10 +149,10 @@ elabInstance info syn what fc cs n ps t expn ds = do

147 Just m -> sNS (SN (sInstanceN n' (map show ps'))) m

149 Just m -> sNS (SN (sInstanceN n' (map show ps'))) m

148 Just nm -> nm

150 Just nm -> nm

149

151

150− substInstance ips pnames (PInstance syn _ cs n ps t expn ds)

152+ substInstance ips pnames (PInstance doc argDocs syn _ cs n ps t expn ds)

151− = PInstance syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

153+ = PInstance doc argDocs syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

152

154

153− isOverlapping i (PInstance syn _ _ n ps t expn _)

155+ isOverlapping i (PInstance doc argDocs syn _ _ n ps t expn _)

154 = case lookupCtxtName n (idris_classes i) of

156 = case lookupCtxtName n (idris_classes i) of

155 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in

157 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in

156 case lookupTy iname (tt_ctxt i) of

158 case lookupTy iname (tt_ctxt i) of

src/Idris/Elab/Provider.hs+4−5

@@ -52,8 +52,8 @@ import Data.List.Split (splitOn)

52import Util.Pretty(pretty, text)

53

54-- | Elaborate a type provider

55−elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()

55+elabProvider :: Docstring (Either Err PTerm) -> ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()

56−elabProvider info syn fc what n

56+elabProvider doc info syn fc what n

57 = do i <- getIState

58 -- Ensure that the experimental extension is enabled

59 unless (TypeProviders `elem` idris_language_extensions i) $

@@ -93,12 +93,12 @@ elabProvider info syn fc what n

93 Provide tm

94 | ProvTerm ty _ <- what ->

95 do -- Finally add a top-level definition of the provided term

96− elabType info syn emptyDocstring [] fc [] n ty

96+ elabType info syn doc [] fc [] n ty

97 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

98 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

99 | ProvPostulate _ <- what ->

100 do -- Add the postulate

101− elabPostulate info syn (fmap (const (Left $ Msg "")) . parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)

101+ elabPostulate info syn doc fc [] n (delab i tm)

102 logLvl 3 $ "Elaborated provided postulate " ++ show n

103 | otherwise ->

104 ierror . Msg $ "Attempted to provide a postulate where a term was expected."

@@ -120,4 +120,3 @@ elabProvider info syn fc what n

120 case converts ctxt [] (providerOf tp) prov of

121 OK _ -> True

122 _ -> False

123−

src/Idris/Elab/Type.hs+9−1

@@ -90,7 +90,7 @@ buildType info syn fc opts n ty' = do

90 let (inaccData, impls) = unzip $ getUnboundImplicits i cty ty

91 let inacc = inaccessibleImps 0 cty inaccData

92 logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc ++

93− " from " ++ show (cty, ty)

93+ " from " ++ show cty ++ "\n" ++ showTmImpls ty

94

95 putIState $ i { idris_implicits = addDef n impls (idris_implicits i) }

96 logLvl 3 ("Implicit " ++ show n ++ " " ++ show impls)

@@ -181,6 +181,12 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

181 addIBC (IBCErrorHandler n)

182 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"

183 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."

184+ -- if it's an export list type, make a note of it

185+ case (unApply usety) of

186+ (P _ ut _, _)

187+ | ut == ffiexport -> do addIBC (IBCExport n)

188+ addExport n

189+ _ -> return ()

184 return usety

190 return usety

185 where

191 where

186 -- for making an internalapp, we only want the explicit ones, and don't

192 -- for making an internalapp, we only want the explicit ones, and don't

@@ -191,6 +197,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

191 | otherwise = mergeTy sc sc'

197 | otherwise = mergeTy sc sc'

192 mergeTy _ sc = sc

198 mergeTy _ sc = sc

193

199

200+ ffiexport = sNS (sUN "FFI_Export") ["FFI_Export"]

201+

194 err = txt "Err"

202 err = txt "Err"

195 maybe = txt "Maybe"

203 maybe = txt "Maybe"

196 lst = txt "List"

204 lst = txt "List"

src/Idris/ElabDecls.hs+6−7

@@ -200,11 +200,11 @@ elabDecl' what info (PMutual f ps)

200 where isDataDecl (PData _ _ _ _ _ _) = True

201 isDataDecl _ = False

202

203− setMutData ns n

203+ setMutData ns n

204 = do i <- getIState

205 case lookupCtxt n (idris_datatypes i) of

206 [x] -> do let x' = x { mutual_types = ns }

207− putIState $ i { idris_datatypes

207+ putIState $ i { idris_datatypes

208 = addDef n x' (idris_datatypes i) }

209 _ -> return ()

210

@@ -233,9 +233,9 @@ elabDecl' what info (PClass doc s f cs n ps pdocs ds)

233 | what /= EDefns

234 = do iLOG $ "Elaborating class " ++ show n

235 elabClass info (s { syn_params = [] }) doc f cs n ps pdocs ds

236−elabDecl' what info (PInstance s f cs n ps t expn ds)

236+elabDecl' what info (PInstance doc argDocs s f cs n ps t expn ds)

237 = do iLOG $ "Elaborating instance " ++ show n

238− elabInstance info s what f cs n ps t expn ds

238+ elabInstance info s doc argDocs what f cs n ps t expn ds

239elabDecl' what info (PRecord doc s f tyn ty opts cdoc cn args cty)

240 | what /= ETypes

241 = do iLOG $ "Elaborating record " ++ show tyn

@@ -249,12 +249,11 @@ elabDecl' _ info (PDSL n dsl)

249 addIBC (IBCDSL n)

250elabDecl' what info (PDirective i)

251 | what /= EDefns = i

252−elabDecl' what info (PProvider syn fc provWhat n)

252+elabDecl' what info (PProvider doc syn fc provWhat n)

253 | what /= EDefns

254 = do iLOG $ "Elaborating type provider " ++ show n

255− elabProvider info syn fc provWhat n

255+ elabProvider doc info syn fc provWhat n

256elabDecl' what info (PTransform fc safety old new)

257 = do elabTransform info fc safety old new

258 return ()

259elabDecl' _ _ _ = return () -- skipped this time

260−

src/Idris/ElabTerm.hs+41−24

@@ -1066,7 +1066,7 @@ elab ist info emode opts fn tm

1066 delayElab $ do focus h

1067 dotterm

1068 elab' ina fc t

1069− elab' ina _ (PRunTactics fc tm) =

1069+ elab' ina fc (PRunTactics fc' tm) =

1070 do attack

1071 n <- getNameFrom (sMN 0 "tacticScript")

1072 n' <- getNameFrom (sMN 0 "tacticExpr")

@@ -1075,10 +1075,10 @@ elab ist info emode opts fn tm

1075 movelast n

1076 letbind n' scriptTy (Var n)

1077 focus n

1078− elab' ina (Just fc) tm

1078+ elab' ina (Just fc') tm

1079 env <- get_env

1080 ctxt <- get_context

1081− runTactical fc ctxt env (P Bound n' Erased)

1081+ runTactical (maybe fc' id fc) ctxt env (P Bound n' Erased)

1082 solve

1083 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

1084

@@ -1508,7 +1508,7 @@ case_ ind autoSolve ist fn tm = do

1508runTactical :: FC -> Context -> Env -> Term -> ElabD ()

1509runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1510 where

1511− eval = normaliseAll ctxt env

1511+ eval = normaliseAll ctxt env . finalise

1512 tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]

1513 returnUnit = fmap fst $ get_type_val (Var unitCon)

1514

@@ -1540,6 +1540,9 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1540 else fmap fst . get_type_val $

1541 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))

1542 (Var (reflm "TT"))

1543+ | n == tacN "prim__SourceLocation", [] <- args

1544+ = fmap fst . get_type_val $

1545+ reflectFC fc

1543 | n == tacN "prim__Env", [] <- args

1546 | n == tacN "prim__Env", [] <- args

1544 = do env <- get_env

1547 = do env <- get_env

1545 fmap fst . get_type_val $ reflectEnv env

1548 fmap fst . get_type_val $ reflectEnv env

@@ -1547,7 +1550,7 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1547 = do parts <- reifyReportParts (eval errs)

1550 = do parts <- reifyReportParts (eval errs)

1548 lift . tfail $ ReflectionError [parts] (Msg "")

1551 lift . tfail $ ReflectionError [parts] (Msg "")

1549 | n == tacN "prim__PureTactical", [_a, tm] <- args

1552 | n == tacN "prim__PureTactical", [_a, tm] <- args

1550− = return tm

1553+ = return tm

1551 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args

1554 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args

1552 = do let first' = eval first

1555 = do let first' = eval first

1553 res <- runTacTm first'

1556 res <- runTacTm first'

@@ -1575,6 +1578,10 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1575 | n == tacN "prim__Attack", [] <- args

1578 | n == tacN "prim__Attack", [] <- args

1576 = do attack

1579 = do attack

1577 returnUnit

1580 returnUnit

1581+ | n == tacN "prim__Rewrite", [rule] <- args

1582+ = do r <- reifyRaw rule

1583+ rewrite r

1584+ returnUnit

1578 | n == tacN "prim__Focus", [what] <- args

1585 | n == tacN "prim__Focus", [what] <- args

1579 = do n' <- reifyTTName what

1586 = do n' <- reifyTTName what

1580 focus n'

1587 focus n'

@@ -1583,6 +1590,12 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1583 = do n' <- reifyTTName what

1590 = do n' <- reifyTTName what

1584 movelast n'

1591 movelast n'

1585 returnUnit

1592 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

1586 runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x

1599 runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x

1587

1600

1588-- Running tactics directly

1601-- Running tactics directly

@@ -1829,22 +1842,7 @@ runTac autoSolve ist perhapsFC fn tac

1829 case perhapsFC of

1842 case perhapsFC of

1830 Nothing -> lift . tfail $ Msg "There is no source location available."

1843 Nothing -> lift . tfail $ Msg "There is no source location available."

1831 Just fc ->

1844 Just fc ->

1832− do let intTy = RConstant (AType (ATInt ITNative))

1845+ do fill $ reflectFC fc

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− ]

1848 solve

1846 solve

1849 runT x = fail $ "Not implemented " ++ show x

1847 runT x = fail $ "Not implemented " ++ show x

1850

1848

@@ -1966,7 +1964,7 @@ reifyRaw t@(App _ _)

1966 | (P _ f _, args) <- unApply t = reifyRawApp f args

1964 | (P _ f _, args) <- unApply t = reifyRawApp f args

1967reifyRaw t@(P _ n _)

1965reifyRaw t@(P _ n _)

1968 | n == reflm "RType" = return $ RType

1966 | 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)

1970

1968

1971reifyRawApp :: Name -> [Term] -> ElabD Raw

1969reifyRawApp :: Name -> [Term] -> ElabD Raw

1972reifyRawApp t [n]

1970reifyRawApp t [n]

@@ -1982,7 +1980,7 @@ reifyRawApp t [t']

1982 | t == reflm "RForce" = liftM RForce (reifyRaw t')

1980 | t == reflm "RForce" = liftM RForce (reifyRaw t')

1983reifyRawApp t [c]

1981reifyRawApp t [c]

1984 | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)

1982 | 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))

1986

1984

1987reifyTTName :: Term -> ElabD Name

1985reifyTTName :: Term -> ElabD Name

1988reifyTTName t

1986reifyTTName t

@@ -2602,7 +2600,7 @@ reflectErr (NotInjective t1 t2 t3) =

2602reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2600reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2603reflectErr (CantResolveAlts ss) =

2601reflectErr (CantResolveAlts ss) =

2604 raw_apply (Var $ reflErrName "CantResolveAlts")

2602 raw_apply (Var $ reflErrName "CantResolveAlts")

2605− [rawList (Var $ (sUN "String")) (map Var ss)]

2603+ [rawList (Var $ reflm "TTName") (map reflectName ss)]

2606reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

2604reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

2607reflectErr UniverseError = Var $ reflErrName "UniverseError"

2605reflectErr UniverseError = Var $ reflErrName "UniverseError"

2608reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

2606reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

@@ -2617,6 +2615,25 @@ reflectErr (LoadingFailed str err) =

2617 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]

2615 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]

2618reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]

2616reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]

2619

2617

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+

2620elaboratingArgErr :: [(Name, Name)] -> Err -> Err

2637elaboratingArgErr :: [(Name, Name)] -> Err -> Err

2621elaboratingArgErr [] err = err

2638elaboratingArgErr [] err = err

2622elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)

2639elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)

src/Idris/Erasure.hs+19−15

@@ -65,12 +65,12 @@ type Vars = Map Name VarInfo

65

66-- Perform usage analysis, write the relevant information in the internal

67-- structures, returning the list of reachable names.

68−performUsageAnalysis :: Idris [Name]

68+performUsageAnalysis :: [Name] -> Idris [Name]

69−performUsageAnalysis = do

69+performUsageAnalysis roots = do

70 ctx <- tt_ctxt <$> getIState

71− mainName <- getMainName <$> getIState

71+ startNames <- getStartNames <$> getIState

72

73− case mainName of

73+ case startNames of

74 Left reason -> return [] -- no main -> not compiling -> reachability irrelevant

75 Right main -> do

76 ci <- idris_classes <$> getIState

@@ -106,11 +106,14 @@ performUsageAnalysis = do

106

107 return $ S.toList reachableNames

108 where

109− getMainName :: IState -> Either Err Name

109+ getStartNames :: IState -> Either Err [Name]

110+ getStartNames ist

110− getMainName ist = case lookupCtxtName n (idris_implicits ist) of

111+ = case lookupCtxtName n (idris_implicits ist) of

111− [(n', _)] -> Right n'

112+ [(n', _)] -> Right (n' : roots)

113+ [] -> if null roots

112− [] -> Left (NoSuchVariable n)

114+ then Left (NoSuchVariable n)

115+ else Right roots

113− more -> Left (CantResolveAlts (map fst more))

116+ more -> Left (CantResolveAlts (map fst more))

114 where

117 where

115 n = sNS (sUN "main") ["Main"]

118 n = sNS (sUN "main") ["Main"]

116

119

@@ -171,9 +174,9 @@ forwardChain deps

171

174

172-- Build the dependency graph,

175-- Build the dependency graph,

173-- starting the depth-first search from a list of Names.

176-- starting the depth-first search from a list of Names.

174−buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> Context -> Name -> Deps

177+buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> Context -> [Name] -> Deps

175−buildDepMap ci used ctx mainName = addPostulates used $

178+buildDepMap ci used ctx startNames = addPostulates used $

176− dfs S.empty M.empty [mainName]

179+ dfs S.empty M.empty startNames

177 where

180 where

178 -- mark the result of Main.main as used with the empty assumption

181 -- mark the result of Main.main as used with the empty assumption

179 addPostulates :: [(Name, Int)] -> Deps -> Deps

182 addPostulates :: [(Name, Int)] -> Deps -> Deps

@@ -191,10 +194,11 @@ buildDepMap ci used ctx mainName = addPostulates used $

191

194

192 postulates used =

195 postulates used =

193 [ [] ==> concat

196 [ [] ==> concat

194− -- These two, Main.main and run__IO, are always evaluated

197+ -- Main.main ( + export lists) and run__IO, are always evaluated

195 -- but they elude analysis since they come from the seed term.

198 -- but they elude analysis since they come from the seed term.

196− [ [(mainName, Result)]

199+ [(map (\n -> (n, Result)) startNames)

197− , [(sUN "run__IO", Result), (sUN "run__IO", Arg 1)]

200+ ,[(sUN "run__IO", Result), (sUN "run__IO", Arg 1)]

201+ ,[(sUN "call__IO", Result), (sUN "call__IO", Arg 2)]

198

202

199 -- Explicit usage declarations from a %used pragma

203 -- Explicit usage declarations from a %used pragma

200 , map (\(n, i) -> (n, Arg i)) used

204 , map (\(n, i) -> (n, Arg i)) used

src/Idris/IBC.hs+54−38

@@ -37,7 +37,7 @@ import Codec.Compression.Zlib (compress)

37import Util.Zlib (decompressEither)

38

39ibcVersion :: Word8

40−ibcVersion = 98

40+ibcVersion = 99

41

42data IBCFile = IBCFile { ver :: Word8,

43 sourcefile :: FilePath,

@@ -80,7 +80,8 @@ data IBCFile = IBCFile { ver :: Word8,

80 ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))],

81 ibc_postulates :: ![Name],

82 ibc_parsedSpan :: !(Maybe FC),

83− ibc_usage :: ![(Name, Int)]

83+ ibc_usage :: ![(Name, Int)],

84+ ibc_exports :: ![Name]

84 }

85 }

85 deriving Show

86 deriving Show

86{-!

87{-!

@@ -88,11 +89,11 @@ deriving instance Binary IBCFile

88!-}

89!-}

89

90

90initIBC :: IBCFile

91initIBC :: IBCFile

91−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing []

92+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] []

92

93

93−loadIBC :: Bool -- ^ True = reexport, False = make everything private

94+loadIBC :: Bool -- ^ True = reexport, False = make everything private

94 -> FilePath -> Idris ()

95 -> FilePath -> Idris ()

95−loadIBC reexport fp

96+loadIBC reexport fp

96 = do imps <- getImported

97 = do imps <- getImported

97 let redo = case lookup fp imps of

98 let redo = case lookup fp imps of

98 Nothing -> True

99 Nothing -> True

@@ -193,7 +194,7 @@ ibc i (IBCLib tgt n) f = return f { ibc_libs = (tgt, n) : ibc_libs f }

193ibc i (IBCCGFlag tgt n) f = return f { ibc_cgflags = (tgt, n) : ibc_cgflags f }

194ibc i (IBCCGFlag tgt n) f = return f { ibc_cgflags = (tgt, n) : ibc_cgflags f }

194ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }

195ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }

195ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }

196ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }

196−ibc i (IBCDef n) f

197+ibc i (IBCDef n) f

197 = do f' <- case lookupDefExact n (tt_ctxt i) of

198 = do f' <- case lookupDefExact n (tt_ctxt i) of

198 Just v -> return f { ibc_defs = (n,v) : ibc_defs f }

199 Just v -> return f { ibc_defs = (n,v) : ibc_defs f }

199 _ -> ifail "IBC write failed"

200 _ -> ifail "IBC write failed"

@@ -233,17 +234,18 @@ ibc i (IBCModDocs n) f = case lookupCtxtExact n (idris_moduledocs i) of

233 Just v -> return f { ibc_moduledocs = (n,v) : ibc_moduledocs f }

234 Just v -> return f { ibc_moduledocs = (n,v) : ibc_moduledocs f }

234 _ -> ifail "IBC write failed"

235 _ -> ifail "IBC write failed"

235ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f }

236ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f }

237+ibc i (IBCExport n) f = return f { ibc_exports = n : ibc_exports f }

236

238

237process :: Bool -- ^ Reexporting

239process :: Bool -- ^ Reexporting

238 -> IBCFile -> FilePath -> Idris ()

240 -> IBCFile -> FilePath -> Idris ()

239process reexp i fn

241process reexp i fn

240− | ver i /= ibcVersion

242+ | ver i /= ibcVersion

241 = do iLOG "ibc out of date"

243 = do iLOG "ibc out of date"

242 let e = if ver i < ibcVersion then " an earlier " else " a later "

244 let e = if ver i < ibcVersion then " an earlier " else " a later "

243 ifail $ "Incompatible ibc version.\nThis library was built with"

245 ifail $ "Incompatible ibc version.\nThis library was built with"

244 ++ e ++ "version of Idris.\n" ++

246 ++ e ++ "version of Idris.\n" ++

245 "Please clean and rebuild."

247 "Please clean and rebuild."

246−

248+

247 --- please rebuild"

249 --- please rebuild"

248 | otherwise =

250 | otherwise =

249 do srcok <- runIO $ doesFileExist (sourcefile i)

251 do srcok <- runIO $ doesFileExist (sourcefile i)

@@ -290,6 +292,7 @@ process reexp i fn

290 pPostulates $ force (ibc_postulates i)

292 pPostulates $ force (ibc_postulates i)

291 pParsedSpan $ force (ibc_parsedSpan i)

293 pParsedSpan $ force (ibc_parsedSpan i)

292 pUsage $ force (ibc_usage i)

294 pUsage $ force (ibc_usage i)

295+ pExports $ force (ibc_exports i)

293

296

294timestampOlder :: FilePath -> FilePath -> Idris ()

297timestampOlder :: FilePath -> FilePath -> Idris ()

295timestampOlder src ibc = do srct <- runIO $ getModificationTime src

298timestampOlder src ibc = do srct <- runIO $ getModificationTime src

@@ -311,12 +314,16 @@ pUsage :: [(Name, Int)] -> Idris ()

311pUsage ns = do ist <- getIState

314pUsage ns = do ist <- getIState

312 putIState ist { idris_erasureUsed = ns ++ idris_erasureUsed ist }

315 putIState ist { idris_erasureUsed = ns ++ idris_erasureUsed ist }

313

316

317+pExports :: [Name] -> Idris ()

318+pExports ns = do ist <- getIState

319+ putIState ist { idris_exports = ns ++ idris_exports ist }

320+

314pImportDirs :: [FilePath] -> Idris ()

321pImportDirs :: [FilePath] -> Idris ()

315pImportDirs fs = mapM_ addImportDir fs

322pImportDirs fs = mapM_ addImportDir fs

316

323

317pImports :: [(Bool, FilePath)] -> Idris ()

324pImports :: [(Bool, FilePath)] -> Idris ()

318pImports fs

325pImports fs

319− = do mapM_ (\(re, f) ->

326+ = do mapM_ (\(re, f) ->

320 do i <- getIState

327 do i <- getIState

321 ibcsd <- valIBCSubDir i

328 ibcsd <- valIBCSubDir i

322 ids <- allImportDirs

329 ids <- allImportDirs

@@ -420,20 +427,20 @@ pHdrs :: [(Codegen, String)] -> Idris ()

420pHdrs hs = mapM_ (uncurry addHdr) hs

427pHdrs hs = mapM_ (uncurry addHdr) hs

421

428

422pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()

429pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()

423−pPatdefs ds

430+pPatdefs ds

424− = mapM_ (\ (n, d) ->

431+ = mapM_ (\ (n, d) ->

425 do i <- getIState

432 do i <- getIState

426 putIState (i { idris_patdefs = addDef n (force d) (idris_patdefs i) }))

433 putIState (i { idris_patdefs = addDef n (force d) (idris_patdefs i) }))

427 ds

434 ds

428

435

429pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()

436pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()

430−pDefs reexp syms ds

437+pDefs reexp syms ds

431 = mapM_ (\ (n, d) ->

438 = mapM_ (\ (n, d) ->

432 do d' <- updateDef d

439 do d' <- updateDef d

433 case d' of

440 case d' of

434− TyDecl _ _ -> return ()

441+ TyDecl _ _ -> return ()

435 _ -> do iLOG $ "SOLVING " ++ show n

442 _ -> do iLOG $ "SOLVING " ++ show n

436− solveDeferred n

443+ solveDeferred n

437 i <- getIState

444 i <- getIState

438-- logLvl 1 $ "Added " ++ show (n, d')

445-- logLvl 1 $ "Added " ++ show (n, d')

439 putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })

446 putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })

@@ -502,8 +509,8 @@ pMDocs ds = mapM_ addMDocStr ds

502

509

503pAccess :: Bool -- ^ Reexporting?

510pAccess :: Bool -- ^ Reexporting?

504 -> [(Name, Accessibility)] -> Idris ()

511 -> [(Name, Accessibility)] -> Idris ()

505−pAccess reexp ds

512+pAccess reexp ds

506− = mapM_ (\ (n, a_in) ->

513+ = mapM_ (\ (n, a_in) ->

507 do let a = if reexp then a_in else Hidden

514 do let a = if reexp then a_in else Hidden

508 logLvl 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a

515 logLvl 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a

509 i <- getIState

516 i <- getIState

@@ -561,7 +568,7 @@ pFunctionErrorHandlers ((fn, arg, handler):ns) = do addFunctionErrorHandlers fn

561

568

562pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()

569pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()

563pMetavars ns = do i <- getIState

570pMetavars ns = do i <- getIState

564− putIState $ i { idris_metavars = Data.List.reverse ns

571+ putIState $ i { idris_metavars = Data.List.reverse ns

565 ++ idris_metavars i }

572 ++ idris_metavars i }

566

573

567----- For Cheapskate and docstrings

574----- For Cheapskate and docstrings

@@ -855,7 +862,7 @@ safeToEnum :: (Enum a, Bounded a, Integral int) => String -> int -> a

855safeToEnum label x' = result

862safeToEnum label x' = result

856 where

863 where

857 x = fromIntegral x'

864 x = fromIntegral x'

858− result

865+ result

859 | x < fromEnum (minBound `asTypeOf` result)

866 | x < fromEnum (minBound `asTypeOf` result)

860 || x > fromEnum (maxBound `asTypeOf` result)

867 || x > fromEnum (maxBound `asTypeOf` result)

861 = error $ label ++ ": corrupted binary representation in IBC"

868 = error $ label ++ ": corrupted binary representation in IBC"

@@ -927,7 +934,7 @@ instance Binary MetaInformation where

927 _ -> error "Corrupted binary data for MetaInformation"

934 _ -> error "Corrupted binary data for MetaInformation"

928

935

929instance Binary IBCFile where

936instance Binary IBCFile where

930− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42)

937+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43)

931 = {-# SCC "putIBCFile" #-}

938 = {-# SCC "putIBCFile" #-}

932 do put x1

939 do put x1

933 put x2

940 put x2

@@ -971,6 +978,7 @@ instance Binary IBCFile where

971 put x40

978 put x40

972 put x41

979 put x41

973 put x42

980 put x42

981+ put x43

974

982

975 get

983 get

976 = do x1 <- get

984 = do x1 <- get

@@ -1016,7 +1024,8 @@ instance Binary IBCFile where

1016 x40 <- get

1024 x40 <- get

1017 x41 <- get

1025 x41 <- get

1018 x42 <- get

1026 x42 <- get

1027+ x43 <- get

1019− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42)

1028+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43)

1020 else return (initIBC { ver = x1 })

1029 else return (initIBC { ver = x1 })

1021

1030

1022instance Binary DataOpt where

1031instance Binary DataOpt where

@@ -1240,15 +1249,18 @@ instance (Binary t) => Binary (PDecl' t) where

1240 put x6

1249 put x6

1241 put x7

1250 put x7

1242 put x8

1251 put x8

1243− PInstance x1 x2 x3 x4 x5 x6 x7 x8 -> do putWord8 8

1252+ PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

1253+ do putWord8 8

1244− put x1

1254+ put x1

1245− put x2

1255+ put x2

1246− put x3

1256+ put x3

1247− put x4

1257+ put x4

1248− put x5

1258+ put x5

1249− put x6

1259+ put x6

1250− put x7

1260+ put x7

1251− put x8

1261+ put x8

1262+ put x9

1263+ put x10

1252 PDSL x1 x2 -> do putWord8 9

1264 PDSL x1 x2 -> do putWord8 9

1253 put x1

1265 put x1

1254 put x2

1266 put x2

@@ -1271,16 +1283,18 @@ instance (Binary t) => Binary (PDecl' t) where

1271 put x1

1283 put x1

1272 put x2

1284 put x2

1273 PDirective x1 -> error "Cannot serialize PDirective"

1285 PDirective x1 -> error "Cannot serialize PDirective"

1274− PProvider x1 x2 x3 x4 -> do putWord8 15

1286+ PProvider x1 x2 x3 x4 x5 ->

1287+ do putWord8 15

1275− put x1

1288+ put x1

1276− put x2

1289+ put x2

1277− put x3

1290+ put x3

1278− put x4

1291+ put x4

1292+ put x5

1279 PTransform x1 x2 x3 x4 -> do putWord8 16

1293 PTransform x1 x2 x3 x4 -> do putWord8 16

1280 put x1

1294 put x1

1281 put x2

1295 put x2

1282 put x3

1296 put x3

1283− put x4

1297+ put x4

1284 get

1298 get

1285 = do i <- getWord8

1299 = do i <- getWord8

1286 case i of

1300 case i of

@@ -1343,7 +1357,9 @@ instance (Binary t) => Binary (PDecl' t) where

1343 x6 <- get

1357 x6 <- get

1344 x7 <- get

1358 x7 <- get

1345 x8 <- get

1359 x8 <- get

1360+ x9 <- get

1361+ x10 <- get

1346− return (PInstance x1 x2 x3 x4 x5 x6 x7 x8)

1362+ return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

1347 9 -> do x1 <- get

1363 9 -> do x1 <- get

1348 x2 <- get

1364 x2 <- get

1349 return (PDSL x1 x2)

1365 return (PDSL x1 x2)

@@ -1369,7 +1385,8 @@ instance (Binary t) => Binary (PDecl' t) where

1369 x2 <- get

1385 x2 <- get

1370 x3 <- get

1386 x3 <- get

1371 x4 <- get

1387 x4 <- get

1388+ x5 <- get

1372− return (PProvider x1 x2 x3 x4)

1389+ return (PProvider x1 x2 x3 x4 x5)

1373 16 -> do x1 <- get

1390 16 -> do x1 <- get

1374 x2 <- get

1391 x2 <- get

1375 x3 <- get

1392 x3 <- get

@@ -2191,4 +2208,3 @@ instance Binary Codegen where

2191 return (Via x1)

2208 return (Via x1)

2192 1 -> return Bytecode

2209 1 -> return Bytecode

2193 _ -> error "Corrupted binary data for Codegen"

2210 _ -> error "Corrupted binary data for Codegen"

2194−

src/Idris/IdeMode.hs+8−3

@@ -2,7 +2,7 @@

2

3{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}

4

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

6

7import Text.Printf

8import Numeric

@@ -206,6 +206,8 @@ parseSExp = parseString pSExp (Directed (UTF8.fromString "(unknown)") 0 0 0 0)

206

207data Opt = ShowImpl | ErrContext deriving Show

208

209+data WhatDocs = Overview | Full

210+

209data IdeModeCommand = REPLCompletions String

211data IdeModeCommand = REPLCompletions String

210 | Interpret String

212 | Interpret String

211 | TypeOf String

213 | TypeOf String

@@ -217,7 +219,7 @@ data IdeModeCommand = REPLCompletions String

217 | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth

219 | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth

218 | MakeLemma Int String

220 | MakeLemma Int String

219 | LoadFile String (Maybe Int)

221 | LoadFile String (Maybe Int)

220− | DocsFor String

222+ | DocsFor String WhatDocs

221 | Apropos String

223 | Apropos String

222 | GetOpts

224 | GetOpts

223 | SetOpt Opt Bool

225 | SetOpt Opt Bool

@@ -258,7 +260,10 @@ sexpToCommand (SexpList (SymbolAtom "proof-search" : IntegerAtom line : StringAt

258 _ -> Nothing)

260 _ -> Nothing)

259sexpToCommand (SexpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom name]) = Just (MakeLemma (fromInteger line) name)

261sexpToCommand (SexpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom name]) = Just (MakeLemma (fromInteger line) name)

260sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint] Nothing)

262sexpToCommand (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)]

262sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)

267sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)

263sexpToCommand (SymbolAtom "get-options") = Just GetOpts

268sexpToCommand (SymbolAtom "get-options") = Just GetOpts

264sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])

269sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])

src/Idris/IdrisDoc.hs+6−6

@@ -168,7 +168,7 @@ removeOrphans list =

168 in filter ((`S.notMember` children) . (\(n, _, _) -> n)) list

169

170 where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds

171− names (Just (ClassDoc _ _ fds _ _ _)) = map (\(FD n _ _ _ _) -> n) fds

171+ names (Just (ClassDoc _ _ fds _ _ _ _)) = map (\(FD n _ _ _ _) -> n) fds

172 names _ = []

173

174-- | Whether a Name names something which should be documented

@@ -219,7 +219,7 @@ referredNss (n, Just d, _) =

219

220 where getFunDocs (FunDoc f) = [f]

221 getFunDocs (DataDoc f fs) = f:fs

222− getFunDocs (ClassDoc _ _ fs _ _ _) = fs

222+ getFunDocs (ClassDoc _ _ fs _ _ _ _) = fs

223 types (FD _ _ args t _) = t:(map second args)

224 second (_, x, _, _) = x

225

@@ -273,7 +273,7 @@ loadDocs :: IState -- ^ IState to extract infomation from

273 -> Name -- ^ Name to load Docs for

274 -> IO (Maybe Docs)

275loadDocs ist n

276− | mayHaveDocs n = do docs <- runExceptT $ evalStateT (getDocs n) ist

276+ | mayHaveDocs n = do docs <- runExceptT $ evalStateT (getDocs n FullDocs) ist

277 case docs of Right d -> return (Just d)

278 Left _ -> return Nothing

279 | otherwise = return Nothing

@@ -417,7 +417,7 @@ createIndex nss out =

417 BS2.hPut h $ renderHtml $ wrapper Nothing $ do

418 H.h1 $ "Namespaces"

419 H.ul ! class_ "names" $ do

420− let path ns = "docs" </> genRelNsPath ns "html"

420+ let path ns = "docs" </> genRelNsPath ns "html"

421 item ns = do let n = toHtml $ nsName2Str ns

422 link = toValue $ path ns

423 H.li $ H.a ! href link ! class_ "code" $ n

@@ -439,7 +439,7 @@ createNsDoc :: IState -- ^ Needed to determine the types of names

439createNsDoc ist ns content out =

440 do let tpath = out </> "docs" </> (genRelNsPath ns "html")

441 dir = takeDirectory tpath

442− file = takeFileName tpath

442+ file = takeFileName tpath

443 haveDocs (_, Just d, _) = [d]

444 haveDocs _ = []

445 -- We cannot do anything without a Doc

@@ -575,7 +575,7 @@ createOtherDoc :: IState -- ^ Needed to determine the types of names

575 -> H.Html -- ^ Resulting HTML

576createOtherDoc ist (FunDoc fd) = createFunDoc ist fd

577

578−createOtherDoc ist (ClassDoc n docstring fds _ _ _) = do

578+createOtherDoc ist (ClassDoc n docstring fds _ _ _ _) = do

579 H.dt ! (A.id $ toValue $ show n) $ do

580 H.span ! class_ "word" $ do "class"; nbsp

581 H.span ! class_ "name type"

src/Idris/Imports.hs+22−6

@@ -44,7 +44,7 @@ ibcPath ibcsd use_ibcsd fp = let (d_fp, n_fp) = splitFileName fp

44

45ibcPathWithFallback :: FilePath -> FilePath -> IO FilePath

46ibcPathWithFallback ibcsd fp = do let ibcp = ibcPath ibcsd True fp

47− ibc <- doesFileExist ibcp

47+ ibc <- doesFileExist' ibcp

48 return (if ibc

49 then ibcp

50 else ibcPath ibcsd False fp)

@@ -58,9 +58,9 @@ findImport (d:ds) ibcsd fp = do let fp_full = d </> fp

58 ibcp <- runIO $ ibcPathWithFallback ibcsd fp_full

59 let idrp = srcPath fp_full

60 let lidrp = lsrcPath fp_full

61− ibc <- runIO $ doesFileExist ibcp

61+ ibc <- runIO $ doesFileExist' ibcp

62− idr <- runIO $ doesFileExist idrp

62+ idr <- runIO $ doesFileExist' idrp

63− lidr <- runIO $ doesFileExist lidrp

63+ lidr <- runIO $ doesFileExist' lidrp

64-- when idr $ putStrLn $ idrp ++ " ok"

65-- when lidr $ putStrLn $ lidrp ++ " ok"

66-- when ibc $ putStrLn $ ibcp ++ " ok"

@@ -78,7 +78,7 @@ findImport (d:ds) ibcsd fp = do let fp_full = d </> fp

78findInPath :: [FilePath] -> FilePath -> IO FilePath

79findInPath [] fp = fail $ "Can't find file " ++ fp

80findInPath (d:ds) fp = do let p = d </> fp

81− e <- doesFileExist p

81+ e <- doesFileExist' p

82 if e then return p else findInPath ds fp

83

84findPkgIndex :: String -> Idris FilePath

@@ -94,10 +94,26 @@ installedPackages = do

94 where

95 allFilesInDir base fp = do

96 let fullpath = base </> fp

97− isDir <- doesDirectoryExist fullpath

97+ isDir <- doesDirectoryExist' fullpath

98 if isDir

99 then fmap concat (mapM (allFilesInDir fullpath) =<< dirContents fullpath)

100 else return [fp]

101 dirContents = fmap (filter (not . (`elem` [".", ".."]))) . getDirectoryContents

102 goodDir idir d = any (".ibc" `isSuffixOf`) <$> allFilesInDir idir d

103

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

554 args <- many (do notEndApp; arg syn)

555 case args of

556 [] -> return f

557− _ -> return (dslify i (PApp fc f args)))

557+ _ -> return (PApp fc f args))

558 <?> "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

565

559

566{-| Parses a function argument

560{-| Parses a function argument

567@

561@

@@ -878,7 +872,9 @@ pi syn =

878 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)) <|> (do

872 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)) <|> (do

879 try (lchar '{' *> reserved "default")

873 try (lchar '{' *> reserved "default")

880 when (st == Static) $ fail "default tactic constraints can not be static"

874 when (st == Static) $ fail "default tactic constraints can not be static"

875+ ist <- get

881− script <- simpleExpr syn

876+ script' <- simpleExpr syn

877+ let script = debindApp syn . desugar syn ist $ script'

882 xt <- typeDeclList syn

878 xt <- typeDeclList syn

883 lchar '}'

879 lchar '}'

884 symbol "->"

880 symbol "->"

src/Idris/ParseHelpers.hs+11−4

@@ -119,7 +119,7 @@ singleLineComment :: MonadicParsing m => m ()

119singleLineComment = (string "--" *>

120 many (satisfy (not . isEol)) *>

121 eol *> pure ())

122− <?> "single-line comment"

122+ <?> ""

123

124{- | Consumes a multi-line comment

125

@@ -321,10 +321,17 @@ opChars = ":!#$%&*+./<=>?@\\^|-~"

321operatorLetter :: MonadicParsing m => m Char

322operatorLetter = oneOf opChars

323

324+

325+commentMarkers :: [String]

326+commentMarkers = [ "--", "|||" ]

327+

328+invalidOperators :: [String]

329+invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!"]

330+

324-- | Parses an operator

331-- | Parses an operator

325operator :: MonadicParsing m => m String

332operator :: MonadicParsing m => m String

326operator = do op <- token . some $ operatorLetter

333operator = do op <- token . some $ operatorLetter

327− when (op `elem` [":", "=>", "->", "<-", "=", "?=", "|"]) $

334+ when (op `elem` (invalidOperators ++ commentMarkers)) $

328 fail $ op ++ " is not a valid operator"

335 fail $ op ++ " is not a valid operator"

329 return op

336 return op

330

337

@@ -580,7 +587,7 @@ collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

580collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

587collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

581collect (PClass doc f s cs n ps pdocs ds : ds')

588collect (PClass doc f s cs n ps pdocs ds : ds')

582 = PClass doc f s cs n ps pdocs (collect ds) : collect ds'

589 = PClass doc f s cs n ps pdocs (collect ds) : collect ds'

583−collect (PInstance f s cs n ps t en ds : ds')

590+collect (PInstance doc argDocs f s cs n ps t en ds : ds')

584− = PInstance f s cs n ps t en (collect ds) : collect ds'

591+ = PInstance doc argDocs f s cs n ps t en (collect ds) : collect ds'

585collect (d : ds) = d : collect ds

592collect (d : ds) = d : collect ds

586collect [] = []

593collect [] = []

src/Idris/ParseOps.hs+9−1

@@ -37,7 +37,8 @@ table fixes

37 toTable (reverse fixes) ++

38 [[backtick],

39 [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]]

41 where

42 where

42 flatten :: PTerm -> PTerm -- flatten application

43 flatten :: PTerm -> PTerm -- flatten application

43 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

44 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

@@ -80,6 +81,13 @@ backtick = Infix (do indentPropHolds gtProp

80 fc <- getFC

81 fc <- getFC

81 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone

82 return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone

82

83

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+

83{- | Parses an operator in function position i.e. enclosed by `()', with an

91{- | Parses an operator in function position i.e. enclosed by `()', with an

84 optional namespace

92 optional namespace

85

93

src/Idris/Parser.hs+59−43

@@ -9,7 +9,7 @@ module Idris.Parser(module Idris.Parser,

9import Prelude hiding (pi)

10

11import Text.Trifecta.Delta

12−import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)

12+import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace, Err)

13import Text.Parser.LookAhead

14import Text.Parser.Expression

15import qualified Text.Parser.Token as Tok

@@ -87,7 +87,7 @@ import System.IO

87{- | Parses module definition

88

89@

90− ModuleHeader ::= 'module' Identifier_t ';'?;

90+ ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;

91@

92-}

93moduleHeader :: IdrisParser (Maybe (Docstring ()), [String])

@@ -291,6 +291,10 @@ syntaxRule syn

291

292 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :

293 mkSimple es

294+ -- Can't parse a full expression followed by operator like characters due to ambiguity

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

294 mkSimple' (e : es) = e : mkSimple' es

298 mkSimple' (e : es) = e : mkSimple' es

295 mkSimple' [] = []

299 mkSimple' [] = []

296

300

@@ -344,13 +348,9 @@ fnDecl' :: SyntaxInfo -> IdrisParser PDecl

344fnDecl' syn = checkFixity $

348fnDecl' syn = checkFixity $

345 do (doc, argDocs, fc, opts', n, acc) <- try (do

349 do (doc, argDocs, fc, opts', n, acc) <- try (do

346 pushIndent

350 pushIndent

347− (doc, argDocs) <- option noDocs docComment

351+ (doc, argDocs) <- docstring syn

348 ist <- get

352 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

354 then [TotalFn]

355 else []

356 opts <- fnOpts initOpts

@@ -360,7 +360,7 @@ fnDecl' syn = checkFixity $

360 let n = expandNS syn n_in

361 fc <- getFC

362 lchar ':'

363− return (doc', argDocs', fc, opts', n, acc))

363+ return (doc, argDocs, fc, opts', n, acc))

364 ty <- typeExpr (allowImp syn)

365 terminator

366 addAcc n acc

@@ -455,12 +455,10 @@ Postulate ::=

455@

456-}

457postulate :: SyntaxInfo -> IdrisParser PDecl

458−postulate syn = do doc <- try $ do (doc, _) <- option noDocs docComment

458+postulate syn = do doc <- try $ do (doc, _) <- docstring syn

459− ist <- get

460− let doc' = annotCode (tryFullExpr syn ist) doc

461 pushIndent

459 pushIndent

462 reserved "postulate"

460 reserved "postulate"

463− return doc'

461+ return doc

464 ist <- get

462 ist <- get

465 let initOpts = if default_total ist

463 let initOpts = if default_total ist

466 then [TotalFn]

464 then [TotalFn]

@@ -583,7 +581,7 @@ ClassBlock ::=

583classBlock :: SyntaxInfo -> IdrisParser [PDecl]

581classBlock :: SyntaxInfo -> IdrisParser [PDecl]

584classBlock syn = do reserved "where"

582classBlock syn = do reserved "where"

585 openBlock

583 openBlock

586− ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)

584+ ds <- many (notEndBlock >> instance_ syn <|> fnDecl syn)

587 closeBlock

585 closeBlock

588 return (concat ds)

586 return (concat ds)

589 <?> "class block"

587 <?> "class block"

@@ -604,15 +602,14 @@ Class ::=

604@

602@

605-}

603-}

606class_ :: SyntaxInfo -> IdrisParser [PDecl]

604class_ :: SyntaxInfo -> IdrisParser [PDecl]

607−class_ syn = do (doc, argDocs, acc) <- try (do

605+class_ syn = do (doc, argDocs, acc)

608− (doc, argDocs) <- option noDocs docComment

606+ <- try (do (doc, argDocs) <- docstring syn

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

607+ acc <- optional accessibility

614− return (doc', argDocs', acc))

608+ reserved "class"

609+ return (doc, argDocs, acc))

610+ fc <- getFC

615− reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName

611+ cons <- constraintList syn

612+ n_in <- fnName

616 let n = expandNS syn n_in

613 let n = expandNS syn n_in

617 cs <- many carg

614 cs <- many carg

618 ds <- option [] (classBlock syn)

615 ds <- option [] (classBlock syn)

@@ -630,7 +627,7 @@ class_ syn = do (doc, argDocs, acc) <- try (do

630

627

631@

628@

632 Instance ::=

629 Instance ::=

633− 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?

630+ DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?

634 ;

631 ;

635@

632@

636

633

@@ -639,7 +636,9 @@ InstanceName ::= '[' Name ']';

639@

636@

640-}

637-}

641instance_ :: SyntaxInfo -> IdrisParser [PDecl]

638instance_ :: SyntaxInfo -> IdrisParser [PDecl]

639+instance_ syn = do (doc, argDocs)

642−instance_ syn = do reserved "instance"; fc <- getFC

640+ <- try (docstring syn <* reserved "instance")

641+ fc <- getFC

643 en <- optional instanceName

642 en <- optional instanceName

644 cs <- constraintList syn

643 cs <- constraintList syn

645 cn <- fnName

644 cn <- fnName

@@ -647,7 +646,7 @@ instance_ syn = do reserved "instance"; fc <- getFC

647 let sc = PApp fc (PRef fc cn) (map pexp args)

646 let sc = PApp fc (PRef fc cn) (map pexp args)

648 let t = bindList (PPi constraint) cs sc

647 let t = bindList (PPi constraint) cs sc

649 ds <- option [] (instanceBlock syn)

648 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]

651 <?> "instance declaration"

650 <?> "instance declaration"

652 where instanceName :: IdrisParser Name

651 where instanceName :: IdrisParser Name

653 instanceName = do lchar '['; n_in <- fnName; lchar ']'

652 instanceName = do lchar '['; n_in <- fnName; lchar ']'

@@ -656,6 +655,18 @@ instance_ syn = do reserved "instance"; fc <- getFC

656 <?> "instance name"

655 <?> "instance name"

657

656

658

657

658+-- | Parse a docstring

659+docstring :: SyntaxInfo

660+ -> IdrisParser (Docstring (Either Err PTerm),

661+ [(Name,Docstring (Either Err PTerm))])

662+docstring syn = do (doc, argDocs) <- option noDocs docComment

663+ ist <- get

664+ let doc' = annotCode (tryFullExpr syn ist) doc

665+ argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

666+ | (n, d) <- argDocs ]

667+ return (doc', argDocs')

668+

669+

659{- | Parses a using declaration list

670{- | Parses a using declaration list

660

671

661@

672@

@@ -1097,25 +1108,30 @@ totality

1097{- | Parses a type provider

1108{- | Parses a type provider

1098

1109

1099@

1110@

1100−Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;

1111+Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;

1101ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'

1112ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'

1102@

1113@

1103 -}

1114 -}

1104provider :: SyntaxInfo -> IdrisParser [PDecl]

1115provider :: SyntaxInfo -> IdrisParser [PDecl]

1116+provider syn = do doc <- try (do (doc, _) <- docstring syn

1117+ lchar '%'

1105−provider syn = do try (lchar '%' *> reserved "provide");

1118+ reserved "provide"

1119+ return doc)

1106− provideTerm <|> providePostulate

1120+ provideTerm doc <|> providePostulate doc

1107 <?> "type provider"

1121 <?> "type provider"

1122+ where provideTerm doc =

1108− where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1123+ do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1109− fc <- getFC

1124+ fc <- getFC

1110− reserved "with"

1125+ reserved "with"

1111− e <- expr syn <?> "provider expression"

1126+ e <- expr syn <?> "provider expression"

1112− return [PProvider syn fc (ProvTerm t e) n]

1127+ return [PProvider doc syn fc (ProvTerm t e) n]

1128+ providePostulate doc =

1113− providePostulate = do reserved "postulate"

1129+ do reserved "postulate"

1114− n <- fnName

1130+ n <- fnName

1115− fc <- getFC

1131+ fc <- getFC

1116− reserved "with"

1132+ reserved "with"

1117− e <- expr syn <?> "provider expression"

1133+ e <- expr syn <?> "provider expression"

1118− return [PProvider syn fc (ProvPostulate e) n]

1134+ return [PProvider doc syn fc (ProvPostulate e) n]

1119

1135

1120{- | Parses a transform

1136{- | Parses a transform

1121

1137

@@ -1399,9 +1415,9 @@ loadSource lidr f toline

1399 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)

1415 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)

1400 toMutual x = let r = PMutual (fileFC "single mutual") [x] in

1416 toMutual x = let r = PMutual (fileFC "single mutual") [x] in

1401 case x of

1417 case x of

1402− PClauses _ _ _ _ -> r

1418+ PClauses{} -> r

1403− PClass _ _ _ _ _ _ _ _ -> r

1419+ PClass{} -> r

1404− PInstance _ _ _ _ _ _ _ _ -> r

1420+ PInstance{} -> r

1405 _ -> x

1421 _ -> x

1406

1422

1407 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()

1423 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

138 True)

139 -- if all else fails, make a new metavariable

140 (if fromProver

141− then cantSolveGoal

141+ then fail "cantSolveGoal"

142 else do attack; defer [] nroot; solve) True) True

143

144 getFn d Nothing = []

src/Idris/Prover.hs+2−2

@@ -202,7 +202,7 @@ receiveInput h e =

202 receiveInput h e

203 Just (IdeMode.Interpret cmd) -> return (Just cmd)

204 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))

206 _ -> return Nothing

207

208ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])

@@ -336,7 +336,7 @@ ploop fn d prompt prf e h

336 return (False, e, False, prf,

337 Right $ iRenderResult (vsep toShow)))

338 (\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

340 return $ pprintDocs ist doc

341 docStr (Right c) = do ist <- getIState

342 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

54

55import IRTS.Compiler

56import IRTS.CodegenCommon

57+import IRTS.Exports

57import IRTS.System

58import IRTS.System

58

59

59import Control.Category

60import Control.Category

@@ -344,13 +345,15 @@ runIdeModeCommand h id orig fn mods (IdeMode.TypeOf name) =

344 Left err -> iPrintError err

345 Left err -> iPrintError err

345 Right n -> process "(idemode)"

346 Right n -> process "(idemode)"

346 (Check (PRef (FC "(idemode)" (0,0) (0,0)) n))

347 (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) =

348 case parseConst orig name of

349 case parseConst orig name of

349− Success c -> process "(idemode)" (DocStr (Right c))

350+ Success c -> process "(idemode)" (DocStr (Right c) (howMuch w))

350 Failure _ ->

351 Failure _ ->

351 case splitName name of

352 case splitName name of

352 Left err -> iPrintError err

353 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

354runIdeModeCommand h id orig fn mods (IdeMode.CaseSplit line name) =

357runIdeModeCommand h id orig fn mods (IdeMode.CaseSplit line name) =

355 process fn (CaseSplitAt False line (sUN name))

358 process fn (CaseSplitAt False line (sUN name))

356runIdeModeCommand h id orig fn mods (IdeMode.AddClause line name) =

359runIdeModeCommand h id orig fn mods (IdeMode.AddClause line name) =

@@ -553,7 +556,7 @@ idemodeProcess fn (Undefine n) = process fn (Undefine n)

553idemodeProcess fn (ExecVal t) = process fn (ExecVal t)

556idemodeProcess fn (ExecVal t) = process fn (ExecVal t)

554idemodeProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))

557idemodeProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))

555idemodeProcess fn (Check t) = process fn (Check t)

558idemodeProcess 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)

557idemodeProcess fn Universes = process fn Universes

560idemodeProcess fn Universes = process fn Universes

558idemodeProcess fn (Defn n) = do process fn (Defn n)

561idemodeProcess fn (Defn n) = do process fn (Defn n)

559 iPrintResult ""

562 iPrintResult ""

@@ -808,8 +811,8 @@ process fn (NewDefn decls) = do

808 fixClauses :: PDecl' t -> PDecl' t

811 fixClauses :: PDecl' t -> PDecl' t

809 fixClauses (PClauses fc opts _ css@(clause:cs)) =

812 fixClauses (PClauses fc opts _ css@(clause:cs)) =

810 PClauses fc opts (getClauseName clause) css

813 PClauses fc opts (getClauseName clause) css

811− fixClauses (PInstance syn fc constraints cls parms ty instName decls) =

814+ fixClauses (PInstance doc argDocs syn fc constraints cls parms ty instName decls) =

812− PInstance syn fc constraints cls parms ty instName (map fixClauses decls)

815+ PInstance doc argDocs syn fc constraints cls parms ty instName (map fixClauses decls)

813 fixClauses decl = decl

816 fixClauses decl = decl

814

817

815process fn (Undefine names) = undefine names

818process fn (Undefine names) = undefine names

@@ -905,21 +908,23 @@ process fn (Check t)

905 _ -> iPrintTermWithType (pprintDelab ist tm)

908 _ -> iPrintTermWithType (pprintDelab ist tm)

906 (pprintDelab ist ty)

909 (pprintDelab ist ty)

907

910

908−process fn (DocStr (Left n))

911+process fn (DocStr (Left n) w)

909 = do ist <- getIState

912 = do ist <- getIState

910 let docs = lookupCtxtName n (idris_docstrings ist) ++

913 let docs = lookupCtxtName n (idris_docstrings ist) ++

914+ map (\(n,d)-> (n, (d, [])))

911− map (\(n,d)-> (n, (d,[]))) (lookupCtxtName (modDocN n) (idris_moduledocs ist))

915+ (lookupCtxtName (modDocN n) (idris_moduledocs ist))

912 case docs of

916 case docs of

913 [] -> iPrintError $ "No documentation for " ++ show n

917 [] -> iPrintError $ "No documentation for " ++ show n

914 ns -> do toShow <- mapM (showDoc ist) ns

918 ns -> do toShow <- mapM (showDoc ist) ns

915 iRenderResult (vsep toShow)

919 iRenderResult (vsep toShow)

916− where showDoc ist (n, d) = do doc <- getDocs n

920+ where showDoc ist (n, d) = do doc <- getDocs n w

917 return $ pprintDocs ist doc

921 return $ pprintDocs ist doc

922+

918 modDocN (NS (UN n) ns) = NS modDocName (n:ns)

923 modDocN (NS (UN n) ns) = NS modDocName (n:ns)

919 modDocN (UN n) = NS modDocName [n]

924 modDocN (UN n) = NS modDocName [n]

920 modDocN _ = sMN 1 "NotFoundForSure"

925 modDocN _ = sMN 1 "NotFoundForSure"

921

926

922−process fn (DocStr (Right c))

927+process fn (DocStr (Right c) _) -- constants only have overviews

923 = do ist <- getIState

928 = do ist <- getIState

924 iRenderResult $ pprintConstDocs ist c (constDocs c)

929 iRenderResult $ pprintConstDocs ist c (constDocs c)

925

930

@@ -1106,7 +1111,7 @@ process fn Execute

1106 t <- codegen

1111 t <- codegen

1107 -- gcc adds .exe when it builds windows programs

1112 -- gcc adds .exe when it builds windows programs

1108 progName <- return $ if isWindows then tmpn ++ ".exe" else tmpn

1113 progName <- return $ if isWindows then tmpn ++ ".exe" else tmpn

1109− ir <- compile t tmpn m

1114+ ir <- compile t tmpn (Just m)

1110 runIO $ generate t (fst (head (idris_imported ist))) ir

1115 runIO $ generate t (fst (head (idris_imported ist))) ir

1111 case idris_outputmode ist of

1116 case idris_outputmode ist of

1112 RawOutput h -> do runIO $ rawSystem progName []

1117 RawOutput h -> do runIO $ rawSystem progName []

@@ -1118,9 +1123,13 @@ process fn Execute

1118process fn (Compile codegen f)

1123process fn (Compile codegen f)

1119 | map toLower (takeExtension f) `elem` [".idr", ".lidr", ".idc"] =

1124 | map toLower (takeExtension f) `elem` [".idr", ".lidr", ".idc"] =

1120 iPrintError $ "Invalid filename for compiler output \"" ++ f ++"\""

1125 iPrintError $ "Invalid filename for compiler output \"" ++ f ++"\""

1126+ | otherwise = do opts <- getCmdLine

1127+ let iface = Interface `elem` opts

1128+ m <- if iface then return Nothing else

1121− | otherwise = do (m, _) <- elabVal recinfo ERHS

1129+ do (m', _) <- elabVal recinfo ERHS

1122− (PApp fc (PRef fc (sUN "run__IO"))

1130+ (PApp fc (PRef fc (sUN "run__IO"))

1123− [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

1131+ [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

1132+ return (Just m')

1124 ir <- compile codegen f m

1133 ir <- compile codegen f m

1125 i <- getIState

1134 i <- getIState

1126 runIO $ generate codegen (fst (head (idris_imported i))) ir

1135 runIO $ generate codegen (fst (head (idris_imported i))) ir

@@ -1414,9 +1423,10 @@ loadInputs inputs toline -- furthest line to read in input source files

1414 ist <- getIState

1423 ist <- getIState

1415 putIState (ist { idris_tyinfodata = tidata,

1424 putIState (ist { idris_tyinfodata = tidata,

1416 idris_patdefs = patdefs })

1425 idris_patdefs = patdefs })

1426+ exports <- findExports

1417

1427

1418 case opt getOutput opts of

1428 case opt getOutput opts of

1419− [] -> performUsageAnalysis -- interactive

1429+ [] -> performUsageAnalysis (getExpNames exports) -- interactive

1420 _ -> return [] -- batch, will be checked by the compiler

1430 _ -> return [] -- batch, will be checked by the compiler

1421

1431

1422 return (map fst ifiles))

1432 return (map fst ifiles))

@@ -1511,7 +1521,8 @@ idrisMain opts =

1511 xs -> last xs

1521 xs -> last xs

1512 setOptLevel optimise

1522 setOptLevel optimise

1513 let outty = case opt getOutputTy opts of

1523 let outty = case opt getOutputTy opts of

1524+ [] -> if Interface `elem` opts then

1514− [] -> Executable

1525+ Object else Executable

1515 xs -> last xs

1526 xs -> last xs

1516 let cgn = case opt getCodegen opts of

1527 let cgn = case opt getCodegen opts of

1517 [] -> Via "c"

1528 [] -> Via "c"

src/Idris/REPLParser.hs+2−2

@@ -258,9 +258,9 @@ cmd_doc name = do

258 let constant = do

259 c <- P.constant

260 eof

261− return $ Right (DocStr (Right c))

261+ return $ Right (DocStr (Right c) FullDocs)

262

263− let fnName = fnNameArg (\n -> DocStr (Left n)) name

263+ let fnName = fnNameArg (\n -> DocStr (Left n) FullDocs) name

264

265 try constant <|> fnName

266

test/Makefile+1−7

@@ -7,14 +7,8 @@ test: $(TESTS)

7%.test:

8 @perl ./runtest.pl $(patsubst %.test,%,$@)

9

10−test_java:

11− @perl ./runtest.pl without primitives004 --codegen Java

12−

13test_js:

10test_js:

14− @perl ./runtest.pl without sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 effects003 buffer001 basic007 basic011 primitives004 --codegen node

11+ @perl ./runtest.pl without sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 effects003 buffer001 basic007 basic011 primitives004 ffi006 --codegen node

15−

16−test_llvm:

17− @perl ./runtest.pl without primitives003 primitives004 sugar004 io003 buffer001 --codegen llvm

18

12

19update:

13update:

20 /usr/bin/env perl ./runtest.pl all -u

14 /usr/bin/env perl ./runtest.pl all -u

test/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)

35 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

36 Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b

37

38+ lam_ : TTName -> Expr (a :: G) t -> Expr G (TyFun a t)

39+ lam_ _ = Lam

40+

38 dsl expr

41 dsl expr

39− lambda = Lam

42+ lambda = lam_

40 variable = Var

43 variable = Var

41 index_first = stop

44 index_first = stop

42 index_next = pop

45 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)

156 = interp env v (\env', v' => do n <- v'

157 interp env' (f n) k)

158

159+ let_ : _ -> Creator (interpTy a) ->

160+ Res (a :: gam) (Val () :: gam') (R t) ->

161+ Res gam gam' (R t)

162+ let_ _ = Let

163+

159-- run : {static} Res [] [] (R t) -> IO t

164-- run : {static} Res [] [] (R t) -> IO t

160-- run prog = interp [] prog (\env, res => res)

165-- run prog = interp [] prog (\env, res => res)

161

166

@@ -163,7 +168,7 @@ syntax run [prog] = interp [] prog (\env, res => res)

163

168

164dsl res

169dsl res

165 variable = id

170 variable = id

166− let = Let

171+ let = let_

167 index_first = stop

172 index_first = stop

168 index_next = pop

173 index_next = pop

169

174

test/dsl003/DSLPi.idr+8−2

@@ -5,8 +5,11 @@ import Data.Vect

5

6data Ty = BOOL | INT | UNIT | ARR Ty Ty

7

8+arr_ : _ -> Ty -> Ty -> Ty

9+arr_ _ = ARR

10+

8dsl simple_type

11dsl simple_type

9− pi = ARR

12+ pi = arr_

10

13

11test1 : simple_type (BOOL -> INT -> UNIT) = BOOL `ARR` (INT `ARR` UNIT)

14test1 : simple_type (BOOL -> INT -> UNIT) = BOOL `ARR` (INT `ARR` UNIT)

12test1 = Refl

15test1 = Refl

@@ -25,8 +28,11 @@ using (vars : Vect n Ty)

25 implicit exprSpec : Expr vars BOOL -> Spec vars

28 implicit exprSpec : Expr vars BOOL -> Spec vars

26 exprSpec = ItHolds

29 exprSpec = ItHolds

27

30

31+ forall_ : _ -> (t : Ty) -> Spec (t :: vars) -> Spec vars

32+ forall_ _ = ForAll

33+

28dsl specs

34dsl specs

29− pi = ForAll

35+ pi = forall_

30 variable = Var

36 variable = Var

31 index_first = FZ

37 index_first = FZ

32 index_next = FS

38 index_next = FS

test/error005/error005.idr+7

@@ -18,3 +18,10 @@ ok n = 1

18

19notOk : (n : Nat) -> Fin (plus 2 n)

20notOk n = 2

21+

22+b0rken : Integer -> Fin 3

23+b0rken n = fromInteger n

24+

25+x : Fin 4

26+x = the (Fin 4) 5

27+

test/error005/expected+12−4

@@ -1,12 +1,20 @@

1error005.idr:13:1:When elaborating right hand side of two:

2When elaborating argument prf to function Data.Fin.fromInteger:

3 When using 2 as a literal for a Fin 2

4− Could not show that 2 is less than 2

4+ 2 is not strictly less than 2

5error005.idr:16:1:When elaborating right hand side of hahaha:

6When elaborating argument prf to function Data.Fin.fromInteger:

7 When using 0 as a literal for a Fin n

8− Could not show that 0 is less than n

8+ 0 is not strictly less than n

9−error005.idr:21:1:When elaborating right hand side of notOk:

9+error005.idr:22:1:When elaborating right hand side of notOk:

10When elaborating argument prf to function Data.Fin.fromInteger:

11 When using 2 as a literal for a Fin (S (S n))

12+ 2 is not strictly less than S (S n)

13+error005.idr:23:24:When elaborating right hand side of b0rken:

14+When elaborating argument prf to function Data.Fin.fromInteger:

15+ When using n as a literal for a Fin 3

12− Could not show that 2 is less than S (S n)

16+ Could not show that n is less than 3 because n is a bound variable instead of a constant Integer

17+error005.idr:28:1:When elaborating right hand side of x:

18+When elaborating argument prf to function Data.Fin.fromInteger:

19+ When using 5 as a literal for a Fin 4

20+ 5 is not strictly less than 4

test/ffi006/expectednew file+2

@@ -0,0 +1,2 @@

1+Ready to show...

2+[10, 20, 30, 40]

test/ffi006/ffi006.cnew file+14

@@ -0,0 +1,14 @@

1+#include "testHdr.h"

2+

3+int main() {

4+

5+ VM* vm = idris_vm();

6+

7+ ListInt x = cons(vm, 10, cons(vm, 20, nil(vm)));

8+ ListInt y = cons(vm, 30, cons(vm, 40, nil(vm)));

9+ ListInt z = addLists(vm, x, y);

10+

11+ printf("%s\n", showList(vm, z));

12+

13+ close_vm(vm);

14+}

test/ffi006/ffi006.idrnew file+30

@@ -0,0 +1,30 @@

1+import Data.List

2+

3+addLists : List Int -> List Int -> List Int

4+addLists xs ys = xs ++ ys

5+

6+nil : List Int

7+nil = []

8+

9+cons : Int -> List Int -> List Int

10+cons x xs = x :: xs

11+

12+show' : List Int -> IO String

13+show' xs = do putStrLn "Ready to show..."

14+ return (show xs)

15+

16+testList : FFI_Export FFI_C "testHdr.h" []

17+testList = Data (List Int) "ListInt" $

18+ Data (List Nat) "ListNat" $

19+ Fun addLists "addLists" $

20+ Fun nil "nil" $

21+ Fun cons "cons" $

22+ Data Nat "Nat" $

23+ Fun Strings.length "lengthS" $

24+ Fun show' "showList" $

25+ End

26+

27+-- main : IO ()

28+-- main = do s <- show' 42

29+-- putStrLn s

30+

test/ffi006/runnew file+5

@@ -0,0 +1,5 @@

1+#!/usr/bin/env bash

2+idris $@ ffi006.idr --interface -o ffi006.o

3+cc ffi006.c ffi006.o `idris --include` `idris --link` -o ffi006

4+./ffi006

5+rm -f ffi006 *.ibc *.o *.h

test/reg027/reg027.idr+1−1

@@ -14,7 +14,7 @@ instance Functor IntFn where -- (\x => Int -> x) where

14

15instance Applicative (\x => Int -> x) where

16 pure v = \x => v

17− (<$>) f a = \x => f x (a x)

17+ (<*>) f a = \x => f x (a x)

18

19instance Monad IntFn where

20 f >>= k = \x => k (f x) x

test/reg041/ott.idr+1−1

@@ -37,6 +37,6 @@ EQ two False two False = one

37EQ (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)

38EQ _ _ _ _ = zero

39

40−example : <| id == id in (two ~> two) |>

40+example : <| (id == id in (two ~> two)) |>

41example = ?prf

42

test/reg050/expected+9−28

@@ -1,29 +1,10 @@

1−badbangop.idr:16:1:When elaborating right hand side of opUse:

1+./badbangop.idr:7:1: error: ! is

2−When elaborating an application of function Prelude.Monad.>>=:

2+ not a valid

3− Can't unify

3+ operator, expected: space

4− List Integer

4+(!) : List a -> Nat -> Maybe a

5− with

5+^

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

6+./baddoublebang.idr:6:28: error: unexpected

14− a terminator, expected: "$",

7+ Operator without known fixity:

15− "$>", "&&", "*", "+", "++", "-",

8+ !!, expected: space

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

28doubleBang mmn = do pure !!mmn

9doubleBang mmn = do pure !!mmn

29− ^

10+ ^

test/reg053/four.idr+1−1

@@ -5,5 +5,5 @@ data FourFunctor y = Four y y y y

5traverseFourFunctor : Applicative f ->

6 (x -> f b) -> FourFunctor x -> f (FourFunctor b)

7traverseFourFunctor 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)

9

test/sourceLocation001/SourceLoc.idr+3−1

@@ -54,6 +54,8 @@ using (ctxt : Vect n Ty)

54 run (App f x) env = !(run f env) !(run x env)

55 run (Die {loc}) _ = Left loc

56

57+ lam_ : _ -> Tm (t::ctxt) t' -> Tm ctxt (Arr t t')

58+ lam_ _ = Lam

57

59

58exec : Tm [] t -> IO ()

60exec : Tm [] t -> IO ()

59exec tm = case run tm [] of

61exec tm = case run tm [] of

@@ -64,7 +66,7 @@ dsl lang

64 variable = Var

66 variable = Var

65 index_first = FZ

67 index_first = FZ

66 index_next = FS

68 index_next = FS

67− lambda = Lam

69+ lambda = lam_

68

70

69testTerm1 : Tm [] (Arr U U)

71testTerm1 : Tm [] (Arr U U)

70testTerm1 = lang (\x=>Die)

72testTerm1 = lang (\x=>Die)

test/sourceLocation001/expected+2−2

@@ -3,9 +3,9 @@ FileLoc "SourceLoc.idr" (16, 11) (16, 11)

3Testing using inline tactics

4FileLoc "SourceLoc.idr" (20, 17) (20, 17)

5Testing using metavariable with later definition

6−FileLoc "SourceLoc.idr" (96, 16) (96, 16)

6+FileLoc "SourceLoc.idr" (98, 16) (98, 16)

7-----------------------

8Success!

9−Error at FileLoc "SourceLoc.idr" (70, 23) (70, 23)

9+Error at FileLoc "SourceLoc.idr" (72, 23) (72, 23)

10Success!

11Success!

test/sugar001/test007.idr+1−1

@@ -19,7 +19,7 @@ instance Functor Eval where

19instance Applicative Eval where

20 pure x = MkEval (\e => Just x)

21

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

23 appAux : Maybe (a -> b) -> Maybe a -> Maybe b

24 appAux (Just fx) (Just gx) = Just (fx gx)

25 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

19instance Applicative Eval where

20 pure x = MkEval (\e => Just x)

21

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

23 app : Maybe (a -> b) -> Maybe a -> Maybe b

24 app (Just fx) (Just gx) = Just (fx gx)

25 app _ _ = Nothing