26da5c7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Save index file when installing a package

26da5c7Edwin Brady12 years ago

src/Idris/AbsSyntaxTree.hs+2−1

compare with master

unifiedsplit

@@ -346,7 +346,7 @@ data Command = Quit

346 | DynamicLink FilePath

347 | ListDynamic

348 | Pattelab PTerm

349− | Search PTerm

349+ | Search [Name] PTerm

350 | CaseSplitAt Bool Int Name

351 | AddClauseFrom Bool Int Name

352 | AddProofClauseFrom Bool Int Name

@@ -413,6 +413,7 @@ data Opt = Filename String

413 | PkgREPL String

414 | PkgMkDoc String -- IdrisDoc

415 | PkgTest String

416+ | PkgIndex FilePath

416 | WarnOnly

417 | WarnOnly

417 | Pkg String

418 | Pkg String

418 | BCAsm String

419 | BCAsm String

src/Idris/Help.hs+2

@@ -4,6 +4,7 @@ data CmdArg = ExprArg -- ^ The command takes an expression

4 | NameArg -- ^ The command takes a name

5 | FileArg -- ^ The command takes a file

6 | ModuleArg -- ^ The command takes a module name

7+ | PkgArgs -- ^ The command takes a list of package names

7 | NumberArg -- ^ The command takes a number

8 | NumberArg -- ^ The command takes a number

8 | NamespaceArg -- ^ The command takes a namespace name

9 | NamespaceArg -- ^ The command takes a namespace name

9 | OptionArg -- ^ The command takes an option

10 | OptionArg -- ^ The command takes an option

@@ -22,6 +23,7 @@ instance Show CmdArg where

22 show NameArg = "<name>"

23 show NameArg = "<name>"

23 show FileArg = "<filename>"

24 show FileArg = "<filename>"

24 show ModuleArg = "<module>"

25 show ModuleArg = "<module>"

26+ show PkgArgs = "<package list>"

25 show NumberArg = "<number>"

27 show NumberArg = "<number>"

26 show NamespaceArg = "<namespace>"

28 show NamespaceArg = "<namespace>"

27 show OptionArg = "<option>"

29 show OptionArg = "<option>"

src/Idris/IBC.hs+16

@@ -121,6 +121,22 @@ writeIBC src f

121 (\c -> do iLOG $ "Failed " ++ pshow i c)

122 return ()

123

124+-- Write a package index containing all the imports in the current IState

125+-- Used for ':search' of an entire package, to ensure everything is loaded.

126+writePkgIndex :: FilePath -> Idris ()

127+writePkgIndex f

128+ = do i <- getIState

129+ let imps = map (\ (x, y) -> (True, x)) $ idris_imported i

130+ iLOG $ "Writing package index " ++ show f ++ " including\n" ++

131+ show (map snd imps)

132+ resetNameIdx

133+ let ibcf = initIBC { ibc_imports = imps }

134+ idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

135+ runIO $ bencode f ibcf

136+ iLOG "Written")

137+ (\c -> do iLOG $ "Failed " ++ pshow i c)

138+ return ()

139+

124mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile

140mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile

125mkIBC [] f = return f

141mkIBC [] f = return f

126mkIBC (i:is) f = do ist <- getIState

142mkIBC (i:is) f = do ist <- getIState

src/Idris/Prover.hs+1−1

@@ -340,4 +340,4 @@ ploop fn d prompt prf e h

340 return $ pprintDocs ist doc

341 docStr (Right c) = do ist <- getIState

342 return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c))

343− search t = return (False, e, False, prf, Right $ searchByType t)

343+ search t = return (False, e, False, prf, Right $ searchByType [] t)

src/Idris/REPL.hs+11−2

@@ -33,6 +33,7 @@ import Idris.Output

33import Idris.Interactive

34import Idris.WhoCalls

35import Idris.TypeSearch (searchByType)

36+import Idris.IBC (writePkgIndex)

37import Idris.Elab.Type

38import Idris.Elab.Type

38import Idris.Elab.Clause

39import Idris.Elab.Clause

@@ -540,7 +541,7 @@ ideslaveProcess fn (Defn n) = do process fn (Defn n)

540ideslaveProcess fn (TotCheck n) = process fn (TotCheck n)

541ideslaveProcess fn (TotCheck n) = process fn (TotCheck n)

541ideslaveProcess fn (DebugInfo n) = do process fn (DebugInfo n)

542ideslaveProcess fn (DebugInfo n) = do process fn (DebugInfo n)

542 iPrintResult ""

543 iPrintResult ""

543−ideslaveProcess fn (Search t) = process fn (Search t)

544+ideslaveProcess fn (Search ps t) = process fn (Search ps t)

544ideslaveProcess fn (Spec t) = process fn (Spec t)

545ideslaveProcess fn (Spec t) = process fn (Spec t)

545-- RmProof and AddProof not supported!

546-- RmProof and AddProof not supported!

546ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')

547ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')

@@ -957,7 +958,7 @@ process fn (DebugInfo n)

