3820110 · Idris-dev · git.iko.soy

libs/prelude/Prelude/Applicative.idr+2

compare with master

unifiedsplit

@@ -1,6 +1,8 @@

1module Prelude.Applicative

2

3import Builtins

4+import Prelude.Basics

5+import Prelude.Classes

4import Prelude.Functor

6import Prelude.Functor

5

7

6---- Applicative functors/Idioms

8---- Applicative functors/Idioms

libs/prelude/Prelude/Chars.idr+3

@@ -1,6 +1,9 @@

1module Prelude.Char

2-- Functions operating over Chars

3

4+import Prelude.Bool

5+import Prelude.Classes

6+import Prelude.List

4import Builtins

7import Builtins

5

8

6||| Return the ASCII representation of the character.

9||| Return the ASCII representation of the character.

libs/prelude/Prelude/Fin.idr+5

@@ -2,6 +2,7 @@ module Prelude.Fin

2

3import Prelude.Nat

4import Prelude.Either

5+import Prelude.Uninhabited

5

6

6%default total

7%default total

7

8

@@ -11,6 +12,10 @@ data Fin : (n : Nat) -> Type where

11 fZ : Fin (S k)

12 fZ : Fin (S k)

12 fS : Fin k -> Fin (S k)

13 fS : Fin k -> Fin (S k)

13

14

15+instance Uninhabited (Fin Z) where

16+ uninhabited fZ impossible

17+ uninhabited (fS f) impossible

18+

14fSInjective : (m : Fin k) -> (n : Fin k) -> fS m = fS n -> m = n

19fSInjective : (m : Fin k) -> (n : Fin k) -> fS m = fS n -> m = n

15fSInjective left _ refl = refl

20fSInjective left _ refl = refl

16

21

libs/prelude/Prelude/Nat.idr+4

@@ -6,6 +6,7 @@ import Prelude.Algebra

6import Prelude.Bool

7import Prelude.Cast

8import Prelude.Classes

9+import Prelude.Uninhabited

9

10

10%access public

11%access public

11%default total

12%default total

@@ -20,6 +21,9 @@ import Prelude.Classes

20-- name hints for interactive editing

21-- name hints for interactive editing

21%name Nat k,j,i,n,m

22%name Nat k,j,i,n,m

22

23

24+instance Uninhabited (Z = S n) where

25+ uninhabited refl impossible

26+

23--------------------------------------------------------------------------------

27--------------------------------------------------------------------------------

24-- Syntactic tests

28-- Syntactic tests

25--------------------------------------------------------------------------------

29--------------------------------------------------------------------------------

libs/prelude/Prelude/Uninhabited.idr+2−7

@@ -1,18 +1,13 @@

1module Prelude.Uninhabited

2

3+import Builtins

4+

3||| A canonical proof that some type is empty

5||| A canonical proof that some type is empty

4class Uninhabited t where

6class Uninhabited t where

5 ||| If I have a t, I've had a contradiction

7 ||| If I have a t, I've had a contradiction

6 ||| @ t the uninhabited type

8 ||| @ t the uninhabited type

7 total uninhabited : t -> _|_

9 total uninhabited : t -> _|_

8

10

9−instance Uninhabited (Fin Z) where

10− uninhabited fZ impossible

11− uninhabited (fS f) impossible

12−

13−instance Uninhabited (Z = S n) where

14− uninhabited refl impossible

15−

16||| Use an absurd assumption to discharge a proof obligation

11||| Use an absurd assumption to discharge a proof obligation

17||| @ t some empty type

12||| @ t some empty type

18||| @ a the goal type

13||| @ a the goal type

src/Idris/AbsSyntax.hs+7

@@ -88,6 +88,10 @@ addDyLib libs = do i <- getIState

88addHdr :: Codegen -> String -> Idris ()

89addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }

90

91+addImported :: FilePath -> Idris ()

92+addImported f = do i <- getIState

93+ putIState $ i { idris_imported = nub $ f : idris_imported i }

94+

91addLangExt :: LanguageExt -> Idris ()

95addLangExt :: LanguageExt -> Idris ()

92addLangExt TypeProviders = do i <- getIState

96addLangExt TypeProviders = do i <- getIState

