d910c2c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Use Markdown to represent docstrings

d910c2cDavid Raymond Christiansen13 years ago

idris.cabal+2

compare with master

unifiedsplit

@@ -440,6 +440,7 @@ Library

440 , Idris.DeepSeq

441 , Idris.Delaborate

442 , Idris.Docs

443+ , Idris.Docstrings

443 , Idris.ElabDecls

444 , Idris.ElabDecls

444 , Idris.ElabTerm

445 , Idris.ElabTerm

445 , Idris.Error

446 , Idris.Error

@@ -506,6 +507,7 @@ Library

506 , ansi-wl-pprint

507 , ansi-wl-pprint

507 , binary

508 , binary

508 , bytestring

509 , bytestring

510+ , cheapskate

509 , containers >= 0.5

511 , containers >= 0.5

510 , directory

512 , directory

511 , directory >= 1.2

513 , directory >= 1.2

src/Idris/AbsSyntax.hs+2−1

@@ -9,6 +9,7 @@ import Idris.Core.Elaborate hiding (Tactic(..))

9import Idris.Core.Typecheck

10import Idris.AbsSyntaxTree

11import Idris.Colours

12+import Idris.Docstrings

12import Idris.IdeSlave

13import Idris.IdeSlave

13import IRTS.CodegenCommon

14import IRTS.CodegenCommon

14import Util.DynamicLinker

15import Util.DynamicLinker

@@ -262,7 +263,7 @@ addCoercion :: Name -> Idris ()

262addCoercion n = do i <- getIState

263addCoercion n = do i <- getIState

263 putIState $ i { idris_coercions = nub $ n : idris_coercions i }

264 putIState $ i { idris_coercions = nub $ n : idris_coercions i }

264

265

265−addDocStr :: Name -> String -> [(Name, String)] -> Idris ()

266+addDocStr :: Name -> Docstring -> [(Name, Docstring)] -> Idris ()

266addDocStr n doc args

267addDocStr n doc args

267 = do i <- getIState

268 = do i <- getIState

268 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }

269 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }

src/Idris/AbsSyntaxTree.hs+27−26

@@ -7,6 +7,7 @@ import Idris.Core.TT

7import Idris.Core.Evaluate

8import Idris.Core.Elaborate hiding (Tactic(..))

9import Idris.Core.Typecheck

10+import Idris.Docstrings

10import IRTS.Lang

11import IRTS.Lang

11import IRTS.CodegenCommon

12import IRTS.CodegenCommon

12import Util.Pretty

13import Util.Pretty

@@ -111,7 +112,7 @@ data IState = IState {

111 idris_flags :: Ctxt [FnOpt],

112 idris_flags :: Ctxt [FnOpt],

112 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

113 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

113 idris_calledgraph :: Ctxt [Name],

114 idris_calledgraph :: Ctxt [Name],

114− idris_docstrings :: Ctxt (String, [(Name, String)]),

115+ idris_docstrings :: Ctxt (Docstring, [(Name, Docstring)]),

115 idris_tyinfodata :: Ctxt TIData,

116 idris_tyinfodata :: Ctxt TIData,

116 idris_totcheck :: [(FC, Name)], -- names to check totality on

117 idris_totcheck :: [(FC, Name)], -- names to check totality on

117 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

118 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

@@ -450,15 +451,15 @@ data ProvideWhat = ProvTerm -- ^ only allow providing terms

450-- datatypes and typeclasses.

451-- datatypes and typeclasses.

451data PDecl' t

452data PDecl' t

452 = PFix FC Fixity [String] -- ^ Fixity declaration

453 = PFix FC Fixity [String] -- ^ Fixity declaration

453− | PTy String [(Name, String)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration

454+ | PTy Docstring [(Name, Docstring)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration

454− | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate

455+ | PPostulate Docstring SyntaxInfo FC FnOpts Name t -- ^ Postulate

455 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

456 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

456 | PCAF FC Name t -- ^ Top level constant

457 | PCAF FC Name t -- ^ Top level constant

457− | PData String [(Name, String)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

458+ | PData Docstring [(Name, Docstring)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

458 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

459 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

459 | PNamespace String [PDecl' t] -- ^ New namespace

460 | PNamespace String [PDecl' t] -- ^ New namespace

460− | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration

461+ | PRecord Docstring SyntaxInfo FC Name t Docstring Name t -- ^ Record declaration

461− | PClass String SyntaxInfo FC

462+ | PClass Docstring SyntaxInfo FC

462 [t] -- constraints

463 [t] -- constraints

463 Name

464 Name

464 [(Name, t)] -- parameters

465 [(Name, t)] -- parameters

@@ -512,7 +513,7 @@ deriving instance NFData PClause'

512-- | Data declaration

513-- | Data declaration

513data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype

514data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype

514 d_tcon :: t, -- ^ Type constructor

515 d_tcon :: t, -- ^ Type constructor

515− d_cons :: [(String, [(Name, String)], Name, t, FC, [Name])] -- ^ Constructors

516+ d_cons :: [(Docstring, [(Name, Docstring)], Name, t, FC, [Name])] -- ^ Constructors

516 }

517 }

517 -- ^ Data declaration

518 -- ^ Data declaration

518 | PLaterdecl { d_name :: Name, d_tcon :: t }

519 | PLaterdecl { d_name :: Name, d_tcon :: t }

@@ -948,9 +949,9 @@ inferTy = sMN 0 "__Infer"

948inferCon = sMN 0 "__infer"

949inferCon = sMN 0 "__infer"

949inferDecl = PDatadecl inferTy

950inferDecl = PDatadecl inferTy

950 PType

951 PType

951− [("", [], inferCon, PPi impl (sMN 0 "iType") PType (

952+ [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (

952− PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

953+ PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

953− (PRef bi inferTy)), bi, [])]

954+ (PRef bi inferTy)), bi, [])]

954inferOpts = []

955inferOpts = []

955

956

956infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

957infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

@@ -978,7 +979,7 @@ primNames = [unitTy, unitCon,

978unitTy = sMN 0 "__Unit"

979unitTy = sMN 0 "__Unit"

979unitCon = sMN 0 "__II"

980unitCon = sMN 0 "__II"

980unitDecl = PDatadecl unitTy PType

981unitDecl = PDatadecl unitTy PType

981− [("", [], unitCon, PRef bi unitTy, bi, [])]

982+ [(emptyDocstring, [], unitCon, PRef bi unitTy, bi, [])]

982unitOpts = [DefaultEliminator]

983unitOpts = [DefaultEliminator]

983

984

984falseTy = sMN 0 "__False"

985falseTy = sMN 0 "__False"

@@ -988,12 +989,12 @@ falseOpts = []

988pairTy = sMN 0 "__Pair"

989pairTy = sMN 0 "__Pair"

989pairCon = sMN 0 "__MkPair"

990pairCon = sMN 0 "__MkPair"

990pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

991pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

991− [("", [], pairCon, PPi impl (n "A") PType (

992+ [(emptyDocstring, [], pairCon, PPi impl (n "A") PType (

992− PPi impl (n "B") PType (

993+ PPi impl (n "B") PType (

993− PPi expl (n "a") (PRef bi (n "A")) (

994+ PPi expl (n "a") (PRef bi (n "A")) (

994− PPi expl (n "b") (PRef bi (n "B"))

995+ PPi expl (n "b") (PRef bi (n "B"))

995− (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

996+ (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

996− pexp (PRef bi (n "B"))])))), bi, [])]

997+ pexp (PRef bi (n "B"))])))), bi, [])]

997 where n a = sMN 0 a

998 where n a = sMN 0 a

998pairOpts = []

999pairOpts = []

999

1000

@@ -1002,21 +1003,21 @@ eqCon = sUN "refl"

1002eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

1003eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

1003 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

1004 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

1004 PType)

1005 PType)

1005− [("", [], eqCon, PPi impl (n "A") PType (

1006+ [(emptyDocstring, [], eqCon, PPi impl (n "A") PType (

1006− PPi impl (n "x") (PRef bi (n "A"))

1007+ PPi impl (n "x") (PRef bi (n "A"))

1007− (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

1008+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

1008− pimp (n "B") Placeholder False,

1009+ pimp (n "B") Placeholder False,

1009− pexp (PRef bi (n "x")),

1010+ pexp (PRef bi (n "x")),

1010− pexp (PRef bi (n "x"))])), bi, [])]

1011+ pexp (PRef bi (n "x"))])), bi, [])]

