diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,9 @@ # New since last release +# New in 1.3.4 ++ Renamed 'forall' function for compability with future GHC releases ++ Updated version bounds ++ Bugfixes # New in 1.3.3 + Updated to work with GHC 8.8 and cabal 3.0 + Bugfixes and documentation updates diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -# Idris +# Idris 1 [![Build Status](https://travis-ci.org/idris-lang/Idris-dev.svg?branch=master)](https://travis-ci.org/idris-lang/Idris-dev) [![Appveyor build](https://ci.appveyor.com/api/projects/status/xi8yu81oy1134g7o/branch/master?svg=true)](https://ci.appveyor.com/project/idrislang/idris-dev) @@ -11,7 +11,7 @@ Idris (https://idris-lang.org/) is a general-purpose functional programming language with dependent types. -## Installation Guides. +## Installation This repository represents the latest development version of the language, and may contain bugs that are being actively worked on. For @@ -26,10 +26,19 @@ Idris has support for external code generators. Supplied with the distribution is a C code generator to compile executables, and a JavaScript code generator -with support for node.js and browser JavaScript. +with support for `node.js` and browser JavaScript. -More information about [code generators can be found on the wiki](https://idris.readthedocs.io/en/latest/reference/codegen.html). +More information about code generators can be found +[here](https://idris.readthedocs.io/en/latest/reference/codegen.html). +## Status + +This is Idris 1, implemented in Haskell. Idris 1 is not actively +worked on anymore. + +[Idris 2](https://github.com/idris-lang/Idris2) is the next generation +of Idris, and where primary development happens. + ## More Information If you would like to find out more information, or ask questions, we @@ -45,5 +54,3 @@ For those interested in contributing to Idris directly we kindly ask that prospective developers please consult the [Contributing Guide](CONTRIBUTING.md) first. -[Idris 2](https://github.com/edwinb/Idris2) is an early preview of the next generation -of Idris, implemented in Idris. diff --git a/codegen/idris-codegen-node/Main.hs b/codegen/idris-codegen-node/Main.hs --- a/codegen/idris-codegen-node/Main.hs +++ b/codegen/idris-codegen-node/Main.hs @@ -7,8 +7,6 @@ import IRTS.CodegenJavaScript import IRTS.Compiler -import Paths_idris - import Control.Monad import System.Environment diff --git a/idris.cabal b/idris.cabal --- a/idris.cabal +++ b/idris.cabal @@ -1,6 +1,6 @@ Cabal-Version: 2.4 Name: idris -Version: 1.3.3 +Version: 1.3.4 License: BSD-3-Clause License-file: LICENSE Author: Edwin Brady @@ -146,7 +146,7 @@ custom-setup setup-depends: - Cabal >= 2.4 && < 3.1, + Cabal >= 2.4 && <= 3.4, base >= 4 && <5, directory, filepath, @@ -166,7 +166,7 @@ -- Defaults to True because Hackage is a source release Flag release Description: This is an official release - Default: True + Default: False manual: True Flag freestanding @@ -319,12 +319,12 @@ , BuildFlags_idris Build-depends: base >=4 && <5 - , aeson >= 0.6 && < 1.5 + , aeson >= 0.6 && < 1.6 , annotated-wl-pprint >= 0.7 && < 0.8 - , ansi-terminal < 0.11 + , ansi-terminal < 0.12 , ansi-wl-pprint < 0.7 , array >= 0.4.0.1 && < 0.6 - , base64-bytestring < 1.2 + , base64-bytestring < 1.3 , binary >= 0.8.4.1 && < 0.9 , blaze-html >= 0.6.1.3 && < 0.10 , blaze-markup >= 0.5.2.1 && < 0.10 @@ -336,12 +336,12 @@ , directory >= 1.2.2.0 && < 1.2.3.0 || > 1.2.3.0 , filepath < 1.5 , fingertree >= 0.1.4.1 && < 0.2 - , haskeline >= 0.7 && < 0.8 + , haskeline >= 0.8 && < 0.9 , ieee754 >= 0.7 && < 0.9 - , megaparsec >= 7.0.4 && < 9 + , megaparsec >= 7.0.4 && < 10 , mtl >= 2.1 && < 2.3 , network >= 2.7 && < 3.1.2 - , optparse-applicative >= 0.13 && < 0.16 + , optparse-applicative >= 0.13 && < 0.17 , parser-combinators >= 1.0.0 , pretty < 1.2 , process < 1.7 @@ -416,7 +416,7 @@ , filepath , directory , haskeline >= 0.7 - , optparse-applicative >= 0.13 && < 0.16 + , optparse-applicative >= 0.13 && < 0.17 , tagged , tasty >= 0.8 , tasty-golden >= 2.0 diff --git a/libs/base/Data/List/Views.idr b/libs/base/Data/List/Views.idr --- a/libs/base/Data/List/Views.idr +++ b/libs/base/Data/List/Views.idr @@ -28,7 +28,7 @@ data Split : List a -> Type where SplitNil : Split [] SplitOne : Split [x] - SplitPair : {x, y : a} -> {xs, ys : List a} -> -- Explicit, don't erae + SplitPair : {x, y : a} -> {xs, ys : List a} -> -- Explicit, don't erase Split (x :: xs ++ y :: ys) splitHelp : (head : a) -> diff --git a/libs/contrib/Network/Socket.idr b/libs/contrib/Network/Socket.idr --- a/libs/contrib/Network/Socket.idr +++ b/libs/contrib/Network/Socket.idr @@ -178,10 +178,10 @@ recvRec : Socket -> List String -> ByteLength -> IO (Either SocketError String) recvRec sock acc n = do res <- recv sock n case res of - Left 0 => pure (Right $ concat $ reverse acc) Left c => pure (Left c) - Right (str, _) => let n' = min (n * 2) 65536 in - recvRec sock (str :: acc) n' + Right (str, res) => let n' = min (n * 2) 65536 in + if res < n then pure (Right $ concat $ reverse $ str :: acc) + else recvRec sock (str :: acc) n' ||| Send a message. ||| diff --git a/rts/arduino/idris_main.c b/rts/arduino/idris_main.c --- a/rts/arduino/idris_main.c +++ b/rts/arduino/idris_main.c @@ -3,6 +3,8 @@ #include "idris_rts.h" #include "Arduino.h" +void* _idris__123_runMain_95_0_125_(VM* vm, VAL* oldbase); + // The default options should give satisfactory results under many circumstances. RTSOpts opts = { .init_heap_size = 128, @@ -15,7 +17,7 @@ init(); // arduino init function VM* vm = init_vm(opts.max_stack_size, opts.init_heap_size, 1); - _idris__123_runMain0_125_(vm, NULL); + _idris__123_runMain_95_0_125_(vm, NULL); #ifdef IDRIS_DEBUG if (opts.show_summary) { diff --git a/src/IRTS/Compiler.hs b/src/IRTS/Compiler.hs --- a/src/IRTS/Compiler.hs +++ b/src/IRTS/Compiler.hs @@ -35,7 +35,6 @@ import Control.Monad.State import Data.List import qualified Data.Map as M -import Data.Maybe (maybe) import Data.Ord import qualified Data.Set as S import System.Directory diff --git a/src/IRTS/JavaScript/Codegen.hs b/src/IRTS/JavaScript/Codegen.hs --- a/src/IRTS/JavaScript/Codegen.hs +++ b/src/IRTS/JavaScript/Codegen.hs @@ -23,10 +23,8 @@ import IRTS.Lang import IRTS.System -import Control.Applicative (pure, (<$>)) import Control.Monad import Control.Monad.Trans.State -import Data.Foldable (foldMap) import Data.Generics.Uniplate.Data import Data.List import Data.Map.Strict (Map) diff --git a/src/IRTS/LangOpts.hs b/src/IRTS/LangOpts.hs --- a/src/IRTS/LangOpts.hs +++ b/src/IRTS/LangOpts.hs @@ -14,9 +14,6 @@ import IRTS.Lang import Control.Monad.State hiding (lift) -import Data.List - -import Debug.Trace inlineAll :: [(Name, LDecl)] -> [(Name, LDecl)] inlineAll lds = let defs = addAlist lds emptyContext in diff --git a/src/IRTS/System.hs b/src/IRTS/System.hs --- a/src/IRTS/System.hs +++ b/src/IRTS/System.hs @@ -27,7 +27,6 @@ #endif import BuildFlags_idris -import Control.Applicative ((<$>)) import Data.List.Split import Data.Maybe (fromMaybe) import System.Environment diff --git a/src/Idris/CmdOptions.hs b/src/Idris/CmdOptions.hs --- a/src/Idris/CmdOptions.hs +++ b/src/Idris/CmdOptions.hs @@ -24,7 +24,6 @@ import Control.Monad.Trans.Reader (ask) import Data.Char import Data.Maybe -import Data.Monoid ((<>)) import Options.Applicative import Options.Applicative.Arrows import Options.Applicative.Types (ReadM(..)) diff --git a/src/Idris/Core/Binary.hs b/src/Idris/Core/Binary.hs --- a/src/Idris/Core/Binary.hs +++ b/src/Idris/Core/Binary.hs @@ -12,7 +12,6 @@ import Idris.Core.TT -import Control.Applicative ((<$>), (<*>)) import Data.Binary import Data.Binary.Get import Data.Binary.Put diff --git a/src/Idris/Core/Elaborate.hs b/src/Idris/Core/Elaborate.hs --- a/src/Idris/Core/Elaborate.hs +++ b/src/Idris/Core/Elaborate.hs @@ -434,8 +434,8 @@ introTy :: Raw -> Maybe Name -> Elab' aux () introTy ty n = processTactic' (IntroTy ty n) -forall :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> Elab' aux () -forall n r i t = processTactic' (Forall n r i t) +forAll :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> Elab' aux () +forAll n r i t = processTactic' (Forall n r i t) letbind :: Name -> RigCount -> Raw -> Raw -> Elab' aux () letbind n rig t v = processTactic' (LetBind n rig t v) @@ -823,7 +823,7 @@ arg n r i tyhole = do ty <- unique_hole tyhole claim ty RType movelast ty - forall n r i (Var ty) + forAll n r i (Var ty) -- try a tactic, if it adds any unification problem, return an error no_errors :: Elab' aux () -> Maybe Err -> Elab' aux () diff --git a/src/Idris/Core/ProofState.hs b/src/Idris/Core/ProofState.hs --- a/src/Idris/Core/ProofState.hs +++ b/src/Idris/Core/ProofState.hs @@ -28,7 +28,6 @@ import Util.Pretty hiding (fill) -import Control.Arrow ((***)) import Control.Monad.State.Strict import Data.List @@ -659,13 +658,13 @@ _ -> lift $ tfail $ CantIntroduce t' intro n ctxt env _ = fail "Can't introduce here." -forall :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> RunTactic -forall n rig impl ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = +forAll :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> RunTactic +forAll n rig impl ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do (tyv, tyt) <- lift $ check ctxt env ty unify' ctxt env (tyt, Nothing) (TType (UVar [] 0), Nothing) unify' ctxt env (t, Nothing) (TType (UVar [] 0), Nothing) return $ Bind n (Pi rig impl tyv (TType (UVar [] 0))) (Bind x (Hole t) (P Bound x t)) -forall n rig impl ty ctxt env _ = fail "Can't pi bind here" +forAll n rig impl ty ctxt env _ = fail "Can't pi bind here" patvar :: Name -> RunTactic patvar n ctxt env (Bind x (Hole t) sc) = @@ -1053,7 +1052,7 @@ mktac WHNF_ComputeArgs = whnf_compute_args mktac (Intro n) = intro n mktac (IntroTy ty n) = introTy ty n - mktac (Forall n r i t) = forall n r i t + mktac (Forall n r i t) = forAll n r i t mktac (LetBind n r t v) = letbind n r t v mktac (ExpandLet n b) = expandLet n b mktac (Rewrite t) = rewrite t diff --git a/src/Idris/Core/TT.hs b/src/Idris/Core/TT.hs --- a/src/Idris/Core/TT.hs +++ b/src/Idris/Core/TT.hs @@ -58,10 +58,10 @@ import Util.Pretty hiding (Str) -- Work around AMP without CPP -import Prelude (Bool(..), Double, Enum(..), Eq(..), FilePath, Functor(..), Int, - Integer, Maybe(..), Monad(..), Monoid(..), Num(..), Ord(..), - Ordering(..), Show(..), String, div, error, fst, max, min, mod, - not, otherwise, read, snd, ($), (&&), (.), (||)) +import Prelude (Bool(..), Double, Enum(..), Eq(..), FilePath, Int, Integer, + Maybe(..), Monoid(..), Num(..), Ord(..), Ordering(..), Show(..), + String, div, error, fst, max, min, mod, not, otherwise, read, + snd, ($), (&&), (.), (||)) #if (MIN_VERSION_base(4,11,0)) import qualified Prelude as S (Semigroup(..)) diff --git a/src/Idris/Delaborate.hs b/src/Idris/Delaborate.hs --- a/src/Idris/Delaborate.hs +++ b/src/Idris/Delaborate.hs @@ -10,7 +10,7 @@ module Idris.Delaborate ( annName, bugaddr, delab, delabWithEnv, delabDirect, delab', delabMV, delabSugared , delabTy, delabTy', fancifyAnnots, pprintDelab, pprintNoDelab - , pprintDelabTy, pprintErr, resugar + , pprintDelabTy', pprintDelabTy, pprintErr, resugar ) where import Idris.AbsSyntax @@ -283,14 +283,18 @@ pprintNoDelab ist tm = annotate (AnnTerm [] tm) (prettyIst ist (delab ist tm)) +pprintDelabTy' :: IState -> Name -> Term -> Doc OutputAnnotation +pprintDelabTy' i n ty + = annotate (AnnTerm [] ty) . prettyIst i $ + case lookupCtxt n (idris_implicits i) of + (imps:_) -> resugar i $ delabTy' i imps [] ty False False True + _ -> resugar i $ delabTy' i [] [] ty False False True + -- | Pretty-print the type of some name pprintDelabTy :: IState -> Name -> Doc OutputAnnotation pprintDelabTy i n = case lookupTy n (tt_ctxt i) of - (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $ - case lookupCtxt n (idris_implicits i) of - (imps:_) -> resugar i $ delabTy' i imps [] ty False False True - _ -> resugar i $ delabTy' i [] [] ty False False True + (ty:_) -> pprintDelabTy' i n ty [] -> error "pprintDelabTy got a name that doesn't exist" pprintTerm :: IState -> PTerm -> Doc OutputAnnotation diff --git a/src/Idris/Docstrings.hs b/src/Idris/Docstrings.hs --- a/src/Idris/Docstrings.hs +++ b/src/Idris/Docstrings.hs @@ -27,11 +27,9 @@ import qualified Cheapskate as C import Cheapskate.Html (renderDoc) import qualified Cheapskate.Types as CT -import Data.Foldable (Foldable) import qualified Data.Foldable as F import qualified Data.Sequence as S import qualified Data.Text as T -import Data.Traversable (Traversable) import GHC.Generics (Generic) import Text.Blaze.Html (Html) diff --git a/src/Idris/Elab/Data.hs b/src/Idris/Elab/Data.hs --- a/src/Idris/Elab/Data.hs +++ b/src/Idris/Elab/Data.hs @@ -32,13 +32,8 @@ import Control.Category import Control.Monad -import Control.Monad.State.Strict as State -import Data.Char (isLetter, toLower) import Data.List -import qualified Data.Map as Map -import Data.Maybe import qualified Data.Set as S -import qualified Data.Text as T warnLC :: FC -> Name -> Idris () warnLC fc n diff --git a/src/Idris/Elab/Term.hs b/src/Idris/Elab/Term.hs --- a/src/Idris/Elab/Term.hs +++ b/src/Idris/Elab/Term.hs @@ -30,7 +30,6 @@ import Idris.Reflection import Idris.Termination (buildSCG, checkDeclTotality, checkPositive) -import Control.Applicative ((<$>)) import Control.Monad import Control.Monad.State.Strict import Data.Foldable (for_) @@ -686,7 +685,7 @@ _ -> unless (LinearTypes `elem` idris_language_extensions ist || e_qq ina) $ lift $ tfail $ At nfc (Msg "You must turn on the LinearTypes extension to use a linear argument") - forall n' (pcount p) (is_scoped p) (Var tyn) + forAll n' (pcount p) (is_scoped p) (Var tyn) addAutoBind p n' addPSname n' -- okay for proof search focus tyn @@ -2108,7 +2107,7 @@ = do ~[n, ty] <- tacTmArgs 2 tac args n' <- reifyTTName n ty' <- reifyRaw ty - forall n' RigW Nothing ty' + forAll n' RigW Nothing ty' returnUnit | n == tacN "Prim__PatVar" = do ~[n] <- tacTmArgs 1 tac args diff --git a/src/Idris/Erasure.hs b/src/Idris/Erasure.hs --- a/src/Idris/Erasure.hs +++ b/src/Idris/Erasure.hs @@ -607,16 +607,13 @@ -- convert applications of lambdas to lets -- note that this transformation preserves de bruijn numbering lamToLet :: Term -> Term - lamToLet tm = lamToLet' args f + lamToLet tm = lamToLet' 0 args f where (f, args) = unApply tm - lamToLet' :: [Term] -> Term -> Term - lamToLet' (v:vs) (Bind n (Lam rig ty) tm) = Bind n (Let rig ty v) $ lamToLet' vs tm - lamToLet' [] tm = tm - lamToLet' vs tm = error $ - "Erasure.hs:lamToLet': unexpected input: " - ++ "vs = " ++ show vs ++ ", tm = " ++ show tm + lamToLet' :: Int -> [Term] -> Term -> Term + lamToLet' wk (v:vs) (Bind n (Lam rig ty) tm) = Bind n (Let rig ty (weakenTm wk v)) $ lamToLet' (wk+1) vs tm + lamToLet' wk vs tm = mkApp tm $ map (weakenTm wk) vs -- split "\x_i -> T(x_i)" into [x_i] and T unfoldLams :: Term -> ([Name], Term) diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs --- a/src/Idris/IBC.hs +++ b/src/Idris/IBC.hs @@ -41,7 +41,7 @@ import System.FilePath ibcVersion :: Word16 -ibcVersion = 166 +ibcVersion = 167 -- | When IBC is being loaded - we'll load different things (and omit -- different structures/definitions) depending on which phase we're in. diff --git a/src/Idris/IdrisDoc.hs b/src/Idris/IdrisDoc.hs --- a/src/Idris/IdrisDoc.hs +++ b/src/Idris/IdrisDoc.hs @@ -29,7 +29,6 @@ import qualified Data.List as L import qualified Data.Map as M hiding ((!)) import Data.Maybe -import Data.Monoid (mempty) import qualified Data.Set as S import qualified Data.Text as T import System.Directory diff --git a/src/Idris/Imports.hs b/src/Idris/Imports.hs --- a/src/Idris/Imports.hs +++ b/src/Idris/Imports.hs @@ -16,7 +16,6 @@ import Idris.Error import IRTS.System (getIdrisLibDir) -import Control.Applicative ((<$>)) import Control.Monad.State.Strict import Data.Char (isAlpha, isDigit, toLower) import Data.List (isSuffixOf) diff --git a/src/Idris/Output.hs b/src/Idris/Output.hs --- a/src/Idris/Output.hs +++ b/src/Idris/Output.hs @@ -37,21 +37,13 @@ #endif import Control.Arrow (first) -import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT) import Data.List (intersperse, nub) import Data.Maybe (fromJust, fromMaybe, isJust, listToMaybe) import qualified Data.Set as S -import System.Console.Haskeline.MonadException (MonadException(controlIO), - RunIO(RunIO)) import System.FilePath (replaceExtension) import System.IO (Handle, hPutStr, hPutStrLn) import System.IO.Error (tryIOError) -instance MonadException m => MonadException (ExceptT Err m) where - controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let - run' = RunIO (fmap ExceptT . run . runExceptT) - in fmap runExceptT $ f run' - pshow :: IState -> Err -> String pshow ist err = displayDecorated (consoleDecorate ist) . renderPretty 1.0 80 . @@ -319,7 +311,7 @@ iputStr s = do i <- getIState case idris_outputmode i of RawOutput h -> runIO $ hPutStr h s - IdeMode n h -> runIO . hPutStr h $ convSExp "write-string" s n + IdeMode n h -> runIO . hPutStrLn h $ convSExp "write-string" s n idemodePutSExp :: SExpable a => String -> a -> Idris () idemodePutSExp cmd info = do i <- getIState diff --git a/src/Idris/Package.hs b/src/Idris/Package.hs --- a/src/Idris/Package.hs +++ b/src/Idris/Package.hs @@ -9,7 +9,6 @@ module Idris.Package where import System.Directory -import System.Directory (copyFile, createDirectoryIfMissing) import System.Environment import System.Exit import System.FilePath (addExtension, addTrailingPathSeparator, dropExtension, diff --git a/src/Idris/Parser/Data.hs b/src/Idris/Parser/Data.hs --- a/src/Idris/Parser/Data.hs +++ b/src/Idris/Parser/Data.hs @@ -12,7 +12,6 @@ import Idris.AbsSyntax import Idris.Core.TT import Idris.Docstrings -import Idris.Options import Idris.Parser.Expr import Idris.Parser.Helpers import Idris.Parser.Ops diff --git a/src/Idris/Parser/Stack.hs b/src/Idris/Parser/Stack.hs --- a/src/Idris/Parser/Stack.hs +++ b/src/Idris/Parser/Stack.hs @@ -84,7 +84,11 @@ (pos, _) = P.reachOffsetNoLine (parseErrorOffset err) (parseErrorPosState err) #endif messageText = PP.text . init . P.parseErrorTextPretty . parseError +#if MIN_VERSION_megaparsec(9,0,0) + messageSource err = sline +#else messageSource err = Just sline +#endif where #if MIN_VERSION_megaparsec(8,0,0) (sline, _) = P.reachOffset (parseErrorOffset err) (parseErrorPosState err) diff --git a/src/Idris/ProofSearch.hs b/src/Idris/ProofSearch.hs --- a/src/Idris/ProofSearch.hs +++ b/src/Idris/ProofSearch.hs @@ -22,7 +22,6 @@ import Idris.Core.Unify import Idris.Delaborate -import Control.Applicative ((<$>)) import Control.Monad import Control.Monad.State.Strict import Data.List diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs --- a/src/Idris/REPL.hs +++ b/src/Idris/REPL.hs @@ -122,23 +122,21 @@ (if colour && not isWindows then colourisePrompt theme str else str) ++ " " - x <- H.catch (H.withInterrupt $ getInputLine prompt) - (ctrlC (return $ Just "")) + x <- H.handleInterrupt (ctrlC (return $ Just "")) (H.withInterrupt $ getInputLine prompt) case x of Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye") return () Just input -> -- H.catch - do ms <- H.catch (H.withInterrupt $ lift $ processInput input orig mods efile) - (ctrlC (return (Just mods))) + do ms <- H.handleInterrupt (ctrlC (return (Just mods))) (H.withInterrupt $ lift $ processInput input orig mods efile) case ms of Just mods -> let efile' = fromMaybe efile (listToMaybe mods) in repl orig mods efile' Nothing -> return () -- ctrlC) -- ctrlC - where ctrlC :: InputT Idris a -> SomeException -> InputT Idris a - ctrlC act e = do lift $ iputStrLn (show e) - act -- repl orig mods + where ctrlC :: InputT Idris a -> InputT Idris a + ctrlC act = do lift $ iputStrLn "Interrupted" + act -- repl orig mods showMVs c thm [] = "" showMVs c thm ms = "Holes: " ++ @@ -258,6 +256,7 @@ idemodeStart s orig mods = do h <- runIO $ if s then initIdemodeSocket else return stdout setIdeMode True h + runIO $ hSetNewlineMode h (NewlineMode { inputNL = CRLF, outputNL = LF }) i <- getIState case idris_outputmode i of IdeMode n h -> @@ -517,7 +516,7 @@ prettyName True False [] n <> case lookupTyExact n ctxt of Just t -> - space <> colon <> space <> align (group (pprintDelab ist t)) + space <> colon <> space <> align (group (pprintDelabTy' ist n t)) Nothing -> empty @@ -682,6 +681,7 @@ iPrintResult "" idemodeProcess fn (Apropos pkg a) = do process fn (Apropos pkg a) iPrintResult "" +idemodeProcess fn (Browse ns) = process fn (Browse ns) idemodeProcess fn (WhoCalls n) = process fn (WhoCalls n) idemodeProcess fn (CallsWho n) = process fn (CallsWho n) idemodeProcess fn (PrintDef n) = process fn (PrintDef n) diff --git a/src/Idris/TypeSearch.hs b/src/Idris/TypeSearch.hs --- a/src/Idris/TypeSearch.hs +++ b/src/Idris/TypeSearch.hs @@ -38,20 +38,18 @@ #else import Prelude hiding (pred) #endif -import Control.Applicative (Applicative(..), (<$>), (<*>), (<|>)) +import Control.Applicative ((<|>)) import Control.Arrow (first, second, (&&&), (***)) import Control.Monad (guard, when) import Data.List (find, partition, (\\)) import Data.Map (Map) import qualified Data.Map as M import Data.Maybe (catMaybes, fromMaybe, isJust, mapMaybe, maybeToList) -import Data.Monoid (Monoid(mappend, mempty)) import Data.Ord (comparing) import qualified Data.PriorityQueue.FingerTree as Q import Data.Set (Set) import qualified Data.Set as S import qualified Data.Text as T (isPrefixOf, pack) -import Data.Traversable (traverse) searchByType :: [PkgName] -> PTerm -> Idris () searchByType pkgs pterm = do diff --git a/src/Util/DynamicLinker.hs b/src/Util/DynamicLinker.hs --- a/src/Util/DynamicLinker.hs +++ b/src/Util/DynamicLinker.hs @@ -25,7 +25,6 @@ import Foreign.Ptr (FunPtr, nullFunPtr, nullPtr) #ifdef linux_HOST_OS import Data.Array (bounds, inRange, (!)) -import Data.Functor ((<$>)) import Data.Maybe (catMaybes) #else import Data.Array (bounds, (!)) diff --git a/test/TestRun.hs b/test/TestRun.hs --- a/test/TestRun.hs +++ b/test/TestRun.hs @@ -6,7 +6,6 @@ import Control.Monad import Data.Char (isLetter) import qualified Data.IntMap as IMap -import Data.Monoid ((<>)) import Data.Proxy import Data.Typeable import Options.Applicative