e1f7597 · Idris-dev · git.iko.soy

CHANGELOG+3

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

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

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

1919 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.

2023

2124Internal changes

2225

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

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

12281228 case fp of

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

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

1231− IBC fn src -> loadIBC fn)

1231+ IBC fn src -> loadIBC fn)

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

12331233 reportParserWarnings

12341234

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

12941294 addHides (hide_list i)

12951295

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

1297−

12981297 ok <- noErrors

12991298 when ok $

13001299 idrisCatch (do writeIBC f ibc; clearIBC)

src/Idris/REPL.hs+19−15

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

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

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

957957 mapM_ checkDeclTotality (idris_totcheck i)

958+ warnTotality

958959

959960process h fn (HNF t)

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

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

970971 c <- colourise

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

972973process h fn Execute

973− = do ist <- getIState

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

975− (PApp fc

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

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

978− (tmpn, tmph) <- runIO tempfile

979− runIO $ hClose tmph

980− t <- codegen

981− compile t tmpn m

982− case idris_outputmode ist of

983− RawOutput -> do runIO $ system tmpn

984− return ()

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

974+ = idrisCatch

975+ (do ist <- getIState

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

977+ (PApp fc

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

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

980+ (tmpn, tmph) <- runIO tempfile

981+ runIO $ hClose tmph

982+ t <- codegen

983+ compile t tmpn m

984+ case idris_outputmode ist of

985+ RawOutput -> do runIO $ system tmpn

986+ return ()

987+ IdeSlave n -> runIO . hPutStrLn h $

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

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

986990 where fc = fileFC "main"

987991process h fn (Compile codegen f)

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

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

12821286 ihWarn stdout emptyFC $ pprintErr i e)

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

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

1285− tryLoad keepstate [] = return ()

1286− tryLoad keepstate (f : fs)

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

1290+ tryLoad keepstate (f : fs)

12871291 = do ist <- getIState

12881292 loadFromIFile h f

12891293 inew <- getIState

test/reg018/expected+1

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

11reg018a.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

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

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

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

test/totality001/run+3−3

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

11#!/usr/bin/env bash

2−idris $@ test010.idr -o test010

3−idris $@ test010a.idr -o test010

4−idris $@ test010b.idr -o test010

2+idris $@ --check test010.idr

3+idris $@ --check test010a.idr

4+idris $@ --check test010b.idr

55

66rm -f *.ibc

test/totality004/expected+1

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

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

22totality004a.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

21[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 @@

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

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

44

5+partial

56fib : Stream Nat

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

78

8−main : IO ()

9+partial main : IO ()

910main = print (take 15 fib)