ec3daa4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Make sure deferred definitions get totality checked

ec3daa4Edwin Brady13 years ago

libs/prelude/Prelude/List.idr+2−2

compare with master

unifiedsplit

@@ -306,7 +306,7 @@ find p (x::xs) =

306findIndex : (a -> Bool) -> List a -> Maybe Nat

307findIndex = findIndex' Z

308 where

309−-- findIndex' : Nat -> (a -> Bool) -> List a -> Maybe Nat

309+ findIndex' : Nat -> (a -> Bool) -> List a -> Maybe Nat

310 findIndex' cnt p [] = Nothing

311 findIndex' cnt p (x::xs) =

312 if p x then

@@ -317,7 +317,7 @@ findIndex = findIndex' Z

317findIndices : (a -> Bool) -> List a -> List Nat

318findIndices = findIndices' Z

319 where

320−-- findIndices' : Nat -> (a -> Bool) -> List a -> List Nat

320+ findIndices' : Nat -> (a -> Bool) -> List a -> List Nat

321 findIndices' cnt p [] = []

322 findIndices' cnt p (x::xs) =

323 if p x then

src/Idris/AbsSyntax.hs+5

@@ -96,6 +96,11 @@ addTrans t = do i <- getIState

96totcheck :: (FC, Name) -> Idris ()

97totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

99+defer_totcheck :: (FC, Name) -> Idris ()

100+defer_totcheck n

101+ = do i <- getIState;

102+ putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }

103+

99clear_totcheck :: Idris ()

104clear_totcheck :: Idris ()

100clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }

105clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }

101

106

src/Idris/AbsSyntaxTree.hs+3−2

