3eb8fc8 · Idris-dev · git.iko.soy

src/Idris/Coverage.hs+1−9

compare with master

unifiedsplit

@@ -371,15 +371,7 @@ checkDeclTotality (fc, n)

371-- buildSCG (fc, n)

372-- logLvl 2 $ "Built SCG"

373 i <- getIState

374− let opts = case lookupCtxt n (idris_flags i) of

375− [fs] -> fs

376− _ -> []

377− case lookupDef n (tt_ctxt i) of

378− [CaseOp _ _ _ pats _] ->

379− if AssertTotal `elem` opts

380− then return $ Total []

381− else checkTotality [] fc n

382− _ -> checkTotality [] fc n

374+ checkTotality [] fc n

383

375

384-- Calculate the size change graph for this definition

376-- Calculate the size change graph for this definition

385

377

src/Idris/ElabDecls.hs+2−1

@@ -2048,7 +2048,8 @@ elabCaseBlock info opts d@(PClauses f o n ps)

2048 = do addIBC (IBCDef n)

2049 logLvl 6 $ "CASE BLOCK: " ++ show (n, d)

2050 let opts' = nub (o ++ opts)

2051− setFlags n opts'

2051+ -- propagate totality assertion to the new definitions

2052+ when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]

2052 elabDecl' EAll info (PClauses f opts' n ps )

2053 elabDecl' EAll info (PClauses f opts' n ps )

2053

2054

2054-- elabDecl' info (PImport i) = loadModule i

2055-- elabDecl' info (PImport i) = loadModule i

test/reg006/expected+1−1

@@ -1 +1 @@

1−reg006.idr:22:11:RBTree.case block in case block in lookup is possibly not total due to recursive path RBTree.case block in case block in lookup --> RBTree.case block in lookup --> RBTree.lookup --> RBTree.lookup

1+reg006.idr:17:1:RBTree.lookup is possibly not total due to: RBTree.case block in lookup