b8f0ef6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Separate modules for termination/coverage

b8f0ef6Edwin Brady10 years ago

idris.cabal+1

compare with master

unifiedsplit

@@ -209,6 +209,7 @@ Library

209 , Idris.REPL

210 , Idris.REPL.Parser

211 , Idris.REPL.Commands

212+ , Idris.Termination

212 , Idris.Transforms

213 , Idris.Transforms

213 , Idris.TypeSearch

214 , Idris.TypeSearch

214 , Idris.Unlit

215 , Idris.Unlit

src/Idris/Coverage.hs+1−624

@@ -1,6 +1,6 @@

1{-|

2Module : Idris.Coverage

3−Description : The coverage and totality checkers for Idris are in this module.

3+Description : Clause generation for coverage checking

4Copyright :

5License : BSD3

6Maintainer : The Idris Community.

@@ -362,626 +362,3 @@ genAll i (addPH, args)

362upd :: t -> PArg' t -> PArg' t

363upd p' p = p { getTm = p' }

364

365−-- | Check whether function and all descendants cover all cases

366−-- (partial is okay, as long as it's due to recursion)

367−checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()

368−checkAllCovering fc done top n | not (n `elem` done)

369− = do i <- get

370− case lookupTotal n (tt_ctxt i) of

371− [tot@(Partial NotCovering)] ->

372− do let msg = show top ++ " is " ++ show tot ++ " due to " ++ show n

373− putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i }

374− addIBC (IBCTotCheckErr fc msg)

375− [Partial _] ->

376− case lookupCtxt n (idris_callgraph i) of

377− [cg] -> mapM_ (checkAllCovering fc (n : done) top)

378− (calls cg)

379− _ -> return ()

380− x -> return () -- stop if total

381−checkAllCovering _ _ _ _ = return ()

382−

383−-- | Check whether all 'Inf' arguments to the name end up guaranteed to be

384−-- guarded by constructors (conservatively... maybe this can do better later).

385−-- Essentially, all it does is check that every branch is a constructor application

386−-- with no other function applications.

387−--

388−-- If so, set the 'AllGuarded' flag which can be used by the productivity check

389−checkIfGuarded :: Name -> Idris ()

390−checkIfGuarded n

391− = do i <- get

392− let ctxt = tt_ctxt i

393− case lookupDefExact n ctxt of

394− Just (CaseOp _ ty _ _ _ cases) ->

395− let gnames = fst (cases_compiletime cases) in

396− if allGuarded gnames i (snd (cases_compiletime cases))

397− then -- trace (show (n, gnames, ty, cases_compiletime cases)) $

398− addFnOpt n AllGuarded

399− else return ()

400− _ -> return ()

401− where

402− guard n ist = isConName n (tt_ctxt ist) || guardFlag n ist

403− guardFlag n ist = case lookupCtxtExact n (idris_flags ist) of

404− Nothing -> False

405− Just fs -> AllGuarded `elem` fs

406−

407− -- Top level thing always needs to be a constructor application if

408− -- the delayed things are going to be definitely guarded by this definition

409− allGuarded names i (STerm t)

410− | (P _ fn _, args) <- unApply t,

411− guard fn i

412− = and (map (guardedTerm names i) args)

413− | otherwise = False

414− allGuarded names i (ProjCase _ alts) = and (map (guardedAlt names i) alts)

415− allGuarded names i (Case _ _ alts) = and (map (guardedAlt names i) alts)

416− allGuarded names i _ = True

417−

418− guardedTerm names i (P _ v _) = v `elem` names || guard v i

419− guardedTerm names i (Bind n (Let t v) sc)

420− = guardedTerm names i v && guardedTerm names i sc

421− guardedTerm names i (Bind n b sc) = False

422− guardedTerm names i ap@(App _ _ _)

423− | (P _ fn _, args) <- unApply ap,

424− guard fn i || fn `elem` names

425− = and (map (guardedTerm names i) args)

426− guardedTerm names i (App _ f a) = False

427− guardedTerm names i tm = True

428−

429− guardedAlt names i (ConCase _ _ _ t) = allGuarded names i t

430− guardedAlt names i (FnCase _ _ t) = allGuarded names i t

431− guardedAlt names i (ConstCase _ t) = allGuarded names i t

432− guardedAlt names i (SucCase _ t) = allGuarded names i t

433− guardedAlt names i (DefaultCase t) = allGuarded names i t

434−

435−-- | Check if, in a given group of type declarations mut_ns, the

436−-- constructor cn : ty is strictly positive, and update the context

437−-- accordingly

438−checkPositive :: [Name] -- ^ the group of type declarations

439− -> (Name, Type) -- ^ the constructor

440− -> Idris Totality

441−checkPositive mut_ns (cn, ty')

442− = do i <- getIState

443− let ty = delazy' True (normalise (tt_ctxt i) [] ty')

444− let p = cp i ty

445− let tot = if p then Total (args ty) else Partial NotPositive

446− let ctxt' = setTotal cn tot (tt_ctxt i)

