54ad219 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add size change termination

54ad219Edwin Brady14 years ago

lib/Prelude/List.idr+1−1

compare with master

unifiedsplit

@@ -167,7 +167,7 @@ zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)

167

168zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->

169 (z : List c) -> (length x = length y) -> (length y = length z) -> List d

170−zipWith3 f [] [] [] p q = []

170+zipWith3 f [] [] [] refl refl = []

171zipWith3 f (x::xs) (y::ys) (z::zs) p q =

172 f x y z :: (zipWith3 f xs ys zs ?zipWith3TailProof ?zipWith3TailProof')

173

src/Core/Evaluate.hs+2−1

@@ -759,7 +759,8 @@ lookupP root n ctxt

759lookupDef :: Maybe [String] -> Name -> Context -> [Def]

760lookupDef root n ctxt = map tfst $ lookupCtxt root n (definitions ctxt)

761

762−lookupDefAcc :: Maybe [String] -> Name -> Bool -> Context -> [(Def, Accessibility)]

762+lookupDefAcc :: Maybe [String] -> Name -> Bool -> Context ->

763+ [(Def, Accessibility)]

763lookupDefAcc root n mkpublic ctxt

764lookupDefAcc root n mkpublic ctxt

764 = map mkp $ lookupCtxt root n (definitions ctxt)

765 = map mkp $ lookupCtxt root n (definitions ctxt)

765 where mkp (d, a, _) = if mkpublic then (d, Public) else (d, a)

766 where mkp (d, a, _) = if mkpublic then (d, Public) else (d, a)

src/Idris/AbsSyntaxTree.hs+4−2

@@ -82,14 +82,16 @@ data IState = IState {

82 }

84data SizeChange = Smaller | Same | Bigger | Unknown

85− deriving Show

85+ deriving (Show, Eq)

86{-!

87deriving instance Binary SizeChange

88!-}

90+type SCGEntry = (Name, [Maybe (Int, SizeChange)])

91+

90data CGInfo = CGInfo { argsdef :: [Name],

92data CGInfo = CGInfo { argsdef :: [Name],

91 calls :: [(Name, [[Name]])],

93 calls :: [(Name, [[Name]])],

92− scg :: [(Name, [Maybe (Name, SizeChange)])],

94+ scg :: [SCGEntry],

93 argsused :: [Name],

95 argsused :: [Name],

94 unusedpos :: [Int] }

96 unusedpos :: [Int] }

95 deriving Show

97 deriving Show

src/Idris/Coverage.hs+165−107

@@ -12,6 +12,7 @@ import Idris.Error

13import Data.List

14import Data.Either

15+import Data.Maybe

15import Debug.Trace

16import Debug.Trace

17import Control.Monad.State

18import Control.Monad.State

@@ -22,12 +23,14 @@ import Control.Monad.State

22genMissing :: Name -> [Name] -> SC -> Idris [PTerm]

23genMissing :: Name -> [Name] -> SC -> Idris [PTerm]

23genMissing fn args sc

24genMissing fn args sc

24 = do sc' <- expandTree sc

25 = do sc' <- expandTree sc

25− logLvl 5 $ "Checking missing cases for " ++ show fn ++ "\n" ++ (show sc')

26+ logLvl 5 $ "Checking missing cases for " ++

27+ show fn ++ "\n" ++ (show sc')

26 (got, missing) <- gm fn (map (\x -> P Bound x Erased) args) sc'

28 (got, missing) <- gm fn (map (\x -> P Bound x Erased) args) sc'

27 return $ filter (\x -> not (x `elem` got)) missing

29 return $ filter (\x -> not (x `elem` got)) missing

29-- Make a term to feed to the pattern matcher from a LHS declared impossible

31-- Make a term to feed to the pattern matcher from a LHS declared impossible

30−-- (we can't type check it, but we need the case analysis to check for covering...)

32+-- (we can't type check it, but we need the case analysis to check for

33+-- covering...)

32mkPatTm :: PTerm -> Idris Term

35mkPatTm :: PTerm -> Idris Term

33mkPatTm t = do i <- get

36mkPatTm t = do i <- get

@@ -69,7 +72,8 @@ gm fn args (UnmatchedCase _) = do logLvl 3 ("Missing: " ++ show args)

70gmAlt fn args n (ConCase cn t cargs sc)

73gmAlt fn args n (ConCase cn t cargs sc)

71 = do let args' = map (subst n (mkApp (P Bound cn Erased)

74 = do let args' = map (subst n (mkApp (P Bound cn Erased)

72− (map (\x -> P Bound x Erased) cargs))) args

75+ (map (\x -> P Bound x Erased) cargs)))

