5950e1e · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+3−2

compare with master

unifiedsplit

@@ -7,6 +7,8 @@ Maintainer : The Idris Community.

7-}

8

9{-# LANGUAGE DeriveFunctor, FlexibleContexts, PatternGuards #-}

10+-- FIXME: {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

11+{-# OPTIONS_GHC -fwarn-unused-imports #-}

10

12

11module Idris.AbsSyntax(

13module Idris.AbsSyntax(

12 module Idris.AbsSyntax

14 module Idris.AbsSyntax

@@ -39,7 +41,6 @@ import System.IO.Error (tryIOError)

39

41

40import Data.Generics.Uniplate.Data (descend, descendM)

42import Data.Generics.Uniplate.Data (descend, descendM)

41

43

42−import Debug.Trace

43import Util.DynamicLinker

44import Util.DynamicLinker

44import Util.Pretty

45import Util.Pretty

45import Util.System

46import Util.System

@@ -597,7 +598,7 @@ getHdrs :: Codegen -> Idris [String]

597getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)

598getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)

598

599

599getImported :: Idris [(FilePath, Bool)]

600getImported :: Idris [(FilePath, Bool)]

600−getImported = do i <- getIState; return (idris_imported i)

601+getImported = idris_imported `fmap` getIState

601

602

602setErrSpan :: FC -> Idris ()

603setErrSpan :: FC -> Idris ()

603setErrSpan x = do i <- getIState;

604setErrSpan x = do i <- getIState;

src/Idris/Completion.hs+11−5

@@ -5,12 +5,16 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8+

9+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

10+{-# OPTIONS_GHC -fwarn-unused-imports #-}

11+

8module Idris.Completion (replCompletion, proverCompletion) where

12module Idris.Completion (replCompletion, proverCompletion) where

9

13

10−import Idris.AbsSyntax (runIO)

14+import Idris.AbsSyntax (runIO, getIState)

11import Idris.AbsSyntaxTree

15import Idris.AbsSyntaxTree

12import Idris.Colours

16import Idris.Colours

13−import Idris.Core.Evaluate (ctxtAlist, definitions)

17+import Idris.Core.Evaluate (ctxtAlist, visibleDefinitions)

14import Idris.Core.TT

18import Idris.Core.TT

15import Idris.Help

19import Idris.Help

16import Idris.Imports (installedPackages)

20import Idris.Imports (installedPackages)

@@ -28,19 +32,21 @@ import qualified Data.Text as T

28import System.Console.ANSI (Color)

32import System.Console.ANSI (Color)

29import System.Console.Haskeline

33import System.Console.Haskeline

30

34

35+commands :: [String]

31commands = [ n | (names, _, _) <- allHelp ++ extraHelp, n <- names ]

36commands = [ n | (names, _, _) <- allHelp ++ extraHelp, n <- names ]

32

37

33tacticArgs :: [(String, Maybe TacticArg)]

38tacticArgs :: [(String, Maybe TacticArg)]

34tacticArgs = [ (name, args) | (names, args, _) <- Idris.Parser.Expr.tactics

39tacticArgs = [ (name, args) | (names, args, _) <- Idris.Parser.Expr.tactics

35 , name <- names ]

40 , name <- names ]

41+

42+tactics :: [String]

36tactics = map fst tacticArgs

43tactics = map fst tacticArgs

37

44

38-- | Get the user-visible names from the current interpreter state.

45-- | Get the user-visible names from the current interpreter state.

39names :: Idris [String]

46names :: Idris [String]

40−names = do i <- get

41− let ctxt = tt_ctxt i

47+names = do ctxt <- tt_ctxt <$> getIState

42 return $

48 return $

43− mapMaybe nameString (allNames $ definitions ctxt) ++

49+ mapMaybe nameString (allNames (visibleDefinitions ctxt)) ++

44 "Type" : map fst Idris.Parser.Expr.constants

50 "Type" : map fst Idris.Parser.Expr.constants

45 where

51 where

46 -- We need both fully qualified names and identifiers that map to them

52 -- We need both fully qualified names and identifiers that map to them

src/Idris/Core/Evaluate.hs+13−4

@@ -5,9 +5,11 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8+

8{-# LANGUAGE BangPatterns, DeriveGeneric, FlexibleInstances,

9{-# LANGUAGE BangPatterns, DeriveGeneric, FlexibleInstances,

9 MultiParamTypeClasses, PatternGuards #-}

10 MultiParamTypeClasses, PatternGuards #-}

10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

11{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

12+{-# OPTIONS_GHC -fwarn-unused-imports #-}

11

13

12module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

14module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

13 normaliseAll, normaliseBlocking, toValue, quoteTerm,

15 normaliseAll, normaliseBlocking, toValue, quoteTerm,

@@ -28,20 +30,19 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

28 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,

30 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,

29 conGuarded,

31 conGuarded,

30 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

32 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

33+ visibleDefinitions,

31 isUniverse, linearCheck, linearCheckArg) where

34 isUniverse, linearCheck, linearCheckArg) where

32

35

33import Idris.Core.CaseTree

36import Idris.Core.CaseTree

34import Idris.Core.TT

37import Idris.Core.TT

35

38

36−import Control.Applicative hiding (Const)

37import Control.Monad.State

39import Control.Monad.State

38−import Data.Binary hiding (get, put)

39−import qualified Data.Binary as B

40import Data.List

41import Data.Maybe (listToMaybe)

42−import Debug.Trace

43import GHC.Generics (Generic)

42import GHC.Generics (Generic)

44

43

44+import qualified Data.Map.Strict as Map

45+

45data EvalState = ES { limited :: [(Name, Int)],

46data EvalState = ES { limited :: [(Name, Int)],

46 nexthole :: Int,

47 nexthole :: Int,

47 blocking :: Bool }

48 blocking :: Bool }

@@ -1152,6 +1153,14 @@ conGuarded ctxt n tm = guarded n tm

1152 isConName f ctxt = any (guarded n) as

1153 isConName f ctxt = any (guarded n) as

1153 guarded _ _ = False

1154 guarded _ _ = False

1154

1155

1156+visibleDefinitions :: Context -> Ctxt TTDecl

1157+visibleDefinitions ctxt =

1158+ Map.filter (\m -> length m > 0) . Map.map onlyVisible . definitions $ ctxt

1159+ where

1160+ onlyVisible = Map.filter visible

1161+ visible (_def, _rigCount, _injectivity, accessibility, _totality, _metaInformation) =

1162+ accessibility `notElem` [Hidden, Private]

1163+

1155lookupP :: Name -> Context -> [Term]

1164lookupP :: Name -> Context -> [Term]

1156lookupP = lookupP_all False False

1165lookupP = lookupP_all False False

1157

1166

src/Idris/IBC.hs+24−19

@@ -5,20 +5,20 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8+

8{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}

9{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}

9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

11+{-# OPTIONS_GHC -fwarn-unused-imports #-}

10

12

11module Idris.IBC (loadIBC, loadPkgIndex,

13module Idris.IBC (loadIBC, loadPkgIndex,

12 writeIBC, writePkgIndex,

14 writeIBC, writePkgIndex,

13 hasValidIBCVersion, IBCPhase(..)) where

15 hasValidIBCVersion, IBCPhase(..)) where

14

16

15import Idris.AbsSyntax

17import Idris.AbsSyntax

16−import Idris.Core.Binary

17import Idris.Core.CaseTree

18import Idris.Core.CaseTree

18import Idris.Core.Evaluate

19import Idris.Core.Evaluate

19import Idris.Core.TT

20import Idris.Core.TT

20−import Idris.DeepSeq

21+import Idris.DeepSeq ()

21−import Idris.Delaborate

22import Idris.Docstrings (Docstring)

23import qualified Idris.Docstrings as D

24import Idris.Error

@@ -27,23 +27,15 @@ import Idris.Options

27import Idris.Output

28import IRTS.System (getIdrisLibDir)

29

30−import Paths_idris

31−

32import qualified Cheapskate.Types as CT

30import qualified Cheapskate.Types as CT

33import Codec.Archive.Zip

31import Codec.Archive.Zip

34import Control.DeepSeq

32import Control.DeepSeq

35import Control.Monad

33import Control.Monad

36−import Control.Monad.State.Strict hiding (get, put)

37−import qualified Control.Monad.State.Strict as ST

38import Data.Binary

34import Data.Binary

39import Data.ByteString.Lazy as B hiding (elem, length, map)

35import Data.ByteString.Lazy as B hiding (elem, length, map)

40−import Data.Functor

41import Data.List as L

36import Data.List as L

42import Data.Maybe (catMaybes)

37import Data.Maybe (catMaybes)

43import qualified Data.Set as S

38import qualified Data.Set as S

44−import qualified Data.Text as T

45−import Data.Vector.Binary

46−import Debug.Trace

47import System.Directory

39import System.Directory

48import System.FilePath

40import System.FilePath

49

41

@@ -131,7 +123,9 @@ loadIBC :: Bool -- ^ True = reexport, False = make everything private

131 -> IBCPhase

123 -> IBCPhase

132 -> FilePath -> Idris ()

124 -> FilePath -> Idris ()

133loadIBC reexport phase fp

125loadIBC reexport phase fp

126+ = do logIBC 1 $ "loadIBC (reexport, phase, fp)" ++ show (reexport, phase, fp)

134− = do imps <- getImported

127+ imps <- getImported

128+ logIBC 3 $ "loadIBC imps" ++ show imps

135 case lookup fp imps of

129 case lookup fp imps of

136 Nothing -> load True

130 Nothing -> load True

137 Just p -> if (not p && reexport) then load False else return ()

131 Just p -> if (not p && reexport) then load False else return ()

@@ -517,13 +511,15 @@ processImports reexp phase fname ar = do

517 ibcsd <- valIBCSubDir i

511 ibcsd <- valIBCSubDir i

518 ids <- rankedImportDirs fname

512 ids <- rankedImportDirs fname

519 putIState (i { imported = f : imported i })

513 putIState (i { imported = f : imported i })

520− let phase' = case phase of

514+ let (phase', reexp') = case phase of

521− IBC_REPL _ -> IBC_REPL False

515+ IBC_REPL True -> (IBC_REPL False, reexp)

522− p -> p

516+ IBC_REPL False -> (IBC_Building, reexp && re)

517+ p -> (p, reexp && re)

523 fp <- findIBC ids ibcsd f

518 fp <- findIBC ids ibcsd f

519+ logIBC 4 $ "processImports (fp, phase')" ++ show (fp, phase')

524 case fp of

520 case fp of

525 Nothing -> do logIBC 2 $ "Failed to load ibc " ++ f

521 Nothing -> do logIBC 2 $ "Failed to load ibc " ++ f

526− Just fn -> do loadIBC (reexp && re) phase' fn) fs

522+ Just fn -> do loadIBC reexp' phase' fn) fs

527

523

528processImplicits :: Archive -> Idris ()

524processImplicits :: Archive -> Idris ()

529processImplicits ar = do

525processImplicits ar = do

@@ -639,6 +635,7 @@ processPatternDefs ar = do

639processDefs :: Archive -> Idris ()

635processDefs :: Archive -> Idris ()

640processDefs ar = do

636processDefs ar = do

641 ds <- getEntry [] "ibc_defs" ar

637 ds <- getEntry [] "ibc_defs" ar

638+ logIBC 4 $ "processDefs ds" ++ show ds

642 mapM_ (\ (n, d) -> do

639 mapM_ (\ (n, d) -> do

643 d' <- updateDef d

640 d' <- updateDef d

644 case d' of

641 case d' of

@@ -735,8 +732,11 @@ processAccess :: Bool -- ^ Reexporting?

735 -> IBCPhase

732 -> IBCPhase

736 -> Archive -> Idris ()

733 -> Archive -> Idris ()

737processAccess reexp phase ar = do

734processAccess reexp phase ar = do

735+ logIBC 3 $ "processAccess (reexp, phase)" ++ show (reexp, phase)

738 ds <- getEntry [] "ibc_access" ar

736 ds <- getEntry [] "ibc_access" ar

737+ logIBC 3 $ "processAccess ds" ++ show ds

739 mapM_ (\ (n, a_in) -> do

738 mapM_ (\ (n, a_in) -> do

739+

740 let a = if reexp then a_in else Hidden

741 logIBC 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a

742 updateIState (\i -> i { tt_ctxt = setAccess n a (tt_ctxt i) })

@@ -745,10 +745,15 @@ processAccess reexp phase ar = do

745 then do

746 logIBC 2 $ "Not exporting " ++ show n

747 setAccessibility n Hidden

748+ else

748− else logIBC 2 $ "Exporting " ++ show n

749+ logIBC 2 $ "Exporting " ++ show n

750+

749 -- Everything should be available at the REPL from

751 -- Everything should be available at the REPL from

750− -- things imported publicly

752+ -- things imported publicly.

753+ when (phase == IBC_REPL True) $ do

754+ logIBC 2 $ "Top level, exporting " ++ show n

751− when (phase == IBC_REPL True) $ setAccessibility n Public) ds

755+ setAccessibility n Public

756+ ) ds

752

757

753processFlags :: Archive -> Idris ()

758processFlags :: Archive -> Idris ()

754processFlags ar = do

759processFlags ar = do

src/Idris/ModeCommon.hs+22−23

@@ -4,6 +4,11 @@ Description : Common utilities used by all modes.

4License : BSD3

5Maintainer : The Idris Community.

6-}

7+

8+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

9+{-# OPTIONS_GHC -fwarn-unused-binds #-}

10+{-# OPTIONS_GHC -fwarn-unused-imports #-}

11+

7module Idris.ModeCommon where

12module Idris.ModeCommon where

8

13

9import Idris.AbsSyntax

14import Idris.AbsSyntax

@@ -25,16 +30,11 @@ import Prelude hiding (id, (.), (<$>))

25import Control.Category

30import Control.Category

26import Control.DeepSeq

31import Control.DeepSeq

27import Control.Monad

32import Control.Monad

28−import Control.Monad.Trans.State.Strict (get)

29−import Data.List hiding (group)

30−import Data.Maybe

31import Network.Socket (PortNumber)

33import Network.Socket (PortNumber)

32−import System.Directory

33

34

34defaultPort :: PortNumber

35defaultPort :: PortNumber

35defaultPort = fromIntegral 4294

36defaultPort = fromIntegral 4294

36

37

37−

38loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]

39loadInputs inputs toline -- furthest line to read in input source files

40 = idrisCatch

@@ -49,6 +49,8 @@ loadInputs inputs toline -- furthest line to read in input source files

49 [] -> not (NoREPL `elem` opts)

50 _ -> True

51

52+ logParser 3 $ show "loadInputs loadCode" ++ show loadCode

53+

52 -- For each ifile list, check it and build ibcs in the same clean IState

54 -- For each ifile list, check it and build ibcs in the same clean IState

53 -- so that they don't interfere with each other when checking

55 -- so that they don't interfere with each other when checking

54

56

@@ -59,6 +61,7 @@ loadInputs inputs toline -- furthest line to read in input source files

59 let ninputs = zip [1..] inputs

61 let ninputs = zip [1..] inputs

60 ifiles <- mapWhileOK (\(num, input) ->

62 ifiles <- mapWhileOK (\(num, input) ->

61 do putIState ist

63 do putIState ist

64+ logParser 3 $ show "loadInputs (num, input)" ++ show (num, input)

62 modTree <- buildTree

65 modTree <- buildTree

63 (map snd (take (num-1) ninputs))

66 (map snd (take (num-1) ninputs))

64 importlists

67 importlists

@@ -77,9 +80,18 @@ loadInputs inputs toline -- furthest line to read in input source files

77 case errSpan inew of

80 case errSpan inew of

78 Nothing ->

81 Nothing ->

79 do putIState $!! ist { idris_tyinfodata = tidata }

82 do putIState $!! ist { idris_tyinfodata = tidata }

80− ibcfiles <- mapM findNewIBC (nub (concatMap snd ifiles))

83+ logParser 3 $ "loadInputs ifiles" ++ show ifiles

81−-- logLvl 0 $ "Loading from " ++ show ibcfiles

84+

85+ let fileToIFileType :: FilePath -> Idris IFileType

86+ fileToIFileType file = do

87+ ibcsd <- valIBCSubDir ist

88+ ids <- rankedImportDirs file

89+ findImport ids ibcsd file

90+

91+ ibcfiles <- mapM fileToIFileType inputs

92+ logParser 3 $ show "loadInputs ibcfiles" ++ show ibcfiles

93+

82− tryLoad True (IBC_REPL True) (mapMaybe id ibcfiles)

94+ tryLoad True (IBC_REPL True) ibcfiles

83 _ -> return ()

95 _ -> return ()

84 exports <- findExports

96 exports <- findExports

85

97

@@ -103,6 +115,8 @@ loadInputs inputs toline -- furthest line to read in input source files

103 tryLoad keepstate phase [] = warnTotality >> return ()

115 tryLoad keepstate phase [] = warnTotality >> return ()

104 tryLoad keepstate phase (f : fs)

116 tryLoad keepstate phase (f : fs)

105 = do ist <- getIState

117 = do ist <- getIState

118+ logParser 3 $ "tryLoad (keepstate, phase, f : fs)" ++

119+ show (keepstate, phase, f : fs)

106 let maxline

120 let maxline

107 = case toline of

121 = case toline of

108 Nothing -> Nothing

122 Nothing -> Nothing

@@ -142,21 +156,6 @@ loadInputs inputs toline -- furthest line to read in input source files

142 fmatch xs ('.':'/':ys) = fmatch xs ys

156 fmatch xs ('.':'/':ys) = fmatch xs ys

143 fmatch xs ys = xs == ys

157 fmatch xs ys = xs == ys

144

158

145− findNewIBC :: IFileType -> Idris (Maybe IFileType)

146− findNewIBC i@(IBC _ _) = return (Just i)

147− findNewIBC s@(IDR f) = do ist <- get

148− ibcsd <- valIBCSubDir ist

149− let ibc = ibcPathNoFallback ibcsd f

150− ok <- runIO $ doesFileExist ibc

151− if ok then return (Just (IBC ibc s))

152− else return Nothing

153− findNewIBC s@(LIDR f) = do ist <- get

154− ibcsd <- valIBCSubDir ist

155− let ibc = ibcPathNoFallback ibcsd f

156− ok <- runIO $ doesFileExist ibc

157− if ok then return (Just (IBC ibc s))

158− else return Nothing

159−

160 -- Like mapM, but give up when there's an error

159 -- Like mapM, but give up when there's an error

161 mapWhileOK f [] = return []

160 mapWhileOK f [] = return []

162 mapWhileOK f (x : xs) = do x' <- f x

161 mapWhileOK f (x : xs) = do x' <- f x

src/Idris/Parser.hs+6−17

@@ -5,9 +5,13 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8+

8{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,

9{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,

9 PatternGuards #-}

10 PatternGuards #-}

10{-# OPTIONS_GHC -O0 #-}

11{-# OPTIONS_GHC -O0 #-}

12+-- FIXME: {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

13+{-# OPTIONS_GHC -fwarn-unused-imports #-}

14+

11module Idris.Parser(module Idris.Parser,

15module Idris.Parser(module Idris.Parser,

12 module Idris.Parser.Expr,

16 module Idris.Parser.Expr,

13 module Idris.Parser.Data,

17 module Idris.Parser.Data,

@@ -17,11 +21,9 @@ module Idris.Parser(module Idris.Parser,

17import Idris.AbsSyntax hiding (namespace, params)

21import Idris.AbsSyntax hiding (namespace, params)

18import Idris.Core.Evaluate

22import Idris.Core.Evaluate

19import Idris.Core.TT

23import Idris.Core.TT

20−import Idris.Coverage

21import Idris.Delaborate

24import Idris.Delaborate

22import Idris.Docstrings hiding (Unchecked)

25import Idris.Docstrings hiding (Unchecked)

23import Idris.DSL

26import Idris.DSL

24−import Idris.Elab.Term

25import Idris.Elab.Value

27import Idris.Elab.Value

26import Idris.ElabDecls

28import Idris.ElabDecls

27import Idris.Error

29import Idris.Error

@@ -33,15 +35,11 @@ import Idris.Parser.Data

33import Idris.Parser.Expr

35import Idris.Parser.Expr

34import Idris.Parser.Helpers

36import Idris.Parser.Helpers

35import Idris.Parser.Ops

37import Idris.Parser.Ops

36−import Idris.Providers

37import Idris.Termination

38import Idris.Termination

38import Idris.Unlit

39import Idris.Unlit

39

40

40−import Util.DynamicLinker

41import qualified Util.Pretty as P

42−import Util.System (readSource, writeSource)

42+import Util.System (readSource)

43−

44−import Paths_idris

45

43

46import Prelude hiding (pi)

44import Prelude hiding (pi)

47

45

@@ -53,24 +51,14 @@ import Data.Char

53import Data.Foldable (asum)

51import Data.Foldable (asum)

54import Data.Function

52import Data.Function

55import Data.Generics.Uniplate.Data (descendM)

53import Data.Generics.Uniplate.Data (descendM)

56−import qualified Data.HashSet as HS

57import Data.List

54import Data.List

58import qualified Data.List.Split as Spl

55import qualified Data.List.Split as Spl

59import qualified Data.Map as M

56import qualified Data.Map as M

60import Data.Maybe

57import Data.Maybe

61−import Data.Monoid

62import Data.Ord

58import Data.Ord

63−import qualified Data.Set as S

64import qualified Data.Text as T

59import qualified Data.Text as T

65−import Debug.Trace

66import qualified System.Directory as Dir (makeAbsolute)

60import qualified System.Directory as Dir (makeAbsolute)

67import System.FilePath

61import System.FilePath

68−import System.IO

69−import qualified Text.Parser.Char as Chr

70−import Text.Parser.Expression

71−import Text.Parser.LookAhead

72−import qualified Text.Parser.Token as Tok

73−import qualified Text.Parser.Token.Highlight as Hi

74import Text.PrettyPrint.ANSI.Leijen (Doc, plain)

62import Text.PrettyPrint.ANSI.Leijen (Doc, plain)

75import qualified Text.PrettyPrint.ANSI.Leijen as ANSI

63import qualified Text.PrettyPrint.ANSI.Leijen as ANSI

76import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

64import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

@@ -1685,6 +1673,7 @@ loadModule' f phase

1685loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()

1673loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()

1686loadFromIFile reexp phase i@(IBC fn src) maxline

1674loadFromIFile reexp phase i@(IBC fn src) maxline

1687 = do logParser 1 $ "Skipping " ++ getSrcFile i

1675 = do logParser 1 $ "Skipping " ++ getSrcFile i

1676+ logParser 3 $ "loadFromIFile i" ++ show i

1688 idrisCatch (loadIBC reexp phase fn)

1677 idrisCatch (loadIBC reexp phase fn)

1689 (\err -> ierror $ LoadingFailed fn err)

1678 (\err -> ierror $ LoadingFailed fn err)

1690 where

1679 where

src/Idris/REPL.hs+6−4

@@ -6,6 +6,8 @@ Maintainer : The Idris Community.

6-}

7

8{-# LANGUAGE FlexibleContexts, PatternGuards #-}

9+-- FIXME: {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

10+{-# OPTIONS_GHC -fwarn-unused-imports #-}

9

11

10module Idris.REPL

12module Idris.REPL

11 ( idemodeStart

13 ( idemodeStart

@@ -49,7 +51,6 @@ import Idris.Core.Execute (execute)

49import Idris.Core.TT

51import Idris.Core.TT

50import Idris.Core.Unify

52import Idris.Core.Unify

51import Idris.Core.WHNF

53import Idris.Core.WHNF

52−import Idris.Coverage

53import Idris.DataOpts

54import Idris.DataOpts

54import Idris.Delaborate

55import Idris.Delaborate

55import Idris.Docs

56import Idris.Docs

@@ -98,8 +99,6 @@ import Util.Pretty hiding ((</>))

98import Util.System

99import Util.System

99import Version_idris (gitHash)

100import Version_idris (gitHash)

100

101

101−import Debug.Trace

102−

103-- | Run the REPL

102-- | Run the REPL

104repl :: IState -- ^ The initial state

103repl :: IState -- ^ The initial state

105 -> [FilePath] -- ^ The loaded modules

104 -> [FilePath] -- ^ The loaded modules

@@ -981,7 +980,7 @@ process fn (Check (PRef _ _ n))

981 = do ctxt <- getContext

980 = do ctxt <- getContext

982 ist <- getIState

981 ist <- getIState

983 let ppo = ppOptionIst ist

982 let ppo = ppOptionIst ist

984− case lookupNames n ctxt of

983+ case lookupVisibleNames n ctxt of

985 ts@(t:_) ->

984 ts@(t:_) ->

986 case lookup t (idris_metavars ist) of

985 case lookup t (idris_metavars ist) of

987 Just (_, i, _, _, _) -> iRenderResult . fmap (fancifyAnnots ist True) $

986 Just (_, i, _, _, _) -> iRenderResult . fmap (fancifyAnnots ist True) $

@@ -989,6 +988,9 @@ process fn (Check (PRef _ _ n))

989 Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)

988 Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)

990 [] -> iPrintError $ "No such variable " ++ show n

989 [] -> iPrintError $ "No such variable " ++ show n

991 where

990 where

991+ lookupVisibleNames :: Name -> Context -> [Name]

992+ lookupVisibleNames n ctxt = map fst $ lookupCtxtName n (visibleDefinitions ctxt)

993+

992 showMetavarInfo ppo ist n i

994 showMetavarInfo ppo ist n i

993 = case lookupTy n (tt_ctxt ist) of

995 = case lookupTy n (tt_ctxt ist) of

994 (ty:_) -> let ty' = normaliseC (tt_ctxt ist) [] ty in

996 (ty:_) -> let ty' = normaliseC (tt_ctxt ist) [] ty in

test/interactive018/Bar.idrdeleted−10

@@ -1,10 +0,0 @@

1−module Bar

2−

3−import Foo

4−

5−bar_private : Nat -> Nat

6−bar_private n = n

7−

8−export

9−bar_visible : Nat -> Nat

10−bar_visible n = n

test/interactive018/Foo.idrdeleted−8

@@ -1,8 +0,0 @@

1−module Foo

2−

3−foo_private : Nat -> Nat

4−foo_private n = n

5−

6−export

7−foo_visible : Nat -> Nat

8−foo_visible n = n

test/interactive018/Imported1.idrnew file+10

@@ -0,0 +1,10 @@

1+module Imported1

2+

3+import Imported2

4+

5+imported1_private : a -> a

6+imported1_private a = a

7+

8+export

9+imported1_visible : a -> a

10+imported1_visible a = a

test/interactive018/Imported2.idrnew file+8

@@ -0,0 +1,8 @@

1+module Imported1

2+

3+imported2_private : a -> a

4+imported2_private a = a

5+

6+export

7+imported2_visible : a -> a

8+imported2_visible a = a

test/interactive018/Public1.idrnew file+10

@@ -0,0 +1,10 @@

1+module Public1

2+

3+import public Public2

4+

5+public1_private : a -> a

6+public1_private a = a

7+

8+export

9+public1_visible : a -> a

10+public1_visible a = a

test/interactive018/Public2.idrnew file+8

@@ -0,0 +1,8 @@

1+module Public2

2+

3+public2_private : a -> a

4+public2_private a = a

5+

6+export

7+public2_visible : a -> a

8+public2_visible a = a

test/interactive018/Top.idrnew file+11

@@ -0,0 +1,11 @@

1+module Top

2+

3+import Imported1

4+import public Public1

5+

6+top_private : a -> a

7+top_private a = a

8+

9+export

10+top_visible : a -> a

11+top_visible a = a

test/interactive018/expected+20−4

@@ -1,4 +1,20 @@

1−bar_private : Nat -> Nat

1+1 : Integer

2−bar_visible : Nat -> Nat

2+top_private : a -> a

3+1 : Integer

4+top_visible : a -> a

5+No such variable imported1_private

6+No such variable imported1_private

7+1 : Integer

8+imported1_visible : a -> a

9+No such variable imported2_private

10+No such variable imported2_private

11+No such variable imported2_visible

12+No such variable imported2_visible

13+No such variable public1_private

14+No such variable public1_private

15+1 : Integer

16+public1_visible : a -> a

3−No such variable foo_private

17+No such variable public2_private

4−foo_visible : Nat -> Nat

18+No such variable public2_private

19+1 : Integer

20+public2_visible : a -> a

test/interactive018/input+20−4

@@ -1,4 +1,20 @@

1−:t bar_private

1+top_private 1

2−:t bar_visible

2+:t top_private

3−:t foo_private

3+top_visible 1

4−:t foo_visible

4+:t top_visible

5+imported1_private 1

6+:t imported1_private

7+imported1_visible 1

8+:t imported1_visible

9+imported2_private 1

10+:t imported2_private

11+imported2_visible 1

12+:t imported2_visible

13+public1_private 1

14+:t public1_private

15+public1_visible 1

16+:t public1_visible

17+public2_private 1

18+:t public2_private

19+public2_visible 1

20+:t public2_visible

test/interactive018/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none Bar.idr < input

2+${IDRIS:-idris} $@ --quiet --port none Top.idr < input

3rm -f *.ibc