ec3daa4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make sure deferred definitions get totality checked

Fixes #677. Now deferred definitions are all checked at the end of checking a module. Also, a minor fix for the situation where a function had no descending or same arguments, which was getting ignored.

commitec3daa4a0714e0e0d006cc035cc87776d55925d4 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 27 Nov 2013, 12:26 (13 years ago) parentb3bf956

6 files changed+52−13

compare with master

unifiedsplit

libs/prelude/Prelude/List.idr+2−2 src/Idris/AbsSyntax.hs+5 src/Idris/AbsSyntaxTree.hs+3−2 src/Idris/Coverage.hs+29−9 src/Idris/ElabDecls.hs+5 src/Idris/Parser.hs+8

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

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

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

307307findIndex = findIndex' Z

308308 where

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

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

310310 findIndex' cnt p [] = Nothing

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

312312 if p x then

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

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

318318findIndices = findIndices' Z

319319 where

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

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

321321 findIndices' cnt p [] = []

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

323323 if p x then

src/Idris/AbsSyntax.hs+5

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

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

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

9898

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+

99104clear_totcheck :: Idris ()

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

101106

src/Idris/AbsSyntaxTree.hs+3−2

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

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

9797 idris_calledgraph :: Ctxt [Name],

9898 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

100101 idris_options :: IOption,

101102 idris_name :: Int,

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

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

186187idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

187188 emptyContext emptyContext emptyContext emptyContext

188189 emptyContext emptyContext emptyContext emptyContext

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

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

190191 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

191192 True defaultTheme stdout

192193

src/Idris/Coverage.hs+29−9

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

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

424424 findCalls _ _ _ = []

425425

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

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+

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

427435 where

428436 sizes [] = []

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

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

574582 -- thread, then the function terminates

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

576584 -- (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

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

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

580588 return (noPartial tot)

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

582590 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"

583595

584596type MultiPath = [SCGEntry]

585597

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

609621

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

611623checkMP 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

613627 else tryPath 0 [] mp 0

614628 where

615629 tryPath' d path mp arg

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

635649 | Just d <- lookup e path

636650 = if desc > 0

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

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

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

639653 Total []

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

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

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

643− collapse' Unchecked $

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

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

658+ x -> x

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

660+ pathres =

644661 do (a, pos) <- argspos

645662 case a of

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

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

662679 pos

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

664681 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+

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

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

668688 | otherwise = Unchecked

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

671691

672692collapseNothing ((Nothing, _) : xs)

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

674− Nothing -> False

675− _ -> True) xs

694+ Nothing -> False

695+ _ -> True) xs

676696collapseNothing (x : xs) = x : collapseNothing xs

677697collapseNothing [] = []

678698

src/Idris/ElabDecls.hs+5

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

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

10061006 addDeferred def''

10071007

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+

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

10091014 -- from the where block

10101015

src/Idris/Parser.hs+8

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

10431043 i <- getIState

10441044 mapM_ buildSCG (idris_totcheck i)

10451045 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+

10461054 iLOG ("Finished " ++ f)

10471055 ibcsd <- valIBCSubDir i

10481056 iLOG "Universe checking"