9affb75 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Totality checker improvements

Now does a better job of checking type class instances for totality, by inlining dictionaries where possible. Added %default total declarations to some libraries where possible

commit9affb75a82ce51f73d6c44445b2ac01287ddd0f6 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 28 Oct 2012, 23:22 (14 years ago) parentf8920a0

21 files changed+291−130

compare with master

unifiedsplit

CHANGELOG+1

@@ -12,6 +12,7 @@ User visible changes:

1212 for functions, and a corresponding "partial" reserved words to mark functions

1313 as allowed to be partial. Also "--total" and "--partial" added as command

1414 line options.

15+* New termination checker supporting mutually recursive definitions.

1516

1617Internal changes:

1718

lib/Builtins.idr+5−1

@@ -1,4 +1,5 @@

11%access public

2+%default total

34data Exists : (a : Set) -> (P : a -> Set) -> Set where

45 Ex_intro : {P : a -> Set} -> (x : a) -> P x -> Exists a P

@@ -234,7 +235,7 @@ instance Num Float where

234235 abs x = if x<0 then -x else x

235236 fromInteger = prim__intToFloat

236237

237−

238+partial

238239div : Int -> Int -> Int

239240div = prim__divInt

240241

@@ -247,15 +248,18 @@ div = prim__divInt

247248(++) : String -> String -> String

248249(++) = prim__concat

249250

251+partial

250252strHead : String -> Char

251253strHead = prim__strHead

252254

255+partial

253256strTail : String -> String

254257strTail = prim__strTail

255258

256259strCons : Char -> String -> String

257260strCons = prim__strCons

258261

262+partial

259263strIndex : String -> Int -> Char

260264strIndex = prim__strIndex

261265

lib/IO.idr+1−1

@@ -2,7 +2,7 @@ import Prelude.List

33%access public

5−abstract codata IO a = prim__IO a

5+abstract data IO a = prim__IO a

77abstract

88io_bind : IO a -> (a -> IO b) -> IO b

lib/Prelude.idr+22−1

@@ -16,6 +16,7 @@ import Prelude.Strings

1616import Prelude.Chars

1717

1818%access public

19+%default total

1920

2021-- Show and instances

2122

@@ -157,10 +158,12 @@ ceiling x = prim__floatCeil x

157158

158159---- Ranges

159160

161+partial

160162count : (Ord a, Num a) => a -> a -> a -> List a

161163count a inc b = if a <= b then a :: count (a + inc) inc b

162164 else []

163165

166+partial

164167countFrom : (Ord a, Num a) => a -> a -> List a

165168countFrom a inc = a :: lazy (countFrom (a + inc) inc)

166169

@@ -184,21 +187,27 @@ prod = foldl (*) 1

184187

185188---- some basic io

186189

190+partial

187191putStr : String -> IO ()

188192putStr x = mkForeign (FFun "putStr" [FString] FUnit) x

189193

194+partial

190195putStrLn : String -> IO ()

191196putStrLn x = putStr (x ++ "\n")

192197

198+partial

193199print : Show a => a -> IO ()

194200print x = putStrLn (show x)

195201

202+partial

196203getLine : IO String

197204getLine = return (prim__readString prim__stdin)

198205

206+partial

199207putChar : Char -> IO ()

200208putChar c = mkForeign (FFun "putchar" [FChar] FUnit) c

201209

210+partial

202211getChar : IO Char

203212getChar = mkForeign (FFun "getchar" [] FChar)

204213

@@ -216,6 +225,7 @@ fopen f m = do h <- do_fopen f m

216225

217226data Mode = Read | Write | ReadWrite

218227

228+partial

219229openFile : String -> Mode -> IO File

220230openFile f m = fopen f (modeStr m) where

221231 modeStr : Mode -> String

@@ -223,24 +233,31 @@ openFile f m = fopen f (modeStr m) where

223233 modeStr Write = "w"

224234 modeStr ReadWrite = "r+"

225235

236+partial

226237do_fclose : Ptr -> IO ()

227238do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h

228239

240+partial

229241closeFile : File -> IO ()

230242closeFile (FHandle h) = do_fclose h

231243

244+partial

232245do_fread : Ptr -> IO String

233246do_fread h = return (prim__readString h)

234247

248+partial

235249fread : File -> IO String

236250fread (FHandle h) = do_fread h

237251

252+partial

238253do_fwrite : Ptr -> String -> IO ()

239254do_fwrite h s = mkForeign (FFun "fputStr" [FPtr, FString] FUnit) h s

240255

256+partial

241257fwrite : File -> String -> IO ()

242258fwrite (FHandle h) s = do_fwrite h s

243259

260+partial

244261do_feof : Ptr -> IO Int

245262do_feof h = mkForeign (FFun "feof" [FPtr] FInt) h

246263

@@ -248,27 +265,31 @@ feof : File -> IO Bool

248265feof (FHandle h) = do eof <- do_feof h

249266 return (not (eof == 0))

250267

268+partial

251269nullPtr : Ptr -> IO Bool

252270nullPtr p = do ok <- mkForeign (FFun "isNull" [FPtr] FInt) p

253271 return (ok /= 0);

254272

273+partial

255274validFile : File -> IO Bool

256275validFile (FHandle h) = do x <- nullPtr h

257276 return (not x)

258277

278+partial -- obviously

259279while : |(test : IO Bool) -> |(body : IO ()) -> IO ()

260280while t b = do v <- t

261281 if v then do b

262282 while t b

263283 else return ()

264284

265−

285+partial -- no error checking!

266286readFile : String -> IO String

267287readFile fn = do h <- openFile fn Read

268288 c <- readFile' h ""

269289 closeFile h

270290 return c

271291 where

292+ partial

272293 readFile' : File -> String -> IO String

273294 readFile' h contents =

274295 do x <- feof h

lib/Prelude/List.idr+11−1

@@ -7,6 +7,7 @@ import Prelude.Maybe

77import Prelude.Nat

99%access public

10+%default total

1011

1112infixr 7 ::

1213

@@ -30,6 +31,7 @@ isCons (x::xs) = True

3031-- Indexing into lists

3132--------------------------------------------------------------------------------

