e1f7597 · Idris-dev · git.iko.soy

CHANGELOG+3

compare with master

unifiedsplit

@@ -17,6 +17,9 @@ New in 0.9.13:

17* :apropos now accepts space-delimited lists of query items, and searches for the conjunction

18 of its inputs. It also accepts binder syntax as search strings - for instance, -> finds

19 functions.

20+* Totality errors are now treated as warnings until code generation time, when they become

21+ errors again. This allows users to use the interactive editing features to fix totality

22+ issues, but no programs that violate the stated assumptions will actually run.

20

23

21Internal changes

24Internal changes

22

25

src/IRTS/Compiler.hs+5

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

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

53compile codegen f tm

54 = do checkMVs -- check for undefined metavariables

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

55 reachableNames <- performUsageAnalysis

56 reachableNames <- performUsageAnalysis

56 maindef <- irMain tm

57 maindef <- irMain tm

57 iLOG $ "MAIN: " ++ show maindef

58 iLOG $ "MAIN: " ++ show maindef

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

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

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

106 [] -> return ()

107 [] -> return ()

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

108 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

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

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

109 ex <- doesFileExist f

114 ex <- doesFileExist f

110 if ex then return f else return h

115 if ex then return f else return h

src/Idris/AbsSyntaxTree.hs+3−1

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

149 idris_tyinfodata :: Ctxt TIData,

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

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

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

152 idris_options :: IOption,

153 idris_options :: IOption,

153 idris_name :: Int,

154 idris_name :: Int,

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

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

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

253 | IBCErrorHandler Name

254 | IBCErrorHandler Name

254 | IBCFunctionErrorHandler Name Name Name

255 | IBCFunctionErrorHandler Name Name Name

255 | IBCPostulate Name

256 | IBCPostulate Name

257+ | IBCTotCheckErr FC String

256 deriving Show

258 deriving Show

257

259

258-- | The initial state for the compiler

260-- | The initial state for the compiler

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

261 emptyContext emptyContext emptyContext emptyContext

263 emptyContext emptyContext emptyContext emptyContext

262 emptyContext emptyContext emptyContext emptyContext

264 emptyContext emptyContext emptyContext emptyContext

263 emptyContext emptyContext

265 emptyContext emptyContext

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

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

265 [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

267 [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

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

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

267 AutomaticWidth S.empty Nothing Nothing

269 AutomaticWidth S.empty Nothing Nothing

src/Idris/Coverage.hs+12−8

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

9import Idris.AbsSyntax

10import Idris.Delaborate

11import Idris.Error

12−import Idris.Output (iputStrLn)

12+import Idris.Output (iWarn)

13

14import Data.List

15import Data.Either

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

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

254 = do i <- get

255 case lookupTotal n (tt_ctxt i) of

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

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

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

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

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

258+ addIBC (IBCTotCheckErr fc msg)

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

259 _ -> return ()

260 _ -> return ()

260 case lookupCtxt n (idris_callgraph i) of

261 case lookupCtxt n (idris_callgraph i) of

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

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

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

388 Productive -> return t'

389 Productive -> return t'

389 e -> do w <- cmdOptType WarnPartial

390 e -> do w <- cmdOptType WarnPartial

390 if TotalFn `elem` opts

391 if TotalFn `elem` opts

391− then totalityError t'

392+ then do totalityError t'; return t'

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

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

393 warnPartial n t'

394 warnPartial n t'

394 return t'

395 return t'

395 where

396 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)

397

401

398 warnPartial n t

402 warnPartial n t

399 = do i <- getIState

403 = do i <- getIState

400 case lookupDef n (tt_ctxt i) of

404 case lookupDef n (tt_ctxt i) of

401 [x] -> do

405 [x] -> do

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

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

403-- ++ "\n" ++ show x

407-- ++ "\n" ++ show x

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

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

405-- iputStrLn (show cg)

409-- iputStrLn (show cg)

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

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

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

411-- buildSCG (fc, n)

415-- buildSCG (fc, n)

412-- logLvl 2 $ "Built SCG"

416-- logLvl 2 $ "Built SCG"

413− i <- getIState

417+ i <- getIState

414 t <- checkTotality [] fc n

418 t <- checkTotality [] fc n

415 case t of

419 case t of

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

420 -- 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)

30import Util.Zlib (decompressEither)

