c56d5cf · Idris-dev · git.iko.soy

CHANGELOG.md+4

compare with master

unifiedsplit

@@ -26,6 +26,10 @@

26 be called directly, so the recursive structure of `SnocList` can direct the

27 recursion structure of `my_reverse`.

28

29+* Added `%fragile` directive, which gives a warning and a message when a

30+ fragile name is referenced. For use in detailing fragile APIs.

31+

32+

29## Library updates

33## Library updates

30

34

31* `Control.WellFounded` module removed, and added to the Prelude as

35* `Control.WellFounded` module removed, and added to the Prelude as

idris.cabal+5−1

@@ -91,7 +91,7 @@ Extra-source-files:

91 config.mk

92 stack.yaml

93 man/idris.1

94−

94+

95 rts/*.c

96 rts/*.h

97 rts/arduino/*.c

@@ -409,6 +409,10 @@ Extra-source-files:

409 test/corecords002/run

410 test/corecords002/expected

411

412+ test/directives001/*.idr

413+ test/directives001/run

414+ test/directives001/expected

415+

412 test/delab001/*.idr

416 test/delab001/*.idr

413 test/delab001/run

417 test/delab001/run

414 test/delab001/expected

418 test/delab001/expected

src/Idris/AbsSyntax.hs+25−12

@@ -381,12 +381,25 @@ getNameHints i n =

381 _ -> []

382

383addDeprecated :: Name -> String -> Idris ()

384−addDeprecated n reason = do i <- getIState

384+addDeprecated n reason = do

385+ i <- getIState

385− putIState $ i { idris_deprecated = addDef n reason (idris_deprecated i) }

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

386

387

387getDeprecated :: Name -> Idris (Maybe String)

388getDeprecated :: Name -> Idris (Maybe String)

388−getDeprecated n = do i <- getIState

389+getDeprecated n = do

390+ i <- getIState

389− return $ lookupCtxtExact n (idris_deprecated i)

391+ return $ lookupCtxtExact n (idris_deprecated i)

392+

393+

394+addFragile :: Name -> String -> Idris ()

395+addFragile n reason = do

396+ i <- getIState

397+ putIState $ i { idris_fragile = addDef n reason (idris_fragile i) }

398+

399+getFragile :: Name -> Idris (Maybe String)

400+getFragile n = do

401+ i <- getIState

402+ return $ lookupCtxtExact n (idris_fragile i)

390

403

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

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

392push_estack n inst

405push_estack n inst

@@ -658,7 +671,7 @@ addDeferred' nt ns

658 = do mapM_ (\(n, (i, _, t, _, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns

671 = do mapM_ (\(n, (i, _, t, _, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns

659 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns

672 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns

660 i <- getIState

673 i <- getIState

661− putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel, isDefinable)) ->

674+ putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel, isDefinable)) ->

662 (n, (top, i, ns, isTopLevel, isDefinable))) ns ++

675 (n, (top, i, ns, isTopLevel, isDefinable))) ns ++

663 idris_metavars i }

676 idris_metavars i }

664 where

677 where

@@ -673,7 +686,7 @@ addDeferred' nt ns

673 tidyNames used b = b

686 tidyNames used b = b

674

687

675solveDeferred :: FC -> Name -> Idris ()

688solveDeferred :: FC -> Name -> Idris ()

676−solveDeferred fc n

689+solveDeferred fc n

677 = do i <- getIState

690 = do i <- getIState

678 case lookup n (idris_metavars i) of

691 case lookup n (idris_metavars i) of

679 Just (_, _, _, _, False) ->

692 Just (_, _, _, _, False) ->

@@ -1701,7 +1714,7 @@ addImpl' inpat env infns imp_meths ist ptm

1701 ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm

1714 ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm

1702 ai inpat qq env ds (PRef fc fcs f)

1715 ai inpat qq env ds (PRef fc fcs f)

1703 | f `elem` infns = PInferRef fc fcs f

1716 | f `elem` infns = PInferRef fc fcs f

1704− | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds []

1717+ | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds []

1705 ai inpat qq env ds (PHidden (PRef fc hl f))

1718 ai inpat qq env ds (PHidden (PRef fc hl f))

1706 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [])

1719 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [])

1707 ai inpat qq env ds (PRewrite fc by l r g)

1720 ai inpat qq env ds (PRewrite fc by l r g)

@@ -1742,7 +1755,7 @@ addImpl' inpat env infns imp_meths ist ptm

1742 = let f' = ai inpat qq env ds f

1755 = let f' = ai inpat qq env ds f

1743 as' = map (fmap (ai inpat qq env ds)) as in

1756 as' = map (fmap (ai inpat qq env ds)) as in

1744 mkPApp fc 1 f' as'

1757 mkPApp fc 1 f' as'

1745− ai inpat qq env ds (PWithApp fc f a)

1758+ ai inpat qq env ds (PWithApp fc f a)

1746 = PWithApp fc (ai inpat qq env ds f) (ai inpat qq env ds a)

1759 = PWithApp fc (ai inpat qq env ds f) (ai inpat qq env ds a)

1747 ai inpat qq env ds (PCase fc c os)

1760 ai inpat qq env ds (PCase fc c os)

1748 = let c' = ai inpat qq env ds c in

1761 = let c' = ai inpat qq env ds c in

@@ -1750,7 +1763,7 @@ addImpl' inpat env infns imp_meths ist ptm

1750 -- definition which is passed through addImpl again

1763 -- definition which is passed through addImpl again

1751 PCase fc c' (map aiCase os)

1764 PCase fc c' (map aiCase os)

1752 where

1765 where

1753− aiCase (lhs, rhs)

1766+ aiCase (lhs, rhs)

1754 = (lhs, ai inpat qq (env ++ patnames lhs) ds rhs)

1767 = (lhs, ai inpat qq (env ++ patnames lhs) ds rhs)

1755

1768

1756 -- Anything beginning with a lower case letter, not applied,

1769 -- Anything beginning with a lower case letter, not applied,

@@ -1854,9 +1867,9 @@ aiFn topname inpat True qq imp_meths ist fc f ffc ds []

1854 vname (UN n) = True -- non qualified

1867 vname (UN n) = True -- non qualified

1855 vname _ = False

1868 vname _ = False

1856

1869

1857−aiFn topname inpat expat qq imp_meths ist fc f ffc ds as

1870+aiFn topname inpat expat qq imp_meths ist fc f ffc ds as

1858 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as

1871 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as

1859−aiFn topname inpat expat qq imp_meths ist fc f ffc ds as

1872+aiFn topname inpat expat qq imp_meths ist fc f ffc ds as

1860 -- This is where namespaces get resolved by adding PAlternative

1873 -- This is where namespaces get resolved by adding PAlternative

1861 = do let ns = lookupCtxtName f (idris_implicits ist)

1874 = do let ns = lookupCtxtName f (idris_implicits ist)

1862 let nh = filter (\(n, _) -> notHidden n) ns

1875 let nh = filter (\(n, _) -> notHidden n) ns

@@ -1920,7 +1933,7 @@ aiFn topname inpat expat qq imp_meths ist fc f ffc ds as

1920 case find n imps [] of

1933 case find n imps [] of

1921 Just (tm, imps') ->

1934 Just (tm, imps') ->

1922 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'

1935 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'

1923− Nothing ->

1936+ Nothing ->

1924 PImp p True l n Placeholder :

1937 PImp p True l n Placeholder :

1925 insImpAcc (M.insert n Placeholder pnas) ps given imps

1938 insImpAcc (M.insert n Placeholder pnas) ps given imps

1926 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =

1939 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =

src/Idris/AbsSyntaxTree.hs+9−6

@@ -60,7 +60,7 @@ data ElabInfo = EInfo { params :: [(Name, PTerm)],

60 namespace :: Maybe [String],

61 elabFC :: Maybe FC,

62 -- We may, recursively, collect transformations to

63− -- do on the rhs, e.g. rewriting recursive calls to

63+ -- do on the rhs, e.g. rewriting recursive calls to

64 -- functions defined by 'with'

65 rhs_trans :: PTerm -> PTerm,

66 rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->

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

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

272 idris_deprecated :: Ctxt String, -- ^ Deprecated names and explanation

273 idris_inmodule :: S.Set Name, -- ^ Names defined in current module

274− idris_ttstats :: M.Map Term (Int, Term)

274+ idris_ttstats :: M.Map Term (Int, Term),

275+ idris_fragile :: Ctxt String -- ^ Fragile names and explanation.

275 }

276 }

276

277

277-- Required for parsers library, and therefore trifecta

278-- Required for parsers library, and therefore trifecta

@@ -347,6 +348,7 @@ data IBCWrite = IBCFix FixDecl

347 | IBCExport Name

348 | IBCExport Name

348 | IBCAutoHint Name Name

349 | IBCAutoHint Name Name

349 | IBCDeprecate Name String

350 | IBCDeprecate Name String

351+ | IBCFragile Name String

350 deriving Show

352 deriving Show

351

353

352-- | The initial state for the compiler

354-- | The initial state for the compiler

@@ -361,7 +363,7 @@ idrisInit = IState initContext S.empty []

361 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private False [] Nothing [] []

363 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private False [] Nothing [] []

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

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

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

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

364− emptyContext S.empty M.empty

366+ emptyContext S.empty M.empty emptyContext

365

367

366

368

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

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

@@ -772,6 +774,7 @@ data Directive = DLib Codegen String |

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

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

773 DLanguage LanguageExt |

775 DLanguage LanguageExt |

774 DDeprecate Name String |

776 DDeprecate Name String |

777+ DFragile Name String |

775 DAutoImplicits Bool |

778 DAutoImplicits Bool |

776 DUsed FC Name Name

779 DUsed FC Name Name

777

780

@@ -1016,7 +1019,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

1016 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)

1019 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)

1017 | PTyped PTerm PTerm -- ^ Term with explicit type

1020 | PTyped PTerm PTerm -- ^ Term with explicit type

1018 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x

1021 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x

1019− | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument

1022+ | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument

1020 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)

1023 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)

1021 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application

1024 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application

1022 | PMatchApp FC Name -- ^ Make an application by type matching

1025 | PMatchApp FC Name -- ^ Make an application by type matching

@@ -1024,7 +1027,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

1024 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs

1027 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs

1025 | PTrue FC PunInfo -- ^ Unit type..?

1028 | PTrue FC PunInfo -- ^ Unit type..?

1026 | PResolveTC FC -- ^ Solve this dictionary by type class resolution

1029 | PResolveTC FC -- ^ Solve this dictionary by type class resolution

1027− | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)

1030+ | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)

1028 -- ^ "rewrite" syntax, with optional rewriting function

1031 -- ^ "rewrite" syntax, with optional rewriting function

1029 -- and optional result type

1032 -- and optional result type

1030 | PPair FC [FC] PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration). The list of FCs is its punctuation.

1033 | PPair FC [FC] PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration). The list of FCs is its punctuation.

@@ -1886,7 +1889,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1886 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"

1889 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"

1887 prettySe d p bnd (PRewrite _ by l r _) =

1890 prettySe d p bnd (PRewrite _ by l r _) =

1888 depth d . bracket p startPrec $

1891 depth d . bracket p startPrec $

1889− text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l

1892+ text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l

1890 <+> (case by of

1893 <+> (case by of

1891 Nothing -> empty

1894 Nothing -> empty

1892 Just fn -> text "using" <+>

1895 Just fn -> text "using" <+>

src/Idris/DeepSeq.hs+3−2

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

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

307 rnf (IBCDeprecate n1 n2) = rnf n1 `seq` rnf n2 `seq` ()

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

309+ rnf (IBCFragile n1 n2) = rnf n1 `seq` rnf n2 `seq` ()

309

310

311

311instance NFData a => NFData (D.Block a) where

312instance NFData a => NFData (D.Block a) where

@@ -698,8 +699,8 @@ instance NFData IState where

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

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

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

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

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

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

701− x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74 x75)

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

702 = 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`

703 = 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`

703 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`

704 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`

704 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`

705 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`

705− 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` rnf x75 `seq` ()

706+ 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` rnf x75 `seq` rnf x76 `seq` ()

src/Idris/Directives.hs+6−2

@@ -59,8 +59,7 @@ directiveAction (DNameHint ty tyFC ns) = do

59 ty' <- disambiguate ty

60 mapM_ (addNameHint ty' . fst) ns

61 mapM_ (\n -> addIBC (IBCNameHint (ty', fst n))) ns

62− sendHighlighting $

63− [(tyFC, AnnName ty' Nothing Nothing Nothing)] ++ map (\(n, fc) -> (fc, AnnBoundName n False)) ns

62+ sendHighlighting $ [(tyFC, AnnName ty' Nothing Nothing Nothing)] ++ map (\(n, fc) -> (fc, AnnBoundName n False)) ns

64

63

65directiveAction (DErrorHandlers fn nfc arg afc ns) = do

64directiveAction (DErrorHandlers fn nfc arg afc ns) = do

66 fn' <- disambiguate fn

65 fn' <- disambiguate fn

@@ -81,6 +80,11 @@ directiveAction (DDeprecate n reason) = do

81 addDeprecated n' reason

80 addDeprecated n' reason

82 addIBC (IBCDeprecate n' reason)

81 addIBC (IBCDeprecate n' reason)

83

82

83+directiveAction (DFragile n reason) = do

84+ n' <- disambiguate n

85+ addFragile n' reason

86+ addIBC (IBCFragile n' reason)

87+

84directiveAction (DAutoImplicits b) = setAutoImpls b

88directiveAction (DAutoImplicits b) = setAutoImpls b

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

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

86

90

src/Idris/Elab/Utils.hs+24−7

@@ -41,6 +41,9 @@ recheckC_borrowing uniq_check addConstrs bs fc mkerr env t

41 when addConstrs $ addConstraints fc cs

42 mapM_ (checkDeprecated fc) (allTTNames tm)

43 mapM_ (checkDeprecated fc) (allTTNames ty)

44+ mapM_ (checkFragile fc) (allTTNames tm)

45+ mapM_ (checkFragile fc) (allTTNames ty)

46+

44 return (tm, ty)

47 return (tm, ty)

45

48

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

49checkDeprecated :: FC -> Name -> Idris ()

@@ -53,6 +56,20 @@ checkDeprecated fc n

53 "" -> Util.Pretty.empty

56 "" -> Util.Pretty.empty

54 _ -> line <> text r

57 _ -> line <> text r

55

58

59+

60+checkFragile :: FC -> Name -> Idris ()

61+checkFragile fc n = do

62+ r <- getFragile n

63+ case r of

64+ Nothing -> return ()

65+ Just r -> do

66+ iWarn fc $ text "Use of a fragile construct "

67+ <> annName n

68+ <> case r of

69+ "" -> Util.Pretty.empty

70+ _ -> line <> text r

71+

72+

56iderr :: Name -> Err -> Err

73iderr :: Name -> Err -> Err

57iderr _ e = e

74iderr _ e = e

58

75

@@ -319,14 +336,14 @@ mkStaticTy ns t = t

319

336

320-- Check that a name has the minimum required accessibility

337-- Check that a name has the minimum required accessibility

321checkVisibility :: FC -> Name -> Accessibility -> Accessibility -> Name -> Idris ()

338checkVisibility :: FC -> Name -> Accessibility -> Accessibility -> Name -> Idris ()

322−checkVisibility fc n minAcc acc ref

339+checkVisibility fc n minAcc acc ref

323 = do nvis <- getFromHideList ref

340 = do nvis <- getFromHideList ref

324 case nvis of

341 case nvis of

325 Nothing -> return ()

342 Nothing -> return ()

326− Just acc' -> if acc' > minAcc

343+ Just acc' -> if acc' > minAcc

327− then tclift $ tfail (At fc

344+ then tclift $ tfail (At fc

328− (Msg $ show acc ++ " " ++ show n ++

345+ (Msg $ show acc ++ " " ++ show n ++

329− " can't refer to " ++

346+ " can't refer to " ++

330 show acc' ++ " " ++ show ref))

347 show acc' ++ " " ++ show ref))

331 else return ()

348 else return ()

332

349

@@ -397,10 +414,10 @@ setDetaggable n = do

397 _ -> putIState ist { idris_optimisation = addDef n (Optimise [] True) opt }

414 _ -> putIState ist { idris_optimisation = addDef n (Optimise [] True) opt }

398

415

399displayWarnings :: EState -> Idris ()

416displayWarnings :: EState -> Idris ()

400−displayWarnings est

417+displayWarnings est

401 = mapM_ displayImpWarning (implicit_warnings est)

418 = mapM_ displayImpWarning (implicit_warnings est)

402 where

419 where

403 displayImpWarning :: (FC, Name) -> Idris ()

420 displayImpWarning :: (FC, Name) -> Idris ()

404− displayImpWarning (fc, n) =

421+ displayImpWarning (fc, n) =

405 iputStrLn $ show fc ++ ":WARNING: " ++ show (nsroot n) ++ " is bound as an implicit\n"

422 iputStrLn $ show fc ++ ":WARNING: " ++ show (nsroot n) ++ " is bound as an implicit\n"

406 ++ "\tDid you mean to refer to " ++ show n ++ "?"

423 ++ "\tDid you mean to refer to " ++ show n ++ "?"

src/Idris/IBC.hs+13−4

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

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 137

43+ibcVersion = 138

44

45-- When IBC is being loaded - we'll load different things (and omit different

46-- structures/definitions) depending on which phase we're in

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

95 ibc_deprecated :: ![(Name, String)],

96 ibc_defs :: ![(Name, Def)],

97 ibc_total :: ![(Name, Totality)],

98− ibc_access :: ![(Name, Accessibility)]

98+ ibc_access :: ![(Name, Accessibility)],

99+ ibc_fragile :: ![(Name, String)]

99 }

100 }

100 deriving Show

101 deriving Show

101{-!

102{-!

@@ -103,7 +104,7 @@ deriving instance Binary IBCFile

103!-}

104!-}

104

105

105initIBC :: IBCFile

106initIBC :: IBCFile

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

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

107

108

108hasValidIBCVersion :: FilePath -> Idris Bool

109hasValidIBCVersion :: FilePath -> Idris Bool

109hasValidIBCVersion fp = do

110hasValidIBCVersion fp = do

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

196 makeEntry "ibc_deprecated" (ibc_deprecated i),

197 makeEntry "ibc_deprecated" (ibc_deprecated i),

197 makeEntry "ibc_defs" (ibc_defs i),

198 makeEntry "ibc_defs" (ibc_defs i),

198 makeEntry "ibc_total" (ibc_total i),

199 makeEntry "ibc_total" (ibc_total i),

199− makeEntry "ibc_access" (ibc_access i)]

200+ makeEntry "ibc_access" (ibc_access i),

201+ makeEntry "ibc_fragile" (ibc_fragile i)]

200

202

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

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

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

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

@@ -323,6 +325,7 @@ ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f }

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

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

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

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

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

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

328+ibc i (IBCFragile n r) f = return f { ibc_fragile = (n,r) : ibc_fragile f }

326

329

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

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

328getEntry alt f a = case findEntryByPath f a of

331getEntry alt f a = case findEntryByPath f a of

@@ -392,6 +395,7 @@ process reexp phase archive fn = do

392 processDefs archive

395 processDefs archive

393 processTotal archive

396 processTotal archive

394 processAccess reexp phase archive

397 processAccess reexp phase archive

398+ processFragile archive

395

399

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

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

397timestampOlder src ibc = do

401timestampOlder src ibc = do

@@ -441,6 +445,11 @@ processDeprecate ar = do

441 ns <- getEntry [] "ibc_deprecated" ar

445 ns <- getEntry [] "ibc_deprecated" ar

442 mapM_ (\(n,reason) -> addDeprecated n reason) ns

446 mapM_ (\(n,reason) -> addDeprecated n reason) ns

443

447

448+processFragile :: Archive -> Idris ()

449+processFragile ar = do

450+ ns <- getEntry [] "ibc_fragile" ar

451+ mapM_ (\(n,reason) -> addFragile n reason) ns

452+

444processImportDirs :: Archive -> Idris ()

453processImportDirs :: Archive -> Idris ()

445processImportDirs ar = do

454processImportDirs ar = do

446 fs <- getEntry [] "ibc_importdirs" ar

455 fs <- getEntry [] "ibc_importdirs" ar

src/Idris/Parser.hs+9−3

@@ -535,7 +535,7 @@ syntaxRule syn

535 flip PQuasiquote goal <$> fixBind (q + 1) rens tm

536 fixBind q rens (PUnquote tm) =

537 PUnquote <$> fixBind (q - 1) rens tm

538−

538+

539 fixBind q rens x = descendM (fixBind q rens) x

540

541 gensym :: Name -> IdrisParser Name

@@ -923,11 +923,11 @@ instance_ kwopt syn

923 then [TotalFn]

924 else []

925

926− (doc, argDocs) <- docstring syn

926+ (doc, argDocs) <- docstring syn

927 opts <- fnOpts initOpts

928 acc <- accessibility

929 opts' <- fnOpts opts

930−

930+

931 if kwopt then optional instanceKeyword

932 else do instanceKeyword

933 return (Just ())

@@ -1319,6 +1319,8 @@ Directive' ::= 'lib' CodeGen String_t

1319 | 'error_handlers' Name NameList

1320 | 'language' 'TypeProviders'

1321 | 'language' 'ErrorReflection'

1322+ | 'deprecated' Name String

1323+ | 'fragile' Name Reason

1322 ;

1324 ;

1323@

1325@

1324-}

1326-}

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

1371 n <- fst <$> fnName

1373 n <- fst <$> fnName

1372 alt <- option "" (fst <$> stringLiteral)

1374 alt <- option "" (fst <$> stringLiteral)

1373 return [PDirective (DDeprecate n alt)]

1375 return [PDirective (DDeprecate n alt)]

1376+ <|> do try (lchar '%' *> reserved "fragile")

1377+ n <- fst <$> fnName

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

1379+ return [PDirective (DFragile n alt)]

1374 <|> do fc <- getFC

1380 <|> do fc <- getFC

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

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

1376 fn <- fst <$> fnName

1382 fn <- fst <$> fnName

test/directives001/directives001.idrnew file+28

@@ -0,0 +1,28 @@

1+module directives001

2+

3+%access export

4+

5+

6+data Foo = MkFoo String

7+

8+%deprecate Foo "To be replaced with `Bar`."

9+

10+data Bar : Type where

11+ MkBar : Nat -> Nat -> Bar

12+

13+

14+mkFoo : String -> Foo

15+mkFoo = MkFoo

16+

17+%deprecate mkFoo "To be replaced with `mkBar`."

18+

19+mkBar : Nat -> Bar

20+mkBar a = MkBar a a

21+

22+%fragile mkBar "How `Bar`s are to be created is still being discussed, `mkBar` is subject to change."

23+

24+namespace Main

25+ main : IO ()

26+ main = do

27+ let b = mkBar 1

28+ putStrLn $ "Hello World"

test/directives001/expectednew file+14

@@ -0,0 +1,14 @@

1+directives001.idr:14:7:Use of deprecated name directives001.Foo

2+To be replaced with `Bar`.

3+directives001.idr:14:7:Use of deprecated name directives001.Foo

4+To be replaced with `Bar`.

5+directives001.idr:15:7:Use of deprecated name directives001.Foo

6+To be replaced with `Bar`.

7+directives001.idr:15:7:Use of deprecated name directives001.Foo

8+To be replaced with `Bar`.

9+directives001.idr:26:8:

10+Use of a fragile construct directives001.mkBar

11+How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.

12+directives001.idr:26:8:

13+Use of a fragile construct directives001.mkBar

14+How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.

test/directives001/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ directives001.idr --check --nocolour

3+

4+rm -f directives001 *.ibc