7f74f91 · Idris-dev · git.iko.soy

lib/Makefile+1−8

compare with master

unifiedsplit

@@ -1,13 +1,6 @@

1

2check: .PHONY

3− for x in *.idr ; do \

4− echo "Checking $$x"; \

5− idris --noprelude --check $$x; \

3+ idris --noprelude --verbose --check checkall.idr

6− done

7− for x in network/*.idr ; do \

8− echo "Checking $$x"; \

9− idris --noprelude --check $$x; \

10− done

11

4

12recheck: clean check

5recheck: clean check

13

6

lib/checkall.idrnew file+24

@@ -0,0 +1,24 @@

1+module checkall

2+

3+-- This file just exists to typecheck all the prelude modules

4+-- Add imports here

5+

6+import builtins

7+import prelude

8+import io

9+import system

10+

11+import prelude.cast

12+import prelude.nat

13+import prelude.fin

14+import prelude.list

15+import prelude.maybe

16+import prelude.either

17+import prelude.vect

18+import prelude.strings

19+import prelude.char

20+

21+import network.cgi

22+

23+private dummy : Int

24+dummy = 42

samples/interp.idr+8−8

@@ -11,11 +11,11 @@ using (G : Vect Ty n)

11

12 data Env : Vect Ty n -> Set where

13 Nil : Env Nil

14− | (::) : interpTy a -> Env G -> Env (a :: G)

14+ (::) : interpTy a -> Env G -> Env (a :: G)

15

16 data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where

17 stop : HasType fO (t :: G) t

18− | pop : HasType k G t -> HasType (fS k) (u :: G) t

18+ pop : HasType k G t -> HasType (fS k) (u :: G) t

19

20 lookup : HasType i G t -> Env G -> interpTy t

21 lookup stop (x :: xs) = x

@@ -23,13 +23,13 @@ using (G : Vect Ty n)

23

24 data Expr : Vect Ty n -> Ty -> Set where

25 Var : HasType i G t -> Expr G t

26− | Val : (x : Int) -> Expr G TyInt

26+ Val : (x : Int) -> Expr G TyInt

27− | Lam : Expr (a :: G) t -> Expr G (TyFun a t)

27+ Lam : Expr (a :: G) t -> Expr G (TyFun a t)

28− | App : Expr G (TyFun a t) -> Expr G a -> Expr G t

28+ App : Expr G (TyFun a t) -> Expr G a -> Expr G t

29− | Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

29+ Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

30 Expr G c

31− | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

31+ If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

32− | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b

32+ Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b

33

34 interp : Env G -> {static} Expr G t -> interpTy t

35 interp env (Var i) = lookup i env

src/Idris/AbsSyntax.hs+13−2

@@ -20,11 +20,12 @@ data IOption = IOption { opt_logLevel :: Int,

20 opt_typecase :: Bool,

21 opt_typeintype :: Bool,

22 opt_showimp :: Bool,

23− opt_repl :: Bool

23+ opt_repl :: Bool,

24+ opt_verbose :: Bool

24 }

25 }

25 deriving (Show, Eq)

26 deriving (Show, Eq)

26

27

27−defaultOpts = IOption 0 False False False True

28+defaultOpts = IOption 0 False False False True True

28

29

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

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

30-- without typechecking).

31-- without typechecking).

@@ -210,6 +211,16 @@ setREPL t = do i <- get

210 let opt' = opts { opt_repl = t }

211 let opt' = opts { opt_repl = t }

211 put (i { idris_options = opt' })

212 put (i { idris_options = opt' })

212

213

214+verbose :: Idris Bool

215+verbose = do i <- get

216+ return (opt_verbose (idris_options i))

217+

218+setVerbose :: Bool -> Idris ()

219+setVerbose t = do i <- get

220+ let opts = idris_options i

221+ let opt' = opts { opt_verbose = t }

222+ put (i { idris_options = opt' })

223+

213typeInType :: Idris Bool

224typeInType :: Idris Bool

214typeInType = do i <- get

225typeInType = do i <- get

215 return (opt_typeintype (idris_options i))

226 return (opt_typeintype (idris_options i))

src/Idris/Error.hs+4−1

@@ -30,7 +30,7 @@ report e

30 | isUserError e = ioeGetErrorString e

31 | otherwise = show e

32

33−idrisCatch :: Idris a -> (IdrisErr -> Idris a) -> Idris a

33+idrisCatch :: Idris a -> (SomeException -> Idris a) -> Idris a

34idrisCatch = catch

35

36data IdrisErr = IErr String

@@ -41,6 +41,9 @@ instance Show IdrisErr where

41

42instance Exception IdrisErr

43

44+ifail :: String -> Idris ()

45+ifail str = throwIO (IErr str)

46+

44tclift :: TC a -> Idris a

47tclift :: TC a -> Idris a

45tclift tc = case tc of

48tclift tc = case tc of

46 OK v -> return v

49 OK v -> return v

src/Idris/IBC.hs+10−8

@@ -8,6 +8,7 @@ import Core.CaseTree

8import Idris.Compiler

9import Idris.AbsSyntax

10import Idris.Imports

11+import Idris.Error

11

12

12import Data.Binary

13import Data.Binary

13import Data.List

14import Data.List

@@ -96,7 +97,10 @@ process i fn

96 | ver i /= ibcVersion = do iLOG "ibc out of date"

97 | ver i /= ibcVersion = do iLOG "ibc out of date"

97 fail "Incorrect ibc version"

98 fail "Incorrect ibc version"

98 | otherwise =

99 | otherwise =

100+ do srcok <- liftIO $ doesFileExist (sourcefile i)

99− do liftIO $ timestampOlder (sourcefile i) fn

101+ when srcok $ liftIO $ timestampOlder (sourcefile i) fn

102+ v <- verbose

103+ when (v && srcok) $ iputStrLn $ "Skipping " ++ sourcefile i

100 pImports (ibc_imports i)

104 pImports (ibc_imports i)

101 pImps (ibc_implicits i)

105 pImps (ibc_implicits i)

102 pFixes (ibc_fixes i)

106 pFixes (ibc_fixes i)

@@ -111,13 +115,11 @@ process i fn

111 pAccess (ibc_access i)

115 pAccess (ibc_access i)

112

116

113timestampOlder :: FilePath -> FilePath -> IO ()

117timestampOlder :: FilePath -> FilePath -> IO ()

114−timestampOlder src ibc = do srcok <- doesFileExist src

115− when srcok $ do

116− srct <- getModificationTime src

118+timestampOlder src ibc = do srct <- getModificationTime src

117− ibct <- getModificationTime ibc

119+ ibct <- getModificationTime ibc

118− if (srct > ibct)

120+ if (srct > ibct)

119− then fail "Needs reloading"

121+ then fail "Needs reloading"

120− else return ()

122+ else return ()

121

123

122pImports :: [FilePath] -> Idris ()

124pImports :: [FilePath] -> Idris ()

123pImports fs

125pImports fs

src/Idris/Parser.hs+2−2

@@ -92,8 +92,8 @@ loadSource lidr f

92 logLvl 10 (show (toAlist (idris_implicits i)))

93 logLvl 3 (show (idris_infixes i))

94 -- Now add all the declarations to the context

95− repl <- useREPL

95+ v <- verbose

96− when repl $ iputStrLn $ "Type checking " ++ f

96+ when v $ iputStrLn $ "Type checking " ++ f

97 mapM_ (elabDecl toplevel) ds

98 iLOG ("Finished " ++ f)

99 let ibc = dropExtension f ++ ".ibc"

src/Main.hs+4

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

38 | Output String

39 | TypeCase

40 | TypeInType

41+ | Verbose

41 deriving Eq

42 deriving Eq

42

43

43main = do xs <- getArgs

44main = do xs <- getArgs

@@ -52,6 +53,8 @@ runIdris opts =

52 when (Ver `elem` opts) $ liftIO showver

53 when (Ver `elem` opts) $ liftIO showver

53 when (Usage `elem` opts) $ liftIO usage

54 when (Usage `elem` opts) $ liftIO usage

54 setREPL runrepl

55 setREPL runrepl

56+ setVerbose runrepl

57+ when (Verbose `elem` opts) $ setVerbose True

55 mapM_ makeOption opts

58 mapM_ makeOption opts

56 elabPrims

59 elabPrims

57 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"

60 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"

@@ -99,6 +102,7 @@ parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)

99parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)

102parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)

100parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)

103parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)

101parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)

104parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)

105+parseArgs ("--verbose":ns) = liftM (Verbose : ) (parseArgs ns)

102parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)

106parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)

103

107

104ver = showVersion version

108ver = showVersion version