76+ args

73 gm fn args' sc

77 gm fn args' sc

74gmAlt fn args n (ConstCase c sc)

78gmAlt fn args n (ConstCase c sc)

75 = do let args' = map (subst n (Constant c)) args

79 = do let args' = map (subst n (Constant c)) args

@@ -87,7 +91,8 @@ dropDefault [] = []

88expandTree :: SC -> Idris SC

92expandTree :: SC -> Idris SC

89expandTree (Case n alts) = do i <- get

93expandTree (Case n alts) = do i <- get

90− as <- expandAlts i (dropDefault alts) (getDefault alts)

94+ as <- expandAlts i (dropDefault alts)

95+ (getDefault alts)

91 alts' <- mapM expandTreeA as

96 alts' <- mapM expandTreeA as

92 return (Case n alts')

97 return (Case n alts')

93 where expandTreeA (ConCase n i ns sc) = do sc' <- expandTree sc

98 where expandTreeA (ConCase n i ns sc) = do sc' <- expandTree sc

@@ -116,15 +121,17 @@ expandAlts i all@(ConCase n _ _ _ : alts) def

116 addAlts [] got alts = alts

121 addAlts [] got alts = alts

117 addAlts ((n, arity) : ps) got alts

122 addAlts ((n, arity) : ps) got alts

118 | n `elem` got = addAlts ps got alts

123 | n `elem` got = addAlts ps got alts

119− | otherwise = addAlts ps got (alts ++ [ConCase n (-1) (argList arity) def])

124+ | otherwise = addAlts ps got (alts ++

125+ [ConCase n (-1) (argList arity) def])

120

126

121 argList i = take i (map (\x -> (MN x "ign")) [0..])

127 argList i = take i (map (\x -> (MN x "ign")) [0..])

122

128

129+ getTy n ctxt

123− getTy n ctxt = case lookupTy Nothing n ctxt of

130+ = case lookupTy Nothing n ctxt of

124− (t : _) -> case unApply (getRetTy t) of

131+ (t : _) -> case unApply (getRetTy t) of

125− (P _ tyn _, _) -> tyn

132+ (P _ tyn _, _) -> tyn

126− x -> error $ "Can't happen getTy 1 " ++ show (n, x)

133+ x -> error $ "Can't happen getTy 1 " ++ show (n, x)

127− _ -> error "Can't happen getTy 2"

134+ _ -> error "Can't happen getTy 2"

128

135

129 mkPat x = case lookupCtxt Nothing x (idris_implicits i) of

136 mkPat x = case lookupCtxt Nothing x (idris_implicits i) of

130 (pargs : _)

137 (pargs : _)

@@ -152,14 +159,14 @@ genClauses fc n xs given

152 logLvl 7 $ "COVERAGE of " ++ show n

159 logLvl 7 $ "COVERAGE of " ++ show n

153 logLvl 10 $ show argss ++ "\n" ++ show all_args

160 logLvl 10 $ show argss ++ "\n" ++ show all_args

154 logLvl 10 $ "Original: \n" ++

161 logLvl 10 $ "Original: \n" ++

155− showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)

162+ showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)

156 let parg = case lookupCtxt Nothing n (idris_implicits i) of

163 let parg = case lookupCtxt Nothing n (idris_implicits i) of

157 (p : _) -> p