1011 where n a = sMN 0 a

1012 where n a = sMN 0 a

1012eqOpts = []

1013eqOpts = []

1013

1014

1014elimName = sUN "__Elim"

1015elimName = sUN "__Elim"

1015elimMethElimTy = sUN "__elimTy"

1016elimMethElimTy = sUN "__elimTy"

1016elimMethElim = sUN "elim"

1017elimMethElim = sUN "elim"

1017−elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]

1018+elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]

1018− [PTy "" [] defaultSyntax bi [TotalFn] elimMethElimTy PType,

1019+ [PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElimTy PType,

1019− PTy "" [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1020+ PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1020

1021

1021-- Defined in builtins.idr

1022-- Defined in builtins.idr

1022sigmaTy = sUN "Exists"

1023sigmaTy = sUN "Exists"

src/Idris/DeepSeq.hs+42

@@ -6,6 +6,48 @@ import Idris.AbsSyntaxTree

7import Control.DeepSeq

9+import qualified Cheapskate.Types as CT

10+

11+-- Manual from imported libs

12+instance NFData CT.Doc where

13+ rnf (CT.Doc opts contents) = rnf opts `seq` rnf contents `seq` ()

14+

15+instance NFData CT.Options where

16+ rnf (CT.Options x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

17+

18+instance NFData CT.Block where

19+ rnf (CT.Para lines) = rnf lines `seq` ()

20+ rnf (CT.Header i lines) = rnf i `seq` rnf lines `seq` ()

21+ rnf (CT.Blockquote bs) = rnf bs `seq` ()

22+ rnf (CT.List b t xs) = rnf b `seq` rnf t `seq` rnf xs `seq` ()

23+ rnf (CT.CodeBlock attr txt) = rnf attr `seq` rnf txt `seq` ()

24+ rnf (CT.HtmlBlock txt) = rnf txt `seq` ()

25+ rnf CT.HRule = ()

26+

27+instance NFData CT.Inline where

28+ rnf (CT.Str txt) = rnf txt `seq` ()

29+ rnf CT.Space = ()

30+ rnf CT.SoftBreak = ()

31+ rnf CT.LineBreak = ()

32+ rnf (CT.Emph xs) = rnf xs `seq` ()

33+ rnf (CT.Strong xs) = rnf xs `seq` ()

34+ rnf (CT.Code xs) = rnf xs `seq` ()

35+ rnf (CT.Link a b xs) = rnf a `seq` rnf b `seq` rnf xs `seq` ()

36+ rnf (CT.Image a b c) = rnf a `seq` rnf b `seq` rnf c `seq` ()

37+ rnf (CT.Entity a) = rnf a `seq` ()

38+ rnf (CT.RawHtml x) = rnf x `seq` ()

39+

40+instance NFData CT.ListType where

41+ rnf (CT.Bullet c) = rnf c `seq` ()

42+ rnf (CT.Numbered nw i) = rnf nw `seq` rnf i `seq` ()

43+

44+instance NFData CT.CodeAttr where

45+ rnf (CT.CodeAttr a b) = rnf a `seq` rnf b `seq` ()

46+

47+instance NFData CT.NumWrapper where

48+ rnf CT.PeriodFollowing = ()

49+ rnf CT.ParenFollowing = ()

50+

9-- All generated by 'derive'

51-- All generated by 'derive'

11instance NFData Forceability where

53instance NFData Forceability where

src/Idris/Docs.hs+15−13

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

1+{-# LANGUAGE PatternGuards #-}

1module Idris.Docs where

2module Idris.Docs where

3import Idris.AbsSyntax

4import Idris.AbsSyntax

@@ -5,6 +6,7 @@ import Idris.AbsSyntaxTree

5import Idris.Delaborate

6import Idris.Delaborate

6import Idris.Core.TT

7import Idris.Core.TT

7import Idris.Core.Evaluate

8import Idris.Core.Evaluate

9+import Idris.Docstrings

9import Util.Pretty

11import Util.Pretty

@@ -13,8 +15,8 @@ import Data.List

14-- TODO: Only include names with public/abstract accessibility

16-- TODO: Only include names with public/abstract accessibility

16−data FunDoc = FD Name String

18+data FunDoc = FD Name Docstring

17− [(Name, PTerm, Plicity, Maybe String)] -- args: name, ty, implicit, docs

19+ [(Name, PTerm, Plicity, Maybe Docstring)] -- args: name, ty, implicit, docs

18 PTerm -- function type

20 PTerm -- function type

19 (Maybe Fixity)

21 (Maybe Fixity)

20 deriving Show

22 deriving Show

@@ -22,16 +24,16 @@ data FunDoc = FD Name String

22data Docs = FunDoc FunDoc

24data Docs = FunDoc FunDoc

23 | DataDoc FunDoc -- type constructor docs

25 | DataDoc FunDoc -- type constructor docs

24 [FunDoc] -- data constructor docs

26 [FunDoc] -- data constructor docs

25− | ClassDoc Name String -- class docs

27+ | ClassDoc Name Docstring -- class docs

26 [FunDoc] -- method docs

28 [FunDoc] -- method docs

27 deriving Show

29 deriving Show

29−showDoc "" = empty

31+showDoc d | nullDocstring d = empty

30−showDoc x = text " -- " <> text x

32+ | otherwise = text " -- " <> renderDocstring d

32pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation

34pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation

33pprintFD imp (FD n doc args ty f)

35pprintFD imp (FD n doc args ty f)

34− = nest 4 (prettyName imp [] n <+> colon <+> prettyImp imp ty <$> showDoc doc <$>

36+ = nest 4 (prettyName imp [] n <+> colon <+> prettyImp imp ty <$> renderDocstring doc <$>

35 maybe empty (\f -> text (show f) <> line) f <>

37 maybe empty (\f -> text (show f) <> line) f <>

36 let argshow = showArgs args [] in

38 let argshow = showArgs args [] in

37 if not (null argshow)

39 if not (null argshow)

@@ -41,20 +43,20 @@ pprintFD imp (FD n doc args ty f)

41 where showArgs ((n, ty, Exp {}, d):args) bnd

43 where showArgs ((n, ty, Exp {}, d):args) bnd

42 = bindingOf n False <+> colon <+>

44 = bindingOf n False <+> colon <+>

43 pprintPTerm imp bnd ty <>

45 pprintPTerm imp bnd ty <>

44− showDoc (maybe "" id d) <> line

46+ showDoc (maybe emptyDocstring id d) <> line

45 :

47 :

46 showArgs args ((n, False):bnd)

48 showArgs args ((n, False):bnd)

47 showArgs ((n, ty, Constraint {}, d):args) bnd

49 showArgs ((n, ty, Constraint {}, d):args) bnd

48 = text "Class constraint" <+>

50 = text "Class constraint" <+>

49− pprintPTerm imp bnd ty <> showDoc (maybe "" id d) <> line

51+ pprintPTerm imp bnd ty <> showDoc (maybe emptyDocstring id d) <> line

50 :

52 :

51 showArgs args ((n, True):bnd)

53 showArgs args ((n, True):bnd)

52 showArgs ((n, ty, Imp {}, d):args) bnd

54 showArgs ((n, ty, Imp {}, d):args) bnd

53− | not (null doc)

55+ | Just d' <- d

54 = text "(implicit)" <+>

56 = text "(implicit)" <+>

55 bindingOf n True <+> colon <+>

57 bindingOf n True <+> colon <+>

56 pprintPTerm imp bnd ty <>

58 pprintPTerm imp bnd ty <>

57− showDoc (maybe "" id d) <> line

59+ showDoc d' <> line

58 :

60 :

59 showArgs args ((n, True):bnd)

61 showArgs args ((n, True):bnd)

60 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)

62 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)

@@ -93,7 +95,7 @@ docClass n ci

93 = do i <- getIState

95 = do i <- getIState

94 let docstr = case lookupCtxt n (idris_docstrings i) of

96 let docstr = case lookupCtxt n (idris_docstrings i) of

95 [str] -> fst str

97 [str] -> fst str

96− _ -> ""

98+ _ -> emptyDocstring

97 mdocs <- mapM docFun (map fst (class_methods ci))

99 mdocs <- mapM docFun (map fst (class_methods ci))

98 return (ClassDoc n docstr mdocs)

100 return (ClassDoc n docstr mdocs)

101

@@ -102,7 +104,7 @@ docFun n

102 = do i <- getIState

104 = do i <- getIState

103 let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of

105 let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of

104 [d] -> d

106 [d] -> d

105− _ -> ("", [])

107+ _ -> noDocs

106 let ty = delabTy i n

108 let ty = delabTy i n

107 let args = getPArgNames ty argDocs

109 let args = getPArgNames ty argDocs

108 let infixes = idris_infixes i

110 let infixes = idris_infixes i

@@ -116,7 +118,7 @@ docFun n

116 funName (UN n) = str n

118 funName (UN n) = str n

117 funName (NS n _) = funName n

119 funName (NS n _) = funName n

118

120

119−getPArgNames :: PTerm -> [(Name, String)] -> [(Name, PTerm, Plicity, Maybe String)]

121+getPArgNames :: PTerm -> [(Name, Docstring)] -> [(Name, PTerm, Plicity, Maybe Docstring)]

120getPArgNames (PPi plicity name ty body) ds =

122getPArgNames (PPi plicity name ty body) ds =

121 (name, ty, plicity, lookup name ds) : getPArgNames body ds

123 (name, ty, plicity, lookup name ds) : getPArgNames body ds

122getPArgNames _ _ = []

124getPArgNames _ _ = []

src/Idris/Docstrings.hsnew file+80

@@ -0,0 +1,80 @@

1+-- | Wrapper around Markdown library

2+module Idris.Docstrings (

3+ Docstring, parseDocstring, renderDocstring, emptyDocstring, nullDocstring, noDocs

4+ ) where

6+import qualified Cheapskate as C

7+import qualified Cheapskate.Types as CT

9+import Util.Pretty

10+

11+import Idris.Core.TT (OutputAnnotation, Name)

12+

13+import qualified Data.Text as T

14+import qualified Data.Foldable as F

15+import qualified Data.Sequence as S

16+

17+type Docstring = CT.Doc

18+

19+parseDocstring :: T.Text -> CT.Doc

20+parseDocstring = C.markdown options

21+

22+

23+options = CT.Options { CT.sanitize = True

24+ , CT.allowRawHtml = False

25+ , CT.preserveHardBreaks = True

26+ , CT.debug = False

27+ }

28+

29+renderDocstring :: Docstring -> Doc OutputAnnotation

30+renderDocstring (CT.Doc _ blocks) = renderBlocks blocks

31+

32+renderBlocks :: CT.Blocks -> Doc OutputAnnotation

33+renderBlocks blocks | S.length blocks > 1 = F.foldr1 (\b1 b2 -> b1 <> line <> line <> b2) $

34+ fmap renderBlock blocks

35+ | S.length blocks == 1 = renderBlock (S.index blocks 0)

36+ | otherwise = empty

37+

38+renderBlock :: CT.Block -> Doc OutputAnnotation

39+renderBlock (CT.Para inlines) = renderInlines inlines

40+renderBlock (CT.Header lvl inlines) = renderInlines inlines <+> parens (text (show lvl))

41+renderBlock (CT.Blockquote blocks) = indent 8 $ renderBlocks blocks

42+renderBlock (CT.List b ty blockss) = renderList b ty blockss

43+renderBlock (CT.CodeBlock attr src) = indent 8 $ text (T.unpack src)

44+renderBlock (CT.HtmlBlock txt) = text "<html block>" -- TODO

45+renderBlock CT.HRule = text "----------------------"

46+

47+renderList :: Bool -> CT.ListType -> [CT.Blocks] -> Doc OutputAnnotation

48+renderList b (CT.Bullet c) blockss = vsep $ map (hang 4 . (char c <+>) . renderBlocks) blockss

49+renderList b (CT.Numbered nw i) blockss =

50+ vsep $

51+ zipWith3 (\n p txt -> hang 4 $ text (show n) <> p <+> txt)

52+ [i..] (repeat punc) (map renderBlocks blockss)

53+ where punc = case nw of

54+ CT.PeriodFollowing -> char '.'

55+ CT.ParenFollowing -> char '('

56+

57+renderInlines :: CT.Inlines -> Doc OutputAnnotation

58+renderInlines = F.foldr (<>) empty . fmap renderInline

59+

60+renderInline :: CT.Inline -> Doc OutputAnnotation

61+renderInline (CT.Str s) = text $ T.unpack s

62+renderInline CT.Space = space

63+renderInline CT.SoftBreak = softline

64+renderInline CT.LineBreak = line

65+renderInline (CT.Emph txt) = renderInlines txt -- TODO

66+renderInline (CT.Strong txt) = renderInlines txt -- TODO

67+renderInline (CT.Code txt) = text $ T.unpack txt

68+renderInline (CT.Link body url title) = renderInlines body <+> parens (text $ T.unpack url)

69+renderInline (CT.Image body url title) = text "<image>" -- TODO

70+renderInline (CT.Entity a) = text $ "<entity " ++ T.unpack a ++ ">" -- TODO

71+renderInline (CT.RawHtml txt) = text "<html content>" --TODO

72+

73+emptyDocstring :: Docstring

74+emptyDocstring = CT.Doc options S.empty

75+

76+nullDocstring :: Docstring -> Bool

77+nullDocstring (CT.Doc _ blocks) = S.null blocks

78+

79+noDocs :: (Docstring, [(Name, Docstring)])

80+noDocs = (emptyDocstring, [])

src/Idris/ElabDecls.hs+30−27

@@ -26,6 +26,8 @@ import Idris.Core.Execute

26import Idris.Core.Typecheck

27import Idris.Core.CaseTree

29+import Idris.Docstrings

30+

29import Control.DeepSeq

31import Control.DeepSeq

30import Control.Monad

32import Control.Monad

31import Control.Monad.State.Strict as State

33import Control.Monad.State.Strict as State

@@ -63,12 +65,12 @@ checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

63-- return (n, (i, top, t'))) ns

65-- return (n, (i, top, t'))) ns

65-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

67-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

66−elabType :: ElabInfo -> SyntaxInfo -> String -> [(Name, String)] ->

68+elabType :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->

67 FC -> FnOpts -> Name -> PTerm -> Idris Type

69 FC -> FnOpts -> Name -> PTerm -> Idris Type

68elabType = elabType' False

70elabType = elabType' False

70elabType' :: Bool -> -- normalise it

72elabType' :: Bool -> -- normalise it

71− ElabInfo -> SyntaxInfo -> String -> [(Name, String)] ->

73+ ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->

72 FC -> FnOpts -> Name -> PTerm -> Idris Type

74 FC -> FnOpts -> Name -> PTerm -> Idris Type

73elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

75elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

74 n = liftname info n_in in -}

76 n = liftname info n_in in -}

@@ -171,7 +173,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

171 tyIsHandler _ = False

173 tyIsHandler _ = False

172

174

173

175

174−elabPostulate :: ElabInfo -> SyntaxInfo -> String ->

176+elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->

175 FC -> FnOpts -> Name -> PTerm -> Idris ()

177 FC -> FnOpts -> Name -> PTerm -> Idris ()

176elabPostulate info syn doc fc opts n ty

178elabPostulate info syn doc fc opts n ty

177 = do elabType info syn doc [] fc opts n ty

179 = do elabType info syn doc [] fc opts n ty

@@ -195,7 +197,7 @@ elabPostulate info syn doc fc opts n ty

195 -- remove it from the deferred definitions list

197 -- remove it from the deferred definitions list

196 solveDeferred n

198 solveDeferred n

197

199

198−elabData :: ElabInfo -> SyntaxInfo -> String -> [(Name, String)] -> FC -> DataOpts -> PData -> Idris ()

200+elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()

199elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

201elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

200 = do let codata = Codata `elem` opts

202 = do let codata = Codata `elem` opts

201 iLOG (show (fc, doc))

203 iLOG (show (fc, doc))

@@ -257,8 +259,9 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

257 updateContext (addDatatype (Data n ttag cty cons))

259 updateContext (addDatatype (Data n ttag cty cons))

258 updateContext (setMetaInformation n metainf)

260 updateContext (setMetaInformation n metainf)

259 mapM_ (checkPositive n) cons

261 mapM_ (checkPositive n) cons

262+ if DefaultEliminator `elem` opts

260− if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty

263+ then evalStateT (elabEliminator params n t dcons info) Map.empty

261− else return ()

264+ else return ()

262 where

265 where

263 checkDefinedAs fc n t ctxt

266 checkDefinedAs fc n t ctxt

264 = case lookupDef n ctxt of

267 = case lookupDef n ctxt of

@@ -322,7 +325,7 @@ type EliminatorState = StateT (Map.Map String Int) Idris

322

325

323-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite

326-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite

324elabEliminator :: [Int] -> Name -> PTerm ->

327elabEliminator :: [Int] -> Name -> PTerm ->

325− [(String, [(Name, String)], Name, PTerm, FC, [Name])] ->

328+ [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->

326 ElabInfo -> EliminatorState ()

329 ElabInfo -> EliminatorState ()

327elabEliminator paramPos n ty cons info = do

330elabEliminator paramPos n ty cons info = do

328 elimLog $ "Elaborating eliminator"

331 elimLog $ "Elaborating eliminator"

@@ -339,7 +342,7 @@ elabEliminator paramPos n ty cons info = do

339 let motiveConstr = [(motiveName, expl, motive)]

342 let motiveConstr = [(motiveName, expl, motive)]

340 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

343 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

341 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))

344 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))

342− let eliminatorTyDecl = PTy (show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy

345+ let eliminatorTyDecl = PTy (parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy

343 let clauseConsElimArgs = map getPiName consTerms

346 let clauseConsElimArgs = map getPiName consTerms

344 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

347 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

345 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

348 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

@@ -488,7 +491,7 @@ elabEliminator paramPos n ty cons info = do

488 splitArgPms _ = ([],[])

491 splitArgPms _ = ([],[])

489

492

490

493

491− implicitIndexes :: (String, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]

494+ implicitIndexes :: (Docstring, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]

492 implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do

495 implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do

493 i <- State.lift getIState

496 i <- State.lift getIState

494 implargs' <- case lookupCtxt cnm (idris_implicits i) of

497 implargs' <- case lookupCtxt cnm (idris_implicits i) of

@@ -503,7 +506,7 @@ elabEliminator paramPos n ty cons info = do

503 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs

506 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs

504 _ -> return implargs

507 _ -> return implargs

505

508

506− extractConsTerm :: (String, [(Name, String)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

509+ extractConsTerm :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

507 extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do

510 extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do

508 let cons' = replaceParams paramPos generalParameters ty

511 let cons' = replaceParams paramPos generalParameters ty

509 let (args, resTy) = splitPi cons'

512 let (args, resTy) = splitPi cons'

@@ -539,7 +542,7 @@ elabEliminator paramPos n ty cons info = do

539 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)

542 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)

540 convertImplPi _ = Nothing

543 convertImplPi _ = Nothing

541

544

542− generateEliminatorClauses :: (String, [(Name, String)], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

545+ generateEliminatorClauses :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

543 generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do

546 generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do

544 let cons' = replaceParams paramPos generalParameters ty

547 let cons' = replaceParams paramPos generalParameters ty

545 let (args, resTy) = splitPi cons'

548 let (args, resTy) = splitPi cons'

@@ -561,7 +564,7 @@ elabEliminator paramPos n ty cons info = do

561

564

562elabPrims :: Idris ()

565elabPrims :: Idris ()

563elabPrims = do mapM_ (elabDecl EAll toplevel)

566elabPrims = do mapM_ (elabDecl EAll toplevel)

564− (map (\(opt, decl) -> PData "" [] defaultSyntax (fileFC "builtin") opt decl)

567+ (map (\(opt, decl) -> PData emptyDocstring [] defaultSyntax (fileFC "builtin") opt decl)

565 (zip

568 (zip

566 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]

569 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]

567 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

570 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

@@ -665,7 +668,7 @@ elabProvider info syn fc what n ty tm

665 Provide tm

668 Provide tm

666 | what `elem` [ProvTerm, ProvAny] ->

669 | what `elem` [ProvTerm, ProvAny] ->

667 do -- Finally add a top-level definition of the provided term

670 do -- Finally add a top-level definition of the provided term

668− elabType info syn "" [] fc [] n ty

671+ elabType info syn emptyDocstring [] fc [] n ty

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

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

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

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

671 | otherwise ->

674 | otherwise ->

@@ -673,7 +676,7 @@ elabProvider info syn fc what n ty tm

673 Postulate

676 Postulate

674 | what `elem` [ProvPostulate, ProvAny] ->

677 | what `elem` [ProvPostulate, ProvAny] ->

675 do -- Add the postulate

678 do -- Add the postulate

676− elabPostulate info syn "Provided postulate" fc [] n ty

679+ elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n ty

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

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

678 | otherwise ->

681 | otherwise ->

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

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

@@ -724,8 +727,8 @@ elabTransform info fc safe lhs_in rhs_in

724 addIBC (IBCTrans (clhs_tm, crhs_tm))

727 addIBC (IBCTrans (clhs_tm, crhs_tm))

725

728

726

729

727−elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

730+elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->

728− PTerm -> String -> Name -> PTerm -> Idris ()

731+ PTerm -> Docstring -> Name -> PTerm -> Idris ()

729elabRecord info syn doc fc tyn ty cdoc cn cty

732elabRecord info syn doc fc tyn ty cdoc cn cty

730 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])

733 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])

731 cty' <- implicit syn cn cty

734 cty' <- implicit syn cn cty

@@ -797,7 +800,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

797

800

798 mkProj recty substs cimp ((pn_in, pty), pos)

801 mkProj recty substs cimp ((pn_in, pty), pos)

799 = do let pn = expandNS syn pn_in

802 = do let pn = expandNS syn pn_in

800− let pfnTy = PTy "" [] defaultSyntax fc [] pn

803+ let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn

801 (PPi expl rec recty

804 (PPi expl rec recty

802 (substMatches substs pty))

805 (substMatches substs pty))

803 let pls = repeat Placeholder

806 let pls = repeat Placeholder

@@ -818,7 +821,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

818 let valname = sMN 0 "updateval"

821 let valname = sMN 0 "updateval"

819 let pt = k (PPi expl pn pty

822 let pt = k (PPi expl pn pty

820 (PPi expl rec recty recty))

823 (PPi expl rec recty recty))

821− let pfnTy = PTy "" [] defaultSyntax fc [] setname pt

824+ let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt

822 let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]

825 let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]

823 let lhsArgs = pls

826 let lhsArgs = pls

824 let rhsArgs = take pos pls ++ (PRef fc valname) :

827 let rhsArgs = take pos pls ++ (PRef fc valname) :

@@ -834,7 +837,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

834 return (pn, pfnTy, PClauses fc [] setname [pclause])

837 return (pn, pfnTy, PClauses fc [] setname [pclause])

835

838

836elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

839elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

837− (String, [(Name, String)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)

840+ (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)

838elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

841elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

839 = do checkUndefined fc n

842 = do checkUndefined fc n

840 ctxt <- getContext

843 ctxt <- getContext

@@ -1162,7 +1165,7 @@ elabPE info fc caller r =

1162 (map (\ (lhs, rhs) ->

1165 (map (\ (lhs, rhs) ->

1163 (showTmImpls lhs ++ " = " ++

1166 (showTmImpls lhs ++ " = " ++

1164 showTmImpls rhs)) pats)

1167 showTmImpls rhs)) pats)

1165− elabType info defaultSyntax "" [] fc opts newnm specTy

1168+ elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy

1166 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats

1169 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats

1167 elabClauses info fc opts newnm def

1170 elabClauses info fc opts newnm def

1168 logLvl 2 $ "Specialised " ++ show newnm)

1171 logLvl 2 $ "Specialised " ++ show newnm)

@@ -1721,7 +1724,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1721

1724

1722data MArgTy = IA | EA | CA deriving Show

1725data MArgTy = IA | EA | CA deriving Show

1723

1726

1724−elabClass :: ElabInfo -> SyntaxInfo -> String ->

1727+elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->

1725 FC -> [PTerm] ->

1728 FC -> [PTerm] ->

1726 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

1729 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

1727elabClass info syn doc fc constraints tn ps ds

1730elabClass info syn doc fc constraints tn ps ds

@@ -1748,7 +1751,7 @@ elabClass info syn doc fc constraints tn ps ds

1748 let cty = impbind ps $ conbind constraints

1751 let cty = impbind ps $ conbind constraints

1749 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

1752 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

1750 constraint

1753 constraint

1751− let cons = [("", [], cn, cty, fc, [])]

1754+ let cons = [(emptyDocstring, [], cn, cty, fc, [])]

1752 let ddecl = PDatadecl tn tty cons

1755 let ddecl = PDatadecl tn tty cons

1753 logLvl 5 $ "Class data " ++ show (showDImp True ddecl)

1756 logLvl 5 $ "Class data " ++ show (showDImp True ddecl)

1754 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc [] fc [] ddecl

1757 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc [] fc [] ddecl

@@ -1803,7 +1806,7 @@ elabClass info syn doc fc constraints tn ps ds

1803 case lookup n mtys of

1806 case lookup n mtys of

1804 Just (syn, o, ty) -> do let ty' = insertConstraint c ty

1807 Just (syn, o, ty) -> do let ty' = insertConstraint c ty

1805 let ds = map (decorateid defaultdec)

1808 let ds = map (decorateid defaultdec)

1806− [PTy "" [] syn fc [] n ty',

1809+ [PTy emptyDocstring [] syn fc [] n ty',

1807 PClauses fc (o ++ opts) n cs]

1810 PClauses fc (o ++ opts) n cs]

1808 iLOG (show ds)

1811 iLOG (show ds)

1809 return (n, ((defaultdec n, ds!!1), ds))

1812 return (n, ((defaultdec n, ds!!1), ds))

@@ -1841,7 +1844,7 @@ elabClass info syn doc fc constraints tn ps ds

1841 addInstance False conn' cfn

1844 addInstance False conn' cfn

1842 addIBC (IBCInstance False conn' cfn)

1845 addIBC (IBCInstance False conn' cfn)

1843-- iputStrLn ("Added " ++ show (conn, cfn, ty))

1846-- iputStrLn ("Added " ++ show (conn, cfn, ty))

1844− return [PTy "" [] syn fc [] cfn ty,

1847+ return [PTy emptyDocstring [] syn fc [] cfn ty,

1845 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

1848 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

1846

1849

1847 -- Generate a top level function which looks up a method in a given

1850 -- Generate a top level function which looks up a method in a given

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

1905 let constraint = PApp fc (PRef fc n) (map pexp ps)

1908 let constraint = PApp fc (PRef fc n) (map pexp ps)

1906 let iname = mkiname n ps expn

1909 let iname = mkiname n ps expn

1907 when (what /= EDefns) $ do

1910 when (what /= EDefns) $ do

1908− nty <- elabType' True info syn "" [] fc [] iname t

1911+ nty <- elabType' True info syn emptyDocstring [] fc [] iname t

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

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

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

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

1911 case expn of

1914 case expn of

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

2057 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

2060 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

2058 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

2061 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

2059

2062

2060− mkTyDecl (n, op, t, _) = PTy "" [] syn fc op n t

2063+ mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t

2061

2064

2062 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

2065 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

2063 conbind [] x = x

2066 conbind [] x = x

@@ -2304,7 +2307,7 @@ inferredDiff fc inf user =

2304-- | Check a PTerm against documentation and ensure that every documented

2307-- | Check a PTerm against documentation and ensure that every documented

2305-- argument actually exists. This must be run _after_ implicits have been

2308-- argument actually exists. This must be run _after_ implicits have been

2306-- found, or it will give spurious errors.

2309-- found, or it will give spurious errors.

2307−checkDocs :: FC -> [(Name, String)] -> PTerm -> Idris ()

2310+checkDocs :: FC -> [(Name, Docstring)] -> PTerm -> Idris ()

2308checkDocs fc args tm = cd (Map.fromList args) tm

2311checkDocs fc args tm = cd (Map.fromList args) tm

2309 where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc

2312 where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc

2310 cd as _ | Map.null as = return ()

2313 cd as _ | Map.null as = return ()

src/Idris/IBC.hs+86−3

@@ -9,6 +9,9 @@ import Idris.AbsSyntax

9import Idris.Imports

10import Idris.Error

11import Idris.Delaborate

12+import Idris.Docstrings

13+

14+import qualified Cheapskate.Types as CT

13import Data.Binary

16import Data.Binary

14import Data.Vector.Binary

17import Data.Vector.Binary

@@ -25,7 +28,7 @@ import Codec.Compression.Zlib (compress)

25import Util.Zlib (decompressEither)

28import Util.Zlib (decompressEither)

27ibcVersion :: Word8

30ibcVersion :: Word8

28−ibcVersion = 62

31+ibcVersion = 63

31data IBCFile = IBCFile { ver :: Word8,

34data IBCFile = IBCFile { ver :: Word8,

@@ -52,7 +55,7 @@ data IBCFile = IBCFile { ver :: Word8,

52 ibc_flags :: [(Name, [FnOpt])],

55 ibc_flags :: [(Name, [FnOpt])],

53 ibc_cg :: [(Name, CGInfo)],

56 ibc_cg :: [(Name, CGInfo)],

54 ibc_defs :: [(Name, Def)],

57 ibc_defs :: [(Name, Def)],

55− ibc_docstrings :: [(Name, (String, [(Name, String)]))],

58+ ibc_docstrings :: [(Name, (Docstring, [(Name, Docstring)]))],

56 ibc_transforms :: [(Term, Term)],

59 ibc_transforms :: [(Term, Term)],

57 ibc_errRev :: [(Term, Term)],

60 ibc_errRev :: [(Term, Term)],

58 ibc_coercions :: [Name],

61 ibc_coercions :: [Name],

@@ -405,7 +408,7 @@ pDefs syms ds

405 update (Proj t i) = Proj (update t) i

408 update (Proj t i) = Proj (update t) i

406 update t = t

409 update t = t

407

410

408−pDocs :: [(Name, (String, [(Name, String)]))] -> Idris ()

411+pDocs :: [(Name, (Docstring, [(Name, Docstring)]))] -> Idris ()

409pDocs ds = mapM_ (\ (n, a) -> addDocStr n (fst a) (snd a)) ds

412pDocs ds = mapM_ (\ (n, a) -> addDocStr n (fst a) (snd a)) ds

410

413

411pAccess :: [(Name, Accessibility)] -> Idris ()

414pAccess :: [(Name, Accessibility)] -> Idris ()

@@ -461,6 +464,86 @@ pMetavars ns = do i <- getIState

461 putIState $ i { idris_metavars = Data.List.reverse ns

464 putIState $ i { idris_metavars = Data.List.reverse ns

462 ++ idris_metavars i }

465 ++ idris_metavars i }

463

466

467+----- For Cheapskate

468+

469+instance Binary CT.Doc where

470+ put (CT.Doc opts lines) = do put opts ; put lines

471+ get = do opts <- get

472+ lines <- get

473+ return (CT.Doc opts lines)

474+

475+instance Binary CT.Options where

476+ put (CT.Options x1 x2 x3 x4) = do put x1 ; put x2 ; put x3 ; put x4

477+ get = do x1 <- get

478+ x2 <- get

479+ x3 <- get

480+ x4 <- get

481+ return (CT.Options x1 x2 x3 x4)

482+

483+instance Binary CT.Block where

484+ put (CT.Para lines) = do putWord8 0 ; put lines

485+ put (CT.Header i lines) = do putWord8 1 ; put i ; put lines

486+ put (CT.Blockquote bs) = do putWord8 2 ; put bs

487+ put (CT.List b t xs) = do putWord8 3 ; put b ; put t ; put xs

488+ put (CT.CodeBlock attr txt) = do putWord8 4 ; put attr ; put txt

489+ put (CT.HtmlBlock txt) = do putWord8 5 ; put txt

490+ put CT.HRule = putWord8 6

491+ get = do i <- getWord8

492+ case i of

493+ 0 -> fmap CT.Para get

494+ 1 -> liftM2 CT.Header get get

495+ 2 -> fmap CT.Blockquote get

496+ 3 -> liftM3 CT.List get get get

497+ 4 -> liftM2 CT.CodeBlock get get

498+ 5 -> liftM CT.HtmlBlock get

499+ 6 -> return CT.HRule

500+

501+instance Binary CT.Inline where

502+ put (CT.Str txt) = do putWord8 0 ; put txt

503+ put CT.Space = putWord8 1

504+ put CT.SoftBreak = putWord8 2

505+ put CT.LineBreak = putWord8 3

506+ put (CT.Emph xs) = putWord8 4 >> put xs

507+ put (CT.Strong xs) = putWord8 5 >> put xs

508+ put (CT.Code xs) = putWord8 6 >> put xs

509+ put (CT.Link a b c) = putWord8 7 >> put a >> put b >> put c

510+ put (CT.Image a b c) = putWord8 8 >> put a >> put b >> put c

511+ put (CT.Entity a) = putWord8 9 >> put a

512+ put (CT.RawHtml x) = putWord8 10 >> put x

513+ get = do i <- getWord8

514+ case i of

515+ 0 -> liftM CT.Str get

516+ 1 -> return CT.Space

517+ 2 -> return CT.SoftBreak

518+ 3 -> return CT.LineBreak

519+ 4 -> liftM CT.Emph get

520+ 5 -> liftM CT.Strong get

521+ 6 -> liftM CT.Code get

522+ 7 -> liftM3 CT.Link get get get

523+ 8 -> liftM3 CT.Image get get get

524+ 9 -> liftM CT.Entity get

525+ 10 -> liftM CT.RawHtml get

526+

527+instance Binary CT.ListType where

528+ put (CT.Bullet c) = putWord8 0 >> put c

529+ put (CT.Numbered nw i) = putWord8 1 >> put nw >> put i

530+ get = do i <- getWord8

531+ case i of

532+ 0 -> liftM CT.Bullet get

533+ 1 -> liftM2 CT.Numbered get get

534+

535+instance Binary CT.CodeAttr where

536+ put (CT.CodeAttr a b) = put a >> put b

537+ get = liftM2 CT.CodeAttr get get

538+

539+instance Binary CT.NumWrapper where

540+ put (CT.PeriodFollowing) = putWord8 0

541+ put (CT.ParenFollowing) = putWord8 1

542+ get = do i <- getWord8

543+ case i of

544+ 0 -> return CT.PeriodFollowing

545+ 1 -> return CT.ParenFollowing

546+

464----- Generated by 'derive'

547----- Generated by 'derive'

465

548

466instance Binary SizeChange where

549instance Binary SizeChange where

src/Idris/ParseData.hs+8−6

@@ -20,6 +20,8 @@ import Idris.DSL

20import Idris.Core.TT

21import Idris.Core.Evaluate

23+import Idris.Docstrings

24+

23import Control.Applicative

25import Control.Applicative

24import Control.Monad

26import Control.Monad

25import Control.Monad.State.Strict

27import Control.Monad.State.Strict

@@ -41,7 +43,7 @@ Record ::=

41-}

43-}

42record :: SyntaxInfo -> IdrisParser PDecl

44record :: SyntaxInfo -> IdrisParser PDecl

43record syn = do (doc, acc) <- try (do

45record syn = do (doc, acc) <- try (do

44− doc <- option ("", []) docComment

46+ doc <- option noDocs docComment

45 acc <- optional accessibility

47 acc <- optional accessibility

46 reserved "record"

48 reserved "record"

47 return (doc, acc))

49 return (doc, acc))

@@ -103,7 +105,7 @@ SimpleConstructorList ::=

103-}

105-}

104data_ :: SyntaxInfo -> IdrisParser PDecl

106data_ :: SyntaxInfo -> IdrisParser PDecl

105data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

107data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

106− (doc, argDocs) <- option ("", []) docComment

108+ (doc, argDocs) <- option noDocs docComment

107 pushIndent

109 pushIndent

108 acc <- optional accessibility

110 acc <- optional accessibility

109 elim <- dataOpts []

111 elim <- dataOpts []

@@ -160,9 +162,9 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

160{- | Parses a type constructor declaration

162{- | Parses a type constructor declaration

161 Constructor ::= DocComment? FnName TypeSig;

163 Constructor ::= DocComment? FnName TypeSig;

162-}

164-}

163−constructor :: SyntaxInfo -> IdrisParser (String, [(Name, String)], Name, PTerm, FC, [Name])

165+constructor :: SyntaxInfo -> IdrisParser (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])

164constructor syn

166constructor syn

165− = do (doc, argDocs) <- option ("", []) docComment

167+ = do (doc, argDocs) <- option noDocs docComment

166 cn_in <- fnName; fc <- getFC

168 cn_in <- fnName; fc <- getFC

167 let cn = expandNS syn cn_in

169 let cn = expandNS syn cn_in

168 lchar ':'

170 lchar ':'

@@ -177,9 +179,9 @@ constructor syn

177{- | Parses a constructor for simple discriminative union data types

179{- | Parses a constructor for simple discriminative union data types

178 SimpleConstructor ::= FnName SimpleExpr* DocComment?

180 SimpleConstructor ::= FnName SimpleExpr* DocComment?

179-}

181-}

180−simpleConstructor :: SyntaxInfo -> IdrisParser (String, [(Name, String)], Name, [PTerm], FC, [Name])

182+simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring, [(Name, Docstring)], Name, [PTerm], FC, [Name])

181simpleConstructor syn

183simpleConstructor syn

182− = do doc <- option ("", []) (try docComment)

184+ = do doc <- option noDocs (try docComment)

183 cn_in <- fnName

185 cn_in <- fnName

184 let cn = expandNS syn cn_in

186 let cn = expandNS syn cn_in

185 fc <- getFC

187 fc <- getFC

src/Idris/ParseHelpers.hs+10−8

@@ -16,6 +16,7 @@ import Idris.AbsSyntax

16import Idris.Core.TT

17import Idris.Core.Evaluate

18import Idris.Delaborate (pprintErr)

19+import Idris.Docstrings

20import qualified Util.Pretty as Pretty (text)

21import qualified Util.Pretty as Pretty (text)

@@ -139,25 +140,26 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())

139{-| Parses a documentation comment (similar to haddoc) given a marker character

140{-| Parses a documentation comment (similar to haddoc) given a marker character

140

141

141@

142@

142− DocComment_t ::= '--' DocCommentMarker_t ~EOL_t* EOL_t

143+ DocComment_t ::= '|||' ~EOL_t* EOL_t

143− | '{ -' DocCommentMarket_t ~'- }'* '- }'

144 ;

145@

146 -}

147−docComment :: IdrisParser (String, [(Name, String)])

147+docComment :: IdrisParser (Docstring, [(Name, Docstring)])

148docComment = do dc <- pushIndent *> docCommentLine

149 rest <- many (indented docCommentLine)

150 args <- many (indented argDocCommentLine)

151 popIndent

152− return (T.unpack $ T.strip $ T.pack (dc ++ concat rest), args)

152+ return (parseDocstring $ T.pack (concat . intersperse "\n" $ dc:rest),

153+ map (\(n, d) -> (n, parseDocstring (T.pack d))) args)

153

154

154 where docCommentLine :: MonadicParsing m => m String

155 where docCommentLine :: MonadicParsing m => m String

155 docCommentLine = try (do string "|||"

156 docCommentLine = try (do string "|||"

156− many (satisfy isSpace)

157+ many (satisfy (==' '))

157− first <- satisfy (\c -> not (isEol c || c == '@'))

158+ contents <- option "" (do first <- satisfy (\c -> not (isEol c || c == '@'))

158− res <- many (satisfy (not . isEol))

159+ res <- many (satisfy (not . isEol))

160+ return $ first:res)

159 eol ; someSpace

161 eol ; someSpace

160− return (first:res))-- ++ concat rest))

162+ return contents)-- ++ concat rest))

