@@ -3,33 +3,66 @@
3-- | Generation of HTML documentation for Idris code
3-- | Generation of HTML documentation for Idris code
4module Idris.IdrisDoc (generateDocs) where
4module Idris.IdrisDoc (generateDocs) where
6−import Idris.Core.TT (Name (..), txt, nsroot)
6+import Idris.Core.TT (Name (..), txt, str, nsroot)
7−import Idris.Core.Evaluate (ctxtAlist, Def (..))
7+import Idris.Core.Evaluate (ctxtAlist, Def (..), lookupDefAcc,
8−import Idris.AbsSyntax (IState, tt_ctxt, imported)
9+import Idris.AbsSyntax
12+import Control.Monad.Trans.Error
13+import Control.Monad.Trans.State.Strict
15+import qualified Data.ByteString as BS
16+import qualified Data.Text.Encoding as E
17+import qualified Data.List as L
18+import qualified Data.List.Split as LS
10import qualified Data.Map as M
19import qualified Data.Map as M
20+import qualified Data.Set as S
11import qualified Data.Text as T
21import qualified Data.Text as T
24+import System.IO.Error
25+import System.FilePath
26+import System.Directory
13-- ---------------------------------------------------------------- [ Public ]
28-- ---------------------------------------------------------------- [ Public ]
15-- | Generates HTML documentation for a series of loaded namespaces and their dependencies.
30-- | Generates HTML documentation for a series of loaded namespaces and their dependencies.
16−generateDocs :: IState -- ^ IState where all necessary information is extracted from.
31+generateDocs :: IState -- ^ IState where all necessary information is
17− -> [Name] -- ^ List of namespaces to generate documentation for.
33+ -> [Name] -- ^ List of namespaces to generate
34+ -- documentation for.
18− -> FilePath -- ^ The directory to which documentation will be written.
35+ -> FilePath -- ^ The directory to which documentation will
19 -> IO (Either String ())
37 -> IO (Either String ())
20−generateDocs ist nss out = -- err "IdrisDoc is still in development..."
38+generateDocs ist nss' out =
21− -- Right `fmap` (print $ map toNsName nss)
39+ do let nss = map toNsName nss'
22− -- Right `fmap` (print $ nsDict ist)
40+ docs <- fetchInfo ist nss
23− Right `fmap` (print $ imported ist)
41+ let (c, io) = foldl (checker docs) (0, return ()) nss
43+ if c < length nss then catchIOError (createDocs docs out) (err . show)
44+ else err "No namespaces to generate documentation for"
46+ checker docs st ns | M.member ns docs = st
47+ checker docs (c, io) ns = (c+1, do prev <- io; warnMissing ns)
49+ putStrLn $ "Warning: Ignoring empty or non-existing namespace '" ++
50+ (nsName2Str ns) ++ "'"
26-- ----------------------------------------------------------------- [ Types ]
52-- ----------------------------------------------------------------- [ Types ]
28type Failable = Either String
54type Failable = Either String
29type NsName = [T.Text]
55type NsName = [T.Text]
30−type NsInfo = [(Name, Def)]
56+type NsItem = (Name, Maybe Docs, Accessibility)
57+type NsInfo = [NsItem]
31type NsDict = M.Map NsName NsInfo
58type NsDict = M.Map NsName NsInfo
60+-- Information stored together with IdrisDoc documentation
61+data DocInfo = DocInfo {
62+ -- Namespaces already documented
63+ namespaces :: S.Set NsName
33-- --------------------------------------------------------------- [ Utility ]
66-- --------------------------------------------------------------- [ Utility ]
35-- | Make an error message
68-- | Make an error message
@@ -37,7 +70,8 @@ err :: String -> IO (Failable ())
37err s = return $ Left s
70err s = return $ Left s
40−-- | Converts a Name into a [Text] corresponding to the namespace part of a NS Name
73+-- | Converts a Name into a [Text] corresponding to the namespace
41toNsName :: Name -- ^ Name to convert
75toNsName :: Name -- ^ Name to convert
43toNsName (UN n) = [n]
77toNsName (UN n) = [n]
@@ -51,22 +85,326 @@ getNs :: Name -- ^ Name to retrieve namespace for
51getNs (NS _ ns) = ns
85getNs (NS _ ns) = ns
52getNs _ = []
86getNs _ = []
89+-- | String to replace for the root namespace
91+rootNsStr = "<builtins>"
94+-- | Converts a NsName to string form
95+nsName2Str :: NsName -- ^ NsName to convert
97+nsName2Str n = if null n then rootNsStr else name n
100+ name (ns:nss) = (name nss) ++ ('.' : str ns)
54-- --------------------------------------------------------- [ Info Fetching ]
102-- --------------------------------------------------------- [ Info Fetching ]
56-- | Fetch info about namespaces and their contents
104-- | Fetch info about namespaces and their contents
57−fetchInfo :: IState -- ^ IState to fetch info from
105+fetchInfo :: IState -- ^ IState to fetch info from
58− -> [Name] -- ^ List of namespaces to fetch info for
106+ -> [NsName] -- ^ List of namespaces to fetch info for
59− -> NsDict -- ^ Mapping from namespace name to info about its contents
107+ -> IO NsDict -- ^ Mapping from namespace name to
108+ -- info about its contents
60−fetchInfo ist ns = let nsMap = nsDict ist
109+fetchInfo ist nss =
61− in undefined
110+ do let originNss = S.fromList nss
112+ let reachedNss = traceNss info originNss S.empty
113+ return $ M.filterWithKey (\k _ -> S.member k reachedNss) info
116+-- | Finds all namespaces indirectly referred by a set of namespaces.
117+-- The NsItems of the namespaces are searched for references.
118+traceNss :: NsDict -- ^ Mappings of namespaces and their contents
119+ -> S.Set NsName -- ^ Set of namespaces to trace
120+ -> S.Set NsName -- ^ Set of namespaces which has been traced
121+ -> S.Set NsName -- ^ Set of namespaces to trace and all traced one
123+ let nsTracer ns | Just nsis <- M.lookup ns nsd = map referredNss nsis
124+ nsTracer _ = [S.empty] -- Ignore
125+ reached = S.unions $ concatMap nsTracer (S.toList sT)
126+ processed = S.union sT sD
127+ untraced = S.difference reached processed
128+ in if S.null untraced then processed
129+ else traceNss nsd untraced processed
132+-- | Gets all namespaces directly referred by a NsItem
133+referredNss :: NsItem -- ^ The name to get all directly
134+ -- referred namespaces for
136+referredNss (_, Nothing, _) = S.empty
137+referredNss (n, Just d, _) =
138+ let fds = getFunDocs d
139+ ts = concatMap types fds
140+ names = concatMap (extractPTermNames) ts
141+ in S.map getNs $ S.fromList names
142+ where getFunDocs (FunDoc f) = [f]
143+ getFunDocs (DataDoc f fs) = f:fs
144+ getFunDocs (ClassDoc _ _ fs) = fs
145+ types (FD _ _ args t _) = t:(map second args)
146+ second (_, x, _, _) = x
64−-- | Returns a map of NsName -> [(Name, Def)]
149+-- | Returns an NsDict of containing all known namespaces and their contents
65nsDict :: IState
150nsDict :: IState
66− -> NsDict
151+ -> IO NsDict
67−nsDict ist = let nameDefList = ctxtAlist $ tt_ctxt ist
153+ let nameDefList = ctxtAlist $ tt_ctxt ist
154+ adder m (n, _) = do map <- m
155+ doc <- loadDocs ist n
156+ let acc = getAccess ist n
68− adder m c@(n, d) = M.insertWith (++) (getNs n) [c] m
158+ return $ M.insertWith (++) (getNs n) c map
69− in foldl adder M.empty nameDefList
159+ in foldl adder (return M.empty) nameDefList
162+-- | Gets the Accessibility for a Name
163+getAccess :: IState -- ^ IState containing accessibility information
164+ -> Name -- ^ The Name to retrieve access for
167+ let res = lookupDefAcc n False (tt_ctxt ist)
170+ _ -> Public -- Does this default make sense?
172+-- | Simple predicate for whether an NsItem has Docs
173+hasDoc :: NsItem -- ^ The NsItem to test
174+ -> Bool -- ^ The result
175+hasDoc (_, Just _, _) = True
179+-- | Predicate saying whether a Name possibly may have docs defined
180+-- | Without this, getDocs from Idris.Docs may fail a pattern match.
181+mayHaveDocs :: Name -- ^ The Name to test
182+ -> Bool -- ^ The result
183+mayHaveDocs (UN _) = True
184+mayHaveDocs (NS n _) = mayHaveDocs n
185+mayHaveDocs _ = False
188+-- | Retrieves the Docs for a Name
189+loadDocs :: IState -- ^ IState to extract infomation from
190+ -> Name -- ^ Name to load Docs for
193+ | mayHaveDocs n = do docs <- runErrorT $ evalStateT (getDocs n) ist
194+ case docs of Right d -> return (Just d)
195+ Left _ -> return Nothing
196+ | otherwise = return Nothing
199+-- | Extracts names referred from a type.
200+-- The covering of all PTerms ensures that we avoid unanticipated cases.
201+-- All of them are probably not needed.
202+-- TODO: Remove unnecessary cases
203+extractPTermNames :: PTerm -- ^ Where to extract names from
204+ -> [Name] -- ^ Extracted names
205+extractPTermNames (PRef _ n) = [n]
206+extractPTermNames (PInferRef _ n) = [n]
207+extractPTermNames (PPatvar _ n) = [n]
208+extractPTermNames (PLam n p1 p2) = n : concatMap extract [p1, p2]
209+extractPTermNames (PPi _ n p1 p2) = n : concatMap extract [p1, p2]
210+extractPTermNames (PLet n p1 p2 p3) = n : concatMap extract [p1, p2, p3]
211+extractPTermNames (PTyped p1 p2) = concatMap extract [p1, p2]
212+extractPTermNames (PApp _ p pas) = let names = concatMap extractPArg pas
213+ in (extract p) ++ names
214+extractPTermNames (PAppBind _ p pas) = let names = concatMap extractPArg pas
215+ in (extract p) ++ names
216+extractPTermNames (PMatchApp _ n) = [n]
217+extractPTermNames (PCase _ p ps) = let (ps1, ps2) = unzip ps
218+ in concatMap extract (p:(ps1 ++ ps2))
219+extractPTermNames (PRefl _ p) = extract p
220+extractPTermNames (PEq _ p1 p2) = concatMap extract [p1, p2]
221+extractPTermNames (PRewrite _ a b m) | Just c <- m =
222+ concatMap extract [a, b, c]
223+extractPTermNames (PRewrite _ a b _) = concatMap extract [a, b]
224+extractPTermNames (PPair _ _ p1 p2) = concatMap extract [p1, p2]
225+extractPTermNames (PDPair _ _ a b c) = concatMap extract [a, b, c]
226+extractPTermNames (PAlternative _ l) = concatMap extract l
227+extractPTermNames (PHidden p) = extract p
228+extractPTermNames (PGoal _ p1 n p2) = n : concatMap extract [p1, p2]
229+extractPTermNames (PDoBlock pdos) = concatMap extractPDo pdos
230+extractPTermNames (PIdiom _ p) = extract p
231+extractPTermNames (PMetavar n) = [n]
232+extractPTermNames (PProof tacts) = concatMap extractPTactic tacts
233+extractPTermNames (PTactics tacts) = concatMap extractPTactic tacts
234+extractPTermNames (PCoerced p) = extract p
235+extractPTermNames (PDisamb _ p) = extract p
236+extractPTermNames (PUnifyLog p) = extract p
237+extractPTermNames (PNoImplicits p) = extract p
238+extractPTermNames _ = []
240+extract = extractPTermNames
242+extractPArg (PImp {pname=n, getTm=p}) = n : extract p
243+extractPArg (PExp {getTm=p}) = extract p
244+extractPArg (PConstraint {getTm=p}) = extract p
245+extractPArg (PTacImplicit {pname=n, getScript=p1, getTm=p2})
246+ = n : (concatMap extract [p1, p2])
248+extractPDo (DoExp _ p) = extract p
249+extractPDo (DoBind _ n p) = n : extract p
250+extractPDo (DoBindP _ p1 p2 ps) = let (ps1, ps2) = unzip ps
252+ in concatMap extract (p1 : p2 : ps')
253+extractPDo (DoLet _ n p1 p2) = n : concatMap extract [p1, p2]
254+extractPDo (DoLetP _ p1 p2) = concatMap extract [p1, p2]
256+extractPTactic (Intro ns) = ns
257+extractPTactic (Focus n) = [n]
258+extractPTactic (Refine n _) = [n]
259+extractPTactic (Rewrite p) = extract p
260+extractPTactic (Induction n) = [n]
261+extractPTactic (Equiv p) = extract p
262+extractPTactic (MatchRefine n) = [n]
263+extractPTactic (LetTac n p) = n : extract p
264+extractPTactic (LetTacTy n p1 p2) = n : concatMap extract [p1, p2]
265+extractPTactic (Exact p) = extract p
266+extractPTactic (ProofSearch m ns) | Just n <- m = n : ns
267+extractPTactic (ProofSearch _ ns) = ns
268+extractPTactic (Try t1 t2) = concatMap extractPTactic [t1, t2]
269+extractPTactic (TSeq t1 t2) = concatMap extractPTactic [t1, t2]
270+extractPTactic (ApplyTactic p) = extract p
271+extractPTactic (ByReflection p) = extract p
272+extractPTactic (Reflect p) = extract p
273+extractPTactic (Fill p) = extract p
274+extractPTactic (GoalType _ t) = extractPTactic t
275+extractPTactic (TCheck p) = extract p
276+extractPTactic (TEval p) = extract p
277+extractPTactic _ = []
71-- ------------------------------------------------------- [ HTML Generation ]
279-- ------------------------------------------------------- [ HTML Generation ]
281+-- | Generates the actual HTML output based on info from a NsDict
282+-- A merge of the new docs and any existing docs located in the output dir
284+-- TODO: Ensure the merge always succeeds.
285+-- Currently the content of '<builtins>.ns.html' may change between runs,
286+-- thus not always containing all items referred from other .ns.html files.
287+createDocs :: NsDict -- ^ All info from which to generate docs
288+ -> FilePath -- ^ The base directory to which
289+ -- documentation will be written.
292+ do docInfo <- readDocInfo out
293+ let (new, docInfo') = case docInfo of Nothing -> (True, DocInfo S.empty)
294+ Just di -> (False, di)
295+ nss = S.union (M.keysSet nsd) (namespaces docInfo')
296+ dExists <- doesDirectoryExist out
297+ if new && dExists then err $ "Output directory (" ++ out ++ ") is" ++
298+ " already in use for other than IdrisDoc."
300+ createDirectoryIfMissing True out
301+ foldl (docGen out) (return ()) (M.toList nsd)
302+-- if new then putStrLn "Creating IdrisDoc index"
303+-- else putStrLn "Updating IdrisDoc index"
305+ writeDocInfo out (docInfo' { namespaces = nss })
308+ where docGen out io (n, c) =
310+-- putStrLn $ "Creating IdrisDoc for '" ++ (nsName2Str n) ++ "'"
314+-- | (Over)writes the 'index.html' file in the given directory with
315+-- an (updated) index of namespaces in the documentation
316+createIndex :: S.Set NsName -- ^ Set of namespace names to
317+ -- include in the index
318+ -> FilePath -- ^ The base directory to which
319+ -- documentation will be written.
321+createIndex nss out =
322+ do (path, h) <- openTempFile out "index.html"
323+ hPutStr h $ show $ nss -- TODO: Generate HTML instead
325+ renameFile path (out </> "index.html")
328+-- | Generates a HTML file for a namespace and its contents.
329+-- The location for e.g. Prelude.Algebra is <base>/Prelude/Algebra.html
330+createNsDoc :: NsName -- ^ The name of the namespace to
331+ -- create documentation for
332+ -> NsInfo -- ^ The contents of the namespace
333+ -> FilePath -- ^ The base directory to which
334+ -- documentation will be written.
336+createNsDoc ns content out =
337+ do let tpath = out </> (genRelNsPath ns "ns.html")
338+ dir = takeDirectory tpath
339+ file = takeFileName tpath
340+ createDirectoryIfMissing True dir
341+ (path, h) <- openTempFile dir file
342+ hPutStr h $ show $ content -- TODO: Generate HTML instead
344+ renameFile path tpath
347+-- | Generates a relative filepath for a namespace, appending an extension
348+genRelNsPath :: NsName -- ^ Namespace to generate a path for
349+ -> String -- ^ Extension suffix
351+genRelNsPath ns suffix = subpath ns <.> suffix
353+ where subpath = L.foldl1' (</>) . LS.splitOn "." . nsName2Str
355+-- ---------------------------------------------------- [ DocInfo Read/Write ]
357+-- | Name of the DocInfo file
358+docInfoFile :: String
359+docInfoFile = "IdrisDoc"
362+-- | Reads the 'IdrisDoc' file from the given directory, if it is there
363+-- The info within is converted to a DocInfo
364+readDocInfo :: FilePath -- ^ The IdrisDoc directory also containing the info
365+ -> IO (Maybe DocInfo)
367+ do exists <- doesFileExist (dir </> docInfoFile)
370+ -- Filter out namespaces for which documentation no longer exists
371+ else do di <- (withFile (dir </> docInfoFile) ReadMode reader)
372+ s <- S.fold (onlyValid dir) (return S.empty) (namespaces di)
373+ return . Just . DocInfo $ s
375+ where reader h = let converter = text2DocInfo . E.decodeUtf8
376+ in converter `fmap` BS.hGetContents h
377+ onlyValid out ns s = do s' <- s
378+ let end = (genRelNsPath ns "ns.html")
379+ exists <- doesFileExist $ out </> end
380+ if exists then return $ S.insert ns s'
383+-- | Writes a DocInfo to the 'IdrisDoc' file in the given directory
384+writeDocInfo :: FilePath -- ^ The directory to write to
385+ -> DocInfo -- ^ The DocInfo to write
387+writeDocInfo dir info = withFile (dir </> docInfoFile) WriteMode writer
389+ where writer h = BS.hPut h $ E.encodeUtf8 $ docInfo2Text info
392+-- | Converts a DocInfo to Text for easy writing
393+docInfo2Text :: DocInfo
395+docInfo2Text (DocInfo {namespaces=nss}) = S.fold folder T.empty nss
397+ where folder [] res = T.append (txt rootNsStr) (T.cons '\n' res)
398+ folder ns res = let base = (T.append (head ns) $ T.cons '\n' res)
399+ in foldr joiner base (tail ns)
400+ joiner n r = T.append n (T.cons '.' r)
403+-- | Converts an unmodified Text created by 'docInfo2Text' to DocInfo
404+text2DocInfo :: T.Text
406+text2DocInfo text = DocInfo $ foldl nsAdder S.empty (T.lines text)
408+ where nsAdder set text = S.insert (txt2Ns text) set
409+ txt2Ns t | t == (txt rootNsStr) = []
410+ txt2Ns t = reverse $ T.splitOn (T.singleton '.') t