1e13fbe · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1567 from david-christiansen/feature/doc-code-snippets

1e13fbeDavid Christiansen12 years ago

CHANGELOG+1

compare with master

unifiedsplit

@@ -21,6 +21,7 @@ New in 0.9.15:

21* New REPL command :printdef displays the internal definition of a name

22* New REPL command :pprint pretty-prints a definition or term with LaTeX or HTML highlighting

23* Naming of data and type constructors is made consistent across the standard library (see #1516)

24+* Terms in `code blocks` inside of documentation strings are now parsed and type checked. If this succeeds, they are rendered in full color in documentation lookups, and with semantic highlighting for IDEs.

25New in 0.9.14:

26New in 0.9.14:

26--------------

27--------------

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

@@ -21,7 +21,7 @@ boolElim False t e = e

21||| if you need to perform a Boolean test and convince the type checker of this

22||| fact.

23|||

24−||| If you find yourself using `so` for something other than primitive types,

24+||| If you find yourself using `So` for something other than primitive types,

25||| it may be appropriate to define a type of evidence for the property that you

26||| care about instead.

27data So : Bool -> Type where

src/Idris/AbsSyntax.hs+1−1

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

279addCoercion n = do i <- getIState

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

281

282−addDocStr :: Name -> Docstring -> [(Name, Docstring)] -> Idris ()

282+addDocStr :: Name -> Docstring (Maybe Term) -> [(Name, Docstring (Maybe Term))] -> Idris ()

283addDocStr n doc args

284 = do i <- getIState

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

src/Idris/AbsSyntaxTree.hs+16−20

@@ -158,7 +158,7 @@ data IState = IState {

158 idris_flags :: Ctxt [FnOpt],

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

160 idris_calledgraph :: Ctxt [Name],

161− idris_docstrings :: Ctxt (Docstring, [(Name, Docstring)]),

161+ idris_docstrings :: Ctxt (Docstring (Maybe Term), [(Name, Docstring (Maybe Term))]),

162 idris_tyinfodata :: Ctxt TIData,

163 idris_fninfo :: Ctxt FnInfo,

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

@@ -535,19 +535,19 @@ type ProvideWhat = ProvideWhat' PTerm

535-- datatypes and typeclasses.

536data PDecl' t

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

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

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

539− | PPostulate Docstring SyntaxInfo FC FnOpts Name t -- ^ Postulate

539+ | PPostulate (Docstring (Maybe PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate

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

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

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

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

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

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

545− | PRecord Docstring SyntaxInfo FC Name t DataOpts Docstring Name t -- ^ Record declaration

545+ | PRecord (Docstring (Maybe PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Maybe PTerm)) Name t -- ^ Record declaration

546− | PClass Docstring SyntaxInfo FC

546+ | PClass (Docstring (Maybe PTerm)) SyntaxInfo FC

547 [t] -- constraints

548 Name

549 [(Name, t)] -- parameters

550− [(Name, Docstring)] -- parameter docstrings

550+ [(Name, Docstring (Maybe PTerm))] -- parameter docstrings

551 [PDecl' t] -- declarations

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

553 -- class name, parameters, method declarations

@@ -598,7 +598,7 @@ deriving instance NFData PClause'

598-- | Data declaration

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

600 d_tcon :: t, -- ^ Type constructor

601− d_cons :: [(Docstring, [(Name, Docstring)], Name, t, FC, [Name])] -- ^ Constructors

601+ d_cons :: [(Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, t, FC, [Name])] -- ^ Constructors

602 }

603 -- ^ Data declaration

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

@@ -1071,7 +1071,8 @@ primNames = [falseTy, eqTy, eqCon, inferTy, inferCon]

1071unitTy = sUN "Unit"

1072unitCon = sUN "MkUnit"

1073

1074+-- TODO: elaborate the code samples in the docstring

1074−falseDoc = parseDocstring . T.pack $

1075+falseDoc = fmap (const Nothing) . parseDocstring . T.pack $

1075 "The empty type, also known as the trivially false proposition." ++

1076 "The empty type, also known as the trivially false proposition." ++

1076 "\n\n" ++

1077 "\n\n" ++

1077 "Use `FalseElim` or `absurd` to prove anything if you have a variable " ++

1078 "Use `FalseElim` or `absurd` to prove anything if you have a variable " ++

@@ -1085,7 +1086,7 @@ pairCon = sUN "MkPair"

1085

1086

1086eqTy = sUN "="

1087eqTy = sUN "="

1087eqCon = sUN "Refl"

1088eqCon = sUN "Refl"

1088−eqDoc = parseDocstring . T.pack $

1089+eqDoc = fmap (const Nothing) . parseDocstring . T.pack $

1089 "The propositional equality type. A proof that `x` = `y`." ++

1090 "The propositional equality type. A proof that `x` = `y`." ++

1090 "\n\n" ++

1091 "\n\n" ++

1091 "To use such a proof, pattern-match on it, and the two equal things will " ++

1092 "To use such a proof, pattern-match on it, and the two equal things will " ++

@@ -1108,14 +1109,14 @@ eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]

1108 pexp (PRef bi (n "x")),

1109 pexp (PRef bi (n "x")),

1109 pexp (PRef bi (n "x"))])), bi, [])]

1110 pexp (PRef bi (n "x"))])), bi, [])]

1110 where n a = sUN a

1111 where n a = sUN a

1111− reflDoc = parseDocstring . T.pack $

1112+ reflDoc = annotCode (const Nothing) . parseDocstring . T.pack $

1112 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++

1113 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++

1113 "shown that both sides are in fact equal."

1114 "shown that both sides are in fact equal."

1114− reflParamDoc = [(n "A", parseDocstring . T.pack $ "the type at which the equality is proven"),

1115+ reflParamDoc = [(n "A", annotCode (const Nothing) . parseDocstring . T.pack $ "the type at which the equality is proven"),

1115− (n "x", parseDocstring . T.pack $ "the element shown to be equal to itself.")]

1116+ (n "x", annotCode (const Nothing) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]

1116

1117

1117−eqParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left side of the equality"),

1118+eqParamDoc = [(n "A", annotCode (const Nothing) . parseDocstring . T.pack $ "the type of the left side of the equality"),

1118− (n "B", parseDocstring . T.pack $ "the type of the right side of the equality")

1119+ (n "B", annotCode (const Nothing) . parseDocstring . T.pack $ "the type of the right side of the equality")

1119 ]

1120 ]

1120 where n a = sUN a

1121 where n a = sUN a

1121

1122

@@ -1464,11 +1465,6 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1464 getFixity :: String -> Maybe Fixity

1465 getFixity :: String -> Maybe Fixity

1465 getFixity = flip M.lookup fixities

1466 getFixity = flip M.lookup fixities

1466

1467

1467−prettyDocumentedIst :: IState -> (Name, PTerm, Maybe Docstring) -> Doc OutputAnnotation

1468−prettyDocumentedIst ist (name, ty, docs) =

1469− prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>

1470− fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)

1471−

1472-- | Pretty-printer helper for the binding site of a name

1468-- | Pretty-printer helper for the binding site of a name

1473bindingOf :: Name -- ^^ the bound name

1469bindingOf :: Name -- ^^ the bound name

1474 -> Bool -- ^^ whether the name is implicit

1470 -> Bool -- ^^ whether the name is implicit

src/Idris/Apropos.hs+1−1

@@ -71,7 +71,7 @@ instance Apropos (TT Name) where

71instance Apropos Const where

72 isApropos str c = textIn str (T.pack (show c))

74−instance Apropos Docstring where

74+instance Apropos (Docstring a) where

75 isApropos str d = containsText str d

77instance (Apropos a, Apropos b) => Apropos (a, b) where

src/Idris/DeepSeq.hs+31−31

@@ -7,46 +7,46 @@ import Idris.AbsSyntaxTree

7import Control.DeepSeq

9import qualified Cheapskate.Types as CT

10+import qualified Idris.Docstrings as D

11−-- Manual from imported libs

12−instance NFData CT.Doc where

12+instance NFData a => NFData (D.Docstring a) where

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

13+ rnf (D.DocString opts contents) = rnf opts `seq` rnf contents `seq` ()

15instance NFData CT.Options where

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

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

17−

17+

18−instance NFData CT.Block where

18+instance NFData a => NFData (D.Block a) where

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

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

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

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

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

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

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

