02b6087 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1743 from jfdm/fix/lift-fixme-todo-1

Lifting of TODO/FIXMES

commit02b60872bf9d06b770ae99979edb5a677504eb47 authorEdwin Brady <edwin.brady@gmail.com> dateMon 24 Nov 2014, 11:20 (12 years ago) parentce41442 cbb40b1

3 files changed+81−72

compare with master

unifiedsplit

src/IRTS/Compiler.hs+14−13 src/Idris/AbsSyntax.hs+53−45 src/Idris/Coverage.hs+14−14

src/IRTS/Compiler.hs+14−13

@@ -62,7 +62,7 @@ compile codegen f tm

6262 -- iputStrLn $ showSep "\n" (map show defs)

6363 -- Inlined top level LDecl made here

6464 let defsInlined = inlineAll defs

65− let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))

65+ let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))

6666 defsInlined

6767

6868 let (nexttag, tagged) = addTags 65536 (liftAll defsUniq)

@@ -91,13 +91,13 @@ compile codegen f tm

9191 iLOG "Building output"

9292

9393 case checked of

94− OK c -> do return $ CodegenInfo f outty triple cpu

94+ OK c -> do return $ CodegenInfo f outty triple cpu

9595 hdrs impdirs objs libs flags

9696 NONE c (toAlist defuns)

9797 tagged

9898-- runIO $ case codegen of

9999-- ViaC -> codegenC cginfo

100−-- ViaJava -> codegenJava cginfo

100+-- ViaJava -> codegenJava cginfo

101101-- ViaJavaScript -> codegenJavaScript cginfo

102102-- ViaNode -> codegenNode cginfo

103103-- ViaLLVM -> codegenLLVM cginfo

@@ -116,10 +116,10 @@ compile codegen f tm

116116 if ex then return f else return h

117117

118118generate :: Codegen -> FilePath -> CodegenInfo -> IO ()

119−generate codegen mainmod ir

119+generate codegen mainmod ir

120120 = case codegen of

121121 -- Built-in code generators (FIXME: lift these out!)

122− Via "c" -> codegenC ir

122+ Via "c" -> codegenC ir

123123 -- Any external code generator

124124 Via cg -> do let cmd = "idris-" ++ cg

125125 args = [mainmod, "-o", outputFile ir]

@@ -195,7 +195,7 @@ mkLDecl n (CaseOp ci _ _ _ pats cd)

195195 where

196196 (args, sc) = cases_runtime cd

197197

198− -- Always attempt to inline functions arising from 'case' expressions

198+ -- Always attempt to inline functions arising from 'case' expressions

199199 caseName (SN (CaseN _)) = True

200200 caseName (SN (WithN _ _)) = True

201201 caseName (NS n _) = caseName n

@@ -284,7 +284,7 @@ irTerm vs env tm@(App f a) = case unApply tm of

284284 x' <- irTerm vs env x

285285 t' <- irTerm vs env t

286286 e' <- irTerm vs env e

287− return (LCase Shared x'

287+ return (LCase Shared x'

288288 [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'

289289 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'

290290 ])

@@ -425,7 +425,7 @@ irTerm vs env (Bind _ _ _) = return $ LNothing

425425

426426irTerm vs env (Proj t (-1)) = do

427427 t' <- irTerm vs env t

428− return $ LOp (LMinus (ATInt ITBig))

428+ return $ LOp (LMinus (ATInt ITBig))

429429 [t', LConst (BI 1)]

430430

431431irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i

@@ -458,13 +458,13 @@ doForeign vs env (_ : fgn : args)

458458 | fi == txt "FIntT"

459459 = mkIntIty (str intTy)

460460

461− mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))

461+ mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))

462462 | ff == txt "FFunction"

463463 , fa == txt "FAny"

464− , io == txt "IO"

464+ , io == txt "IO"

465465 = FFunctionIO

466466

467− mkIty' (App (App (P _ (UN ff) _) _) _)

467+ mkIty' (App (App (P _ (UN ff) _) _) _)