164 (p : _) -> p

158 _ -> repeat (pexp Placeholder)

165 _ -> repeat (pexp Placeholder)

159 let tryclauses = mkClauses parg all_args

166 let tryclauses = mkClauses parg all_args

160 let new = mnub i $ filter (noMatch i) tryclauses

167 let new = mnub i $ filter (noMatch i) tryclauses

161 logLvl 7 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)

168 logLvl 7 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)

162−-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)

169+-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)

163 return new

170 return new

164-- return (map (\t -> PClause n t [] PImpossible []) new)

171-- return (map (\t -> PClause n t [] PImpossible []) new)

165 where getLHS i term

172 where getLHS i term

@@ -195,8 +202,8 @@ genClauses fc n xs given

195 as' <- mkArg as

202 as' <- mkArg as

196 return (a':as')

203 return (a':as')

197

204

198−-- FIXME: Just look for which one is the deepest, then generate all possibilities

205+-- FIXME: Just look for which one is the deepest, then generate all

199−-- up to that depth.

206+-- possibilities up to that depth.

200

207

201genAll :: IState -> [PTerm] -> [PTerm]

208genAll :: IState -> [PTerm] -> [PTerm]

202genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of

209genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of

@@ -257,7 +264,8 @@ checkPositive n (cn, ty)

257 = n /= n' && posArg sc

264 = n /= n' && posArg sc

258 posArg t = True

265 posArg t = True

259

266

260−-- Totality checking - check for structural recursion (no mutual definitions yet)

267+-- Totality checking - check for structural recursion

268+-- (no mutual definitions yet)

261

269

262data LexOrder = LexXX | LexEQ | LexLT

270data LexOrder = LexXX | LexEQ | LexLT

263 deriving (Show, Eq, Ord)

271 deriving (Show, Eq, Ord)

@@ -268,7 +276,8 @@ calcProd i fc n pats = do patsprod <- mapM prodRec pats

268 then return Productive

276 then return Productive

269 else return (Partial NotProductive)

277 else return (Partial NotProductive)

270 where

278 where

271− -- every application of n must be in an argument of a coinductive constructor

279+ -- every application of n must be in an argument of a coinductive

280+ -- constructor

272

281

273 prodRec :: ([Name], Term, Term) -> Idris Bool

282 prodRec :: ([Name], Term, Term) -> Idris Bool

274 prodRec (_, _, tm) = prod False tm

283 prodRec (_, _, tm) = prod False tm

@@ -294,88 +303,25 @@ calcProd i fc n pats = do patsprod <- mapM prodRec pats

294 _ -> False

303 _ -> False

295 | otherwise = False

304 | otherwise = False

296

305

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

306+calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)]

307+ -> Idris Totality

298calcTotality path fc n pats

308calcTotality path fc n pats

299 = do i <- get

309 = do i <- get

300 let opts = case lookupCtxt Nothing n (idris_flags i) of

310 let opts = case lookupCtxt Nothing n (idris_flags i) of

301 [fs] -> fs

311 [fs] -> fs

302 _ -> []

312 _ -> []

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

314+ (failure : _) -> return failure

303− if (Coinductive `elem` opts) then calcProd i fc n pats

315+ _ -> if (Coinductive `elem` opts)

304− else do orders <- mapM ctot pats

316+ then calcProd i fc n pats

305− let order = sortBy cmpOrd $ concat orders

317+ else checkSizeChange n

306− let (errs, valid) = partitionEithers order

307− let lex = stripNoLT (stripXX valid)

308− case errs of

309− [] -> do logLvl 3 $ show n ++ ":\n" ++ showSep "\n" (map show lex)

310− logLvl 10 $ show pats

311− checkDecreasing lex

312− (e : _) -> return e -- FIXME: should probably combine them

313 where

318 where

314− cmpOrd (Left _) (Left _) = EQ

319+ checkLHS i (P _ fn _)

315− cmpOrd (Left _) (Right _) = LT

