4c83174 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Totality checker mutual fix

4c83174Edwin Brady10 years ago

idris.cabal+3

compare with master

unifiedsplit

@@ -783,6 +783,9 @@ Extra-source-files:

783 test/totality014/run

784 test/totality014/*.idr

785 test/totality014/expected

786+ test/totality015/run

787+ test/totality015/*.idr

788+ test/totality015/expected

786

789

787 test/tutorial001/run

790 test/tutorial001/run

788 test/tutorial001/*.idr

791 test/tutorial001/*.idr

src/Idris/Coverage.hs+42−16

@@ -470,16 +470,43 @@ checkTotality path fc n

470checkDeclTotality :: (FC, Name) -> Idris Totality

471checkDeclTotality (fc, n)

472 = do logCoverage 2 $ "Checking " ++ show n ++ " for totality"

473−-- buildSCG (fc, n)

474−-- logCoverage 2 $ "Built SCG"

475 i <- getIState

473 i <- getIState

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

474+ let opts = case lookupCtxtExact n (idris_flags i) of

477− [fs] -> fs

475+ Just fs -> fs

478 _ -> []

476 _ -> []

479 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n

477 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n

480 t <- checkTotality [] fc n

478 t <- checkTotality [] fc n

481 return t

479 return t

482

480

481+-- If the name calls something which is partial, set it as partial

482+verifyTotality :: (FC, Name) -> Idris ()

483+verifyTotality (fc, n)

484+ = do logCoverage 2 $ "Checking " ++ show n ++ "'s descendents are total"

485+ ist <- getIState

486+ case lookupTotalExact n (tt_ctxt ist) of

487+ Just (Total _) -> do

488+ let ns = getNames (tt_ctxt ist)

489+

490+ case getPartial ist [] ns of

491+ Nothing -> return ()

492+ Just bad -> do let t' = Partial (Other bad)

493+ logCoverage 2 $ "Set to " ++ show t'

494+ setTotality n t'

495+ addIBC (IBCTotal n t')

496+ _ -> return ()

497+ where

498+ getNames ctxt = case lookupDefExact n ctxt of

499+ Just (CaseOp _ _ _ _ _ defs)

500+ -> let (top, def) = cases_compiletime defs in

501+ map fst (findCalls' True def top)

502+ _ -> []

503+

504+ getPartial ist [] [] = Nothing

505+ getPartial ist bad [] = Just bad

506+ getPartial ist bad (n : ns)

507+ = case lookupTotalExact n (tt_ctxt ist) of

508+ Just (Partial _) -> getPartial ist (n : bad) ns

509+ _ -> getPartial ist bad ns

483

510

484-- | Calculate the size change graph for this definition

511-- | Calculate the size change graph for this definition

485--

512--

@@ -547,17 +574,19 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

547 Guarded <- guarded,

574 Guarded <- guarded,

548 del == txt "Delay"

575 del == txt "Delay"

549 = findCalls cases Delayed arg pvs pargs

576 = findCalls cases Delayed arg pvs pargs

550− | (P _ n _, args) <- unApply ap,

551− Delayed <- guarded,

552− n == topfn -- Under a delayed recursive call to the top level function,

553− -- just check the arguments

554− = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args

555 | (P _ n _, args) <- unApply ap,

577 | (P _ n _, args) <- unApply ap,

556 Delayed <- guarded,

578 Delayed <- guarded,

557 isConName n (tt_ctxt ist)

579 isConName n (tt_ctxt ist)

558 = -- Still under a 'Delay' and constructor guarded, so check

580 = -- Still under a 'Delay' and constructor guarded, so check

559 -- just the arguments to the constructor, remaining Delayed

581 -- just the arguments to the constructor, remaining Delayed

560 concatMap (\x -> findCalls cases guarded x pvs pargs) args

582 concatMap (\x -> findCalls cases guarded x pvs pargs) args

583+ | (P _ ifthenelse _, [_, _, t, e]) <- unApply ap,

584+ ifthenelse == sNS (sUN "ifThenElse") ["Bool", "Prelude"]

585+ -- Continue look inside if...then...else blocks

586+ -- TODO: Consider whether we should do this for user defined ifThenElse

587+ -- rather than just the one in the Prelude as a special case

588+ = findCalls cases guarded t pvs pargs ++

589+ findCalls cases guarded e pvs pargs

561 | (P _ n _, args) <- unApply ap,

590 | (P _ n _, args) <- unApply ap,

562 caseName n && n /= topfn,

591 caseName n && n /= topfn,

563 notPartial (lookupTotalExact n (tt_ctxt ist))

592 notPartial (lookupTotalExact n (tt_ctxt ist))

@@ -569,13 +598,10 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

569 if n `notElem` cases

598 if n `notElem` cases

570 then findCallsCase (n : cases) guarded n args pvs pargs

599 then findCallsCase (n : cases) guarded n args pvs pargs

571 else []

600 else []

572− | (P _ ifthenelse _, [_, _, t, e]) <- unApply ap,

601+ | (P _ n _, args) <- unApply ap,

573− ifthenelse == sNS (sUN "ifThenElse") ["Bool", "Prelude"]

602+ Delayed <- guarded

574− -- Continue look inside if...then...else blocks

603+ -- Under a delayed recursive call just check the arguments

575− -- TODO: Consider whether we should do this for user defined ifThenElse

576− -- rather than just the one in the Prelude as a special case

577− = findCalls cases guarded t pvs pargs ++

578− findCalls cases guarded e pvs pargs

604+ = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args

579 | (P _ n _, args) <- unApply ap

605 | (P _ n _, args) <- unApply ap

580 -- Ordinary call, not under a delay.

606 -- Ordinary call, not under a delay.

581 -- If n is a constructor, set 'args' as Guarded

607 -- If n is a constructor, set 'args' as Guarded

src/Idris/ElabDecls.hs+4

@@ -219,6 +219,10 @@ elabDecl' what info (PMutual f ps)

219 (map snd (idris_totcheck i))

220 mapM_ buildSCG (idris_totcheck i)

221 mapM_ checkDeclTotality (idris_totcheck i)

222+ -- We've only checked that things are total independently. Given

223+ -- the ordering, something we think is total might have called

224+ -- something we hadn't checked yet

225+ mapM_ verifyTotality (idris_totcheck i)

222 clear_totcheck

226 clear_totcheck

223 where isDataDecl (PData _ _ _ _ _ _) = True

227 where isDataDecl (PData _ _ _ _ _ _) = True

224 isDataDecl _ = False

228 isDataDecl _ = False

src/Idris/Parser.hs+1

@@ -1821,6 +1821,7 @@ loadSource lidr f toline

1821 i <- getIState

1822 mapM_ buildSCG (idris_totcheck i)

1823 mapM_ checkDeclTotality (idris_totcheck i)

1824+ mapM_ verifyTotality (idris_totcheck i)

1824

1825

1825 -- Redo totality check for deferred names

1826 -- Redo totality check for deferred names

1826 let deftots = idris_defertotcheck i

1827 let deftots = idris_defertotcheck i