957 when (not (null cg')) $ do iputStrLn "Call graph:\n"

958 when (not (null cg')) $ do iputStrLn "Call graph:\n"

958 iputStrLn (show cg')

959 iputStrLn (show cg')

959 when (not (null fn)) $ iputStrLn (show fn)

960 when (not (null fn)) $ iputStrLn (show fn)

960−process fn (Search t) = searchByType t

961+process fn (Search pkgs t) = searchByType pkgs t

961process fn (CaseSplitAt updatefile l n)

962process fn (CaseSplitAt updatefile l n)

962 = caseSplitAt fn updatefile l n

963 = caseSplitAt fn updatefile l n

963process fn (AddClauseFrom updatefile l n)

964process fn (AddClauseFrom updatefile l n)

@@ -1568,6 +1569,10 @@ idrisMain opts =

1568

1569

1569 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir

1570 historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir

1570

1571

1572+ when ok $ case opt getPkgIndex opts of

1573+ (f : _) -> writePkgIndex f

1574+ _ -> return ()

1575+

1571 when (runrepl && not idesl) $ do

1576 when (runrepl && not idesl) $ do

1572-- clearOrigPats

1577-- clearOrigPats

1573 startServer port orig inputs

1578 startServer port orig inputs

@@ -1706,6 +1711,10 @@ getExecScript :: Opt -> Maybe String

1706getExecScript (InterpretScript expr) = Just expr

1711getExecScript (InterpretScript expr) = Just expr

1707getExecScript _ = Nothing

1712getExecScript _ = Nothing

1708

1713

1714+getPkgIndex :: Opt -> Maybe FilePath

1715+getPkgIndex (PkgIndex file) = Just file

1716+getPkgIndex _ = Nothing

1717+

1709getEvalExpr :: Opt -> Maybe String

1718getEvalExpr :: Opt -> Maybe String

1710getEvalExpr (EvalExpr expr) = Just expr

1719getEvalExpr (EvalExpr expr) = Just expr

1711getEvalExpr _ = Nothing

1720getEvalExpr _ = Nothing

src/Idris/REPLParser.hs+8−4

@@ -385,10 +385,14 @@ cmd_colour name = do

385

386

387cmd_search :: String -> P.IdrisParser (Either String Command)

388−cmd_search name = do

388+cmd_search name =

389+ try (do P.whiteSpace

390+ pkgs <- sepBy P.name (P.lchar ',')

391+ t <- P.typeExpr (defaultSyntax { implicitAllowed = True })

392+ return (Right (Search pkgs t)))

389− P.whiteSpace;

393+ <|> do P.whiteSpace;

390− t <- P.typeExpr (defaultSyntax { implicitAllowed = True })

394+ t <- P.typeExpr (defaultSyntax { implicitAllowed = True })

391− return (Right (Search t))

395+ return (Right (Search [] t))

392

396

393cmd_proofsearch :: String -> P.IdrisParser (Either String Command)

397cmd_proofsearch :: String -> P.IdrisParser (Either String Command)

394cmd_proofsearch name = do

398cmd_proofsearch name = do

src/Idris/TypeSearch.hs+4−3

@@ -20,7 +20,7 @@ import qualified Data.Set as S

20import qualified Data.Text as T (pack, isPrefixOf)

21import Data.Traversable (traverse)

23−import Idris.AbsSyntax (addUsingConstraints, addImpl, getIState, putIState, implicit)

23+import Idris.AbsSyntax (addUsingConstraints, addImpl, getIState, putIState, implicit, logLvl)

24import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, eqTy, Idris,

25 IState (idris_classes, idris_docstrings, tt_ctxt, idris_outputmode),

26 implicitAllowed, OutputMode(..), PTerm, toplevel)

@@ -36,8 +36,9 @@ import Prelude hiding (pred)

37import Util.Pretty (text, char, vsep, (<>), Doc, annotate)

39−searchByType :: PTerm -> Idris ()

39+searchByType :: [Name] -> PTerm -> Idris ()

40−searchByType pterm = do

40+searchByType pkgs pterm = do

41+ logLvl 0 $ "Searching in " ++ show pkgs

41 pterm' <- addUsingConstraints syn emptyFC pterm

42 pterm' <- addUsingConstraints syn emptyFC pterm

42 pterm'' <- implicit toplevel syn name pterm'

43 pterm'' <- implicit toplevel syn name pterm'

43 i <- getIState

44 i <- getIState

src/Pkg/Package.hs+19−12

@@ -23,6 +23,7 @@ import Idris.Parser (loadModule)

23import Idris.Output (pshow)

24import Idris.AbsSyntax

25import Idris.IdrisDoc

26+import Idris.IBC

26import Idris.Output

27import Idris.Output

28import IRTS.System

29import IRTS.System

@@ -36,21 +37,26 @@ import Pkg.PParser

36-- * invoke idris on each module, with idris_opts

37-- * invoke idris on each module, with idris_opts

37-- * install everything into datadir/pname, if install flag is set

38-- * install everything into datadir/pname, if install flag is set

40+-- | Get the index file name for a package name

41+pkgIndex :: String -> FilePath

42+pkgIndex s = "00" ++ s ++ "-idx.ibc"

43+

39-- | Run the package through the idris compiler.

44-- | Run the package through the idris compiler.

40buildPkg :: Bool -> (Bool, FilePath) -> IO ()

45buildPkg :: Bool -> (Bool, FilePath) -> IO ()

41buildPkg warnonly (install, fp)

46buildPkg warnonly (install, fp)

42 = do pkgdesc <- parseDesc fp

47 = do pkgdesc <- parseDesc fp

48+ let idx = PkgIndex (pkgIndex (pkgname pkgdesc))

43 ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)

49 ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)

44 when (and ok) $

50 when (and ok) $

45 do dir <- getCurrentDirectory

51 do dir <- getCurrentDirectory

46 setCurrentDirectory $ dir </> sourcedir pkgdesc

52 setCurrentDirectory $ dir </> sourcedir pkgdesc

47 make (makefile pkgdesc)

53 make (makefile pkgdesc)

48 m_ist <- case (execout pkgdesc) of

54 m_ist <- case (execout pkgdesc) of

49− Nothing -> buildMods (NoREPL : Verbose : idris_opts pkgdesc)

55+ Nothing -> buildMods (idx : NoREPL : Verbose : idris_opts pkgdesc)

50 (modules pkgdesc)

56 (modules pkgdesc)

51 Just o -> do let exec = dir </> o

57 Just o -> do let exec = dir </> o

52 buildMods

58 buildMods

53− (NoREPL : Verbose : Output exec : idris_opts pkgdesc)

59+ (idx : NoREPL : Verbose : Output exec : idris_opts pkgdesc)

54 [idris_main pkgdesc]

60 [idris_main pkgdesc]

55 setCurrentDirectory dir

61 setCurrentDirectory dir

56 case m_ist of

62 case m_ist of

@@ -60,14 +66,7 @@ buildPkg warnonly (install, fp)

60 case errSpan ist of

66 case errSpan ist of

61 Just _ -> exitWith (ExitFailure 1)

67 Just _ -> exitWith (ExitFailure 1)

62 _ -> return ()

68 _ -> return ()

63− -- Also give up if there are metavariables to solve

64− case (map fst (idris_metavars ist) \\ primDefs) of

65− _ -> when install $ installPkg pkgdesc

69+ when install $ installPkg pkgdesc

66−-- ms -> do if install

67−-- then putStrLn "Can't install: there are undefined metavariables:"

68−-- else putStrLn "There are undefined metavariables:"

69−-- putStrLn $ "\t" ++ show ms

70−-- exitWith (ExitFailure 1)

72-- | Type check packages only

71-- | Type check packages only

73--

72--

@@ -203,7 +202,8 @@ installPkg pkgdesc

203 = do dir <- getCurrentDirectory

202 = do dir <- getCurrentDirectory

204 setCurrentDirectory $ dir </> sourcedir pkgdesc

203 setCurrentDirectory $ dir </> sourcedir pkgdesc

205 case (execout pkgdesc) of

204 case (execout pkgdesc) of

206− Nothing -> mapM_ (installIBC (pkgname pkgdesc)) (modules pkgdesc)

205+ Nothing -> do mapM_ (installIBC (pkgname pkgdesc)) (modules pkgdesc)

206+ installIdx (pkgname pkgdesc)

207 Just o -> return () -- do nothing, keep executable locally, for noe

208 mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)

209

@@ -213,7 +213,6 @@ installPkg pkgdesc

213

214buildMods :: [Opt] -> [Name] -> IO (Maybe IState)

215buildMods opts ns = do let f = map (toPath . showCG) ns

216−-- putStrLn $ "MODULE: " ++ show f

217 idris (map Filename f ++ opts)

216 idris (map Filename f ++ opts)

218 where toPath n = foldl1' (</>) $ splitOn "." n

217 where toPath n = foldl1' (</>) $ splitOn "." n

219

218

@@ -250,6 +249,14 @@ installIBC p m = do let f = toIBCFile m

250 where getDest (UN n) = ""

249 where getDest (UN n) = ""

251 getDest (NS n ns) = foldl1' (</>) (reverse (getDest n : map str ns))

250 getDest (NS n ns) = foldl1' (</>) (reverse (getDest n : map str ns))

252

251

252+installIdx :: String -> IO ()

253+installIdx p = do d <- getTargetDir

254+ let f = pkgIndex p

255+ let destdir = d </> p

256+ putStrLn $ "Installing " ++ f ++ " to " ++ destdir

257+ createDirectoryIfMissing True destdir

258+ copyFile f (destdir </> takeFileName f)

259+ return ()

253

260

254installObj :: String -> String -> IO ()

261installObj :: String -> String -> IO ()

255installObj p o = do d <- getTargetDir

262installObj p o = do d <- getTargetDir