07b7138 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+2−2

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

77-}

88

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

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

1011

1112module Idris.AbsSyntax(

1213 module Idris.AbsSyntax

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

3940

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

4142

42−import Debug.Trace

4343import Util.DynamicLinker

4444import Util.Pretty

4545import Util.System

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

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

598598

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

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

600+getImported = idris_imported `fmap` getIState

601601

602602setErrSpan :: FC -> Idris ()

603603setErrSpan x = do i <- getIState;

src/Idris/Completion.hs+11−5

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

55License : BSD3

66Maintainer : The Idris Community.

77-}

8+

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

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

11+

812module Idris.Completion (replCompletion, proverCompletion) where

913

10−import Idris.AbsSyntax (runIO)

14+import Idris.AbsSyntax (getIState, runIO)

1115import Idris.AbsSyntaxTree

1216import Idris.Colours

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

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

1418import Idris.Core.TT

1519import Idris.Help

1620import Idris.Imports (installedPackages)

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

2832import System.Console.ANSI (Color)

2933import System.Console.Haskeline

3034

35+commands :: [String]

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

3237

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

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

3540 , name <- names ]

41+

42+tactics :: [String]

3643tactics = map fst tacticArgs

3744

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

3946names :: Idris [String]

40−names = do i <- get

41− let ctxt = tt_ctxt i

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

4248 return $

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

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

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

4551 where

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

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

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

55License : BSD3

66Maintainer : The Idris Community.

77-}

8+

89{-# LANGUAGE BangPatterns, DeriveGeneric, FlexibleInstances,

910 MultiParamTypeClasses, PatternGuards #-}

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

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

1113

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

1315 normaliseAll, normaliseBlocking, toValue, quoteTerm,

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

2830 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,

2931 conGuarded,

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

33+ visibleDefinitions,

3134 isUniverse, linearCheck, linearCheckArg) where

3235

3336import Idris.Core.CaseTree

3437import Idris.Core.TT

3538

36−import Control.Applicative hiding (Const)

3739import Control.Monad.State

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

39−import qualified Data.Binary as B

4040import Data.List

4141import Data.Maybe (listToMaybe)

42−import Debug.Trace

4342import GHC.Generics (Generic)

4443

44+import qualified Data.Map.Strict as Map

45+

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

4647 nexthole :: Int,

4748 blocking :: Bool }

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

11521153 isConName f ctxt = any (guarded n) as

11531154 guarded _ _ = False

11541155

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+

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

11561165lookupP = lookupP_all False False

11571166

src/Idris/IBC.hs+25−19

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

55License : BSD3

66Maintainer : The Idris Community.

77-}

8+

89{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}

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

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

1012

1113module Idris.IBC (loadIBC, loadPkgIndex,

1214 writeIBC, writePkgIndex,

1315 hasValidIBCVersion, IBCPhase(..)) where

1416

1517import Idris.AbsSyntax

16−import Idris.Core.Binary

1718import Idris.Core.CaseTree

1819import Idris.Core.Evaluate

1920import Idris.Core.TT

20−import Idris.DeepSeq

21−import Idris.Delaborate

21+import Idris.DeepSeq ()

2222import Idris.Docstrings (Docstring)

2323import qualified Idris.Docstrings as D

2424import Idris.Error

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

2727import Idris.Output

2828import IRTS.System (getIdrisLibDir)

2929

30−import Paths_idris

31−

3230import qualified Cheapskate.Types as CT

3331import Codec.Archive.Zip

3432import Control.DeepSeq

3533import Control.Monad

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

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

3834import Data.Binary

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

40−import Data.Functor

4136import Data.List as L

4237import Data.Maybe (catMaybes)

4338import qualified Data.Set as S

44−import qualified Data.Text as T

45−import Data.Vector.Binary

46−import Debug.Trace

4739import System.Directory

4840import System.FilePath

4941

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

131123 -> IBCPhase

