c6a8862 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add %deprecate directive

c6a8862Edwin Brady11 years ago

src/Idris/AbsSyntax.hs+8

compare with master

unifiedsplit

@@ -346,6 +346,14 @@ getNameHints i n =

346addToCalledG :: Name -> [Name] -> Idris ()

347addToCalledG n ns = return () -- TODO

348

349+addDeprecated :: Name -> String -> Idris ()

350+addDeprecated n reason = do i <- getIState

351+ putIState $ i { idris_deprecated = addDef n reason (idris_deprecated i) }

352+

353+getDeprecated :: Name -> Idris (Maybe String)

354+getDeprecated n = do i <- getIState

355+ return $ lookupCtxtExact n (idris_deprecated i)

356+

349push_estack :: Name -> Bool -> Idris ()

357push_estack :: Name -> Bool -> Idris ()

350push_estack n inst

358push_estack n inst

351 = do i <- getIState

359 = do i <- getIState

src/Idris/AbsSyntaxTree.hs+5−1

@@ -259,7 +259,8 @@ data IState = IState {

259 idris_symbols :: M.Map Name Name, -- ^ Symbol table (preserves sharing of names)

260 idris_exports :: [Name], -- ^ Functions with ExportList

261 idris_highlightedRegions :: [(FC, OutputAnnotation)], -- ^ Highlighting information to output

262− idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser

262+ idris_parserHighlights :: [(FC, OutputAnnotation)], -- ^ Highlighting information from the parser

263+ idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation

263 }

264 }

264

265

265-- Required for parsers library, and therefore trifecta

266-- Required for parsers library, and therefore trifecta

@@ -335,6 +336,7 @@ data IBCWrite = IBCFix FixDecl

335 | IBCUsage (Name, Int)

336 | IBCUsage (Name, Int)

336 | IBCExport Name

337 | IBCExport Name

337 | IBCAutoHint Name Name

338 | IBCAutoHint Name Name

339+ | IBCDeprecate Name String

338 deriving Show

340 deriving Show

339

341

340-- | The initial state for the compiler

342-- | The initial state for the compiler

@@ -349,6 +351,7 @@ idrisInit = IState initContext S.empty []

349 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

351 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

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

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

351 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []

353 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []

354+ emptyContext

352

355

353-- | The monad for the main REPL - reading and processing files and updating

356-- | The monad for the main REPL - reading and processing files and updating

354-- global state (hence the IO inner monad).

357-- global state (hence the IO inner monad).

@@ -708,6 +711,7 @@ data Directive = DLib Codegen String |

708 DNameHint Name FC [(Name, FC)] |

711 DNameHint Name FC [(Name, FC)] |

709 DErrorHandlers Name FC Name FC [(Name, FC)] |

712 DErrorHandlers Name FC Name FC [(Name, FC)] |

710 DLanguage LanguageExt |

713 DLanguage LanguageExt |

714+ DDeprecate Name String |

711 DUsed FC Name Name

715 DUsed FC Name Name

712

716

713-- | A set of instructions for things that need to happen in IState

717-- | A set of instructions for things that need to happen in IState

src/Idris/DeepSeq.hs+3−2

@@ -300,6 +300,7 @@ instance NFData IBCWrite where

300 rnf (IBCUsage usage) = rnf usage `seq` ()

301 rnf (IBCExport name) = rnf name `seq` ()

302 rnf (IBCAutoHint n1 n2) = rnf n1 `seq` rnf n2 `seq` ()

303+ rnf (IBCDeprecate n1 n2) = rnf n1 `seq` rnf n2 `seq` ()

303 rnf (IBCRecord x) = rnf x `seq` ()

304 rnf (IBCRecord x) = rnf x `seq` ()

304

305

306

@@ -689,8 +690,8 @@ instance NFData IState where

689 rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20

690 rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20

690 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40

691 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40

