7143962 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make totality a warning until compiling

Now, totality errors will not prevent loading a file. This means that features such as :missing and :addmissing can be used to fix the problem. However, the compiler will fail if there are totality errors, just as it does with metavariables.

commit7143962860633d34d49037603dd3480bfad954ce authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 6 May 2014, 19:18 (12 years ago) parent29cd870

7 files changed+69−36

compare with master

unifiedsplit

src/IRTS/Compiler.hs+5 src/Idris/AbsSyntaxTree.hs+3−1 src/Idris/Coverage.hs+12−8 src/Idris/IBC.hs+19−10 src/Idris/Output.hs+10 src/Idris/Parser.hs+1−2 src/Idris/REPL.hs+19−15

src/IRTS/Compiler.hs+5

@@ -52,6 +52,7 @@ import Paths_idris

5252compile :: Codegen -> FilePath -> Term -> Idris ()

5353compile codegen f tm

5454 = do checkMVs -- check for undefined metavariables

55+ checkTotality -- refuse to compile if there are totality problems

5556 reachableNames <- performUsageAnalysis

5657 maindef <- irMain tm

5758 iLOG $ "MAIN: " ++ show maindef

@@ -105,6 +106,10 @@ compile codegen f tm

105106 case map fst (idris_metavars i) \\ primDefs of

106107 [] -> return ()

107108 ms -> ifail $ "There are undefined metavariables: " ++ show ms

109+ checkTotality = do i <- getIState

110+ case idris_totcheckfail i of

111+ [] -> return ()

112+ ((fc, msg):fs) -> ierror . At fc . Msg $ "Cannot compile:\n " ++ msg

108113 inDir d h = do let f = d </> h

109114 ex <- doesFileExist f

110115 if ex then return f else return h

src/Idris/AbsSyntaxTree.hs+3−1

@@ -149,6 +149,7 @@ data IState = IState {

149149 idris_tyinfodata :: Ctxt TIData,

150150 idris_totcheck :: [(FC, Name)], -- names to check totality on

151151 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

152+ idris_totcheckfail :: [(FC, String)],

152153 idris_options :: IOption,

153154 idris_name :: Int,

154155 idris_lineapps :: [((FilePath, Int), PTerm)],

@@ -253,6 +254,7 @@ data IBCWrite = IBCFix FixDecl

253254 | IBCErrorHandler Name

254255 | IBCFunctionErrorHandler Name Name Name

255256 | IBCPostulate Name

257+ | IBCTotCheckErr FC String

256258 deriving Show

257259

258260-- | The initial state for the compiler

@@ -261,7 +263,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

261263 emptyContext emptyContext emptyContext emptyContext

262264 emptyContext emptyContext emptyContext emptyContext

263265 emptyContext emptyContext

264− [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

266+ [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

265267 [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

266268 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

267269 AutomaticWidth S.empty Nothing Nothing

src/Idris/Coverage.hs+12−8

@@ -9,7 +9,7 @@ import Idris.Core.CaseTree

99import Idris.AbsSyntax

1010import Idris.Delaborate

1111import Idris.Error

12−import Idris.Output (iputStrLn)

12+import Idris.Output (iWarn)

1313

1414import Data.List

1515import Data.Either

@@ -253,9 +253,10 @@ checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()

253253checkAllCovering fc done top n | not (n `elem` done)

254254 = do i <- get

255255 case lookupTotal n (tt_ctxt i) of

256− [tot@(Partial NotCovering)] ->

257− tclift $ tfail (At fc (Msg (show top ++ " is " ++ show tot

258− ++ " due to " ++ show n)))

256+ [tot@(Partial NotCovering)] ->

257+ do let msg = show top ++ " is " ++ show tot ++ " due to " ++ show n

258+ addIBC (IBCTotCheckErr fc msg)

259+ putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i }

259260 _ -> return ()

260261 case lookupCtxt n (idris_callgraph i) of

261262 [cg] -> mapM_ (checkAllCovering fc (n : done) top)

@@ -388,18 +389,21 @@ checkTotality path fc n

388389 Productive -> return t'

389390 e -> do w <- cmdOptType WarnPartial

390391 if TotalFn `elem` opts

391− then totalityError t'

392+ then do totalityError t'; return t'

392393 else do when (w && not (PartialFn `elem` opts)) $

393394 warnPartial n t'

394395 return t'

395396 where

396− totalityError t = tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))

397+ totalityError t = do i <- getIState

398+ let msg = show n ++ " is " ++ show t

399+ putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i}

400+ addIBC (IBCTotCheckErr fc msg)

397401

398402 warnPartial n t

399403 = do i <- getIState

400404 case lookupDef n (tt_ctxt i) of

401405 [x] -> do

402− iputStrLn $ show fc ++ ":Warning - " ++ show n ++ " is " ++ show t

406+ iWarn fc . pprintErr i . Msg $ "Warning - " ++ show n ++ " is " ++ show t