3233

34+%assert_total

3335head : (l : List a) -> (isCons l = True) -> a

3436head (x::xs) p = x

3537

@@ -37,6 +39,7 @@ head' : (l : List a) -> Maybe a

3739head' [] = Nothing

3840head' (x::xs) = Just x

3941

42+%assert_total

4043tail : (l : List a) -> (isCons l = True) -> List a

4144tail (x::xs) p = xs

4245

@@ -44,6 +47,7 @@ tail' : (l : List a) -> Maybe (List a)

4447tail' [] = Nothing

4548tail' (x::xs) = Just xs

4649

50+%assert_total

4751last : (l : List a) -> (isCons l = True) -> a

4852last (x::xs) p =

4953 case xs of

@@ -57,6 +61,7 @@ last' (x::xs) =

5761 [] => Just x

5862 y::ys => last' xs

5963

64+%assert_total

6065init : (l : List a) -> (isCons l = True) -> List a

6166init (x::xs) p =

6267 case xs of

@@ -116,9 +121,11 @@ length (x::xs) = 1 + length xs

116121(++) [] right = right

117122(++) (x::xs) right = x :: (xs ++ right)

118123

124+partial

119125repeat : a -> List a

120126repeat x = x :: repeat x

121127

128+%assert_total

122129replicate : Nat -> a -> List a

123130replicate n x = take n (repeat x)

124131

@@ -160,11 +167,13 @@ instance Monoid (List a) where

160167-- Zips and unzips

161168--------------------------------------------------------------------------------

162169

170+%assert_total

163171zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->

164172 (length l = length r) -> List c

165173zipWith f [] [] p = []

166174zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)

167175

176+%assert_total

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

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

170179zipWith3 f [] [] [] refl refl = []

@@ -450,12 +459,13 @@ mergeBy order (x::xs) (y::ys) =

450459merge : Ord a => List a -> List a -> List a

451460merge = mergeBy compare

452461

462+%assert_total

453463sort : Ord a => List a -> List a

454464sort [] = []

455465sort [x] = [x]

456466sort xs =

457467 let (x, y) = split xs in

458− merge (sort x) (sort y)

468+ merge (sort x) (sort y) -- not structurally smaller, hence assert

459469 where

460470 splitRec : List a -> List a -> (List a -> List a) -> (List a, List a)

461471 splitRec (_::_::xs) (y::ys) zs = splitRec xs ys (zs . ((::) y))

lib/Prelude/Nat.idr+1

@@ -6,6 +6,7 @@ import Prelude.Algebra

66import Prelude.Cast

88%access public

9+%default total

910

1011data Nat

1112 = O

lib/Prelude/Vect.idr+4−4

@@ -5,6 +5,7 @@ import Prelude.List

55import Prelude.Nat

77%access public

8+%default total

910infixr 7 ::

1011

@@ -54,11 +55,11 @@ drop (fS k) (x::xs) = drop k xs

5455-- Conversions to and from list

5556--------------------------------------------------------------------------------

5657

57−total toList : Vect a n -> List a

58+toList : Vect a n -> List a

5859toList [] = []

5960toList (x::xs) = x :: toList xs

6061

61−total fromList : (l : List a) -> Vect a (length l)

62+fromList : (l : List a) -> Vect a (length l)

6263fromList [] = []

6364fromList (x::xs) = x :: fromList xs

6465

@@ -66,7 +67,6 @@ fromList (x::xs) = x :: fromList xs

6667-- Building (bigger) vectors

6768--------------------------------------------------------------------------------

6869

69−total

7070(++) : Vect a m -> Vect a n -> Vect a (m + n)

7171(++) [] ys = ys

7272(++) (x::xs) ys = x :: xs ++ ys

@@ -79,7 +79,7 @@ replicate (S k) x = x :: replicate k x

7979-- Maps

8080--------------------------------------------------------------------------------

8181

82−total map : (a -> b) -> Vect a n -> Vect b n

82+map : (a -> b) -> Vect a n -> Vect b n

8383map f [] = []

8484map f (x::xs) = f x :: map f xs

8585

src/Core/CaseTree.hs+1−1

@@ -69,7 +69,7 @@ instance TermSize CaseAlt where

6969

7070-- simple terms can be inlined trivially - good for primitives in particular

7171small :: SC -> Bool

72−small t = termsize t < 150

72+small t = False -- termsize t < 150

7373

7474namesUsed :: SC -> [Name]

7575namesUsed sc = nub $ nu' [] sc where

src/Core/Evaluate.hs+59−26

@@ -5,10 +5,10 @@ module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

55 simplify, specialise, hnf, convEq, convEq',

66 Def(..), Accessibility(..), Totality(..), PReason(..),

77 Context, initContext, ctxtAlist, uconstraints, next_tvar,

8− addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl, addDatatype,

9− addCasedef, addOperator,

10− lookupNames, lookupTy, lookupP, lookupDef, lookupVal, lookupTotal,

11− lookupTyEnv, isConName, isFnName,

8+ addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl,

9+ addDatatype, addCasedef, simplifyCasedef, addOperator,

10+ lookupNames, lookupTy, lookupP, lookupDef, lookupVal,

11+ lookupTotal, lookupTyEnv, isConName, isFnName,

1212 Value(..)) where

1313

1414import Debug.Trace

@@ -167,7 +167,7 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

167167 ev ntimes (n:stk) True env tm

168168 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty

169169 return $ VP nt n vty

170− [(CaseOp inl _ _ [] tree _ _, Public)] -> -- unoptimised version

170+ [(CaseOp inl _ _ _ [] tree _ _, Public)] -> -- unoptimised version

171171 if simpl && (not inl || elem n stk)

172172 then liftM (VP Ref n) (ev ntimes stk top env ty)

173173 else do c <- evCase ntimes (n:stk) top env [] [] tree

@@ -231,7 +231,7 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

231231 = traceWhen traceon (show stk) $

232232 do let val = lookupDefAcc Nothing n atRepl ctxt

233233 case val of

234− [(CaseOp inl _ _ ns tree _ _, Public)] ->

234+ [(CaseOp inl _ _ _ ns tree _ _, Public)] ->