468468 | ff == txt "FFunction"

469469 = FFunction

470470

@@ -472,7 +472,8 @@ doForeign vs env (_ : fgn : args)

472472

473473 -- would be better if these FInt types were evaluated at compile time

474474 -- TODO: add %eval directive for such things

475−

475+ -- Issue #1742 on the issue tracker.

476+ -- https://github.com/idris-lang/Idris-dev/issues/1742

476477 mkIty "FFloat" = FArith ATFloat

477478 mkIty "FInt" = mkIntIty "ITNative"

478479 mkIty "FChar" = mkIntIty "ITChar"

@@ -521,7 +522,7 @@ irSC vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])

521522 | delay == txt "Delay"

522523 = do sc' <- irSC vs $ mkForce n' n sc

523524 return $ LLet n' (LForce (LV (Glob n))) sc'

524−

525+

525526-- There are two transformations in this case:

526527--

527528-- 1. Newtype-case elimination:

src/Idris/AbsSyntax.hs+53−45

@@ -114,12 +114,12 @@ addLangExt ErrorReflection = do i <- getIState

114114-- Transforms are organised by the function being applied on the lhs of the

115115-- transform, to make looking up appropriate transforms quicker

116116addTrans :: Name -> (Term, Term) -> Idris ()

117−addTrans basefn t

117+addTrans basefn t

118118 = do i <- getIState

119119 let t' = case lookupCtxtExact basefn (idris_transforms i) of

120120 Just def -> (t : def)

121121 Nothing -> [t]

122− putIState $ i { idris_transforms = addDef basefn t'

122+ putIState $ i { idris_transforms = addDef basefn t'

123123 (idris_transforms i) }

124124

125125addErrRev :: (Term, Term) -> Idris ()

@@ -130,8 +130,8 @@ totcheck :: (FC, Name) -> Idris ()

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

131131

132132defer_totcheck :: (FC, Name) -> Idris ()

133−defer_totcheck n

134− = do i <- getIState;

133+defer_totcheck n

134+ = do i <- getIState;

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

136136

137137clear_totcheck :: Idris ()

@@ -183,7 +183,7 @@ addToCG n cg

183183 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }

184184

185185addTyInferred :: Name -> Idris ()

186−addTyInferred n

186+addTyInferred n

187187 = do i <- getIState

188188 putIState $ i { idris_tyinfodata =

189189 addDef n TIPartial (idris_tyinfodata i) }

@@ -197,7 +197,7 @@ addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts

197197 findMVApps x y

198198 = do let (fx, argsx) = unApply x

199199 let (fy, argsy) = unApply y

200− if (not (fx == fy))

200+ if (not (fx == fy))

201201 then do

202202 tryAddMV fx y

203203 tryAddMV fy x

@@ -211,17 +211,17 @@ addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts

211211 tryAddMV _ _ = return ()

212212

213213 addConstraintRule :: Name -> Term -> Idris ()

214− addConstraintRule n t

214+ addConstraintRule n t

215215 = do ist <- get

216216 logLvl 1 $ "TI constraint: " ++ show (n, t)

217217 case lookupCtxt n (idris_tyinfodata ist) of

218− [TISolution ts] ->

218+ [TISolution ts] ->

219219 do mapM_ (checkConsistent t) ts

220− let ti' = addDef n (TISolution (t : ts))

220+ let ti' = addDef n (TISolution (t : ts))

221221 (idris_tyinfodata ist)