447− putIState (i { tt_ctxt = ctxt' })

448− logCoverage 5 $ "Constructor " ++ show cn ++ " is " ++ show tot ++ " with " ++ show mut_ns

449− addIBC (IBCTotal cn tot)

450− return tot

451− where

452− args t = [0..length (getArgTys t)-1]

453−

454− cp i (Bind n (Pi _ aty _) sc)

455− = posArg i aty && cp i sc

456− cp i t | (P _ n' _ , args) <- unApply t,

457− n' `elem` mut_ns = all noRec args

458− cp i _ = True

459−

460− posArg ist (Bind _ (Pi _ nty _) sc) = noRec nty && posArg ist sc

461− posArg ist t = posParams ist t

462−

463− noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)

464−

465− -- If the type appears recursively in a parameter argument, that's

466− -- fine, otherwise if it appears in an argument it's not fine.

467− posParams ist t | (P _ n _, args) <- unApply t

468− = case lookupCtxtExact n (idris_datatypes ist) of

469− Just ti -> checkParamsOK (param_pos ti) 0 args

470− Nothing -> and (map (posParams ist) args)

471− posParams ist t = noRec t

472−

473− checkParamsOK ppos i [] = True

474− checkParamsOK ppos i (p : ps)

475− | i `elem` ppos = checkParamsOK ppos (i + 1) ps

476− | otherwise = noRec p && checkParamsOK ppos (i + 1) ps

477−

478−-- | Calculate the totality of a function from its patterns. Either

479−-- follow the size change graph (if inductive) or check for

480−-- productivity (if coinductive)

481−calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality

482−calcTotality fc n pats

483− = do i <- getIState

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

485− [fs] -> fs

486− _ -> []

487− case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of

488− (failure : _) -> return failure

489− _ -> checkSizeChange n

490− where

491− checkLHS i (P _ fn _)

492− = case lookupTotalExact fn (tt_ctxt i) of

493− Just (Partial _) -> return (Partial (Other [fn]))

494− _ -> Nothing

495− checkLHS i (App _ f a) = mplus (checkLHS i f) (checkLHS i a)

496− checkLHS _ _ = Nothing

497−

498−checkTotality :: [Name] -> FC -> Name -> Idris Totality

499−checkTotality path fc n

500− | n `elem` path = return (Partial (Mutual (n : path)))

501− | otherwise = do

502− t <- getTotality n

503− i <- getIState

504− ctxt' <- do ctxt <- getContext

505− tclift $ simplifyCasedef n (getErasureInfo i) ctxt

506− setContext ctxt'

507− ctxt <- getContext

508− i <- getIState

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

510− [fs] -> fs

511− _ -> []

512− t' <- case t of

513− Unchecked ->

514− case lookupDef n ctxt of

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

516− do t' <- if AssertTotal `elem` opts

517− then return $ Total []

518− else calcTotality fc n pats

519− logCoverage 2 $ "Set to " ++ show t'

520− setTotality n t'

521− addIBC (IBCTotal n t')

522− return t'

523− [TyDecl (DCon _ _ _) ty] ->

524− case unApply (getRetTy ty) of

525− (P _ tyn _, _) -> do

526− let ms = case lookupCtxt tyn (idris_datatypes i) of

527− [TI _ _ _ _ xs@(_:_)] -> xs

528− ts -> [tyn]

529− checkPositive ms (n, ty)

530− _-> return $ Total []

531− _ -> return $ Total []

532− x -> return x

533− case t' of

534− Total _ -> return t'

535− Productive -> return t'

536− e -> do w <- cmdOptType WarnPartial

537− if TotalFn `elem` opts

538− then do totalityError t'; return t'

539− else do when (w && not (PartialFn `elem` opts)) $

540− warnPartial n t'

541− return t'

542− where

543− totalityError t = do i <- getIState

544− let msg = show n ++ " is " ++ show t

545− putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i}

546− addIBC (IBCTotCheckErr fc msg)

547−

548− warnPartial n t

549− = do i <- getIState

550− case lookupDef n (tt_ctxt i) of

551− [x] -> do

552− iWarn fc . pprintErr i . Msg $ "Warning - " ++ show n ++ " is " ++ show t

553−-- ++ "\n" ++ show x

554−-- let cg = lookupCtxtName Nothing n (idris_callgraph i)

555−-- iputStrLn (show cg)

556−

557−

558−checkDeclTotality :: (FC, Name) -> Idris Totality

559−checkDeclTotality (fc, n)

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

561− i <- getIState

562− let opts = case lookupCtxtExact n (idris_flags i) of

563− Just fs -> fs

564− _ -> []

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

566− t <- checkTotality [] fc n

567− return t

568−

569−-- If the name calls something which is partial, set it as partial

570−verifyTotality :: (FC, Name) -> Idris ()

571−verifyTotality (fc, n)

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

573− ist <- getIState

574− case lookupTotalExact n (tt_ctxt ist) of

575− Just (Total _) -> do

576− let ns = getNames (tt_ctxt ist)

577−

578− case getPartial ist [] ns of

579− Nothing -> return ()

580− Just bad -> do let t' = Partial (Other bad)

581− logCoverage 2 $ "Set to " ++ show t'

582− setTotality n t'

583− addIBC (IBCTotal n t')

584− _ -> return ()

585− where

586− getNames ctxt = case lookupDefExact n ctxt of

587− Just (CaseOp _ _ _ _ _ defs)

588− -> let (top, def) = cases_compiletime defs in

589− map fst (findCalls' True def top)

590− _ -> []

591−

592− getPartial ist [] [] = Nothing

593− getPartial ist bad [] = Just bad

594− getPartial ist bad (n : ns)

595− = case lookupTotalExact n (tt_ctxt ist) of

596− Just (Partial _) -> getPartial ist (n : bad) ns

597− _ -> getPartial ist bad ns

598−

599−-- | Calculate the size change graph for this definition

600−--

601−-- SCG for a function f consists of a list of:

602−-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])

603−--

604−-- where g is a function called

605−-- a1 ... an are the arguments of f in positions 1..n of g

606−-- sizechange1 ... sizechange2 is how their size has changed wrt the input

607−-- to f

608−-- Nothing, if the argument is unrelated to the input

609−buildSCG :: (FC, Name) -> Idris ()

610−buildSCG (_, n) = do

611− ist <- getIState

612− case lookupCtxt n (idris_callgraph ist) of

613− [cg] -> case lookupDefExact n (tt_ctxt ist) of

614− Just (CaseOp _ _ _ pats _ cd) ->

615− let (args, sc) = cases_compiletime cd in

616− do logCoverage 2 $ "Building SCG for " ++ show n ++ " from\n"

617− ++ show pats ++ "\n" ++ show sc

618− let newscg = buildSCG' ist n (rights pats) args

619− logCoverage 5 $ "SCG is: " ++ show newscg

620− addToCG n ( cg { scg = newscg } )

621− _ -> return () -- CG comes from a type declaration only

622− [] -> logCoverage 5 $ "Could not build SCG for " ++ show n ++ "\n"

623− x -> error $ "buildSCG: " ++ show (n, x)

624−

625−delazy = delazy' False -- not lazy codata

626−delazy' all t@(App _ f a)

627− | (P _ (UN l) _, [_, _, arg]) <- unApply t,

628− l == txt "Force" = delazy' all arg

629− | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,

630− l == txt "Delay" && (all || lty /= txt "Infinite") = delazy arg

631− | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,

632− l == txt "Delayed" && (all || lty /= txt "Infinite") = delazy' all arg

633−delazy' all (App s f a) = App s (delazy' all f) (delazy' all a)

634−delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)

635−delazy' all t = t

636−

637−data Guardedness = Toplevel | Unguarded | Guarded | Delayed

638− deriving Show

639−

640−buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]

641−buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

642− scgPat (lhs, rhs) = let lhs' = delazy lhs

643− rhs' = delazy rhs

