4b3c477 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2569 from GuglielmoS/fix/master/2241

Fix #2241 by adding a customized display for records documentation

commit4b3c47754fa71164fd65d976203e0fd70c68ebd0 authorDavid Christiansen <david@davidchristiansen.dk> dateSat 5 Sep 2015, 11:32 (11 years ago) parent0fbfeab f5f662c

7 files changed+120−2

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+4 src/Idris/AbsSyntaxTree.hs+9−1 src/Idris/DeepSeq.hs+4 src/Idris/Docs.hs+44 src/Idris/Elab/Record.hs+6 src/Idris/IBC.hs+26−1 src/Idris/IdrisDoc.hs+27

src/Idris/AbsSyntax.hs+4

@@ -397,6 +397,10 @@ addClass n i

397397 _ -> i

398398 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }

399399

400+addRecord :: Name -> RecordInfo -> Idris ()

401+addRecord n ri = do ist <- getIState

402+ putIState $ ist { idris_records = addDef n ri (idris_records ist) }

403+

400404addAutoHint :: Name -> Name -> Idris ()

401405addAutoHint n hint =

402406 do ist <- getIState

src/Idris/AbsSyntaxTree.hs+9−1

@@ -177,6 +177,7 @@ data IState = IState {

177177 idris_implicits :: Ctxt [PArg],

178178 idris_statics :: Ctxt [Bool],

179179 idris_classes :: Ctxt ClassInfo,

180+ idris_records :: Ctxt RecordInfo,

180181 idris_dsls :: Ctxt DSL,

181182 idris_optimisation :: Ctxt OptInfo,

182183 idris_datatypes :: Ctxt TypeInfo,

@@ -290,6 +291,7 @@ data IBCWrite = IBCFix FixDecl

290291 | IBCImp Name

291292 | IBCStatic Name

292293 | IBCClass Name

294+ | IBCRecord Name

293295 | IBCInstance Bool Bool Name Name

294296 | IBCDSL Name

295297 | IBCData Name

@@ -336,7 +338,7 @@ idrisInit = IState initContext S.empty []

336338 emptyContext emptyContext emptyContext emptyContext

337339 emptyContext emptyContext emptyContext emptyContext

338340 emptyContext emptyContext emptyContext emptyContext

339− emptyContext

341+ emptyContext emptyContext

340342 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

341343 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

342344 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

@@ -1277,6 +1279,12 @@ deriving instance Binary ClassInfo

12771279deriving instance NFData ClassInfo

12781280!-}

12791281

1282+-- Record data

1283+data RecordInfo = RI { record_parameters :: [(Name,PTerm)],

1284+ record_constructor :: Name,

1285+ record_projections :: [Name] }

1286+ deriving Show

1287+

12801288-- Type inference data

12811289

12821290data TIData = TIPartial -- ^ a function with a partially defined type

src/Idris/DeepSeq.hs+4

@@ -346,6 +346,10 @@ instance NFData ClassInfo where

346346 = rnf x1 `seq`

347347 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

348348

349+instance NFData RecordInfo where

350+ rnf (RI x1 x2 x3)

351+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

352+

349353instance NFData OptInfo where

350354 rnf (Optimise x1 x2)

351355 = rnf x1 `seq` rnf x2 `seq` ()

src/Idris/Docs.hs+44

@@ -41,6 +41,10 @@ data Docs' d = FunDoc (FunDoc' d)

4141 [PTerm] -- subclasses

4242 [PTerm] -- superclasses