161 <?> ""

163 <?> ""

162 argDocCommentLine = do string "|||"

164 argDocCommentLine = do string "|||"

163 many (satisfy isSpace)

165 many (satisfy isSpace)

src/Idris/ParseOps.hs−1

@@ -59,7 +59,6 @@ binary name f = Infix (do fc <- getFC

59 indentPropHolds gtProp

60 reservedOp name

61 indentPropHolds gtProp

62− doc <- option ("", []) docComment

63 return (f fc))

62 return (f fc))

65-- | Prefix operator

64-- | Prefix operator

src/Idris/Parser.hs+7−5

@@ -35,6 +35,8 @@ import Idris.ParseOps

35import Idris.ParseExpr

36import Idris.ParseData

38+import Idris.Docstrings

39+

38import Paths_idris

40import Paths_idris

40import Util.DynamicLinker

42import Util.DynamicLinker

@@ -315,7 +317,7 @@ fnDecl' syn = checkFixity $

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

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

316 pushIndent

318 pushIndent

317 ist <- get

319 ist <- get

318− doc <- option ("", []) docComment

320+ doc <- option noDocs docComment

319 ist <- get

321 ist <- get

320 let initOpts = if default_total ist

322 let initOpts = if default_total ist

321 then [TotalFn]

323 then [TotalFn]

