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

git.iko.soy/Idris-dev

on master help sign in

Totality checker improvements

9affb75Edwin Brady14 years ago

CHANGELOG+1

compare with master

unifiedsplit

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

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

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

14 line options.

15+* New termination checker supporting mutually recursive definitions.

16Internal changes:

17Internal changes:

lib/Builtins.idr+5−1

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

1%access public

2+%default total

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

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

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

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

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

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

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

235 fromInteger = prim__intToFloat

236 fromInteger = prim__intToFloat

236

237

237−

238+partial

238div : Int -> Int -> Int

239div : Int -> Int -> Int

239div = prim__divInt

240div = prim__divInt

240

241

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

247(++) : String -> String -> String

248(++) : String -> String -> String

248(++) = prim__concat

249(++) = prim__concat

249

250

251+partial

250strHead : String -> Char

252strHead : String -> Char

251strHead = prim__strHead

253strHead = prim__strHead

252

254

255+partial

253strTail : String -> String

256strTail : String -> String

254strTail = prim__strTail

257strTail = prim__strTail

255

258

256strCons : Char -> String -> String

259strCons : Char -> String -> String

257strCons = prim__strCons

260strCons = prim__strCons

258

261

262+partial

259strIndex : String -> Int -> Char

263strIndex : String -> Int -> Char

260strIndex = prim__strIndex

264strIndex = prim__strIndex

261

265

lib/IO.idr+1−1

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

3%access public

5−abstract codata IO a = prim__IO a

5+abstract data IO a = prim__IO a

7abstract

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

lib/Prelude.idr+22−1

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

16import Prelude.Chars

18%access public

19+%default total

20-- Show and instances

21-- Show and instances

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

157

158

158---- Ranges

159---- Ranges

159

160

161+partial

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

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

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

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

162 else []

164 else []

163

165

166+partial

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

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

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

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

166

169

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

184

187

185---- some basic io

188---- some basic io

186

189

190+partial

187putStr : String -> IO ()

191putStr : String -> IO ()

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

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

189

193

194+partial

190putStrLn : String -> IO ()

195putStrLn : String -> IO ()

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

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

192

197

198+partial

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

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

194print x = putStrLn (show x)

200print x = putStrLn (show x)

195

201

202+partial

196getLine : IO String

203getLine : IO String

197getLine = return (prim__readString prim__stdin)

204getLine = return (prim__readString prim__stdin)

198

205

206+partial

199putChar : Char -> IO ()

207putChar : Char -> IO ()

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

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

201

209

210+partial

202getChar : IO Char

211getChar : IO Char

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

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

204

213

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

216

225

217data Mode = Read | Write | ReadWrite

226data Mode = Read | Write | ReadWrite

218

227

228+partial

219openFile : String -> Mode -> IO File

229openFile : String -> Mode -> IO File

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

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

221 modeStr : Mode -> String

231 modeStr : Mode -> String

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

223 modeStr Write = "w"

233 modeStr Write = "w"

224 modeStr ReadWrite = "r+"

234 modeStr ReadWrite = "r+"

225

235

236+partial

226do_fclose : Ptr -> IO ()

237do_fclose : Ptr -> IO ()

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

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

228

239

240+partial

229closeFile : File -> IO ()

241closeFile : File -> IO ()

230closeFile (FHandle h) = do_fclose h

242closeFile (FHandle h) = do_fclose h

231

243

244+partial

232do_fread : Ptr -> IO String

245do_fread : Ptr -> IO String

233do_fread h = return (prim__readString h)

246do_fread h = return (prim__readString h)

234

247

248+partial

235fread : File -> IO String

249fread : File -> IO String

236fread (FHandle h) = do_fread h

250fread (FHandle h) = do_fread h

237

251

252+partial

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

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

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

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

240

255

256+partial

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

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

242fwrite (FHandle h) s = do_fwrite h s

258fwrite (FHandle h) s = do_fwrite h s

243

259

260+partial

244do_feof : Ptr -> IO Int

261do_feof : Ptr -> IO Int

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

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

246

263

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

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

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

249 return (not (eof == 0))

266 return (not (eof == 0))

250

267

268+partial

