a726ae7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1155 from paulkoerbitz/fix/1047-repl-doc-for-typeclasses

a726ae7David Christiansen12 years ago

CONTRIBUTORS+1

compare with master

unifiedsplit

@@ -11,6 +11,7 @@ Simon Fowler

11Google

12Cezar Ionescu

13Irene Knapp

14+Paul Koerbitz

14Shea Levy

15Shea Levy

15Mathnerd314

16Mathnerd314

16Hannes Mehnert

17Hannes Mehnert

src/Idris/AbsSyntaxTree.hs−1

@@ -285,7 +285,6 @@ data Command = Quit

285 | HNF PTerm

286 | TestInline PTerm

287 | Defn Name

288− | Info Name

289 | Missing Name

288 | Missing Name

290 | DynamicLink FilePath

289 | DynamicLink FilePath

291 | ListDynamic

290 | ListDynamic

src/Idris/Docs.hs+44−9

@@ -27,6 +27,8 @@ data Docs = FunDoc FunDoc

27 [FunDoc] -- data constructor docs

28 | ClassDoc Name Docstring -- class docs

29 [FunDoc] -- method docs

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

31+ [PTerm] -- instances

30 deriving Show

32 deriving Show

32showDoc d | nullDocstring d = empty

34showDoc d | nullDocstring d = empty

@@ -66,16 +68,47 @@ pprintFD imp (FD n doc args ty f)

66 showArgs [] _ = []

68 showArgs [] _ = []

69−

71+pprintDocs :: Bool -> Docs -> Doc OutputAnnotation

70pprintDocs imp (FunDoc d) = pprintFD imp d

72pprintDocs imp (FunDoc d) = pprintFD imp d

71pprintDocs imp (DataDoc t args)

73pprintDocs imp (DataDoc t args)

72 = text "Data type" <+> pprintFD imp t <$>

74 = text "Data type" <+> pprintFD imp t <$>

73 nest 4 (text "Constructors:" <> line <>

75 nest 4 (text "Constructors:" <> line <>

74 vsep (map (pprintFD imp) args))

76 vsep (map (pprintFD imp) args))

75−pprintDocs imp (ClassDoc n doc meths)

77+pprintDocs imp (ClassDoc n doc meths params instances)

76− = text "Type class" <+> prettyName imp [] n <$> -- parameters?

78+ = nest 4 (text "Type class" <+> prettyName imp [] n <>

79+ if nullDocstring doc then empty else line <> renderDocstring doc)

80+ <> line <$>

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

82+ <> line <$>

77 nest 4 (text "Methods:" <$>

83 nest 4 (text "Methods:" <$>

78− vsep (map (pprintFD imp) meths))

84+ vsep (map (pprintFD imp) meths))

85+ <$>