4343 (Maybe (FunDoc' d)) -- explicit constructor

44+ | RecordDoc Name d -- record docs

45+ (FunDoc' d) -- data constructor docs

46+ [FunDoc' d] -- projection docs

47+ [(Name, PTerm, Maybe d)] -- parameters with type and doc

4448 | NamedInstanceDoc Name (FunDoc' d) -- name is class

4549 | ModDoc [String] -- Module name

4650 d

@@ -209,6 +213,33 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct

209213 then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)

210214 else hsep (punctuate comma (map (prettyName True False params' . fst) params))

211215

216+pprintDocs ist (RecordDoc n doc ctor projs params)

217+ = nest 4 (text "Record" <+> prettyName True (ppopt_impl ppo) [] n <>

218+ if nullDocstring doc

219+ then empty

220+ else line <>

221+ renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc)

222+ -- Parameters

223+ <$> (if null params

224+ then empty

225+ else line <> nest 4 (text "Parameters:" <$> prettyParameters) <> line)

226+ -- Constructor

227+ <$> nest 4 (text "Constructor:" <$> pprintFDWithoutTotality ist False ctor)

228+ -- Projections

229+ <$> nest 4 (text "Projections:" <$> vsep (map (pprintFDWithoutTotality ist False) projs))

230+ where

231+ ppo = ppOptionIst ist

232+ infixes = idris_infixes ist

233+

234+ pNames = [n | (n,_,_) <- params]

235+ params' = zip pNames (repeat False)

236+

237+ prettyParameters =

238+ if any isJust [d | (_,_,d) <- params]

239+ then vsep (map (\(n,pt,d) -> prettyParam (n,pt) <+> maybe empty (showDoc ist) d) params)

240+ else hsep (punctuate comma (map prettyParam [(n,pt) | (n,pt,_) <- params]))

241+ prettyParam (n,pt) = prettyName True False params' n <+> text ":" <+> pprintPTerm ppo params' [] infixes pt

242+

212243pprintDocs ist (NamedInstanceDoc _cls doc)

213244 = nest 4 (text "Named instance:" <$> pprintFDWithoutTotality ist True doc)

214245

@@ -234,6 +265,8 @@ getDocs n w

234265 = do i <- getIState

235266 docs <- if | Just ci <- lookupCtxtExact n (idris_classes i)

236267 -> docClass n ci

268+ | Just ri <- lookupCtxtExact n (idris_records i)

269+ -> docRecord n ri

237270 | Just ti <- lookupCtxtExact n (idris_datatypes i)

238271 -> docData n ti

239272 | Just class_ <- classNameForInst i n

@@ -296,6 +329,17 @@ docClass n ci

296329 isSubclass _

297330 = False

298331

332+docRecord :: Name -> RecordInfo -> Idris Docs

333+docRecord n ri

334+ = do i <- getIState

335+ let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

336+ docstr = maybe emptyDocstring fst docStrings

337+ params = map (\(pn,pt) -> (pn, pt, docStrings >>= (lookup (nsroot pn) . snd)))

338+ (record_parameters ri)

339+ pdocs <- mapM docFun (record_projections ri)

340+ ctorDocs <- docFun $ record_constructor ri

341+ return $ RecordDoc n docstr ctorDocs pdocs params

342+

299343docFun :: Name -> Idris FunDoc

300344docFun n

301345 = do i <- getIState

src/Idris/Elab/Record.hs+6

@@ -64,6 +64,12 @@ elabRecord info what doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc

6464 _ -> PDatadecl tyn NoFC tycon [(cdoc, dconsArgDocs, dconName, NoFC, dconTy, fc, [])]

6565 elabData info rsyn doc paramDocs fc opts datadecl

6666

67+ -- Keep track of the record

68+ let parameters = [(n,pt) | (n, _, _, pt) <- params]

69+ let projections = [n | (n, _, _, _, _) <- fieldsWithName]

70+ addRecord tyn (RI parameters dconName projections)

71+ addIBC (IBCRecord tyn)

72+

6773 when (what /= ETypes) $ do

6874 logLvl 1 $ "fieldsWithName " ++ show fieldsWithName

6975 logLvl 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

src/Idris/IBC.hs+26−1

@@ -50,6 +50,7 @@ data IBCFile = IBCFile { ver :: Word16,

5050 ibc_fixes :: ![FixDecl],

5151 ibc_statics :: ![(Name, [Bool])],

5252 ibc_classes :: ![(Name, ClassInfo)],

53+ ibc_records :: ![(Name, RecordInfo)],

5354 ibc_instances :: ![(Bool, Bool, Name, Name)],

5455 ibc_dsls :: ![(Name, DSL)],

5556 ibc_datatypes :: ![(Name, TypeInfo)],

@@ -93,7 +94,7 @@ deriving instance Binary IBCFile

9394!-}

9495

9596initIBC :: IBCFile

96−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] []

97+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] []

9798

9899hasValidIBCVersion :: FilePath -> Idris Bool

99100hasValidIBCVersion fp = do

@@ -142,6 +143,7 @@ entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),

142143 makeEntry "ibc_fixes" (ibc_fixes i),

143144 makeEntry "ibc_statics" (ibc_statics i),

144145 makeEntry "ibc_classes" (ibc_classes i),

146+ makeEntry "ibc_records" (ibc_records i),

145147 makeEntry "ibc_instances" (ibc_instances i),

146148 makeEntry "ibc_dsls" (ibc_dsls i),

147149 makeEntry "ibc_datatypes" (ibc_datatypes i),

@@ -234,6 +236,10 @@ ibc i (IBCClass n) f

234236 = case lookupCtxtExact n (idris_classes i) of

235237 Just v -> return f { ibc_classes = (n,v): ibc_classes f }

236238 _ -> ifail "IBC write failed"

239+ibc i (IBCRecord n) f

240+ = case lookupCtxtExact n (idris_records i) of

241+ Just v -> return f { ibc_records = (n,v): ibc_records f }

242+ _ -> ifail "IBC write failed"

237243ibc i (IBCInstance int res n ins) f

238244 = return f { ibc_instances = (int, res, n, ins) : ibc_instances f }

239245ibc i (IBCDSL n) f

@@ -324,6 +330,7 @@ process reexp i fn = do

324330 pFixes =<< getEntry [] "ibc_fixes" i

325331 pStatics =<< getEntry [] "ibc_statics" i

326332 pClasses =<< getEntry [] "ibc_classes" i

333+ pRecords =<< getEntry [] "ibc_records" i

327334 pInstances =<< getEntry [] "ibc_instances" i

328335 pDSLs =<< getEntry [] "ibc_dsls" i

329336 pDatatypes =<< getEntry [] "ibc_datatypes" i

@@ -442,6 +449,13 @@ pClasses cs = mapM_ (\ (n, c) ->

442449 = addDef n c' (idris_classes i) }))

443450 cs

444451

452+pRecords :: [(Name, RecordInfo)] -> Idris ()

453+pRecords rs = mapM_ (\ (n, r) ->

454+ do i <- getIState

455+ putIState (i { idris_records

456+ = addDef n r (idris_records i) }))

457+ rs

458+

445459pInstances :: [(Bool, Bool, Name, Name)] -> Idris ()

446460pInstances cs = mapM_ (\ (i, res, n, ins) -> addInstance i res n ins) cs

447461

@@ -2130,6 +2144,17 @@ instance Binary ClassInfo where

21302144 x6 <- get

21312145 return (CI x1 x2 x3 x4 x5 [] x6)

21322146

2147+instance Binary RecordInfo where

2148+ put (RI x1 x2 x3)

2149+ = do put x1

2150+ put x2

2151+ put x3

2152+ get

2153+ = do x1 <- get

2154+ x2 <- get

2155+ x3 <- get

2156+ return (RI x1 x2 x3)

2157+

21332158instance Binary OptInfo where

21342159 put (Optimise x1 x2)

21352160 = do put x1

src/Idris/IdrisDoc.hs+27

@@ -221,6 +221,7 @@ referredNss (n, Just d, _) =

221221 where getFunDocs (FunDoc f) = [f]

222222 getFunDocs (DataDoc f fs) = f:fs

223223 getFunDocs (ClassDoc _ _ fs _ _ _ _ _) = fs

224+ getFunDocs (RecordDoc _ _ f fs _) = f:fs

224225 getFunDocs (NamedInstanceDoc _ fd) = [fd]

225226 getFunDocs (ModDoc _ _) = []

226227 types (FD _ _ args t _) = t:(map second args)

@@ -595,6 +596,32 @@ createOtherDoc ist (ClassDoc n docstring fds _ _ _ _ c) = do

595596 then '(':(n' ++ ")")

596597 else n'

597598

599+createOtherDoc ist (RecordDoc n doc ctor projs params) = do

600+ H.dt ! (A.id $ toValue $ show n) $ do

601+ H.span ! class_ "word" $ do "record"; nbsp

602+ H.span ! class_ "name type"

603+ ! title (toValue $ show n)

604+ $ toHtml $ name $ nsroot n

605+ H.span ! class_ "type" $ do nbsp ; prettyParameters

606+ H.dd $ do

607+ (if nullDocstring doc then Empty else Docstrings.renderHtml doc)

608+ if not $ null params

609+ then H.dl $ forM_ params genParam

610+ else Empty

611+ H.dl ! class_ "decls" $ createFunDoc ist ctor

612+ H.dl ! class_ "decls" $ forM_ projs (createFunDoc ist)

613+ where name (NS n ns) = show (NS (sUN $ name n) ns)

614+ name n = let n' = show n

615+ in if (head n') `elem` opChars

616+ then '(':(n' ++ ")")

617+ else n'

618+

619+ genParam (name, pt, docstring) = do

620+ H.dt $ toHtml $ show (nsroot name)

621+ H.dd $ maybe nbsp Docstrings.renderHtml docstring

622+

623+ prettyParameters = toHtml $ unwords [show $ nsroot n | (n,_,_) <- params]

624+

598625createOtherDoc ist (DataDoc fd@(FD n docstring args _ _) fds) = do

599626 H.dt ! (A.id $ toValue $ show n) $ do

600627 H.span ! class_ "word" $ do "data"; nbsp