132124 -> FilePath -> Idris ()

133125loadIBC reexport phase fp

134− = do imps <- getImported

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

127+ imps <- getImported

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

135129 case lookup fp imps of

136130 Nothing -> load True

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

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

517511 ibcsd <- valIBCSubDir i

518512 ids <- rankedImportDirs fname

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

520− let phase' = case phase of

521− IBC_REPL _ -> IBC_REPL False

522− p -> p

514+ let (phase', reexp') =

515+ case phase of

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

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

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

523519 fp <- findIBC ids ibcsd f

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

524521 case fp of

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

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

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

527524

528525processImplicits :: Archive -> Idris ()

529526processImplicits ar = do

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

639636processDefs :: Archive -> Idris ()

640637processDefs ar = do

641638 ds <- getEntry [] "ibc_defs" ar

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

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

643641 d' <- updateDef d

644642 case d' of

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

735733 -> IBCPhase

736734 -> Archive -> Idris ()

737735processAccess reexp phase ar = do

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

738737 ds <- getEntry [] "ibc_access" ar

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

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

740+

740741 let a = if reexp then a_in else Hidden

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

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

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

745746 then do

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

747748 setAccessibility n Hidden

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

749+ else

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

751+

749752 -- Everything should be available at the REPL from

750− -- things imported publicly

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

753+ -- things imported publicly.

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

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

756+ setAccessibility n Public

757+ ) ds

752758

753759processFlags :: Archive -> Idris ()

754760processFlags ar = do

src/Idris/ModeCommon.hs+22−23

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

44License : BSD3

55Maintainer : The Idris Community.

66-}

7+

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

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

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

11+

712module Idris.ModeCommon where

813

914import Idris.AbsSyntax

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

2530import Control.Category

2631import Control.DeepSeq

2732import Control.Monad

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

29−import Data.List hiding (group)

30−import Data.Maybe

3133import Network.Socket (PortNumber)

32−import System.Directory

3334

3435defaultPort :: PortNumber

3536defaultPort = fromIntegral 4294

3637

37−

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

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

4040 = idrisCatch

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

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

5050 _ -> True

5151

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

53+

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

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

5456

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

5961 let ninputs = zip [1..] inputs

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

6163 do putIState ist

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

6265 modTree <- buildTree

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

6467 importlists

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

7780 case errSpan inew of

7881 Nothing ->

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

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

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

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

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

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+

94+ tryLoad True (IBC_REPL True) ibcfiles

8395 _ -> return ()

8496 exports <- findExports

8597

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

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

104116 tryLoad keepstate phase (f : fs)

105117 = do ist <- getIState

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

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

106120 let maxline

107121 = case toline of

108122 Nothing -> Nothing

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

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

143157 fmatch xs ys = xs == ys

144158

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−

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

161160 mapWhileOK f [] = return []

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

src/Idris/Parser.hs+6−17

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

55License : BSD3

66Maintainer : The Idris Community.

77-}

8+

89{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,

910 PatternGuards #-}

1011{-# OPTIONS_GHC -O0 #-}

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

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

14+

1115module Idris.Parser(module Idris.Parser,

1216 module Idris.Parser.Expr,

1317 module Idris.Parser.Data,

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

1721import Idris.AbsSyntax hiding (namespace, params)

1822import Idris.Core.Evaluate

1923import Idris.Core.TT

20−import Idris.Coverage

2124import Idris.Delaborate

2225import Idris.Docstrings hiding (Unchecked)

2326import Idris.DSL

24−import Idris.Elab.Term

2527import Idris.Elab.Value

2628import Idris.ElabDecls

2729import Idris.Error

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

3335import Idris.Parser.Expr

3436import Idris.Parser.Helpers

3537import Idris.Parser.Ops

36−import Idris.Providers

3738import Idris.Termination

3839import Idris.Unlit

3940

40−import Util.DynamicLinker

4141import qualified Util.Pretty as P

42−import Util.System (readSource, writeSource)

43−

44−import Paths_idris

42+import Util.System (readSource)

4543

4644import Prelude hiding (pi)

4745

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

5351import Data.Foldable (asum)

5452import Data.Function

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

56−import qualified Data.HashSet as HS

5754import Data.List

5855import qualified Data.List.Split as Spl

5956import qualified Data.Map as M

6057import Data.Maybe

61−import Data.Monoid

6258import Data.Ord

63−import qualified Data.Set as S

6459import qualified Data.Text as T

65−import Debug.Trace

6660import qualified System.Directory as Dir (makeAbsolute)

6761import 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

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

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

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

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

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

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

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

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

16881677 idrisCatch (loadIBC reexp phase fn)

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

16901679 where

src/Idris/REPL.hs+6−4

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

66-}

77

88{-# LANGUAGE FlexibleContexts, PatternGuards #-}

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

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

911

1012module Idris.REPL

1113 ( idemodeStart

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

4951import Idris.Core.TT

5052import Idris.Core.Unify

5153import Idris.Core.WHNF

52−import Idris.Coverage

5354import Idris.DataOpts

5455import Idris.Delaborate

5556import Idris.Docs

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

9899import Util.System

99100import Version_idris (gitHash)

100101

101−import Debug.Trace

102−

103102-- | Run the REPL

104103repl :: IState -- ^ The initial state

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

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

981980 = do ctxt <- getContext

982981 ist <- getIState

983982 let ppo = ppOptionIst ist

984− case lookupNames n ctxt of

983+ case lookupVisibleNames n ctxt of

985984 ts@(t:_) ->

986985 case lookup t (idris_metavars ist) of

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

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

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

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

991990 where

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

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

993+

992994 showMetavarInfo ppo ist n i

993995 = case lookupTy n (tt_ctxt ist) of

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

test/TestData.hs+5−1

@@ -158,7 +158,11 @@ testFamiliesData = [

158158 ( 13, ANY ),

159159 ( 14, C_CG ),

160160 ( 15, ANY ),

161− ( 16, ANY )]),

161+ ( 16, ANY ),

162+-- FIXME: Re-enable interactive017 once it works with and without node.

163+-- FIXME: See https://github.com/idris-lang/Idris-dev/pull/4046#issuecomment-326910042

164+-- ( 17, ANY ),

165+ ( 18, ANY )]),

162166 ("interfaces", "Interfaces",

163167 [ ( 1, ANY ),

164168 ( 2, ANY ),

test/interactive017/runmode 100644 → 100755+1−1

@@ -6,4 +6,4 @@ PATH="../../scripts:$PATH"

66./shebang-node.idr

77./shebang-args.idr aaa

88./shebang-args.idr bbb aaa

9−./shebang-import.idr

9+./shebang-import.idr

test/interactive017/shebang-args.idrmode 100644 → 100755

Only the mode changed.

test/interactive017/shebang-import.idrmode 100644 → 100755

Only the mode changed.

test/interactive017/shebang-node.idrmode 100644 → 100755

Only the mode changed.

test/interactive017/shebang.idrmode 100644 → 100755

Only the mode changed.

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 = imported2_visible

7+

8+export

9+imported1_visible : a -> a

10+imported1_visible = imported1_private

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 = public1_private

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 = public2_private

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 = imported1_visible

8+

9+export

10+top_visible : a -> a

11+top_visible = public2_visible

test/interactive018/expectednew file+20

@@ -0,0 +1,20 @@

1+1 : Integer

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

17+No such variable public2_private

18+No such variable public2_private

19+1 : Integer

20+public2_visible : a -> a

test/interactive018/inputnew file+20

@@ -0,0 +1,20 @@

1+top_private 1

2+:t top_private

3+top_visible 1

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/runnew file+3

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

1+#!/usr/bin/env bash

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

3+rm -f *.ibc