222222 put $ ist { idris_tyinfodata = ti' }

223− _ ->

224− do let ti' = addDef n (TISolution [t])

223+ _ ->

224+ do let ti' = addDef n (TISolution [t])

225225 (idris_tyinfodata ist)

226226 put $ ist { idris_tyinfodata = ti' }

227227

@@ -233,14 +233,14 @@ addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts

233233 do let (fx, _) = unApply x

234234 let (fy, _) = unApply y

235235 case (fx, fy) of

236− (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)

236+ (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)

237237 (P (TCon _ _) n _, Constant _) -> errWhen True

238238 (Constant _, P (TCon _ _) n' _) -> errWhen True

239− (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)

239+ (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)

240240 _ -> return ()

241241

242− where errWhen True

243− = throwError (At fc

242+ where errWhen True

243+ = throwError (At fc

244244 (CantUnify False x y (Msg "") [] 0))

245245 errWhen False = return ()

246246

@@ -310,6 +310,8 @@ getNameHints i n =

310310 [ns] -> ns

311311 _ -> []

312312

313+-- Issue #1737 in the Issue Tracker.

314+-- https://github.com/idris-lang/Idris-dev/issues/1737

313315addToCalledG :: Name -> [Name] -> Idris ()

314316addToCalledG n ns = return () -- TODO

315317

@@ -333,7 +335,7 @@ addInstance int n i

333335 insI i (n : ns) | chaser n = i : n : ns

334336 | otherwise = n : insI i ns

335337

336− chaser (UN nm)

338+ chaser (UN nm)

337339 | ('@':'@':_) <- str nm = True

338340 chaser (NS n _) = chaser n

339341 chaser _ = False

@@ -421,6 +423,9 @@ withContext_ ctx name action = withContext ctx name () action

421423runIO :: IO a -> Idris a

422424runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return

423425-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"

426+--

427+-- Issue #1738 on the issue tracker.

428+-- https://github.com/idris-lang/Idris-dev/issues/1738

424429

425430getName :: Idris Int

426431getName = do i <- getIState;

@@ -454,9 +459,9 @@ clearOrigPats = do i <- get

454459-- the .ibc, which is all we need after all the analysis is done)

455460clearPTypes :: Idris ()

456461clearPTypes = do i <- get

457− let ctxt = tt_ctxt i

462+ let ctxt = tt_ctxt i

458463 put (i { tt_ctxt = mapDefCtxt pErase ctxt })

459− where pErase (CaseOp c t tys orig tot cds)

464+ where pErase (CaseOp c t tys orig tot cds)

460465 = CaseOp c t tys orig [] (pErase' cds)

461466 pErase x = x

462467 pErase' (CaseDefs _ (cs, c) _ rs)

@@ -503,7 +508,7 @@ addDeferred' nt ns

503508 i <- getIState

504509 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++

505510 idris_metavars i }

506− where

511+ where

507512 -- 'tidyNames' is to generate user accessible names in case they are

508513 -- needed in tactic scripts

509514 tidyNames used (Bind (MN i x) b sc)

@@ -1075,12 +1080,12 @@ addStatics :: Name -> Term -> PTerm -> Idris ()

10751080addStatics n tm ptm =

10761081 do let (statics, dynamics) = initStatics tm ptm

10771082 ist <- getIState

1078− let paramnames

1083+ let paramnames

10791084 = nub $ case lookupCtxtExact n (idris_fninfo ist) of

10801085 Just p -> getNamesFrom 0 (fn_params p) tm ++

10811086 concatMap (getParamNames ist) (map snd statics)

10821087 _ -> concatMap (getParamNames ist) (map snd statics)

1083−

1088+

10841089 let stnames = nub $ concatMap freeArgNames (map snd statics)

10851090 let dnames = (nub $ concatMap freeArgNames (map snd dynamics))

10861091 \\ paramnames

@@ -1106,7 +1111,7 @@ addStatics n tm ptm =

11061111 initStatics (Bind n (Pi ty _) sc) (PPi p n' _ s)

11071112 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in

11081113 if pstatic p == Static then ((n, ty) : static, dynamic)

1109− else if (not (searchArg p))

1114+ else if (not (searchArg p))

11101115 then (static, (n, ty) : dynamic)

11111116 else (static, dynamic)

11121117 initStatics t pt = ([], [])

@@ -1116,7 +1121,7 @@ addStatics n tm ptm =

11161121 Just ti -> getNamePos 0 (param_pos ti) args

11171122 Nothing -> []

11181123 where getNamePos i ps [] = []

1119− getNamePos i ps (P _ n _ : as)

1124+ getNamePos i ps (P _ n _ : as)

11201125 | i `elem` ps = n : getNamePos (i + 1) ps as

11211126 getNamePos i ps (_ : as) = getNamePos (i + 1) ps as

11221127 getParamNames ist (Bind t (Pi (P _ n _) _) sc)

@@ -1128,7 +1133,7 @@ addStatics n tm ptm =

11281133 | otherwise = getNamesFrom (i + 1) ps sc

11291134 getNamesFrom i ps sc = []

11301135

1131− freeArgNames (Bind n (Pi ty _) sc)

1136+ freeArgNames (Bind n (Pi ty _) sc)

11321137 = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here

11331138 freeArgNames tm = let (_, args) = unApply tm in

11341139 concatMap freeNames args

@@ -1199,11 +1204,11 @@ addUsingImpls syn n fc t

11991204 let ns = implicitNamesIn (map iname uimpls) ist t

12001205 let badnames = filter (\n -> not (implicitable n) &&

12011206 n `notElem` (map iname uimpls)) ns

1202− when (not (null badnames)) $

1203− throwError (At fc (Elaborating "type of " n

1207+ when (not (null badnames)) $

1208+ throwError (At fc (Elaborating "type of " n

12041209 (NoSuchVariable (head badnames))))

1205− let cs = getArgnames t -- get already bound names

1206− let addimpls = filter (\n -> iname n `notElem` cs) uimpls

1210+ let cs = getArgnames t -- get already bound names

1211+ let addimpls = filter (\n -> iname n `notElem` cs) uimpls

12071212 -- if all names in the arguments of addconsts appear in ns,

12081213 -- add the constraint implicitly

12091214 return (bindFree ns (doAdd addimpls ns t))

@@ -1223,9 +1228,9 @@ addUsingImpls syn n fc t

12231228

12241229 -- bind the free names which weren't in the using block

12251230 bindFree [] tm = tm

1226− bindFree (n:ns) tm

1231+ bindFree (n:ns) tm

12271232 | elem n (map iname uimpls) = bindFree ns tm

1228− | otherwise

1233+ | otherwise

12291234 = PPi (Imp [] Dynamic False) n Placeholder (bindFree ns tm)

12301235

12311236 getArgnames (PPi _ n c sc)

@@ -1244,15 +1249,15 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

12441249 getImps (Bind n (Pi t _) sc) imps

12451250 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

12461251 where

1247− argInfo n (Imp opt _ _) t'

1252+ argInfo n (Imp opt _ _) t'

12481253 = (True, PImp (getPriority i t') True opt n t')

12491254 argInfo n (Exp opt _ _) t'

12501255 = (InaccessibleArg `elem` opt,

12511256 PExp (getPriority i t') opt n t')

1252− argInfo n (Constraint opt _) t'

1257+ argInfo n (Constraint opt _) t'

12531258 = (InaccessibleArg `elem` opt,

12541259 PConstraint 10 opt n t')

1255− argInfo n (TacImp opt _ scr) t'

1260+ argInfo n (TacImp opt _ scr) t'

12561261 = (InaccessibleArg `elem` opt,

12571262 PTacImplicit 10 opt n scr t')

12581263 getImps (Bind n (Pi t _) sc) imps = impBind n t : getImps sc imps

@@ -1265,6 +1270,9 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

12651270-- This has become a right mess already. Better redo it some time...

12661271-- TODO: This is obsoleted by the new way of elaborating types, but there's still

12671272-- a couple of places which use it. Clean them up!

1273+--

1274+-- Issue 1739 in the issue tracker

1275+-- https://github.com/idris-lang/Idris-dev/issues/1739

12681276implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm

12691277implicit info syn n ptm = implicit' info syn [] n ptm

12701278

@@ -1283,11 +1291,11 @@ implicit' info syn ignore n ptm

12831291 where

12841292 -- Detect unknown names in default arguments and throw error if found.

12851293 defaultArgCheck :: [Name] -> [PArg] -> Idris ()

1286− defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params

1294+ defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params

12871295

12881296 notFoundInDefault :: [Name] -> PArg -> Idris [Name]

12891297 notFoundInDefault kns (PTacImplicit _ _ n script _)

1290− = do i <- getIState

1298+ = do i <- getIState

12911299 case notFound kns (namesIn [] i script) of

12921300 Nothing -> return (n:kns)

12931301 Just name -> throwError (NoSuchVariable name)

@@ -1545,7 +1553,7 @@ aiFn inpat expat qq ist fc f ds as

15451553 let nh = filter (\(n, _) -> notHidden n) ns

15461554 let ns' = case trimAlts ds nh of

15471555 [] -> nh

1548− x -> x

1556+ x -> x

15491557 case ns' of

15501558 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

15511559 [] -> if f `elem` (map fst (idris_metavars ist))

@@ -1557,7 +1565,7 @@ aiFn inpat expat qq ist fc f ds as

15571565 (insertImpl ns as)) alts

15581566 where

15591567 trimAlts [] alts = alts

1560− trimAlts ns alts

1568+ trimAlts ns alts

15611569 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts

15621570

15631571 nspace (NS _ s) = s

@@ -1612,6 +1620,8 @@ aiFn inpat expat qq ist fc f ds as

16121620 insImpAcc (M.insert n sc pnas) ps given imps

16131621 insImpAcc _ expected [] imps = imps -- so that unused implicits give error

16141622 -- TODO: report here, and prune alternatives

1623+ -- Issue #1740 in the Issue Tracker

1624+-- https://github.com/idris-lang/Idris-dev/issues/1740

16151625 insImpAcc _ _ given imps = given ++ imps

16161626

16171627 find n [] acc = Nothing

@@ -1644,7 +1654,7 @@ stripLinear i tm = evalState (sl tm) [] where

16441654 return (PPatvar fc f)

16451655 sl t@(PAlternative _ (a : as)) = do sl a

16461656 return t

1647− sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var

1657+ sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var

16481658 args' <- mapM slA args

16491659 return $ PApp fc fn args'

16501660 where slA (PImp p m l n t) = do t' <- sl t

@@ -1667,11 +1677,11 @@ stripUnmatchable :: IState -> PTerm -> PTerm

16671677stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

16681678 su :: PTerm -> PTerm

16691679 su (PRef fc f)

1670− | (Bind n (Pi t _) sc :_) <- lookupTy f (tt_ctxt i)

1680+ | (Bind n (Pi t _) sc :_) <- lookupTy f (tt_ctxt i)

16711681 = Placeholder

1672− su (PApp fc fn args)

1682+ su (PApp fc fn args)

16731683 = PApp fc fn (fmap (fmap su) args)

1674− su (PAlternative b alts)

1684+ su (PAlternative b alts)

16751685 = let alts' = filter (/= Placeholder) (map su alts) in

16761686 if null alts' then Placeholder

16771687 else PAlternative b alts'

@@ -1766,7 +1776,7 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

17661776 match (PApp _ x []) (PRef f n) = match x (PRef f n)

17671777 match (PRef _ n) tm@(PRef _ n')

17681778 | n == n' && not names &&

1769− (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))

1779+ (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))

17701780 || tm == Placeholder)

17711781 = return [(n, tm)]

17721782 -- if one namespace is missing, drop the other

@@ -1777,7 +1787,7 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

17771787 | not names && (not (isConName n (tt_ctxt i) ||

17781788 isFnName n (tt_ctxt i)) || tm == Placeholder)

17791789 = return [(n, tm)]

1780− match (PEq _ _ _ l r) (PEq _ _ _ l' r')

1790+ match (PEq _ _ _ l r) (PEq _ _ _ l' r')

17811791 = do ml <- match' l l'

17821792 mr <- match' r r'

17831793 return (ml ++ mr)

@@ -2002,5 +2012,3 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where

20022012 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)

20032013 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)

20042014 mkUniq t = return t

2005−

2006−

src/Idris/Coverage.hs+14−14

@@ -72,7 +72,7 @@ genClauses fc n xs given

7272 -- there may be more case splitting that the idris_implicits record

7373 -- suggests)

7474 let parg = case lookupCtxt n (idris_implicits i) of

75− (p : _) ->

75+ (p : _) ->

7676 p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)

7777 _ -> repeat (pexp Placeholder)

7878 let tryclauses = mkClauses parg all_args

@@ -122,7 +122,8 @@ genClauses fc n xs given

122122

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

124124-- possibilities up to that depth.

125−

125+-- This and below issues for this function are tracked as Issue #1741 on the issue tracker.

126+-- https://github.com/idris-lang/Idris-dev/issues/1741

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

127128genAll i args

128129 = case filter (/=Placeholder) $ fnub (concatMap otherPats (fnub args)) of

@@ -264,13 +265,13 @@ checkAllCovering fc done top n | not (n `elem` done)

264265 addIBC (IBCTotCheckErr fc msg)

265266 [Partial _] ->

266267 case lookupCtxt n (idris_callgraph i) of

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

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

268269 (map fst (calls cg))

269270 _ -> return ()

270271 x -> return () -- stop if total

271272checkAllCovering _ _ _ _ = return ()

272273

273−-- Check if, in a given group of type declarations mut_ns,

274+-- Check if, in a given group of type declarations mut_ns,

274275-- the constructor cn : ty is strictly positive,

275276-- and update the context accordingly

276277

@@ -290,7 +291,7 @@ checkPositive mut_ns (cn, ty')

290291

291292 cp (Bind n (Pi aty _) sc) = posArg aty && cp sc

292293 cp t | (P _ n' _, args) <- unApply t,

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

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

294295 cp _ = True

295296

296297 posArg (Bind _ (Pi nty _) sc)

@@ -439,7 +440,7 @@ checkDeclTotality (fc, n)

439440 i <- getIState

440441 let opts = case lookupCtxt n (idris_flags i) of

441442 [fs] -> fs

442− _ -> []

443+ _ -> []

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

444445 t <- checkTotality [] fc n

445446 case t of

@@ -507,11 +508,11 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

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

508509 at == txt "assert_total" = []

509510 -- under a call to "Delay LazyCodata", don't do any checking of the

510− -- immediate call, as long as the call is guarded.

511+ -- immediate call, as long as the call is guarded.

511512 -- Then check its arguments

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

513514 Guarded <- guarded,

514− del == txt "Delay"

515+ del == txt "Delay"

515516 = let (capp, args) = unApply arg in

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

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

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

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

533534 findCalls _ _ _ _ = []

534535

535− expandToArity n args

536+ expandToArity n args

536537 = case lookupTy n (tt_ctxt ist) of

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

538539 _ -> args

@@ -609,7 +610,7 @@ checkSizeChange n = do

609610 return (noPartial tot)

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

611612 return Unchecked

612− where getArity ist n

613+ where getArity ist n

613614 = case lookupTy n (tt_ctxt ist) of

614615 [ty] -> arity (normalise (tt_ctxt ist) [] ty)

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

@@ -674,14 +675,14 @@ checkMP ist i mp = if i > 0

674675 Total []

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

676677 | e `elem` map (fst . fst) path

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

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

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

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

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

681682 [] -> [(Nothing, 0)]

682683 x -> x

683684-- trace (show (argspos, nextargs, path)) $

684− pathres =

685+ pathres =

685686 do (a, pos) <- argspos

686687 case a of

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

@@ -704,7 +705,7 @@ checkMP ist i mp = if i > 0

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

705706 return (Partial Itself)

706707 else return Unchecked in

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

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

708709 collapse' Unchecked pathres

709710

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

@@ -734,4 +735,3 @@ collapse' def (Unchecked : xs) = collapse' def xs

734735collapse' def (d : xs) = collapse' d xs

735736-- collapse' Unchecked [] = Total []

736737collapse' def [] = def

737−