93 putIState $ i {

97 putIState $ i {

@@ -357,6 +361,9 @@ addNameIdx' i n

357getHdrs :: Codegen -> Idris [String]

361getHdrs :: Codegen -> Idris [String]

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

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

359

363

364+getImported :: Idris [FilePath]

365+getImported = do i <- getIState; return (idris_imported i)

366+

360setErrSpan :: FC -> Idris ()

367setErrSpan :: FC -> Idris ()

361setErrSpan x = do i <- getIState;

368setErrSpan x = do i <- getIState;

362 case (errSpan i) of

369 case (errSpan i) of

src/Idris/AbsSyntaxTree.hs+2−6

@@ -91,11 +91,6 @@ data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines sh

91 | ColsWide Int -- ^ Manually specified - must be positive

92 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise

93

94−-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

95−-- without typechecking).

96−-- This will include all the functions and data declarations, plus fixity declarations

97−-- and syntax macros.

98−

99-- | The global state used in the Idris monad

94-- | The global state used in the Idris monad

100data IState = IState {

95data IState = IState {

101 tt_ctxt :: Context, -- ^ All the currently defined names and their terms

96 tt_ctxt :: Context, -- ^ All the currently defined names and their terms

@@ -134,6 +129,7 @@ data IState = IState {

134 idris_libs :: [(Codegen, String)],

129 idris_libs :: [(Codegen, String)],

135 idris_cgflags :: [(Codegen, String)],

130 idris_cgflags :: [(Codegen, String)],

136 idris_hdrs :: [(Codegen, String)],

131 idris_hdrs :: [(Codegen, String)],

132+ idris_imported :: [FilePath], -- ^ Imported ibc file names

137 proof_list :: [(Name, [String])],

133 proof_list :: [(Name, [String])],

138 errSpan :: Maybe FC,

134 errSpan :: Maybe FC,

139 parserWarnings :: [(FC, Err)],

135 parserWarnings :: [(FC, Err)],

@@ -225,7 +221,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

225 emptyContext emptyContext emptyContext emptyContext

221 emptyContext emptyContext emptyContext emptyContext

226 emptyContext emptyContext

222 emptyContext emptyContext

227 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

223 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

228− [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

224+ [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

229 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

225 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

230 AutomaticWidth

226 AutomaticWidth

231

227

src/Idris/ElabDecls.hs+2−1

@@ -59,7 +59,8 @@ checkAddDef add toplvl fc [] = return []

59checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

60 = do ctxt <- getContext

61 (t', _) <- recheckC fc [] t

62− when add $ addDeferred [(n, (i, top, t, toplvl))]

62+ when add $ do addDeferred [(n, (i, top, t, toplvl))]

63+ addIBC (IBCDef n)

63 ns' <- checkAddDef add toplvl fc ns

64 ns' <- checkAddDef add toplvl fc ns

64 return ((n, (i, top, t')) : ns')

65 return ((n, (i, top, t')) : ns')

65-- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t

66-- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t

src/Idris/IBC.hs+6−3

@@ -76,9 +76,12 @@ initIBC :: IBCFile

76initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

77

78loadIBC :: FilePath -> Idris ()

79+loadIBC fp = do imps <- getImported

80+ when (not (fp `elem` imps)) $

79−loadIBC fp = do iLOG $ "Loading ibc " ++ fp

81+ do iLOG $ "Loading ibc " ++ fp

80− ibcf <- runIO $ (bdecode fp :: IO IBCFile)

82+ ibcf <- runIO $ (bdecode fp :: IO IBCFile)

81− process ibcf fp

83+ process ibcf fp

84+ addImported fp

82

85

83bencode :: Binary a => FilePath -> a -> IO ()

86bencode :: Binary a => FilePath -> a -> IO ()

84bencode f d = B.writeFile f (compress (encode d))

87bencode f d = B.writeFile f (compress (encode d))

src/Idris/Parser.hs+8

@@ -1213,6 +1213,14 @@ loadSource h lidr f

1213 file_in <- runIO $ readFile f

1214 file <- if lidr then tclift $ unlit f file_in else return file_in

1215 (mname, imports, pos) <- parseImports f file

1216+ ids <- allImportDirs

1217+ ibcsd <- valIBCSubDir i

1218+ mapM_ (\f -> do fp <- runIO $ findImport ids ibcsd f

1219+ case fp of

1220+ LIDR fn -> ifail $ "No ibc for " ++ f

1221+ IDR fn -> ifail $ "No ibc for " ++ f

1222+ IBC fn src -> loadIBC fn)

1223+ [fn | (fn, _, _) <- imports]

1216 reportParserWarnings

1224 reportParserWarnings

1217

1225

1218 -- process and check module aliases

1226 -- process and check module aliases

src/Idris/REPL.hs+47−17

@@ -1147,30 +1147,32 @@ loadInputs h inputs

1147 let ninputs = zip [1..] inputs

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

1149 do putIState ist

1150− v <- verbose

1151− -- when v $ iputStrLn $ "(" ++ show num ++ "/" ++

1152− -- show (length inputs) ++

1153− -- ") " ++ input

1154 modTree <- buildTree

1150 modTree <- buildTree

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

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

1156 input

1152 input

1157 let ifiles = getModuleFiles modTree

1153 let ifiles = getModuleFiles modTree

1158 iLOG ("MODULE TREE : " ++ show modTree)

1154 iLOG ("MODULE TREE : " ++ show modTree)

1159 iLOG ("RELOAD: " ++ show ifiles)

1155 iLOG ("RELOAD: " ++ show ifiles)

1160− when (not (all ibc ifiles) || loadCode) $ tryLoad ifiles

1156+ when (not (all ibc ifiles) || loadCode) $

1157+ tryLoad False (filter (not . ibc) ifiles)

1161 -- return the files that need rechecking

1158 -- return the files that need rechecking

1162− return (if (all ibc ifiles) then ifiles else []))

1159+ return ifiles)

1163 ninputs

1160 ninputs

1164 inew <- getIState

1161 inew <- getIState

1165− -- to check everything worked consistently (in particular, will catch

1162+ let tidata = idris_tyinfodata inew

1166− -- if the ibc version is out of date) if we weren't loading per

1163+ let lineapps = idris_lineapps inew

1167− -- module

1164+ let patdefs = idris_patdefs inew

1165+ -- If it worked, load the whole thing from all the ibcs together

1168 case errSpan inew of

1166 case errSpan inew of

1169 Nothing ->

1167 Nothing ->

1170− do putIState ist

1168+ do putIState (ist { idris_tyinfodata = tidata })

1171− when (not loadCode) $ tryLoad $ nub (concat ifiles)

1169+ ibcfiles <- mapM findNewIBC (nub (concat ifiles))

1170+ tryLoad True (mapMaybe id ibcfiles)

1172 _ -> return ()

1171 _ -> return ()

1173− putIState inew)

1172+ ist <- getIState

1173+ putIState (ist { idris_tyinfodata = tidata,

1174+ idris_lineapps = lineapps,

1175+ idris_patdefs = patdefs }))

1174 (\e -> do i <- getIState

1176 (\e -> do i <- getIState

1175 case e of

1177 case e of

1176 At f _ -> do setErrSpan f

1178 At f _ -> do setErrSpan f

@@ -1179,15 +1181,43 @@ loadInputs h inputs

1179 _ -> do setErrSpan emptyFC -- FIXME! Propagate it

1181 _ -> do setErrSpan emptyFC -- FIXME! Propagate it

1180 iputStrLn (pshow i e))

1182 iputStrLn (pshow i e))

1181 where -- load all files, stop if any fail

1183 where -- load all files, stop if any fail

1182− tryLoad :: [IFileType] -> Idris ()

1184+ tryLoad :: Bool -> [IFileType] -> Idris ()

1183− tryLoad [] = return ()

1185+ tryLoad keepstate [] = return ()

1186+ tryLoad keepstate (f : fs)

1187+ = do ist <- getIState

1184− tryLoad (f : fs) = do loadFromIFile h f

1188+ loadFromIFile h f

1189+ inew <- getIState

1190+ -- FIXME: Save these in IBC to avoid this hack! Need to

1191+ -- preserve it all from source inputs

1192+ let tidata = idris_tyinfodata inew

1193+ let lineapps = idris_lineapps inew

1194+ let patdefs = idris_patdefs inew

1185− ok <- noErrors

1195+ ok <- noErrors

1196+ when ok $ do when (not keepstate) $ putIState ist

1197+ ist <- getIState

1198+ putIState (ist { idris_tyinfodata = tidata,

1199+ idris_lineapps = lineapps,

1200+ idris_patdefs = patdefs })

1186− when ok $ tryLoad fs

1201+ tryLoad keepstate fs

1187

1202

1188 ibc (IBC _ _) = True

1203 ibc (IBC _ _) = True

1189 ibc _ = False

1204 ibc _ = False

1190

1205

1206+ findNewIBC :: IFileType -> Idris (Maybe IFileType)

1207+ findNewIBC i@(IBC _ _) = return (Just i)

1208+ findNewIBC s@(IDR f) = do ist <- get

1209+ ibcsd <- valIBCSubDir ist

1210+ let ibc = ibcPathNoFallback ibcsd f

1211+ ok <- runIO $ doesFileExist ibc

1212+ if ok then return (Just (IBC ibc s))

1213+ else return Nothing

1214+ findNewIBC s@(LIDR f) = do ist <- get

1215+ ibcsd <- valIBCSubDir ist

1216+ let ibc = ibcPathNoFallback ibcsd f

1217+ ok <- runIO $ doesFileExist ibc

1218+ if ok then return (Just (IBC ibc s))

1219+ else return Nothing

1220+

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

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

1192 mapWhileOK f [] = return []

1222 mapWhileOK f [] = return []

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

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