git.iko.soy/Idris-dev
on master help sign in
Add deprecation warning for %elim

The command-line option --no-elim-deprecation-warnings turns it off, so that users wanting to write backwards-compatible libraries can still run it.

commit90bbf061dc33e714f4d75232caab8981da195ed5 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 10 Sep 2015, 18:00 (11 years ago) parentb28fecf
7 files changed+19−6
compare with master
unifiedsplit
libs/base/Debug/Error.idr+1−1 libs/base/base.ipkg+1−1 libs/prelude/prelude.ipkg+1−1 src/Idris/AbsSyntaxTree.hs+1 src/Idris/CmdOptions.hs+1 src/Idris/DeepSeq.hs+2−1 src/Idris/ParseData.hs+12−2
libs/base/Debug/Error.idr+1−1
@@ -8,7 +8,7 @@ import System
88||| @ loc The source location to display for the error
99||| @ message The error to print
1010partial
11−error : {default tactics {sourceLocation} loc : SourceLocation} ->
11+error : {default (%runElab sourceLocation) loc : SourceLocation} ->
1212 (message : String) ->
1313 a
1414error {loc = FileLoc filename (line, col) _} message =
libs/base/base.ipkg+1−1
@@ -1,6 +1,6 @@
11package base
22
3−opts = "--nobasepkgs --total -i ../prelude"
3+opts = "--nobasepkgs --total --no-elim-deprecation-warnings -i ../prelude"
44modules = System,
55
66 Debug.Error, Debug.Trace,
libs/prelude/prelude.ipkg+1−1
@@ -1,6 +1,6 @@
11package prelude
22
3−opts = "--nobuiltins --total"
3+opts = "--nobuiltins --total --no-elim-deprecation-warnings"
44modules = Builtins, Prelude, IO,
55
66 Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,
src/Idris/AbsSyntaxTree.hs+1
@@ -503,6 +503,7 @@ data Opt = Filename String
503503 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
504504 | UseConsoleWidth ConsoleWidth
505505 | DumpHighlights
506+ | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim
506507 deriving (Show, Eq)
507508
508509data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm
src/Idris/CmdOptions.hs+1
@@ -148,6 +148,7 @@ parseFlags = many $
148148
149149 <|> (UseConsoleWidth <$> option (str >>= parseConsoleWidth) (long "consolewidth" <> metavar "WIDTH" <> help "Select console width: auto, infinite, nat"))
150150 <|> flag' DumpHighlights (long "highlight" <> help "Emit source code highlighting")
151+ <|> flag' NoElimDeprecationWarnings (long "no-elim-deprecation-warnings" <> help "Disable deprecation warnings for %elim")
151152
152153 where
153154 getExt s = case maybeRead s of
src/Idris/DeepSeq.hs+2−1
@@ -160,7 +160,8 @@ instance NFData Opt where
160160 rnf (AutoWidth) = ()
161161 rnf (AutoSolve) = ()
162162 rnf (UseConsoleWidth cw) = rnf cw `seq` ()
163− rnf (DumpHighlights) = ()
163+ rnf DumpHighlights = ()
164+ rnf NoElimDeprecationWarnings = ()
164165
165166
166167instance NFData TIData where
src/Idris/ParseData.hs+12−2
@@ -157,11 +157,21 @@ DefaultEliminator ::= 'noelim'?
157157 -}
158158dataOpts :: DataOpts -> IdrisParser DataOpts
159159dataOpts opts
160− = do reserved "%elim"; dataOpts (DefaultEliminator : DefaultCaseFun : opts)
161− <|> do reserved "%case"; dataOpts (DefaultCaseFun : opts)
160+ = do fc <- reservedFC "%elim"
161+ warnElim fc
162+ dataOpts (DefaultEliminator : DefaultCaseFun : opts)
163+ <|> do fc <- reservedFC "%case"
164+ warnElim fc
165+ dataOpts (DefaultCaseFun : opts)
162166 <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)
163167 <|> return opts
164168 <?> "data options"
169+ where warnElim fc =
170+ do ist <- get
171+ let cmdline = opt_cmdline (idris_options ist)
172+ unless (NoElimDeprecationWarnings `elem` cmdline) $
173+ put ist { parserWarnings =
174+ (fc, Msg "Eliminator generation is deprecated. Use an eliminator generator in a library instead.") : parserWarnings ist }
165175
166176{- | Parses a data type declaration
167177Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?