86+ nest 4 (text "Instances:" <$>

87+ vsep (if null instances' then [text "<no instances>"]

88+ else map dumpInstance instances'))

89+ <>

90+ if null subclasses then empty

91+ else line <$> nest 4 (text "Subclasses:" <$>

92+ vsep (map (dumpInstance . remConstraint) subclasses))

93+ where

94+ params' = map (\x -> (fst x, False)) params

95+

96+ dumpInstance :: PTerm -> Doc OutputAnnotation

97+ dumpInstance = pprintPTerm imp params' []

98+

99+ remConstraint (PPi (Constraint _ _) _ tm _) = tm

100+ remConstraint (PPi x y z pt) = PPi x y z (remConstraint pt)

101+ remConstraint p = p

102+

103+ hasConstraint (PPi (Constraint _ _) _ _ _) = True

104+ hasConstraint (PPi _ _ _ pt) = hasConstraint pt

105+ hasConstraint _ = False

106+

107+ (subclasses, instances') = partition hasConstraint instances

108+

109+ prettyParameters = if any (isJust . snd) params

110+ then vsep (map (\(n,md) -> prettyName False params' n <+> maybe empty showDoc md) params)

111+ else hsep (punctuate comma (map (prettyName False params' . fst) params))

112

80getDocs :: Name -> Idris Docs

113getDocs :: Name -> Idris Docs

81getDocs n

114getDocs n

@@ -96,11 +129,13 @@ docData n ti

96docClass :: Name -> ClassInfo -> Idris Docs

129docClass :: Name -> ClassInfo -> Idris Docs

97docClass n ci

130docClass n ci

98 = do i <- getIState

131 = do i <- getIState

132+ ctxt <- getContext

99− let docstr = case lookupCtxt n (idris_docstrings i) of

133+ let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

100− [str] -> fst str

101− _ -> emptyDocstring

134+ docstr = maybe emptyDocstring fst docStrings

135+ params = map (\pn -> (pn, docStrings >>= (lookup pn . snd))) (class_params ci)

136+ instances = map (delabTy i) (class_instances ci)

102− mdocs <- mapM docFun (map fst (class_methods ci))

137+ mdocs <- mapM (docFun .fst) (class_methods ci)

103− return (ClassDoc n docstr mdocs)

138+ return $ ClassDoc n docstr mdocs params instances

104

139

105docFun :: Name -> Idris FunDoc

140docFun :: Name -> Idris FunDoc

106docFun n

141docFun n

src/Idris/Help.hs−1

@@ -35,7 +35,6 @@ help =

35 ([":apropos"], NoArg, "Search names, types, and documentation"),

36 ([":whocalls", ":wc"], NameArg, "List the callers of some name"),

37 ([":callswho", ":cw"], NameArg, "List the callees of some name"),

38− ([":i", ":info"], NameArg, "Display information about a type class"),

39 ([":total"], NameArg, "Check the totality of a name"),

38 ([":total"], NameArg, "Check the totality of a name"),

40 ([":r",":reload"], NoArg, "Reload current file"),

39 ([":r",":reload"], NoArg, "Reload current file"),

41 ([":l",":load"], FileArg, "Load a new file"),

40 ([":l",":load"], FileArg, "Load a new file"),

src/Idris/IdrisDoc.hs+9−9

@@ -157,9 +157,9 @@ removeOrphans list =

157 let children = S.fromList $ concatMap (names . (\(_, d, _) -> d)) list

158 in filter ((`S.notMember` children) . (\(n, _, _) -> n)) list

159

160− where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds

160+ where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds

161− names (Just (ClassDoc _ _ fds)) = map (\(FD n _ _ _ _) -> n) fds

161+ names (Just (ClassDoc _ _ fds _ _)) = map (\(FD n _ _ _ _) -> n) fds

162− names _ = []

162+ names _ = []

163

164-- | Whether a Name names something which should be documented

165filterName :: Name -- ^ Name to check

@@ -207,11 +207,11 @@ referredNss (n, Just d, _) =

207 names = concatMap (extractPTermNames) ts

208 in S.map getNs $ S.fromList names

209

210− where getFunDocs (FunDoc f) = [f]

210+ where getFunDocs (FunDoc f) = [f]

211− getFunDocs (DataDoc f fs) = f:fs

211+ getFunDocs (DataDoc f fs) = f:fs

212− getFunDocs (ClassDoc _ _ fs) = fs

212+ getFunDocs (ClassDoc _ _ fs _ _) = fs

213− types (FD _ _ args t _) = t:(map second args)

213+ types (FD _ _ args t _) = t:(map second args)

214− second (_, x, _, _) = x

214+ second (_, x, _, _) = x

215

216

217-- | Returns an NsDict of containing all known namespaces and their contents

@@ -553,7 +553,7 @@ createOtherDoc :: IState -- ^ Needed to determine the types of names

553 -> H.Html -- ^ Resulting HTML

554createOtherDoc ist (FunDoc fd) = createFunDoc ist fd

555

556−createOtherDoc ist (ClassDoc n docstring fds) = do

556+createOtherDoc ist (ClassDoc n docstring fds _ _) = do

557 H.dt ! (A.id $ toValue $ show n) $ do

558 H.span ! class_ "word" $ do "class"; nbsp

559 H.span ! class_ "name type"

src/Idris/REPL.hs−32

@@ -386,7 +386,6 @@ ideslaveProcess fn (Defn n) = do process stdout fn (Defn n)

386ideslaveProcess fn (TotCheck n) = process stdout fn (TotCheck n)

387ideslaveProcess fn (DebugInfo n) = do process stdout fn (DebugInfo n)

388 iPrintResult ""

389−ideslaveProcess fn (Info n) = process stdout fn (Info n)

390ideslaveProcess fn (Search t) = process stdout fn (Search t)

389ideslaveProcess fn (Search t) = process stdout fn (Search t)

391ideslaveProcess fn (Spec t) = process stdout fn (Spec t)

390ideslaveProcess fn (Spec t) = process stdout fn (Spec t)

392-- RmProof and AddProof not supported!

391-- RmProof and AddProof not supported!

@@ -690,12 +689,6 @@ process h fn (DebugInfo n)

690 iputStrLn $ "Size change: " ++ show sc

689 iputStrLn $ "Size change: " ++ show sc

691 when (not (null cg')) $ do iputStrLn "Call graph:\n"

690 when (not (null cg')) $ do iputStrLn "Call graph:\n"

692 iputStrLn (show cg')

691 iputStrLn (show cg')

693−process h fn (Info n)

694− = do i <- getIState

695− case lookupCtxt n (idris_classes i) of

696− [c] -> do info <- classInfo c

697− ihRenderResult h info

698− _ -> iPrintError "Not a class"

699process h fn (Search t) = iPrintError "Not implemented"

692process h fn (Search t) = iPrintError "Not implemented"

700-- FIXME: There is far too much repetition in the cases below!

693-- FIXME: There is far too much repetition in the cases below!

701process h fn (CaseSplitAt updatefile l n)

694process h fn (CaseSplitAt updatefile l n)

@@ -1103,31 +1096,6 @@ process h fn (MakeDoc s) =

1103 Left err -> iPrintError err

1096 Left err -> iPrintError err

1104

1097

1105

1098

1106−classInfo :: ClassInfo -> Idris (Doc OutputAnnotation)

1107−classInfo ci = do ist <- getIState

1108− ctxt <- getContext

1109− return $

1110− text "Parameters:" <+>

1111− hsep (punctuate comma (map (prettyName False params') params)) <>

1112− line <> line <>

1113− text "Methods:" <> line <>

1114− indent 2 (vsep (map (dumpMethod ist) (class_methods ci))) <> line <> line <>

1115− text "Default superclass instances:" <>

1116− line <>

1117− indent 2 (vsep (map (dumpDefaultInstance ist) (class_default_superclasses ci))) <>

1118− line <>

1119− text "Instances:" <> line <>

1120− indent 2 (vsep (map (dumpInstance ist ctxt) (class_instances ci)))

1121− where dumpMethod :: IState -> (Name, (FnOpts, PTerm)) -> Doc OutputAnnotation

1122− dumpMethod ist (n, (_, t)) = prettyName False [] n <+> colon <+> pp ist t

1123− dumpDefaultInstance :: IState -> PDecl -> Doc OutputAnnotation

1124− dumpDefaultInstance ist (PInstance _ _ _ _ _ t _ _) = pp ist t

1125− dumpInstance :: IState -> Context -> Name -> Doc OutputAnnotation

1126− dumpInstance ist ctxt n = pp ist $ delabTy ist n

1127− params = class_params ci

1128− params' = zip params (repeat False)

1129− pp ist = pprintPTerm (opt_showimp (idris_options ist)) params' []

1130−

1131showTotal :: Totality -> IState -> String

1099showTotal :: Totality -> IState -> String

1132showTotal t@(Partial (Other ns)) i

1100showTotal t@(Partial (Other ns)) i

1133 = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)

1101 = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)

src/Idris/REPLParser.hs−1

@@ -59,7 +59,6 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

59 <|> try (do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t))

60 <|> try (do cmd ["u", "universes"]; eof; return Universes)

61 <|> try (do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (DebugInfo n))

62− <|> try (do cmd ["i", "info"]; n <- P.fnName; eof; return (Info n))

63 <|> try (do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n))

62 <|> try (do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n))

64 <|> try (do cmd ["dynamic"]; eof; return ListDynamic)

63 <|> try (do cmd ["dynamic"]; eof; return ListDynamic)

65 <|> try (do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l))

64 <|> try (do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l))