diff --git a/.gitignore b/.gitignore index a164cee55..cfbb1d398 100644 --- a/.gitignore +++ b/.gitignore @@ -42,6 +42,7 @@ idris2docs_venv # Vim swap file *~ +*.*.swp # Emacs swap file .\#* # VS Code diff --git a/CHANGELOG.md b/CHANGELOG.md index 0ff146488..c553ba646 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -37,6 +37,7 @@ * Removes deprecated support for `void` primitive. Now `void` is supported via `prim__void`. +* Adds `%deprecate` pragma that can be used to warn when deprecated functions are used. ### Library changes diff --git a/docs/source/reference/builtins.rst b/docs/source/reference/builtins.rst index 658f75ba4..54782e250 100644 --- a/docs/source/reference/builtins.rst +++ b/docs/source/reference/builtins.rst @@ -1,3 +1,5 @@ +.. _builtins: + ******** Builtins ******** diff --git a/docs/source/reference/index.rst b/docs/source/reference/index.rst index 32a179c26..054e553f7 100644 --- a/docs/source/reference/index.rst +++ b/docs/source/reference/index.rst @@ -23,5 +23,6 @@ This is a placeholder, to get set up with readthedocs. literate overloadedlit strings + pragmas builtins debugging diff --git a/docs/source/reference/pragmas.rst b/docs/source/reference/pragmas.rst new file mode 100644 index 000000000..3d0189118 --- /dev/null +++ b/docs/source/reference/pragmas.rst @@ -0,0 +1,101 @@ +******** +Pragmas +******** + +.. role:: idris(code) + :language: idris + +Idris2 supports a number of pragmas (identifiable by the `%` prefix). Some pragmas change compiler behavior +until the behavior is changed back using the same pragma while others apply to the following declaration. A +small niche of pragmas apply directly to one or more arguments instead of the code following the pragma +(like the `%name` pragma described below). + +.. note:: + This page is a work in progress. If you know about a pragma that is not described yet, please consider + submitting a pull request! + + +``%builtin`` +==================== + +The ``%builtin Natural`` pragma converts recursive/unary representations of natural numbers +into primitive ``Integer`` representations. + +This pragma is explained in detail on its own page. For more, see :ref:`builtins`. + +``%deprecate`` +==================== + +Mark the following definition as deprecated. Whenever the function is used, Idris will show a deprecation +warning. + +.. code-block:: idris + + %deprecate + foo : String -> String + foo x = x ++ "!" + + bar : String + bar = foo "hello" + +.. code-block:: none + + Warning: Deprecation warning: Man.foo is deprecated and will be removed in a future version. + +You can use code documentation (triple vertical bar `||| docs`) to suggest a strategy for removing the +deprecated function call and that documentation will be displayed alongside the warning. + +.. code-block:: idris + + ||| Please use the @altFoo@ function from now on. + %deprecate + foo : String -> String + foo x = x ++ "!" + + bar : String + bar = foo "hello" + +.. code-block:: none + + Warning: Deprecation warning: Man.foo is deprecated and will be removed in a future version. + Please use the @altFoo@ function from now on. + +``%inline`` +==================== + +Instruct the compiler to inline the following definition when it is applied. It is generally best to let the +compiler and the backend you are using optimize code based on its predetermined rules, but if you want to +force a function to be inlined when it is called, this pragma will force it. + +.. code-block:: idris + + %inline + foo : String -> String + foo x = x ++ "!" + +``%noinline`` +==================== + +Instruct the compiler _not_ to inline the following definition when it is applied. It is generally best to let the +compiler and the backend you are using optimize code based on its predetermined rules, but if you want to +force a function to never be inlined when it is called, this pragma will force it. + +.. code-block:: idris + + %noinline + foo : String -> String + foo x = x ++ "!" + +``%name`` +==================== + +Give the compiler some suggested names to use for a particular type when it is asked to generate names for values. +You can specify any number of suggested names; they will be used in-order when more than one is needed for a single +definition. + +.. code-block:: idris + + data Foo = X | Y + + %name Foo foo,bar + diff --git a/libs/base/Language/Reflection/TTImp.idr b/libs/base/Language/Reflection/TTImp.idr index 9fd1b984f..1dc54ab6c 100644 --- a/libs/base/Language/Reflection/TTImp.idr +++ b/libs/base/Language/Reflection/TTImp.idr @@ -99,6 +99,7 @@ mutual data FnOpt : Type where Inline : FnOpt NoInline : FnOpt + Deprecate : FnOpt TCInline : FnOpt -- Flag means the hint is a direct hint, not a function which might -- find the result (e.g. chasing parent interface dictionaries) diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index e93261cf0..6a7806d82 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -33,7 +33,7 @@ import public Libraries.Utils.Binary ||| (Increment this when changing anything in the data format) export ttcVersion : Int -ttcVersion = 68 +ttcVersion = 69 export checkTTCVersion : String -> Int -> Int -> Core () diff --git a/src/Core/Context/Context.idr b/src/Core/Context/Context.idr index 7d1c99779..0e2910c04 100644 --- a/src/Core/Context/Context.idr +++ b/src/Core/Context/Context.idr @@ -200,6 +200,8 @@ public export data DefFlag = Inline | NoInline + | ||| A definition has been marked as deprecated + Deprecate | Invertible -- assume safe to cancel arguments in unification | Overloadable -- allow ad-hoc overloads | TCInline -- always inline before totality checking @@ -234,6 +236,7 @@ export Eq DefFlag where (==) Inline Inline = True (==) NoInline NoInline = True + (==) Deprecate Deprecate = True (==) Invertible Invertible = True (==) Overloadable Overloadable = True (==) TCInline TCInline = True @@ -251,6 +254,7 @@ export Show DefFlag where show Inline = "inline" show NoInline = "noinline" + show Deprecate = "deprecate" show Invertible = "invertible" show Overloadable = "overloadable" show TCInline = "tcinline" diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 64afcbafa..e86cfa9c7 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -68,7 +68,9 @@ data Warning : Type where UnreachableClause : {vars : _} -> FC -> Env Term vars -> Term vars -> Warning ShadowingGlobalDefs : FC -> List1 (String, List1 Name) -> Warning - Deprecated : String -> Warning + ||| A warning about a deprecated definition. Supply an FC and Name to + ||| have the documentation for the definition printed with the warning. + Deprecated : String -> Maybe (FC, Name) -> Warning GenericWarn : String -> Warning -- All possible errors, carrying a location @@ -189,7 +191,7 @@ Show Warning where show (ParserWarning _ msg) = msg show (UnreachableClause _ _ _) = ":Unreachable clause" show (ShadowingGlobalDefs _ _) = ":Shadowing names" - show (Deprecated name) = ":Deprecated " ++ name + show (Deprecated name _) = ":Deprecated " ++ name show (GenericWarn msg) = msg @@ -368,7 +370,7 @@ getWarningLoc : Warning -> Maybe FC getWarningLoc (ParserWarning fc _) = Just fc getWarningLoc (UnreachableClause fc _ _) = Just fc getWarningLoc (ShadowingGlobalDefs fc _) = Just fc -getWarningLoc (Deprecated _) = Nothing +getWarningLoc (Deprecated _ fcAndName) = fst <$> fcAndName getWarningLoc (GenericWarn _) = Nothing export diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index f076d69e5..884c919fd 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -1029,6 +1029,7 @@ TTC NoMangleDirective where TTC DefFlag where toBuf b Inline = tag 2 toBuf b NoInline = tag 13 + toBuf b Deprecate = tag 15 toBuf b Invertible = tag 3 toBuf b Overloadable = tag 4 toBuf b TCInline = tag 5 @@ -1056,6 +1057,7 @@ TTC DefFlag where 12 => do x <- fromBuf b; pure (Identity x) 13 => pure NoInline 14 => do x <- fromBuf b; pure (NoMangle x) + 15 => pure Deprecate _ => corrupt "DefFlag" export diff --git a/src/Idris/Doc/Annotations.idr b/src/Idris/Doc/Annotations.idr index fea9ed9e9..803e9c6bf 100644 --- a/src/Idris/Doc/Annotations.idr +++ b/src/Idris/Doc/Annotations.idr @@ -13,6 +13,7 @@ import Libraries.Text.PrettyPrint.Prettyprinter public export data IdrisDocAnn = Header + | Deprecation | Declarations | Decl Name | DocStringBody @@ -28,6 +29,7 @@ docToDecoration _ = Nothing export styleAnn : IdrisDocAnn -> AnsiStyle styleAnn Header = underline +styleAnn Deprecation = bold styleAnn Declarations = [] styleAnn (Decl{}) = [] styleAnn DocStringBody = [] diff --git a/src/Idris/Doc/String.idr b/src/Idris/Doc/String.idr index 674ed739d..1ebe4aa99 100644 --- a/src/Idris/Doc/String.idr +++ b/src/Idris/Doc/String.idr @@ -201,10 +201,12 @@ getDocsForPrimitive constant = do public export data Config : Type where ||| Configuration of the printer for a name + ||| @ showType Do we show the type? ||| @ longNames Do we print qualified names? ||| @ dropFirst Do we drop the first argument in the type? ||| @ getTotality Do we print the totality status of the function? - MkConfig : {default True longNames : Bool} -> + MkConfig : {default True showType : Bool} -> + {default True longNames : Bool} -> {default False dropFirst : Bool} -> {default True getTotality : Bool} -> Config @@ -219,17 +221,27 @@ data Config : Type where export methodsConfig : Config methodsConfig - = MkConfig {longNames = False} + = MkConfig {showType = True} + {longNames = False} {dropFirst = True} {getTotality = False} export shortNamesConfig : Config shortNamesConfig - = MkConfig {longNames = False} + = MkConfig {showType = True} + {longNames = False} {dropFirst = False} {getTotality = True} +export +justUserDoc : Config +justUserDoc + = MkConfig {showType = False} + {longNames = False} + {dropFirst = True} + {getTotality = False} + export getDocsForName : {auto o : Ref ROpts REPLOpts} -> {auto c : Ref Ctxt Defs} -> @@ -418,7 +430,7 @@ getDocsForName fc n config pure (map (\ cons => tot ++ cons ++ idoc) cdoc) _ => pure (Nothing, []) - showDoc (MkConfig {longNames, dropFirst, getTotality}) (n, str) + showDoc (MkConfig {showType, longNames, dropFirst, getTotality}) (n, str) = do defs <- get Ctxt Just def <- lookupCtxtExact n (gamma defs) | Nothing => undefinedName fc n @@ -441,7 +453,9 @@ getDocsForName fc n config let cat = showCategory Syntax def let nm = prettyKindedName typ $ cat $ ifThenElse longNames (pretty (show nm)) (prettyName nm) - let docDecl = annotate (Decl n) (hsep [nm, colon, prettyTerm ty]) + let deprecated = if Deprecate `elem` def.flags + then annotate Deprecation "=DEPRECATED=" <+> line else emptyDoc + let docDecl = deprecated <+> annotate (Decl n) (hsep [nm, colon, prettyTerm ty]) -- Finally add the user-provided docstring let docText = let docs = reflowDoc str in @@ -454,7 +468,8 @@ getDocsForName fc n config in annotate DocStringBody (concatWith (\l, r => l <+> hardline <+> r) docs) <$ guard (not (null docs)) - pure (vcat (docDecl :: docBody)) + let maybeDocDecl = [docDecl | showType] + pure . vcat . catMaybes $ maybeDocDecl :: (map Just $ docBody) export getDocsForPTerm : {auto o : Ref ROpts REPLOpts} -> diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index fcbda2c96..fe3682ade 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -8,6 +8,7 @@ import Core.Metadata import Core.Options import Core.Value +import Idris.Doc.String import Idris.REPL.Opts import Idris.Resugar import Idris.Syntax @@ -179,8 +180,11 @@ pwarning (ShadowingGlobalDefs fc ns) :: reflow "is shadowing" :: punctuate comma (map pretty (forget ns)) -pwarning (Deprecated s) - = pure $ pretty "Deprecation warning:" <++> pretty s +pwarning (Deprecated s fcAndName) + = do docs <- traverseOpt (\(fc, name) => getDocsForName fc name justUserDoc) fcAndName + pure . vsep $ catMaybes [ Just $ pretty "Deprecation warning:" <++> pretty s + , map (const UserDocString) <$> docs + ] pwarning (GenericWarn s) = pure $ pretty s diff --git a/src/Idris/IDEMode/SyntaxHighlight.idr b/src/Idris/IDEMode/SyntaxHighlight.idr index 2d53b8a48..8b6d1c754 100644 --- a/src/Idris/IDEMode/SyntaxHighlight.idr +++ b/src/Idris/IDEMode/SyntaxHighlight.idr @@ -61,17 +61,19 @@ syntaxToProperties syn = mkDecor <$> syntaxToDecoration syn export annToProperties : IdrisAnn -> Maybe Properties -annToProperties Warning = Nothing -annToProperties Error = Nothing -annToProperties ErrorDesc = Nothing -annToProperties FileCtxt = Nothing -annToProperties Code = Nothing -annToProperties Meta = Nothing -annToProperties (Syntax syn) = syntaxToProperties syn +annToProperties Warning = Nothing +annToProperties Error = Nothing +annToProperties ErrorDesc = Nothing +annToProperties FileCtxt = Nothing +annToProperties Code = Nothing +annToProperties Meta = Nothing +annToProperties (Syntax syn) = syntaxToProperties syn +annToProperties UserDocString = Nothing export docToProperties : IdrisDocAnn -> Maybe Properties docToProperties Header = pure $ mkFormat Underline +docToProperties Deprecation = pure $ mkFormat Bold docToProperties Declarations = Nothing docToProperties (Decl _) = Nothing docToProperties DocStringBody = Nothing diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index a4bc752d6..0ffe0ea53 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -210,7 +210,7 @@ addField : {auto c : Ref Ctxt Defs} -> DescField -> PkgDesc -> Core PkgDesc addField (PVersion fc n) pkg = pure $ record { version = Just n } pkg addField (PVersionDep fc n) pkg - = do emitWarning (Deprecated "version numbers must now be of the form x.y.z") + = do emitWarning (Deprecated "version numbers must now be of the form x.y.z" Nothing) pure pkg addField (PAuthors fc a) pkg = pure $ record { authors = Just a } pkg addField (PMaintainers fc a) pkg = pure $ record { maintainers = Just a } pkg diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index cca345fa8..e682809ec 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1386,6 +1386,9 @@ fnDirectOpt fname <|> do pragma "noinline" commit pure $ IFnOpt NoInline + <|> do pragma "deprecate" + commit + pure $ IFnOpt Deprecate <|> do pragma "tcinline" commit pure $ IFnOpt TCInline diff --git a/src/Idris/Pretty.idr b/src/Idris/Pretty.idr index bad3c2632..ee62595cc 100644 --- a/src/Idris/Pretty.idr +++ b/src/Idris/Pretty.idr @@ -61,6 +61,7 @@ data IdrisAnn | Code | Meta | Syntax IdrisSyntax + | UserDocString export annToDecoration : IdrisAnn -> Maybe Decoration @@ -86,6 +87,7 @@ colorAnn FileCtxt = color BrightBlue colorAnn Code = color Magenta colorAnn Meta = color Green colorAnn (Syntax syn) = syntaxAnn syn +colorAnn UserDocString = [] export warning : Doc IdrisAnn -> Doc IdrisAnn diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index fadb12008..4074507e3 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -34,16 +34,21 @@ checkVisibleNS fc (NS ns x) vis else throw $ InvisibleName fc (NS ns x) (Just ns) checkVisibleNS _ _ _ = pure () +onLHS : ElabMode -> Bool +onLHS (InLHS _) = True +onLHS _ = False + -- Get the type of a variable, assuming we haven't found it in the nested -- names. Look in the Env first, then the global context. getNameType : {vars : _} -> {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> {auto e : Ref EST (EState vars)} -> + ElabMode -> RigCount -> Env Term vars -> FC -> Name -> Core (Term vars, Glued vars) -getNameType rigc env fc x +getNameType elabMode rigc env fc x = case defined x env of Just (MkIsDefined rigb lv) => do rigSafe rigb rigc @@ -71,6 +76,8 @@ getNameType rigc env fc x [(pname, i, def)] <- lookupCtxtName x (gamma defs) | ns => ambiguousName fc x (map fst ns) checkVisibleNS fc (fullname def) (visibility def) + when (not $ onLHS elabMode) $ + checkDeprecation fc def rigSafe (multiplicity def) rigc let nt = fromMaybe Func (defNameType $ definition def) @@ -91,17 +98,26 @@ getNameType rigc env fc x rigSafe lhs rhs = when (lhs < rhs) (throw (LinearMisuse fc !(getFullName x) lhs rhs)) + checkDeprecation : FC -> GlobalDef -> Core () + checkDeprecation fc gdef = + do when (Deprecate `elem` gdef.flags) $ + recordWarning $ + Deprecated + "\{show gdef.fullname} is deprecated and will be removed in a future version." + (Just (fc, gdef.fullname)) + -- Get the type of a variable, looking it up in the nested names first. getVarType : {vars : _} -> {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> {auto e : Ref EST (EState vars)} -> + ElabMode -> RigCount -> NestedNames vars -> Env Term vars -> FC -> Name -> Core (Term vars, Nat, Glued vars) -getVarType rigc nest env fc x +getVarType elabMode rigc nest env fc x = case lookup x (names nest) of - Nothing => do (tm, ty) <- getNameType rigc env fc x + Nothing => do (tm, ty) <- getNameType elabMode rigc env fc x pure (tm, 0, ty) Just (nestn, argns, tmf) => do defs <- get Ctxt @@ -320,10 +336,6 @@ mutual needsDelayLHS (IWithUnambigNames _ _ t) = needsDelayLHS t needsDelayLHS _ = pure False - onLHS : ElabMode -> Bool - onLHS (InLHS _) = True - onLHS _ = False - needsDelay : {auto c : Ref Ctxt Defs} -> ElabMode -> (knownRet : Bool) -> RawImp -> @@ -783,10 +795,10 @@ checkApp rig elabinfo nest env fc (IAutoApp fc' fn arg) expargs autoargs namedar checkApp rig elabinfo nest env fc (INamedApp fc' fn nm arg) expargs autoargs namedargs exp = checkApp rig elabinfo nest env fc' fn expargs autoargs ((nm, arg) :: namedargs) exp checkApp rig elabinfo nest env fc (IVar fc' n) expargs autoargs namedargs exp - = do (ntm, arglen, nty_in) <- getVarType rig nest env fc' n + = do (ntm, arglen, nty_in) <- getVarType elabinfo.elabMode rig nest env fc' n nty <- getNF nty_in prims <- getPrimitiveNames - elabinfo <- updateElabInfo prims (elabMode elabinfo) n expargs elabinfo + elabinfo <- updateElabInfo prims elabinfo.elabMode n expargs elabinfo addNameLoc fc' n diff --git a/src/TTImp/Elab/Check.idr b/src/TTImp/Elab/Check.idr index 382b3eb09..ddfba1f84 100644 --- a/src/TTImp/Elab/Check.idr +++ b/src/TTImp/Elab/Check.idr @@ -34,6 +34,7 @@ isLHS : ElabMode -> Maybe RigCount isLHS (InLHS w) = Just w isLHS _ = Nothing +export Show ElabMode where show InType = "InType" show (InLHS c) = "InLHS " ++ show c diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index a40faa778..d01ec2f86 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -114,6 +114,8 @@ fnDirectOpt pure Inline <|> do pragma "noinline" pure NoInline + <|> do pragma "deprecate" + pure Deprecate <|> do pragma "extern" pure ExternFn diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index a461094dc..0a23c8dc7 100644 --- a/src/TTImp/ProcessDef.idr +++ b/src/TTImp/ProcessDef.idr @@ -1140,7 +1140,7 @@ processDef opts nest env fc n_in cs_in -- Filter out the ones which are actually matched (perhaps having -- come up due to some overlapping patterns) missMatch <- traverse (checkMatched covcs) (mapMaybe id missImp) - let miss = mapMaybe id missMatch + let miss = catMaybes missMatch if isNil miss then do [] <- getNonCoveringRefs fc (Resolved n) | ns => toFullNames (NonCoveringCall ns) diff --git a/src/TTImp/ProcessType.idr b/src/TTImp/ProcessType.idr index 4fab2a39c..5d1772f47 100644 --- a/src/TTImp/ProcessType.idr +++ b/src/TTImp/ProcessType.idr @@ -49,6 +49,8 @@ processFnOpt fc _ ndef Inline processFnOpt fc _ ndef NoInline = do throwIfHasFlag fc ndef Inline "%inline and %noinline are mutually exclusive" setFlag fc ndef NoInline +processFnOpt fc _ ndef Deprecate + = setFlag fc ndef Deprecate processFnOpt fc _ ndef TCInline = setFlag fc ndef TCInline processFnOpt fc True ndef (Hint d) diff --git a/src/TTImp/Reflect.idr b/src/TTImp/Reflect.idr index faf450c96..f842bd907 100644 --- a/src/TTImp/Reflect.idr +++ b/src/TTImp/Reflect.idr @@ -290,6 +290,7 @@ mutual = case (dropAllNS !(full (gamma defs) n), args) of (UN (Basic "Inline"), _) => pure Inline (UN (Basic "NoInline"), _) => pure NoInline + (UN (Basic "Deprecate"), _) => pure Deprecate (UN (Basic "TCInline"), _) => pure TCInline (UN (Basic "Hint"), [(_, x)]) => do x' <- reify defs !(evalClosure defs x) @@ -666,6 +667,7 @@ mutual Reflect FnOpt where reflect fc defs lhs env Inline = getCon fc defs (reflectionttimp "Inline") reflect fc defs lhs env NoInline = getCon fc defs (reflectionttimp "NoInline") + reflect fc defs lhs env Deprecate = getCon fc defs (reflectionttimp "Deprecate") reflect fc defs lhs env TCInline = getCon fc defs (reflectionttimp "TCInline") reflect fc defs lhs env (Hint x) = do x' <- reflect fc defs lhs env x diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index a93627cb9..226a09788 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -216,6 +216,8 @@ mutual data FnOpt' : Type -> Type where Inline : FnOpt' nm NoInline : FnOpt' nm + ||| Mark a function as deprecated. + Deprecate : FnOpt' nm TCInline : FnOpt' nm -- Flag means the hint is a direct hint, not a function which might -- find the result (e.g. chasing parent interface dictionaries) @@ -247,6 +249,7 @@ mutual Show nm => Show (FnOpt' nm) where show Inline = "%inline" show NoInline = "%noinline" + show Deprecate = "%deprecate" show TCInline = "%tcinline" show (Hint t) = "%hint " ++ show t show (GlobalHint t) = "%globalhint " ++ show t @@ -271,6 +274,7 @@ mutual Eq FnOpt where Inline == Inline = True NoInline == NoInline = True + Deprecate == Deprecate = True TCInline == TCInline = True (Hint x) == (Hint y) = x == y (GlobalHint x) == (GlobalHint y) = x == y @@ -1265,6 +1269,7 @@ mutual toBuf b Inline = tag 0 toBuf b NoInline = tag 12 toBuf b TCInline = tag 11 + toBuf b Deprecate = tag 14 toBuf b (Hint t) = do tag 1; toBuf b t toBuf b (GlobalHint t) = do tag 2; toBuf b t toBuf b ExternFn = tag 3 @@ -1293,6 +1298,7 @@ mutual 11 => pure TCInline 12 => pure NoInline 13 => do name <- fromBuf b; pure (NoMangle name) + 14 => pure Deprecate _ => corrupt "FnOpt" export diff --git a/src/TTImp/TTImp/Functor.idr b/src/TTImp/TTImp/Functor.idr index a893a0e98..7ad717267 100644 --- a/src/TTImp/TTImp/Functor.idr +++ b/src/TTImp/TTImp/Functor.idr @@ -112,6 +112,7 @@ mutual Functor FnOpt' where map f Inline = Inline map f NoInline = NoInline + map f Deprecate = Deprecate map f TCInline = TCInline map f (Hint b) = Hint b map f (GlobalHint b) = GlobalHint b diff --git a/tests/Main.idr b/tests/Main.idr index 20dd49cc0..59bf9db10 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -61,7 +61,7 @@ idrisTestsCasetree = MkTestPool "Case tree building" [] Nothing idrisTestsWarning : TestPool idrisTestsWarning = MkTestPool "Warnings" [] Nothing - ["warning001"] + ["warning001", "warning002"] idrisTestsError : TestPool idrisTestsError = MkTestPool "Error messages" [] Nothing diff --git a/tests/idris2/warning002/Foo.idr b/tests/idris2/warning002/Foo.idr new file mode 100644 index 000000000..91797b30b --- /dev/null +++ b/tests/idris2/warning002/Foo.idr @@ -0,0 +1,23 @@ +module Foo + +%deprecate +export +dep1 : String +dep1 = "hello" + +||| Just use the string "world" directly from now on. +%deprecate +export +dep2 : String +dep2 = "world" + +%deprecate +export +dep3 : String -> String +dep3 x = x ++ "!" + +%deprecate +public export +0 foo : (0 a : Type) -> Type +foo x = List x + diff --git a/tests/idris2/warning002/Main.idr b/tests/idris2/warning002/Main.idr new file mode 100644 index 000000000..294e6630d --- /dev/null +++ b/tests/idris2/warning002/Main.idr @@ -0,0 +1,19 @@ +module Main + +import Foo + +testConstValue1 : String +testConstValue1 = dep1 + +testConstValue2 : String +testConstValue2 = dep2 + +testFunctionPass : String -> String +testFunctionPass = dep3 + +testErasedFunction : List Int -> Foo.foo Int +testErasedFunction xs = xs + +0 testInErasedContext : Type +testInErasedContext = foo Int + diff --git a/tests/idris2/warning002/deprecated.ipkg b/tests/idris2/warning002/deprecated.ipkg new file mode 100644 index 000000000..04ec9c10b --- /dev/null +++ b/tests/idris2/warning002/deprecated.ipkg @@ -0,0 +1,5 @@ +package deprecated + +modules = Foo + , Main + diff --git a/tests/idris2/warning002/expected b/tests/idris2/warning002/expected new file mode 100644 index 000000000..38f19de38 --- /dev/null +++ b/tests/idris2/warning002/expected @@ -0,0 +1,18 @@ +1/2: Building Foo (Foo.idr) +2/2: Building Main (Main.idr) +Warning: Deprecation warning: Foo.dep1 is deprecated and will be removed in a future version. + +Warning: Deprecation warning: Foo.dep2 is deprecated and will be removed in a future version. + Just use the string "world" directly from now on. +Warning: Deprecation warning: Foo.dep3 is deprecated and will be removed in a future version. + +Warning: Deprecation warning: Foo.foo is deprecated and will be removed in a future version. + +Warning: Deprecation warning: Foo.foo is deprecated and will be removed in a future version. + +Foo> Imported module Foo +Foo> =DEPRECATED= +Foo.dep1 : String + +Foo> +Bye for now! diff --git a/tests/idris2/warning002/run b/tests/idris2/warning002/run new file mode 100755 index 000000000..c3e3b212d --- /dev/null +++ b/tests/idris2/warning002/run @@ -0,0 +1,8 @@ +rm -rf ./build + +$1 --no-color --console-width 0 --build deprecated.ipkg +$1 --no-color --no-banner --console-width 0 Foo.idr <