691 x41 x42 x43 x44 x45 x46 x47 x48 x49 x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x60

692 x41 x42 x43 x44 x45 x46 x47 x48 x49 x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x60

692− x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73)

693+ x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74)

693 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` () `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` rnf x16 `seq` rnf x17 `seq` rnf x18 `seq` rnf x19 `seq` rnf x20 `seq`

694 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` () `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` rnf x16 `seq` rnf x17 `seq` rnf x18 `seq` rnf x19 `seq` rnf x20 `seq`

694 rnf x21 `seq` rnf x22 `seq` rnf x23 `seq` rnf x24 `seq` rnf x25 `seq` rnf x26 `seq` rnf x27 `seq` rnf x28 `seq` rnf x29 `seq` rnf x30 `seq` rnf x31 `seq` rnf x32 `seq` rnf x33 `seq` rnf x34 `seq` rnf x35 `seq` rnf x36 `seq` rnf x37 `seq` rnf x38 `seq` rnf x39 `seq` rnf x40 `seq`

695 rnf x21 `seq` rnf x22 `seq` rnf x23 `seq` rnf x24 `seq` rnf x25 `seq` rnf x26 `seq` rnf x27 `seq` rnf x28 `seq` rnf x29 `seq` rnf x30 `seq` rnf x31 `seq` rnf x32 `seq` rnf x33 `seq` rnf x34 `seq` rnf x35 `seq` rnf x36 `seq` rnf x37 `seq` rnf x38 `seq` rnf x39 `seq` rnf x40 `seq`

695 rnf x41 `seq` rnf x42 `seq` rnf x43 `seq` rnf x44 `seq` rnf x45 `seq` rnf x46 `seq` rnf x47 `seq` rnf x48 `seq` rnf x49 `seq` rnf x50 `seq` rnf x51 `seq` rnf x52 `seq` rnf x53 `seq` rnf x54 `seq` rnf x55 `seq` rnf x56 `seq` rnf x57 `seq` rnf x58 `seq` rnf x59 `seq` rnf x60 `seq`

696 rnf x41 `seq` rnf x42 `seq` rnf x43 `seq` rnf x44 `seq` rnf x45 `seq` rnf x46 `seq` rnf x47 `seq` rnf x48 `seq` rnf x49 `seq` rnf x50 `seq` rnf x51 `seq` rnf x52 `seq` rnf x53 `seq` rnf x54 `seq` rnf x55 `seq` rnf x56 `seq` rnf x57 `seq` rnf x58 `seq` rnf x59 `seq` rnf x60 `seq`

696− rnf x61 `seq` rnf x62 `seq` rnf x63 `seq` rnf x64 `seq` rnf x65 `seq` rnf x66 `seq` rnf x67 `seq` rnf x68 `seq` rnf x69 `seq` rnf x70 `seq` rnf x71 `seq` rnf x72 `seq` rnf x73 `seq` ()

697+ rnf x61 `seq` rnf x62 `seq` rnf x63 `seq` rnf x64 `seq` rnf x65 `seq` rnf x66 `seq` rnf x67 `seq` rnf x68 `seq` rnf x69 `seq` rnf x70 `seq` rnf x71 `seq` rnf x72 `seq` rnf x73 `seq` rnf x74 `seq` ()

src/Idris/Directives.hs+4−1

@@ -64,7 +64,10 @@ directiveAction (DErrorHandlers fn nfc arg afc ns) =

64 map (\(n, fc) -> (fc, AnnName n Nothing Nothing Nothing)) ns'

66directiveAction (DLanguage ext) = addLangExt ext

67−

67+directiveAction (DDeprecate n reason)

68+ = do n' <- disambiguate n

69+ addDeprecated n' reason

