d1d6a7e · Idris-dev · git.iko.soy

CHANGELOG+13−13

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

2222* DSL notation can now be applied with $

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

2424 called from foreign code

25+* Instances can now have documentation strings.

2526

2627New in 0.9.16:

2728--------------

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

5960 solved automatically.

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

6162 of large expressions.

62−* EXPERIMENTAL Implementation of uniqueness types

63+* EXPERIMENTAL Implementation of uniqueness types

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

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

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

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

7374 library (see #1516)

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

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

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

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

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

7879 as code examples.

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

8081 provide error messages to IDE clients.

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

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

8283 Engine style)

8384

8485New in 0.9.14:

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

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

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

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

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

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

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

160161* Updated 'effects' library

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

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

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

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

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

188− a pattern for use in totality checking.

189+ a pattern for use in totality checking.

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

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

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

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

210211 types may now depend on earlier methods.

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

212213 expressions can be made instances of a type class.

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

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

214215 monadic/do/etc expressions.

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

216217 "if_valid", "if_error", etc.

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

335336Internal changes:

336337

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

338−* Fixed nested parameters blocks

339+* Fixed nested parameters blocks

339340* Improve efficiency of elaborator by:

340341 - only normalising when necessary

341342 - reducing backtracking with resolving ambiguities

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

416417Internal changes:

417418

418419* Some type class resolution fixes

419−* Several minor bug fixes

420+* Several minor bug fixes

420421* Performance improvements in resolving overloading and type classes

421422

422423New in 0.9.1:

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

464465Internal changes:

465466

466467* Everything :-)

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

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

469− which are verified by a minimal type checker.

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

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

470+ which are verified by a minimal type checker.

470471

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

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

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

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

474−

CONTRIBUTORS+1

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

2828raichoo

2929Philip Rasmussen

3030Reynir Reynisson

31+Adam Sandberg Eriksson

3132Seo Sanghyeon

3233Benjamin Saunders

3334Alexander Shabalin

idris.cabal+7

@@ -611,6 +611,13 @@ Extra-source-files:

611611 test/unique003/*.idr

612612 test/unique003/expected

613613

614+ test/docs001/run

615+ test/docs001/input

616+ test/docs001/*.idr

617+ test/docs001/expected

618+

619+

620+

614621source-repository head

615622 type: git

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

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

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

1−module Data.VectType

1+module Data.VectType

22

33import Data.Fin

44

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

66%default total

77

88namespace Vect {

9−

9+

1010infixr 7 ::

1111

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

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

531531

532532 fs <*> vs = zipWith apply fs vs

533533

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

535+||| uses the diagonal.

534536instance Monad (Vect n) where

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

536538

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

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

540542

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

542−-- Show

544+-- Show

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

544546

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

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

595597

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

597599-- internal implementations.

598−

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

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

195195instance MinBound Nat where

196196 minBound = Z

197197

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

198199instance Cast Integer Nat where

199200 cast = fromInteger

200201

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

250251 bottom = Z

251252

252253

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

253255instance Cast Int Nat where

254256 cast i = fromInteger (cast i)

255257

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

333335

334336

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

336−-- An informative comparison view

338+-- An informative comparison view

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

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

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

src/Idris/AbsSyntax.hs+11−11

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

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

9797

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

99−addImported pub f

99+addImported pub f

100100 = do i <- getIState

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

102102

@@ -134,7 +134,7 @@ addExport n = do ist <- getIState

134134 putIState $ ist { idris_exports = n : idris_exports ist }

135135

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

137−addUsedName fc n arg

137+addUsedName fc n arg

138138 = do ist <- getIState

139139 case lookupTyName n (tt_ctxt ist) of

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

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

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

10831083 pDocs

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

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

1086− = PInstance info f

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

1086+ = PInstance doc argDocs info f

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

10881088 n

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

@@ -1300,7 +1300,7 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

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

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

13021302 where

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

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

13041304 = (True, PImp 0 True opt n Placeholder)

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

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

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

15521552 PLam fc n ty' sc'

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

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

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

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

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

15571557 = case lookupDef n (tt_ctxt ist) of

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

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

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

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

17281728 t' <- sl t

1729− r' <- sl r

1729+ r' <- sl r

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

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

17321732 args' <- mapM slA args

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

19251925 match (PHidden x) (PHidden y)

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

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

1928− match (PHidden x) y

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

1928+ match (PHidden x) y

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

19301930 | otherwise = return []

1931− match x (PHidden y)

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

1931+ match x (PHidden y)

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

19331933 | otherwise = return []

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

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

src/Idris/AbsSyntaxTree.hs+29−25

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

5757 liftname :: Name -> Name,

5858 namespace :: Maybe [String],

5959 elabFC :: Maybe FC,

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

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

6161 Idris () }

6262

6363toplevel :: ElabInfo

@@ -601,14 +601,19 @@ data PDecl' t

601601 [PDecl' t] -- declarations

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

603603 -- class name, parameters, method declarations

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

605− Name -- class

606− [t] -- parameters

607− t -- full instance type

608− (Maybe Name) -- explicit name

609− [PDecl' t]

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

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

604+ | PInstance

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

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

607+ SyntaxInfo

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

609+ Name -- class

610+ [t] -- parameters

611+ t -- full instance type

612+ (Maybe Name) -- explicit name

613+ [PDecl' t]

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

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

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

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

613618 | PSyntax FC Syntax -- ^ Syntax definition

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

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

688693declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

692697declared (PDSL n _) = [n]

693698declared (PSyntax _ _) = []

694699declared (PMutual _ ds) = concatMap declared ds

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

707712tldeclared (PMutual _ ds) = concatMap tldeclared ds

708713tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

711716tldeclared _ = []

712717

713718defined :: PDecl -> [Name]

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

723728defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

727732defined (PDSL n _) = [n]

728733defined (PSyntax _ _) = []

729734defined (PMutual _ ds) = concatMap defined ds

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

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

779784 | PHidden PTerm -- ^ Irrelevant or hidden pattern

780785 | PType -- ^ 'Type' type

781− | PUniverse Universe -- ^ Some universe

786+ | PUniverse Universe -- ^ Some universe

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

783788 | PConstant Const -- ^ Builtin types

784789 | Placeholder -- ^ Underscore

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

11131118 | Expr Name

11141119 | SimpleExpr Name

11151120 deriving (Show, Eq)

1116−

1121+

11171122

11181123{-!

11191124deriving instance Binary SSymbol

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

13881393 where

13891394 startPrec = 0

13901395 funcAppPrec = 10

1391−

1396+

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

13931398 prettySe p bnd (PQuote r) =

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

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

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

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

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

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

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

14551460 bracket p funcAppPrec $

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

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

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

14671472 Just (Infixr p') -> p'

14681473 Just f' -> prec f' + 1

14691474 inFix l r = align . group $

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

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

14711476 group (prettySe right bnd r)

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

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

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

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

14871492 indent 2 (vsep (map ppcase cases))

14881493 where

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

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

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

14911496 in nest nestingSize $

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

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

15571562 prettyAs =

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

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

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

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

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

15621567 -- XXX: add pretty for tactics

15631568 prettySe p bnd (PProof ts) =

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

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

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

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

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

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

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

17341739showDeclImp _ _ = text "..."

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

@@ -1905,16 +1910,16 @@ implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

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

19061911 where

19071912 ni env (PRef _ n)

1908− | not (n `elem` env)

1913+ | not (n `elem` env)

19091914 = case lookupTy n (tt_ctxt ist) of

19101915 [] -> [n]

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

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

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

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

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

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

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

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

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

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

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

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

@@ -1944,7 +1949,7 @@ namesIn uvars ist tm = nub $ ni [] tm

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

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

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

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

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

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

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

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

@@ -2003,4 +2008,3 @@ getErasureInfo ist n =

20032008 case lookupCtxtExact n (idris_optimisation ist) of

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

20052010 Nothing -> []

2006−

src/Idris/DeepSeq.hs+5−5

@@ -153,11 +153,14 @@ instance (NFData t) => NFData (PDecl' t) where

153153 = rnf x1 `seq`

154154 rnf x2 `seq`

155155 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

156− rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8)

156+ rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

157157 = rnf x1 `seq`

158158 rnf x2 `seq`

159159 rnf x3 `seq`

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

160+ rnf x4 `seq`

161+ rnf x5 `seq`

162+ rnf x6 `seq`

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

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

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

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

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

357360 rnf x4 `seq`

358361 rnf x5 `seq`

359362 rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

360−

361−

362−

src/Idris/Docs.hs+50−12

@@ -32,7 +32,8 @@ data Docs' d = FunDoc (FunDoc' d)

3232 | ClassDoc Name d -- class docs

3333 [FunDoc' d] -- method docs

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

35− [PTerm] -- instances

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

36+ [PTerm] -- subclasses

3637 [PTerm] -- superclasses

3738 | ModDoc [String] -- Module name

3839 d

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

8889 if null args then text "No constructors."

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

9091 vsep (map (pprintFD ist) args))

91−pprintDocs ist (ClassDoc n doc meths params instances superclasses)

92+pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)

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

9394 if nullDocstring doc

9495 then empty

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

100101 vsep (map (pprintFD ist) meths))

101102 <$>

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

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

104− else map dumpInstance instances'))

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

105+ else map pprintInstance instances))

105106 <>

106107 (if null subclasses then empty

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

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

118119 ppo = ppOptionIst ist

119120 infixes = idris_infixes ist

120121

122+ pprintInstance (term, (doc, argDocs)) =

123+ nest 4 (dumpInstance term <>

124+ (if nullDocstring doc

125+ then empty

126+ else line <>

127+ renderDocstring

128+ (renderDocTerm

129+ (pprintDelab ist)

130+ (normaliseAll (tt_ctxt ist) []))

131+ doc) <>

132+ if null argDocs

133+ then empty

134+ else line <> vsep (map (prettyInstanceParam (map fst argDocs)) argDocs))

135+

136+ prettyInstanceParam params (name, doc) =

137+ if nullDocstring doc

138+ then empty

139+ else prettyName True False (zip params (repeat False)) name <+>

140+ showDoc ist doc

141+

142+-- if any (isJust . snd) params

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

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

145+

121146 dumpInstance :: PTerm -> Doc OutputAnnotation

122147 dumpInstance = pprintPTerm ppo params' [] infixes

123148

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

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

141166 isSubclass _ = False

142167

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

144−

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

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

147− else hsep (punctuate comma (map (prettyName True False params' . fst) params))

168+ prettyParameters =

169+ if any (isJust . snd) params

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

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

148172

149173pprintDocs ist (ModDoc mod docs)

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

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

186210 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

187211 docstr = maybe emptyDocstring fst docStrings

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

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

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

214+ listToMaybe .

215+ flip lookupCtxt (idris_docstrings i))

216+ (class_instances ci)

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

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

190219 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

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

192− return $ ClassDoc n docstr mdocs params instances superclasses

221+ return $ ClassDoc

222+ n docstr mdocs params

223+ instances' (map fst subclasses) superclasses

193224 where

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

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

195226 getDInst _ = Nothing

196227

228+ isSubclass (PPi (Constraint _ _) _ (PApp _ _ args) (PApp _ (PRef _ nm) args'))

229+ = nm == n && map getTm args == map getTm args'

230+ isSubclass (PPi _ _ _ pt)

231+ = isSubclass pt

232+ isSubclass _

233+ = False

234+

197235docFun :: Name -> Idris FunDoc

198236docFun n

199237 = do i <- getIState

src/Idris/Elab/Class.hs+7−9

@@ -109,8 +109,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

109109 mdec x = x

110110

111111 -- TODO: probably should normalise

112− checkDefaultSuperclassInstance :: PDecl -> Idris ()

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

112+ checkDefaultSuperclassInstance :: PDecl -> Idris ()

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

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

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

116116 i <- getIState

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

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

121121 return ()

122122

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

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

124124 impbind [] x = x

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

126126

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

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

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

129129 conbind [] x = x

130130

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

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

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

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

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

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

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

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

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

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

155155

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

157157 tydecl _ = False

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

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

159159 instdecl _ = False

160160 clause (PClauses _ _ _ _) = True

161161 clause _ = False

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

221221

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

223223 = PPi p n ty (insertConstraint c sc)

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

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

225225 (sMN 0 "class") c sc

226226

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

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

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

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

232232 toExp ns e sc = sc

233−

234−

src/Idris/Elab/Instance.hs+7−5

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

5151import Util.Pretty(pretty, text)

5252

5353elabInstance :: ElabInfo -> SyntaxInfo ->

54+ Docstring (Either Err PTerm) ->

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

5456 ElabWhat -> -- phase

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

5658 Name -> -- the class

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

5860 PTerm -> -- full instance type

5961 Maybe Name -> -- explicit name

6062 [PDecl] -> Idris ()

61−elabInstance info syn what fc cs n ps t expn ds = do

63+elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

6264 i <- getIState

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

6466 [c] -> return c

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

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

7072 let emptyclass = null (class_methods ci)

7173 when (what /= EDefns || (null ds && not emptyclass)) $ do

72− nty <- elabType' True info syn emptyDocstring [] fc [] iname t

74+ nty <- elabType' True info syn doc argDocs fc [] iname t

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

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

7577 case expn of

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

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

148150 Just nm -> nm

149151

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

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

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

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

152154

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

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

154156 = case lookupCtxtName n (idris_classes i) of

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

156158 case lookupTy iname (tt_ctxt i) of

src/Idris/ElabDecls.hs+4−5

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

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

201201 isDataDecl _ = False

202202

203− setMutData ns n

203+ setMutData ns n

204204 = do i <- getIState

205205 case lookupCtxt n (idris_datatypes i) of

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

207− putIState $ i { idris_datatypes

207+ putIState $ i { idris_datatypes

208208 = addDef n x' (idris_datatypes i) }

209209 _ -> return ()

210210

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

233233 | what /= EDefns

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

235235 elabClass info (s { syn_params = [] }) doc f cs n ps pdocs ds

236−elabDecl' what info (PInstance s f cs n ps t expn ds)

236+elabDecl' what info (PInstance doc argDocs s f cs n ps t expn ds)

237237 = do iLOG $ "Elaborating instance " ++ show n

238− elabInstance info s what f cs n ps t expn ds

238+ elabInstance info s doc argDocs what f cs n ps t expn ds

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

240240 | what /= ETypes

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

@@ -257,4 +257,3 @@ elabDecl' what info (PTransform fc safety old new)

257257 = do elabTransform info fc safety old new

258258 return ()

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

260−

src/Idris/IBC.hs+31−27

@@ -91,9 +91,9 @@ deriving instance Binary IBCFile

9191initIBC :: IBCFile

9292initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] []

9393

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

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

9595 -> FilePath -> Idris ()

96−loadIBC reexport fp

96+loadIBC reexport fp

9797 = do imps <- getImported

9898 let redo = case lookup fp imps of

9999 Nothing -> True

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

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

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

196196ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }

197−ibc i (IBCDef n) f

197+ibc i (IBCDef n) f

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

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

200200 _ -> ifail "IBC write failed"

@@ -239,13 +239,13 @@ ibc i (IBCExport n) f = return f { ibc_exports = n : ibc_exports f }

239239process :: Bool -- ^ Reexporting

240240 -> IBCFile -> FilePath -> Idris ()

241241process reexp i fn

242− | ver i /= ibcVersion

242+ | ver i /= ibcVersion

243243 = do iLOG "ibc out of date"

244244 let e = if ver i < ibcVersion then " an earlier " else " a later "

245245 ifail $ "Incompatible ibc version.\nThis library was built with"

246246 ++ e ++ "version of Idris.\n" ++

247247 "Please clean and rebuild."

248−

248+

249249 --- please rebuild"

250250 | otherwise =

251251 do srcok <- runIO $ doesFileExist (sourcefile i)

@@ -323,7 +323,7 @@ pImportDirs fs = mapM_ addImportDir fs

323323

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

325325pImports fs

326− = do mapM_ (\(re, f) ->

326+ = do mapM_ (\(re, f) ->

327327 do i <- getIState

328328 ibcsd <- valIBCSubDir i

329329 ids <- allImportDirs

@@ -427,20 +427,20 @@ pHdrs :: [(Codegen, String)] -> Idris ()

427427pHdrs hs = mapM_ (uncurry addHdr) hs

428428

429429pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()

430−pPatdefs ds

431− = mapM_ (\ (n, d) ->

430+pPatdefs ds

431+ = mapM_ (\ (n, d) ->

432432 do i <- getIState

433433 putIState (i { idris_patdefs = addDef n (force d) (idris_patdefs i) }))

434434 ds

435435

436436pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()

437−pDefs reexp syms ds

437+pDefs reexp syms ds

438438 = mapM_ (\ (n, d) ->

439439 do d' <- updateDef d

440440 case d' of

441− TyDecl _ _ -> return ()

441+ TyDecl _ _ -> return ()

442442 _ -> do iLOG $ "SOLVING " ++ show n

443− solveDeferred n

443+ solveDeferred n

444444 i <- getIState

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

446446 putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })

@@ -509,8 +509,8 @@ pMDocs ds = mapM_ addMDocStr ds

509509

510510pAccess :: Bool -- ^ Reexporting?

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

512−pAccess reexp ds

513− = mapM_ (\ (n, a_in) ->

512+pAccess reexp ds

513+ = mapM_ (\ (n, a_in) ->

514514 do let a = if reexp then a_in else Hidden

515515 logLvl 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a

516516 i <- getIState

@@ -568,7 +568,7 @@ pFunctionErrorHandlers ((fn, arg, handler):ns) = do addFunctionErrorHandlers fn

568568

569569pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()

570570pMetavars ns = do i <- getIState

571− putIState $ i { idris_metavars = Data.List.reverse ns

571+ putIState $ i { idris_metavars = Data.List.reverse ns

572572 ++ idris_metavars i }

573573

574574----- For Cheapskate and docstrings

@@ -862,7 +862,7 @@ safeToEnum :: (Enum a, Bounded a, Integral int) => String -> int -> a

862862safeToEnum label x' = result

863863 where

864864 x = fromIntegral x'

865− result

865+ result

866866 | x < fromEnum (minBound `asTypeOf` result)

867867 || x > fromEnum (maxBound `asTypeOf` result)

868868 = error $ label ++ ": corrupted binary representation in IBC"

@@ -1248,15 +1248,18 @@ instance (Binary t) => Binary (PDecl' t) where

12481248 put x6

12491249 put x7

12501250 put x8

1251− PInstance x1 x2 x3 x4 x5 x6 x7 x8 -> do putWord8 8

1252− put x1

1253− put x2

1254− put x3

1255− put x4

1256− put x5

1257− put x6

1258− put x7

1259− put x8

1251+ PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

1252+ do putWord8 8

1253+ put x1

1254+ put x2

1255+ put x3

1256+ put x4

1257+ put x5

1258+ put x6

1259+ put x7

1260+ put x8

1261+ put x9

1262+ put x10

12601263 PDSL x1 x2 -> do putWord8 9

12611264 put x1

12621265 put x2

@@ -1288,7 +1291,7 @@ instance (Binary t) => Binary (PDecl' t) where

12881291 put x1

12891292 put x2

12901293 put x3

1291− put x4

1294+ put x4

12921295 get

12931296 = do i <- getWord8

12941297 case i of

@@ -1350,7 +1353,9 @@ instance (Binary t) => Binary (PDecl' t) where

13501353 x6 <- get

13511354 x7 <- get

13521355 x8 <- get

1353− return (PInstance x1 x2 x3 x4 x5 x6 x7 x8)

1356+ x9 <- get

1357+ x10 <- get

1358+ return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

13541359 9 -> do x1 <- get

13551360 x2 <- get

13561361 return (PDSL x1 x2)

@@ -2198,4 +2203,3 @@ instance Binary Codegen where

21982203 return (Via x1)

21992204 1 -> return Bytecode

22002205 _ -> error "Corrupted binary data for Codegen"

2201−

src/Idris/IdrisDoc.hs+5−5

@@ -168,7 +168,7 @@ removeOrphans list =

168168 in filter ((`S.notMember` children) . (\(n, _, _) -> n)) list

169169

170170 where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds

171− names (Just (ClassDoc _ _ fds _ _ _)) = map (\(FD n _ _ _ _) -> n) fds

171+ names (Just (ClassDoc _ _ fds _ _ _ _)) = map (\(FD n _ _ _ _) -> n) fds

172172 names _ = []

173173

174174-- | Whether a Name names something which should be documented

@@ -219,7 +219,7 @@ referredNss (n, Just d, _) =

219219

220220 where getFunDocs (FunDoc f) = [f]

221221 getFunDocs (DataDoc f fs) = f:fs

222− getFunDocs (ClassDoc _ _ fs _ _ _) = fs

222+ getFunDocs (ClassDoc _ _ fs _ _ _ _) = fs

223223 types (FD _ _ args t _) = t:(map second args)

224224 second (_, x, _, _) = x

225225

@@ -417,7 +417,7 @@ createIndex nss out =

417417 BS2.hPut h $ renderHtml $ wrapper Nothing $ do

418418 H.h1 $ "Namespaces"

419419 H.ul ! class_ "names" $ do

420− let path ns = "docs" </> genRelNsPath ns "html"

420+ let path ns = "docs" </> genRelNsPath ns "html"

421421 item ns = do let n = toHtml $ nsName2Str ns

422422 link = toValue $ path ns

423423 H.li $ H.a ! href link ! class_ "code" $ n

@@ -439,7 +439,7 @@ createNsDoc :: IState -- ^ Needed to determine the types of names

439439createNsDoc ist ns content out =

440440 do let tpath = out </> "docs" </> (genRelNsPath ns "html")

441441 dir = takeDirectory tpath

442− file = takeFileName tpath

442+ file = takeFileName tpath

443443 haveDocs (_, Just d, _) = [d]

444444 haveDocs _ = []

445445 -- We cannot do anything without a Doc

@@ -575,7 +575,7 @@ createOtherDoc :: IState -- ^ Needed to determine the types of names

575575 -> H.Html -- ^ Resulting HTML

576576createOtherDoc ist (FunDoc fd) = createFunDoc ist fd

577577

578−createOtherDoc ist (ClassDoc n docstring fds _ _ _) = do

578+createOtherDoc ist (ClassDoc n docstring fds _ _ _ _) = do

579579 H.dt ! (A.id $ toValue $ show n) $ do

580580 H.span ! class_ "word" $ do "class"; nbsp

581581 H.span ! class_ "name type"

src/Idris/ParseHelpers.hs+2−2

@@ -587,7 +587,7 @@ collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

587587collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

588588collect (PClass doc f s cs n ps pdocs ds : ds')

589589 = PClass doc f s cs n ps pdocs (collect ds) : collect ds'

590−collect (PInstance f s cs n ps t en ds : ds')

591− = PInstance f s cs n ps t en (collect ds) : collect ds'

590+collect (PInstance doc argDocs f s cs n ps t en ds : ds')

591+ = PInstance doc argDocs f s cs n ps t en (collect ds) : collect ds'

592592collect (d : ds) = d : collect ds

593593collect [] = []

src/Idris/Parser.hs+37−30

@@ -9,7 +9,7 @@ module Idris.Parser(module Idris.Parser,

99import Prelude hiding (pi)

1010

1111import Text.Trifecta.Delta

12−import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)

12+import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace, Err)

1313import Text.Parser.LookAhead

1414import Text.Parser.Expression

1515import qualified Text.Parser.Token as Tok

@@ -87,7 +87,7 @@ import System.IO

8787{- | Parses module definition

8888

8989@

90− ModuleHeader ::= 'module' Identifier_t ';'?;

90+ ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;

9191@

9292-}

9393moduleHeader :: IdrisParser (Maybe (Docstring ()), [String])

@@ -291,7 +291,7 @@ syntaxRule syn

291291

292292 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :

293293 mkSimple es

294− -- Can't parse a full expression followed by operator like characters due to ambiguity

294+ -- Can't parse a full expression followed by operator like characters due to ambiguity

295295 mkSimple' (Expr e : Symbol s : es)

296296 | takeWhile (`elem` opChars) ts /= "" && ts `notElem` invalidOperators = SimpleExpr e : Symbol s : mkSimple' es

297297 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s

@@ -348,13 +348,9 @@ fnDecl' :: SyntaxInfo -> IdrisParser PDecl

348348fnDecl' syn = checkFixity $

349349 do (doc, argDocs, fc, opts', n, acc) <- try (do

350350 pushIndent

351− (doc, argDocs) <- option noDocs docComment

351+ (doc, argDocs) <- docstring syn

352352 ist <- get

353− let doc' = annotCode (tryFullExpr syn ist) doc

354− argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

355− | (n, d) <- argDocs ]

356−

357− initOpts = if default_total ist

353+ let initOpts = if default_total ist

358354 then [TotalFn]

359355 else []

360356 opts <- fnOpts initOpts

@@ -364,7 +360,7 @@ fnDecl' syn = checkFixity $

364360 let n = expandNS syn n_in

365361 fc <- getFC

366362 lchar ':'

367− return (doc', argDocs', fc, opts', n, acc))

363+ return (doc, argDocs, fc, opts', n, acc))

368364 ty <- typeExpr (allowImp syn)

369365 terminator

370366 addAcc n acc

@@ -459,12 +455,10 @@ Postulate ::=

459455@

460456-}

461457postulate :: SyntaxInfo -> IdrisParser PDecl

462−postulate syn = do doc <- try $ do (doc, _) <- option noDocs docComment

463− ist <- get

464− let doc' = annotCode (tryFullExpr syn ist) doc

458+postulate syn = do doc <- try $ do (doc, _) <- docstring syn

465459 pushIndent

466460 reserved "postulate"

467− return doc'

461+ return doc

468462 ist <- get

469463 let initOpts = if default_total ist

470464 then [TotalFn]

@@ -587,7 +581,7 @@ ClassBlock ::=

587581classBlock :: SyntaxInfo -> IdrisParser [PDecl]

588582classBlock syn = do reserved "where"

589583 openBlock

590− ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)

584+ ds <- many (notEndBlock >> instance_ syn <|> fnDecl syn)

591585 closeBlock

592586 return (concat ds)

593587 <?> "class block"

@@ -608,15 +602,14 @@ Class ::=

608602@

609603-}

610604class_ :: SyntaxInfo -> IdrisParser [PDecl]

611−class_ syn = do (doc, argDocs, acc) <- try (do

612− (doc, argDocs) <- option noDocs docComment

613− ist <- get

614− let doc' = annotCode (tryFullExpr syn ist) doc

615− argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

616− | (n, d) <- argDocs ]

617− acc <- optional accessibility

618− return (doc', argDocs', acc))

619− reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName

605+class_ syn = do (doc, argDocs, acc)

606+ <- try (do (doc, argDocs) <- docstring syn

607+ acc <- optional accessibility

608+ reserved "class"

609+ return (doc, argDocs, acc))

610+ fc <- getFC

611+ cons <- constraintList syn

612+ n_in <- fnName

620613 let n = expandNS syn n_in

621614 cs <- many carg

622615 ds <- option [] (classBlock syn)

@@ -634,7 +627,7 @@ class_ syn = do (doc, argDocs, acc) <- try (do

634627

635628@

636629 Instance ::=

637− 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?

630+ DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?

638631 ;

639632@

640633

@@ -643,7 +636,9 @@ InstanceName ::= '[' Name ']';

643636@

644637-}

645638instance_ :: SyntaxInfo -> IdrisParser [PDecl]

646−instance_ syn = do reserved "instance"; fc <- getFC

639+instance_ syn = do (doc, argDocs)

640+ <- try (docstring syn <* reserved "instance")

641+ fc <- getFC

647642 en <- optional instanceName

648643 cs <- constraintList syn

649644 cn <- fnName

@@ -651,7 +646,7 @@ instance_ syn = do reserved "instance"; fc <- getFC

651646 let sc = PApp fc (PRef fc cn) (map pexp args)

652647 let t = bindList (PPi constraint) cs sc

653648 ds <- option [] (instanceBlock syn)

654− return [PInstance syn fc cs cn args t en ds]

649+ return [PInstance doc argDocs syn fc cs cn args t en ds]

655650 <?> "instance declaration"

656651 where instanceName :: IdrisParser Name

657652 instanceName = do lchar '['; n_in <- fnName; lchar ']'

@@ -660,6 +655,18 @@ instance_ syn = do reserved "instance"; fc <- getFC

660655 <?> "instance name"

661656

662657

658+-- | Parse a docstring

659+docstring :: SyntaxInfo

660+ -> IdrisParser (Docstring (Either Err PTerm),

661+ [(Name,Docstring (Either Err PTerm))])

662+docstring syn = do (doc, argDocs) <- option noDocs docComment

663+ ist <- get

664+ let doc' = annotCode (tryFullExpr syn ist) doc

665+ argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

666+ | (n, d) <- argDocs ]

667+ return (doc', argDocs')

668+

669+

663670{- | Parses a using declaration list

664671

665672@

@@ -1403,9 +1410,9 @@ loadSource lidr f toline

14031410 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)

14041411 toMutual x = let r = PMutual (fileFC "single mutual") [x] in

14051412 case x of

1406− PClauses _ _ _ _ -> r

1407− PClass _ _ _ _ _ _ _ _ -> r

1408− PInstance _ _ _ _ _ _ _ _ -> r

1413+ PClauses{} -> r

1414+ PClass{} -> r

1415+ PInstance{} -> r

14091416 _ -> x

14101417

14111418 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()

src/Idris/REPL.hs+2−2

@@ -811,8 +811,8 @@ process fn (NewDefn decls) = do

811811 fixClauses :: PDecl' t -> PDecl' t

812812 fixClauses (PClauses fc opts _ css@(clause:cs)) =

813813 PClauses fc opts (getClauseName clause) css

814− fixClauses (PInstance syn fc constraints cls parms ty instName decls) =

815− PInstance syn fc constraints cls parms ty instName (map fixClauses decls)

814+ fixClauses (PInstance doc argDocs syn fc constraints cls parms ty instName decls) =

815+ PInstance doc argDocs syn fc constraints cls parms ty instName (map fixClauses decls)

816816 fixClauses decl = decl

817817

818818process fn (Undefine names) = undefine names

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