git.iko.soy/Idris-dev
on master help sign in
Merge pull request #962 from david-christiansen/markdown-docs
a7e6550Edwin Brady
idris.cabal+2
compare with master
unifiedsplit
@@ -440,6 +440,7 @@ Library
440 , Idris.DeepSeq
440 , Idris.DeepSeq
441 , Idris.Delaborate
441 , Idris.Delaborate
442 , Idris.Docs
442 , Idris.Docs
443+ , Idris.Docstrings
443 , Idris.ElabDecls
444 , Idris.ElabDecls
444 , Idris.ElabTerm
445 , Idris.ElabTerm
445 , Idris.Error
446 , Idris.Error
@@ -506,6 +507,7 @@ Library
506 , ansi-wl-pprint
507 , ansi-wl-pprint
507 , binary
508 , binary
508 , bytestring
509 , bytestring
510+ , cheapskate
509 , containers >= 0.5
511 , containers >= 0.5
510 , directory
512 , directory
511 , directory >= 1.2
513 , directory >= 1.2
src/Idris/AbsSyntax.hs+2−1
@@ -9,6 +9,7 @@ import Idris.Core.Elaborate hiding (Tactic(..))
9import Idris.Core.Typecheck
9import Idris.Core.Typecheck
10import Idris.AbsSyntaxTree
10import Idris.AbsSyntaxTree
11import Idris.Colours
11import Idris.Colours
12+import Idris.Docstrings
12import Idris.IdeSlave
13import Idris.IdeSlave
13import IRTS.CodegenCommon
14import IRTS.CodegenCommon
14import Util.DynamicLinker
15import Util.DynamicLinker
@@ -262,7 +263,7 @@ addCoercion :: Name -> Idris ()
262addCoercion n = do i <- getIState
263addCoercion n = do i <- getIState
263 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
264 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
264
265
265−addDocStr :: Name -> String -> [(Name, String)] -> Idris ()
266+addDocStr :: Name -> Docstring -> [(Name, Docstring)] -> Idris ()
266addDocStr n doc args
267addDocStr n doc args
267 = do i <- getIState
268 = do i <- getIState
268 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
269 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
src/Idris/AbsSyntaxTree.hs+27−26
@@ -7,6 +7,7 @@ import Idris.Core.TT
7import Idris.Core.Evaluate
7import Idris.Core.Evaluate
8import Idris.Core.Elaborate hiding (Tactic(..))
8import Idris.Core.Elaborate hiding (Tactic(..))
9import Idris.Core.Typecheck
9import Idris.Core.Typecheck
10+import Idris.Docstrings
10import IRTS.Lang
11import IRTS.Lang
11import IRTS.CodegenCommon
12import IRTS.CodegenCommon
12import Util.Pretty
13import Util.Pretty
@@ -113,7 +114,7 @@ data IState = IState {
113 idris_flags :: Ctxt [FnOpt],
114 idris_flags :: Ctxt [FnOpt],
114 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
115 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
115 idris_calledgraph :: Ctxt [Name],
116 idris_calledgraph :: Ctxt [Name],
116− idris_docstrings :: Ctxt (String, [(Name, String)]),
117+ idris_docstrings :: Ctxt (Docstring, [(Name, Docstring)]),
117 idris_tyinfodata :: Ctxt TIData,
118 idris_tyinfodata :: Ctxt TIData,
118 idris_totcheck :: [(FC, Name)], -- names to check totality on
119 idris_totcheck :: [(FC, Name)], -- names to check totality on
119 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
120 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
@@ -453,15 +454,15 @@ data ProvideWhat = ProvTerm -- ^ only allow providing terms
453-- datatypes and typeclasses.
454-- datatypes and typeclasses.
454data PDecl' t
455data PDecl' t
455 = PFix FC Fixity [String] -- ^ Fixity declaration
456 = PFix FC Fixity [String] -- ^ Fixity declaration
456− | PTy String [(Name, String)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
457+ | PTy Docstring [(Name, Docstring)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
457− | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate
458+ | PPostulate Docstring SyntaxInfo FC FnOpts Name t -- ^ Postulate
458 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
459 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
459 | PCAF FC Name t -- ^ Top level constant
460 | 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.
461 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
462 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
462 | PNamespace String [PDecl' t] -- ^ New namespace
463 | PNamespace String [PDecl' t] -- ^ New namespace
463− | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration
464+ | PRecord Docstring SyntaxInfo FC Name t Docstring Name t -- ^ Record declaration
464− | PClass String SyntaxInfo FC
465+ | PClass Docstring SyntaxInfo FC
465 [t] -- constraints
466 [t] -- constraints
466 Name
467 Name
467 [(Name, t)] -- parameters
468 [(Name, t)] -- parameters
@@ -515,7 +516,7 @@ deriving instance NFData PClause'
515-- | Data declaration
516-- | Data declaration
516data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
517data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
517 d_tcon :: t, -- ^ Type constructor
518 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
519 }
520 }
520 -- ^ Data declaration
521 -- ^ Data declaration
521 | PLaterdecl { d_name :: Name, d_tcon :: t }
522 | PLaterdecl { d_name :: Name, d_tcon :: t }
@@ -951,9 +952,9 @@ inferTy = sMN 0 "__Infer"
951inferCon = sMN 0 "__infer"
952inferCon = sMN 0 "__infer"
952inferDecl = PDatadecl inferTy
953inferDecl = PDatadecl inferTy
953 PType
954 PType
954− [("", [], inferCon, PPi impl (sMN 0 "iType") PType (
955+ [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
955− PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
956+ PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
956− (PRef bi inferTy)), bi, [])]
957+ (PRef bi inferTy)), bi, [])]
957inferOpts = []
958inferOpts = []
958
959
959infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
960infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
@@ -981,7 +982,7 @@ primNames = [unitTy, unitCon,
981unitTy = sMN 0 "__Unit"
982unitTy = sMN 0 "__Unit"
982unitCon = sMN 0 "__II"
983unitCon = sMN 0 "__II"
983unitDecl = PDatadecl unitTy PType
984unitDecl = PDatadecl unitTy PType
984− [("", [], unitCon, PRef bi unitTy, bi, [])]
985+ [(emptyDocstring, [], unitCon, PRef bi unitTy, bi, [])]
985unitOpts = [DefaultEliminator]
986unitOpts = [DefaultEliminator]
986
987
987falseTy = sMN 0 "__False"
988falseTy = sMN 0 "__False"
@@ -991,12 +992,12 @@ falseOpts = []
991pairTy = sMN 0 "__Pair"
992pairTy = sMN 0 "__Pair"
992pairCon = sMN 0 "__MkPair"
993pairCon = sMN 0 "__MkPair"
993pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
994pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
994− [("", [], pairCon, PPi impl (n "A") PType (
995+ [(emptyDocstring, [], pairCon, PPi impl (n "A") PType (
995− PPi impl (n "B") PType (
996+ PPi impl (n "B") PType (
996− PPi expl (n "a") (PRef bi (n "A")) (
997+ PPi expl (n "a") (PRef bi (n "A")) (
997− PPi expl (n "b") (PRef bi (n "B"))
998+ PPi expl (n "b") (PRef bi (n "B"))
998− (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
999+ (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
999− pexp (PRef bi (n "B"))])))), bi, [])]
1000+ pexp (PRef bi (n "B"))])))), bi, [])]
1000 where n a = sMN 0 a
1001 where n a = sMN 0 a
1001pairOpts = []
1002pairOpts = []
1002
1003
@@ -1005,21 +1006,21 @@ eqCon = sUN "refl"
1005eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
1006eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
1006 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1007 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1007 PType)
1008 PType)
1008− [("", [], eqCon, PPi impl (n "A") PType (
1009+ [(emptyDocstring, [], eqCon, PPi impl (n "A") PType (
1009− PPi impl (n "x") (PRef bi (n "A"))
1010+ PPi impl (n "x") (PRef bi (n "A"))
1010− (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1011+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1011− pimp (n "B") Placeholder False,
1012+ pimp (n "B") Placeholder False,
1012− pexp (PRef bi (n "x")),
1013+ pexp (PRef bi (n "x")),
1013− pexp (PRef bi (n "x"))])), bi, [])]
1014+ pexp (PRef bi (n "x"))])), bi, [])]
1014 where n a = sMN 0 a
1015 where n a = sMN 0 a
1015eqOpts = []
1016eqOpts = []
1016
1017
1017elimName = sUN "__Elim"
1018elimName = sUN "__Elim"
1018elimMethElimTy = sUN "__elimTy"
1019elimMethElimTy = sUN "__elimTy"
1019elimMethElim = sUN "elim"
1020elimMethElim = sUN "elim"
1020−elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]
1021+elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]
1021− [PTy "" [] defaultSyntax bi [TotalFn] elimMethElimTy PType,
1022+ [PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElimTy PType,
1022− PTy "" [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
1023+ PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
1023
1024
1024-- Defined in builtins.idr
1025-- Defined in builtins.idr
1025sigmaTy = sUN "Exists"
1026sigmaTy = sUN "Exists"
src/Idris/DeepSeq.hs+42
@@ -6,6 +6,48 @@ import Idris.AbsSyntaxTree
6
6
7import Control.DeepSeq
7import Control.DeepSeq
8
8
9+import qualified Cheapskate.Types as CT
10+
11+-- Manual from imported libs
12+instance NFData CT.Doc where
13+ rnf (CT.Doc opts contents) = rnf opts `seq` rnf contents `seq` ()
14+
15+instance NFData CT.Options where
16+ rnf (CT.Options x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
17+
18+instance NFData CT.Block where
19+ rnf (CT.Para lines) = rnf lines `seq` ()
20+ rnf (CT.Header i lines) = rnf i `seq` rnf lines `seq` ()
21+ rnf (CT.Blockquote bs) = rnf bs `seq` ()
22+ rnf (CT.List b t xs) = rnf b `seq` rnf t `seq` rnf xs `seq` ()
23+ rnf (CT.CodeBlock attr txt) = rnf attr `seq` rnf txt `seq` ()
24+ rnf (CT.HtmlBlock txt) = rnf txt `seq` ()
25+ rnf CT.HRule = ()
26+
27+instance NFData CT.Inline where
28+ rnf (CT.Str txt) = rnf txt `seq` ()
29+ rnf CT.Space = ()
30+ rnf CT.SoftBreak = ()
31+ rnf CT.LineBreak = ()
32+ rnf (CT.Emph xs) = rnf xs `seq` ()
33+ rnf (CT.Strong xs) = rnf xs `seq` ()
34+ rnf (CT.Code xs) = rnf xs `seq` ()
35+ rnf (CT.Link a b xs) = rnf a `seq` rnf b `seq` rnf xs `seq` ()
36+ rnf (CT.Image a b c) = rnf a `seq` rnf b `seq` rnf c `seq` ()
37+ rnf (CT.Entity a) = rnf a `seq` ()
38+ rnf (CT.RawHtml x) = rnf x `seq` ()
39+
40+instance NFData CT.ListType where
41+ rnf (CT.Bullet c) = rnf c `seq` ()
42+ rnf (CT.Numbered nw i) = rnf nw `seq` rnf i `seq` ()
43+
44+instance NFData CT.CodeAttr where
45+ rnf (CT.CodeAttr a b) = rnf a `seq` rnf b `seq` ()
46+
47+instance NFData CT.NumWrapper where
48+ rnf CT.PeriodFollowing = ()
49+ rnf CT.ParenFollowing = ()
50+
9-- All generated by 'derive'
51-- All generated by 'derive'
10
52
11instance NFData Forceability where
53instance NFData Forceability where
src/Idris/Docs.hs+15−13
@@ -1,3 +1,4 @@
1+{-# LANGUAGE PatternGuards #-}
1module Idris.Docs where
2module Idris.Docs where
2
3
3import Idris.AbsSyntax
4import Idris.AbsSyntax
@@ -5,6 +6,7 @@ import Idris.AbsSyntaxTree
5import Idris.Delaborate
6import Idris.Delaborate
6import Idris.Core.TT
7import Idris.Core.TT
7import Idris.Core.Evaluate
8import Idris.Core.Evaluate
9+import Idris.Docstrings
8
10
9import Util.Pretty
11import Util.Pretty
10
12
@@ -13,8 +15,8 @@ import Data.List
13
15
14-- TODO: Only include names with public/abstract accessibility
16-- TODO: Only include names with public/abstract accessibility
15
17
16−data FunDoc = FD Name String
18+data FunDoc = FD Name Docstring
17− [(Name, PTerm, Plicity, Maybe String)] -- args: name, ty, implicit, docs
19+ [(Name, PTerm, Plicity, Maybe Docstring)] -- args: name, ty, implicit, docs
18 PTerm -- function type
20 PTerm -- function type
19 (Maybe Fixity)
21 (Maybe Fixity)
20 deriving Show
22 deriving Show
@@ -22,16 +24,16 @@ data FunDoc = FD Name String
22data Docs = FunDoc FunDoc
24data Docs = FunDoc FunDoc
23 | DataDoc FunDoc -- type constructor docs
25 | DataDoc FunDoc -- type constructor docs
24 [FunDoc] -- data constructor docs
26 [FunDoc] -- data constructor docs
25− | ClassDoc Name String -- class docs
27+ | ClassDoc Name Docstring -- class docs
26 [FunDoc] -- method docs
28 [FunDoc] -- method docs
27 deriving Show
29 deriving Show
28
30
29−showDoc "" = empty
31+showDoc d | nullDocstring d = empty
30−showDoc x = text " -- " <> text x
32+ | otherwise = text " -- " <> renderDocstring d
31
33
32pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation
34pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation
33pprintFD imp (FD n doc args ty f)
35pprintFD imp (FD n doc args ty f)
34− = nest 4 (prettyName imp [] n <+> colon <+> prettyImp imp ty <$> showDoc doc <$>
36+ = nest 4 (prettyName imp [] n <+> colon <+> prettyImp imp ty <$> renderDocstring doc <$>
35 maybe empty (\f -> text (show f) <> line) f <>
37 maybe empty (\f -> text (show f) <> line) f <>
36 let argshow = showArgs args [] in
38 let argshow = showArgs args [] in
37 if not (null argshow)
39 if not (null argshow)
@@ -41,20 +43,20 @@ pprintFD imp (FD n doc args ty f)
41 where showArgs ((n, ty, Exp {}, d):args) bnd
43 where showArgs ((n, ty, Exp {}, d):args) bnd
42 = bindingOf n False <+> colon <+>
44 = bindingOf n False <+> colon <+>
43 pprintPTerm imp bnd ty <>
45 pprintPTerm imp bnd ty <>
44− showDoc (maybe "" id d) <> line
46+ showDoc (maybe emptyDocstring id d) <> line
45 :
47 :
46 showArgs args ((n, False):bnd)
48 showArgs args ((n, False):bnd)
47 showArgs ((n, ty, Constraint {}, d):args) bnd
49 showArgs ((n, ty, Constraint {}, d):args) bnd
48 = text "Class constraint" <+>
50 = text "Class constraint" <+>
49− pprintPTerm imp bnd ty <> showDoc (maybe "" id d) <> line
51+ pprintPTerm imp bnd ty <> showDoc (maybe emptyDocstring id d) <> line
50 :
52 :
51 showArgs args ((n, True):bnd)
53 showArgs args ((n, True):bnd)
52 showArgs ((n, ty, Imp {}, d):args) bnd
54 showArgs ((n, ty, Imp {}, d):args) bnd
53− | not (null doc)
55+ | Just d' <- d
54 = text "(implicit)" <+>
56 = text "(implicit)" <+>
55 bindingOf n True <+> colon <+>
57 bindingOf n True <+> colon <+>
56 pprintPTerm imp bnd ty <>
58 pprintPTerm imp bnd ty <>
57− showDoc (maybe "" id d) <> line
59+ showDoc d' <> line
58 :
60 :
59 showArgs args ((n, True):bnd)
61 showArgs args ((n, True):bnd)
60 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
62 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
@@ -93,7 +95,7 @@ docClass n ci
93 = do i <- getIState
95 = do i <- getIState
94 let docstr = case lookupCtxt n (idris_docstrings i) of
96 let docstr = case lookupCtxt n (idris_docstrings i) of
95 [str] -> fst str
97 [str] -> fst str
96− _ -> ""
98+ _ -> emptyDocstring
97 mdocs <- mapM docFun (map fst (class_methods ci))
99 mdocs <- mapM docFun (map fst (class_methods ci))
98 return (ClassDoc n docstr mdocs)
100 return (ClassDoc n docstr mdocs)
99
101
@@ -102,7 +104,7 @@ docFun n
102 = do i <- getIState
104 = do i <- getIState
103 let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of
105 let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of
104 [d] -> d
106 [d] -> d
105− _ -> ("", [])
107+ _ -> noDocs
106 let ty = delabTy i n
108 let ty = delabTy i n
107 let args = getPArgNames ty argDocs
109 let args = getPArgNames ty argDocs
108 let infixes = idris_infixes i
110 let infixes = idris_infixes i
@@ -116,7 +118,7 @@ docFun n
116 funName (UN n) = str n
118 funName (UN n) = str n
117 funName (NS n _) = funName n
119 funName (NS n _) = funName n
118
120
119−getPArgNames :: PTerm -> [(Name, String)] -> [(Name, PTerm, Plicity, Maybe String)]
121+getPArgNames :: PTerm -> [(Name, Docstring)] -> [(Name, PTerm, Plicity, Maybe Docstring)]
120getPArgNames (PPi plicity name ty body) ds =
122getPArgNames (PPi plicity name ty body) ds =
121 (name, ty, plicity, lookup name ds) : getPArgNames body ds
123 (name, ty, plicity, lookup name ds) : getPArgNames body ds
122getPArgNames _ _ = []
124getPArgNames _ _ = []
src/Idris/Docstrings.hsnew file+80
@@ -0,0 +1,80 @@
1+-- | Wrapper around Markdown library
2+module Idris.Docstrings (
3+ Docstring, parseDocstring, renderDocstring, emptyDocstring, nullDocstring, noDocs
4+ ) where
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
26import Idris.Core.Typecheck
26import Idris.Core.Typecheck
27import Idris.Core.CaseTree
27import Idris.Core.CaseTree
28
28
29+import Idris.Docstrings
30+
29import Control.DeepSeq
31import Control.DeepSeq
30import Control.Monad
32import Control.Monad
31import Control.Monad.State.Strict as State
33import Control.Monad.State.Strict as State
@@ -63,12 +65,12 @@ checkAddDef add toplvl fc ((n, (i, top, t)) : ns)
63-- return (n, (i, top, t'))) ns
65-- return (n, (i, top, t'))) ns
64
66
65-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
67-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
66−elabType :: ElabInfo -> SyntaxInfo -> String -> [(Name, String)] ->
68+elabType :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->
67 FC -> FnOpts -> Name -> PTerm -> Idris Type
69 FC -> FnOpts -> Name -> PTerm -> Idris Type
68elabType = elabType' False
70elabType = elabType' False
69
71
70elabType' :: Bool -> -- normalise it
72elabType' :: Bool -> -- normalise it
71− ElabInfo -> SyntaxInfo -> String -> [(Name, String)] ->
73+ ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] ->
72 FC -> FnOpts -> Name -> PTerm -> Idris Type
74 FC -> FnOpts -> Name -> PTerm -> Idris Type
73elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in
75elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in
74 n = liftname info n_in in -}
76 n = liftname info n_in in -}
@@ -171,7 +173,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
171 tyIsHandler _ = False
173 tyIsHandler _ = False
172
174
173
175
174−elabPostulate :: ElabInfo -> SyntaxInfo -> String ->
176+elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->
175 FC -> FnOpts -> Name -> PTerm -> Idris ()
177 FC -> FnOpts -> Name -> PTerm -> Idris ()
176elabPostulate info syn doc fc opts n ty
178elabPostulate info syn doc fc opts n ty
177 = do elabType info syn doc [] fc opts n ty
179 = do elabType info syn doc [] fc opts n ty
@@ -195,7 +197,7 @@ elabPostulate info syn doc fc opts n ty
195 -- remove it from the deferred definitions list
197 -- remove it from the deferred definitions list
196 solveDeferred n
198 solveDeferred n
197
199
198−elabData :: ElabInfo -> SyntaxInfo -> String -> [(Name, String)] -> FC -> DataOpts -> PData -> Idris ()
200+elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()
199elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
201elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
200 = do let codata = Codata `elem` opts
202 = do let codata = Codata `elem` opts
201 iLOG (show (fc, doc))
203 iLOG (show (fc, doc))
@@ -257,8 +259,9 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
257 updateContext (addDatatype (Data n ttag cty cons))
259 updateContext (addDatatype (Data n ttag cty cons))
258 updateContext (setMetaInformation n metainf)
260 updateContext (setMetaInformation n metainf)
259 mapM_ (checkPositive n) cons
261 mapM_ (checkPositive n) cons
262+ if DefaultEliminator `elem` opts
260− if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty
263+ then evalStateT (elabEliminator params n t dcons info) Map.empty
261− else return ()
264+ else return ()
262 where
265 where
263 checkDefinedAs fc n t ctxt
266 checkDefinedAs fc n t ctxt
264 = case lookupDef n ctxt of
267 = case lookupDef n ctxt of
@@ -322,7 +325,7 @@ type EliminatorState = StateT (Map.Map String Int) Idris
322
325
323-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
326-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
324elabEliminator :: [Int] -> Name -> PTerm ->
327elabEliminator :: [Int] -> Name -> PTerm ->
325− [(String, [(Name, String)], Name, PTerm, FC, [Name])] ->
328+ [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->
326 ElabInfo -> EliminatorState ()
329 ElabInfo -> EliminatorState ()
327elabEliminator paramPos n ty cons info = do
330elabEliminator paramPos n ty cons info = do
328 elimLog $ "Elaborating eliminator"
331 elimLog $ "Elaborating eliminator"
@@ -339,7 +342,7 @@ elabEliminator paramPos n ty cons info = do
339 let motiveConstr = [(motiveName, expl, motive)]
342 let motiveConstr = [(motiveName, expl, motive)]
340 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))
343 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))
341 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))
344 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))
342− let eliminatorTyDecl = PTy (show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy
345+ let eliminatorTyDecl = PTy (parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy
343 let clauseConsElimArgs = map getPiName consTerms
346 let clauseConsElimArgs = map getPiName consTerms
344 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
347 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
345 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
348 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
@@ -488,7 +491,7 @@ elabEliminator paramPos n ty cons info = do
488 splitArgPms _ = ([],[])
491 splitArgPms _ = ([],[])
489
492
490
493
491− implicitIndexes :: (String, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
494+ implicitIndexes :: (Docstring, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
492 implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do
495 implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do
493 i <- State.lift getIState
496 i <- State.lift getIState
494 implargs' <- case lookupCtxt cnm (idris_implicits i) of
497 implargs' <- case lookupCtxt cnm (idris_implicits i) of
@@ -503,7 +506,7 @@ elabEliminator paramPos n ty cons info = do
503 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
506 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
504 _ -> return implargs
507 _ -> return implargs
505
508
506− extractConsTerm :: (String, [(Name, String)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
509+ extractConsTerm :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
507 extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do
510 extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do
508 let cons' = replaceParams paramPos generalParameters ty
511 let cons' = replaceParams paramPos generalParameters ty
509 let (args, resTy) = splitPi cons'
512 let (args, resTy) = splitPi cons'
@@ -539,7 +542,7 @@ elabEliminator paramPos n ty cons info = do
539 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
542 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
540 convertImplPi _ = Nothing
543 convertImplPi _ = Nothing
541
544
542− generateEliminatorClauses :: (String, [(Name, String)], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
545+ generateEliminatorClauses :: (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
543 generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do
546 generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do
544 let cons' = replaceParams paramPos generalParameters ty
547 let cons' = replaceParams paramPos generalParameters ty
545 let (args, resTy) = splitPi cons'
548 let (args, resTy) = splitPi cons'
@@ -561,7 +564,7 @@ elabEliminator paramPos n ty cons info = do
561
564
562elabPrims :: Idris ()
565elabPrims :: Idris ()
563elabPrims = do mapM_ (elabDecl EAll toplevel)
566elabPrims = do mapM_ (elabDecl EAll toplevel)
564− (map (\(opt, decl) -> PData "" [] defaultSyntax (fileFC "builtin") opt decl)
567+ (map (\(opt, decl) -> PData emptyDocstring [] defaultSyntax (fileFC "builtin") opt decl)
565 (zip
568 (zip
566 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
569 [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
567 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))
570 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))
@@ -665,7 +668,7 @@ elabProvider info syn fc what n ty tm
665 Provide tm
668 Provide tm
666 | what `elem` [ProvTerm, ProvAny] ->
669 | what `elem` [ProvTerm, ProvAny] ->
667 do -- Finally add a top-level definition of the provided term
670 do -- Finally add a top-level definition of the provided term
668− elabType info syn "" [] fc [] n ty
671+ elabType info syn emptyDocstring [] fc [] n ty
669 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]
672 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]
670 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
673 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
671 | otherwise ->
674 | otherwise ->
@@ -673,7 +676,7 @@ elabProvider info syn fc what n ty tm
673 Postulate
676 Postulate
674 | what `elem` [ProvPostulate, ProvAny] ->
677 | what `elem` [ProvPostulate, ProvAny] ->
675 do -- Add the postulate
678 do -- Add the postulate
676− elabPostulate info syn "Provided postulate" fc [] n ty
679+ elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n ty
677 logLvl 3 $ "Elaborated provided postulate " ++ show n
680 logLvl 3 $ "Elaborated provided postulate " ++ show n
678 | otherwise ->
681 | otherwise ->
679 ierror . Msg $ "Attempted to provide a postulate where a term was expected."
682 ierror . Msg $ "Attempted to provide a postulate where a term was expected."
@@ -724,8 +727,8 @@ elabTransform info fc safe lhs_in rhs_in
724 addIBC (IBCTrans (clhs_tm, crhs_tm))
727 addIBC (IBCTrans (clhs_tm, crhs_tm))
725
728
726
729
727−elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
730+elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->
728− PTerm -> String -> Name -> PTerm -> Idris ()
731+ PTerm -> Docstring -> Name -> PTerm -> Idris ()
729elabRecord info syn doc fc tyn ty cdoc cn cty
732elabRecord info syn doc fc tyn ty cdoc cn cty
730 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])
733 = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])
731 cty' <- implicit syn cn cty
734 cty' <- implicit syn cn cty
@@ -797,7 +800,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
797
800
798 mkProj recty substs cimp ((pn_in, pty), pos)
801 mkProj recty substs cimp ((pn_in, pty), pos)
799 = do let pn = expandNS syn pn_in
802 = do let pn = expandNS syn pn_in
800− let pfnTy = PTy "" [] defaultSyntax fc [] pn
803+ let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn
801 (PPi expl rec recty
804 (PPi expl rec recty
802 (substMatches substs pty))
805 (substMatches substs pty))
803 let pls = repeat Placeholder
806 let pls = repeat Placeholder
@@ -818,7 +821,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
818 let valname = sMN 0 "updateval"
821 let valname = sMN 0 "updateval"
819 let pt = k (PPi expl pn pty
822 let pt = k (PPi expl pn pty
820 (PPi expl rec recty recty))
823 (PPi expl rec recty recty))
821− let pfnTy = PTy "" [] defaultSyntax fc [] setname pt
824+ let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt
822 let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]
825 let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]
823 let lhsArgs = pls
826 let lhsArgs = pls
824 let rhsArgs = take pos pls ++ (PRef fc valname) :
827 let rhsArgs = take pos pls ++ (PRef fc valname) :
@@ -834,7 +837,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
834 return (pn, pfnTy, PClauses fc [] setname [pclause])
837 return (pn, pfnTy, PClauses fc [] setname [pclause])
835
838
836elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
839elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
837− (String, [(Name, String)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)
840+ (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)
838elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
841elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
839 = do checkUndefined fc n
842 = do checkUndefined fc n
840 ctxt <- getContext
843 ctxt <- getContext
@@ -1166,7 +1169,7 @@ elabPE info fc caller r =
1166 (map (\ (lhs, rhs) ->
1169 (map (\ (lhs, rhs) ->
1167 (showTmImpls lhs ++ " = " ++
1170 (showTmImpls lhs ++ " = " ++
1168 showTmImpls rhs)) pats)
1171 showTmImpls rhs)) pats)
1169− elabType info defaultSyntax "" [] fc opts newnm specTy
1172+ elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy
1170 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats
1173 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats
1171 elabClauses info fc opts newnm def
1174 elabClauses info fc opts newnm def
1172 logLvl 2 $ "Specialised " ++ show newnm)
1175 logLvl 2 $ "Specialised " ++ show newnm)
@@ -1725,7 +1728,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1725
1728
1726data MArgTy = IA | EA | CA deriving Show
1729data MArgTy = IA | EA | CA deriving Show
1727
1730
1728−elabClass :: ElabInfo -> SyntaxInfo -> String ->
1731+elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->
1729 FC -> [PTerm] ->
1732 FC -> [PTerm] ->
1730 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
1733 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
1731elabClass info syn doc fc constraints tn ps ds
1734elabClass info syn doc fc constraints tn ps ds
@@ -1752,7 +1755,7 @@ elabClass info syn doc fc constraints tn ps ds
1752 let cty = impbind ps $ conbind constraints
1755 let cty = impbind ps $ conbind constraints
1753 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
1756 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
1754 constraint
1757 constraint
1755− let cons = [("", [], cn, cty, fc, [])]
1758+ let cons = [(emptyDocstring, [], cn, cty, fc, [])]
1756 let ddecl = PDatadecl tn tty cons
1759 let ddecl = PDatadecl tn tty cons
1757 logLvl 5 $ "Class data " ++ show (showDImp True ddecl)
1760 logLvl 5 $ "Class data " ++ show (showDImp True ddecl)
1758 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc [] fc [] ddecl
1761 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
1807 case lookup n mtys of
1810 case lookup n mtys of
1808 Just (syn, o, ty) -> do let ty' = insertConstraint c ty
1811 Just (syn, o, ty) -> do let ty' = insertConstraint c ty
1809 let ds = map (decorateid defaultdec)
1812 let ds = map (decorateid defaultdec)
1810− [PTy "" [] syn fc [] n ty',
1813+ [PTy emptyDocstring [] syn fc [] n ty',
1811 PClauses fc (o ++ opts) n cs]
1814 PClauses fc (o ++ opts) n cs]
1812 iLOG (show ds)
1815 iLOG (show ds)
1813 return (n, ((defaultdec n, ds!!1), ds))
1816 return (n, ((defaultdec n, ds!!1), ds))
@@ -1845,7 +1848,7 @@ elabClass info syn doc fc constraints tn ps ds
1845 addInstance False conn' cfn
1848 addInstance False conn' cfn
1846 addIBC (IBCInstance False conn' cfn)
1849 addIBC (IBCInstance False conn' cfn)
1847-- iputStrLn ("Added " ++ show (conn, cfn, ty))
1850-- iputStrLn ("Added " ++ show (conn, cfn, ty))
1848− return [PTy "" [] syn fc [] cfn ty,
1851+ return [PTy emptyDocstring [] syn fc [] cfn ty,
1849 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
1852 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]
1850
1853
1851 -- Generate a top level function which looks up a method in a given
1854 -- 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
1909 let constraint = PApp fc (PRef fc n) (map pexp ps)
1912 let constraint = PApp fc (PRef fc n) (map pexp ps)
1910 let iname = mkiname n ps expn
1913 let iname = mkiname n ps expn
1911 when (what /= EDefns) $ do
1914 when (what /= EDefns) $ do
1912− nty <- elabType' True info syn "" [] fc [] iname t
1915+ nty <- elabType' True info syn emptyDocstring [] fc [] iname t
1913 -- if the instance type matches any of the instances we have already,
1916 -- if the instance type matches any of the instances we have already,
1914 -- and it's not a named instance, then it's overlapping, so report an error
1917 -- and it's not a named instance, then it's overlapping, so report an error
1915 case expn of
1918 case expn of
@@ -2061,7 +2064,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
2061 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
2064 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns
2062 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
2065 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
2063
2066
2064− mkTyDecl (n, op, t, _) = PTy "" [] syn fc op n t
2067+ mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t
2065
2068
2066 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)
2069 conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)
2067 conbind [] x = x
2070 conbind [] x = x
@@ -2308,7 +2311,7 @@ inferredDiff fc inf user =
2308-- | Check a PTerm against documentation and ensure that every documented
2311-- | Check a PTerm against documentation and ensure that every documented
2309-- argument actually exists. This must be run _after_ implicits have been
2312-- argument actually exists. This must be run _after_ implicits have been
2310-- found, or it will give spurious errors.
2313-- found, or it will give spurious errors.
2311−checkDocs :: FC -> [(Name, String)] -> PTerm -> Idris ()
2314+checkDocs :: FC -> [(Name, Docstring)] -> PTerm -> Idris ()
2312checkDocs fc args tm = cd (Map.fromList args) tm
2315checkDocs fc args tm = cd (Map.fromList args) tm
2313 where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc
2316 where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc
2314 cd as _ | Map.null as = return ()
2317 cd as _ | Map.null as = return ()
src/Idris/IBC.hs+85−2
@@ -9,6 +9,9 @@ import Idris.AbsSyntax
9import Idris.Imports
9import Idris.Imports
10import Idris.Error
10import Idris.Error
11import Idris.Delaborate
11import Idris.Delaborate
12+import Idris.Docstrings
13+
14+import qualified Cheapskate.Types as CT
12
15
13import Data.Binary
16import Data.Binary
14import Data.Vector.Binary
17import Data.Vector.Binary
@@ -52,7 +55,7 @@ data IBCFile = IBCFile { ver :: Word8,
52 ibc_flags :: [(Name, [FnOpt])],
55 ibc_flags :: [(Name, [FnOpt])],
53 ibc_cg :: [(Name, CGInfo)],
56 ibc_cg :: [(Name, CGInfo)],
54 ibc_defs :: [(Name, Def)],
57 ibc_defs :: [(Name, Def)],
55− ibc_docstrings :: [(Name, (String, [(Name, String)]))],
58+ ibc_docstrings :: [(Name, (Docstring, [(Name, Docstring)]))],
56 ibc_transforms :: [(Term, Term)],
59 ibc_transforms :: [(Term, Term)],
57 ibc_errRev :: [(Term, Term)],
60 ibc_errRev :: [(Term, Term)],
58 ibc_coercions :: [Name],
61 ibc_coercions :: [Name],
@@ -405,7 +408,7 @@ pDefs syms ds
405 update (Proj t i) = Proj (update t) i
408 update (Proj t i) = Proj (update t) i
406 update t = t
409 update t = t
407
410
408−pDocs :: [(Name, (String, [(Name, String)]))] -> Idris ()
411+pDocs :: [(Name, (Docstring, [(Name, Docstring)]))] -> Idris ()
409pDocs ds = mapM_ (\ (n, a) -> addDocStr n (fst a) (snd a)) ds
412pDocs ds = mapM_ (\ (n, a) -> addDocStr n (fst a) (snd a)) ds
410
413
411pAccess :: [(Name, Accessibility)] -> Idris ()
414pAccess :: [(Name, Accessibility)] -> Idris ()
@@ -461,6 +464,86 @@ pMetavars ns = do i <- getIState
461 putIState $ i { idris_metavars = Data.List.reverse ns
464 putIState $ i { idris_metavars = Data.List.reverse ns
462 ++ idris_metavars i }
465 ++ idris_metavars i }
463
466
467+----- For Cheapskate
468+
469+instance Binary CT.Doc where
470+ put (CT.Doc opts lines) = do put opts ; put lines
471+ get = do opts <- get
472+ lines <- get
473+ return (CT.Doc opts lines)
474+
475+instance Binary CT.Options where
476+ put (CT.Options x1 x2 x3 x4) = do put x1 ; put x2 ; put x3 ; put x4
477+ get = do x1 <- get
478+ x2 <- get
479+ x3 <- get
480+ x4 <- get
481+ return (CT.Options x1 x2 x3 x4)
482+
483+instance Binary CT.Block where
484+ put (CT.Para lines) = do putWord8 0 ; put lines
485+ put (CT.Header i lines) = do putWord8 1 ; put i ; put lines
486+ put (CT.Blockquote bs) = do putWord8 2 ; put bs
487+ put (CT.List b t xs) = do putWord8 3 ; put b ; put t ; put xs
488+ put (CT.CodeBlock attr txt) = do putWord8 4 ; put attr ; put txt
489+ put (CT.HtmlBlock txt) = do putWord8 5 ; put txt
490+ put CT.HRule = putWord8 6
491+ get = do i <- getWord8
492+ case i of
493+ 0 -> fmap CT.Para get
494+ 1 -> liftM2 CT.Header get get
495+ 2 -> fmap CT.Blockquote get
496+ 3 -> liftM3 CT.List get get get
497+ 4 -> liftM2 CT.CodeBlock get get
498+ 5 -> liftM CT.HtmlBlock get
499+ 6 -> return CT.HRule
500+
501+instance Binary CT.Inline where
502+ put (CT.Str txt) = do putWord8 0 ; put txt
503+ put CT.Space = putWord8 1
504+ put CT.SoftBreak = putWord8 2
505+ put CT.LineBreak = putWord8 3
506+ put (CT.Emph xs) = putWord8 4 >> put xs
507+ put (CT.Strong xs) = putWord8 5 >> put xs
508+ put (CT.Code xs) = putWord8 6 >> put xs
509+ put (CT.Link a b c) = putWord8 7 >> put a >> put b >> put c
510+ put (CT.Image a b c) = putWord8 8 >> put a >> put b >> put c
511+ put (CT.Entity a) = putWord8 9 >> put a
512+ put (CT.RawHtml x) = putWord8 10 >> put x
513+ get = do i <- getWord8
514+ case i of
515+ 0 -> liftM CT.Str get
516+ 1 -> return CT.Space
517+ 2 -> return CT.SoftBreak
518+ 3 -> return CT.LineBreak
519+ 4 -> liftM CT.Emph get
520+ 5 -> liftM CT.Strong get
521+ 6 -> liftM CT.Code get
522+ 7 -> liftM3 CT.Link get get get
523+ 8 -> liftM3 CT.Image get get get
524+ 9 -> liftM CT.Entity get
525+ 10 -> liftM CT.RawHtml get
526+
527+instance Binary CT.ListType where
528+ put (CT.Bullet c) = putWord8 0 >> put c
529+ put (CT.Numbered nw i) = putWord8 1 >> put nw >> put i
530+ get = do i <- getWord8
531+ case i of
532+ 0 -> liftM CT.Bullet get
533+ 1 -> liftM2 CT.Numbered get get
534+
535+instance Binary CT.CodeAttr where
536+ put (CT.CodeAttr a b) = put a >> put b
537+ get = liftM2 CT.CodeAttr get get
538+
539+instance Binary CT.NumWrapper where
540+ put (CT.PeriodFollowing) = putWord8 0
541+ put (CT.ParenFollowing) = putWord8 1
542+ get = do i <- getWord8
543+ case i of
544+ 0 -> return CT.PeriodFollowing
545+ 1 -> return CT.ParenFollowing
546+
464----- Generated by 'derive'
547----- Generated by 'derive'
465
548
466instance Binary SizeChange where
549instance Binary SizeChange where
src/Idris/ParseData.hs+8−6
@@ -20,6 +20,8 @@ import Idris.DSL
20import Idris.Core.TT
20import Idris.Core.TT
21import Idris.Core.Evaluate
21import Idris.Core.Evaluate
22
22
23+import Idris.Docstrings
24+
23import Control.Applicative
25import Control.Applicative
24import Control.Monad
26import Control.Monad
25import Control.Monad.State.Strict
27import Control.Monad.State.Strict
@@ -41,7 +43,7 @@ Record ::=
41-}
43-}
42record :: SyntaxInfo -> IdrisParser PDecl
44record :: SyntaxInfo -> IdrisParser PDecl
43record syn = do (doc, acc) <- try (do
45record syn = do (doc, acc) <- try (do
44− doc <- option ("", []) docComment
46+ doc <- option noDocs docComment
45 acc <- optional accessibility
47 acc <- optional accessibility
46 reserved "record"
48 reserved "record"
47 return (doc, acc))
49 return (doc, acc))
@@ -103,7 +105,7 @@ SimpleConstructorList ::=
103-}
105-}
104data_ :: SyntaxInfo -> IdrisParser PDecl
106data_ :: SyntaxInfo -> IdrisParser PDecl
105data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do
107data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do
106− (doc, argDocs) <- option ("", []) docComment
108+ (doc, argDocs) <- option noDocs docComment
107 pushIndent
109 pushIndent
108 acc <- optional accessibility
110 acc <- optional accessibility
109 elim <- dataOpts []
111 elim <- dataOpts []
@@ -160,9 +162,9 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do
160{- | Parses a type constructor declaration
162{- | Parses a type constructor declaration
161 Constructor ::= DocComment? FnName TypeSig;
163 Constructor ::= DocComment? FnName TypeSig;
162-}
164-}
163−constructor :: SyntaxInfo -> IdrisParser (String, [(Name, String)], Name, PTerm, FC, [Name])
165+constructor :: SyntaxInfo -> IdrisParser (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])
164constructor syn
166constructor syn
165− = do (doc, argDocs) <- option ("", []) docComment
167+ = do (doc, argDocs) <- option noDocs docComment
166 cn_in <- fnName; fc <- getFC
168 cn_in <- fnName; fc <- getFC
167 let cn = expandNS syn cn_in
169 let cn = expandNS syn cn_in
168 lchar ':'
170 lchar ':'
@@ -177,9 +179,9 @@ constructor syn
177{- | Parses a constructor for simple discriminative union data types
179{- | Parses a constructor for simple discriminative union data types
178 SimpleConstructor ::= FnName SimpleExpr* DocComment?
180 SimpleConstructor ::= FnName SimpleExpr* DocComment?
179-}
181-}
180−simpleConstructor :: SyntaxInfo -> IdrisParser (String, [(Name, String)], Name, [PTerm], FC, [Name])
182+simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring, [(Name, Docstring)], Name, [PTerm], FC, [Name])
181simpleConstructor syn
183simpleConstructor syn
182− = do doc <- option ("", []) (try docComment)
184+ = do doc <- option noDocs (try docComment)
183 cn_in <- fnName
185 cn_in <- fnName
184 let cn = expandNS syn cn_in
186 let cn = expandNS syn cn_in
185 fc <- getFC
187 fc <- getFC
src/Idris/ParseHelpers.hs+10−8
@@ -17,6 +17,7 @@ import Idris.AbsSyntax
17import Idris.Core.TT
17import Idris.Core.TT
18import Idris.Core.Evaluate
18import Idris.Core.Evaluate
19import Idris.Delaborate (pprintErr)
19import Idris.Delaborate (pprintErr)
20+import Idris.Docstrings
20
21
21import qualified Util.Pretty as Pretty (text)
22import qualified Util.Pretty as Pretty (text)
22
23
@@ -142,25 +143,26 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())
142{-| Parses a documentation comment (similar to haddoc) given a marker character
143{-| Parses a documentation comment (similar to haddoc) given a marker character
143
144
144@
145@
145− DocComment_t ::= '--' DocCommentMarker_t ~EOL_t* EOL_t
146+ DocComment_t ::= '|||' ~EOL_t* EOL_t
146− | '{ -' DocCommentMarket_t ~'- }'* '- }'
147 ;
147 ;
148@
148@
149 -}
149 -}
150−docComment :: IdrisParser (String, [(Name, String)])
150+docComment :: IdrisParser (Docstring, [(Name, Docstring)])
151docComment = do dc <- pushIndent *> docCommentLine
151docComment = do dc <- pushIndent *> docCommentLine
152 rest <- many (indented docCommentLine)
152 rest <- many (indented docCommentLine)
153 args <- many (indented argDocCommentLine)
153 args <- many (indented argDocCommentLine)
154 popIndent
154 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)
156
157
157 where docCommentLine :: MonadicParsing m => m String
158 where docCommentLine :: MonadicParsing m => m String
158 docCommentLine = try (do string "|||"
159 docCommentLine = try (do string "|||"
159− many (satisfy isSpace)
160+ many (satisfy (==' '))
160− first <- satisfy (\c -> not (isEol c || c == '@'))
161+ contents <- option "" (do first <- satisfy (\c -> not (isEol c || c == '@'))
161− res <- many (satisfy (not . isEol))
162+ res <- many (satisfy (not . isEol))
163+ return $ first:res)
162 eol ; someSpace
164 eol ; someSpace
163− return (first:res))-- ++ concat rest))
165+ return contents)-- ++ concat rest))
164 <?> ""
166 <?> ""
165 argDocCommentLine = do string "|||"
167 argDocCommentLine = do string "|||"
166 many (satisfy isSpace)
168 many (satisfy isSpace)
src/Idris/ParseOps.hs−1
@@ -59,7 +59,6 @@ binary name f = Infix (do fc <- getFC
59 indentPropHolds gtProp
59 indentPropHolds gtProp
60 reservedOp name
60 reservedOp name
61 indentPropHolds gtProp
61 indentPropHolds gtProp
62− doc <- option ("", []) docComment
63 return (f fc))
62 return (f fc))
64
63
65-- | Prefix operator
64-- | Prefix operator
src/Idris/Parser.hs+7−5
@@ -35,6 +35,8 @@ import Idris.ParseOps
35import Idris.ParseExpr
35import Idris.ParseExpr
36import Idris.ParseData
36import Idris.ParseData
37
37
38+import Idris.Docstrings
39+
38import Paths_idris
40import Paths_idris
39
41
40import Util.DynamicLinker
42import Util.DynamicLinker
@@ -315,7 +317,7 @@ fnDecl' syn = checkFixity $
315 do (doc, fc, opts', n, acc) <- try (do
317 do (doc, fc, opts', n, acc) <- try (do
316 pushIndent
318 pushIndent
317 ist <- get
319 ist <- get
318− doc <- option ("", []) docComment
320+ doc <- option noDocs docComment
319 ist <- get
321 ist <- get
320 let initOpts = if default_total ist
322 let initOpts = if default_total ist
321 then [TotalFn]
323 then [TotalFn]
@@ -413,7 +415,7 @@ Postulate ::=
413@
415@
414-}
416-}
415postulate :: SyntaxInfo -> IdrisParser PDecl
417postulate :: SyntaxInfo -> IdrisParser PDecl
416−postulate syn = do doc <- try $ do doc <- option ("", []) docComment
418+postulate syn = do doc <- try $ do doc <- option noDocs docComment
417 pushIndent
419 pushIndent
418 reserved "postulate"
420 reserved "postulate"
419 return doc
421 return doc
@@ -561,7 +563,7 @@ Class ::=
561-}
563-}
562class_ :: SyntaxInfo -> IdrisParser [PDecl]
564class_ :: SyntaxInfo -> IdrisParser [PDecl]
563class_ syn = do (doc, acc) <- try (do
565class_ syn = do (doc, acc) <- try (do
564− doc <- option ("", []) docComment
566+ doc <- option noDocs docComment
565 acc <- optional accessibility
567 acc <- optional accessibility
566 return (doc, acc))
568 return (doc, acc))
567 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName
569 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- fnName
@@ -1003,8 +1005,8 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st
1003 mapM_ (addNameHint ty') ns
1005 mapM_ (addNameHint ty') ns
1004 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1006 mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]
1005 <|> do try (lchar '%' *> reserved "error_handlers")
1007 <|> do try (lchar '%' *> reserved "error_handlers")
1006− fn <- iName []
1008+ fn <- fnName
1007− arg <- iName []
1009+ arg <- fnName
1008 ns <- sepBy1 name (lchar ',')
1010 ns <- sepBy1 name (lchar ',')
1009 return [PDirective (do fn' <- disambiguate fn
1011 return [PDirective (do fn' <- disambiguate fn
1010 ns' <- mapM disambiguate ns
1012 ns' <- mapM disambiguate ns