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

git.iko.soy/Idris-dev

on master help sign in

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

4b3c477David Christiansen11 years ago

src/Idris/AbsSyntax.hs+4

compare with master

unifiedsplit

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

397 _ -> i

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

399

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

401+addRecord n ri = do ist <- getIState

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

403+

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

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

401addAutoHint n hint =

405addAutoHint n hint =

402 do ist <- getIState

406 do ist <- getIState

src/Idris/AbsSyntaxTree.hs+9−1

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

177 idris_implicits :: Ctxt [PArg],

178 idris_statics :: Ctxt [Bool],

179 idris_classes :: Ctxt ClassInfo,

180+ idris_records :: Ctxt RecordInfo,

180 idris_dsls :: Ctxt DSL,

181 idris_dsls :: Ctxt DSL,

181 idris_optimisation :: Ctxt OptInfo,

182 idris_optimisation :: Ctxt OptInfo,

182 idris_datatypes :: Ctxt TypeInfo,

183 idris_datatypes :: Ctxt TypeInfo,

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

290 | IBCImp Name

291 | IBCImp Name

291 | IBCStatic Name

292 | IBCStatic Name

292 | IBCClass Name

293 | IBCClass Name

294+ | IBCRecord Name

293 | IBCInstance Bool Bool Name Name

295 | IBCInstance Bool Bool Name Name

294 | IBCDSL Name

296 | IBCDSL Name

295 | IBCData Name

297 | IBCData Name

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

336 emptyContext emptyContext emptyContext emptyContext

338 emptyContext emptyContext emptyContext emptyContext

337 emptyContext emptyContext emptyContext emptyContext

339 emptyContext emptyContext emptyContext emptyContext

338 emptyContext emptyContext emptyContext emptyContext

340 emptyContext emptyContext emptyContext emptyContext

339− emptyContext

341+ emptyContext emptyContext

340 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

342 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

341 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

343 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

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

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

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

1277deriving instance NFData ClassInfo

1279deriving instance NFData ClassInfo

1278!-}

1280!-}

1279

1281

1282+-- Record data

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

1284+ record_constructor :: Name,

1285+ record_projections :: [Name] }

1286+ deriving Show

1287+

1280-- Type inference data

1288-- Type inference data

1281

1289

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

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

src/Idris/DeepSeq.hs+4

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

346 = rnf x1 `seq`

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

348

349+instance NFData RecordInfo where

350+ rnf (RI x1 x2 x3)

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

352+

349instance NFData OptInfo where

353instance NFData OptInfo where

350 rnf (Optimise x1 x2)

354 rnf (Optimise x1 x2)

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

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

src/Idris/Docs.hs+44

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

41 [PTerm] -- subclasses

42 [PTerm] -- superclasses

43 (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

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

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

45 | ModDoc [String] -- Module name

49 | ModDoc [String] -- Module name

46 d

50 d

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

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

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

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

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

211

215

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+

212pprintDocs ist (NamedInstanceDoc _cls doc)

243pprintDocs ist (NamedInstanceDoc _cls doc)

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

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

214

245

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

234 = do i <- getIState

265 = do i <- getIState

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

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

236 -> docClass n ci

267 -> docClass n ci

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

269+ -> docRecord n ri

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

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

238 -> docData n ti

271 -> docData n ti

239 | Just class_ <- classNameForInst i n

272 | Just class_ <- classNameForInst i n

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

296 isSubclass _

329 isSubclass _

297 = False

330 = False

298

331

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+

299docFun :: Name -> Idris FunDoc

343docFun :: Name -> Idris FunDoc

300docFun n

344docFun n

301 = do i <- getIState

345 = 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

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

65 elabData info rsyn doc paramDocs fc opts datadecl

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+

67 when (what /= ETypes) $ do

73 when (what /= ETypes) $ do

68 logLvl 1 $ "fieldsWithName " ++ show fieldsWithName

74 logLvl 1 $ "fieldsWithName " ++ show fieldsWithName

69 logLvl 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

75 logLvl 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

src/Idris/IBC.hs+26−1

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

50 ibc_fixes :: ![FixDecl],

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

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

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

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

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

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

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

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

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

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

93!-}

94!-}

95initIBC :: IBCFile

96initIBC :: IBCFile

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

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

98hasValidIBCVersion :: FilePath -> Idris Bool

99hasValidIBCVersion :: FilePath -> Idris Bool

99hasValidIBCVersion fp = do

100hasValidIBCVersion fp = do

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

142 makeEntry "ibc_fixes" (ibc_fixes i),

143 makeEntry "ibc_fixes" (ibc_fixes i),

143 makeEntry "ibc_statics" (ibc_statics i),

144 makeEntry "ibc_statics" (ibc_statics i),

144 makeEntry "ibc_classes" (ibc_classes i),

145 makeEntry "ibc_classes" (ibc_classes i),

146+ makeEntry "ibc_records" (ibc_records i),

145 makeEntry "ibc_instances" (ibc_instances i),

147 makeEntry "ibc_instances" (ibc_instances i),

146 makeEntry "ibc_dsls" (ibc_dsls i),

148 makeEntry "ibc_dsls" (ibc_dsls i),

147 makeEntry "ibc_datatypes" (ibc_datatypes i),

149 makeEntry "ibc_datatypes" (ibc_datatypes i),

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

234 = case lookupCtxtExact n (idris_classes i) of

236 = case lookupCtxtExact n (idris_classes i) of

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

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

236 _ -> ifail "IBC write failed"

238 _ -> 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"

237ibc i (IBCInstance int res n ins) f

243ibc i (IBCInstance int res n ins) f

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

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

239ibc i (IBCDSL n) f

245ibc i (IBCDSL n) f

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

443 cs

450 cs

444

451

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+

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

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

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

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

447

461

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

2130 x6 <- get

2144 x6 <- get

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

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

2132

2146

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+

2133instance Binary OptInfo where

2158instance Binary OptInfo where

2134 put (Optimise x1 x2)

2159 put (Optimise x1 x2)

2135 = do put x1

2160 = do put x1

src/Idris/IdrisDoc.hs+27

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

221 where getFunDocs (FunDoc f) = [f]

222 getFunDocs (DataDoc f fs) = f:fs

223 getFunDocs (ClassDoc _ _ fs _ _ _ _ _) = fs

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

224 getFunDocs (NamedInstanceDoc _ fd) = [fd]

225 getFunDocs (NamedInstanceDoc _ fd) = [fd]

225 getFunDocs (ModDoc _ _) = []

226 getFunDocs (ModDoc _ _) = []

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

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

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

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

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

596 else n'

597 else n'

597

598

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+

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

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

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

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

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

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