70+ addIBC (IBCDeprecate n' reason)

68directiveAction (DUsed fc fn arg) = addUsedName fc fn arg

71directiveAction (DUsed fc fn arg) = addUsedName fc fn arg

70disambiguate :: Name -> Idris Name

73disambiguate :: Name -> Idris Name

src/Idris/Elab/Utils.hs+15

@@ -6,12 +6,15 @@ import Idris.Error

6import Idris.DeepSeq

7import Idris.Delaborate

8import Idris.Docstrings

9+import Idris.Output

10import Idris.Core.TT

11import Idris.Core.TT

11import Idris.Core.Elaborate hiding (Tactic(..))

12import Idris.Core.Elaborate hiding (Tactic(..))

12import Idris.Core.Evaluate

13import Idris.Core.Evaluate

13import Idris.Core.Typecheck

14import Idris.Core.Typecheck

16+import Util.Pretty

17+

15import Control.Applicative hiding (Const)

18import Control.Applicative hiding (Const)

16import Control.Monad.State

19import Control.Monad.State

17import Control.Monad

20import Control.Monad

@@ -36,8 +39,20 @@ recheckC_borrowing uniq_check addConstrs bs fc mkerr env t

36 OK x -> return x

39 OK x -> return x

37 logLvl 6 $ "CONSTRAINTS ADDED: " ++ show (tm, ty, cs)

40 logLvl 6 $ "CONSTRAINTS ADDED: " ++ show (tm, ty, cs)

38 when addConstrs $ addConstraints fc cs

41 when addConstrs $ addConstraints fc cs

42+ mapM_ (checkDeprecated fc) (allTTNames tm)

43+ mapM_ (checkDeprecated fc) (allTTNames ty)

39 return (tm, ty)

44 return (tm, ty)

46+checkDeprecated :: FC -> Name -> Idris ()

47+checkDeprecated fc n

48+ = do r <- getDeprecated n

49+ case r of

50+ Nothing -> return ()

51+ Just r -> do iWarn fc $ text "Use of deprecated name " <> annName n

52+ <> case r of

53+ "" -> Util.Pretty.empty

54+ _ -> line <> text r

55+

41iderr :: Name -> Err -> Err

56iderr :: Name -> Err -> Err

42iderr _ e = e

57iderr _ e = e

src/Idris/IBC.hs+11−4

@@ -40,7 +40,7 @@ import System.Directory

40import Codec.Archive.Zip

42ibcVersion :: Word16

43−ibcVersion = 125

43+ibcVersion = 126

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

@@ -86,7 +86,8 @@ data IBCFile = IBCFile { ver :: Word16,

86 ibc_parsedSpan :: !(Maybe FC),

87 ibc_usage :: ![(Name, Int)],

88 ibc_exports :: ![Name],

89− ibc_autohints :: ![(Name, Name)]

89+ ibc_autohints :: ![(Name, Name)],

90+ ibc_deprecated :: ![(Name, String)]

90 }

91 }

91 deriving Show

92 deriving Show

92{-!

93{-!

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

94!-}

95!-}

96initIBC :: IBCFile

97initIBC :: IBCFile

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

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

99hasValidIBCVersion :: FilePath -> Idris Bool

100hasValidIBCVersion :: FilePath -> Idris Bool

100hasValidIBCVersion fp = do

101hasValidIBCVersion fp = do

@@ -179,7 +180,8 @@ entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),

179 toEntry "ibc_parsedSpan" 0 . encode <$> ibc_parsedSpan i,

180 toEntry "ibc_parsedSpan" 0 . encode <$> ibc_parsedSpan i,

180 makeEntry "ibc_usage" (ibc_usage i),

181 makeEntry "ibc_usage" (ibc_usage i),

181 makeEntry "ibc_exports" (ibc_exports i),

182 makeEntry "ibc_exports" (ibc_exports i),

182− makeEntry "ibc_autohints" (ibc_autohints i)]

183+ makeEntry "ibc_autohints" (ibc_autohints i),

184+ makeEntry "ibc_deprecated" (ibc_deprecated i)]

