@@ -1,4 +1,5 @@
1−{-# LANGUAGE DeriveFunctor, PatternGuards #-}
1+{-# LANGUAGE DeriveFunctor, PatternGuards, MultiWayIf #-}
2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
2module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc, FunDoc'(..), Docs, Docs'(..)) where
3module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc, FunDoc'(..), Docs, Docs'(..)) where
4import Idris.AbsSyntax
5import Idris.AbsSyntax
@@ -37,6 +38,7 @@ data Docs' d = FunDoc (FunDoc' d)
37 [(Maybe Name, PTerm, (d, [(Name, d)]))] -- instances: name for named instances, the constraint term, the docs
38 [(Maybe Name, PTerm, (d, [(Name, d)]))] -- instances: name for named instances, the constraint term, the docs
38 [PTerm] -- subclasses
39 [PTerm] -- subclasses
39 [PTerm] -- superclasses
40 [PTerm] -- superclasses
41+ | NamedInstanceDoc Name (FunDoc' d) -- name is class
40 | ModDoc [String] -- Module name
42 | ModDoc [String] -- Module name
42 deriving Functor
44 deriving Functor
@@ -183,6 +185,9 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)
183 then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)
185 then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)
184 else hsep (punctuate comma (map (prettyName True False params' . fst) params))
186 else hsep (punctuate comma (map (prettyName True False params' . fst) params))
188+pprintDocs ist (NamedInstanceDoc _cls doc)
189+ = nest 4 (text "Named instance:" <$> pprintFD ist doc)
186pprintDocs ist (ModDoc mod docs)
191pprintDocs ist (ModDoc mod docs)
187 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>
192 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>
188 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) docs
193 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) docs
@@ -203,13 +208,23 @@ getDocs n@(NS n' ns) w | n' == modDocName
203 " do not exist! This shouldn't have happened and is a bug."
208 " do not exist! This shouldn't have happened and is a bug."
204getDocs n w
209getDocs n w
205 = do i <- getIState
210 = do i <- getIState
206− docs <- case lookupCtxt n (idris_classes i) of
211+ docs <- if | Just ci <- lookupCtxtExact n (idris_classes i)
207− [ci] -> docClass n ci
212+ -> docClass n ci
208− _ -> case lookupCtxt n (idris_datatypes i) of
213+ | Just ti <- lookupCtxtExact n (idris_datatypes i)
209− [ti] -> docData n ti
214+ -> docData n ti
215+ | Just class_ <- classNameForInst i n
216+ -> do fd <- docFun n
217+ return $ NamedInstanceDoc class_ fd
210− _ -> do fd <- docFun n
219+ -> do fd <- docFun n
211− return (FunDoc fd)
220+ return (FunDoc fd)
212 return $ fmap (howMuch w) docs
221 return $ fmap (howMuch w) docs
222+ where classNameForInst :: IState -> Name -> Maybe Name
223+ classNameForInst ist n =
225+ | (cn, ci) <- toAlist (idris_classes ist)
226+ , n `elem` class_instances ci
214docData :: Name -> TypeInfo -> Idris Docs
229docData :: Name -> TypeInfo -> Idris Docs
215docData n ti
230docData n ti
@@ -270,6 +285,7 @@ docFun n
270 where funName :: Name -> String
285 where funName :: Name -> String
271 funName (UN n) = str n
286 funName (UN n) = str n
272 funName (NS n _) = funName n
287 funName (NS n _) = funName n
274getPArgNames :: PTerm -> [(Name, Docstring DocTerm)] -> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
290getPArgNames :: PTerm -> [(Name, Docstring DocTerm)] -> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
275getPArgNames (PPi plicity name ty body) ds =
291getPArgNames (PPi plicity name ty body) ds =