git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1155 from paulkoerbitz/fix/1047-repl-doc-for-typeclasses

Fix/1047 repl doc for typeclasses

commita726ae701279f4e7b4b262df292a8d64e1d7608c authorDavid Christiansen <david@davidchristiansen.dk> dateThu 1 May 2014, 17:55 (12 years ago) parent8f8a40fcc92419
7 files changed+54−53
compare with master
unifiedsplit
CONTRIBUTORS+1 src/Idris/AbsSyntaxTree.hs−1 src/Idris/Docs.hs+44−9 src/Idris/Help.hs−1 src/Idris/IdrisDoc.hs+9−9 src/Idris/REPL.hs−32 src/Idris/REPLParser.hs−1
CONTRIBUTORS+1
@@ -11,6 +11,7 @@ Simon Fowler
1111Google
1212Cezar Ionescu
1313Irene Knapp
14+Paul Koerbitz
1415Shea Levy
1516Mathnerd314
1617Hannes Mehnert
src/Idris/AbsSyntaxTree.hs−1
@@ -285,7 +285,6 @@ data Command = Quit
285285 | HNF PTerm
286286 | TestInline PTerm
287287 | Defn Name
288− | Info Name
289288 | Missing Name
290289 | DynamicLink FilePath
291290 | ListDynamic
src/Idris/Docs.hs+44−9
@@ -27,6 +27,8 @@ data Docs = FunDoc FunDoc
2727 [FunDoc] -- data constructor docs
2828 | ClassDoc Name Docstring -- class docs
2929 [FunDoc] -- method docs
30+ [(Name, Maybe Docstring)] -- parameters and their docstrings
31+ [PTerm] -- instances
3032 deriving Show
3133
3234showDoc d | nullDocstring d = empty
@@ -66,16 +68,47 @@ pprintFD imp (FD n doc args ty f)
6668 showArgs [] _ = []
6769
6870
69−
71+pprintDocs :: Bool -> Docs -> Doc OutputAnnotation
7072pprintDocs imp (FunDoc d) = pprintFD imp d
7173pprintDocs imp (DataDoc t args)
7274 = text "Data type" <+> pprintFD imp t <$>
7375 nest 4 (text "Constructors:" <> line <>
7476 vsep (map (pprintFD imp) args))
75−pprintDocs imp (ClassDoc n doc meths)
76− = text "Type class" <+> prettyName imp [] n <$> -- parameters?
77+pprintDocs imp (ClassDoc n doc meths params instances)
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 <$>
7783 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))
79112
80113getDocs :: Name -> Idris Docs
81114getDocs n
@@ -96,11 +129,13 @@ docData n ti
96129docClass :: Name -> ClassInfo -> Idris Docs
97130docClass n ci
98131 = do i <- getIState
99− let docstr = case lookupCtxt n (idris_docstrings i) of
100− [str] -> fst str
101− _ -> emptyDocstring
102− mdocs <- mapM docFun (map fst (class_methods ci))
103− return (ClassDoc n docstr mdocs)
132+ ctxt <- getContext
133+ let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i
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)
137+ mdocs <- mapM (docFun .fst) (class_methods ci)
138+ return $ ClassDoc n docstr mdocs params instances
104139
105140docFun :: Name -> Idris FunDoc
106141docFun n
src/Idris/Help.hs−1
@@ -35,7 +35,6 @@ help =
3535 ([":apropos"], NoArg, "Search names, types, and documentation"),
3636 ([":whocalls", ":wc"], NameArg, "List the callers of some name"),
3737 ([":callswho", ":cw"], NameArg, "List the callees of some name"),
38− ([":i", ":info"], NameArg, "Display information about a type class"),
3938 ([":total"], NameArg, "Check the totality of a name"),
4039 ([":r",":reload"], NoArg, "Reload current file"),
4140 ([":l",":load"], FileArg, "Load a new file"),
src/Idris/IdrisDoc.hs+9−9
@@ -157,9 +157,9 @@ removeOrphans list =
157157 let children = S.fromList $ concatMap (names . (\(_, d, _) -> d)) list
158158 in filter ((`S.notMember` children) . (\(n, _, _) -> n)) list
159159
160− where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds
161− names (Just (ClassDoc _ _ fds)) = map (\(FD n _ _ _ _) -> n) fds
162− names _ = []
160+ where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds
161+ names (Just (ClassDoc _ _ fds _ _)) = map (\(FD n _ _ _ _) -> n) fds
162+ names _ = []
163163
164164-- | Whether a Name names something which should be documented
165165filterName :: Name -- ^ Name to check
@@ -207,11 +207,11 @@ referredNss (n, Just d, _) =
207207 names = concatMap (extractPTermNames) ts
208208 in S.map getNs $ S.fromList names
209209
210− where getFunDocs (FunDoc f) = [f]
211− getFunDocs (DataDoc f fs) = f:fs
212− getFunDocs (ClassDoc _ _ fs) = fs
213− types (FD _ _ args t _) = t:(map second args)
214− second (_, x, _, _) = x
210+ where getFunDocs (FunDoc f) = [f]
211+ getFunDocs (DataDoc f fs) = f:fs
212+ getFunDocs (ClassDoc _ _ fs _ _) = fs
213+ types (FD _ _ args t _) = t:(map second args)
214+ second (_, x, _, _) = x
215215
216216
217217-- | Returns an NsDict of containing all known namespaces and their contents
@@ -553,7 +553,7 @@ createOtherDoc :: IState -- ^ Needed to determine the types of names
553553 -> H.Html -- ^ Resulting HTML
554554createOtherDoc ist (FunDoc fd) = createFunDoc ist fd
555555
556−createOtherDoc ist (ClassDoc n docstring fds) = do
556+createOtherDoc ist (ClassDoc n docstring fds _ _) = do
557557 H.dt ! (A.id $ toValue $ show n) $ do
558558 H.span ! class_ "word" $ do "class"; nbsp
559559 H.span ! class_ "name type"
src/Idris/REPL.hs−32
@@ -386,7 +386,6 @@ ideslaveProcess fn (Defn n) = do process stdout fn (Defn n)
386386ideslaveProcess fn (TotCheck n) = process stdout fn (TotCheck n)
387387ideslaveProcess fn (DebugInfo n) = do process stdout fn (DebugInfo n)
388388 iPrintResult ""
389−ideslaveProcess fn (Info n) = process stdout fn (Info n)
390389ideslaveProcess fn (Search t) = process stdout fn (Search t)
391390ideslaveProcess fn (Spec t) = process stdout fn (Spec t)
392391-- RmProof and AddProof not supported!
@@ -690,12 +689,6 @@ process h fn (DebugInfo n)
690689 iputStrLn $ "Size change: " ++ show sc
691690 when (not (null cg')) $ do iputStrLn "Call graph:\n"
692691 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"
699692process h fn (Search t) = iPrintError "Not implemented"
700693-- FIXME: There is far too much repetition in the cases below!
701694process h fn (CaseSplitAt updatefile l n)
@@ -1103,31 +1096,6 @@ process h fn (MakeDoc s) =
11031096 Left err -> iPrintError err
11041097
11051098
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−
11311099showTotal :: Totality -> IState -> String
11321100showTotal t@(Partial (Other ns)) i
11331101 = 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)
5959 <|> try (do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t))
6060 <|> try (do cmd ["u", "universes"]; eof; return Universes)
6161 <|> 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))
6362 <|> try (do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n))
6463 <|> try (do cmd ["dynamic"]; eof; return ListDynamic)
6564 <|> try (do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l))