@@ -413,7 +415,7 @@ Postulate ::=

413@

415@

414-}

416-}

415postulate :: SyntaxInfo -> IdrisParser PDecl

417postulate :: SyntaxInfo -> IdrisParser PDecl

416−postulate syn = do doc <- try $ do doc <- option ("", []) docComment

418+postulate syn = do doc <- try $ do doc <- option noDocs docComment

417 pushIndent

419 pushIndent

418 reserved "postulate"

420 reserved "postulate"

419 return doc

421 return doc

@@ -561,7 +563,7 @@ Class ::=

561-}

563-}

562class_ :: SyntaxInfo -> IdrisParser [PDecl]

564class_ :: SyntaxInfo -> IdrisParser [PDecl]

563class_ syn = do (doc, acc) <- try (do

565class_ syn = do (doc, acc) <- try (do

564− doc <- option ("", []) docComment

566+ doc <- option noDocs docComment

565 acc <- optional accessibility

567 acc <- optional accessibility

566 return (doc, acc))

568 return (doc, acc))

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

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

@@ -1003,8 +1005,8 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st

1003 mapM_ (addNameHint ty') ns

1005 mapM_ (addNameHint ty') ns

1004 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]

1006 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]

1005 <|> do try (lchar '%' *> reserved "error_handlers")

1007 <|> do try (lchar '%' *> reserved "error_handlers")

1006− fn <- iName []

1008+ fn <- fnName

1007− arg <- iName []

1009+ arg <- fnName

1008 ns <- sepBy1 name (lchar ',')

1010 ns <- sepBy1 name (lchar ',')

1009 return [PDirective (do fn' <- disambiguate fn

1011 return [PDirective (do fn' <- disambiguate fn

1010 ns' <- mapM disambiguate ns

1012 ns' <- mapM disambiguate ns