403407-- ++ "\n" ++ show x

404408-- let cg = lookupCtxtName Nothing n (idris_callgraph i)

405409-- iputStrLn (show cg)

@@ -410,7 +414,7 @@ checkDeclTotality (fc, n)

410414 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"

411415-- buildSCG (fc, n)

412416-- logLvl 2 $ "Built SCG"

413− i <- getIState

417+ i <- getIState

414418 t <- checkTotality [] fc n

415419 case t of

416420 -- if it's not total, it can't reduce, to keep

src/Idris/IBC.hs+19−10

@@ -30,7 +30,7 @@ import Codec.Compression.Zlib (compress)

3030import Util.Zlib (decompressEither)

3131

3232ibcVersion :: Word8

33−ibcVersion = 69

33+ibcVersion = 70

3434

3535data IBCFile = IBCFile { ver :: Word8,

3636 sourcefile :: FilePath,

@@ -53,6 +53,7 @@ data IBCFile = IBCFile { ver :: Word8,

5353 ibc_hdrs :: [(Codegen, String)],

5454 ibc_access :: [(Name, Accessibility)],

5555 ibc_total :: [(Name, Totality)],

56+ ibc_totcheckfail :: [(FC, String)],

5657 ibc_flags :: [(Name, [FnOpt])],

5758 ibc_cg :: [(Name, CGInfo)],

5859 ibc_defs :: [(Name, Def)],

@@ -75,7 +76,7 @@ deriving instance Binary IBCFile

7576!-}

7677

7778initIBC :: IBCFile

78−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

79+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

7980

8081loadIBC :: FilePath -> Idris ()

8182loadIBC fp = do imps <- getImported

@@ -234,11 +235,12 @@ ibc i (IBCMetaInformation n m) f = return f { ibc_metainformation = (n,m) : ibc_

234235ibc i (IBCErrorHandler n) f = return f { ibc_errorhandlers = n : ibc_errorhandlers f }

235236ibc i (IBCFunctionErrorHandler fn a n) f =

236237 return f { ibc_function_errorhandlers = (fn, a, n) : ibc_function_errorhandlers f }

237−ibc i (IBCMetavar n) f =

238+ibc i (IBCMetavar n) f =

238239 case lookup n (idris_metavars i) of

239240 Nothing -> return f

240241 Just t -> return f { ibc_metavars = (n, t) : ibc_metavars f }

241242ibc i (IBCPostulate n) f = return f { ibc_postulates = n : ibc_postulates f }

243+ibc i (IBCTotCheckErr fc err) f = return f { ibc_totcheckfail = (fc, err) : ibc_totcheckfail f }

242244

243245process :: IBCFile -> FilePath -> Idris ()

244246process i fn

@@ -246,7 +248,7 @@ process i fn

246248 ifail "Incorrect ibc version --- please rebuild"

247249 | otherwise =

248250 do srcok <- runIO $ doesFileExist (sourcefile i)

249− when srcok $ runIO $ timestampOlder (sourcefile i) fn

251+ when srcok $ timestampOlder (sourcefile i) fn

250252 v <- verbose

251253 quiet <- getQuiet

252254-- when (v && srcok && not quiet) $ iputStrLn $ "Skipping " ++ sourcefile i

@@ -270,6 +272,7 @@ process i fn

270272 pPatdefs (ibc_patdefs i)

271273 pAccess (ibc_access i)

272274 pTotal (ibc_total i)

275+ pTotCheckErr (ibc_totcheckfail i)

273276 pCG (ibc_cg i)

274277 pDocs (ibc_docstrings i)

275278 pCoercions (ibc_coercions i)

@@ -283,11 +286,11 @@ process i fn

283286 pMetavars (ibc_metavars i)

284287 pPostulates (ibc_postulates i)

285288

286−timestampOlder :: FilePath -> FilePath -> IO ()

287−timestampOlder src ibc = do srct <- getModificationTime src

288− ibct <- getModificationTime ibc

289+timestampOlder :: FilePath -> FilePath -> Idris ()

290+timestampOlder src ibc = do srct <- runIO $ getModificationTime src

291+ ibct <- runIO $ getModificationTime ibc

289292 if (srct > ibct)

290− then fail "Needs reloading"

293+ then ifail "Needs reloading"

291294 else return ()

292295

293296pPostulates :: [Name] -> Idris ()

@@ -454,6 +457,10 @@ pTotal ds = mapM_ (\ (n, a) ->

454457 putIState (i { tt_ctxt = setTotal n a (tt_ctxt i) }))

455458 ds

456459

460+pTotCheckErr :: [(FC, String)] -> Idris ()

461+pTotCheckErr es = do ist <- getIState

462+ putIState ist { idris_totcheckfail = idris_totcheckfail ist ++ es }

463+

457464pCG :: [(Name, CGInfo)] -> Idris ()

458465pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds

459466

@@ -1161,7 +1168,7 @@ instance Binary MetaInformation where

11611168 return (DataMI x1)

11621169

11631170instance Binary IBCFile where

1164− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36)

1171+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37)