31

32ibcVersion :: Word8

33−ibcVersion = 69

33+ibcVersion = 70

34

35data IBCFile = IBCFile { ver :: Word8,

36 sourcefile :: FilePath,

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

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

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

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

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

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

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

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

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

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

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

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

75!-}

76!-}

76

77

77initIBC :: IBCFile

78initIBC :: IBCFile

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

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

79

80

80loadIBC :: FilePath -> Idris ()

81loadIBC :: FilePath -> Idris ()

81loadIBC fp = do imps <- getImported

82loadIBC fp = do imps <- getImported

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

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

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

235ibc i (IBCFunctionErrorHandler fn a n) f =

236ibc i (IBCFunctionErrorHandler fn a n) f =

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

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

237−ibc i (IBCMetavar n) f =

238+ibc i (IBCMetavar n) f =

238 case lookup n (idris_metavars i) of

239 case lookup n (idris_metavars i) of

239 Nothing -> return f

240 Nothing -> return f

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

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

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

242ibc 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 }

242

244

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

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

244process i fn

246process i fn

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

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

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

247 | otherwise =

249 | otherwise =

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

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

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

251+ when srcok $ timestampOlder (sourcefile i) fn

250 v <- verbose

252 v <- verbose

251 quiet <- getQuiet

253 quiet <- getQuiet

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

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

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

270 pPatdefs (ibc_patdefs i)

272 pPatdefs (ibc_patdefs i)

271 pAccess (ibc_access i)

273 pAccess (ibc_access i)

272 pTotal (ibc_total i)

274 pTotal (ibc_total i)

275+ pTotCheckErr (ibc_totcheckfail i)

273 pCG (ibc_cg i)

276 pCG (ibc_cg i)

274 pDocs (ibc_docstrings i)

277 pDocs (ibc_docstrings i)

275 pCoercions (ibc_coercions i)

278 pCoercions (ibc_coercions i)

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

283 pMetavars (ibc_metavars i)

286 pMetavars (ibc_metavars i)

284 pPostulates (ibc_postulates i)

287 pPostulates (ibc_postulates i)

285

288

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

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

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

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

288− ibct <- getModificationTime ibc

291+ ibct <- runIO $ getModificationTime ibc

289 if (srct > ibct)

292 if (srct > ibct)

290− then fail "Needs reloading"

293+ then ifail "Needs reloading"

291 else return ()

294 else return ()

292

295

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

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

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

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

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

455 ds

458 ds

456

459

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

461+pTotCheckErr es = do ist <- getIState

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

463+

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

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

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

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

459

466

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

1161 return (DataMI x1)

1168 return (DataMI x1)

1162

1169

1163instance Binary IBCFile where

1170instance 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)

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

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

1166 do put x1

1173 do put x1

1167 put x2

1174 put x2

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

1199 put x34

1206 put x34

1200 put x35

1207 put x35

1201 put x36

1208 put x36

1209+ put x37

1202

1210

1203 get

1211 get

1204 = do x1 <- get

1212 = do x1 <- get

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

1238 x34 <- get

1246 x34 <- get

1239 x35 <- get

1247 x35 <- get

1240 x36 <- get

1248 x36 <- get

1249+ x37 <- 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)

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)

1242 else return (initIBC { ver = x1 })

1251 else return (initIBC { ver = x1 })

1243

1252

1244instance Binary DataOpt where

1253instance Binary DataOpt where

src/Idris/Output.hs+10

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

11import Util.Pretty

12import Util.ScreenSize (getScreenWidth)

13

14+import Debug.Trace

15+

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

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

15

17

18+import Data.List (nub)

19+

16pshow :: IState -> Err -> String

20pshow :: IState -> Err -> String

17pshow ist err = displayDecorated (consoleDecorate ist) .

21pshow ist err = displayDecorated (consoleDecorate ist) .

18 renderPretty 1.0 80 .

22 renderPretty 1.0 80 .

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

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

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

176 IdeSlave n -> runIO . putStrLn $

180 IdeSlave n -> runIO . putStrLn $

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

181 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

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

1228 case fp of

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

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

1231− IBC fn src -> loadIBC fn)

1231+ IBC fn src -> loadIBC fn)

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

1233 reportParserWarnings

1234

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

1294 addHides (hide_list i)

1295

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

