3985f42 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Propagate assert_total to case blocks

3985f42Edwin Brady13 years ago

src/Idris/Coverage.hs+10−1

@@ -370,7 +370,16 @@ checkDeclTotality (fc, n)

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

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

373− checkTotality [] fc n

382+ _ -> checkTotality [] fc n

374

383

375-- Calculate the size change graph for this definition

384-- Calculate the size change graph for this definition

376

385

src/Idris/ElabDecls.hs+3−1

@@ -2047,7 +2047,9 @@ elabDecl' _ _ _ = return () -- skipped this time

2047elabCaseBlock 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'

2050− elabDecl' EAll info (PClauses f (nub (o ++ opts)) n ps )

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

2051

2053

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

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

2053

2055