251nullPtr : Ptr -> IO Bool

269nullPtr : Ptr -> IO Bool

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

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

253 return (ok /= 0);

271 return (ok /= 0);

254

272

273+partial

255validFile : File -> IO Bool

274validFile : File -> IO Bool

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

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

257 return (not x)

276 return (not x)

258

277

278+partial -- obviously

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

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

260while t b = do v <- t

280while t b = do v <- t

261 if v then do b

281 if v then do b

262 while t b

282 while t b

263 else return ()

283 else return ()

264

284

265−

285+partial -- no error checking!

266readFile : String -> IO String

286readFile : String -> IO String

267readFile fn = do h <- openFile fn Read

287readFile fn = do h <- openFile fn Read

268 c <- readFile' h ""

288 c <- readFile' h ""

269 closeFile h

289 closeFile h

270 return c

290 return c

271 where

291 where

292+ partial

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

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

273 readFile' h contents =

294 readFile' h contents =

274 do x <- feof h

295 do x <- feof h

lib/Prelude/List.idr+11−1

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

7import Prelude.Nat

9%access public

10+%default total

11infixr 7 ::

12infixr 7 ::

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

30-- Indexing into lists

31-- Indexing into lists

31--------------------------------------------------------------------------------

32--------------------------------------------------------------------------------

34+%assert_total

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

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

34head (x::xs) p = x

36head (x::xs) p = x

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

37head' [] = Nothing

39head' [] = Nothing

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

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

42+%assert_total

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

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

41tail (x::xs) p = xs

44tail (x::xs) p = xs

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

44tail' [] = Nothing

47tail' [] = Nothing

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

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

50+%assert_total

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

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

48last (x::xs) p =

52last (x::xs) p =

49 case xs of

53 case xs of

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

57 [] => Just x

61 [] => Just x

58 y::ys => last' xs

62 y::ys => last' xs

64+%assert_total

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

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

61init (x::xs) p =

66init (x::xs) p =

62 case xs of

67 case xs of

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

116(++) [] right = right

121(++) [] right = right

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

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

118

123

124+partial

119repeat : a -> List a

125repeat : a -> List a

120repeat x = x :: repeat x

126repeat x = x :: repeat x

121

127

128+%assert_total

122replicate : Nat -> a -> List a

129replicate : Nat -> a -> List a

123replicate n x = take n (repeat x)

130replicate n x = take n (repeat x)

124

131

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

160-- Zips and unzips

167-- Zips and unzips

161--------------------------------------------------------------------------------

168--------------------------------------------------------------------------------

162

169

170+%assert_total

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

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

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

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

165zipWith f [] [] p = []

173zipWith f [] [] p = []

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

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

167

175

176+%assert_total

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

177zipWith3 : (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

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

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

179zipWith3 f [] [] [] refl refl = []

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

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

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

451merge = mergeBy compare

460merge = mergeBy compare

452

461

462+%assert_total

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

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

454sort [] = []

464sort [] = []

455sort [x] = [x]

465sort [x] = [x]

456sort xs =

466sort xs =

457 let (x, y) = split xs in

467 let (x, y) = split xs in

458− merge (sort x) (sort y)

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

459 where

469 where

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

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

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

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

lib/Prelude/Nat.idr+1

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

6import Prelude.Cast

8%access public

9+%default total

10data Nat

11data Nat

11 = O

12 = O

lib/Prelude/Vect.idr+4−4

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

5import Prelude.Nat

7%access public

8+%default total

9infixr 7 ::

10infixr 7 ::

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

54-- Conversions to and from list

55-- Conversions to and from list

55--------------------------------------------------------------------------------

56--------------------------------------------------------------------------------

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

58+toList : Vect a n -> List a

58toList [] = []

59toList [] = []

59toList (x::xs) = x :: toList xs

60toList (x::xs) = x :: toList xs

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

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

62fromList [] = []

63fromList [] = []

63fromList (x::xs) = x :: fromList xs

64fromList (x::xs) = x :: fromList xs

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

66-- Building (bigger) vectors

67-- Building (bigger) vectors

67--------------------------------------------------------------------------------

68--------------------------------------------------------------------------------

69−total

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

71(++) [] ys = ys

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

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

79-- Maps

80--------------------------------------------------------------------------------

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

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

83map f [] = []

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

src/Core/CaseTree.hs+1−1

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

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

71small :: SC -> Bool

72−small t = termsize t < 150

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

74namesUsed :: SC -> [Name]

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

src/Core/Evaluate.hs+59−26

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

5 simplify, specialise, hnf, convEq, convEq',

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

7 Context, initContext, ctxtAlist, uconstraints, next_tvar,

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

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

9− addCasedef, addOperator,

9+ addDatatype, addCasedef, simplifyCasedef, addOperator,

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

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

11− lookupTyEnv, isConName, isFnName,

11+ lookupTotal, lookupTyEnv, isConName, isFnName,

12 Value(..)) where

