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

git.iko.soy/Idris-dev

Fix earlier %assert_total propagation

commit3eb8fc8cf77edfd8bc8459bd50dee8f90c3de1c7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 3 Jan 2014, 01:31 (13 years ago) parent327487c

3 files changed+4−11

compare with master

unifiedsplit

src/Idris/Coverage.hs+1−9 src/Idris/ElabDecls.hs+2−1 test/reg006/expected+1−1

src/Idris/Coverage.hs+1−9

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

371371-- buildSCG (fc, n)

372372-- logLvl 2 $ "Built SCG"

373373 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

383375

384376-- Calculate the size change graph for this definition

385377

src/Idris/ElabDecls.hs+2−1

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

20482048 = do addIBC (IBCDef n)

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

20502050 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]

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

20532054

20542055-- 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