183

185

184writeArchive :: FilePath -> IBCFile -> Idris ()

186writeArchive :: FilePath -> IBCFile -> Idris ()

185writeArchive fp i = do let a = L.foldl (\x y -> addEntryToArchive y x) emptyArchive (entries i)

187writeArchive fp i = do let a = L.foldl (\x y -> addEntryToArchive y x) emptyArchive (entries i)

@@ -305,6 +307,7 @@ ibc i (IBCModDocs n) f = case lookupCtxtExact n (idris_moduledocs i) of

305ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f }

307ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f }

306ibc i (IBCExport n) f = return f { ibc_exports = n : ibc_exports f }

308ibc i (IBCExport n) f = return f { ibc_exports = n : ibc_exports f }

307ibc i (IBCAutoHint n h) f = return f { ibc_autohints = (n, h) : ibc_autohints f }

309ibc i (IBCAutoHint n h) f = return f { ibc_autohints = (n, h) : ibc_autohints f }

310+ibc i (IBCDeprecate n r) f = return f { ibc_deprecated = (n, r) : ibc_deprecated f }

308

311

309getEntry :: (Binary b, NFData b) => b -> FilePath -> Archive -> Idris b

312getEntry :: (Binary b, NFData b) => b -> FilePath -> Archive -> Idris b

310getEntry alt f a = case findEntryByPath f a of

313getEntry alt f a = case findEntryByPath f a of

@@ -367,6 +370,7 @@ process reexp i fn = do

367 pUsage =<< getEntry [] "ibc_usage" i

370 pUsage =<< getEntry [] "ibc_usage" i

368 pExports =<< getEntry [] "ibc_exports" i

371 pExports =<< getEntry [] "ibc_exports" i

369 pAutoHints =<< getEntry [] "ibc_autohints" i

372 pAutoHints =<< getEntry [] "ibc_autohints" i

373+ pDeprecate =<< getEntry [] "ibc_deprecated" i

370

374

371timestampOlder :: FilePath -> FilePath -> Idris ()

375timestampOlder :: FilePath -> FilePath -> Idris ()

372timestampOlder src ibc = do srct <- runIO $ getModificationTime src

376timestampOlder src ibc = do srct <- runIO $ getModificationTime src

@@ -394,6 +398,9 @@ pExports ns = updateIState (\i -> i { idris_exports = ns ++ idris_exports i })

394pAutoHints :: [(Name, Name)] -> Idris ()

398pAutoHints :: [(Name, Name)] -> Idris ()

395pAutoHints ns = mapM_ (\(n,h) -> addAutoHint n h) ns

399pAutoHints ns = mapM_ (\(n,h) -> addAutoHint n h) ns

396

400

401+pDeprecate :: [(Name, String)] -> Idris ()

402+pDeprecate ns = mapM_ (\(n,reason) -> addDeprecated n reason) ns

403+

397pImportDirs :: [FilePath] -> Idris ()

404pImportDirs :: [FilePath] -> Idris ()

398pImportDirs fs = mapM_ addImportDir fs

405pImportDirs fs = mapM_ addImportDir fs

399

406

src/Idris/Parser.hs+4

@@ -1323,6 +1323,10 @@ directive syn = do try (lchar '%' *> reserved "lib")

1323 return [PDirective (DErrorHandlers fn nfc arg afc ns) ]

1324 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;

1325 return [PDirective (DLanguage ext)]

1326+ <|> do try (lchar '%' *> reserved "deprecate")

1327+ n <- fst <$> fnName

1328+ alt <- option "" (fst <$> stringLiteral)

1329+ return [PDirective (DDeprecate n alt)]

1326 <|> do fc <- getFC

1330 <|> do fc <- getFC

1327 try (lchar '%' *> reserved "used")

1331 try (lchar '%' *> reserved "used")

1328 fn <- fst <$> fnName

1332 fn <- fst <$> fnName