14import Debug.Trace

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

167 ev ntimes (n:stk) True env tm

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

169 return $ VP nt n vty

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

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

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

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

173 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

231 = traceWhen traceon (show stk) $

232 do let val = lookupDefAcc Nothing n atRepl ctxt

233 case val of

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

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

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

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

237 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

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

392 [Function _ t] -> ev env t

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

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

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

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

396 case c of

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

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

421 app <- apply env sc' as

422 wknH (-1) app

423 apply env (HP Ref n ty) args

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

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

425 = do c <- evCase env ns args tree

426 case c of

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

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

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

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

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

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

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

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

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

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

554 _ -> return False

555

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

571data Def = Function Type Term

572 | TyDecl NameType Type

573 | 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

575 [Name] SC -- Compile time case definition

577 [Name] SC -- Compile time case definition

576 [Name] SC -- Run time cae definitions

578 [Name] SC -- Run time cae definitions

577{-!

579{-!

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

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

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

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

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

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

586 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')

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

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

587 show ns ++ " " ++ show sc ++ "\n" ++

589 show ns ++ " " ++ show sc ++ "\n" ++

588 show ns' ++ " " ++ show sc'

590 show ns' ++ " " ++ show sc'

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

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

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

621 show (Partial NotProductive) = "not productive"

623 show (Partial NotProductive) = "not productive"

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

624 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 " ++

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

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

625

627

626{-!

628{-!

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

635deriving instance Binary PReason

637deriving instance Binary PReason

636!-}

638!-}

637

639

640+data Context = MkContext {

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

641+ uconstraints :: [UConstraint],

639− next_tvar :: Int,

642+ next_tvar :: Int,

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

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

644+ }

641

645

642initContext = MkContext [] 0 emptyContext

646initContext = MkContext [] 0 emptyContext

643

647

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

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

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

691

695

692addCasedef :: Name -> Bool -> Bool -> Bool ->

696addCasedef :: Name -> Bool -> Bool -> Bool ->

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

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

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

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

694 Type -> Context -> Context

700 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

696 = let ctxt = definitions uctxt

702 = let ctxt = definitions uctxt

697 access = case lookupDefAcc Nothing n False uctxt of

703 access = case lookupDefAcc Nothing n False uctxt of

698 [(_, acc)] -> acc

704 [(_, acc)] -> acc

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

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

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

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

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

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

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

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

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

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

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

705− access, Unchecked) ctxt in

711+ access, Unchecked) ctxt in

706 uctxt { definitions = ctxt' }

712 uctxt { definitions = ctxt' }

707−

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+

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

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

741+ Context -> Context

709addOperator n ty a op uctxt

742addOperator n ty a op uctxt

710 = let ctxt = definitions uctxt

743 = let ctxt = definitions uctxt

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

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

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

725 (Function ty _) -> return ty

758 (Function ty _) -> return ty

726 (TyDecl _ ty) -> return ty

759 (TyDecl _ ty) -> return ty

727 (Operator ty _ _) -> return ty

760 (Operator ty _ _) -> return ty

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

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

729

762

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

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

731isConName root n ctxt

764isConName root n ctxt

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

741 case tfst def of

774 case tfst def of

742 (Function _ _) -> return True

775 (Function _ _) -> return True

743 (Operator _ _ _) -> return True

776 (Operator _ _ _) -> return True

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

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

745 _ -> return False

778 _ -> return False

746

779

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

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

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

750 p <- case def of

783 p <- case def of

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

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

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

785 (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)

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

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

755 case snd p of

788 case snd p of

756 Hidden -> []

789 Hidden -> []

src/Core/TT.hs+4

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

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

196emptyContext = Map.empty

197

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

199+tcname (NS n _) = tcname n

200+tcname _ = False

201+

198nsroot (NS n _) = n

202nsroot (NS n _) = n

199nsroot n = n

203nsroot n = n

200

204

src/IRTS/Compiler.hs+2−2

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

129

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

131 return (declArgs [] n e)

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

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

133− return (declArgs [] n e)

133+ return (declArgs [] n e)

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

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

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

src/Idris/AbsSyntax.hs+5−5

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

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

45totcheck :: (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] })

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