@@ -96,7 +96,8 @@ data IState = IState {

96 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

97 idris_calledgraph :: Ctxt [Name],

98 idris_docstrings :: Ctxt String,

99− idris_totcheck :: [(FC, Name)],

99+ idris_totcheck :: [(FC, Name)], -- names to check totality on

100+ idris_defertotcheck :: [(FC, Name)], -- names to check at the end

100 idris_options :: IOption,

101 idris_options :: IOption,

101 idris_name :: Int,

102 idris_name :: Int,

102 idris_lineapps :: [((FilePath, Int), PTerm)],

103 idris_lineapps :: [((FilePath, Int), PTerm)],

@@ -186,7 +187,7 @@ data IBCWrite = IBCFix FixDecl

186idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

187idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

187 emptyContext emptyContext emptyContext emptyContext

188 emptyContext emptyContext emptyContext emptyContext

189 emptyContext emptyContext emptyContext emptyContext

189− [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

190+ [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

190 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

191 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

191 True defaultTheme stdout

192 True defaultTheme stdout

192

193

src/Idris/Coverage.hs+29−9

@@ -423,7 +423,15 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

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

424 findCalls _ _ _ = []

425

426+ expandToArity n args

427+ = case lookupTy n (tt_ctxt ist) of

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

429+ _ -> args

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

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

432+ expand i _ xs = xs

433+

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

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

427 where

435 where

428 sizes [] = []

436 sizes [] = []

429 sizes (a : as) = checkSize a pargs 0 : sizes as

437 sizes (a : as) = checkSize a pargs 0 : sizes as

@@ -574,12 +582,16 @@ checkSizeChange n = do

574 -- thread, then the function terminates

582 -- thread, then the function terminates

575 -- also need to checks functions called are all total

583 -- also need to checks functions called are all total

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

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

577− let tot = map (checkMP ist (length (argsdef cg))) ms

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

578 logLvl 4 $ "Generated " ++ show (length tot) ++ " paths"

586 logLvl 4 $ "Generated " ++ show (length tot) ++ " paths"

579 logLvl 6 $ "Paths for " ++ show n ++ " yield " ++ (show tot)

587 logLvl 6 $ "Paths for " ++ show n ++ " yield " ++ (show tot)

580 return (noPartial tot)

588 return (noPartial tot)

581 [] -> do logLvl 5 $ "No paths for " ++ show n

589 [] -> do logLvl 5 $ "No paths for " ++ show n

582 return Unchecked

590 return Unchecked

591+ where getArity ist n

592+ = case lookupTy n (tt_ctxt ist) of

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

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

583

595

584type MultiPath = [SCGEntry]

596type MultiPath = [SCGEntry]

585

597

@@ -609,7 +621,9 @@ mkMultiPaths ist path cg

609

621

610checkMP :: IState -> Int -> MultiPath -> Totality

622checkMP :: IState -> Int -> MultiPath -> Totality

611checkMP ist i mp = if i > 0

623checkMP ist i mp = if i > 0

612− then collapse (map (tryPath 0 [] mp) [0..i-1])

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

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

626+ collapse paths

613 else tryPath 0 [] mp 0

627 else tryPath 0 [] mp 0

614 where

628 where

615 tryPath' d path mp arg

629 tryPath' d path mp arg

@@ -635,12 +649,15 @@ checkMP ist i mp = if i > 0

635 | Just d <- lookup e path

649 | Just d <- lookup e path

636 = if desc > 0

650 = if desc > 0

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

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

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

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

639 Total []

653 Total []

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

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

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

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

642− let argspos = collapseNothing (zip nextargs [0..]) in

656+ let argspos = case collapseNothing (zip nextargs [0..]) of

643− collapse' Unchecked $

657+ [] -> [(Nothing, 0)]

658+ x -> x

659+-- trace (show (argspos, nextargs, path)) $

660+ pathres =

644 do (a, pos) <- argspos

661 do (a, pos) <- argspos

645 case a of

662 case a of

646 Nothing -> -- don't know, but if the

663 Nothing -> -- don't know, but if the

@@ -662,7 +679,10 @@ checkMP ist i mp = if i > 0

662 pos

679 pos

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

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

664 return (Partial Itself)

681 return (Partial Itself)

665− else return Unchecked

682+ else return Unchecked in

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

684+ collapse' Unchecked pathres

685+

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

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

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

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

668 | otherwise = Unchecked

688 | otherwise = Unchecked

@@ -671,8 +691,8 @@ allNothing xs = null (collapseNothing (zip xs [0..]))

671

691

672collapseNothing ((Nothing, _) : xs)

692collapseNothing ((Nothing, _) : xs)

673 = filter (\ (x, _) -> case x of

693 = filter (\ (x, _) -> case x of

674− Nothing -> False

694+ Nothing -> False

675− _ -> True) xs

695+ _ -> True) xs

676collapseNothing (x : xs) = x : collapseNothing xs

696collapseNothing (x : xs) = x : collapseNothing xs

677collapseNothing [] = []

697collapseNothing [] = []

678

698

src/Idris/ElabDecls.hs+5

@@ -1005,6 +1005,11 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1005 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

1006 addDeferred def''

1007

1008+ when (not (null def')) $ do

1009+ -- check these at the end, when definitions are complete

1010+ defer_totcheck (fc, fname)

1011+ mapM_ defer_totcheck (map (\x -> (fc, fst x)) def'')

1012+

1008 -- Now the remaining deferred (i.e. no type declarations) clauses

1013 -- Now the remaining deferred (i.e. no type declarations) clauses

1009 -- from the where block

1014 -- from the where block

1010

1015

src/Idris/Parser.hs+8

@@ -1043,6 +1043,14 @@ loadSource h lidr f

1043 i <- getIState

1044 mapM_ buildSCG (idris_totcheck i)

1045 mapM_ checkDeclTotality (idris_totcheck i)

1046+

1047+ -- Redo totality check for deferred names

1048+ let deftots = idris_defertotcheck i

1049+ iLOG $ "Totality checking " ++ show deftots

1050+ mapM_ (\x -> setTotality x Unchecked) (map snd deftots)

1051+ mapM_ buildSCG deftots

1052+ mapM_ checkDeclTotality deftots

1053+

1046 iLOG ("Finished " ++ f)

1054 iLOG ("Finished " ++ f)

1047 ibcsd <- valIBCSubDir i

1055 ibcsd <- valIBCSubDir i

1048 iLOG "Universe checking"

1056 iLOG "Universe checking"