@@ -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
@@ -10,6 +11,8 @@ import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, rende
1011
1112import Util.Pretty
1213
14+import Control.Arrow (first)
15+
1316import Data.Maybe
1417import Data.List
1518import qualified Data.Text as T
@@ -32,9 +35,10 @@ data Docs' d = FunDoc (FunDoc' d)
3235 | ClassDoc Name d -- class docs
3336 [FunDoc' d] -- method docs
3437 [(Name, Maybe d)] -- parameters and their docstrings
35− [(PTerm, (d, [(Name, d)]))] -- instances
38+ [(Maybe Name, PTerm, (d, [(Name, d)]))] -- instances: name for named instances, the constraint term, the docs
3639 [PTerm] -- subclasses
3740 [PTerm] -- superclasses
41+ | NamedInstanceDoc Name (FunDoc' d) -- name is class
3842 | ModDoc [String] -- Module name
3943 d
4044 deriving Functor
@@ -102,7 +106,11 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)
102106 <$>
103107 nest 4 (text "Instances:" <$>
104108 vsep (if null instances then [text "<no instances>"]
105− else map pprintInstance instances))
109+ else map pprintInstance normalInstances))
110+ <>
111+ (if null namedInstances then empty
112+ else line <$> nest 4 (text "Named instances:" <$>
113+ vsep (map pprintInstance namedInstances)))
106114 <>
107115 (if null subclasses then empty
108116 else line <$> nest 4 (text "Subclasses:" <$>
@@ -113,14 +121,17 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)
113121 vsep (map dumpInstance superclasses)))
114122 where
115123 params' = zip pNames (repeat False)
124+
125+ (normalInstances, namedInstances) = partition (\(n, _, _) -> not $ isJust n)
126+ instances
116127
117128 pNames = map fst params
118129
119130 ppo = ppOptionIst ist
120131 infixes = idris_infixes ist
121132
122− pprintInstance (term, (doc, argDocs)) =
123− nest 4 (dumpInstance term <>
133+ pprintInstance (mname, term, (doc, argDocs)) =
134+ nest 4 (iname mname <> dumpInstance term <>
124135 (if nullDocstring doc
125136 then empty
126137 else line <>
@@ -133,6 +144,10 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)
133144 then empty
134145 else line <> vsep (map (prettyInstanceParam (map fst argDocs)) argDocs))
135146
147+
148+ iname Nothing = empty
149+ iname (Just n) = annName n <+> colon <> space
150+
136151 prettyInstanceParam params (name, doc) =
137152 if nullDocstring doc
138153 then empty
@@ -170,6 +185,9 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)
170185 then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)
171186 else hsep (punctuate comma (map (prettyName True False params' . fst) params))
172187
188+pprintDocs ist (NamedInstanceDoc _cls doc)
189+ = nest 4 (text "Named instance:" <$> pprintFD ist doc)
190+
173191pprintDocs ist (ModDoc mod docs)
174192 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>
175193 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) docs
@@ -190,13 +208,23 @@ getDocs n@(NS n' ns) w | n' == modDocName
190208 " do not exist! This shouldn't have happened and is a bug."
191209getDocs n w
192210 = do i <- getIState
193− docs <- case lookupCtxt n (idris_classes i) of
194− [ci] -> docClass n ci
195− _ -> case lookupCtxt n (idris_datatypes i) of
196− [ti] -> docData n ti
197− _ -> do fd <- docFun n
198− 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)
199221 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+ ]
200228
201229docData :: Name -> TypeInfo -> Idris Docs
202230docData n ti
@@ -209,19 +237,26 @@ docClass n ci
209237 = do i <- getIState
210238 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i
211239 docstr = maybe emptyDocstring fst docStrings
212− params = map (\pn -> (pn, docStrings >>= (lookup pn . snd))) (class_params ci)
213− instanceDocs = map (fromMaybe (emptyDocstring, []) .
214− listToMaybe .
215− flip lookupCtxt (idris_docstrings i))
216− (class_instances ci)
217− instances = zip (map (delabTy i) (class_instances ci)) instanceDocs
218− (subclasses, instances') = partition (isSubclass . fst) instances
240+ params = map (\pn -> (pn, docStrings >>= (lookup pn . snd)))
241+ (class_params ci)
242+ docsForInstance inst = fromMaybe (emptyDocstring, []) .
243+ flip lookupCtxtExact (idris_docstrings i) $
244+ inst
245+ instances = map (\inst -> (namedInst inst,
246+ delabTy i inst,
247+ docsForInstance inst))
248+ (nub (class_instances ci))
249+ (subclasses, instances') = partition (isSubclass . (\(_,tm,_) -> tm)) instances
219250 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)
220251 mdocs <- mapM (docFun . fst) (class_methods ci)
221252 return $ ClassDoc
222253 n docstr mdocs params
223− instances' (map fst subclasses) superclasses
254+ instances' (map (\(_,tm,_) -> tm) subclasses) superclasses
224255 where
256+ namedInst (NS n ns) = fmap (flip NS ns) (namedInst n)
257+ namedInst n@(UN _) = Just n
258+ namedInst _ = Nothing
259+
225260 getDInst (PInstance _ _ _ _ _ _ _ t _ _) = Just t
226261 getDInst _ = Nothing
227262
@@ -250,6 +285,7 @@ docFun n
250285 where funName :: Name -> String
251286 funName (UN n) = str n
252287 funName (NS n _) = funName n
288+ funName n = show n
253289
254290getPArgNames :: PTerm -> [(Name, Docstring DocTerm)] -> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
255291getPArgNames (PPi plicity name ty body) ds =