49setFlags 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

325 $ do liftIO (putStrLn str)

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

327

328+cmdOptSet :: Opt -> Idris Bool

329+cmdOptSet x = do i <- get

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

331+

328iLOG :: String -> Idris ()

332iLOG :: String -> Idris ()

329iLOG = logLvl 1

333iLOG = logLvl 1

330

334

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

413piBindp p [] t = t

417piBindp p [] t = t

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

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

415

419

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

417−tcname (NS n _) = tcname n

418−tcname _ = False

419−

420-- Dealing with parameters

421

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

src/Idris/AbsSyntaxTree.hs+1

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

184 | TypeInType

185 | DefaultTotal

186 | DefaultPartial

187+ | WarnPartial

187 | NoCoverage

188 | NoCoverage

188 | ErrContext

189 | ErrContext

189 | ShowImpl

190 | ShowImpl

src/Idris/Coverage.hs+66−23

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

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

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

254 putIState (i { tt_ctxt = ctxt' })

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

255 addIBC (IBCTotal cn tot)

256 addIBC (IBCTotal cn tot)

256 where

257 where

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

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

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

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

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

329 | otherwise = do

330 | otherwise = do

330 t <- getTotality n

331 t <- getTotality n

332+ updateContext (simplifyCasedef n)

331 ctxt <- getContext

333 ctxt <- getContext

332 i <- getIState

334 i <- getIState

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

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

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

336 t' <- case t of

338 t' <- case t of

337 Unchecked ->

339 Unchecked ->

338 case lookupDef Nothing n ctxt of

340 case lookupDef Nothing n ctxt of

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

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

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

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

341 then return $ Total []

343 then return $ Total []

342 else calcTotality path fc n pats

344 else calcTotality path fc n pats

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

349-- p@(Partial _) ->

351-- p@(Partial _) ->

350-- do setAccessibility n Frozen

352-- do setAccessibility n Frozen

351-- addIBC (IBCAccess n Frozen)

353-- addIBC (IBCAccess n Frozen)

352−-- iputStrLn $ "HIDDEN: "

354+-- logLvl 5 $ "HIDDEN: "

353-- ++ show n ++ show p

355-- ++ show n ++ show p

354− _ -> return ()

356+ _ -> return ()

355 return t'

357 return t'

356 _ -> return $ Total []

358 _ -> return $ Total []

357 x -> return x

359 x -> return x

358− if TotalFn `elem` opts

359− then case t' of

360+ case t' of

360− Total _ -> return t'

361+ Total _ -> return t'

361− Productive -> return t'

362+ Productive -> return t'

363+ e -> do w <- cmdOptSet WarnPartial

364+ if TotalFn `elem` opts

362− e -> totalityError t'

365+ then totalityError t'

366+ else do when w $ warnPartial n t'

363− else return t'

367+ return t'

364 where

368 where

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

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

366

370

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+

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

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

368checkDeclTotality (fc, n)

382checkDeclTotality (fc, n)

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

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

384+ buildSCG (fc, n)

370 checkTotality [] fc n

385 checkTotality [] fc n

371

386

372-- Calculate the size change graph for this definition

387-- Calculate the size change graph for this definition

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

380-- to f

395-- to f

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

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

382

397

383−-- FIXME: Higher order recursive arguments

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

384−

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+

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

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

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

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

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

412 (zip args (zip args (repeat Same)))

388 where

413 where

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

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

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

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

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

428

453

429 scgTerm f@(App _ _) vars szs

454 scgTerm f@(App _ _) vars szs

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

456+ = scgTerm arg vars szs

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

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

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

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

432 case lookup fn vars of

459 case lookup fn vars of

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

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

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

448 -> Maybe (Int, SizeChange)

475 -> Maybe (Int, SizeChange)

449 mkChange szs tm

476 mkChange szs tm

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

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

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

451 = do sc <- lookup n szs

479 = do sc <- lookup n szs

452 case sc of

480 case sc of

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

466 case lookupCtxt Nothing n (idris_callgraph ist) of

494 case lookupCtxt Nothing n (idris_callgraph ist) of

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

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

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

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

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

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

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

499+ logLvl 6 (show cg)

470 -- every multipath must have an infinitely descending

500 -- every multipath must have an infinitely descending

471 -- thread, then the function terminates

501 -- thread, then the function terminates

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

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

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

478type MultiPath = [SCGEntry]

508type MultiPath = [SCGEntry]

479

509

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

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

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

481mkMultiPaths ist path cg

512mkMultiPaths ist path cg

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

513+ = concat (map extend cg)

514+ where extend (nextf, args)

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

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

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

516+ | otherwise

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

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

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

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

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)

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

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

488

527

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

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

490-- Try a route beginning with every argument.

529-- Try a route beginning with every argument.

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

507 x -> error (show x)

546 x -> error (show x)

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

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

509 = Total []

548 = Total []

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

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

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

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

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

511 | Just d <- lookup e path

553 | Just d <- lookup e path

512 = if (desc - d) > 0

554 = if (desc - d) > 0

513 then Total []

555 then Total []

514− else Partial Itself

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

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

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

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

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

517− collapse $

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

518 do (arg, pos) <- argspos

560 do (arg, pos) <- argspos

519 case arg of

561 case arg of

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

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

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

540noPartial (_ : xs) = noPartial xs

582noPartial (_ : xs) = noPartial xs

541noPartial [] = Total []

583noPartial [] = Total []

542

584

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

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

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

544−collapse (_ : xs) = collapse xs

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

545−collapse [] = Partial Itself

588+collapse' def [] = def

546

589

src/Idris/ElabDecls.hs+82−57

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

133

134 tryElabDecl info (fn, ty, val)

135 = do i <- get

136− idrisCatch (do elabDecl' info ty

136+ idrisCatch (do elabDecl' EAll info ty

137− elabDecl' info val)

137+ elabDecl' EAll info val)

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

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

140 show fn ++ " (" ++ show ty ++ ")"

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

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

296

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

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

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

299+ simpleCase tcase False CompileTime fc pdef

299 cov <- coverage

300 cov <- coverage

300 pmissing <-

301 pmissing <-

301 if cov

302 if cov

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

325 case tree of

326 case tree of

326 CaseDef _ _ [] -> return ()

327 CaseDef _ _ [] -> return ()

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

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

328− iputStrLn $ show fc ++

329+ iputStrLn $ show fc ++

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

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

330− show (delab ist x)) xs

331+ show (delab ist x)) xs

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

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

332 logLvl 3 (show tree)

333 logLvl 3 (show tree)

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

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

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

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

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

337 case lookupTy (namespace info) n ctxt of

338 case lookupTy (namespace info) n ctxt of

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

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

340+ tcase pcover pats

339− tcase pcover pdef pdef' ty)

341+ pdef pdef' ty)

340 addIBC (IBCDef n)

342 addIBC (IBCDef n)

341 setTotality n tot

343 setTotality n tot

342 totcheck (fc, n)

344 totcheck (fc, n)

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

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

344 i <- get

346 i <- get

345 case lookupDef Nothing n (tt_ctxt i) of

347 case lookupDef Nothing n (tt_ctxt i) of

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

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

347 do let calls = findCalls sc' scargs'

349 do let calls = findCalls sc' scargs'

348 let used = findUsedArgs sc' scargs'

350 let used = findUsedArgs sc' scargs'

349− let scg = buildSCG i sc scargs

351+ -- let scg = buildSCG i sc scargs

352+ -- add SCG later, when checking totality

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

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

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

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

352 addToCG n cg

355 addToCG n cg

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

356 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)

