@@ -1,4 +1,5 @@
1−{-# LANGUAGE DeriveFunctor, PatternGuards #-}
1+{-# LANGUAGE DeriveFunctor, PatternGuards, MultiWayIf #-}
2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
23module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc, FunDoc'(..), Docs, Docs'(..)) where
34
45import Idris.AbsSyntax
@@ -37,6 +38,7 @@ data Docs' d = FunDoc (FunDoc' d)
3738 [(Maybe Name, PTerm, (d, [(Name, d)]))] -- instances: name for named instances, the constraint term, the docs
3839 [PTerm] -- subclasses
3940 [PTerm] -- superclasses
41+ | NamedInstanceDoc Name (FunDoc' d) -- name is class
4042 | ModDoc [String] -- Module name
4143 d
4244 deriving Functor
@@ -183,6 +185,9 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)
183185 then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)
184186 else hsep (punctuate comma (map (prettyName True False params' . fst) params))
185187
188+pprintDocs ist (NamedInstanceDoc _cls doc)
189+ = nest 4 (text "Named instance:" <$> pprintFD ist doc)
190+
186191pprintDocs ist (ModDoc mod docs)
187192 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>
188193 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) docs
@@ -203,13 +208,23 @@ getDocs n@(NS n' ns) w | n' == modDocName
203208 " do not exist! This shouldn't have happened and is a bug."
204209getDocs n w
205210 = do i <- getIState
206− docs <- case lookupCtxt n (idris_classes i) of
207− [ci] -> docClass n ci
208− _ -> case lookupCtxt n (idris_datatypes i) of
209− [ti] -> docData n ti
210− _ -> do fd <- docFun n
211− return (FunDoc fd)
211+ docs <- if | Just ci <- lookupCtxtExact n (idris_classes i)
212+ -> docClass n ci
213+ | Just ti <- lookupCtxtExact n (idris_datatypes i)
214+ -> docData n ti
215+ | Just class_ <- classNameForInst i n
216+ -> do fd <- docFun n
217+ return $ NamedInstanceDoc class_ fd
218+ | otherwise
219+ -> do fd <- docFun n
220+ return (FunDoc fd)
212221 return $ fmap (howMuch w) docs
222+ where classNameForInst :: IState -> Name -> Maybe Name
223+ classNameForInst ist n =
224+ listToMaybe [ cn
225+ | (cn, ci) <- toAlist (idris_classes ist)
226+ , n `elem` class_instances ci
227+ ]
213228
214229docData :: Name -> TypeInfo -> Idris Docs
215230docData n ti
@@ -270,6 +285,7 @@ docFun n
270285 where funName :: Name -> String
271286 funName (UN n) = str n
272287 funName (NS n _) = funName n
288+ funName n = show n
273289
274290getPArgNames :: PTerm -> [(Name, Docstring DocTerm)] -> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
275291getPArgNames (PPi plicity name ty body) ds =