11651172 = {-# SCC "putIBCFile" #-}

11661173 do put x1

11671174 put x2

@@ -1199,6 +1206,7 @@ instance Binary IBCFile where

11991206 put x34

12001207 put x35

12011208 put x36

1209+ put x37

12021210

12031211 get

12041212 = do x1 <- get

@@ -1238,7 +1246,8 @@ instance Binary IBCFile where

12381246 x34 <- get

12391247 x35 <- get

12401248 x36 <- get

1241− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36)

1249+ x37 <- get

1250+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37)

12421251 else return (initIBC { ver = x1 })

12431252

12441253instance Binary DataOpt where

src/Idris/Output.hs+10

@@ -11,8 +11,12 @@ import Idris.IdeSlave

1111import Util.Pretty

1212import Util.ScreenSize (getScreenWidth)

1313

14+import Debug.Trace

15+

1416import System.IO (stdout, Handle, hPutStrLn)

1517

18+import Data.List (nub)

19+

1620pshow :: IState -> Err -> String

1721pshow ist err = displayDecorated (consoleDecorate ist) .

1822 renderPretty 1.0 80 .

@@ -175,3 +179,9 @@ iputGoal g = do i <- getIState

175179 RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)

176180 IdeSlave n -> runIO . putStrLn $

177181 convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n

182+

183+-- | Warn about totality problems without failing to compile

184+warnTotality :: Idris ()

185+warnTotality = do ist <- getIState

186+ mapM_ (warn ist) (nub (idris_totcheckfail ist))

187+ where warn ist (fc, e) = iWarn fc (pprintErr ist (Msg e))

src/Idris/Parser.hs+1−2

@@ -1224,7 +1224,7 @@ loadSource h lidr f

12241224 case fp of

12251225 LIDR fn -> ifail $ "No ibc for " ++ f

12261226 IDR fn -> ifail $ "No ibc for " ++ f

1227− IBC fn src -> loadIBC fn)

1227+ IBC fn src -> loadIBC fn)

12281228 [fn | (fn, _, _) <- imports]

12291229 reportParserWarnings

12301230

@@ -1290,7 +1290,6 @@ loadSource h lidr f

12901290 addHides (hide_list i)

12911291

12921292 -- Finally, write an ibc if checking was successful

1293−

12941293 ok <- noErrors

12951294 when ok $

12961295 idrisCatch (do writeIBC f ibc; clearIBC)

src/Idris/REPL.hs+19−15

@@ -947,6 +947,7 @@ process h fn (Prove n')

947947 totcheck (fileFC "(input)", n)

948948 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)

949949 mapM_ checkDeclTotality (idris_totcheck i)

950+ warnTotality

950951

951952process h fn (HNF t)

952953 = do (tm, ty) <- elabVal toplevel False t

@@ -962,19 +963,22 @@ process h fn (TestInline t)

962963 c <- colourise

963964 iPrintResult (showTm ist (delab ist tm'))

964965process h fn Execute

965− = do ist <- getIState

966− (m, _) <- elabVal toplevel False

967− (PApp fc

968− (PRef fc (sUN "run__IO"))

969− [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

970− (tmpn, tmph) <- runIO tempfile

971− runIO $ hClose tmph

972− t <- codegen

973− compile t tmpn m

974− case idris_outputmode ist of

975− RawOutput -> do runIO $ system tmpn

976− return ()

977− IdeSlave n -> do runIO . hPutStrLn h $ IdeSlave.convSExp "run-program" tmpn n

966+ = idrisCatch

967+ (do ist <- getIState

968+ (m, _) <- elabVal toplevel False

969+ (PApp fc

970+ (PRef fc (sUN "run__IO"))

971+ [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

972+ (tmpn, tmph) <- runIO tempfile

973+ runIO $ hClose tmph

974+ t <- codegen

975+ compile t tmpn m

976+ case idris_outputmode ist of

977+ RawOutput -> do runIO $ system tmpn

978+ return ()

979+ IdeSlave n -> runIO . hPutStrLn h $

980+ IdeSlave.convSExp "run-program" tmpn n)

981+ (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

978982 where fc = fileFC "main"

979983process h fn (Compile codegen f)

980984 = do (m, _) <- elabVal toplevel False

@@ -1274,8 +1278,8 @@ loadInputs h inputs

12741278 ihWarn stdout emptyFC $ pprintErr i e)

12751279 where -- load all files, stop if any fail

12761280 tryLoad :: Bool -> [IFileType] -> Idris ()

1277− tryLoad keepstate [] = return ()

1278− tryLoad keepstate (f : fs)

1281+ tryLoad keepstate [] = warnTotality >> return ()

1282+ tryLoad keepstate (f : fs)

12791283 = do ist <- getIState

12801284 loadFromIFile h f

12811285 inew <- getIState