441 let newargs = pvars ist lhs_tm

444 let newargs = pvars ist lhs_tm

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

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

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

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

444− mapM_ (elabDecl' info) wb

447+ mapM_ (elabDecl' EAll info) wb

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

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

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

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

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

450 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)

475 checkInferred fc (delab' i crhs True) rhs

478 checkInferred fc (delab' i crhs True) rhs

476 return $ Right (clhs, crhs)

479 return $ Right (clhs, crhs)

477 where

480 where

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

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

479 pinfo ns ps i

482 pinfo ns ps i

480 = let ds = concatMap declared ps

483 = let ds = concatMap declared ps

481 newps = params info ++ ns

484 newps = params info ++ ns

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

765 _ -> []

768 _ -> []

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

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

767 let t' = substMatches ips t in

770 let t' = substMatches ips t in

771+ (decorate ns iname n,

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

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

769 (class_methods ci)

773 (class_methods ci)

770 logLvl 3 (show (mtys, ips))

774 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

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

776 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))

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

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

779+ let wbTys = map mkTyDecl mtys

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

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

781+ let wb = wbTys ++ wbVals

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

782 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

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

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

779 PApp _ _ args -> getWParams args

786 PApp _ _ args -> getWParams args

780 _ -> return []) ps

787 _ -> return []) ps

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

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

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

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

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