1297−

1298 ok <- noErrors

1297 ok <- noErrors

1299 when ok $

1298 when ok $

1300 idrisCatch (do writeIBC f ibc; clearIBC)

1299 idrisCatch (do writeIBC f ibc; clearIBC)

src/Idris/REPL.hs+19−15

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

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

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

957 mapM_ checkDeclTotality (idris_totcheck i)

958+ warnTotality

958

959

959process h fn (HNF t)

960process h fn (HNF t)

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

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

@@ -970,19 +971,22 @@ process h fn (TestInline t)

970 c <- colourise

971 c <- colourise

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

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

972process h fn Execute

973process h fn Execute

974+ = idrisCatch

973− = do ist <- getIState

975+ (do ist <- getIState

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

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

975− (PApp fc

977+ (PApp fc

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

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

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

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

978− (tmpn, tmph) <- runIO tempfile

980+ (tmpn, tmph) <- runIO tempfile

979− runIO $ hClose tmph

981+ runIO $ hClose tmph

980− t <- codegen

982+ t <- codegen

981− compile t tmpn m

983+ compile t tmpn m

982− case idris_outputmode ist of

984+ case idris_outputmode ist of

983− RawOutput -> do runIO $ system tmpn

985+ RawOutput -> do runIO $ system tmpn

984− return ()

986+ return ()

987+ IdeSlave n -> runIO . hPutStrLn h $

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

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

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

986 where fc = fileFC "main"

990 where fc = fileFC "main"

987process h fn (Compile codegen f)

991process h fn (Compile codegen f)

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

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

@@ -1282,8 +1286,8 @@ loadInputs h inputs

1282 ihWarn stdout emptyFC $ pprintErr i e)

1286 ihWarn stdout emptyFC $ pprintErr i e)

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

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

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

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

1285− tryLoad keepstate [] = return ()

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

1286− tryLoad keepstate (f : fs)

1290+ tryLoad keepstate (f : fs)

1287 = do ist <- getIState

1291 = do ist <- getIState

1288 loadFromIFile h f

1292 loadFromIFile h f

1289 inew <- getIState

1293 inew <- getIState

test/reg018/expected+1

@@ -1,4 +1,5 @@

1reg018a.idr:16:1:conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat

2+reg018a.idr:21:1:conat.loopForever is possibly not total due to: conat.minusCoNat

2reg018b.idr:8:1:A.showB is possibly not total due to recursive path A.showB

3reg018b.idr:8:1:A.showB is possibly not total due to recursive path A.showB

3reg018c.idr:19:1:CodataTest.inf is possibly not total due to: {CodataTest.inf19}

4reg018c.idr:19:1:CodataTest.inf is possibly not total due to: {CodataTest.inf19}

4reg018d.idr:5:1:Main.pull is not total as there are missing cases

5reg018d.idr:5:1:Main.pull is not total as there are missing cases

test/totality001/run+3−3

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

1#!/usr/bin/env bash

2−idris $@ test010.idr -o test010

2+idris $@ --check test010.idr

3−idris $@ test010a.idr -o test010

3+idris $@ --check test010a.idr

4−idris $@ test010b.idr -o test010

4+idris $@ --check test010b.idr

5

6rm -f *.ibc

test/totality004/expected+1

@@ -1,2 +1,3 @@

1[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]

2totality004a.idr:13:1:Main.process is possibly not total due to recursive path Main.process --> Main.process --> Main.process

3+totality004a.idr:24:1:Main.main is possibly not total due to: Main.process

test/totality005/expected−1

@@ -1,2 +1 @@

1−totality005.idr:6:1:Main.fib is possibly not total due to recursive path Main.fib

2[0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377]

1[0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377]

test/totality005/totality005.idr+2−1

@@ -2,8 +2,9 @@

2zipWithS : (f : a -> b -> c) -> Stream a -> Stream b -> Stream c

3zipWithS f (x :: xs) (y :: ys) = f x y :: zipWithS f xs ys

4

5+partial

5fib : Stream Nat

6fib : Stream Nat

6fib = 0 :: zipWithS (+) fib (1 :: fib)

7fib = 0 :: zipWithS (+) fib (1 :: fib)

7

8

8−main : IO ()

9+partial main : IO ()

9main = print (take 15 fib)

10main = print (take 15 fib)