22+ rnf (D.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` ()

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

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

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

25− rnf CT.HRule = ()

25+ rnf D.HRule = ()

26−

26+

27−instance NFData CT.Inline where

27+instance NFData a => NFData (D.Inline a) where

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

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

29− rnf CT.Space = ()

29+ rnf D.Space = ()

30− rnf CT.SoftBreak = ()

30+ rnf D.SoftBreak = ()

31− rnf CT.LineBreak = ()

31+ rnf D.LineBreak = ()

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

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

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

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

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

34+ rnf (D.Code xs tm) = rnf xs `seq` rnf tm `seq` ()

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

35+ rnf (D.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` ()

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

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

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

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

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

40instance NFData CT.ListType where

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

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

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

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

44instance NFData CT.CodeAttr where

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

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

47instance NFData CT.NumWrapper where

48− rnf CT.PeriodFollowing = ()

48+ rnf CT.PeriodFollowing = ()

49− rnf CT.ParenFollowing = ()

49+ rnf CT.ParenFollowing = ()

51-- All generated by 'derive'

src/Idris/Delaborate.hs+2−1

@@ -428,7 +428,8 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

428 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

429 let o = overview (fst docs)

430 -- TODO make width configurable

431− out = displayS . renderPretty 1.0 50 $ renderDocstring o

431+ out = displayS . renderPretty 1.0 50 $

432+ renderDocstring (pprintDelab ist) o

432 return (out "")

433 return (out "")

433 getTy :: IState -> Name -> String -- fails if name not already extant!

434 getTy :: IState -> Name -> String -- fails if name not already extant!

434 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

435 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

src/Idris/Docs.hs+18−14

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

6import Idris.Delaborate

7import Idris.Core.TT

8import Idris.Core.Evaluate

9−import Idris.Docstrings

9+import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, renderDocstring)

11import Util.Pretty

@@ -16,8 +16,8 @@ import qualified Data.Text as T

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

19−data FunDoc = FD Name Docstring

19+data FunDoc = FD Name (Docstring (Maybe Term))

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

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

21 PTerm -- function type

22 (Maybe Fixity)

23 deriving Show

@@ -25,22 +25,22 @@ data FunDoc = FD Name Docstring

25data Docs = FunDoc FunDoc

26 | DataDoc FunDoc -- type constructor docs

27 [FunDoc] -- data constructor docs

28− | ClassDoc Name Docstring -- class docs

28+ | ClassDoc Name (Docstring (Maybe Term))-- class docs

29 [FunDoc] -- method docs

30− [(Name, Maybe Docstring)] -- parameters and their docstrings

30+ [(Name, Maybe (Docstring (Maybe Term)))] -- parameters and their docstrings

31 [PTerm] -- instances

32 [PTerm] -- superclasses

33 deriving Show

35−showDoc d | nullDocstring d = empty

35+showDoc ist d | nullDocstring d = empty

36− | otherwise = text " -- " <> renderDocstring d

36+ | otherwise = text " -- " <> renderDocstring (pprintDelab ist) d

38pprintFD :: IState -> FunDoc -> Doc OutputAnnotation

39pprintFD ist (FD n doc args ty f)

40 = nest 4 (prettyName True (ppopt_impl ppo) [] n <+> colon <+>

41 pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args

42 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>

43− renderDocstring doc <$>

43+ renderDocstring (pprintDelab ist) doc <$>

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

45 let argshow = showArgs args [] in

46 if not (null argshow)

@@ -52,19 +52,19 @@ pprintFD ist (FD n doc args ty f)

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

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

54 pprintPTerm ppo bnd [] infixes ty <>

55− showDoc d <> line

55+ showDoc ist d <> line

56 :

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

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

59 = text "Class constraint" <+>

60− pprintPTerm ppo bnd [] infixes ty <> showDoc d <> line

60+ pprintPTerm ppo bnd [] infixes ty <> showDoc ist d <> line

61 :

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

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

64 = text "(implicit)" <+>

65 bindingOf n True <+> colon <+>

66 pprintPTerm ppo bnd [] infixes ty <>

67− showDoc d <> line

67+ showDoc ist d <> line

68 :

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

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

@@ -80,7 +80,9 @@ pprintDocs ist (DataDoc t args)

80 vsep (map (pprintFD ist) args))

81pprintDocs ist (ClassDoc n doc meths params instances superclasses)

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

83+ if nullDocstring doc

84+ then empty

83− if nullDocstring doc then empty else line <> renderDocstring doc)

85+ else line <> renderDocstring (pprintDelab ist) doc)

84 <> line <$>

86 <> line <$>

85 nest 4 (text "Parameters:" <$> prettyParameters)

87 nest 4 (text "Parameters:" <$> prettyParameters)

86 <> line <$>

88 <> line <$>

@@ -131,7 +133,7 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

