0a6fb1f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Don't install packages if there are metavariables

0a6fb1fEdwin Brady13 years ago

src/Idris/AbsSyntax.hs+4

compare with master

unifiedsplit

@@ -337,6 +337,10 @@ solveDeferred n = do i <- getIState

337 filter (\(n', _) -> n/=n')

338 (idris_metavars i) }

339

340+getUndefined :: Idris [Name]

341+getUndefined = do i <- getIState

342+ return (map fst (idris_metavars i) \\ primDefs)

343+

340ihPrintResult :: Handle -> String -> Idris ()

344ihPrintResult :: Handle -> String -> Idris ()

341ihPrintResult h s = do i <- getIState

345ihPrintResult h s = do i <- getIState

342 case idris_outputmode i of

346 case idris_outputmode i of

src/Idris/REPL.hs+16−9

@@ -1029,11 +1029,12 @@ replSettings hFile = setComplete replCompletion $ defaultSettings {

1029 }

1030

1031-- invoke as if from command line

1032−idris :: [Opt] -> IO ()

1032+idris :: [Opt] -> IO (Maybe IState)

1033idris opts = do res <- runErrorT $ execStateT (idrisMain opts) idrisInit

1034 case res of

1035− Left err -> putStrLn $ pshow idrisInit err

1035+ Left err -> do putStrLn $ pshow idrisInit err

1036+ return Nothing

1036− Right ist -> return ()

1037+ Right ist -> return (Just ist)

1037

1038

1039

1039loadInputs :: Handle -> [FilePath] -> Idris ()

1040loadInputs :: Handle -> [FilePath] -> Idris ()

@@ -1054,7 +1055,7 @@ loadInputs h inputs

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

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

1055

1056

1056 let ninputs = zip [1..] inputs

1057 let ninputs = zip [1..] inputs

1057− ifiles <- mapM (\(num, input) ->

1058+ ifiles <- mapWhileOK (\(num, input) ->

1058 do putIState ist

1059 do putIState ist

1059 v <- verbose

1060 v <- verbose

1060 -- when v $ iputStrLn $ "(" ++ show num ++ "/" ++

1061 -- when v $ iputStrLn $ "(" ++ show num ++ "/" ++

@@ -1080,7 +1081,7 @@ loadInputs h inputs

1080 when (not loadCode) $ tryLoad $ nub (concat ifiles)

1081 when (not loadCode) $ tryLoad $ nub (concat ifiles)

1081 _ -> return ()

1082 _ -> return ()

1082 putIState inew)

1083 putIState inew)

1083− (\e -> case e of

1084+ (\e -> do case e of

1084 At f _ -> do setErrLine (fc_line f)

1085 At f _ -> do setErrLine (fc_line f)

1085 iputStrLn (show e)

1086 iputStrLn (show e)

1086 ProgramLineComment -> return () -- fail elsewhere

1087 ProgramLineComment -> return () -- fail elsewhere

@@ -1090,14 +1091,20 @@ loadInputs h inputs

1090 tryLoad :: [IFileType] -> Idris ()

1091 tryLoad :: [IFileType] -> Idris ()

1091 tryLoad [] = return ()

1092 tryLoad [] = return ()

1092 tryLoad (f : fs) = do loadFromIFile h f

1093 tryLoad (f : fs) = do loadFromIFile h f

1093− inew <- getIState

1094+ ok <- noErrors

1094− case errLine inew of

1095− Nothing -> tryLoad fs

1095+ when ok $ tryLoad fs

1096− _ -> return () -- error, stop

1097

1096

1098 ibc (IBC _ _) = True

1097 ibc (IBC _ _) = True

1099 ibc _ = False

1098 ibc _ = False

1100

1099

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

1101+ mapWhileOK f [] = return []

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

1103+ ok <- noErrors

1104+ if ok then do xs' <- mapWhileOK f xs

1105+ return (x' : xs')

1106+ else return [x']

1107+

1101idrisMain :: [Opt] -> Idris ()

1108idrisMain :: [Opt] -> Idris ()

1102idrisMain opts =

1109idrisMain opts =

1103 do let inputs = opt getFile opts

1110 do let inputs = opt getFile opts

src/Pkg/Package.hs+17−4

@@ -39,7 +39,7 @@ buildPkg warnonly (install, fp)

39 do dir <- getCurrentDirectory

40 setCurrentDirectory $ dir </> sourcedir pkgdesc

41 make (makefile pkgdesc)

42− case (execout pkgdesc) of

42+ m_ist <- case (execout pkgdesc) of

43 Nothing -> buildMods (NoREPL : Verbose : idris_opts pkgdesc)

44 (modules pkgdesc)

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

@@ -47,7 +47,21 @@ buildPkg warnonly (install, fp)

47 (NoREPL : Verbose : Output exec : idris_opts pkgdesc)

48 [idris_main pkgdesc]

49 setCurrentDirectory dir

50+ case m_ist of

51+ Nothing -> exitWith (ExitFailure 1)

52+ Just ist -> do

53+ -- Quit with error code if there was a problem

54+ case errLine ist of

55+ Just _ -> exitWith (ExitFailure 1)

56+ _ -> return ()

57+ -- Also give up if there are metavariables to solve

58+ case (map fst (idris_metavars ist) \\ primDefs) of

50− when install $ installPkg pkgdesc

59+ [] -> when install $ installPkg pkgdesc

60+ ms -> do if install

61+ then putStrLn "Can't install: there are undefined metavariables:"

62+ else putStrLn "There are undefined metavariables:"

63+ putStrLn $ "\t" ++ show ms

64+ exitWith (ExitFailure 1)

52cleanPkg :: FilePath -> IO ()

66cleanPkg :: FilePath -> IO ()

53cleanPkg fp

67cleanPkg fp

@@ -69,11 +83,10 @@ installPkg pkgdesc

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

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

70 mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)

84 mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)

72−buildMods :: [Opt] -> [Name] -> IO ()

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

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

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

74-- putStrLn $ "MODULE: " ++ show f

88-- putStrLn $ "MODULE: " ++ show f

75 idris (map Filename f ++ opts)

89 idris (map Filename f ++ opts)

76− return ()

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

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

79testLib :: Bool -> String -> String -> IO Bool

92testLib :: Bool -> String -> String -> IO Bool