mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 13:36:08 +03:00
Add %deprecate pragma (#2086)
This commit is contained in:
parent
cc45ff957a
commit
0eba4c691e
1
.gitignore
vendored
1
.gitignore
vendored
@ -42,6 +42,7 @@ idris2docs_venv
|
||||
|
||||
# Vim swap file
|
||||
*~
|
||||
*.*.swp
|
||||
# Emacs swap file
|
||||
.\#*
|
||||
# VS Code
|
||||
|
@ -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
|
||||
|
||||
|
@ -1,3 +1,5 @@
|
||||
.. _builtins:
|
||||
|
||||
********
|
||||
Builtins
|
||||
********
|
||||
|
@ -23,5 +23,6 @@ This is a placeholder, to get set up with readthedocs.
|
||||
literate
|
||||
overloadedlit
|
||||
strings
|
||||
pragmas
|
||||
builtins
|
||||
debugging
|
||||
|
101
docs/source/reference/pragmas.rst
Normal file
101
docs/source/reference/pragmas.rst
Normal file
@ -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
|
||||
|
@ -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)
|
||||
|
@ -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 ()
|
||||
|
@ -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"
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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 = []
|
||||
|
@ -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} ->
|
||||
|
@ -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
|
||||
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
||||
|
@ -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
|
||||
|
@ -114,6 +114,8 @@ fnDirectOpt
|
||||
pure Inline
|
||||
<|> do pragma "noinline"
|
||||
pure NoInline
|
||||
<|> do pragma "deprecate"
|
||||
pure Deprecate
|
||||
<|> do pragma "extern"
|
||||
pure ExternFn
|
||||
|
||||
|
@ -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)
|
||||
|
@ -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)
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
23
tests/idris2/warning002/Foo.idr
Normal file
23
tests/idris2/warning002/Foo.idr
Normal file
@ -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
|
||||
|
19
tests/idris2/warning002/Main.idr
Normal file
19
tests/idris2/warning002/Main.idr
Normal file
@ -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
|
||||
|
5
tests/idris2/warning002/deprecated.ipkg
Normal file
5
tests/idris2/warning002/deprecated.ipkg
Normal file
@ -0,0 +1,5 @@
|
||||
package deprecated
|
||||
|
||||
modules = Foo
|
||||
, Main
|
||||
|
18
tests/idris2/warning002/expected
Normal file
18
tests/idris2/warning002/expected
Normal file
@ -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!
|
8
tests/idris2/warning002/run
Executable file
8
tests/idris2/warning002/run
Executable file
@ -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 <<EOF
|
||||
:module Foo
|
||||
:doc dep1
|
||||
EOF
|
||||
|
Loading…
Reference in New Issue
Block a user