644− (f, pargs) = unApply (dePat lhs') in

645− findCalls [] Toplevel (dePat rhs') (patvars lhs')

646− (zip pargs [0..])

647−

648− -- Under a delay, calls are excluded from the graph - if it's a call to a

649− -- non-total function we'll find that in the final totality check

650− findCalls cases Delayed ap@(P _ n _) pvs args = []

651− findCalls cases guarded ap@(App _ f a) pvs pargs

652− -- under a call to "assert_total", don't do any checking, just believe

653− -- that it is total.

654− | (P _ (UN at) _, [_, _]) <- unApply ap,

655− at == txt "assert_total" = []

656− -- don't go under calls to functions which are asserted total

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

658− Just opts <- lookupCtxtExact n (idris_flags ist),

659− AssertTotal `elem` opts = []

660− -- under a guarded call to "Delay Infinite", we are 'Delayed', so don't

661− -- check under guarded constructors.

662− | (P _ (UN del) _, [_,_,arg]) <- unApply ap,

663− Guarded <- guarded,

664− del == txt "Delay"

665− = findCalls cases Delayed arg pvs pargs

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

667− Delayed <- guarded,

668− isConName n (tt_ctxt ist) || allGuarded n ist

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

670− -- just the arguments to the constructor, remaining Delayed

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

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

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

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

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

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

677− = findCalls cases guarded t pvs pargs ++

678− findCalls cases guarded e pvs pargs

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

680− caseName n && n /= topfn,

681− notPartial (lookupTotalExact n (tt_ctxt ist))

682− -- case block - look inside the block, as long as it was covering

683− -- (i.e. not currently set at Partial) to get a more accurate size

684− -- change result from the top level patterns (also to help pass

685− -- information through from guarded corecursion accurately)

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

687− if n `notElem` cases

688− then findCallsCase (n : cases) guarded n args pvs pargs

689− else []

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

691− Delayed <- guarded

692− -- Under a delayed recursive call just check the arguments

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

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

695− -- Ordinary call, not under a delay.

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

697− = let nguarded = case guarded of

698− Unguarded -> Unguarded

699− x -> if isConName n (tt_ctxt ist)

700− || allGuarded n ist

701− then Guarded

702− else Unguarded in

703− mkChange n args pargs ++

704− concatMap (\x -> findCalls cases nguarded x pvs pargs) args

705− where notPartial (Just (Partial NotCovering)) = False

706− notPartial _ = True

707− findCalls cases guarded (App _ f a) pvs pargs

708− = findCalls cases Unguarded f pvs pargs ++ findCalls cases Unguarded a pvs pargs

709− findCalls cases guarded (Bind n (Let t v) e) pvs pargs

710− = findCalls cases Unguarded t pvs pargs ++

711− findCalls cases Unguarded v pvs pargs ++

712− -- Substitute in the scope since this might reveal some useful

713− -- structure

714− findCalls cases guarded (substV v e) pvs pargs

715− findCalls cases guarded (Bind n t e) pvs pargs

716− = findCalls cases Unguarded (binderTy t) pvs pargs ++

717− findCalls cases guarded e (n : pvs) pargs

718− findCalls cases guarded (P _ f _ ) pvs pargs

719− | not (f `elem` pvs) = [(f, [])]

720− findCalls _ _ _ _ _ = []

721−

722− -- Assumption is that names are preserved in the case block (shadowing

723− -- dealt with by the elaborator) so we can just assume the top level names

724− -- are okay for building the size change

725− findCallsCase cases guarded n args pvs pargs

726− = case lookupDefExact n (tt_ctxt ist) of

727− Just (CaseOp _ _ _ pats _ cd) ->

728− concatMap (fccPat cases pvs pargs args guarded) (rights pats)

729− Nothing -> []

730−

731− fccPat cases pvs pargs args g (lhs, rhs)

732− = let lhs' = delazy lhs

733− rhs' = delazy rhs

734− (f, pargs_case) = unApply (dePat lhs')

735− -- pargs is a pair of a term, and the argument position that

736− -- term appears in. If any of the arguments to the case block

737− -- are also on the lhs, we also want those patterns to appear

738− -- in the parg list so that we'll spot patterns which are

739− -- smaller than then

740− newpargs = newPArg args pargs

741− -- Now need to update the rhs of the case with the names in the

742− -- outer definition: In rhs', wherever we see what's in pargs_case,

743− -- replace it with the corresponding thing in pargs

744− csubs = zip pargs_case args

745− newrhs = doCaseSubs csubs (dePat rhs')

746− pargs' = pargs ++ addPArg newpargs pargs_case in

747− findCalls cases g newrhs pvs pargs'

748− where

749− doCaseSubs [] tm = tm

750− doCaseSubs ((x, x') : cs) tm

751− = doCaseSubs (subIn x x' cs) (substTerm x x' tm)

752−

753− subIn x x' [] = []

754− subIn x x' ((l, r) : cs)

755− = (substTerm x x' l, substTerm x x' r) : subIn x x' cs

756−

757− addPArg (Just (t, i) : ts) (t' : ts') = (t', i) : addPArg ts ts'

758− addPArg (Nothing : ts) (t' : ts') = addPArg ts ts'

759− addPArg _ _ = []

760−

761− newPArg :: [Term] -> [(Term, Int)] -> [Maybe (Term, Int)]

762− newPArg (t : ts) pargs = case lookup t pargs of

763− Just i -> Just (t, i) : newPArg ts pargs

764− Nothing -> Nothing : newPArg ts pargs

765− newPArg [] pargs = []

766−

767− expandToArity n args

768− = case lookupTy n (tt_ctxt ist) of

769− [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args

770− _ -> args

771− where expand i (Bind n (Pi _ _ _) sc) (x : xs) = x : expand (i + 1) sc xs

772− expand i (Bind n (Pi _ _ _) sc) [] = Just (i, Same) : expand (i + 1) sc []

773− expand i _ xs = xs

774−

775− mkChange n args pargs = [(n, expandToArity n (sizes args))]

776− where

777− sizes [] = []

778− sizes (a : as) = checkSize a pargs : sizes as

779−

780− -- find which argument in pargs <a> is smaller than, if any

781− checkSize a ((p, i) : ps)

782− | a == p = Just (i, Same)

783− | (P _ (UN as) _, [_,_,arg,_]) <- unApply a,

784− as == txt "assert_smaller" && arg == p

785− = Just (i, Smaller)

786− | smaller Nothing a (p, Nothing) = Just (i, Smaller)

787− | otherwise = checkSize a ps

788− checkSize a [] = Nothing

789−

790− -- the smaller thing we find must be defined in the same group of mutally

791− -- defined types as <a>, and not be coinductive - so carry the type of

792− -- the constructor we've gone under.

793−

794− smaller (Just tyn) a (t, Just tyt)

795− | a == t = isInductive (fst (unApply (getRetTy tyn)))

796− (fst (unApply (getRetTy tyt)))

797− smaller ty a (ap@(App _ f s), _)

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

799− = let tyn = getType n in

800− any (smaller (ty `mplus` Just tyn) a)

801− (zip args (map toJust (getArgTys tyn)))

802− -- check higher order recursive arguments

803− smaller ty (App _ f s) a = smaller ty f a

804− smaller _ _ _ = False

805−

806− toJust (n, t) = Just t

807−

808− getType n = case lookupTyExact n (tt_ctxt ist) of

809− Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist

810−

811− isInductive (P _ nty _) (P _ nty' _) =

812− let (co, muts) = case lookupCtxt nty (idris_datatypes ist) of

813− [TI _ x _ _ muts] -> (x, muts)

814− _ -> (False, []) in

815− (nty == nty' || any (== nty') muts) && not co

816− isInductive _ _ = False

817−

818− dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)

819− dePat t = t

820−

821− patvars (Bind x (PVar _) sc) = x : patvars sc

822− patvars _ = []

823−

824− allGuarded n ist = case lookupCtxtExact n (idris_flags ist) of

825− Nothing -> False

826− Just fs -> AllGuarded `elem` fs

827−

828−checkSizeChange :: Name -> Idris Totality

829−checkSizeChange n = do

830− ist <- getIState

831− case lookupCtxt n (idris_callgraph ist) of

832− [cg] -> do let ms = mkMultiPaths ist [] (scg cg)

833− logCoverage 5 ("Multipath for " ++ show n ++ ":\n" ++

834− "from " ++ show (scg cg) ++ "\n" ++

835− show (length ms) ++ "\n" ++

836− showSep "\n" (map show ms))

837− logCoverage 6 (show cg)

838− -- every multipath must have an infinitely descending

839− -- thread, then the function terminates

840− -- also need to checks functions called are all total

841− -- (Unchecked is okay as we'll spot problems here)

842− let tot = map (checkMP ist n (getArity ist n)) ms

843− logCoverage 4 $ "Generated " ++ show (length tot) ++ " paths"

844− logCoverage 5 $ "Paths for " ++ show n ++ " yield " ++

845− (showSep "\n" (map show (zip ms tot)))

846− return (noPartial tot)

847− [] -> do logCoverage 5 $ "No paths for " ++ show n

848− return Unchecked

849− where getArity ist n

850− = case lookupTy n (tt_ctxt ist) of

851− [ty] -> arity (normalise (tt_ctxt ist) [] ty)

852− _ -> error "Can't happen: checkSizeChange.getArity"

853−

854−type MultiPath = [SCGEntry]

855−

856−mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]

857−mkMultiPaths ist path [] = [reverse path]

858−mkMultiPaths ist path cg = concatMap extend cg

859− where extend (nextf, args)

860− | (nextf, args) `inPath` path = [ reverse ((nextf, args) : path) ]

861− | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)

862− = case lookupCtxt nextf (idris_callgraph ist) of

863− [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)

864− _ -> [ reverse ((nextf, args) : path) ]

865− | otherwise = [ reverse ((nextf, args) : path) ]

866−

867− inPath :: SCGEntry -> [SCGEntry] -> Bool

868− inPath f [] = False

869− inPath f (g : gs) = smallerEq f g || f == g || inPath f gs

870−

871− smallerEq :: SCGEntry -> SCGEntry -> Bool

872− smallerEq (f, args) (g, args')

873− = f == g && not (null (filter smallers args))

874− && filter smallers args == filter smallers args'

875− smallers (Just (_, Smaller)) = True

876− smallers _ = False

877−

878−-- If any route along the multipath leads to infinite descent, we're fine.

879−-- Try a route beginning with every argument.

880−-- If we reach a point we've been to before, but with a smaller value,

881−-- that means there is an infinitely descending path from that argument.

882−

883−checkMP :: IState -> Name -> Int -> MultiPath -> Totality

884−checkMP ist topfn i mp = if i > 0

885− then let paths = (map (tryPath 0 [] mp) [0..i-1]) in

886−-- trace ("Paths " ++ show paths) $

887− collapse paths

888− else tryPath 0 [] mp 0

889− where

890− tryPath' d path mp arg

891− = let res = tryPath d path mp arg in

892− trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res

893−

894− mkBig (e, d) = (e, 10000)

895−

896− tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality

897− tryPath desc path [] _ = Total []

898−-- tryPath desc path ((UN "believe_me", _) : _) arg

899−-- = Partial BelieveMe

900− -- if we get to a constructor, it's fine as long as it's strictly positive

901− tryPath desc path ((f, _) : es) arg

902− | [TyDecl (DCon _ _ _) _] <- lookupDef f (tt_ctxt ist)

903− = case lookupTotalExact f (tt_ctxt ist) of

904− Just (Total _) -> Unchecked -- okay so far

905− Just (Partial _) -> Partial (Other [f])

906− x -> Unchecked -- An error elsewhere, set as Unchecked to make

907− -- some progress

908− | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)

909− = Total []

910− tryPath desc path (e@(f, args) : es) arg

911− | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a

912− | e `elem` es && allNothing args = Partial (Mutual [f])

913− tryPath desc path (e@(f, nextargs) : es) arg

914− | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a

915− | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])

916− | Just d <- lookup (e, arg) path

917− = if desc - d > 0 -- Now lower than when we were last here

918− then -- trace ("Descent " ++ show (desc - d) ++ " "

919− -- ++ show (path, e)) $

920− Total []

921− else Partial (Mutual (map (fst . fst . fst) path ++ [f]))

922− | e `elem` map (fst . fst) path

923− && not (f `elem` map fst es)

924− = Partial (Mutual (map (fst . fst . fst) path ++ [f]))

925− | [Unchecked] <- lookupTotal f (tt_ctxt ist) =

926− let argspos = zip nextargs [0..]

927− pathres =

928− do (a, pos) <- argspos

929− case a of

930− Nothing -> -- gone up, but if the

931− -- rest definitely terminates without any

932− -- cycles (including the path so far, which

933− -- we take as inaccessible) the path is fine

934− return $ tryPath 0 (map mkBig (((e, arg), desc) : path)) es pos

935− Just (nextarg, sc) ->

936− if nextarg == arg then

937− case sc of

938− Same -> return $ tryPath desc (((e, arg), desc) : path)

939− es pos

940− Smaller -> return $ tryPath (desc+1)

941− (((e, arg), desc) : path)

942− es

943− pos

944− _ -> trace ("Shouldn't happen " ++ show e) $

945− return (Partial Itself)

946− else return Unchecked in

947−-- trace (show (desc, argspos, path, es, pathres)) $

948− collapse pathres

949−

950− | otherwise = Unchecked

951−

952−allNothing :: [Maybe a] -> Bool

953−allNothing xs = null (collapseNothing (zip xs [0..]))

954−

955−collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]

956−collapseNothing ((Nothing, t) : xs)

957− = (Nothing, t) : filter (\ (x, _) -> case x of

958− Nothing -> False

959− _ -> True) xs

960−collapseNothing (x : xs) = x : collapseNothing xs

961−collapseNothing [] = []

962−

963−noPartial :: [Totality] -> Totality

964−noPartial (Partial p : xs) = Partial p

965−noPartial (_ : xs) = noPartial xs

966−noPartial [] = Total []

967−

968−collapse :: [Totality] -> Totality

969−collapse xs = collapse' Unchecked xs

970−collapse' def (Total r : xs) = Total r

971−collapse' def (Unchecked : xs) = collapse' def xs

972−collapse' def (d : xs) = collapse' d xs

973−-- collapse' Unchecked [] = Total []

974−collapse' def [] = def

975−

976−totalityCheckBlock :: Idris ()

977−totalityCheckBlock = do

978− ist <- getIState

979− -- Do totality checking after entire mutual block

980− mapM_ (\n -> do logElab 5 $ "Simplifying " ++ show n

981− ctxt' <- do ctxt <- getContext

982− tclift $ simplifyCasedef n (getErasureInfo ist) ctxt

983− setContext ctxt')

984− (map snd (idris_totcheck ist))

985− mapM_ buildSCG (idris_totcheck ist)

986− mapM_ checkDeclTotality (idris_totcheck ist)

987− clear_totcheck

src/Idris/Elab/Clause.hs+1

@@ -34,6 +34,7 @@ import Idris.Output (iRenderResult, iWarn, iputStrLn, pshow, sendHighlighting)

34import Idris.PartialEval

35import Idris.Primitives

36import Idris.Providers

37+import Idris.Termination

37import Idris.Transforms

38import Idris.Transforms

38import IRTS.Lang

39import IRTS.Lang

src/Idris/Elab/Term.hs+2−2

@@ -19,8 +19,7 @@ import Idris.Core.TT

19import Idris.Core.Typecheck (check, converts, isType, recheck)

20import Idris.Core.Unify

21import Idris.Core.WHNF (whnf)

22−import Idris.Coverage (buildSCG, checkDeclTotality, checkPositive, genClauses,

23− recoverableCoverage, validCoverageCase)

22+import Idris.Coverage (genClauses, recoverableCoverage, validCoverageCase)

24import Idris.Delaborate

23import Idris.Delaborate

25import Idris.DSL

24import Idris.DSL

26import Idris.Elab.Quasiquote (extractUnquotes)

25import Idris.Elab.Quasiquote (extractUnquotes)

@@ -31,6 +30,7 @@ import Idris.ErrReverse (errReverse)

31import Idris.Output (pshow)

30import Idris.Output (pshow)

32import Idris.ProofSearch

31import Idris.ProofSearch

33import Idris.Reflection

32import Idris.Reflection

33+import Idris.Termination(buildSCG, checkDeclTotality, checkPositive)

35import qualified Util.Pretty as U

src/Idris/ElabDecls.hs+1

@@ -45,6 +45,7 @@ import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)

45import Idris.PartialEval

46import Idris.Primitives

47import Idris.Providers

48+import Idris.Termination

48import IRTS.Lang

49import IRTS.Lang

50import Util.Pretty (pretty, text)

51import Util.Pretty (pretty, text)

src/Idris/Parser.hs+1

@@ -32,6 +32,7 @@ import Idris.Parser.Expr

32import Idris.Parser.Helpers

33import Idris.Parser.Ops

34import Idris.Providers

35+import Idris.Termination

35import Idris.Unlit

36import Idris.Unlit

37import Util.DynamicLinker

38import Util.DynamicLinker

src/Idris/REPL.hs+1

@@ -51,6 +51,7 @@ import Idris.Prover

51import Idris.REPL.Browse (namesInNS, namespacesInNS)

52import Idris.REPL.Commands

53import Idris.REPL.Parser

54+import Idris.Termination

54import Idris.TypeSearch (searchByType)

55import Idris.TypeSearch (searchByType)

55import Idris.WhoCalls

56import Idris.WhoCalls

56import IRTS.Compiler

57import IRTS.Compiler

src/Idris/Termination.hsnew file+649

@@ -0,0 +1,649 @@

1+{-|

2+Module : Idris.Coverage

3+Description : The coverage and totality checkers for Idris are in this module.

4+Copyright :

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

8+{-# LANGUAGE PatternGuards #-}

9+module Idris.Termination where

10+

11+import Idris.AbsSyntax

12+import Idris.Core.CaseTree

13+import Idris.Core.Evaluate

14+import Idris.Core.TT

15+import Idris.Delaborate

16+import Idris.Error

17+import Idris.Output (iWarn, iputStrLn)

18+

19+import Control.Monad.State.Strict

20+import Data.Char

21+import Data.Either

22+import Data.List

23+import Data.Maybe

24+import Debug.Trace

25+

26+-- | Check whether function and all descendants cover all cases

27+-- (partial is okay, as long as it's due to recursion)

28+checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()

29+checkAllCovering fc done top n | not (n `elem` done)

30+ = do i <- get

31+ case lookupTotal n (tt_ctxt i) of

32+ [tot@(Partial NotCovering)] ->

33+ do let msg = show top ++ " is " ++ show tot ++ " due to " ++ show n

34+ putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i }

35+ addIBC (IBCTotCheckErr fc msg)

36+ [Partial _] ->

37+ case lookupCtxt n (idris_callgraph i) of

38+ [cg] -> mapM_ (checkAllCovering fc (n : done) top)

39+ (calls cg)

40+ _ -> return ()

41+ x -> return () -- stop if total

42+checkAllCovering _ _ _ _ = return ()

43+

44+-- | Check whether all 'Inf' arguments to the name end up guaranteed to be

45+-- guarded by constructors (conservatively... maybe this can do better later).

46+-- Essentially, all it does is check that every branch is a constructor application

47+-- with no other function applications.

48+--

49+-- If so, set the 'AllGuarded' flag which can be used by the productivity check

50+checkIfGuarded :: Name -> Idris ()

51+checkIfGuarded n

52+ = do i <- get

53+ let ctxt = tt_ctxt i

54+ case lookupDefExact n ctxt of

55+ Just (CaseOp _ ty _ _ _ cases) ->

56+ let gnames = fst (cases_compiletime cases) in

57+ if allGuarded gnames i (snd (cases_compiletime cases))

58+ then -- trace (show (n, gnames, ty, cases_compiletime cases)) $

59+ addFnOpt n AllGuarded

60+ else return ()

61+ _ -> return ()

62+ where

63+ guard n ist = isConName n (tt_ctxt ist) || guardFlag n ist

64+ guardFlag n ist = case lookupCtxtExact n (idris_flags ist) of

65+ Nothing -> False

66+ Just fs -> AllGuarded `elem` fs

67+

68+ -- Top level thing always needs to be a constructor application if

69+ -- the delayed things are going to be definitely guarded by this definition

70+ allGuarded names i (STerm t)

71+ | (P _ fn _, args) <- unApply t,

72+ guard fn i

73+ = and (map (guardedTerm names i) args)

74+ | otherwise = False

75+ allGuarded names i (ProjCase _ alts) = and (map (guardedAlt names i) alts)

76+ allGuarded names i (Case _ _ alts) = and (map (guardedAlt names i) alts)

77+ allGuarded names i _ = True

78+

79+ guardedTerm names i (P _ v _) = v `elem` names || guard v i

80+ guardedTerm names i (Bind n (Let t v) sc)

81+ = guardedTerm names i v && guardedTerm names i sc

82+ guardedTerm names i (Bind n b sc) = False

83+ guardedTerm names i ap@(App _ _ _)

84+ | (P _ fn _, args) <- unApply ap,

85+ guard fn i || fn `elem` names

86+ = and (map (guardedTerm names i) args)

87+ guardedTerm names i (App _ f a) = False

88+ guardedTerm names i tm = True

89+

90+ guardedAlt names i (ConCase _ _ _ t) = allGuarded names i t

91+ guardedAlt names i (FnCase _ _ t) = allGuarded names i t

92+ guardedAlt names i (ConstCase _ t) = allGuarded names i t

93+ guardedAlt names i (SucCase _ t) = allGuarded names i t

94+ guardedAlt names i (DefaultCase t) = allGuarded names i t

95+

96+-- | Check if, in a given group of type declarations mut_ns, the

97+-- constructor cn : ty is strictly positive, and update the context

98+-- accordingly

99+checkPositive :: [Name] -- ^ the group of type declarations

100+ -> (Name, Type) -- ^ the constructor

101+ -> Idris Totality

102+checkPositive mut_ns (cn, ty')

103+ = do i <- getIState

104+ let ty = delazy' True (normalise (tt_ctxt i) [] ty')

105+ let p = cp i ty

106+ let tot = if p then Total (args ty) else Partial NotPositive

107+ let ctxt' = setTotal cn tot (tt_ctxt i)

108+ putIState (i { tt_ctxt = ctxt' })

109+ logCoverage 5 $ "Constructor " ++ show cn ++ " is " ++ show tot ++ " with " ++ show mut_ns

110+ addIBC (IBCTotal cn tot)

111+ return tot

112+ where

113+ args t = [0..length (getArgTys t)-1]

114+

115+ cp i (Bind n (Pi _ aty _) sc)

116+ = posArg i aty && cp i sc

117+ cp i t | (P _ n' _ , args) <- unApply t,

118+ n' `elem` mut_ns = all noRec args

119+ cp i _ = True

120+

121+ posArg ist (Bind _ (Pi _ nty _) sc) = noRec nty && posArg ist sc

122+ posArg ist t = posParams ist t

123+

124+ noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)

125+

126+ -- If the type appears recursively in a parameter argument, that's

127+ -- fine, otherwise if it appears in an argument it's not fine.

128+ posParams ist t | (P _ n _, args) <- unApply t

129+ = case lookupCtxtExact n (idris_datatypes ist) of

130+ Just ti -> checkParamsOK (param_pos ti) 0 args

131+ Nothing -> and (map (posParams ist) args)

132+ posParams ist t = noRec t

133+

134+ checkParamsOK ppos i [] = True

135+ checkParamsOK ppos i (p : ps)

136+ | i `elem` ppos = checkParamsOK ppos (i + 1) ps

137+ | otherwise = noRec p && checkParamsOK ppos (i + 1) ps

138+

139+-- | Calculate the totality of a function from its patterns. Either

140+-- follow the size change graph (if inductive) or check for

141+-- productivity (if coinductive)

142+calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality

143+calcTotality fc n pats

144+ = do i <- getIState

145+ let opts = case lookupCtxt n (idris_flags i) of

146+ [fs] -> fs

147+ _ -> []

148+ case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of

149+ (failure : _) -> return failure

150+ _ -> checkSizeChange n

151+ where

152+ checkLHS i (P _ fn _)

153+ = case lookupTotalExact fn (tt_ctxt i) of

154+ Just (Partial _) -> return (Partial (Other [fn]))

155+ _ -> Nothing

156+ checkLHS i (App _ f a) = mplus (checkLHS i f) (checkLHS i a)

157+ checkLHS _ _ = Nothing

158+

159+checkTotality :: [Name] -> FC -> Name -> Idris Totality

160+checkTotality path fc n

161+ | n `elem` path = return (Partial (Mutual (n : path)))

162+ | otherwise = do

163+ t <- getTotality n

164+ i <- getIState

165+ ctxt' <- do ctxt <- getContext

166+ tclift $ simplifyCasedef n (getErasureInfo i) ctxt

167+ setContext ctxt'

168+ ctxt <- getContext

169+ i <- getIState

170+ let opts = case lookupCtxt n (idris_flags i) of

171+ [fs] -> fs

172+ _ -> []

173+ t' <- case t of

174+ Unchecked ->

175+ case lookupDef n ctxt of

176+ [CaseOp _ _ _ _ pats _] ->

177+ do t' <- if AssertTotal `elem` opts

178+ then return $ Total []

179+ else calcTotality fc n pats

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

181+ setTotality n t'

182+ addIBC (IBCTotal n t')

183+ return t'

184+ [TyDecl (DCon _ _ _) ty] ->

185+ case unApply (getRetTy ty) of

186+ (P _ tyn _, _) -> do

187+ let ms = case lookupCtxt tyn (idris_datatypes i) of

188+ [TI _ _ _ _ xs@(_:_)] -> xs

189+ ts -> [tyn]

190+ checkPositive ms (n, ty)

191+ _-> return $ Total []

192+ _ -> return $ Total []

193+ x -> return x

194+ case t' of

195+ Total _ -> return t'

196+ Productive -> return t'

197+ e -> do w <- cmdOptType WarnPartial

198+ if TotalFn `elem` opts

199+ then do totalityError t'; return t'

200+ else do when (w && not (PartialFn `elem` opts)) $

201+ warnPartial n t'

202+ return t'

203+ where

204+ totalityError t = do i <- getIState

205+ let msg = show n ++ " is " ++ show t

206+ putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i}

207+ addIBC (IBCTotCheckErr fc msg)

208+

209+ warnPartial n t

210+ = do i <- getIState

211+ case lookupDef n (tt_ctxt i) of

212+ [x] -> do

213+ iWarn fc . pprintErr i . Msg $ "Warning - " ++ show n ++ " is " ++ show t

214+-- ++ "\n" ++ show x

215+-- let cg = lookupCtxtName Nothing n (idris_callgraph i)

216+-- iputStrLn (show cg)

217+

218+

219+checkDeclTotality :: (FC, Name) -> Idris Totality

220+checkDeclTotality (fc, n)

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

222+ i <- getIState

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

224+ Just fs -> fs

225+ _ -> []

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

227+ t <- checkTotality [] fc n

228+ return t

229+

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

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

232+verifyTotality (fc, n)

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

234+ ist <- getIState

235+ case lookupTotalExact n (tt_ctxt ist) of

236+ Just (Total _) -> do

237+ let ns = getNames (tt_ctxt ist)

238+

239+ case getPartial ist [] ns of

240+ Nothing -> return ()

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

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

243+ setTotality n t'

244+ addIBC (IBCTotal n t')

245+ _ -> return ()

246+ where

247+ getNames ctxt = case lookupDefExact n ctxt of

248+ Just (CaseOp _ _ _ _ _ defs)

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

250+ map fst (findCalls' True def top)

251+ _ -> []

252+

253+ getPartial ist [] [] = Nothing

254+ getPartial ist bad [] = Just bad

255+ getPartial ist bad (n : ns)

256+ = case lookupTotalExact n (tt_ctxt ist) of

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

258+ _ -> getPartial ist bad ns

259+

260+-- | Calculate the size change graph for this definition

261+--

262+-- SCG for a function f consists of a list of:

263+-- (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])

264+--

265+-- where g is a function called

266+-- a1 ... an are the arguments of f in positions 1..n of g

267+-- sizechange1 ... sizechange2 is how their size has changed wrt the input

268+-- to f

269+-- Nothing, if the argument is unrelated to the input

270+buildSCG :: (FC, Name) -> Idris ()

271+buildSCG (_, n) = do

272+ ist <- getIState

273+ case lookupCtxt n (idris_callgraph ist) of

274+ [cg] -> case lookupDefExact n (tt_ctxt ist) of

275+ Just (CaseOp _ _ _ pats _ cd) ->

276+ let (args, sc) = cases_compiletime cd in

277+ do logCoverage 2 $ "Building SCG for " ++ show n ++ " from\n"

278+ ++ show pats ++ "\n" ++ show sc

279+ let newscg = buildSCG' ist n (rights pats) args

280+ logCoverage 5 $ "SCG is: " ++ show newscg

281+ addToCG n ( cg { scg = newscg } )

282+ _ -> return () -- CG comes from a type declaration only

283+ [] -> logCoverage 5 $ "Could not build SCG for " ++ show n ++ "\n"

284+ x -> error $ "buildSCG: " ++ show (n, x)

285+

286+delazy = delazy' False -- not lazy codata

287+delazy' all t@(App _ f a)

288+ | (P _ (UN l) _, [_, _, arg]) <- unApply t,

289+ l == txt "Force" = delazy' all arg

290+ | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,

291+ l == txt "Delay" && (all || lty /= txt "Infinite") = delazy arg

292+ | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,

293+ l == txt "Delayed" && (all || lty /= txt "Infinite") = delazy' all arg

294+delazy' all (App s f a) = App s (delazy' all f) (delazy' all a)

295+delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)

296+delazy' all t = t

297+

298+data Guardedness = Toplevel | Unguarded | Guarded | Delayed

299+ deriving Show

300+

301+buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]

302+buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

303+ scgPat (lhs, rhs) = let lhs' = delazy lhs

304+ rhs' = delazy rhs

305+ (f, pargs) = unApply (dePat lhs') in

306+ findCalls [] Toplevel (dePat rhs') (patvars lhs')

307+ (zip pargs [0..])

308+

309+ -- Under a delay, calls are excluded from the graph - if it's a call to a

310+ -- non-total function we'll find that in the final totality check

311+ findCalls cases Delayed ap@(P _ n _) pvs args = []

312+ findCalls cases guarded ap@(App _ f a) pvs pargs

313+ -- under a call to "assert_total", don't do any checking, just believe

314+ -- that it is total.

315+ | (P _ (UN at) _, [_, _]) <- unApply ap,

316+ at == txt "assert_total" = []

317+ -- don't go under calls to functions which are asserted total

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

319+ Just opts <- lookupCtxtExact n (idris_flags ist),

320+ AssertTotal `elem` opts = []

321+ -- under a guarded call to "Delay Infinite", we are 'Delayed', so don't

322+ -- check under guarded constructors.

323+ | (P _ (UN del) _, [_,_,arg]) <- unApply ap,

324+ Guarded <- guarded,

325+ del == txt "Delay"

326+ = findCalls cases Delayed arg pvs pargs

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

328+ Delayed <- guarded,

329+ isConName n (tt_ctxt ist) || allGuarded n ist

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

331+ -- just the arguments to the constructor, remaining Delayed

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

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

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

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

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

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

338+ = findCalls cases guarded t pvs pargs ++

339+ findCalls cases guarded e pvs pargs

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

341+ caseName n && n /= topfn,

342+ notPartial (lookupTotalExact n (tt_ctxt ist))

343+ -- case block - look inside the block, as long as it was covering

344+ -- (i.e. not currently set at Partial) to get a more accurate size

345+ -- change result from the top level patterns (also to help pass

346+ -- information through from guarded corecursion accurately)

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

348+ if n `notElem` cases

349+ then findCallsCase (n : cases) guarded n args pvs pargs

350+ else []

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

352+ Delayed <- guarded

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

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

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

356+ -- Ordinary call, not under a delay.

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

358+ = let nguarded = case guarded of

359+ Unguarded -> Unguarded

360+ x -> if isConName n (tt_ctxt ist)

361+ || allGuarded n ist

362+ then Guarded

363+ else Unguarded in

364+ mkChange n args pargs ++

365+ concatMap (\x -> findCalls cases nguarded x pvs pargs) args

366+ where notPartial (Just (Partial NotCovering)) = False

367+ notPartial _ = True

368+ findCalls cases guarded (App _ f a) pvs pargs

369+ = findCalls cases Unguarded f pvs pargs ++ findCalls cases Unguarded a pvs pargs

370+ findCalls cases guarded (Bind n (Let t v) e) pvs pargs

371+ = findCalls cases Unguarded t pvs pargs ++

372+ findCalls cases Unguarded v pvs pargs ++

373+ -- Substitute in the scope since this might reveal some useful

374+ -- structure

375+ findCalls cases guarded (substV v e) pvs pargs

376+ findCalls cases guarded (Bind n t e) pvs pargs

377+ = findCalls cases Unguarded (binderTy t) pvs pargs ++

378+ findCalls cases guarded e (n : pvs) pargs

379+ findCalls cases guarded (P _ f _ ) pvs pargs

380+ | not (f `elem` pvs) = [(f, [])]

381+ findCalls _ _ _ _ _ = []

382+

383+ -- Assumption is that names are preserved in the case block (shadowing

384+ -- dealt with by the elaborator) so we can just assume the top level names

385+ -- are okay for building the size change

386+ findCallsCase cases guarded n args pvs pargs

387+ = case lookupDefExact n (tt_ctxt ist) of

388+ Just (CaseOp _ _ _ pats _ cd) ->

389+ concatMap (fccPat cases pvs pargs args guarded) (rights pats)

390+ Nothing -> []

391+

392+ fccPat cases pvs pargs args g (lhs, rhs)

393+ = let lhs' = delazy lhs

394+ rhs' = delazy rhs

395+ (f, pargs_case) = unApply (dePat lhs')

396+ -- pargs is a pair of a term, and the argument position that

397+ -- term appears in. If any of the arguments to the case block

398+ -- are also on the lhs, we also want those patterns to appear

399+ -- in the parg list so that we'll spot patterns which are

400+ -- smaller than then

401+ newpargs = newPArg args pargs

402+ -- Now need to update the rhs of the case with the names in the

403+ -- outer definition: In rhs', wherever we see what's in pargs_case,

404+ -- replace it with the corresponding thing in pargs

405+ csubs = zip pargs_case args

406+ newrhs = doCaseSubs csubs (dePat rhs')

407+ pargs' = pargs ++ addPArg newpargs pargs_case in

408+ findCalls cases g newrhs pvs pargs'

409+ where

410+ doCaseSubs [] tm = tm

411+ doCaseSubs ((x, x') : cs) tm

412+ = doCaseSubs (subIn x x' cs) (substTerm x x' tm)

413+

414+ subIn x x' [] = []

415+ subIn x x' ((l, r) : cs)

416+ = (substTerm x x' l, substTerm x x' r) : subIn x x' cs

417+

418+ addPArg (Just (t, i) : ts) (t' : ts') = (t', i) : addPArg ts ts'

419+ addPArg (Nothing : ts) (t' : ts') = addPArg ts ts'

420+ addPArg _ _ = []

421+

422+ newPArg :: [Term] -> [(Term, Int)] -> [Maybe (Term, Int)]

423+ newPArg (t : ts) pargs = case lookup t pargs of

424+ Just i -> Just (t, i) : newPArg ts pargs

425+ Nothing -> Nothing : newPArg ts pargs

426+ newPArg [] pargs = []

427+

428+ expandToArity n args

429+ = case lookupTy n (tt_ctxt ist) of

430+ [ty] -> expand 0 (normalise (tt_ctxt ist) [] ty) args

431+ _ -> args

432+ where expand i (Bind n (Pi _ _ _) sc) (x : xs) = x : expand (i + 1) sc xs

433+ expand i (Bind n (Pi _ _ _) sc) [] = Just (i, Same) : expand (i + 1) sc []

434+ expand i _ xs = xs

435+

436+ mkChange n args pargs = [(n, expandToArity n (sizes args))]

437+ where

438+ sizes [] = []

439+ sizes (a : as) = checkSize a pargs : sizes as

440+

441+ -- find which argument in pargs <a> is smaller than, if any

442+ checkSize a ((p, i) : ps)

443+ | a == p = Just (i, Same)

444+ | (P _ (UN as) _, [_,_,arg,_]) <- unApply a,

445+ as == txt "assert_smaller" && arg == p

446+ = Just (i, Smaller)

447+ | smaller Nothing a (p, Nothing) = Just (i, Smaller)

448+ | otherwise = checkSize a ps

449+ checkSize a [] = Nothing

450+

451+ -- the smaller thing we find must be defined in the same group of mutally

452+ -- defined types as <a>, and not be coinductive - so carry the type of

453+ -- the constructor we've gone under.

454+

455+ smaller (Just tyn) a (t, Just tyt)

456+ | a == t = isInductive (fst (unApply (getRetTy tyn)))

457+ (fst (unApply (getRetTy tyt)))

458+ smaller ty a (ap@(App _ f s), _)

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

460+ = let tyn = getType n in

461+ any (smaller (ty `mplus` Just tyn) a)

462+ (zip args (map toJust (getArgTys tyn)))

463+ -- check higher order recursive arguments

464+ smaller ty (App _ f s) a = smaller ty f a

465+ smaller _ _ _ = False

466+

467+ toJust (n, t) = Just t

468+

469+ getType n = case lookupTyExact n (tt_ctxt ist) of

470+ Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist

471+

472+ isInductive (P _ nty _) (P _ nty' _) =

473+ let (co, muts) = case lookupCtxt nty (idris_datatypes ist) of

474+ [TI _ x _ _ muts] -> (x, muts)

475+ _ -> (False, []) in

476+ (nty == nty' || any (== nty') muts) && not co

477+ isInductive _ _ = False

478+

479+ dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)

480+ dePat t = t

481+

482+ patvars (Bind x (PVar _) sc) = x : patvars sc

483+ patvars _ = []

484+

485+ allGuarded n ist = case lookupCtxtExact n (idris_flags ist) of

486+ Nothing -> False

487+ Just fs -> AllGuarded `elem` fs

488+

489+checkSizeChange :: Name -> Idris Totality

490+checkSizeChange n = do

491+ ist <- getIState

492+ case lookupCtxt n (idris_callgraph ist) of

493+ [cg] -> do let ms = mkMultiPaths ist [] (scg cg)

494+ logCoverage 5 ("Multipath for " ++ show n ++ ":\n" ++

495+ "from " ++ show (scg cg) ++ "\n" ++

496+ show (length ms) ++ "\n" ++

497+ showSep "\n" (map show ms))

498+ logCoverage 6 (show cg)

499+ -- every multipath must have an infinitely descending

500+ -- thread, then the function terminates

501+ -- also need to checks functions called are all total

502+ -- (Unchecked is okay as we'll spot problems here)

503+ let tot = map (checkMP ist n (getArity ist n)) ms

504+ logCoverage 4 $ "Generated " ++ show (length tot) ++ " paths"

505+ logCoverage 5 $ "Paths for " ++ show n ++ " yield " ++

506+ (showSep "\n" (map show (zip ms tot)))

507+ return (noPartial tot)

508+ [] -> do logCoverage 5 $ "No paths for " ++ show n

509+ return Unchecked

510+ where getArity ist n

511+ = case lookupTy n (tt_ctxt ist) of

512+ [ty] -> arity (normalise (tt_ctxt ist) [] ty)

513+ _ -> error "Can't happen: checkSizeChange.getArity"

514+

515+type MultiPath = [SCGEntry]

516+

517+mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]

518+mkMultiPaths ist path [] = [reverse path]

519+mkMultiPaths ist path cg = concatMap extend cg

520+ where extend (nextf, args)

521+ | (nextf, args) `inPath` path = [ reverse ((nextf, args) : path) ]

522+ | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)

523+ = case lookupCtxt nextf (idris_callgraph ist) of

524+ [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)

525+ _ -> [ reverse ((nextf, args) : path) ]

526+ | otherwise = [ reverse ((nextf, args) : path) ]

527+

528+ inPath :: SCGEntry -> [SCGEntry] -> Bool

529+ inPath f [] = False

530+ inPath f (g : gs) = smallerEq f g || f == g || inPath f gs

531+

532+ smallerEq :: SCGEntry -> SCGEntry -> Bool

533+ smallerEq (f, args) (g, args')

534+ = f == g && not (null (filter smallers args))

535+ && filter smallers args == filter smallers args'

536+ smallers (Just (_, Smaller)) = True

537+ smallers _ = False

538+

539+-- If any route along the multipath leads to infinite descent, we're fine.

540+-- Try a route beginning with every argument.

541+-- If we reach a point we've been to before, but with a smaller value,

542+-- that means there is an infinitely descending path from that argument.

543+

544+checkMP :: IState -> Name -> Int -> MultiPath -> Totality

545+checkMP ist topfn i mp = if i > 0

546+ then let paths = (map (tryPath 0 [] mp) [0..i-1]) in

547+-- trace ("Paths " ++ show paths) $

548+ collapse paths

549+ else tryPath 0 [] mp 0

550+ where

551+ tryPath' d path mp arg

552+ = let res = tryPath d path mp arg in

553+ trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res

554+

555+ mkBig (e, d) = (e, 10000)

556+

557+ tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality

558+ tryPath desc path [] _ = Total []

559+-- tryPath desc path ((UN "believe_me", _) : _) arg

560+-- = Partial BelieveMe

561+ -- if we get to a constructor, it's fine as long as it's strictly positive

562+ tryPath desc path ((f, _) : es) arg

563+ | [TyDecl (DCon _ _ _) _] <- lookupDef f (tt_ctxt ist)

564+ = case lookupTotalExact f (tt_ctxt ist) of

565+ Just (Total _) -> Unchecked -- okay so far

566+ Just (Partial _) -> Partial (Other [f])

567+ x -> Unchecked -- An error elsewhere, set as Unchecked to make

568+ -- some progress

569+ | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)

570+ = Total []

571+ tryPath desc path (e@(f, args) : es) arg

572+ | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a

573+ | e `elem` es && allNothing args = Partial (Mutual [f])

574+ tryPath desc path (e@(f, nextargs) : es) arg

575+ | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a

576+ | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])

577+ | Just d <- lookup (e, arg) path

578+ = if desc - d > 0 -- Now lower than when we were last here

579+ then -- trace ("Descent " ++ show (desc - d) ++ " "

580+ -- ++ show (path, e)) $

581+ Total []

582+ else Partial (Mutual (map (fst . fst . fst) path ++ [f]))

583+ | e `elem` map (fst . fst) path

584+ && not (f `elem` map fst es)

585+ = Partial (Mutual (map (fst . fst . fst) path ++ [f]))

586+ | [Unchecked] <- lookupTotal f (tt_ctxt ist) =

587+ let argspos = zip nextargs [0..]

588+ pathres =

589+ do (a, pos) <- argspos

590+ case a of

591+ Nothing -> -- gone up, but if the

592+ -- rest definitely terminates without any

593+ -- cycles (including the path so far, which

594+ -- we take as inaccessible) the path is fine

595+ return $ tryPath 0 (map mkBig (((e, arg), desc) : path)) es pos

596+ Just (nextarg, sc) ->

597+ if nextarg == arg then

598+ case sc of

599+ Same -> return $ tryPath desc (((e, arg), desc) : path)

600+ es pos

601+ Smaller -> return $ tryPath (desc+1)

602+ (((e, arg), desc) : path)

603+ es

604+ pos

605+ _ -> trace ("Shouldn't happen " ++ show e) $

606+ return (Partial Itself)

607+ else return Unchecked in

608+-- trace (show (desc, argspos, path, es, pathres)) $

609+ collapse pathres

610+

611+ | otherwise = Unchecked

612+

613+allNothing :: [Maybe a] -> Bool

614+allNothing xs = null (collapseNothing (zip xs [0..]))

615+

616+collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]

617+collapseNothing ((Nothing, t) : xs)

618+ = (Nothing, t) : filter (\ (x, _) -> case x of

619+ Nothing -> False

620+ _ -> True) xs

621+collapseNothing (x : xs) = x : collapseNothing xs

622+collapseNothing [] = []

623+

624+noPartial :: [Totality] -> Totality

625+noPartial (Partial p : xs) = Partial p

626+noPartial (_ : xs) = noPartial xs

627+noPartial [] = Total []

628+

629+collapse :: [Totality] -> Totality

630+collapse xs = collapse' Unchecked xs

631+collapse' def (Total r : xs) = Total r

632+collapse' def (Unchecked : xs) = collapse' def xs

633+collapse' def (d : xs) = collapse' d xs

634+-- collapse' Unchecked [] = Total []

635+collapse' def [] = def

636+

637+totalityCheckBlock :: Idris ()

638+totalityCheckBlock = do

639+ ist <- getIState

640+ -- Do totality checking after entire mutual block

641+ mapM_ (\n -> do logElab 5 $ "Simplifying " ++ show n

642+ ctxt' <- do ctxt <- getContext

643+ tclift $ simplifyCasedef n (getErasureInfo ist) ctxt

644+ setContext ctxt')

645+ (map snd (idris_totcheck ist))

646+ mapM_ buildSCG (idris_totcheck ist)

647+ mapM_ checkDeclTotality (idris_totcheck ist)

648+ clear_totcheck

649+