787 (map (pexp . mkMethApp) mtys)

794 (map (pexp . mkMethApp) mtys)

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

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

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

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

790− iLOG (show idecl)

797+ iLOG (show idecls)

791− elabDecl info idecl

798+ mapM (elabDecl info) idecls

792 addIBC (IBCInstance intInst n iname)

799 addIBC (IBCInstance intInst n iname)

793 where

800 where

794 intInst = case ps of

801 intInst = case ps of

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

838 _ -> return ps'

845 _ -> return ps'

839 getWParams (_ : ps) = getWParams ps

846 getWParams (_ : ps) = getWParams ps

840

847

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

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

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

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

843

850

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

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

845

852

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

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

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

850 coninsert cs sc = conbind cs sc

857 coninsert cs sc = conbind cs sc

851

858

859+ insertDefaults :: IState -> Name ->

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

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

861+ [PDecl] -> [PDecl]

853− insertDefaults i [] ns ds = ds

862+ insertDefaults i iname [] ns ds = ds

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

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

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

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

856

865

857− insertDef i meth def clauses ns decls

866+ insertDef i meth def clauses ns iname decls

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

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

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

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

860 -- trace (show newd) $

869 -- trace (show newd) $

861 decls ++ [newd]

870 decls ++ [newd]

862 | otherwise = decls

871 | otherwise = decls

863

872

864− warnMissing decls ns meth

873+ warnMissing decls ns iname meth

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

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

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

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

867 | otherwise = return ()

876 | otherwise = return ()

868

877

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

873

882

874 eqRoot x y = nsroot x == nsroot y

883 eqRoot x y = nsroot x == nsroot y

875

884

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

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

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

877− clauseFor m ns _ = False

887+ clauseFor m iname ns _ = False

878

888

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

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

880decorateid decorate (PClauses f o n cs)

890decorateid decorate (PClauses f o n cs)

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

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

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

903pvars ist _ = []

913pvars ist _ = []

904

914

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

915+data ElabWhat = ETypes | EDefns | EAll

916+ deriving (Show, Eq)

906

917

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

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

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

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

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

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

910 setErrLine (getErrLine msg)

921 setErrLine (getErrLine msg)

911 iputStrLn msg)

922 iputStrLn msg)

912

923

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

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

925+ = return () -- nothing to elaborate

926+elabDecl' _ info (PSyntax _ p)

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

927+ = return () -- nothing to elaborate

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

929+ | what /= EDefns

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

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

916− elabType info s f o n ty

931+ elabType info s f o n ty

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

933+ | what /= EDefns

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

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

918− elabData info s f co d