320+ = case lookupTotal fn (tt_ctxt i) of

316− cmpOrd (Right _) (Left _) = GT

317− cmpOrd (Right x) (Right y) = compare x y

318−

319− checkDecreasing [] = return (Total [])

320− checkDecreasing (c : cs) | dec c = checkDecreasing cs

321− | otherwise = return (Partial Itself)

322−

323− dec [] = False

324− dec (LexLT : _) = True

325− dec (LexEQ : xs) = dec xs

326− dec (LexXX : xs) = False

327−

328− stripXX [] = []

329− stripXX v@(c : cs)

330− = case span (==LexXX) c of

331− (ns, rest) -> map (drop (length ns)) v

332−

333− -- argument positions which are never LT are no use to us

334− stripNoLT [] = [] -- no recursive calls

335− stripNoLT xs = case transpose (filter (any (==LexLT)) (transpose xs)) of

336− [] -> [[]] -- recursive calls are all useless...

337− xs -> xs

338−

339− ctot (_, lhs, rhs)

340− | (_, args) <- unApply lhs

341− = do -- check lhs doesn't use any dodgy names

342− lhsOK <- mapM (chkOrd [] []) args

343− chkOrd (filter isLeft (concat lhsOK)) args rhs

344−

345− isLeft (Left _) = True

346− isLeft _ = False

347−

348− chkOrd ords args (Bind n (Let t v) sc)

349− = do ov <- chkOrd ords args v

350− chkOrd ov args sc

351− chkOrd ords args (Bind n b sc) = chkOrd ords (args ++ [P Ref n Erased]) sc

352− chkOrd ords args ap@(App f a)

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

354− = if fn == n && length args == length args'

355− then do orf <- chkOrd (Right (zipWith lexOrd args args') : ords) args f

356− chkOrd orf args a

357− else do orf <- chkOrd ords args f

358− chkOrd orf args a

359− | otherwise = do orf <- chkOrd ords args f

360− chkOrd orf args a

361− chkOrd ords args (P _ fn _)

362− | n /= fn

363− = do tf <- checkTotality (n : path) fc fn

364− case tf of

365− Total _ -> return ords

366− p@(Partial (Mutual x)) -> return ((Left p) : ords)

367− _ -> return (Left (Partial (Other [fn])) : ords)

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

368− | null args = return (Left (Partial Itself) : ords)

322+ _ -> Nothing

369− chkOrd ords args _ = return ords

323+ checkLHS i (App f a) = mplus (checkLHS i f) (checkLHS i a)

370−

324+ checkLHS _ _ = Nothing

371− lexOrd x y | x == y = LexEQ

372− lexOrd f@(App _ _) x

373− | (f', args) <- unApply f

374− = let ords = map (\x' -> lexOrd x' x) args in

375− if any (\o -> o == LexEQ || o == LexLT) ords

376− then LexLT

377− else LexXX

378− lexOrd _ _ = LexXX

379

325

380checkTotality :: [Name] -> FC -> Name -> Idris Totality

326checkTotality :: [Name] -> FC -> Name -> Idris Totality

381checkTotality path fc n

327checkTotality path fc n

@@ -400,10 +346,11 @@ checkTotality path fc n

400 -- typechecking decidable

346 -- typechecking decidable

401 case t' of

347 case t' of

402-- FIXME: Put this back when we can handle mutually recursive things

348-- FIXME: Put this back when we can handle mutually recursive things

403−-- p@(Partial _) ->

349+-- p@(Partial _) ->

404−-- do setAccessibility n Frozen

350+-- do setAccessibility n Frozen

405−-- addIBC (IBCAccess n Frozen)

351+-- addIBC (IBCAccess n Frozen)

406−-- iputStrLn $ "HIDDEN: " ++ show n ++ show p

352+-- iputStrLn $ "HIDDEN: "

353+-- ++ show n ++ show p

407 _ -> return ()

354 _ -> return ()

408 return t'

355 return t'

409 _ -> return $ Total []

356 _ -> return $ Total []

@@ -429,16 +376,29 @@ checkDeclTotality (fc, n)

429

376

430-- where g is a function called

377-- where g is a function called

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

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

432−-- sizechange1 ... sizechange2 is how their size has changed wrt the input to f

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

380+-- to f

433-- Nothing, if the argument is unrelated to the input

381-- Nothing, if the argument is unrelated to the input

434

382

383+-- FIXME: Higher order recursive arguments

384+

435−buildSCG :: IState -> SC -> [Name] -> [(Name, [Maybe (Name, SizeChange)])]

385+buildSCG :: IState -> SC -> [Name] -> [SCGEntry]

436−buildSCG ist sc args = scg sc (zip args args) (zip args (zip args (repeat Same)))

386+buildSCG ist sc args = scg sc (zip args args)

387+ (zip args (zip args (repeat Same)))

437 where

388 where

438 scg :: SC -> [(Name, Name)] -> -- local var, originating top level var

389 scg :: SC -> [(Name, Name)] -> -- local var, originating top level var

439− [(Name, (Name, SizeChange))] -> -- map from orig to new and relationship

390+ [(Name, (Name, SizeChange))] -> -- orig to new, and relationship

440− [(Name, [Maybe (Name, SizeChange)])]

391+ [SCGEntry]

392+ scg (Case x alts) vars szs

393+ = let x' = findTL x vars in

441− scg (Case x alts) vars szs = concatMap (scgAlt x vars szs) alts

394+ concatMap (scgAlt x' vars szs) alts

395+ where

396+ findTL x vars

397+ | Just x' <- lookup x vars

398+ = if x' `elem` args then x'

399+ else findTL x' vars

400+ | otherwise = x

401+

442 scg (STerm tm) vars szs = scgTerm tm vars szs

402 scg (STerm tm) vars szs = scgTerm tm vars szs

443 scg _ _ _ = []

403 scg _ _ _ = []

444

404

@@ -458,7 +418,8 @@ buildSCG ist sc args = scg sc (zip args args) (zip args (zip args (repeat Same))

458 -- (as long as they are in the same type family)

418 -- (as long as they are in the same type family)

459 | Just tvar <- lookup x vars

419 | Just tvar <- lookup x vars

460 = let arel = argRels n

420 = let arel = argRels n

461− szs' = zipWith (\arg (_,t) -> (arg, (x, t))) args arel ++ szs

421+ szs' = zipWith (\arg (_,t) -> (arg, (x, t))) args arel

422+ ++ szs

462 vars' = zip args (repeat tvar) ++ vars in

423 vars' = zip args (repeat tvar) ++ vars in

463 scg sc vars' szs'

424 scg sc vars' szs'

464 | otherwise = scg sc vars szs

425 | otherwise = scg sc vars szs

@@ -477,11 +438,108 @@ buildSCG ist sc args = scg sc (zip args args) (zip args (zip args (repeat Same))

477 = scgTerm v vars szs ++ scgTerm e vars szs

438 = scgTerm v vars szs ++ scgTerm e vars szs

478 scgTerm (Bind n _ e) vars szs

439 scgTerm (Bind n _ e) vars szs

479 = scgTerm e ((n, n) : vars) szs

440 = scgTerm e ((n, n) : vars) szs

441+ scgTerm (P _ fn _) vars szs

442+ = case lookup fn vars of

443+ Just _ -> []

444+ Nothing -> [(fn, [])]

480 scgTerm _ _ _ = []

445 scgTerm _ _ _ = []

481

446

482− mkChange :: [(Name, (Name, SizeChange))] -> Term -> Maybe (Name, SizeChange)

447+ mkChange :: [(Name, (Name, SizeChange))] -> Term

448+ -> Maybe (Int, SizeChange)

483− mkChange szs (P _ n ty) = case lookup n szs of

449+ mkChange szs (P _ n ty)

450+ = do sc <- lookup n szs

451+ case sc of

484− Just (_, Unknown) -> Nothing

452+ (_, Unknown) -> Nothing

485− t -> t

453+ (o, sc) -> do i <- getArgPos 0 o args

454+ return (i, sc)

486 mkChange _ _ = Nothing

455 mkChange _ _ = Nothing

487

456

457+ getArgPos :: Int -> Name -> [Name] -> Maybe Int

458+ getArgPos i n [] = Nothing

459+ getArgPos i n (x : xs) | n == x = Just i

460+ | otherwise = getArgPos (i + 1) n xs

461+

462+checkSizeChange :: Name -> Idris Totality

463+checkSizeChange n = do

464+ ist <- get

465+ case lookupCtxt Nothing n (idris_callgraph ist) of

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

467+ logLvl 6 ("Multipath for " ++ show n ++ ":\n" ++

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

469+ -- every multipath must have an infinitely descending

470+ -- thread, then the function terminates

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

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

473+ let tot = map (checkMP ist (length (argsdef cg))) ms

474+ logLvl 3 $ "Paths for " ++ show n ++ " yield " ++ (show tot)

475+ return (noPartial tot)

476+

477+type MultiPath = [SCGEntry]

478+

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

480+mkMultiPaths ist path cg

481+ = do (nextf, args) <- cg

482+ if ((nextf, args) `elem` path)

483+ then return (reverse ((nextf, args) : path))

484+ else case lookupCtxt Nothing nextf (idris_callgraph ist) of

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

486+ _ -> return (reverse ((nextf, args) : path))

487+

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

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

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

491+-- that means there is an infinitely descending path.

492+

493+checkMP :: IState -> Int -> MultiPath -> Totality

494+checkMP ist i mp = if i > 0

495+ then collapse (map (tryPath 0 [] mp) [0..i-1])

496+ else tryPath 0 [] mp 0

497+ where

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

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

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

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

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

503+ = case lookupTotal f (tt_ctxt ist) of

504+ [Total _] -> Total []

505+ [Partial _] -> Partial (Other [f])

506+ x -> error (show x)

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

508+ = Total []

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

510+ | Just d <- lookup e path

511+ = if (desc - d) > 0

512+ then Total []

513+ else Partial Itself

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

515+ let argspos = zip nextargs [0..] in

516+ collapse $

517+ do (arg, pos) <- argspos

518+ case arg of

519+ Nothing -> -- don't know, but it's okay if the

520+ -- rest definitely terminates without

521+ -- any cycles with route so far

522+ map (tryPath (-10000) ((e, desc):path) es)

523+ [0..length nextargs - 1]

524+ Just (nextarg, sc) ->

525+ case sc of

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

527+ es

528+ nextarg

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

530+ ((e, desc):path)

531+ es

532+ nextarg

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

534+ return (Partial Itself)

535+ | [tot] <- lookupTotal f (tt_ctxt ist) = tot

536+ | otherwise = Total []

537+

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

539+noPartial (_ : xs) = noPartial xs

540+noPartial [] = Total []

541+

542+collapse (Total r : xs) = Total r

543+collapse (_ : xs) = collapse xs

544+collapse [] = Partial Itself

545+

src/Idris/REPL.hs+20−17

@@ -204,28 +204,31 @@ process fn (Defn n) = do i <- get

204 case lookupTotal n (tt_ctxt i) of

205 [t] -> iputStrLn (showTotal t i)

206 _ -> return ()

207+ where printCase i (_, lhs, rhs)

207− where printCase i (_, lhs, rhs) = do liftIO $ putStr $ showImp True (delab i lhs)

208+ = do liftIO $ putStr $ showImp True (delab i lhs)

208− liftIO $ putStr " = "

209+ liftIO $ putStr " = "

209− liftIO $ putStrLn $ showImp True (delab i rhs)

210+ liftIO $ putStrLn $ showImp True (delab i rhs)

210process fn (TotCheck n) = do i <- get

211process fn (TotCheck n) = do i <- get

211 case lookupTotal n (tt_ctxt i) of

212 case lookupTotal n (tt_ctxt i) of

212 [t] -> iputStrLn (showTotal t i)

213 [t] -> iputStrLn (showTotal t i)

213 _ -> return ()

214 _ -> return ()

214process fn (DebugInfo n)

215process fn (DebugInfo n)

215− = do i <- get

216+ = do i <- get

216− let oi = lookupCtxtName Nothing n (idris_optimisation i)

217+ let oi = lookupCtxtName Nothing n (idris_optimisation i)

217− when (not (null oi)) $ iputStrLn (show oi)

218+ when (not (null oi)) $ iputStrLn (show oi)

218− let si = lookupCtxt Nothing n (idris_statics i)

219+ let si = lookupCtxt Nothing n (idris_statics i)

219− when (not (null si)) $ iputStrLn (show si)

220+ when (not (null si)) $ iputStrLn (show si)

220− let d = lookupDef Nothing n (tt_ctxt i)

221+ let d = lookupDef Nothing n (tt_ctxt i)

221− when (not (null d)) $ liftIO $

222+ when (not (null d)) $ liftIO $

222− do print (head d)

223+ do print (head d)

223− let cg = lookupCtxtName Nothing n (idris_callgraph i)

224+ let cg = lookupCtxtName Nothing n (idris_callgraph i)

224− findUnusedArgs (map fst cg)

225+ findUnusedArgs (map fst cg)

225− i <- get

226+ i <- get

226− let cg' = lookupCtxtName Nothing n (idris_callgraph i)

227+ let cg' = lookupCtxtName Nothing n (idris_callgraph i)

228+ sc <- checkSizeChange n

229+ iputStrLn $ "Size change: " ++ show sc

227− when (not (null cg')) $ do iputStrLn "Call graph:\n"

230+ when (not (null cg')) $ do iputStrLn "Call graph:\n"

228− iputStrLn (show cg')

231+ iputStrLn (show cg')

229process fn (Info n) = do i <- get

232process fn (Info n) = do i <- get

230 case lookupCtxt Nothing n (idris_classes i) of

233 case lookupCtxt Nothing n (idris_classes i) of

231 [c] -> classInfo c

234 [c] -> classInfo c

test/test010/expected+2

@@ -1 +1,3 @@

1test010.idr:13:foo is possibly not total due to: MkBad

2+test010a.idr:9:main.bar is possibly not total due to: main.MkBad

3+test010b.idr:9:main.bar is possibly not total due to: main.MkBad

test/test010/run+4

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

1#!/bin/bash

2idris test010.idr -o test010

3+idris test010a.idr -o test010

4+idris test010b.idr -o test010

6+rm -f *.ibc

test/test010/test010.idr+3−2

@@ -1,14 +1,15 @@

1data MyNat = MyO | MyS MyNat

3+%default total

3data Bad = MkBad (Bad -> Int) Int

5data Bad = MkBad (Bad -> Int) Int

4 | MkBad' Int

6 | MkBad' Int

6−total

7vapp : Vect a n -> Vect a m -> Vect a (n + m)

8vapp : Vect a n -> Vect a m -> Vect a (n + m)

8vapp [] ys = ys

9vapp [] ys = ys

9vapp (x :: xs) ys = x :: vapp xs ys

10vapp (x :: xs) ys = x :: vapp xs ys

11−total

12foo : Bad -> Int

13foo (MkBad f i) = f (MkBad' i)

14foo (MkBad' x) = x

15+

test/test010/test010a.idrnew file+9

@@ -0,0 +1,9 @@

1+module main

3+%default total

5+data Bad = MkBad (Bad -> Int) Int

6+ | MkBad' Int

8+bar : Bad

9+bar = MkBad (\x => 3) 3

test/test010/test010b.idrnew file+9

@@ -0,0 +1,9 @@

1+module main

3+%default total

5+data Bad = MkBad (Bad -> Int) Int

6+ | MkBad' Int

8+bar : Bad

9+bar = MkBad (\x => 3) 3