6a011d8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add docstrings to internally defined types

Add docstrings to the type constructors and constructors for (=), (,), _|_, and (). Some of these are not easy to look up from :doc, but they show up in tooltips in certain IDEs, and :doc should be improved to make them easier to find.

commit6a011d8b208899fa2021678902cfc852808f8b21 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 21 Apr 2014, 06:52 (13 years ago) parent8bf2f8a

2 files changed+55−16

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+50−13 src/Idris/ElabDecls.hs+5−3

src/Idris/AbsSyntaxTree.hs+50−13

@@ -986,40 +986,77 @@ primNames = [unitTy, unitCon,

986986 falseTy, pairTy, pairCon,

987987 eqTy, eqCon, inferTy, inferCon]

988988

989+unitDoc = parseDocstring . T.pack $ "The canonical single-element type, also known as the trivially true proposition."

989990unitTy = sMN 0 "__Unit"

990991unitCon = sMN 0 "__II"

991992unitDecl = PDatadecl unitTy PType

992− [(emptyDocstring, [], unitCon, PRef bi unitTy, bi, [])]

993+ [(parseDocstring . T.pack $ "The trivial constructor for `()`. ", [], unitCon, PRef bi unitTy, bi, [])]

993994unitOpts = [DefaultEliminator]

994995

996+falseDoc = parseDocstring . T.pack $

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

998+ "\n\n" ++

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

1000+ "of type `_|_` in scope."

9951001falseTy = sMN 0 "__False"

9961002falseDecl = PDatadecl falseTy PType []

9971003falseOpts = []

9981004

1005+pairDoc = parseDocstring . T.pack $ "The non-dependent pair type, also known as conjunction."

9991006pairTy = sMN 0 "__Pair"

10001007pairCon = sMN 0 "__MkPair"

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

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

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

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

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

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

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

1009+ [(pairConDoc, pairConParamDoc,

1010+ pairCon, PPi impl (n "A") PType (

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

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

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

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

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

10081016 where n a = sMN 0 a

1017+ pairConDoc = parseDocstring . T.pack $ "A pair of elements"

1018+ pairConParamDoc = [(n "a", parseDocstring . T.pack $ "the left element of the pair"),

1019+ (n "b", parseDocstring . T.pack $ "the right element of the pair")]

10091020pairOpts = []

1021+pairParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left elements in the pair"),

1022+ (n "B", parseDocstring . T.pack $ "the type of the left elements in the pair")]

1023+ where n a = sMN 0 a

10101024

10111025eqTy = sUN "="

10121026eqCon = sUN "refl"

1027+eqDoc = parseDocstring . T.pack $

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

1029+ "\n\n" ++

1030+ "**Note**: Idris's equality type is _heterogeneous_, which means that it " ++

1031+ "is possible to state equalities between values of potentially different " ++

1032+ "types. This is sometimes referred to in the literature as \"John Major\" " ++

1033+ "equality." ++

1034+ "\n\n" ++

1035+ "Thus, if Idris can't infer the type of one side of the equality, then " ++

1036+ "you may need to annotate it. See the function `the`."

1037+

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

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

10151040 PType)

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

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

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

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

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

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

1041+ [(reflDoc, reflParamDoc,

1042+ eqCon, PPi impl (n "A") PType (

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

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

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

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

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

10221048 where n a = sMN 0 a

1049+ reflDoc = parseDocstring . T.pack $

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

1051+ "shown that both sides are in fact equal."

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

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

1054+

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

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

1057+ ]

1058+ where n a = sMN 0 a

1059+

10231060eqOpts = []

10241061

10251062elimName = sUN "__Elim"

src/Idris/ElabDecls.hs+5−3

@@ -605,10 +605,12 @@ elabEliminator paramPos n ty cons info = do

605605

606606elabPrims :: Idris ()

607607elabPrims = do mapM_ (elabDecl EAll toplevel)

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

609− (zip

608+ (map (\(opt, decl, docs, argdocs) -> PData docs argdocs defaultSyntax (fileFC "builtin") opt decl)

609+ (zip4

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

611− [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

611+ [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]

612+ [emptyDocstring, unitDoc, falseDoc, pairDoc, eqDoc]

613+ [[], [], [], pairParamDoc, eqParamDoc]))

612614 addNameHint eqTy (sUN "prf")

613615 elabDecl EAll toplevel elimDecl

614616 mapM_ elabPrim primitives