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

git.iko.soy/Idris-dev

Fix error handling again in repl

commit7f74f914b7d8ace5971bed772104d9200a9d5b40 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 8 Jan 2012, 00:05 (15 years ago) parent62ea7f8

8 files changed+66−29

compare with master

unifiedsplit

lib/Makefile+1−8 lib/checkall.idr+24 samples/interp.idr+8−8 src/Idris/AbsSyntax.hs+13−2 src/Idris/Error.hs+4−1 src/Idris/IBC.hs+10−8 src/Idris/Parser.hs+2−2 src/Main.hs+4

lib/Makefile+1−8

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

22check: .PHONY

3− for x in *.idr ; do \

4− echo "Checking $$x"; \

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

6− done

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

8− echo "Checking $$x"; \

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

10− done

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

114

125recheck: clean check

136

lib/checkall.idrnew file+24

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

1+module checkall

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

4+-- Add imports here

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)

1111

1212 data Env : Vect Ty n -> Set where

1313 Nil : Env Nil

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

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

1515

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

1717 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

1919

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

2121 lookup stop (x :: xs) = x

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

2323

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

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

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

27− | Lam : Expr (a :: G) t -> Expr G (TyFun a 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 ->

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

27+ Lam : Expr (a :: G) t -> Expr G (TyFun a 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 ->

3030 Expr G c

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

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

3333

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

3535 interp env (Var i) = lookup i env

src/Idris/AbsSyntax.hs+13−2

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

2020 opt_typecase :: Bool,

2121 opt_typeintype :: Bool,

2222 opt_showimp :: Bool,

23− opt_repl :: Bool

23+ opt_repl :: Bool,

24+ opt_verbose :: Bool

2425 }

2526 deriving (Show, Eq)

2627

27−defaultOpts = IOption 0 False False False True

28+defaultOpts = IOption 0 False False False True True

2829

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

3031-- without typechecking).

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

210211 let opt' = opts { opt_repl = t }

211212 put (i { idris_options = opt' })

212213

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+

213224typeInType :: Idris Bool

214225typeInType = do i <- get

215226 return (opt_typeintype (idris_options i))

src/Idris/Error.hs+4−1

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

3030 | isUserError e = ioeGetErrorString e

3131 | otherwise = show e

3232

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

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

3434idrisCatch = catch

3535

3636data IdrisErr = IErr String

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

4141

4242instance Exception IdrisErr

4343

44+ifail :: String -> Idris ()

45+ifail str = throwIO (IErr str)

46+

4447tclift :: TC a -> Idris a

4548tclift tc = case tc of

4649 OK v -> return v

src/Idris/IBC.hs+10−8

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

88import Idris.Compiler

99import Idris.AbsSyntax

1010import Idris.Imports

11+import Idris.Error

1112

1213import Data.Binary

1314import Data.List

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

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

9798 fail "Incorrect ibc version"

9899 | otherwise =

99− do liftIO $ timestampOlder (sourcefile i) fn

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

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

102+ v <- verbose

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

100104 pImports (ibc_imports i)

101105 pImps (ibc_implicits i)

102106 pFixes (ibc_fixes i)

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

111115 pAccess (ibc_access i)

112116

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

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

115− when srcok $ do

116− srct <- getModificationTime src

117− ibct <- getModificationTime ibc

118− if (srct > ibct)

119− then fail "Needs reloading"

120− else return ()

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

119+ ibct <- getModificationTime ibc

120+ if (srct > ibct)

121+ then fail "Needs reloading"

122+ else return ()

121123

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

123125pImports fs

src/Idris/Parser.hs+2−2

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

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

9393 logLvl 3 (show (idris_infixes i))

9494 -- Now add all the declarations to the context

95− repl <- useREPL

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

95+ v <- verbose

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

9797 mapM_ (elabDecl toplevel) ds

9898 iLOG ("Finished " ++ f)

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

src/Main.hs+4

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

3838 | Output String

3939 | TypeCase

4040 | TypeInType

41+ | Verbose

4142 deriving Eq

4243

4344main = do xs <- getArgs

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

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

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

5455 setREPL runrepl

56+ setVerbose runrepl

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

5558 mapM_ makeOption opts

5659 elabPrims

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

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

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

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

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

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

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

103107

104108ver = showVersion version