git.iko.soy/Idris-dev
on master help sign in
Merge pull request #962 from david-christiansen/markdown-docs

Markdown syntax for documenation strings

commita7e655059300913335e26e78bc21c655979e616a authorEdwin Brady <edwin.brady@gmail.com> dateSun 9 Mar 2014, 22:44 (13 years ago) parentaf6eaebd910c2c
12 files changed+308−89
compare with master
unifiedsplit
idris.cabal+2 src/Idris/AbsSyntax.hs+2−1 src/Idris/AbsSyntaxTree.hs+27−26 src/Idris/DeepSeq.hs+42 src/Idris/Docs.hs+15−13 src/Idris/Docstrings.hs+80 src/Idris/ElabDecls.hs+30−27 src/Idris/IBC.hs+85−2 src/Idris/ParseData.hs+8−6 src/Idris/ParseHelpers.hs+10−8 src/Idris/ParseOps.hs−1 src/Idris/Parser.hs+7−5
idris.cabal+2
@@ -440,6 +440,7 @@ Library
440440 , Idris.DeepSeq
441441 , Idris.Delaborate
442442 , Idris.Docs
443+ , Idris.Docstrings
443444 , Idris.ElabDecls
444445 , Idris.ElabTerm
445446 , Idris.Error
@@ -506,6 +507,7 @@ Library
506507 , ansi-wl-pprint
507508 , binary
508509 , bytestring
510+ , cheapskate
509511 , containers >= 0.5
510512 , directory
511513 , directory >= 1.2
src/Idris/AbsSyntax.hs+2−1
@@ -9,6 +9,7 @@ import Idris.Core.Elaborate hiding (Tactic(..))
99import Idris.Core.Typecheck
1010import Idris.AbsSyntaxTree
1111import Idris.Colours
12+import Idris.Docstrings
1213import Idris.IdeSlave
1314import IRTS.CodegenCommon
1415import Util.DynamicLinker
@@ -262,7 +263,7 @@ addCoercion :: Name -> Idris ()
262263addCoercion n = do i <- getIState
263264 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
264265
265−addDocStr :: Name -> String -> [(Name, String)] -> Idris ()
266+addDocStr :: Name -> Docstring -> [(Name, Docstring)] -> Idris ()
266267addDocStr n doc args
267268 = do i <- getIState
268269 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
77import Idris.Core.Evaluate
88import Idris.Core.Elaborate hiding (Tactic(..))
99import Idris.Core.Typecheck
10+import Idris.Docstrings
1011import IRTS.Lang
1112import IRTS.CodegenCommon
1213import Util.Pretty
@@ -113,7 +114,7 @@ data IState = IState {
113114 idris_flags :: Ctxt [FnOpt],
114115 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
115116 idris_calledgraph :: Ctxt [Name],
116− idris_docstrings :: Ctxt (String, [(Name, String)]),
117+ idris_docstrings :: Ctxt (Docstring, [(Name, Docstring)]),
117118 idris_tyinfodata :: Ctxt TIData,
118119 idris_totcheck :: [(FC, Name)], -- names to check totality on
119120 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
@@ -453,15 +454,15 @@ data ProvideWhat = ProvTerm -- ^ only allow providing terms
453454-- datatypes and typeclasses.
454455data PDecl' t
455456 = PFix FC Fixity [String] -- ^ Fixity declaration
456− | PTy String [(Name, String)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
457− | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate
457+ | PTy Docstring [(Name, Docstring)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
458+ | PPostulate Docstring SyntaxInfo FC FnOpts Name t -- ^ Postulate
458459 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
459460 | PCAF FC Name t -- ^ Top level constant
460− | PData String [(Name, String)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
461+ | PData Docstring [(Name, Docstring)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
461462 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
462463 | PNamespace String [PDecl' t] -- ^ New namespace
463− | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration
464− | PClass String SyntaxInfo FC
464+ | PRecord Docstring SyntaxInfo FC Name t Docstring Name t -- ^ Record declaration
465+ | PClass Docstring SyntaxInfo FC
465466 [t] -- constraints
466467 Name
467468 [(Name, t)] -- parameters
@@ -515,7 +516,7 @@ deriving instance NFData PClause'
515516-- | Data declaration
516517data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
517518 d_tcon :: t, -- ^ Type constructor
518− d_cons :: [(String, [(Name, String)], Name, t, FC, [Name])] -- ^ Constructors
519+ d_cons :: [(Docstring, [(Name, Docstring)], Name, t, FC, [Name])] -- ^ Constructors
519520 }
520521 -- ^ Data declaration
521522 | PLaterdecl { d_name :: Name, d_tcon :: t }
@@ -951,9 +952,9 @@ inferTy = sMN 0 "__Infer"
951952inferCon = sMN 0 "__infer"
952953inferDecl = PDatadecl inferTy
953954 PType
954− [("", [], inferCon, PPi impl (sMN 0 "iType") PType (
955− PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
956− (PRef bi inferTy)), bi, [])]
955+ [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
956+ PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
957+ (PRef bi inferTy)), bi, [])]
957958inferOpts = []
958959
959960infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
@@ -981,7 +982,7 @@ primNames = [unitTy, unitCon,
981982unitTy = sMN 0 "__Unit"
982983unitCon = sMN 0 "__II"
983984unitDecl = PDatadecl unitTy PType
984− [("", [], unitCon, PRef bi unitTy, bi, [])]
985+ [(emptyDocstring, [], unitCon, PRef bi unitTy, bi, [])]
985986unitOpts = [DefaultEliminator]
986987
987988falseTy = sMN 0 "__False"
@@ -991,12 +992,12 @@ falseOpts = []
991992pairTy = sMN 0 "__Pair"
992993pairCon = sMN 0 "__MkPair"
993994pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
994− [("", [], pairCon, PPi impl (n "A") PType (
995− PPi impl (n "B") PType (
996− PPi expl (n "a") (PRef bi (n "A")) (
997− PPi expl (n "b") (PRef bi (n "B"))
998− (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
999− pexp (PRef bi (n "B"))])))), bi, [])]
995+ [(emptyDocstring, [], pairCon, PPi impl (n "A") PType (
996+ PPi impl (n "B") PType (
997+ PPi expl (n "a") (PRef bi (n "A")) (
998+ PPi expl (n "b") (PRef bi (n "B"))
999+ (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
1000+ pexp (PRef bi (n "B"))])))), bi, [])]
10001001 where n a = sMN 0 a
10011002pairOpts = []
10021003
@@ -1005,21 +1006,21 @@ eqCon = sUN "refl"
10051006eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
10061007 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
10071008 PType)
1008− [("", [], eqCon, PPi impl (n "A") PType (
1009− PPi impl (n "x") (PRef bi (n "A"))
1010− (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1011− pimp (n "B") Placeholder False,
1012− pexp (PRef bi (n "x")),
1013− pexp (PRef bi (n "x"))])), bi, [])]
1009+ [(emptyDocstring, [], eqCon, PPi impl (n "A") PType (
1010+ PPi impl (n "x") (PRef bi (n "A"))
1011+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1012+ pimp (n "B") Placeholder False,
1013+ pexp (PRef bi (n "x")),
1014+ pexp (PRef bi (n "x"))])), bi, [])]
10141015 where n a = sMN 0 a
10151016eqOpts = []
10161017
10171018elimName = sUN "__Elim"
10181019elimMethElimTy = sUN "__elimTy"
10191020elimMethElim = sUN "elim"
1020−elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]
1021− [PTy "" [] defaultSyntax bi [TotalFn] elimMethElimTy PType,
1022− PTy "" [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
1021+elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]
1022+ [PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElimTy PType,
1023+ PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
10231024
10241025-- Defined in builtins.idr
10251026sigmaTy = sUN "Exists"
src/Idris/DeepSeq.hs+42
@@ -6,6 +6,48 @@ import Idris.AbsSyntaxTree
66
77import Control.DeepSeq
88
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+
951-- All generated by 'derive'
1052
1153instance NFData Forceability where
src/Idris/Docs.hs+15−13
@@ -1,3 +1,4 @@
1+{-# LANGUAGE PatternGuards #-}
12module Idris.Docs where
23
34import Idris.AbsSyntax
@@ -5,6 +6,7 @@ import Idris.AbsSyntaxTree
56import Idris.Delaborate
67import Idris.Core.TT
78import Idris.Core.Evaluate
9+import Idris.Docstrings
810
911import Util.Pretty
1012
@@ -13,8 +15,8 @@ import Data.List
1315
1416-- TODO: Only include names with public/abstract accessibility
1517
16−data FunDoc = FD Name String
17− [(Name, PTerm, Plicity, Maybe String)] -- args: name, ty, implicit, docs
18+data FunDoc = FD Name Docstring
19+ [(Name, PTerm, Plicity, Maybe Docstring)] -- args: name, ty, implicit, docs
1820 PTerm -- function type
1921 (Maybe Fixity)
2022 deriving Show
@@ -22,16 +24,16 @@ data FunDoc = FD Name String
2224data Docs = FunDoc FunDoc
2325 | DataDoc FunDoc -- type constructor docs
2426 [FunDoc] -- data constructor docs
25− | ClassDoc Name String -- class docs
27+ | ClassDoc Name Docstring -- class docs
2628 [FunDoc] -- method docs
2729 deriving Show
2830
29−showDoc "" = empty
30−showDoc x = text " -- " <> text x
31+showDoc d | nullDocstring d = empty
32+ | otherwise = text " -- " <> renderDocstring d
3133
3234pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation
3335pprintFD 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 <$>
3537 maybe empty (\f -> text (show f) <> line) f <>
3638 let argshow = showArgs args [] in
3739 if not (null argshow)
@@ -41,20 +43,20 @@ pprintFD imp (FD n doc args ty f)
4143 where showArgs ((n, ty, Exp {}, d):args) bnd
4244 = bindingOf n False <+> colon <+>
4345 pprintPTerm imp bnd ty <>
44− showDoc (maybe "" id d) <> line
46+ showDoc (maybe emptyDocstring id d) <> line
4547 :
4648 showArgs args ((n, False):bnd)
4749 showArgs ((n, ty, Constraint {}, d):args) bnd
4850 = text "Class constraint" <+>
49− pprintPTerm imp bnd ty <> showDoc (maybe "" id d) <> line
51+ pprintPTerm imp bnd ty <> showDoc (maybe emptyDocstring id d) <> line
5052 :
5153 showArgs args ((n, True):bnd)
5254 showArgs ((n, ty, Imp {}, d):args) bnd
53− | not (null doc)
55+ | Just d' <- d
5456 = text "(implicit)" <+>
5557 bindingOf n True <+> colon <+>
5658 pprintPTerm imp bnd ty <>
57− showDoc (maybe "" id d) <> line
59+ showDoc d' <> line
5860 :
5961 showArgs args ((n, True):bnd)
6062 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
@@ -93,7 +95,7 @@ docClass n ci
9395 = do i <- getIState
9496 let docstr = case lookupCtxt n (idris_docstrings i) of
9597 [str] -> fst str
96− _ -> ""
98+ _ -> emptyDocstring
9799 mdocs <- mapM docFun (map fst (class_methods ci))
98100 return (ClassDoc n docstr mdocs)
99101
@@ -102,7 +104,7 @@ docFun n
102104 = do i <- getIState
103105 let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of
104106 [d] -> d
105− _ -> ("", [])
107+ _ -> noDocs
106108 let ty = delabTy i n
107109 let args = getPArgNames ty argDocs
108110 let infixes = idris_infixes i
@@ -116,7 +118,7 @@ docFun n
116118 funName (UN n) = str n
117119 funName (NS n _) = funName n
118120
119−getPArgNames :: PTerm -> [(Name, String)] -> [(Name, PTerm, Plicity, Maybe String)]
121+getPArgNames :: PTerm -> [(Name, Docstring)] -> [(Name, PTerm, Plicity, Maybe Docstring)]
120122getPArgNames (PPi plicity name ty body) ds =
121123 (name, ty, plicity, lookup name ds) : getPArgNames body ds
122124getPArgNames _ _ = []
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
5+
6+import qualified Cheapskate as C
7+import qualified Cheapskate.Types as CT
8+
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
2626import Idris.Core.Typecheck
2727import Idris.Core.CaseTree
2828
29+import Idris.Docstrings
30+
2931import Control.DeepSeq
3032import Control.Monad
3133import Control.Monad.State.Strict as State
@@ -63,12 +65,12 @@ checkAddDef add toplvl fc ((n, (i, top, t)) : ns)
6365-- return (n, (i, top, t'))) ns
6466
6567-- | 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)] ->
6769 FC -> FnOpts -> Name -> PTerm -> Idris Type
6870elabType = elabType' False
6971
7072elabType' :: Bool -> -- normalise it
71− ElabInfo -> SyntaxInfo -> String -> [(Name, String)] ->
73+ ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->
7274 FC -> FnOpts -> Name -> PTerm -> Idris Type
7375elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in
7476 n = liftname info n_in in -}
@@ -171,7 +173,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
171173 tyIsHandler _ = False
172174
173175
174−elabPostulate :: ElabInfo -> SyntaxInfo -> String ->
176+elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->
175177 FC -> FnOpts -> Name -> PTerm -> Idris ()
176178elabPostulate info syn doc fc opts n ty
177179 = do elabType info syn doc [] fc opts n ty
@@ -195,7 +197,7 @@ elabPostulate info syn doc fc opts n ty
195197 -- remove it from the deferred definitions list
196198 solveDeferred n
197199
198−elabData :: ElabInfo -> SyntaxInfo -> String -> [(Name, String)] -> FC -> DataOpts -> PData -> Idris ()
200+elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()
199201elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
200202 = do let codata = Codata `elem` opts
201203 iLOG (show (fc, doc))
@@ -257,8 +259,9 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
257259 updateContext (addDatatype (Data n ttag cty cons))
258260 updateContext (setMetaInformation n metainf)
259261 mapM_ (checkPositive n) cons
260− if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty
261− else return ()
262+ if DefaultEliminator `elem` opts
263+ then evalStateT (elabEliminator params n t dcons info) Map.empty
264+ else return ()
262265 where
263266 checkDefinedAs fc n t ctxt
264267 = case lookupDef n ctxt of
@@ -322,7 +325,7 @@ type EliminatorState = StateT (Map.Map String Int) Idris
322325
323326-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
324327elabEliminator :: [Int] -> Name -> PTerm ->
325− [(String, [(Name, String)], Name, PTerm, FC, [Name])] ->
328+ [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->
326329 ElabInfo -> EliminatorState ()
327330elabEliminator paramPos n ty cons info = do
328331 elimLog $ "Elaborating eliminator"
@@ -339,7 +342,7 @@ elabEliminator paramPos n ty cons info = do
339342 let motiveConstr = [(motiveName, expl, motive)]
340343 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))
341344 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
343346 let clauseConsElimArgs = map getPiName consTerms
344347 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
345348 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
@@ -488,7 +491,7 @@ elabEliminator paramPos n ty cons info = do
488491 splitArgPms _ = ([],[])
489492
490493
491− implicitIndexes :: (String, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
494+ implicitIndexes :: (Docstring, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
492495 implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do
493496 i <- State.lift getIState
494497 implargs' <- case lookupCtxt cnm (idris_implicits i) of
@@ -503,7 +506,7 @@ elabEliminator paramPos n ty cons info = do
503506 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
504507 _ -> return implargs
505508
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
507510 extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do
508511 let cons' = replaceParams paramPos generalParameters ty
509512 let (args, resTy) = splitPi cons'
@@ -539,7 +542,7 @@ elabEliminator paramPos n ty cons info = do
539542 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
540543 convertImplPi _ = Nothing
541544
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
543546 generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do
544547 let cons' = replaceParams paramPos generalParameters ty
545548 let (args, resTy) = splitPi cons'
@@ -561,7 +564,7 @@ elabEliminator paramPos n ty cons info = do
561564
562565elabPrims :: Idris ()
563566elabPrims = 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)
565568 (zip
566569 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
567570 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))
@@ -665,7 +668,7 @@ elabProvider info syn fc what n ty tm
665668 Provide tm
666669 | what `elem` [ProvTerm, ProvAny] ->
667670 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
669672 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]
670673 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
671674 | otherwise ->
@@ -673,7 +676,7 @@ elabProvider info syn fc what n ty tm
673676 Postulate
674677 | what `elem` [ProvPostulate, ProvAny] ->
675678 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
677680 logLvl 3 $ "Elaborated provided postulate " ++ show n
678681 | otherwise ->
679682 ierror . Msg $ "Attempted to provide a postulate where a term was expected."
@@ -724,8 +727,8 @@ elabTransform info fc safe lhs_in rhs_in
724727 addIBC (IBCTrans (clhs_tm, crhs_tm))
725728
726729
727−elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
728− PTerm -> String -> Name -> PTerm -> Idris ()
730+elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->
731+ PTerm -> Docstring -> Name -> PTerm -> Idris ()
729732elabRecord info syn doc fc tyn ty cdoc cn cty
730733 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])
731734 cty' <- implicit syn cn cty
@@ -797,7 +800,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
797800
798801 mkProj recty substs cimp ((pn_in, pty), pos)
799802 = do let pn = expandNS syn pn_in
800− let pfnTy = PTy "" [] defaultSyntax fc [] pn
803+ let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn
801804 (PPi expl rec recty
802805 (substMatches substs pty))
803806 let pls = repeat Placeholder
@@ -818,7 +821,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
818821 let valname = sMN 0 "updateval"
819822 let pt = k (PPi expl pn pty
820823 (PPi expl rec recty recty))
821− let pfnTy = PTy "" [] defaultSyntax fc [] setname pt
824+ let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt
822825 let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]
823826 let lhsArgs = pls
824827 let rhsArgs = take pos pls ++ (PRef fc valname) :
@@ -834,7 +837,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
834837 return (pn, pfnTy, PClauses fc [] setname [pclause])
835838
836839elabCon :: 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)
838841elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
839842 = do checkUndefined fc n
840843 ctxt <- getContext
@@ -1166,7 +1169,7 @@ elabPE info fc caller r =
11661169 (map (\ (lhs, rhs) ->
11671170 (showTmImpls lhs ++ " = " ++
11681171 showTmImpls rhs)) pats)
1169− elabType info defaultSyntax "" [] fc opts newnm specTy
1172+ elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy
11701173 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats
11711174 elabClauses info fc opts newnm def
11721175 logLvl 2 $ "Specialised " ++ show newnm)
@@ -1725,7 +1728,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
17251728
17261729data MArgTy = IA | EA | CA deriving Show
17271730
1728−elabClass :: ElabInfo -> SyntaxInfo -> String ->
1731+elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->
17291732 FC -> [PTerm] ->
17301733 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
17311734elabClass info syn doc fc constraints tn ps ds
@@ -1752,7 +1755,7 @@ elabClass info syn doc fc constraints tn ps ds
17521755 let cty = impbind ps $ conbind constraints
17531756 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
17541757 constraint
1755− let cons = [("", [], cn, cty, fc, [])]
1758+ let cons = [(emptyDocstring, [], cn, cty, fc, [])]
17561759 let ddecl = PDatadecl tn tty cons
17571760 logLvl 5 $ "Class data " ++ show (showDImp True ddecl)
17581761 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc [] fc [] ddecl
@@ -1807,7 +1810,7 @@ elabClass info syn doc fc constraints tn ps ds
18071810 case lookup n mtys of
18081811 Just (syn, o, ty) -> do let ty' = insertConstraint c ty
18091812 let ds = map (decorateid defaultdec)
1810− [PTy "" [] syn fc [] n ty',
1813+ [PTy emptyDocstring [] syn fc [] n ty',
18111814 PClauses fc (o ++ opts) n cs]
18121815 iLOG (show ds)
18131816 return (n, ((defaultdec n, ds!!1), ds))
@@ -1845,7 +1848,7 @@ elabClass info syn doc fc constraints tn ps ds
18451848 addInstance False conn' cfn
18461849 addIBC (IBCInstance False conn' cfn)
18471850-- iputStrLn ("Added " ++ show (conn, cfn, ty))
1848− return [PTy "" [] syn fc [] cfn ty,
1851+ return [PTy emptyDocstring [] syn fc [] cfn ty,
18491852 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
18501853
18511854 -- Generate a top level function which looks up a method in a given
@@ -1909,7 +1912,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
19091912 let constraint = PApp fc (PRef fc n) (map pexp ps)
19101913 let iname = mkiname n ps expn
19111914 when (what /= EDefns) $ do
1912− nty <- elabType' True info syn "" [] fc [] iname t
1915+ nty <- elabType' True info syn emptyDocstring [] fc [] iname t
19131916 -- if the instance type matches any of the instances we have already,
19141917 -- and it's not a named instance, then it's overlapping, so report an error
19151918 case expn of
@@ -2061,7 +2064,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
20612064 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
20622065 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
20632066
2064− mkTyDecl (n, op, t, _) = PTy "" [] syn fc op n t
2067+ mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t
20652068
20662069 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)
20672070 conbind [] x = x
@@ -2308,7 +2311,7 @@ inferredDiff fc inf user =
23082311-- | Check a PTerm against documentation and ensure that every documented
23092312-- argument actually exists. This must be run _after_ implicits have been
23102313-- found, or it will give spurious errors.
2311−checkDocs :: FC -> [(Name, String)] -> PTerm -> Idris ()
2314+checkDocs :: FC -> [(Name, Docstring)] -> PTerm -> Idris ()
23122315checkDocs fc args tm = cd (Map.fromList args) tm
23132316 where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc
23142317 cd as _ | Map.null as = return ()
src/Idris/IBC.hs+85−2
@@ -9,6 +9,9 @@ import Idris.AbsSyntax
99import Idris.Imports
1010import Idris.Error
1111import Idris.Delaborate
12+import Idris.Docstrings
13+
14+import qualified Cheapskate.Types as CT
1215
1316import Data.Binary
1417import Data.Vector.Binary
@@ -52,7 +55,7 @@ data IBCFile = IBCFile { ver :: Word8,
5255 ibc_flags :: [(Name, [FnOpt])],
5356 ibc_cg :: [(Name, CGInfo)],
5457 ibc_defs :: [(Name, Def)],
55− ibc_docstrings :: [(Name, (String, [(Name, String)]))],
58+ ibc_docstrings :: [(Name, (Docstring, [(Name, Docstring)]))],
5659 ibc_transforms :: [(Term, Term)],
5760 ibc_errRev :: [(Term, Term)],
5861 ibc_coercions :: [Name],
@@ -405,7 +408,7 @@ pDefs syms ds
405408 update (Proj t i) = Proj (update t) i
406409 update t = t
407410
408−pDocs :: [(Name, (String, [(Name, String)]))] -> Idris ()
411+pDocs :: [(Name, (Docstring, [(Name, Docstring)]))] -> Idris ()
409412pDocs ds = mapM_ (\ (n, a) -> addDocStr n (fst a) (snd a)) ds
410413
411414pAccess :: [(Name, Accessibility)] -> Idris ()
@@ -461,6 +464,86 @@ pMetavars ns = do i <- getIState
461464 putIState $ i { idris_metavars = Data.List.reverse ns
462465 ++ idris_metavars i }
463466
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+
464547----- Generated by 'derive'
465548
466549instance Binary SizeChange where
src/Idris/ParseData.hs+8−6
@@ -20,6 +20,8 @@ import Idris.DSL
2020import Idris.Core.TT
2121import Idris.Core.Evaluate
2222
23+import Idris.Docstrings
24+
2325import Control.Applicative
2426import Control.Monad
2527import Control.Monad.State.Strict
@@ -41,7 +43,7 @@ Record ::=
4143-}
4244record :: SyntaxInfo -> IdrisParser PDecl
4345record syn = do (doc, acc) <- try (do
44− doc <- option ("", []) docComment
46+ doc <- option noDocs docComment
4547 acc <- optional accessibility
4648 reserved "record"
4749 return (doc, acc))
@@ -103,7 +105,7 @@ SimpleConstructorList ::=
103105-}
104106data_ :: SyntaxInfo -> IdrisParser PDecl
105107data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do
106− (doc, argDocs) <- option ("", []) docComment
108+ (doc, argDocs) <- option noDocs docComment
107109 pushIndent
108110 acc <- optional accessibility
109111 elim <- dataOpts []
@@ -160,9 +162,9 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do
160162{- | Parses a type constructor declaration
161163 Constructor ::= DocComment? FnName TypeSig;
162164-}
163−constructor :: SyntaxInfo -> IdrisParser (String, [(Name, String)], Name, PTerm, FC, [Name])
165+constructor :: SyntaxInfo -> IdrisParser (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])
164166constructor syn
165− = do (doc, argDocs) <- option ("", []) docComment
167+ = do (doc, argDocs) <- option noDocs docComment
166168 cn_in <- fnName; fc <- getFC
167169 let cn = expandNS syn cn_in
168170 lchar ':'
@@ -177,9 +179,9 @@ constructor syn
177179{- | Parses a constructor for simple discriminative union data types
178180 SimpleConstructor ::= FnName SimpleExpr* DocComment?
179181-}
180−simpleConstructor :: SyntaxInfo -> IdrisParser (String, [(Name, String)], Name, [PTerm], FC, [Name])
182+simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring, [(Name, Docstring)], Name, [PTerm], FC, [Name])
181183simpleConstructor syn
182− = do doc <- option ("", []) (try docComment)
184+ = do doc <- option noDocs (try docComment)
183185 cn_in <- fnName
184186 let cn = expandNS syn cn_in
185187 fc <- getFC
src/Idris/ParseHelpers.hs+10−8
@@ -17,6 +17,7 @@ import Idris.AbsSyntax
1717import Idris.Core.TT
1818import Idris.Core.Evaluate
1919import Idris.Delaborate (pprintErr)
20+import Idris.Docstrings
2021
2122import qualified Util.Pretty as Pretty (text)
2223
@@ -142,25 +143,26 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())
142143{-| Parses a documentation comment (similar to haddoc) given a marker character
143144
144145@
145− DocComment_t ::= '--' DocCommentMarker_t ~EOL_t* EOL_t
146− | '{ -' DocCommentMarket_t ~'- }'* '- }'
146+ DocComment_t ::= '|||' ~EOL_t* EOL_t
147147 ;
148148@
149149 -}
150−docComment :: IdrisParser (String, [(Name, String)])
150+docComment :: IdrisParser (Docstring, [(Name, Docstring)])
151151docComment = do dc <- pushIndent *> docCommentLine
152152 rest <- many (indented docCommentLine)
153153 args <- many (indented argDocCommentLine)
154154 popIndent
155− return (T.unpack $ T.strip $ T.pack (dc ++ concat rest), args)
155+ return (parseDocstring $ T.pack (concat . intersperse "\n" $ dc:rest),
156+ map (\(n, d) -> (n, parseDocstring (T.pack d))) args)
156157
157158 where docCommentLine :: MonadicParsing m => m String
158159 docCommentLine = try (do string "|||"
159− many (satisfy isSpace)
160− first <- satisfy (\c -> not (isEol c || c == '@'))
161− res <- many (satisfy (not . isEol))
160+ many (satisfy (==' '))
161+ contents <- option "" (do first <- satisfy (\c -> not (isEol c || c == '@'))
162+ res <- many (satisfy (not . isEol))
163+ return $ first:res)
162164 eol ; someSpace
163− return (first:res))-- ++ concat rest))
165+ return contents)-- ++ concat rest))
164166 <?> ""
165167 argDocCommentLine = do string "|||"
166168 many (satisfy isSpace)
src/Idris/ParseOps.hs−1
@@ -59,7 +59,6 @@ binary name f = Infix (do fc <- getFC
5959 indentPropHolds gtProp
6060 reservedOp name
6161 indentPropHolds gtProp
62− doc <- option ("", []) docComment
6362 return (f fc))
6463
6564-- | Prefix operator
src/Idris/Parser.hs+7−5
@@ -35,6 +35,8 @@ import Idris.ParseOps
3535import Idris.ParseExpr
3636import Idris.ParseData
3737
38+import Idris.Docstrings
39+
3840import Paths_idris
3941
4042import Util.DynamicLinker
@@ -315,7 +317,7 @@ fnDecl' syn = checkFixity $
315317 do (doc, fc, opts', n, acc) <- try (do
316318 pushIndent
317319 ist <- get
318− doc <- option ("", []) docComment
320+ doc <- option noDocs docComment
319321 ist <- get
320322 let initOpts = if default_total ist
321323 then [TotalFn]
@@ -413,7 +415,7 @@ Postulate ::=
413415@
414416-}
415417postulate :: SyntaxInfo -> IdrisParser PDecl
416−postulate syn = do doc <- try $ do doc <- option ("", []) docComment
418+postulate syn = do doc <- try $ do doc <- option noDocs docComment
417419 pushIndent
418420 reserved "postulate"
419421 return doc
@@ -561,7 +563,7 @@ Class ::=
561563-}
562564class_ :: SyntaxInfo -> IdrisParser [PDecl]
563565class_ syn = do (doc, acc) <- try (do
564− doc <- option ("", []) docComment
566+ doc <- option noDocs docComment
565567 acc <- optional accessibility
566568 return (doc, acc))
567569 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
10031005 mapM_ (addNameHint ty') ns
10041006 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
10051007 <|> do try (lchar '%' *> reserved "error_handlers")
1006− fn <- iName []
1007− arg <- iName []
1008+ fn <- fnName
1009+ arg <- fnName
10081010 ns <- sepBy1 name (lchar ',')
10091011 return [PDirective (do fn' <- disambiguate fn
10101012 ns' <- mapM disambiguate ns