@@ -96,40 +96,42 @@ loadSource lidr f
9696 mapM_ (addIBC . IBCImport) modules
9797 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
9898 f rest pos
99− let ds = namespaces mname ds'
100− logLvl 3 (dumpDecls ds)
101− i <- getIState
102− logLvl 10 (show (toAlist (idris_implicits i)))
103− logLvl 3 (show (idris_infixes i))
104− -- Now add all the declarations to the context
105− v <- verbose
106− when v $ iputStrLn $ "Type checking " ++ f
107− elabDecls toplevel ds
108− i <- get
109− -- simplify every definition do give the totality checker
110− -- a better chance
111− mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
112− updateContext (simplifyCasedef n))
113− (map snd (idris_totcheck i))
114− -- build size change graph from simplified definitions
115− iLOG "Totality checking"
116− i <- get
117−-- mapM_ buildSCG (idris_totcheck i)
118− mapM_ checkDeclTotality (idris_totcheck i)
119− iLOG ("Finished " ++ f)
120− ibcsd <- valIBCSubDir i
121− let ibc = ibcPathNoFallback ibcsd f
122− iLOG "Universe checking"
123− iucheck
124− i <- getIState
125− addHides (hide_list i)
126− ok <- noErrors
127− when ok $
128− idrisCatch (do writeIBC f ibc; clearIBC)
129− (\c -> return ()) -- failure is harmless
130− i <- getIState
131− putIState (i { default_total = def_total,
132− hide_list = [] })
99+ unless (null ds') $ do
100+ let ds = namespaces mname ds'
101+ logLvl 3 (dumpDecls ds)
102+ i <- getIState
103+ logLvl 10 (show (toAlist (idris_implicits i)))
104+ logLvl 3 (show (idris_infixes i))
105+ -- Now add all the declarations to the context
106+ v <- verbose
107+ when v $ iputStrLn $ "Type checking " ++ f
108+ elabDecls toplevel ds
109+ i <- get
110+ -- simplify every definition do give the totality checker
111+ -- a better chance
112+ mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
113+ updateContext (simplifyCasedef n))
114+ (map snd (idris_totcheck i))
115+ -- build size change graph from simplified definitions
116+ iLOG "Totality checking"
117+ i <- get
118+ -- mapM_ buildSCG (idris_totcheck i)
119+ mapM_ checkDeclTotality (idris_totcheck i)
120+ iLOG ("Finished " ++ f)
121+ ibcsd <- valIBCSubDir i
122+ let ibc = ibcPathNoFallback ibcsd f
123+ iLOG "Universe checking"
124+ iucheck
125+ i <- getIState
126+ addHides (hide_list i)
127+ ok <- noErrors
128+ when ok $
129+ idrisCatch (do writeIBC f ibc; clearIBC)
130+ (\c -> return ()) -- failure is harmless
131+ i <- getIState
132+ putIState (i { default_total = def_total,
133+ hide_list = [] })
134+ return ()
133135 return ()
134136 where
135137 namespaces [] ds = ds
@@ -279,7 +281,8 @@ parseProg syn fname input pos
279281 eof
280282 i' <- getState
281283 return (concat ps, i')) i fname input of
282− Left err -> fail (show err)
284+ Left err -> do iputStrLn (show err)
285+ return []
283286 Right (x, i) -> do put i
284287 return (collect x)
285288