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