235235 if simpl && (not inl || elem n stk)

236236 then return $ unload env (VP Ref n ty) args

237237 else do c <- evCase ntimes (n:stk) top env ns args tree

@@ -391,7 +391,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

391391 ev env (P Ref n ty) = case lookupDef Nothing n ctxt of

392392 [Function _ t] -> ev env t

393393 [TyDecl nt ty] -> return $ HP nt n ty

394− [CaseOp inl _ _ [] tree _ _] ->

394+ [CaseOp inl _ _ _ [] tree _ _] ->

395395 do c <- evCase env [] [] tree

396396 case c of

397397 (Nothing, _, _) -> return $ HP Ref n ty

@@ -421,7 +421,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

421421 app <- apply env sc' as

422422 wknH (-1) app

423423 apply env (HP Ref n ty) args

424− | [CaseOp _ _ _ ns tree _ _] <- lookupDef Nothing n ctxt

424+ | [CaseOp _ _ _ _ ns tree _ _] <- lookupDef Nothing n ctxt

425425 = do c <- evCase env ns args tree

426426 case c of

427427 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args

@@ -548,8 +548,8 @@ convEq ctxt = ceq [] where

548548 sameDefs ps x y = case (lookupDef Nothing x ctxt, lookupDef Nothing y ctxt) of

549549 ([Function _ xdef], [Function _ ydef])

550550 -> ceq ((x,y):ps) xdef ydef

551− ([CaseOp _ _ _ _ xdef _ _],

552− [CaseOp _ _ _ _ ydef _ _])

551+ ([CaseOp _ _ _ _ _ xdef _ _],

552+ [CaseOp _ _ _ _ _ ydef _ _])

553553 -> caseeq ((x,y):ps) xdef ydef

554554 _ -> return False

555555

@@ -571,7 +571,9 @@ spec ctxt statics genv tm = error "spec undefined"

571571data Def = Function Type Term

572572 | TyDecl NameType Type

573573 | Operator Type Int ([Value] -> Maybe Value)

574− | CaseOp Bool Type [([Name], Term, Term)] -- Bool for inlineable

574+ | CaseOp Bool Type -- bool for inlinable

575+ [Either Term (Term, Term)] -- original definition

576+ [([Name], Term, Term)] -- simplified definition

575577 [Name] SC -- Compile time case definition

576578 [Name] SC -- Run time cae definitions

577579{-!

@@ -582,7 +584,7 @@ instance Show Def where

582584 show (Function ty tm) = "Function: " ++ show (ty, tm)

583585 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty

584586 show (Operator ty _ _) = "Operator: " ++ show ty

585− show (CaseOp _ ty ps ns sc ns' sc')

587+ show (CaseOp _ ty ps_in ps ns sc ns' sc')

586588 = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++

587589 show ns ++ " " ++ show sc ++ "\n" ++

588590 show ns' ++ " " ++ show sc'

@@ -620,7 +622,7 @@ instance Show Totality where

620622 show (Partial NotPositive) = "not strictly positive"

621623 show (Partial NotProductive) = "not productive"

622624 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)

623− show (Partial (Mutual ns)) = "possibly not total due to mutual recursive path " ++

625+ show (Partial (Mutual ns)) = "possibly not total due to recursive path " ++

624626 showSep " --> " (map show ns)

625627

626628{-!

@@ -635,9 +637,11 @@ deriving instance Binary Totality

635637deriving instance Binary PReason

636638!-}

637639

638−data Context = MkContext { uconstraints :: [UConstraint],

639− next_tvar :: Int,

640− definitions :: Ctxt (Def, Accessibility, Totality) }

640+data Context = MkContext {

641+ uconstraints :: [UConstraint],

642+ next_tvar :: Int,

643+ definitions :: Ctxt (Def, Accessibility, Totality)

644+ }

641645

642646initContext = MkContext [] 0 emptyContext

643647

@@ -690,9 +694,11 @@ addDatatype (Data n tag ty cons) uctxt