131 (subclasses, instances') = partition isSubclass instances

133 (subclasses, instances') = partition isSubclass instances

132

134

133 prettyParameters = if any (isJust . snd) params

135 prettyParameters = if any (isJust . snd) params

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

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

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

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

136

138

137getDocs :: Name -> Idris Docs

139getDocs :: Name -> Idris Docs

@@ -185,7 +187,7 @@ docFun n

185 funName n

187 funName n

186 | n == falseTy = "_|_"

188 | n == falseTy = "_|_"

187

189

188−getPArgNames :: PTerm -> [(Name, Docstring)] -> [(Name, PTerm, Plicity, Maybe Docstring)]

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

189getPArgNames (PPi plicity name ty body) ds =

191getPArgNames (PPi plicity name ty body) ds =

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

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

191getPArgNames _ _ = []

193getPArgNames _ _ = []

@@ -201,3 +203,5 @@ pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "ty

201 t (Str _) = PConstant StrType

203 t (Str _) = PConstant StrType

202 t (Ch c) = PConstant $ AType (ATInt ITChar)

204 t (Ch c) = PConstant $ AType (ATInt ITChar)

203 t _ = PType

205 t _ = PType

206+

207+

src/Idris/Docstrings.hs+199−74

@@ -1,26 +1,90 @@

1+{-# LANGUAGE DeriveFunctor, ScopedTypeVariables #-}

2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

1-- | Wrapper around Markdown library

4-- | Wrapper around Markdown library

2module Idris.Docstrings (

5module Idris.Docstrings (

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

6+ Docstring(..), Block(..), Inline(..), parseDocstring, renderDocstring, emptyDocstring, nullDocstring, noDocs,

4− overview, containsText

7+ overview, containsText, renderHtml, annotCode

5 ) where

8 ) where

7import qualified Cheapskate as C

10import qualified Cheapskate as C

8import qualified Cheapskate.Types as CT

11import qualified Cheapskate.Types as CT

12+import Cheapskate.Html (renderDoc)

10import Util.Pretty

14import Util.Pretty

12−import Idris.Core.TT (OutputAnnotation(..), TextFormatting(..), Name)

16+import Idris.Core.TT (OutputAnnotation(..), TextFormatting(..), Name, Term)

14import qualified Data.Text as T

18import qualified Data.Text as T

15import qualified Data.Foldable as F

19import qualified Data.Foldable as F

20+import Data.Foldable (Foldable)

21+import Data.Traversable (Traversable)

16import qualified Data.Sequence as S

22import qualified Data.Sequence as S

24+import Control.DeepSeq (NFData(..))

25+

26+import Text.Blaze.Html (Html)

27+

18−-- | Representation of Idris's inline documentation

28+-- | Representation of Idris's inline documentation. The type paramter

19−type Docstring = CT.Doc

29+-- represents the type of terms that are associated with code blocks.

30+data Docstring a = DocString CT.Options (Blocks a)

31+ deriving (Show, Functor, Foldable, Traversable)

32+

33+type Blocks a = S.Seq (Block a)

34+

35+-- | Block-level elements.

36+data Block a = Para (Inlines a)

37+ | Header Int (Inlines a)

38+ | Blockquote (Blocks a)

39+ | List Bool CT.ListType [Blocks a]

40+ | CodeBlock CT.CodeAttr T.Text a

41+ | HtmlBlock T.Text

42+ | HRule

43+ deriving (Show, Functor, Foldable, Traversable)

44+

45+data Inline a = Str T.Text

46+ | Space

47+ | SoftBreak

48+ | LineBreak

49+ | Emph (Inlines a)

50+ | Strong (Inlines a)

51+ | Code T.Text a

52+ | Link (Inlines a) T.Text T.Text

53+ | Image (Inlines a) T.Text T.Text

54+ | Entity T.Text

55+ | RawHtml T.Text

56+ deriving (Show, Functor, Foldable, Traversable)

57+

58+type Inlines a = S.Seq (Inline a)

59+

21-- | Construct a docstring from a Text that contains Markdown-formatted docs

61-- | Construct a docstring from a Text that contains Markdown-formatted docs

22−parseDocstring :: T.Text -> CT.Doc

62+parseDocstring :: T.Text -> Docstring ()

23−parseDocstring = C.markdown options

63+parseDocstring = toDocstring . C.markdown options

64+ where toDocstring :: CT.Doc -> Docstring ()

65+ toDocstring (CT.Doc opts blocks) = DocString opts (fmap toBlock blocks)

66+

67+ toBlock :: CT.Block -> Block ()

68+ toBlock (CT.Para inlines) = Para (fmap toInline inlines)

69+ toBlock (CT.Header i inlines) = Header i (fmap toInline inlines)

70+ toBlock (CT.Blockquote blocks) = Blockquote (fmap toBlock blocks)

71+ toBlock (CT.List b t blocks) = List b t (fmap (fmap toBlock) blocks)

72+ toBlock (CT.CodeBlock attrs text) = CodeBlock attrs text ()

73+ toBlock (CT.HtmlBlock src) = HtmlBlock src

74+ toBlock CT.HRule = HRule

75+

76+ toInline :: CT.Inline -> Inline ()

77+ toInline (CT.Str t) = Str t

78+ toInline CT.Space = Space

79+ toInline CT.SoftBreak = SoftBreak

80+ toInline CT.LineBreak = LineBreak

81+ toInline (CT.Emph is) = Emph (fmap toInline is)

82+ toInline (CT.Strong is) = Strong (fmap toInline is)

83+ toInline (CT.Code src) = Code src ()

84+ toInline (CT.Link is url title) = Link (fmap toInline is) url title

85+ toInline (CT.Image is url title) = Image (fmap toInline is) url title

86+ toInline (CT.Entity txt) = Entity txt

87+ toInline (CT.RawHtml src) = RawHtml src

26options = CT.Options { CT.sanitize = True

90options = CT.Options { CT.sanitize = True

@@ -30,90 +94,151 @@ options = CT.Options { CT.sanitize = True

30 }

94 }

32-- | Convert a docstring to be shown by the pretty-printer

96-- | Convert a docstring to be shown by the pretty-printer

33−renderDocstring :: Docstring -> Doc OutputAnnotation

97+renderDocstring :: (a -> Doc OutputAnnotation) -> Docstring (Maybe a) -> Doc OutputAnnotation

34−renderDocstring (CT.Doc _ blocks) = renderBlocks blocks

98+renderDocstring pp (DocString _ blocks) = renderBlocks pp blocks

36-- | Construct a docstring consisting of the first block-level element of the

100-- | Construct a docstring consisting of the first block-level element of the

37-- argument docstring, for use in summaries.

101-- argument docstring, for use in summaries.

38−overview :: Docstring -> Docstring

102+overview :: Docstring a -> Docstring a

39−overview (CT.Doc opts blocks) = CT.Doc opts (S.take 1 blocks)

103+overview (DocString opts blocks) = DocString opts (S.take 1 blocks)

40−

104+

41−renderBlocks :: CT.Blocks -> Doc OutputAnnotation

105+renderBlocks :: (a -> Doc OutputAnnotation) -> Blocks (Maybe a) -> Doc OutputAnnotation

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

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

43− fmap renderBlock blocks

107+ fmap (renderBlock pp) blocks

44− | S.length blocks == 1 = renderBlock (S.index blocks 0)

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

45− | otherwise = empty

109+ | otherwise = empty

46−

110+

47−renderBlock :: CT.Block -> Doc OutputAnnotation

111+renderBlock :: (a -> Doc OutputAnnotation) -> Block (Maybe a) -> Doc OutputAnnotation

48−renderBlock (CT.Para inlines) = renderInlines inlines

112+renderBlock pp (Para inlines) = renderInlines pp inlines

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

113+renderBlock pp (Header lvl inlines) = renderInlines pp inlines <+> parens (text (show lvl))

50−renderBlock (CT.Blockquote blocks) = indent 8 $ renderBlocks blocks

114+renderBlock pp (Blockquote blocks) = indent 8 $ renderBlocks pp blocks

51−renderBlock (CT.List b ty blockss) = renderList b ty blockss

115+renderBlock pp (List b ty blockss) = renderList pp b ty blockss

52−renderBlock (CT.CodeBlock attr src) = indent 8 $ text (T.unpack src)

116+renderBlock pp (CodeBlock attr src Nothing) = indent 8 $ text (T.unpack src)

117+renderBlock pp (CodeBlock attr src (Just tm)) = indent 8 $ pp tm

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

118+renderBlock pp (HtmlBlock txt) = text "<html block>" -- TODO

54−renderBlock CT.HRule = text "----------------------"

119+renderBlock pp HRule = text "----------------------"

55−

120+

56−renderList :: Bool -> CT.ListType -> [CT.Blocks] -> Doc OutputAnnotation

121+renderList :: (a -> Doc OutputAnnotation) -> Bool -> CT.ListType -> [Blocks (Maybe a)] -> Doc OutputAnnotation

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

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

58−renderList b (CT.Numbered nw i) blockss =

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

59 vsep $

124 vsep $

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

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

61− [i..] (repeat punc) (map renderBlocks blockss)

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

62 where punc = case nw of

127 where punc = case nw of

63 CT.PeriodFollowing -> char '.'

128 CT.PeriodFollowing -> char '.'

64 CT.ParenFollowing -> char '('

129 CT.ParenFollowing -> char '('

130

66−renderInlines :: CT.Inlines -> Doc OutputAnnotation

131+renderInlines :: (a -> Doc OutputAnnotation) -> Inlines (Maybe a) -> Doc OutputAnnotation

67−renderInlines = F.foldr (<>) empty . fmap renderInline

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

68−

133+

69−renderInline :: CT.Inline -> Doc OutputAnnotation

134+renderInline :: (a -> Doc OutputAnnotation) -> Inline (Maybe a) -> Doc OutputAnnotation

70−renderInline (CT.Str s) = text $ T.unpack s

135+renderInline pp (Str s) = text $ T.unpack s

71−renderInline CT.Space = softline

136+renderInline pp Space = softline

72−renderInline CT.SoftBreak = softline

137+renderInline pp SoftBreak = softline

73−renderInline CT.LineBreak = line

138+renderInline pp LineBreak = line

74−renderInline (CT.Emph txt) = annotate (AnnTextFmt ItalicText) $ renderInlines txt -- TODO

139+renderInline pp (Emph txt) = annotate (AnnTextFmt ItalicText) $ renderInlines pp txt

75−renderInline (CT.Strong txt) = annotate (AnnTextFmt BoldText) $ renderInlines txt -- TODO

140+renderInline pp (Strong txt) = annotate (AnnTextFmt BoldText) $ renderInlines pp txt

76−renderInline (CT.Code txt) = text $ T.unpack txt

141+renderInline pp (Code txt Nothing) = text $ T.unpack txt

142+renderInline pp (Code txt (Just tm)) = pp tm

77−renderInline (CT.Link body url title) = annotate (AnnTextFmt UnderlineText) (renderInlines body) <+>

143+renderInline pp (Link body url title) = annotate (AnnTextFmt UnderlineText) (renderInlines pp body) <+>

78 parens (text $ T.unpack url)

144 parens (text $ T.unpack url)

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

145+renderInline pp (Image body url title) = text "<image>" -- TODO

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

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

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

147+renderInline pp (RawHtml txt) = text "<html content>" --TODO

148

83-- | The empty docstring

149-- | The empty docstring

84−emptyDocstring :: Docstring

150+emptyDocstring :: Docstring a

85−emptyDocstring = CT.Doc options S.empty

151+emptyDocstring = DocString options S.empty

152

87-- | Check whether a docstring is emtpy

153-- | Check whether a docstring is emtpy

88−nullDocstring :: Docstring -> Bool

154+nullDocstring :: Docstring a -> Bool

89−nullDocstring (CT.Doc _ blocks) = S.null blocks

155+nullDocstring (DocString _ blocks) = S.null blocks

156

91-- | Empty documentation for a definition

157-- | Empty documentation for a definition

92−noDocs :: (Docstring, [(Name, Docstring)])

158+noDocs :: (Docstring a, [(Name, Docstring a)])

93noDocs = (emptyDocstring, [])

159noDocs = (emptyDocstring, [])

160

95-- | Does a string occur in the docstring?

161-- | Does a string occur in the docstring?

96−containsText :: T.Text -> Docstring -> Bool

162+containsText :: T.Text -> Docstring a -> Bool

97−containsText str (CT.Doc _ blocks) = F.any (blockContains (T.toLower str)) blocks

163+containsText str (DocString _ blocks) = F.any (blockContains (T.toLower str)) blocks

98 -- blockContains and inlineContains should always be called with a lower-case search string

164 -- blockContains and inlineContains should always be called with a lower-case search string

99− where blockContains :: T.Text -> CT.Block -> Bool

165+ where blockContains :: T.Text -> Block a -> Bool

100− blockContains str (CT.Para inlines) = F.any (inlineContains str) inlines

166+ blockContains str (Para inlines) = F.any (inlineContains str) inlines

101− blockContains str (CT.Header lvl inlines) = F.any (inlineContains str) inlines

167+ blockContains str (Header lvl inlines) = F.any (inlineContains str) inlines

102− blockContains str (CT.Blockquote blocks) = F.any (blockContains str) blocks

168+ blockContains str (Blockquote blocks) = F.any (blockContains str) blocks

103− blockContains str (CT.List b ty blockss) = F.any (F.any (blockContains str)) blockss

169+ blockContains str (List b ty blockss) = F.any (F.any (blockContains str)) blockss

104− blockContains str (CT.CodeBlock attr src) = T.isInfixOf str (T.toLower src)

170+ blockContains str (CodeBlock attr src _) = T.isInfixOf str (T.toLower src)

105− blockContains str (CT.HtmlBlock txt) = False -- TODO

171+ blockContains str (HtmlBlock txt) = False -- TODO

106− blockContains str CT.HRule = False

172+ blockContains str HRule = False

107−

173+

108− inlineContains :: T.Text -> CT.Inline -> Bool

174+ inlineContains :: T.Text -> Inline a -> Bool

109− inlineContains str (CT.Str s) = T.isInfixOf str (T.toLower s)

175+ inlineContains str (Str s) = T.isInfixOf str (T.toLower s)

110− inlineContains str CT.Space = False

176+ inlineContains str Space = False

111− inlineContains str CT.SoftBreak = False

177+ inlineContains str SoftBreak = False

112− inlineContains str CT.LineBreak = False

178+ inlineContains str LineBreak = False

113− inlineContains str (CT.Emph txt) = F.any (inlineContains str) txt

179+ inlineContains str (Emph txt) = F.any (inlineContains str) txt

114− inlineContains str (CT.Strong txt) = F.any (inlineContains str) txt

180+ inlineContains str (Strong txt) = F.any (inlineContains str) txt

115− inlineContains str (CT.Code txt) = T.isInfixOf str (T.toLower txt)

181+ inlineContains str (Code txt _) = T.isInfixOf str (T.toLower txt)

116− inlineContains str (CT.Link body url title) = F.any (inlineContains str) body

182+ inlineContains str (Link body url title) = F.any (inlineContains str) body

117− inlineContains str (CT.Image body url title) = False

183+ inlineContains str (Image body url title) = False

118− inlineContains str (CT.Entity a) = False

184+ inlineContains str (Entity a) = False

119− inlineContains str (CT.RawHtml txt) = T.isInfixOf str (T.toLower txt)

185+ inlineContains str (RawHtml txt) = T.isInfixOf str (T.toLower txt)

186+

187+

188+renderHtml :: Docstring (Maybe Term) -> Html

189+renderHtml = renderDoc . fromDocstring

190+ where

191+ fromDocstring :: Docstring (Maybe Term) -> CT.Doc

192+ fromDocstring (DocString opts blocks) = CT.Doc opts (fmap fromBlock blocks)

193+

194+ fromBlock :: Block (Maybe Term) -> CT.Block

195+ fromBlock (Para inlines) = CT.Para (fmap fromInline inlines)

196+ fromBlock (Header i inlines) = CT.Header i (fmap fromInline inlines)

197+ fromBlock (Blockquote blocks) = CT.Blockquote (fmap fromBlock blocks)

198+ fromBlock (List b t blocks) = CT.List b t (fmap (fmap fromBlock) blocks)

199+ fromBlock (CodeBlock attrs text _) = CT.CodeBlock attrs text

200+ fromBlock (HtmlBlock src) = CT.HtmlBlock src

201+ fromBlock HRule = CT.HRule

202+

203+ fromInline :: Inline (Maybe Term) -> CT.Inline

204+ fromInline (Str t) = CT.Str t

205+ fromInline Space = CT.Space

206+ fromInline SoftBreak = CT.SoftBreak

207+ fromInline LineBreak = CT.LineBreak

208+ fromInline (Emph is) = CT.Emph (fmap fromInline is)

209+ fromInline (Strong is) = CT.Strong (fmap fromInline is)

210+ fromInline (Code src _) = CT.Code src

211+ fromInline (Link is url title) = CT.Link (fmap fromInline is) url title

212+ fromInline (Image is url title) = CT.Image (fmap fromInline is) url title

213+ fromInline (Entity txt) = CT.Entity txt

214+ fromInline (RawHtml src) = CT.RawHtml src

215+

216+

217+-- | Annotate the code samples in a docstring

218+annotCode :: forall a b. (String -> b) -- ^ How to annotate code samples

219+ -> Docstring a

220+ -> Docstring b

221+annotCode annot (DocString opts blocks)

222+ = DocString opts $ fmap annotCodeBlock blocks

223+ where

224+ annotCodeBlock :: Block a -> Block b

225+ annotCodeBlock (Para inlines) = Para (fmap annotCodeInline inlines)

226+ annotCodeBlock (Header i inlines) = Header i (fmap annotCodeInline inlines)

227+ annotCodeBlock (Blockquote blocks) = Blockquote (fmap annotCodeBlock blocks)

228+ annotCodeBlock (List b t blocks) = List b t (fmap (fmap annotCodeBlock) blocks)

229+ annotCodeBlock (CodeBlock attrs src _) = CodeBlock attrs src (annot (T.unpack src))

230+ annotCodeBlock (HtmlBlock src) = HtmlBlock src

231+ annotCodeBlock HRule = HRule

232+

233+ annotCodeInline :: Inline a -> Inline b

234+ annotCodeInline (Str t) = Str t

235+ annotCodeInline Space = Space

236+ annotCodeInline SoftBreak = SoftBreak

237+ annotCodeInline LineBreak = LineBreak

238+ annotCodeInline (Emph is) = Emph (fmap annotCodeInline is)

239+ annotCodeInline (Strong is) = Strong (fmap annotCodeInline is)

240+ annotCodeInline (Code src _) = Code src (annot (T.unpack src))

241+ annotCodeInline (Link is url title) = Link (fmap annotCodeInline is) url title

242+ annotCodeInline (Image is url title) = Image (fmap annotCodeInline is) url title

243+ annotCodeInline (Entity txt) = Entity txt

244+ annotCodeInline (RawHtml src) = RawHtml src

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

@@ -52,9 +52,9 @@ import Util.Pretty(pretty, text)

53data MArgTy = IA | EA | CA deriving Show

55−elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->

55+elabClass :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm) ->

56 FC -> [PTerm] ->

57− Name -> [(Name, PTerm)] -> [(Name, Docstring)] -> [PDecl] -> Idris ()

57+ Name -> [(Name, PTerm)] -> [(Name, Docstring (Maybe PTerm))] -> [PDecl] -> Idris ()

58elabClass info syn_in doc fc constraints tn ps pDocs ds

59 = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

60 let tty = pibind ps PType

src/Idris/Elab/Data.hs+16−9

@@ -20,6 +20,7 @@ import IRTS.Lang

21import Idris.Elab.Type

22import Idris.Elab.Utils

23+import Idris.Elab.Value

24import Idris.Core.TT

25import Idris.Core.TT

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

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

@@ -49,7 +50,7 @@ import Data.List.Split (splitOn)

50import Util.Pretty(pretty, text)

51import Util.Pretty(pretty, text)

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

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

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

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

54 = do let codata = Codata `elem` opts

55 = do let codata = Codata `elem` opts

55 iLOG (show (fc, doc))

56 iLOG (show (fc, doc))

@@ -88,7 +89,10 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

88 addIBC (IBCDef n)

89 addIBC (IBCDef n)

89 addIBC (IBCData n)

90 addIBC (IBCData n)

90 checkDocs fc argDocs t

91 checkDocs fc argDocs t

92+ doc' <- elabDocTerms info doc

93+ argDocs' <- mapM (\(n, d) -> do d' <- elabDocTerms info d

94+ return (n, d')) argDocs

91− addDocStr n doc argDocs

95+ addDocStr n doc' argDocs'

92 addIBC (IBCDoc n)

96 addIBC (IBCDoc n)

93 let metainf = DataMI params

97 let metainf = DataMI params

94 addIBC (IBCMetaInformation n metainf)

98 addIBC (IBCMetaInformation n metainf)

@@ -207,7 +211,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

207-- forcenames is probably no longer needed

211-- forcenames is probably no longer needed

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

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

209 Type -> -- for kind checking

213 Type -> -- for kind checking

210− (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) ->

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

211 Idris (Name, Type)

215 Idris (Name, Type)

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

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

213 = do checkUndefined fc n

217 = do checkUndefined fc n

@@ -225,7 +229,10 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

225

229

226 addIBC (IBCDef n)

230 addIBC (IBCDef n)

227 checkDocs fc argDocs t

231 checkDocs fc argDocs t

232+ doc' <- elabDocTerms info doc

233+ argDocs' <- mapM (\(n, d) -> do d' <- elabDocTerms info d

234+ return (n, d')) argDocs

228− addDocStr n doc argDocs

235+ addDocStr n doc' argDocs'

229 addIBC (IBCDoc n)

236 addIBC (IBCDoc n)

230 fputState (opt_inaccessible . ist_optimisation n) inacc

237 fputState (opt_inaccessible . ist_optimisation n) inacc

231 addIBC (IBCOpt n)

238 addIBC (IBCOpt n)

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

274-- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function

281-- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function

275-- rename to caseFun to match updated intend

282-- rename to caseFun to match updated intend

276elabCaseFun :: Bool -> [Int] -> Name -> PTerm ->

283elabCaseFun :: Bool -> [Int] -> Name -> PTerm ->

277− [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->

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

278 ElabInfo -> EliminatorState ()

285 ElabInfo -> EliminatorState ()

279elabCaseFun ind paramPos n ty cons info = do

286elabCaseFun ind paramPos n ty cons info = do

280 elimLog $ "Elaborating case function"

287 elimLog $ "Elaborating case function"

@@ -293,7 +300,7 @@ elabCaseFun ind paramPos n ty cons info = do

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

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

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

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

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

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

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

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

297 let clauseConsElimArgs = map getPiName consTerms

304 let clauseConsElimArgs = map getPiName consTerms

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

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

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

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

@@ -443,7 +450,7 @@ elabCaseFun ind paramPos n ty cons info = do

443 splitArgPms _ = ([],[])

450 splitArgPms _ = ([],[])

444

451

445

452

446− implicitIndexes :: (Docstring, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]

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

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

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

448 i <- State.lift getIState

455 i <- State.lift getIState

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

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

@@ -458,7 +465,7 @@ elabCaseFun ind paramPos n ty cons info = do

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

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

459 _ -> return implargs

466 _ -> return implargs

460

467

461− extractConsTerm :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

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

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

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

463 let cons' = replaceParams paramPos generalParameters ty

470 let cons' = replaceParams paramPos generalParameters ty

464 let (args, resTy) = splitPi cons'

471 let (args, resTy) = splitPi cons'

@@ -494,7 +501,7 @@ elabCaseFun ind paramPos n ty cons info = do

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

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

495 convertImplPi _ = Nothing

502 convertImplPi _ = Nothing

496

503

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

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

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

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

499 let cons' = replaceParams paramPos generalParameters ty

506 let cons' = replaceParams paramPos generalParameters ty

500 let (args, resTy) = splitPi cons'

507 let (args, resTy) = splitPi cons'

src/Idris/Elab/Provider.hs+1−1

@@ -98,7 +98,7 @@ elabProvider info syn fc what n

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

99 | ProvPostulate _ <- what ->

100 do -- Add the postulate

101− elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)

101+ elabPostulate info syn (fmap (const Nothing) . parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)

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

103 | otherwise ->

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

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

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

51import Util.Pretty(pretty, text)

53−elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->

53+elabRecord :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm) -> FC -> Name ->

54− PTerm -> DataOpts -> Docstring -> Name -> PTerm -> Idris ()

54+ PTerm -> DataOpts -> Docstring (Maybe PTerm) -> Name -> PTerm -> Idris ()

55elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

56 = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty_in, fc, [])])

57 -- TODO think: something more in info?

src/Idris/Elab/Type.hs+15−6

@@ -1,5 +1,5 @@

1{-# LANGUAGE PatternGuards #-}

2−module Idris.Elab.Type(buildType, elabType, elabType', elabPostulate) where

2+module Idris.Elab.Type (buildType, elabType, elabType', elabPostulate) where

4import Idris.AbsSyntax

5import Idris.ASTUtils

@@ -19,6 +19,7 @@ import Idris.Output (iputStrLn, pshow, iWarn)

19import IRTS.Lang

21import Idris.Elab.Utils

22+import Idris.Elab.Value

23import Idris.Core.TT

24import Idris.Core.TT

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

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

@@ -27,7 +28,7 @@ import Idris.Core.Execute

27import Idris.Core.Typecheck

28import Idris.Core.Typecheck

28import Idris.Core.CaseTree

29import Idris.Core.CaseTree

30−import Idris.Docstrings

31+import Idris.Docstrings (Docstring)

32import Prelude hiding (id, (.))

33import Prelude hiding (id, (.))

33import Control.Category

34import Control.Category

@@ -40,6 +41,8 @@ import Data.List

40import Data.Maybe

41import Data.Maybe

41import Debug.Trace

42import Debug.Trace

44+import qualified Data.Traversable as Traversable

45+

43import qualified Data.Map as Map

46import qualified Data.Map as Map

44import qualified Data.Set as S

47import qualified Data.Set as S

45import qualified Data.Text as T

48import qualified Data.Text as T

@@ -111,12 +114,12 @@ buildType info syn fc opts n ty' = do

111 param_pos i ns t = []

114 param_pos i ns t = []

112

115

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

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

114−elabType :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->

117+elabType :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm)-> [(Name, Docstring (Maybe PTerm))] ->

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

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

116elabType = elabType' False

119elabType = elabType' False

117

120

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

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

119− ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->

122+ ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm) -> [(Name, Docstring (Maybe PTerm))] ->

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

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

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

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

122 n = liftname info n_in in -}

125 n = liftname info n_in in -}

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

152 addDeferred ds'

155 addDeferred ds'

153 setFlags n opts'

156 setFlags n opts'

154 checkDocs fc argDocs ty

157 checkDocs fc argDocs ty

158+ doc' <- elabDocTerms info doc

159+ argDocs' <- mapM (\(n, d) -> do d' <- elabDocTerms info d

160+ return (n, d')) argDocs

155− addDocStr n doc argDocs

161+ addDocStr n doc' argDocs'

156 addIBC (IBCDoc n)

162 addIBC (IBCDoc n)

157 addIBC (IBCFlags n opts')

163 addIBC (IBCFlags n opts')

158 fputState (opt_inaccessible . ist_optimisation n) inacc

164 fputState (opt_inaccessible . ist_optimisation n) inacc

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

200 , ns4 == map txt ["Reflection","Language"] = True

206 , ns4 == map txt ["Reflection","Language"] = True

201 tyIsHandler _ = False

207 tyIsHandler _ = False

202

208

203−elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->

209+elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm) ->

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

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

205elabPostulate info syn doc fc opts n ty = do

211elabPostulate info syn doc fc opts n ty = do

206 elabType info syn doc [] fc opts n ty

212 elabType info syn doc [] fc opts n ty

@@ -209,3 +215,6 @@ elabPostulate info syn doc fc opts n ty = do

209

215

210 -- remove it from the deferred definitions list

216 -- remove it from the deferred definitions list

211 solveDeferred n

217 solveDeferred n

218+

219+

220+

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

@@ -16,6 +16,7 @@ import Control.Applicative hiding (Const)

16import Control.Monad.State

17import Control.Monad

18import Data.List

19+import qualified Data.Traversable as Traversable

20import Debug.Trace

21import Debug.Trace

@@ -105,7 +106,7 @@ inferredDiff fc inf user =

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

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

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

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

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

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

108−checkDocs :: FC -> [(Name, Docstring)] -> PTerm -> Idris ()

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

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

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

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

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

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

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

@@ -235,4 +236,3 @@ getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

235 getUniqB env us b = getUniq env us (binderTy b)

236 getUniqB env us b = getUniq env us (binderTy b)

236

237

238

238−

src/Idris/Elab/Value.hs+11−1

@@ -1,5 +1,5 @@

1{-# LANGUAGE PatternGuards #-}

2−module Idris.Elab.Value(elabVal, elabValBind) where

2+module Idris.Elab.Value(elabVal, elabValBind, elabDocTerms) where

4import Idris.AbsSyntax

5import Idris.ASTUtils

@@ -38,6 +38,7 @@ import Control.Monad

38import Control.Monad.State.Strict as State

39import Data.List

40import Data.Maybe

41+import qualified Data.Traversable as Traversable

41import Debug.Trace

42import Debug.Trace

43import qualified Data.Map as Map

44import qualified Data.Map as Map

@@ -86,3 +87,12 @@ elabVal info aspat tm_in

86 return (tm, ty)

87 return (tm, ty)

90+

91+elabDocTerms :: ElabInfo -> Docstring (Maybe PTerm) -> Idris (Docstring (Maybe Term))

92+elabDocTerms info str = Traversable.mapM decorate str

93+ where decorate Nothing = return Nothing

94+ decorate (Just pt) = fmap (fmap fst) (tryElabVal info ERHS pt)

95+ tryElabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Maybe (Term, Type))

96+ tryElabVal info aspat tm_in

97+ = idrisCatch (fmap Just $ elabVal info aspat tm_in)

98+ (const $ return Nothing)

src/Idris/IBC.hs+48−47

@@ -10,7 +10,8 @@ import Idris.AbsSyntax

10import Idris.Imports

11import Idris.Error

12import Idris.Delaborate

13+import qualified Idris.Docstrings as D

13−import Idris.Docstrings

14+import Idris.Docstrings (Docstring)

14import Idris.Output

15import Idris.Output

16import qualified Cheapskate.Types as CT

17import qualified Cheapskate.Types as CT

@@ -31,7 +32,7 @@ import Codec.Compression.Zlib (compress)

31import Util.Zlib (decompressEither)

32import Util.Zlib (decompressEither)

33ibcVersion :: Word8

34ibcVersion :: Word8

34−ibcVersion = 80

35+ibcVersion = 81

36data IBCFile = IBCFile { ver :: Word8,

37data IBCFile = IBCFile { ver :: Word8,

37 sourcefile :: FilePath,

38 sourcefile :: FilePath,

@@ -60,7 +61,7 @@ data IBCFile = IBCFile { ver :: Word8,

60 ibc_fninfo :: [(Name, FnInfo)],

61 ibc_fninfo :: [(Name, FnInfo)],

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

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

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

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

63− ibc_docstrings :: [(Name, (Docstring, [(Name, Docstring)]))],

64+ ibc_docstrings :: [(Name, (Docstring (Maybe Term), [(Name, Docstring (Maybe Term))]))],

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

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

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

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

66 ibc_coercions :: [Name],

67 ibc_coercions :: [Name],

@@ -458,7 +459,7 @@ pDefs syms ds

458 update (Proj t i) = Proj (update t) i

459 update (Proj t i) = Proj (update t) i

459 update t = t

460 update t = t

460

461

461−pDocs :: [(Name, (Docstring, [(Name, Docstring)]))] -> Idris ()

462+pDocs :: [(Name, (Docstring (Maybe Term), [(Name, Docstring (Maybe Term))]))] -> Idris ()

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

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

463

464

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

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

@@ -521,13 +522,13 @@ pMetavars ns = do i <- getIState

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

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

522 ++ idris_metavars i }

523 ++ idris_metavars i }

523

524

524−----- For Cheapskate

525+----- For Cheapskate and docstrings

525

526

526−instance Binary CT.Doc where

527+instance Binary a => Binary (D.Docstring a) where

527− put (CT.Doc opts lines) = do put opts ; put lines

528+ put (D.DocString opts lines) = do put opts ; put lines

528 get = do opts <- get

529 get = do opts <- get

529 lines <- get

530 lines <- get

530− return (CT.Doc opts lines)

531+ return (D.DocString opts lines)

531

532

532instance Binary CT.Options where

533instance Binary CT.Options where

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

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

@@ -537,49 +538,49 @@ instance Binary CT.Options where

537 x4 <- get

538 x4 <- get

538 return (CT.Options x1 x2 x3 x4)

539 return (CT.Options x1 x2 x3 x4)

539

540

540−instance Binary CT.Block where

541+instance Binary a => Binary (D.Block a) where

541− put (CT.Para lines) = do putWord8 0 ; put lines

542+ put (D.Para lines) = do putWord8 0 ; put lines

542− put (CT.Header i lines) = do putWord8 1 ; put i ; put lines

543+ put (D.Header i lines) = do putWord8 1 ; put i ; put lines

543− put (CT.Blockquote bs) = do putWord8 2 ; put bs

544+ put (D.Blockquote bs) = do putWord8 2 ; put bs

544− put (CT.List b t xs) = do putWord8 3 ; put b ; put t ; put xs

545+ put (D.List b t xs) = do putWord8 3 ; put b ; put t ; put xs

545− put (CT.CodeBlock attr txt) = do putWord8 4 ; put attr ; put txt

546+ put (D.CodeBlock attr txt src) = do putWord8 4 ; put attr ; put txt ; put src

546− put (CT.HtmlBlock txt) = do putWord8 5 ; put txt

547+ put (D.HtmlBlock txt) = do putWord8 5 ; put txt

547− put CT.HRule = putWord8 6

548+ put D.HRule = putWord8 6

548 get = do i <- getWord8

549 get = do i <- getWord8

549 case i of

550 case i of

550− 0 -> fmap CT.Para get

551+ 0 -> fmap D.Para get

551− 1 -> liftM2 CT.Header get get

552+ 1 -> liftM2 D.Header get get

552− 2 -> fmap CT.Blockquote get

553+ 2 -> fmap D.Blockquote get

553− 3 -> liftM3 CT.List get get get

554+ 3 -> liftM3 D.List get get get

554− 4 -> liftM2 CT.CodeBlock get get

555+ 4 -> liftM3 D.CodeBlock get get get

555− 5 -> liftM CT.HtmlBlock get

556+ 5 -> liftM D.HtmlBlock get

556− 6 -> return CT.HRule

557+ 6 -> return D.HRule

557−

558+

558−instance Binary CT.Inline where

559+instance Binary a => Binary (D.Inline a) where

559− put (CT.Str txt) = do putWord8 0 ; put txt

560+ put (D.Str txt) = do putWord8 0 ; put txt

560− put CT.Space = putWord8 1

561+ put D.Space = putWord8 1

561− put CT.SoftBreak = putWord8 2

562+ put D.SoftBreak = putWord8 2

562− put CT.LineBreak = putWord8 3

563+ put D.LineBreak = putWord8 3

563− put (CT.Emph xs) = putWord8 4 >> put xs

564+ put (D.Emph xs) = putWord8 4 >> put xs

564− put (CT.Strong xs) = putWord8 5 >> put xs

565+ put (D.Strong xs) = putWord8 5 >> put xs

565− put (CT.Code xs) = putWord8 6 >> put xs

566+ put (D.Code xs tm) = putWord8 6 >> put xs >> put tm

566− put (CT.Link a b c) = putWord8 7 >> put a >> put b >> put c

567+ put (D.Link a b c) = putWord8 7 >> put a >> put b >> put c

567− put (CT.Image a b c) = putWord8 8 >> put a >> put b >> put c

568+ put (D.Image a b c) = putWord8 8 >> put a >> put b >> put c

568− put (CT.Entity a) = putWord8 9 >> put a

569+ put (D.Entity a) = putWord8 9 >> put a

569− put (CT.RawHtml x) = putWord8 10 >> put x

570+ put (D.RawHtml x) = putWord8 10 >> put x

570 get = do i <- getWord8

571 get = do i <- getWord8

571 case i of

572 case i of

572− 0 -> liftM CT.Str get

573+ 0 -> liftM D.Str get

573− 1 -> return CT.Space

574+ 1 -> return D.Space

574− 2 -> return CT.SoftBreak

575+ 2 -> return D.SoftBreak

575− 3 -> return CT.LineBreak

576+ 3 -> return D.LineBreak

576− 4 -> liftM CT.Emph get

577+ 4 -> liftM D.Emph get

577− 5 -> liftM CT.Strong get

578+ 5 -> liftM D.Strong get

578− 6 -> liftM CT.Code get

579+ 6 -> liftM2 D.Code get get

579− 7 -> liftM3 CT.Link get get get

580+ 7 -> liftM3 D.Link get get get

580− 8 -> liftM3 CT.Image get get get

581+ 8 -> liftM3 D.Image get get get

581− 9 -> liftM CT.Entity get

582+ 9 -> liftM D.Entity get

582− 10 -> liftM CT.RawHtml get

583+ 10 -> liftM D.RawHtml get

583

584

584instance Binary CT.ListType where

585instance Binary CT.ListType where

585 put (CT.Bullet c) = putWord8 0 >> put c

586 put (CT.Bullet c) = putWord8 0 >> put c

src/Idris/IdrisDoc.hs+7−7

@@ -13,6 +13,7 @@ import Idris.ParseHelpers (opChars)

13import Idris.AbsSyntax

14import Idris.Docs

15import Idris.Docstrings (nullDocstring)

16+import qualified Idris.Docstrings as Docstrings

17import IRTS.System (getDataFileName)

18import IRTS.System (getDataFileName)

@@ -37,7 +38,6 @@ import System.IO.Error

37import System.FilePath

38import System.FilePath

38import System.Directory

39import System.Directory

40−import Cheapskate.Html (renderDoc)

41import Text.PrettyPrint.Annotated.Leijen (displayDecorated, renderCompact)

43import Text.Blaze (toValue, contents)

@@ -496,7 +496,7 @@ genTypeHeader ist (FD n _ args ftype _) = do

496 docExtractor (_, _, _, Nothing) = Nothing

497 docExtractor (n, _, _, Just d) = Just (n, doc2Str d)

498 -- TODO: Remove <p> tags more robustly

499− doc2Str d = let dirty = renderMarkup $ contents $ renderDoc $ d

499+ doc2Str d = let dirty = renderMarkup $ contents $ Docstrings.renderHtml $ d

500 in take (length dirty - 8) $ drop 3 dirty

501

502 name (NS n ns) = show (NS (sUN $ name n) ns)

@@ -523,7 +523,7 @@ createFunDoc :: IState -- ^ Needed to determine the types of names

523createFunDoc ist fd@(FD name docstring args ftype fixity) = do

524 H.dt ! (A.id $ toValue $ show name) $ genTypeHeader ist fd

525 H.dd $ do

526− (if nullDocstring docstring then Empty else renderDoc docstring)

526+ (if nullDocstring docstring then Empty else Docstrings.renderHtml docstring)

527 let args' = filter (\(_, _, _, d) -> isJust d) args

528 if (not $ null args') || (isJust fixity)

529 then H.dl $ do

@@ -546,7 +546,7 @@ createFunDoc ist fd@(FD name docstring args ftype fixity) = do

546 genArg (_, _, _, Nothing) = Empty

547 genArg (name, _, _, Just docstring) = do

548 H.dt $ toHtml $ show name

549− H.dd $ renderDoc docstring

549+ H.dd $ Docstrings.renderHtml docstring

550

551

552-- | Generates HTML documentation for any Docs type

@@ -564,7 +564,7 @@ createOtherDoc ist (ClassDoc n docstring fds _ _ _) = do

564 $ toHtml $ name $ nsroot n

565 H.span ! class_ "signature" $ nbsp

566 H.dd $ do

567− (if nullDocstring docstring then Empty else renderDoc docstring)

567+ (if nullDocstring docstring then Empty else Docstrings.renderHtml docstring)

568 H.dl ! class_ "decls" $ forM_ fds (createFunDoc ist)

569

570 where name (NS n ns) = show (NS (sUN $ name n) ns)

@@ -578,7 +578,7 @@ createOtherDoc ist (DataDoc fd@(FD n docstring args _ _) fds) = do

578 H.span ! class_ "word" $ do "data"; nbsp

579 genTypeHeader ist fd

580 H.dd $ do

581− (if nullDocstring docstring then Empty else renderDoc docstring)

581+ (if nullDocstring docstring then Empty else Docstrings.renderHtml docstring)

582 let args' = filter (\(_, _, _, d) -> isJust d) args

583 if not $ null args'

584 then H.dl $ forM_ args' genArg

@@ -588,7 +588,7 @@ createOtherDoc ist (DataDoc fd@(FD n docstring args _ _) fds) = do

588 where genArg (_, _, _, Nothing) = Empty

589 genArg (name, _, _, Just docstring) = do

590 H.dt $ toHtml $ show name

591− H.dd $ renderDoc docstring

591+ H.dd $ Docstrings.renderHtml docstring

592

593

594-- | Generates everything but the actual content of the page

src/Idris/Output.hs+10

@@ -175,6 +175,16 @@ printUndefinedNames ns = text "Undefined " <> names <> text "."

175 where names = encloseSep empty empty (char ',') $ map ppName ns

176 ppName = prettyName True True []

177

178+

179+prettyDocumentedIst :: IState

180+ -> (Name, PTerm, Maybe (Docstring (Maybe Term)))

181+ -> Doc OutputAnnotation

182+prettyDocumentedIst ist (name, ty, docs) =

183+ prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>

184+ fromMaybe empty (fmap (\d -> renderDocstring ppTm d <> line) docs)

185+ where ppTm = pprintDelab ist

186+

187+

178renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String

188renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String

179renderExternal fmt width doc

189renderExternal fmt width doc

180 | width < 1 = throwError . Msg $ "There must be at least one column for the pretty-printer."

190 | width < 1 = throwError . Msg $ "There must be at least one column for the pretty-printer."

src/Idris/ParseData.hs+27−13

@@ -42,25 +42,29 @@ Record ::=

42 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;

43-}

44record :: SyntaxInfo -> IdrisParser PDecl

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

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

46− doc <- option noDocs docComment

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

47+ ist <- get

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

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

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

47 acc <- optional accessibility

51 acc <- optional accessibility

48 opts <- dataOpts []

52 opts <- dataOpts []

49 reserved "record"

53 reserved "record"

50− return (doc, acc, opts))

54+ return (doc', argDocs', acc, opts))

51 fc <- getFC

55 fc <- getFC

52 tyn_in <- fnName

56 tyn_in <- fnName

53 lchar ':'

57 lchar ':'

54 ty <- typeExpr (allowImp syn)

58 ty <- typeExpr (allowImp syn)

55 let tyn = expandNS syn tyn_in

59 let tyn = expandNS syn tyn_in

56 reserved "where"

60 reserved "where"

57− (cdoc, argDocs, cn, cty, _, _) <- indentedBlockS (constructor syn)

61+ (cdoc, cargDocs, cn, cty, _, _) <- indentedBlockS (constructor syn)

58 accData acc tyn [cn]

62 accData acc tyn [cn]

59 let rsyn = syn { syn_namespace = show (nsroot tyn) :

63 let rsyn = syn { syn_namespace = show (nsroot tyn) :

60 syn_namespace syn }

64 syn_namespace syn }

61 let fns = getRecNames rsyn cty

65 let fns = getRecNames rsyn cty

62 mapM_ (\n -> addAcc n acc) fns

66 mapM_ (\n -> addAcc n acc) fns

63− return $ PRecord (fst doc) rsyn fc tyn ty opts cdoc cn cty

67+ return $ PRecord doc rsyn fc tyn ty opts cdoc cn cty

64 <?> "record type declaration"

68 <?> "record type declaration"

65 where

69 where

66 getRecNames :: SyntaxInfo -> PTerm -> [Name]

70 getRecNames :: SyntaxInfo -> PTerm -> [Name]

@@ -112,8 +116,12 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

112 acc <- optional accessibility

116 acc <- optional accessibility

113 elim <- dataOpts []

117 elim <- dataOpts []

114 co <- dataI

118 co <- dataI

119+ ist <- get

115− let dataOpts = combineDataOpts(elim ++ co)

120+ let dataOpts = combineDataOpts (elim ++ co)

121+ doc' = annotCode (tryFullExpr syn ist) doc

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

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

116− return (doc, argDocs, acc, dataOpts))

124+ return (doc', argDocs', acc, dataOpts))

117 fc <- getFC

125 fc <- getFC

118 tyn_in <- fnName

126 tyn_in <- fnName

119 (do try (lchar ':')

127 (do try (lchar ':')

@@ -164,7 +172,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

164{- | Parses a type constructor declaration

172{- | Parses a type constructor declaration

165 Constructor ::= DocComment? FnName TypeSig;

173 Constructor ::= DocComment? FnName TypeSig;

166-}

174-}

167−constructor :: SyntaxInfo -> IdrisParser (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])

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

168constructor syn

176constructor syn

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

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

170 cn_in <- fnName; fc <- getFC

178 cn_in <- fnName; fc <- getFC

@@ -175,21 +183,27 @@ constructor syn

175 fs <- option [] (do lchar '%'; reserved "erase"

183 fs <- option [] (do lchar '%'; reserved "erase"

176 sepBy1 name (lchar ','))

184 sepBy1 name (lchar ','))

177 ty <- typeExpr (allowImp syn)

185 ty <- typeExpr (allowImp syn)

186+ ist <- get

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

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

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

178− return (doc, argDocs, cn, ty, fc, fs)

190+ return (doc', argDocs', cn, ty, fc, fs)

179 <?> "constructor"

191 <?> "constructor"

180

192

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

193+{- | Parses a constructor for simple discriminated union data types

182 SimpleConstructor ::= FnName SimpleExpr* DocComment?

194 SimpleConstructor ::= FnName SimpleExpr* DocComment?

183-}

195-}

184−simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring, [(Name, Docstring)], Name, [PTerm], FC, [Name])

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

185simpleConstructor syn

197simpleConstructor syn

186− = do doc <- option noDocs (try docComment)

198+ = do (doc, _) <- option noDocs (try docComment)

199+ ist <- get

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

187 cn_in <- fnName

201 cn_in <- fnName

188 let cn = expandNS syn cn_in

202 let cn = expandNS syn cn_in

189 fc <- getFC

203 fc <- getFC

190 args <- many (do notEndApp

204 args <- many (do notEndApp

191 simpleExpr syn)

205 simpleExpr syn)

192− return (fst doc, [], cn, args, fc, [])

206+ return (doc', [], cn, args, fc, [])

193 <?> "constructor"

207 <?> "constructor"

194

208

195{- | Parses a dsl block declaration

209{- | Parses a dsl block declaration

src/Idris/ParseExpr.hs+6

@@ -53,6 +53,11 @@ fullExpr syn = do x <- expr syn

53 i <- get

54 return $ debindApp syn (desugar syn i x)

56+tryFullExpr :: SyntaxInfo -> IState -> String -> Maybe PTerm

57+tryFullExpr syn st input =

58+ case runparser (fullExpr syn) st "" input of

59+ Success tm -> Just tm

60+ _ -> Nothing

57{- | Parses an expression

62{- | Parses an expression

58@

63@

@@ -1325,3 +1330,4 @@ fullTactic :: SyntaxInfo -> IdrisParser PTactic

1325fullTactic syn = do t <- tactic syn

1330fullTactic syn = do t <- tactic syn

1326 eof

1331 eof

1327 return t

1332 return t

1333+

src/Idris/ParseHelpers.hs+2−2

@@ -146,14 +146,14 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())

146 startEnd :: String

147 startEnd = "{}-"

148

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

149+{-| Parses a documentation comment (similar to haddock) given a marker character

150

151@

152 DocComment_t ::= '|||' ~EOL_t* EOL_t

153 ;

154@

155 -}

156−docComment :: IdrisParser (Docstring, [(Name, Docstring)])

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

157docComment = do dc <- pushIndent *> docCommentLine

158 rest <- many (indented docCommentLine)

159 args <- many $ do (name, first) <- indented argDocCommentLine

src/Idris/Parser.hs+22−13

@@ -329,12 +329,15 @@ fnDecl syn = try (do notEndBlock

329-}

330fnDecl' :: SyntaxInfo -> IdrisParser PDecl

331fnDecl' syn = checkFixity $

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

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

333 pushIndent

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

334 ist <- get

335 ist <- get

335− doc <- option noDocs docComment

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

336− ist <- get

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

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

339+

337− let initOpts = if default_total ist

340+ initOpts = if default_total ist

338 then [TotalFn]

341 then [TotalFn]

339 else []

342 else []

340 opts <- fnOpts initOpts

343 opts <- fnOpts initOpts

@@ -344,11 +347,11 @@ fnDecl' syn = checkFixity $

344 let n = expandNS syn n_in

347 let n = expandNS syn n_in

345 fc <- getFC

348 fc <- getFC

346 lchar ':'

349 lchar ':'

347− return (doc, fc, opts', n, acc))

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

348 ty <- typeExpr (allowImp syn)

351 ty <- typeExpr (allowImp syn)

349 terminator

352 terminator

350 addAcc n acc

353 addAcc n acc

351− return (PTy (fst doc) (snd doc) syn fc opts' n ty)

354+ return (PTy doc argDocs syn fc opts' n ty)

352 <|> postulate syn

355 <|> postulate syn

353 <|> caf syn

356 <|> caf syn

354 <|> pattern syn

357 <|> pattern syn

@@ -434,10 +437,12 @@ Postulate ::=

434@

437@

435-}

438-}

436postulate :: SyntaxInfo -> IdrisParser PDecl

439postulate :: SyntaxInfo -> IdrisParser PDecl

437−postulate syn = do doc <- try $ do doc <- option noDocs docComment

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

441+ ist <- get

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

438 pushIndent

443 pushIndent

439 reserved "postulate"

444 reserved "postulate"

440− return doc

445+ return doc'

441 ist <- get

446 ist <- get

442 let initOpts = if default_total ist

447 let initOpts = if default_total ist

443 then [TotalFn]

448 then [TotalFn]

@@ -452,7 +457,7 @@ postulate syn = do doc <- try $ do doc <- option noDocs docComment

452 fc <- getFC

457 fc <- getFC

453 terminator

458 terminator

454 addAcc n acc

459 addAcc n acc

455− return (PPostulate (fst doc) syn fc opts' n ty)

460+ return (PPostulate doc syn fc opts' n ty)

456 <?> "postulate"

461 <?> "postulate"

457

462

458{- | Parses a using declaration

463{- | Parses a using declaration

@@ -581,16 +586,20 @@ Class ::=

581@

586@

582-}

587-}

583class_ :: SyntaxInfo -> IdrisParser [PDecl]

588class_ :: SyntaxInfo -> IdrisParser [PDecl]

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

589+class_ syn = do (doc, argDocs, acc) <- try (do

585− doc <- option noDocs docComment

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

591+ ist <- get

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

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

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

586 acc <- optional accessibility

595 acc <- optional accessibility

587− return (doc, acc))

596+ return (doc', argDocs', acc))

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

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

589 let n = expandNS syn n_in

598 let n = expandNS syn n_in

590 cs <- many carg

599 cs <- many carg

591 ds <- option [] (classBlock syn)

600 ds <- option [] (classBlock syn)

592 accData acc n (concatMap declared ds)

601 accData acc n (concatMap declared ds)

593− return [PClass (fst doc) syn fc cons n cs (snd doc) ds]

602+ return [PClass doc syn fc cons n cs argDocs ds]

594 <?> "type-class declaration"

603 <?> "type-class declaration"

595 where

604 where

596 carg :: IdrisParser (Name, PTerm)

605 carg :: IdrisParser (Name, PTerm)

src/Idris/TypeSearch.hs+2−2

@@ -23,14 +23,14 @@ import Data.Traversable (traverse)

23import Idris.AbsSyntax (addUsingConstraints, addImpl, getIState, putIState, implicit)

24import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, eqTy, Idris,

25 IState (idris_classes, idris_docstrings, tt_ctxt, idris_outputmode),

26− implicitAllowed, OutputMode(..), prettyDocumentedIst, PTerm, toplevel)

26+ implicitAllowed, OutputMode(..), PTerm, toplevel)

27import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)

28import Idris.Core.TT hiding (score)

29import Idris.Core.Unify (match_unify)

30import Idris.Delaborate (delabTy)

31import Idris.Docstrings (noDocs, overview)

32import Idris.Elab.Type (elabType)

33−import Idris.Output (iRenderOutput, iPrintResult, iRenderResult)

33+import Idris.Output (iRenderOutput, iPrintResult, iRenderResult, prettyDocumentedIst)

35import Prelude hiding (pred)