935+ elabData info s f co d

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

937+ | what /= ETypes

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

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

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

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

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

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

922− [fs] -> fs

941+ [fs] -> fs

923− [] -> []

942+ [] -> []

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

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

925−elabDecl' info (PParams f ns ps)

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

926 = do i <- get

945 = do i <- get

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

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

928 let nblock = pblock i

947 let nblock = pblock i

929− mapM_ (elabDecl' info) nblock

948+ mapM_ (elabDecl' what info) nblock

930 where

949 where

931 pinfo = let ds = concatMap declared ps

950 pinfo = let ds = concatMap declared ps

932 newps = params info ++ ns

951 newps = params info ++ ns

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

936 inblock = newb }

955 inblock = newb }

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

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

938

957

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

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

940 where

959 where

941 ninfo = case namespace info of

960 ninfo = case namespace info of

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

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

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

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

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

964+ | what /= EDefns

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

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

945− elabClass info s f cs n ps ds

966+ elabClass info s f cs n ps ds

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

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

968+ | what /= EDefns

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

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

948 elabInstance info s f cs n ps t expn ds

970 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

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

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

951 elabRecord info s f tyn ty cn cty

974 elabRecord info s f tyn ty cn cty

952−elabDecl' info (PDSL n dsl)

975+elabDecl' _ info (PDSL n dsl)

953 = do i <- get

976 = do i <- get

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

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

955 addIBC (IBCDSL n)

978 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

957

982

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

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

959 = do addIBC (IBCDef n)

984 = do addIBC (IBCDef n)

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

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

961− elabDecl' info d

986+ elabDecl' EAll info d

962

987

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

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

964

989

src/Idris/IBC.hs+5−2

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

612 put x1

613 put x2

614 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

616 put x1

617 put x1

617 put x2

618 put x2

618 put x3

619 put x3

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

620 put x5

621 put x5

621 put x6

622 put x6

622 put x7

623 put x7

624+ put x8

623 get

625 get

624 = do i <- getWord8

626 = do i <- getWord8

625 case i of

627 case i of

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

640 x5 <- get

642 x5 <- get

641 x6 <- get

643 x6 <- get

642 x7 <- get

644 x7 <- get

645+ x8 <- get

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

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

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

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

645

648

646instance Binary Accessibility where

649instance Binary Accessibility where

src/Idris/Parser.hs+13−1

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

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

85loadSource lidr f

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

87+ i <- getIState

88+ let def_total = default_total i

87 file_in <- liftIO $ readFile f

89 file_in <- liftIO $ readFile f

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

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

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

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

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

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

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

105 mapM_ (elabDecl toplevel) ds

107 mapM_ (elabDecl toplevel) ds

106 i <- get

108 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)

107 mapM_ checkDeclTotality (idris_totcheck i)

118 mapM_ checkDeclTotality (idris_totcheck i)

108 iLOG ("Finished " ++ f)

119 iLOG ("Finished " ++ f)

109 ibcsd <- valIBCSubDir i

120 ibcsd <- valIBCSubDir i

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

117 idrisCatch (do writeIBC f ibc; clearIBC)

128 idrisCatch (do writeIBC f ibc; clearIBC)

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

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

119 i <- getIState

130 i <- getIState

131+ putIState (i { default_total = def_total,

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

132+ hide_list = [] })

121 return ()

133 return ()

122 where

134 where

123 namespaces [] ds = ds

135 namespaces [] ds = ds

src/Idris/Prover.hs+4−2

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

50 logLvl 3 (show tree)

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

52 ptm' <- applyOpts ptm

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

53+ updateContext (addCasedef n True False True

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

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

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

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

55 solveDeferred n

57 solveDeferred n

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

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

57elabStep st e = do case runStateT e st of

59elabStep st e = do case runStateT e st of

src/Idris/REPL.hs+2−1

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

338

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

340 case lookupDef Nothing n (tt_ctxt i) of

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

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

342 -> do tms <- genMissing n args t

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

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

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

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

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

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

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

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

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

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

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

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

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

test/test016/test016.idr+1−1

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

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

16-- foo = refl

18−main : IO ()

18+partial main : IO ()

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

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