690694 (TyDecl (DCon tag (arity ty')) ty, Public, Unchecked) ctxt)

691695

692696addCasedef :: Name -> Bool -> Bool -> Bool ->

693− [([Name], Term, Term)] -> [([Name], Term, Term)] ->

697+ [Either Term (Term, Term)] ->

698+ [([Name], Term, Term)] ->

699+ [([Name], Term, Term)] ->

694700 Type -> Context -> Context

695−addCasedef n alwaysInline tcase covering ps psrt ty uctxt

701+addCasedef n alwaysInline tcase covering ps_in ps psrt ty uctxt

696702 = let ctxt = definitions uctxt

697703 access = case lookupDefAcc Nothing n False uctxt of

698704 [(_, acc)] -> acc

@@ -700,12 +706,39 @@ addCasedef n alwaysInline tcase covering ps psrt ty uctxt

700706 ctxt' = case (simpleCase tcase covering CompileTime (FC "" 0) ps,

701707 simpleCase tcase covering RunTime (FC "" 0) psrt) of

702708 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->

703− let inl = alwaysInline || small sc' in

704− addDef n (CaseOp inl ty ps args sc args' sc',

705− access, Unchecked) ctxt in

709+ let inl = alwaysInline || small sc' in

710+ addDef n (CaseOp inl ty ps_in ps args sc args' sc',

711+ access, Unchecked) ctxt in

706712 uctxt { definitions = ctxt' }

707−

708−addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context

713+

714+simplifyCasedef :: Name -> Context -> Context

715+simplifyCasedef n uctxt

716+ = let ctxt = definitions uctxt

717+ ctxt' = case lookupCtxt Nothing n ctxt of

718+ [(CaseOp inl ty ps_in ps args sc args' sc', acc, tot)] ->

719+ let pdef = map debind $ map simpl ps_in in

720+ case simpleCase False True CompileTime (FC "" 0) pdef of

721+ OK (CaseDef args sc _) ->

722+-- trace ("Simplify " ++ show n ++ "\n" ++

723+-- show sc) $

724+ addDef n (CaseOp inl ty ps_in ps args sc args' sc',

725+ acc, tot) ctxt

726+ _ -> ctxt in

727+ uctxt { definitions = ctxt' }

728+ where

729+ depat acc (Bind n (PVar t) sc)

730+ = depat (n : acc) (instantiate (P Bound n t) sc)

731+ depat acc x = (acc, x)

732+ debind (Right (x, y)) = let (vs, x') = depat [] x

733+ (_, y') = depat [] y in

734+ (vs, x', y')

735+ debind (Left x) = let (vs, x') = depat [] x in

736+ (vs, x', Impossible)

737+ simpl (Right (x, y)) = Right (x, simplify uctxt [] y)

738+ simpl t = t

739+

740+addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->

741+ Context -> Context

709742addOperator n ty a op uctxt

710743 = let ctxt = definitions uctxt

711744 ctxt' = addDef n (Operator ty a op, Public, Unchecked) ctxt in

@@ -725,7 +758,7 @@ lookupTy root n ctxt

725758 (Function ty _) -> return ty

726759 (TyDecl _ ty) -> return ty

727760 (Operator ty _ _) -> return ty

728− (CaseOp _ ty _ _ _ _ _) -> return ty

761+ (CaseOp _ ty _ _ _ _ _ _) -> return ty

729762

730763isConName :: Maybe [String] -> Name -> Context -> Bool

731764isConName root n ctxt

@@ -741,7 +774,7 @@ isFnName root n ctxt

741774 case tfst def of

742775 (Function _ _) -> return True

743776 (Operator _ _ _) -> return True

744− (CaseOp _ _ _ _ _ _ _) -> return True

777+ (CaseOp _ _ _ _ _ _ _ _) -> return True

745778 _ -> return False

746779

747780lookupP :: Maybe [String] -> Name -> Context -> [Term]

@@ -750,7 +783,7 @@ lookupP root n ctxt

750783 p <- case def of

751784 (Function ty tm, a, _) -> return (P Ref n ty, a)

752785 (TyDecl nt ty, a, _) -> return (P nt n ty, a)

753− (CaseOp _ ty _ _ _ _ _, a, _) -> return (P Ref n ty, a)

786+ (CaseOp _ ty _ _ _ _ _ _, a, _) -> return (P Ref n ty, a)

754787 (Operator ty _ _, a, _) -> return (P Ref n ty, a)

755788 case snd p of

756789 Hidden -> []

src/Core/TT.hs+4

@@ -195,6 +195,10 @@ instance Show Name where

195195type Ctxt a = Map.Map Name (Map.Map Name a)

196196emptyContext = Map.empty

197197

198+tcname (UN ('@':_)) = True

199+tcname (NS n _) = tcname n

200+tcname _ = False

201+

198202nsroot (NS n _) = n

199203nsroot n = n

200204

src/IRTS/Compiler.hs+2−2

@@ -129,8 +129,8 @@ declArgs args n x = LFun n args x

129129

130130mkLDecl n (Function tm _) = do e <- ir tm

131131 return (declArgs [] n e)

132−mkLDecl n (CaseOp _ _ pats _ _ args sc) = do e <- ir (args, sc)

133− return (declArgs [] n e)

132+mkLDecl n (CaseOp _ _ _ pats _ _ args sc) = do e <- ir (args, sc)

133+ return (declArgs [] n e)

134134mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a

135135mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a

136136mkLDecl n _ = return (LFun n [] (LError ("Impossible declaration " ++ show n)))

src/Idris/AbsSyntax.hs+5−5

@@ -43,7 +43,7 @@ addHdr :: String -> Idris ()

4343addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })

4444

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

46−totcheck n = do i <- get; put (i { idris_totcheck = n : idris_totcheck i })

46+totcheck n = do i <- get; put (i { idris_totcheck = idris_totcheck i ++ [n] })

4747

4848setFlags :: Name -> [FnOpt] -> Idris ()

4949setFlags n fs = do i <- get; put (i { idris_flags = addDef n fs (idris_flags i) })

@@ -325,6 +325,10 @@ logLvl l str = do i <- get

325325 $ do liftIO (putStrLn str)

326326 put (i { idris_log = idris_log i ++ str ++ "\n" } )

327327

328+cmdOptSet :: Opt -> Idris Bool

329+cmdOptSet x = do i <- get

330+ return $ x `elem` opt_cmdline (idris_options i)

331+

328332iLOG :: String -> Idris ()

329333iLOG = logLvl 1

330334

@@ -413,10 +417,6 @@ piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm

413417piBindp p [] t = t

414418piBindp p ((n, ty):ns) t = PPi p n ty (piBind ns t)

415419

416−tcname (UN ('@':_)) = True

417−tcname (NS n _) = tcname n

418−tcname _ = False

419−

420420-- Dealing with parameters

421421

422422expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm

src/Idris/AbsSyntaxTree.hs+1

@@ -184,6 +184,7 @@ data Opt = Filename String

184184 | TypeInType

185185 | DefaultTotal

186186 | DefaultPartial

187+ | WarnPartial

187188 | NoCoverage

188189 | ErrContext

189190 | ShowImpl

src/Idris/Coverage.hs+66−23

@@ -252,6 +252,7 @@ checkPositive n (cn, ty)

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

253253 let ctxt' = setTotal cn tot (tt_ctxt i)

254254 putIState (i { tt_ctxt = ctxt' })

255+ logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot

255256 addIBC (IBCTotal cn tot)

256257 where

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

@@ -328,6 +329,7 @@ checkTotality path fc n

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

329330 | otherwise = do

330331 t <- getTotality n

332+ updateContext (simplifyCasedef n)

331333 ctxt <- getContext

332334 i <- getIState

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

@@ -336,7 +338,7 @@ checkTotality path fc n

336338 t' <- case t of

337339 Unchecked ->

338340 case lookupDef Nothing n ctxt of

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

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

340342 do t' <- if AssertTotal `elem` opts

341343 then return $ Total []

342344 else calcTotality path fc n pats

@@ -349,24 +351,37 @@ checkTotality path fc n

349351-- p@(Partial _) ->

350352-- do setAccessibility n Frozen

351353-- addIBC (IBCAccess n Frozen)

352−-- iputStrLn $ "HIDDEN: "

354+-- logLvl 5 $ "HIDDEN: "

353355-- ++ show n ++ show p

354− _ -> return ()

356+ _ -> return ()

355357 return t'

356358 _ -> return $ Total []

357359 x -> return x

358− if TotalFn `elem` opts

359− then case t' of

360− Total _ -> return t'

361− Productive -> return t'

362− e -> totalityError t'

363− else return t'

360+ case t' of

361+ Total _ -> return t'

362+ Productive -> return t'

363+ e -> do w <- cmdOptSet WarnPartial

364+ if TotalFn `elem` opts

365+ then totalityError t'

366+ else do when w $ warnPartial n t'

367+ return t'

364368 where

365369 totalityError t = tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))

366370

371+ warnPartial n t

372+ = do i <- get

373+ case lookupDef Nothing n (tt_ctxt i) of

374+ [x] -> do

375+ iputStrLn $ show fc ++ ":Warning - " ++ show n ++ " is " ++ show t

376+-- ++ "\n" ++ show x

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

378+-- iputStrLn (show cg)

379+

380+

367381checkDeclTotality :: (FC, Name) -> Idris Totality

368382checkDeclTotality (fc, n)

369383 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"

384+ buildSCG (fc, n)

370385 checkTotality [] fc n

371386

372387-- Calculate the size change graph for this definition

@@ -380,10 +395,20 @@ checkDeclTotality (fc, n)

380395-- to f

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

382397

383−-- FIXME: Higher order recursive arguments

384−

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

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

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

399+buildSCG (_, n) = do

400+ ist <- get

401+ case lookupCtxt Nothing n (idris_callgraph ist) of

402+ [cg] -> case lookupDef Nothing n (tt_ctxt ist) of

403+ [CaseOp _ _ _ _ args sc _ _] ->

404+ do logLvl 5 $ "Building SCG for " ++ show n ++ " from\n"

405+ ++ show sc

406+ let newscg = buildSCG' ist sc args

407+ logLvl 5 $ show newscg

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

409+

410+buildSCG' :: IState -> SC -> [Name] -> [SCGEntry]

411+buildSCG' ist sc args = nub $ scg sc (zip args args)

387412 (zip args (zip args (repeat Same)))

388413 where

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

@@ -427,6 +452,8 @@ buildSCG ist sc args = scg sc (zip args args)

427452 scgAlt x vars szs (DefaultCase sc) = scg sc vars szs

428453

429454 scgTerm f@(App _ _) vars szs

455+ | (P _ (UN "lazy") _, [_, arg]) <- unApply f

456+ = scgTerm arg vars szs

430457 | (P _ fn _, args) <- unApply f

431458 = let rest = concatMap (\x -> scgTerm x vars szs) args in

432459 case lookup fn vars of

@@ -447,6 +474,7 @@ buildSCG ist sc args = scg sc (zip args args)

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

448475 -> Maybe (Int, SizeChange)

449476 mkChange szs tm

477+ | (P _ (UN "lazy") _, [_, arg]) <- unApply tm = mkChange szs arg

450478 | (P _ n ty, _) <- unApply tm -- get higher order args too

451479 = do sc <- lookup n szs

452480 case sc of

@@ -466,7 +494,9 @@ checkSizeChange n = do

466494 case lookupCtxt Nothing n (idris_callgraph ist) of

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

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

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

469498 showSep "\n" (map show ms))

499+ logLvl 6 (show cg)

470500 -- every multipath must have an infinitely descending

471501 -- thread, then the function terminates

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

@@ -478,13 +508,22 @@ checkSizeChange n = do

478508type MultiPath = [SCGEntry]

479509

480510mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]

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

481512mkMultiPaths ist path cg

482− = do (nextf, args) <- cg

483− if ((nextf, args) `elem` path)

484− then return (reverse ((nextf, args) : path))

485− else case lookupCtxt Nothing nextf (idris_callgraph ist) of

513+ = concat (map extend cg)

514+ where extend (nextf, args)

515+ | (nextf, args) `elem` path = [ (nextf, args) : path ]

516+ | otherwise

517+ = case lookupCtxt Nothing nextf (idris_callgraph ist) of

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

487− _ -> return (reverse ((nextf, args) : path))

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

520+

521+-- do (nextf, args) <- cg

522+-- if ((nextf, args) `elem` path)

523+-- then return (reverse ((nextf, args) : path))

524+-- else case lookupCtxt Nothing nextf (idris_callgraph ist) of

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

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

488527

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

490529-- Try a route beginning with every argument.

@@ -507,14 +546,17 @@ checkMP ist i mp = if i > 0

507546 x -> error (show x)

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

509548 = Total []

549+-- tryPath desc path (e@(f, []) : es) arg

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

551+-- tryPath (-10000) ((e, desc) : path) es 0

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

511553 | Just d <- lookup e path

512554 = if (desc - d) > 0

513555 then Total []

514− else Partial Itself

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

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

516558 let argspos = zip nextargs [0..] in

517− collapse $

559+ collapse' (Partial (Other (map (fst . fst) path ++ [f]))) $

518560 do (arg, pos) <- argspos

519561 case arg of

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

@@ -540,7 +582,8 @@ noPartial (Partial p : xs) = Partial p

540582noPartial (_ : xs) = noPartial xs

541583noPartial [] = Total []

542584

543−collapse (Total r : xs) = Total r

544−collapse (_ : xs) = collapse xs

545−collapse [] = Partial Itself

585+collapse xs = collapse' (Partial Itself) xs

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

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

588+collapse' def [] = def

546589

src/Idris/ElabDecls.hs+82−57

@@ -133,8 +133,8 @@ elabRecord info syn fc tyn ty cn cty

133133

134134 tryElabDecl info (fn, ty, val)

135135 = do i <- get

136− idrisCatch (do elabDecl' info ty

137− elabDecl' info val)

136+ idrisCatch (do elabDecl' EAll info ty

137+ elabDecl' EAll info val)

138138 (\v -> do iputStrLn $ show fc ++

139139 ":Warning - can't generate setter for " ++

140140 show fn ++ " (" ++ show ty ++ ")"

@@ -295,7 +295,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

295295 logLvl 5 $ "Optimised patterns:\n" ++ show optpats

296296

297297 let optpdef = map debind $ map (simpl (tt_ctxt ist)) optpats

298− tree@(CaseDef scargs sc _) <- tclift $ simpleCase tcase False CompileTime fc pdef

298+ tree@(CaseDef scargs sc _) <- tclift $

299+ simpleCase tcase False CompileTime fc pdef

299300 cov <- coverage

300301 pmissing <-

301302 if cov

@@ -325,9 +326,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

325326 case tree of

326327 CaseDef _ _ [] -> return ()

327328 CaseDef _ _ xs -> mapM_ (\x ->

328− iputStrLn $ show fc ++

329− ":warning - Unreachable case: " ++

330− show (delab ist x)) xs

329+ iputStrLn $ show fc ++

330+ ":warning - Unreachable case: " ++

331+ show (delab ist x)) xs

331332 tree' <- tclift $ simpleCase tcase pcover RunTime fc pdef'

332333 logLvl 3 (show tree)

333334 logLvl 3 $ "Optimised: " ++ show tree'

@@ -336,18 +337,20 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

336337 put (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) })

337338 case lookupTy (namespace info) n ctxt of

338339 [ty] -> do updateContext (addCasedef n (inlinable opts)

339− tcase pcover pdef pdef' ty)

340+ tcase pcover pats

341+ pdef pdef' ty)

340342 addIBC (IBCDef n)

341343 setTotality n tot

342344 totcheck (fc, n)

343345 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

344346 i <- get

345347 case lookupDef Nothing n (tt_ctxt i) of

346− (CaseOp _ _ _ scargs sc scargs' sc' : _) ->

348+ (CaseOp _ _ _ _ scargs sc scargs' sc' : _) ->

347349 do let calls = findCalls sc' scargs'

348350 let used = findUsedArgs sc' scargs'

349− let scg = buildSCG i sc scargs

350− let cg = CGInfo scargs' calls scg used []

351+ -- let scg = buildSCG i sc scargs

352+ -- add SCG later, when checking totality

353+ let cg = CGInfo scargs' calls [] used []

351354 logLvl 2 $ "Called names: " ++ show cg

352355 addToCG n cg

353356 addToCalledG n (nub (map fst calls)) -- plus names in type!

@@ -441,7 +444,7 @@ elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)

441444 let newargs = pvars ist lhs_tm

442445 let wb = map (expandParamsD ist decorate newargs decls) whereblock

443446 logLvl 5 $ "Where block: " ++ show wb

444− mapM_ (elabDecl' info) wb

447+ mapM_ (elabDecl' EAll info) wb

445448 -- Now build the RHS, using the type of the LHS as the goal.

446449 i <- get -- new implicits from where block

447450 logLvl 5 (showImp True (expandParams decorate newargs decls rhs_in))

@@ -475,7 +478,7 @@ elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)

475478 checkInferred fc (delab' i crhs True) rhs

476479 return $ Right (clhs, crhs)

477480 where

478− decorate x = UN (show fname ++ "#" ++ show x)

481+ decorate x = UN (show x ++ "#" ++ show fname)

479482 pinfo ns ps i

480483 = let ds = concatMap declared ps

481484 newps = params info ++ ns

@@ -765,16 +768,20 @@ elabInstance info syn fc cs n ps t expn ds

765768 _ -> []

766769 let mtys = map (\ (n, (op, t)) ->

767770 let t' = substMatches ips t in

768− (decorate ns n, op, coninsert cs t', t'))

771+ (decorate ns iname n,

772+ op, coninsert cs t', t'))

769773 (class_methods ci)

770774 logLvl 3 (show (mtys, ips))

771− let ds' = insertDefaults i (class_defaults ci) ns ds

775+ let ds' = insertDefaults i iname (class_defaults ci) ns ds

772776 iLOG ("Defaults inserted: " ++ show ds' ++ "\n" ++ show ci)

773− mapM_ (warnMissing ds' ns) (map fst (class_methods ci))

777+ mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))

774778 mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')

775− let wb = map mkTyDecl mtys ++ map (decorateid (decorate ns)) ds'

779+ let wbTys = map mkTyDecl mtys

780+ let wbVals = map (decorateid (decorate ns iname)) ds'

781+ let wb = wbTys ++ wbVals

776782 logLvl 3 $ "Method types " ++ showSep "\n" (map (showDeclImp True . mkTyDecl) mtys)

777− -- get the implicit parameters that need passing through to the where block

783+ -- get the implicit parameters that need passing through to the

784+ -- where block

778785 wparams <- mapM (\p -> case p of

779786 PApp _ _ args -> getWParams args

780787 _ -> return []) ps

@@ -785,10 +792,10 @@ elabInstance info syn fc cs n ps t expn ds

785792 as -> PApp fc (PRef fc iname) as

786793 let rhs = PApp fc (PRef fc (instanceName ci))

787794 (map (pexp . mkMethApp) mtys)

788− let idecl = PClauses fc [Inlinable, TCGen] iname

789− [PClause fc iname lhs [] rhs wb]

790− iLOG (show idecl)

791− elabDecl info idecl

795+ let idecls = [PClauses fc [Inlinable, TCGen] iname

796+ [PClause fc iname lhs [] rhs wb]]

797+ iLOG (show idecls)

798+ mapM (elabDecl info) idecls

792799 addIBC (IBCInstance intInst n iname)

793800 where

794801 intInst = case ps of

@@ -838,8 +845,8 @@ elabInstance info syn fc cs n ps t expn ds

838845 _ -> return ps'

839846 getWParams (_ : ps) = getWParams ps

840847

841− decorate ns (UN n) = NS (UN ('!':n)) ns

842− decorate ns (NS (UN n) s) = NS (UN ('!':n)) ns

848+ decorate ns iname (UN n) = NS (UN ('!':n)) ns

849+ decorate ns iname (NS (UN n) s) = NS (UN ('!':n)) ns

843850

844851 mkTyDecl (n, op, t, _) = PTy syn fc op n t

845852

@@ -849,20 +856,22 @@ elabInstance info syn fc cs n ps t expn ds

849856 coninsert cs (PPi p@(Imp _ _) n t sc) = PPi p n t (coninsert cs sc)

850857 coninsert cs sc = conbind cs sc

851858

852− insertDefaults :: IState -> [(Name, (Name, PDecl))] -> [String] -> [PDecl] -> [PDecl]

853− insertDefaults i [] ns ds = ds

854− insertDefaults i ((n,(dn, clauses)) : defs) ns ds

855− = insertDefaults i defs ns (insertDef i n dn clauses ns ds)

859+ insertDefaults :: IState -> Name ->

860+ [(Name, (Name, PDecl))] -> [String] ->

861+ [PDecl] -> [PDecl]

862+ insertDefaults i iname [] ns ds = ds

863+ insertDefaults i iname ((n,(dn, clauses)) : defs) ns ds

864+ = insertDefaults i iname defs ns (insertDef i n dn clauses ns iname ds)

856865

857− insertDef i meth def clauses ns decls

858− | null $ filter (clauseFor meth ns) decls

866+ insertDef i meth def clauses ns iname decls

867+ | null $ filter (clauseFor meth iname ns) decls

859868 = let newd = expandParamsD i (\n -> meth) [] [def] clauses in

860869 -- trace (show newd) $

861870 decls ++ [newd]

862871 | otherwise = decls

863872

864− warnMissing decls ns meth

865− | null $ filter (clauseFor meth ns) decls

873+ warnMissing decls ns iname meth

874+ | null $ filter (clauseFor meth iname ns) decls

866875 = iWarn fc $ "method " ++ show meth ++ " not defined"

867876 | otherwise = return ()

868877

@@ -873,8 +882,9 @@ elabInstance info syn fc cs n ps t expn ds

873882

874883 eqRoot x y = nsroot x == nsroot y

875884

876− clauseFor m ns (PClauses _ _ m' _) = decorate ns m == decorate ns m'

877− clauseFor m ns _ = False

885+ clauseFor m iname ns (PClauses _ _ m' _)

886+ = decorate ns iname m == decorate ns iname m'

887+ clauseFor m iname ns _ = False

878888

879889decorateid decorate (PTy s f o n t) = PTy s f o (decorate n) t

880890decorateid decorate (PClauses f o n cs)

@@ -902,31 +912,40 @@ psolve tm = return ()

902912pvars ist (Bind n (PVar t) sc) = (n, delab ist t) : pvars ist sc

903913pvars ist _ = []

904914

905−-- TODO: Also build a 'binary' version of each declaration for fast reloading

915+data ElabWhat = ETypes | EDefns | EAll

916+ deriving (Show, Eq)

906917

907918elabDecl :: ElabInfo -> PDecl -> Idris ()

908−elabDecl info d = idrisCatch (elabDecl' info d)

919+elabDecl info d = idrisCatch (elabDecl' EAll info d)

909920 (\e -> do let msg = show e

910921 setErrLine (getErrLine msg)

911922 iputStrLn msg)

912923

913−elabDecl' info (PFix _ _ _) = return () -- nothing to elaborate

914−elabDecl' info (PSyntax _ p) = return () -- nothing to elaborate

915−elabDecl' info (PTy s f o n ty) = do iLOG $ "Elaborating type decl " ++ show n ++ show o

916− elabType info s f o n ty

917−elabDecl' info (PData s f co d) = do iLOG $ "Elaborating " ++ show (d_name d)

918− elabData info s f co d

919−elabDecl' info d@(PClauses f o n ps) = do iLOG $ "Elaborating clause " ++ show n

920− i <- get -- get the type options too

921− let o' = case lookupCtxt Nothing n (idris_flags i) of

922− [fs] -> fs

923− [] -> []

924− elabClauses info f (o ++ o') n ps

925−elabDecl' info (PParams f ns ps)

924+elabDecl' _ info (PFix _ _ _)

925+ = return () -- nothing to elaborate

926+elabDecl' _ info (PSyntax _ p)

927+ = return () -- nothing to elaborate

928+elabDecl' what info (PTy s f o n ty)

929+ | what /= EDefns

930+ = do iLOG $ "Elaborating type decl " ++ show n ++ show o

931+ elabType info s f o n ty

932+elabDecl' what info (PData s f co d)

933+ | what /= EDefns

934+ = do iLOG $ "Elaborating " ++ show (d_name d)

935+ elabData info s f co d

936+elabDecl' what info d@(PClauses f o n ps)

937+ | what /= ETypes

938+ = do iLOG $ "Elaborating clause " ++ show n

939+ i <- get -- get the type options too

940+ let o' = case lookupCtxt Nothing n (idris_flags i) of

941+ [fs] -> fs

942+ [] -> []

943+ elabClauses info f (o ++ o') n ps

944+elabDecl' what info (PParams f ns ps)

926945 = do i <- get

927946 iLOG $ "Expanding params block with " ++ show (concatMap declared ps)

928947 let nblock = pblock i

929− mapM_ (elabDecl' info) nblock

948+ mapM_ (elabDecl' what info) nblock

930949 where

931950 pinfo = let ds = concatMap declared ps

932951 newps = params info ++ ns

@@ -936,29 +955,35 @@ elabDecl' info (PParams f ns ps)

936955 inblock = newb }

937956 pblock i = map (expandParamsD i id ns (concatMap declared ps)) ps

938957

939−elabDecl' info (PNamespace n ps) = mapM_ (elabDecl' ninfo) ps

958+elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps

940959 where

941960 ninfo = case namespace info of

942961 Nothing -> info { namespace = Just [n] }

943962 Just ns -> info { namespace = Just (n:ns) }

944−elabDecl' info (PClass s f cs n ps ds) = do iLOG $ "Elaborating class " ++ show n

945− elabClass info s f cs n ps ds

946−elabDecl' info (PInstance s f cs n ps t expn ds)

963+elabDecl' what info (PClass s f cs n ps ds)

964+ | what /= EDefns

965+ = do iLOG $ "Elaborating class " ++ show n

966+ elabClass info s f cs n ps ds

967+elabDecl' what info (PInstance s f cs n ps t expn ds)

968+ | what /= EDefns

947969 = do iLOG $ "Elaborating instance " ++ show n

948970 elabInstance info s f cs n ps t expn ds

949−elabDecl' info (PRecord s f tyn ty cn cty)

971+elabDecl' what info (PRecord s f tyn ty cn cty)

972+ | what /= EDefns

950973 = do iLOG $ "Elaborating record " ++ show tyn

951974 elabRecord info s f tyn ty cn cty

952−elabDecl' info (PDSL n dsl)

975+elabDecl' _ info (PDSL n dsl)

953976 = do i <- get

954977 put (i { idris_dsls = addDef n dsl (idris_dsls i) })

955978 addIBC (IBCDSL n)

956−elabDecl' info (PDirective i) = i

979+elabDecl' what info (PDirective i)

980+ | what /= EDefns = i

981+elabDecl' _ _ _ = return () -- skipped this time

957982

958983elabCaseBlock info d@(PClauses f o n ps)

959984 = do addIBC (IBCDef n)

960985-- iputStrLn $ "CASE BLOCK: " ++ show (n, d)

961− elabDecl' info d

986+ elabDecl' EAll info d

962987

963988-- elabDecl' info (PImport i) = loadModule i

964989

src/Idris/IBC.hs+5−2

@@ -612,7 +612,8 @@ instance Binary Def where

612612 put x1

613613 put x2

614614 put x3

615− CaseOp x1 x2 x3 x4 x5 x6 x7 -> do putWord8 3

615+ CaseOp x1 x2 x3 x4 x5 x6 x7 x8 ->

616+ do putWord8 3

616617 put x1

617618 put x2

618619 put x3

@@ -620,6 +621,7 @@ instance Binary Def where

620621 put x5

621622 put x6

622623 put x7

624+ put x8

623625 get

624626 = do i <- getWord8

625627 case i of

@@ -640,7 +642,8 @@ instance Binary Def where

640642 x5 <- get

641643 x6 <- get

642644 x7 <- get

643− return (CaseOp x1 x2 x3 x4 x5 x6 x7)

645+ x8 <- get

646+ return (CaseOp x1 x2 x3 x4 x5 x6 x7 x8)

644647 _ -> error "Corrupted binary data for Def"

645648

646649instance Binary Accessibility where

src/Idris/Parser.hs+13−1

@@ -84,6 +84,8 @@ loadModule f

8484loadSource :: Bool -> FilePath -> Idris ()

8585loadSource lidr f

8686 = do iLOG ("Reading " ++ f)

87+ i <- getIState

88+ let def_total = default_total i

8789 file_in <- liftIO $ readFile f

8890 file <- if lidr then tclift $ unlit f file_in else return file_in

8991 (mname, modules, rest, pos) <- parseImports f file

@@ -104,6 +106,15 @@ loadSource lidr f

104106 when v $ iputStrLn $ "Type checking " ++ f

105107 mapM_ (elabDecl toplevel) ds

106108 i <- get

109+ -- simplify every definition do give the totality checker

110+ -- a better chance

111+ mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

112+ updateContext (simplifyCasedef n))

113+ (map snd (idris_totcheck i))

114+ -- build size change graph from simplified definitions

115+ iLOG "Totality checking"

116+ i <- get

117+-- mapM_ buildSCG (idris_totcheck i)

107118 mapM_ checkDeclTotality (idris_totcheck i)

108119 iLOG ("Finished " ++ f)

109120 ibcsd <- valIBCSubDir i

@@ -117,7 +128,8 @@ loadSource lidr f

117128 idrisCatch (do writeIBC f ibc; clearIBC)

118129 (\c -> return ()) -- failure is harmless

119130 i <- getIState

120− putIState (i { hide_list = [] })

131+ putIState (i { default_total = def_total,

132+ hide_list = [] })

121133 return ()

122134 where

123135 namespaces [] ds = ds

src/Idris/Prover.hs+4−2

@@ -50,8 +50,10 @@ prove ctxt lit n ty

5050 logLvl 3 (show tree)

5151 (ptm, pty) <- recheckC (FC "proof" 0) [] tm

5252 ptm' <- applyOpts ptm

53− updateContext (addCasedef n True False True [([], P Ref n ty, ptm)]

54− [([], P Ref n ty, ptm')] ty)

53+ updateContext (addCasedef n True False True

54+ [Right (P Ref n ty, ptm)]

55+ [([], P Ref n ty, ptm)]

56+ [([], P Ref n ty, ptm')] ty)

5557 solveDeferred n

5658elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

5759elabStep st e = do case runStateT e st of

src/Idris/REPL.hs+2−1

@@ -338,7 +338,7 @@ process fn (Pattelab t)

338338

339339process fn (Missing n) = do i <- get

340340 case lookupDef Nothing n (tt_ctxt i) of

341− [CaseOp _ _ _ args t _ _]

341+ [CaseOp _ _ _ _ args t _ _]

342342 -> do tms <- genMissing n args t

343343 iputStrLn (showSep "\n" (map (showImp True) tms))

344344 [] -> iputStrLn $ show n ++ " undefined"

@@ -404,6 +404,7 @@ parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)

404404parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)

405405parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)

406406parseArgs ("--partial":ns) = DefaultPartial : (parseArgs ns)

407+parseArgs ("--warnpartial":ns) = WarnPartial : (parseArgs ns)

407408parseArgs ("--nocoverage":ns) = NoCoverage : (parseArgs ns)

408409parseArgs ("--errorcontext":ns) = ErrContext : (parseArgs ns)

409410parseArgs ("--help":ns) = Usage : (parseArgs ns)

test/test016/test016.idr+1−1

@@ -15,6 +15,6 @@ take n [] = []

1515-- foo : main.countFrom 4 = 4 :: main.countFrom 5

1616-- foo = refl

1717

18−main : IO ()

18+partial main : IO ()

1919main = do print (take 10 (Main.countFrom 10))

2020

test/test017/expected+1−1

@@ -1 +1 @@

1−test017a.idr:5:scg.vtrans is possibly not total as it is not well founded

1+test017a.idr:5:scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans