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

git.iko.soy/Idris-dev

Propagate assert_total to case blocks

commit3985f4261e946cd87b04cabf7a4be4fe3ae095ea authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 3 Jan 2014, 00:34 (13 years ago) parent4d42a2a

2 files changed+13−2

unifiedsplit

src/Idris/Coverage.hs+10−1

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

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

371371-- buildSCG (fc, n)

372372-- logLvl 2 $ "Built SCG"

373− checkTotality [] fc n

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

374383

375384-- Calculate the size change graph for this definition

376385

src/Idris/ElabDecls.hs+3−1

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

20472047elabCaseBlock info opts d@(PClauses f o n ps)

20482048 = do addIBC (IBCDef n)

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

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

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

2051+ setFlags n opts'

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

20512053

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

20532055