Fix error handling again in repl

lib/Makefile

@@ -1,13 +1,6 @@
 
 check: .PHONY
-	for x in *.idr ; do \
-	echo "Checking $$x"; \
-	idris --noprelude --check $$x; \
-	done
-	for x in network/*.idr ; do \
-	echo "Checking $$x"; \
-	idris --noprelude --check $$x; \
-	done
+	idris --noprelude --verbose --check checkall.idr
 
 recheck: clean check
 

lib/checkall.idr

@@ -0,0 +1,24 @@
+module checkall
+
+-- This file just exists to typecheck all the prelude modules
+-- Add imports here 
+
+import builtins
+import prelude
+import io
+import system
+
+import prelude.cast
+import prelude.nat
+import prelude.fin
+import prelude.list
+import prelude.maybe
+import prelude.either
+import prelude.vect
+import prelude.strings
+import prelude.char
+
+import network.cgi 
+
+private dummy : Int
+dummy = 42

samples/interp.idr

@@ -11,11 +11,11 @@ using (G : Vect Ty n)
 
   data Env : Vect Ty n -> Set where
       Nil  : Env Nil
-    | (::) : interpTy a -> Env G -> Env (a :: G)
+      (::) : interpTy a -> Env G -> Env (a :: G)
 
   data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
       stop : HasType fO (t :: G) t
-    | pop  : HasType k G t -> HasType (fS k) (u :: G) t
+      pop  : HasType k G t -> HasType (fS k) (u :: G) t
 
   lookup : HasType i G t -> Env G -> interpTy t
   lookup stop    (x :: xs) = x
@@ -23,13 +23,13 @@ using (G : Vect Ty n)
 
   data Expr : Vect Ty n -> Ty -> Set where
       Var : HasType i G t -> Expr G t
-    | Val : (x : Int) -> Expr G TyInt
-    | Lam : Expr (a :: G) t -> Expr G (TyFun a t)
-    | App : Expr G (TyFun a t) -> Expr G a -> Expr G t
-    | Op  : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b -> 
+      Val : (x : Int) -> Expr G TyInt
+      Lam : Expr (a :: G) t -> Expr G (TyFun a t)
+      App : Expr G (TyFun a t) -> Expr G a -> Expr G t
+      Op  : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b -> 
             Expr G c
-    | If  : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
-    | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
+      If  : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
+      Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
   
   interp : Env G -> {static} Expr G t -> interpTy t
   interp env (Var i)     = lookup i env

src/Idris/AbsSyntax.hs

@@ -20,11 +20,12 @@ data IOption = IOption { opt_logLevel :: Int,
                          opt_typecase :: Bool,
                          opt_typeintype :: Bool,
                          opt_showimp  :: Bool,
-                         opt_repl     :: Bool
+                         opt_repl     :: Bool,
+                         opt_verbose  :: Bool
                        }
     deriving (Show, Eq)
 
-defaultOpts = IOption 0 False False False True
+defaultOpts = IOption 0 False False False True True
 
 -- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
 -- without typechecking).
@@ -210,6 +211,16 @@ setREPL t = do i <- get
                let opt' = opts { opt_repl = t }
                put (i { idris_options = opt' })
 
+verbose :: Idris Bool
+verbose = do i <- get
+             return (opt_verbose (idris_options i))
+
+setVerbose :: Bool -> Idris ()
+setVerbose t = do i <- get
+                  let opts = idris_options i
+                  let opt' = opts { opt_verbose = t }
+                  put (i { idris_options = opt' })
+
 typeInType :: Idris Bool
 typeInType = do i <- get
                 return (opt_typeintype (idris_options i))

src/Idris/Error.hs

@@ -30,7 +30,7 @@ report e
     | isUserError e = ioeGetErrorString e 
     | otherwise     = show e
 
-idrisCatch :: Idris a -> (IdrisErr -> Idris a) -> Idris a
+idrisCatch :: Idris a -> (SomeException -> Idris a) -> Idris a
 idrisCatch = catch
 
 data IdrisErr = IErr String
@@ -41,6 +41,9 @@ instance Show IdrisErr where
 
 instance Exception IdrisErr
 
+ifail :: String -> Idris ()
+ifail str = throwIO (IErr str)
+
 tclift :: TC a -> Idris a
 tclift tc = case tc of
                OK v -> return v

src/Idris/IBC.hs

@@ -8,6 +8,7 @@ import Core.CaseTree
 import Idris.Compiler
 import Idris.AbsSyntax
 import Idris.Imports
+import Idris.Error
 
 import Data.Binary
 import Data.List
@@ -96,7 +97,10 @@ process i fn
    | ver i /= ibcVersion = do iLOG "ibc out of date"
                               fail "Incorrect ibc version"
    | otherwise =  
-            do liftIO $ timestampOlder (sourcefile i) fn
+            do srcok <- liftIO $ doesFileExist (sourcefile i)
+               when srcok $ liftIO $ timestampOlder (sourcefile i) fn
+               v <- verbose
+               when (v && srcok) $ iputStrLn $ "Skipping " ++ sourcefile i
                pImports (ibc_imports i)
                pImps (ibc_implicits i)
                pFixes (ibc_fixes i)
@@ -111,13 +115,11 @@ process i fn
                pAccess (ibc_access i)
 
 timestampOlder :: FilePath -> FilePath -> IO ()
-timestampOlder src ibc = do srcok <- doesFileExist src
-                            when srcok $ do
-                                srct <- getModificationTime src
-                                ibct <- getModificationTime ibc
-                                if (srct > ibct)
-                                    then fail "Needs reloading"
-                                    else return ()
+timestampOlder src ibc = do srct <- getModificationTime src
+                            ibct <- getModificationTime ibc
+                            if (srct > ibct)
+                               then fail "Needs reloading"
+                               else return ()
 
 pImports :: [FilePath] -> Idris ()
 pImports fs 

src/Idris/Parser.hs

@@ -92,8 +92,8 @@ loadSource lidr f
                   logLvl 10 (show (toAlist (idris_implicits i)))
                   logLvl 3 (show (idris_infixes i))
                   -- Now add all the declarations to the context
-                  repl <- useREPL
-                  when repl $ iputStrLn $ "Type checking " ++ f
+                  v <- verbose
+                  when v $ iputStrLn $ "Type checking " ++ f
                   mapM_ (elabDecl toplevel) ds
                   iLOG ("Finished " ++ f)
                   let ibc = dropExtension f ++ ".ibc"

src/Main.hs

@@ -38,6 +38,7 @@ data Opt = Filename String
          | Output String
          | TypeCase
          | TypeInType
+         | Verbose
     deriving Eq
 
 main = do xs <- getArgs
@@ -52,6 +53,8 @@ runIdris opts =
        when (Ver `elem` opts) $ liftIO showver
        when (Usage `elem` opts) $ liftIO usage
        setREPL runrepl
+       setVerbose runrepl
+       when (Verbose `elem` opts) $ setVerbose True
        mapM_ makeOption opts
        elabPrims
        when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"
@@ -99,6 +102,7 @@ parseArgs ("--typecase":ns)  = liftM (TypeCase : ) (parseArgs ns)
 parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)
 parseArgs ("--help":ns)      = liftM (Usage : ) (parseArgs ns)
 parseArgs ("--version":ns)   = liftM (Ver : ) (parseArgs ns)
+parseArgs ("--verbose":ns)   = liftM (Verbose : ) (parseArgs ns)
 parseArgs (n:ns)             = liftM (Filename n : ) (parseArgs ns)
 
 ver = showVersion version