d00053b · Idris-dev · git.iko.soy

CHANGELOG+1

compare with master

unifiedsplit

@@ -25,6 +25,7 @@ New in 0.9.13:

25* Extend :addclause to add instance bodies as well as definitions

26* Reverse parameters to BoundedList -- now matches Vect, and is easier to instantiate classes.

27* Move foldl into Foldable so it can be overridden.

28+* Experimental :search REPL command for finding functions by type

28

29

29Internal changes

30Internal changes

30

31

idris.cabal+3

@@ -452,6 +452,9 @@ Extra-source-files:

452 test/totality007/*.ipkg

453 test/totality007/src/*.idr

454 test/totality007/expected

455+ test/totality008/run

456+ test/totality008/*.idr

457+ test/totality008/expected

455

458

456 test/tutorial001/run

459 test/tutorial001/run

457 test/tutorial001/*.idr

460 test/tutorial001/*.idr

libs/effects/Effect/Exception.idr+1−1

@@ -27,7 +27,7 @@ EXCEPTION : Type -> EFFECT

27EXCEPTION t = MkEff () (Exception t)

28

29raise : a -> { [EXCEPTION a ] } Eff m b

30−raise err = effect $ Raise err

30+raise err = call $ Raise err

31

32

33

libs/effects/Effect/File.idr+5−5

@@ -107,27 +107,27 @@ open : Handler FileIO e =>

107 -> { [FILE_IO ()] ==> [FILE_IO (if result

108 then OpenFile m

109 else ())] } Eff e Bool

110−open f m = effect $ Open f m

110+open f m = call $ Open f m

111

112

113||| Close a file.

114close : Handler FileIO e =>

115 { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()

116−close = effect $ Close

116+close = call $ Close

117

118||| Read a line from the file.

119readLine : Handler FileIO e =>

120 { [FILE_IO (OpenFile Read)] } Eff e String

121−readLine = effect $ ReadLine

121+readLine = call $ ReadLine

122

123||| Write a line to a file.

124writeLine : Handler FileIO e =>

125 String -> { [FILE_IO (OpenFile Write)] } Eff e ()

126−writeLine str = effect $ WriteLine str

126+writeLine str = call $ WriteLine str

127

128||| End of file?

129eof : Handler FileIO e =>

130 { [FILE_IO (OpenFile Read)] } Eff e Bool

131−eof = effect $ EOF

131+eof = call $ EOF

132

133-- --------------------------------------------------------------------- [ EOF ]

libs/effects/Effect/Memory.idr+7−7

@@ -102,7 +102,7 @@ RAW_MEMORY t = MkEff t RawMemory

102

103allocate : (n : Nat) ->

104 Eff m () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])

105−allocate size = effect $ Allocate size

105+allocate size = call $ Allocate size

106

107initialize : {i : Nat} ->

108 {n : Nat} ->

@@ -111,17 +111,17 @@ initialize : {i : Nat} ->

111 so (i + size <= n) ->

112 Eff m () [RAW_MEMORY (MemoryChunk n i)]

113 (\v => [RAW_MEMORY (MemoryChunk n (i + size))])

114−initialize c size prf = effect $ Initialize c size prf

114+initialize c size prf = call $ Initialize c size prf

115

116free : Eff m () [RAW_MEMORY (MemoryChunk n i)] (\v => [RAW_MEMORY ()])

117−free = effect Free

117+free = call Free

118

119peek : {i : Nat} ->

120 (offset : Nat) ->

121 (size : Nat) ->

122 so (offset + size <= i) ->

123 { [RAW_MEMORY (MemoryChunk n i)] } Eff m (Vect size Bits8)

124−peek offset size prf = effect $ Peek offset size prf

124+peek offset size prf = call $ Peek offset size prf

125

126poke : {n : Nat} ->

127 {i : Nat} ->

@@ -130,11 +130,11 @@ poke : {n : Nat} ->

130 so (offset <= i && offset + size <= n) ->

131 Eff m () [RAW_MEMORY (MemoryChunk n i)]

132 (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])

133−poke offset content prf = effect $ Poke offset content prf

133+poke offset content prf = call $ Poke offset content prf

134

135private

136getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff m (MemoryChunk n i)

137−getRawPtr = effect $ GetRawPtr

137+getRawPtr = call $ GetRawPtr

138

139private

140move' : {dst_size : Nat} ->

@@ -149,7 +149,7 @@ move' : {dst_size : Nat} ->

149 Eff m () [RAW_MEMORY (MemoryChunk dst_size dst_init)]

150 (\v => [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))])

151move' src_ptr dst_offset src_offset size dst_bounds src_bounds

152− = effect $ Move src_ptr dst_offset src_offset size dst_bounds src_bounds

152+ = call $ Move src_ptr dst_offset src_offset size dst_bounds src_bounds

153

154data MoveDescriptor = Dst | Src

155

libs/effects/Effect/Random.idr+3−3

@@ -18,14 +18,14 @@ RND = MkEff Integer Random

18

19||| Generates a random Integer in a given range

20rndInt : Integer -> Integer -> { [RND] } Eff m Integer

21−rndInt lower upper = do v <- effect $ getRandom

21+rndInt lower upper = do v <- call $ getRandom

22 return (v `prim__sremBigInt` (upper - lower) + lower)

23

24||| Generate a random number in Fin (S `k`)

25|||

26||| Note that rndFin k takes values 0, 1, ..., k.

27rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))

28−rndFin k = do let v = assert_total $ !(effect getRandom) `prim__sremBigInt` (cast (S k))

28+rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast (S k))

29 return (toFin v)

30 where toFin : Integer -> Fin (S k)

31 toFin x = case integerToFin x (S k) of

@@ -43,5 +43,5 @@ rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))

43

44||| Sets the random seed

45srand : Integer -> { [RND] } Eff m ()

46−srand n = effect $ setSeed n

46+srand n = call $ setSeed n

47

libs/effects/Effect/Select.idr+1−1

@@ -19,5 +19,5 @@ SELECT : EFFECT

19SELECT = MkEff () Selection

20

21select : List a -> { [SELECT] } Eff m a

22−select xs = effect $ Select xs

22+select xs = call $ Select xs

23

libs/effects/Effect/State.idr+3−3

@@ -17,13 +17,13 @@ STATE : Type -> EFFECT

17STATE t = MkEff t State

18

19get : { [STATE x] } Eff m x

20−get = effect $ Get

20+get = call $ Get

21

22put : x -> { [STATE x] } Eff m ()

23−put val = effect $ Put val

23+put val = call $ Put val

24

25putM : y -> { [STATE x] ==> [STATE y] } Eff m ()

26−putM val = effect $ Put val

26+putM val = call $ Put val

27

28update : (x -> x) -> { [STATE x] } Eff m ()

29update f = put (f !get)

libs/effects/Effect/StdIO.idr+4−4

@@ -40,11 +40,11 @@ STDIO = MkEff () StdIO

40

41||| Write a string to standard output.

42putStr : Handler StdIO e => String -> { [STDIO] } Eff e ()

43−putStr s = effect $ PutStr s

43+putStr s = call $ PutStr s

44

45||| Write a character to standard output.

46putChar : Handler StdIO e => Char -> { [STDIO] } Eff e ()

47−putChar c = effect $ PutCh c

47+putChar c = call $ PutCh c

48

49||| Write a string to standard output, terminating with a newline.

50putStrLn : Handler StdIO e => String -> { [STDIO] } Eff e ()

@@ -52,9 +52,9 @@ putStrLn s = putStr (s ++ "\n")

52

53||| Read a string from standard input.

54getStr : Handler StdIO e => { [STDIO] } Eff e String

55−getStr = effect $ GetStr

55+getStr = call $ GetStr

56

57||| Read a character from standard input.

58getChar : Handler StdIO e => { [STDIO] } Eff e Char

59−getChar = effect $ GetCh

59+getChar = call $ GetCh

60

libs/effects/Effect/System.idr+3−3

@@ -28,11 +28,11 @@ SYSTEM : EFFECT

28SYSTEM = MkEff () System

29

30getArgs : Handler System e => { [SYSTEM] } Eff e (List String)

31−getArgs = effect Args

31+getArgs = call Args

32

33time : Handler System e => { [SYSTEM] } Eff e Int

34−time = effect Time

34+time = call Time

35

36getEnv : Handler System e => String -> { [SYSTEM] } Eff e (Maybe String)

37−getEnv s = effect $ GetEnv s

37+getEnv s = call $ GetEnv s

38

libs/effects/Effects.idr+22−8

@@ -144,7 +144,7 @@ data Eff : (m : Type -> Type)

144 Eff m a xs xs'

145 ebind : Eff m a xs xs' ->

146 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''

147− effectP : (prf : EffElem e a xs) ->

147+ callP : (prf : EffElem e a xs) ->

148 (eff : e t a b) ->

149 Eff m t xs (\v => updateResTy v xs prf eff)

150

@@ -166,6 +166,20 @@ data Eff : (m : Type -> Type)

166 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''

167(>>=) = ebind

168

169+-- namespace SimpleBind

170+-- (>>=) : Eff m a xs (\v => xs) ->

171+-- ((val : a) -> Eff m b xs xs') -> Eff m b xs xs'

172+-- (>>=) = ebind

173+

174+||| Run a subprogram which results in an effect state the same as the input.

175+staticEff : Eff m a xs (\v => xs) -> Eff m a xs (\v => xs)

176+staticEff = id

177+

178+||| Explicitly give the expected set of result effects for an effectful

179+||| operation.

180+toEff : .(xs' : List EFFECT) -> Eff m a xs (\v => xs') -> Eff m a xs (\v => xs')

181+toEff xs' = id

182+

169return : a -> Eff m a xs (\v => xs)

183return : a -> Eff m a xs (\v => xs)

170return x = value x

184return x = value x

171

185

@@ -204,7 +218,7 @@ eff env (value x) k = k x env

204eff env (with_val x prog) k = eff env prog (\p', env' => k x env')

218eff env (with_val x prog) k = eff env prog (\p', env' => k x env')

205eff env (prog `ebind` c) k

219eff env (prog `ebind` c) k

206 = eff env prog (\p', env' => eff env' (c p') k)

220 = eff env prog (\p', env' => eff env' (c p') k)

207−eff env (effectP prf effP) k = execEff env prf effP k

221+eff env (callP prf effP) k = execEff env prf effP k

208eff env (liftP prf effP) k

222eff env (liftP prf effP) k

209 = let env' = dropEnv env prf in

223 = let env' = dropEnv env prf in

210 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))

224 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))

@@ -233,12 +247,12 @@ syntax MkDefaultEnv = with Env

233 [default, default, default, default, default, default, default],

247 [default, default, default, default, default, default, default],

234 [default, default, default, default, default, default, default, default] |)

248 [default, default, default, default, default, default, default, default] |)

235

249

236−effect : {a, b: _} -> {e : Effect} ->

250+call : {a, b: _} -> {e : Effect} ->

237− (eff : e t a b) ->

251+ (eff : e t a b) ->

238− {default tactics { search 100; }

252+ {default tactics { search 100; }

239− prf : EffElem e a xs} ->

253+ prf : EffElem e a xs} ->

240− Eff m t xs (\v => updateResTy v xs prf eff)

254+ Eff m t xs (\v => updateResTy v xs prf eff)

241−effect e {prf} = effectP prf e

255+call e {prf} = callP prf e

242

256

243implicit

257implicit

244lift : Eff m t ys ys' ->

258lift : Eff m t ys ys' ->

libs/prelude/Builtins.idr+1−6

@@ -38,17 +38,12 @@ sym refl = refl

38trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c

39trans refl refl = refl

40

41−lazy : a -> a

42−lazy x = x -- compiled specially

43−

44−force : a -> a

45−force x = x -- compiled specially

46−

47||| There are two types of laziness: that arising from lazy functions, and that

41||| There are two types of laziness: that arising from lazy functions, and that

48||| arising from codata. They differ in their totality condition.

42||| arising from codata. They differ in their totality condition.

49data LazyType = LazyCodata | LazyEval

43data LazyType = LazyCodata | LazyEval

50

44

51||| The underlying implementation of Lazy and Inf.

45||| The underlying implementation of Lazy and Inf.

46+%error_reverse

52data Lazy' : LazyType -> Type -> Type where

47data Lazy' : LazyType -> Type -> Type where

53 ||| A delayed computation.

48 ||| A delayed computation.

54 |||

49 |||

libs/prelude/Prelude/List.idr−7

@@ -195,13 +195,6 @@ list nil cons (x::xs) = (Force cons) x xs

195(++) [] right = right

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

197

198−||| Create an infinite sequence of some item.

199−|||

200−||| Consider using a `Stream` instead.

201−partial

202−repeat : a -> List a

203−repeat x = x :: lazy (repeat x)

204−

205||| Construct a list with `n` copies of `x`

198||| Construct a list with `n` copies of `x`

206||| @ n how many copies

199||| @ n how many copies

207||| @ x the element to replicate

200||| @ x the element to replicate

libs/prelude/Prelude/Vect.idr+4

@@ -254,6 +254,10 @@ concat : Vect m (Vect n a) -> Vect (m * n) a

254concat [] = []

255concat (v::vs) = v ++ concat vs

256

257+||| Fold without seeding the accumulator

258+foldr1 : (t -> t -> t) -> Vect (S n) t -> t

259+foldr1 f (x::xs) = foldr f x xs

260+

257--------------------------------------------------------------------------------

261--------------------------------------------------------------------------------

258-- Scans

262-- Scans

259--------------------------------------------------------------------------------

263--------------------------------------------------------------------------------

src/Idris/AbsSyntax.hs+5−3

@@ -1329,9 +1329,11 @@ addImpl' inpat env infns ist ptm

1329 as' = map (fmap (ai env ds)) as in

1330 mkPApp fc 1 f' as'

1331 ai env ds (PCase fc c os)

1332− = let c' = ai env ds c

1332+ = let c' = ai env ds c in

1333− os' = map (pmap (ai env ds)) os in

1333+ -- leave os alone, because they get lifted into a new pattern match

1334+ -- definition which is passed through addImpl again with more scope

1335+ -- information

1334− PCase fc c' os'

1336+ PCase fc c' os

1335 ai env ds (PLam n ty sc)

1337 ai env ds (PLam n ty sc)

1336 = let ty' = ai env ds ty

1338 = let ty' = ai env ds ty

1337 sc' = ai ((n, Just ty):env) ds sc in

1339 sc' = ai ((n, Just ty):env) ds sc in

src/Idris/AbsSyntaxTree.hs+4−2

@@ -884,7 +884,8 @@ deriving instance NFData OptInfo

884data TypeInfo = TI { con_names :: [Name],

885 codata :: Bool,

886 data_opts :: DataOpts,

887− param_pos :: [Int] }

887+ param_pos :: [Int],

888+ mutual_types :: [Name] }

888 deriving Show

889 deriving Show

889{-!

890{-!

890deriving instance Binary TypeInfo

891deriving instance Binary TypeInfo

@@ -963,6 +964,7 @@ data SyntaxInfo = Syn { using :: [Using],

963 inPattern :: Bool,

964 inPattern :: Bool,

964 implicitAllowed :: Bool,

965 implicitAllowed :: Bool,

965 maxline :: Maybe Int,

966 maxline :: Maybe Int,

967+ mut_nesting :: Int,

966 dsl_info :: DSL }

968 dsl_info :: DSL }

967 deriving Show

969 deriving Show

968{-!

970{-!

@@ -970,7 +972,7 @@ deriving instance NFData SyntaxInfo

970deriving instance Binary SyntaxInfo

972deriving instance Binary SyntaxInfo

971!-}

973!-}

972

974

973−defaultSyntax = Syn [] [] [] [] id False False Nothing initDSL

975+defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL

974

976

975expandNS :: SyntaxInfo -> Name -> Name

977expandNS :: SyntaxInfo -> Name -> Name

976expandNS syn n@(NS _ _) = n

978expandNS syn n@(NS _ _) = n

src/Idris/Core/Elaborate.hs+4−2

@@ -681,11 +681,13 @@ try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

681try' t1 t2 proofSearch

682 = do s <- get

683 ps <- get_probs

684+ ulog <- getUnifyLog

684 case prunStateT 999999 False ps t1 s of

685 case prunStateT 999999 False ps t1 s of

685 OK ((v, _, _), s') -> do put s'

686 OK ((v, _, _), s') -> do put s'

686 return $! v

687 return $! v

688+ Error e1 -> traceWhen ulog ("try failed " ++ show e1) $

687− Error e1 -> if recoverableErr e1 then

689+ if recoverableErr e1 then

688− do case runStateT t2 s of

690+ do case runStateT t2 s of

689 OK (v, s') -> do put s'; return $! v

691 OK (v, s') -> do put s'; return $! v

690 Error e2 -> if score e1 >= score e2

692 Error e2 -> if score e1 >= score e2

691 then lift (tfail e1)

693 then lift (tfail e1)

src/Idris/Core/ProofState.hs+25−7

@@ -180,6 +180,19 @@ match_unify' ctxt env topx topy =

180-- -- ++ show (pterm ps)

181-- ++ "\n----------") $

182

183+mergeSolutions :: Env -> [(Name, TT Name)] -> StateT TState TC [(Name, TT Name)]

184+mergeSolutions env ns = merge [] ns

185+ where

186+ merge acc [] = return (reverse acc)

187+ merge acc ((n, t) : ns)

188+ | Just t' <- lookup n ns

189+ = do ps <- get

190+ let probs = problems ps

191+ put (ps { problems = probs ++ [(t,t',env,Msg "New problem",

192+ [], Unify)] })

193+ merge acc ns

194+ | otherwise = merge ((n, t): acc) ns

195+

183unify' :: Context -> Env -> TT Name -> TT Name ->

196unify' :: Context -> Env -> TT Name -> TT Name ->

184 StateT TState TC [(Name, TT Name)]

197 StateT TState TC [(Name, TT Name)]

185unify' ctxt env topx topy =

198unify' ctxt env topx topy =

@@ -206,17 +219,22 @@ unify' ctxt env topx topy =

206 ++ "\nCurrent problems:\n" ++ qshow (problems ps)

219 ++ "\nCurrent problems:\n" ++ qshow (problems ps)

207-- ++ show (pterm ps)

220-- ++ show (pterm ps)

208 ++ "\n----------") $

221 ++ "\n----------") $

209− do ps <- get

210− let (h, ns) = unified ps

222+ do let (h, ns) = unified ps

223+ -- if a metavar has multiple solutions, make a new unification

224+ -- problem for each.

225+ uns <- mergeSolutions env (u ++ ns)

226+ ps <- get

211− let (ns', probs') = updateProblems (context ps) (u ++ ns)

227+ let (ns', probs') = updateProblems (context ps) uns

212 (fails ++ problems ps)

228 (fails ++ problems ps)

213 (injective ps)

229 (injective ps)

214 (holes ps)

230 (holes ps)

215 let (notu', probs_notu) = mergeNotunified env (notu ++ notunified ps)

231 let (notu', probs_notu) = mergeNotunified env (notu ++ notunified ps)

232+ traceWhen (unifylog ps)

233+ ("Now solved: " ++ show ns') $

216− put (ps { problems = probs' ++ probs_notu,

234+ put (ps { problems = probs' ++ probs_notu,

217− unified = (h, ns'),

235+ unified = (h, ns'),

218− injective = updateInj u (injective ps),

236+ injective = updateInj u (injective ps),

219− notunified = notu' })

237+ notunified = notu' })

220 return u

238 return u

221 where updateInj ((n, a) : us) inj

239 where updateInj ((n, a) : us) inj

222 | (P _ n' _, _) <- unApply a,

240 | (P _ n' _, _) <- unApply a,

src/Idris/Core/Unify.hs+14−1

@@ -69,7 +69,20 @@ match_unify ctxt env topx topy inj holes from =

69 return (map (renameBinders env) (trimSolutions v))

70 _ -> tfail e

71 where

72−

72+ -- This rule is highly dubious... it certainly produces a valid answer

73+ -- but it scares me. However, matching is never guaranteed to give a unique

74+ -- answer, merely a valid one, so perhaps we're okay.

75+ -- In other words: it may vanish without warning some day :)

76+ un names x tm@(App (P _ f (Bind fn (Pi t) sc)) a)

77+ | (P (DCon _ _) _ _, _) <- unApply x,

78+ holeIn env f || f `elem` holes

79+ = let n' = uniqueName (sMN 0 "mv") (map fst env) in

80+ checkCycle names (f, Bind n' (Lam t) x)

81+ un names tm@(App (P _ f (Bind fn (Pi t) sc)) a) x

82+ | (P (DCon _ _) _ _, _) <- unApply x,

83+ holeIn env f || f `elem` holes

84+ = let n' = uniqueName fn (map fst env) in

85+ checkCycle names (f, Bind n' (Lam t) x)

73

86

74 un names (P _ x _) tm

87 un names (P _ x _) tm

75 | holeIn env x || x `elem` holes

88 | holeIn env x || x `elem` holes

src/Idris/Coverage.hs+29−12

@@ -211,7 +211,7 @@ genAll i args

211 let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))

212 let tyn = getTy n (tt_ctxt i)

213 case lookupCtxt tyn (idris_datatypes i) of

214− (TI ns _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])

214+ (TI ns _ _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])

215 _ -> [p]

216 ops fc n arg o = return Placeholder

217

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

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

266checkAllCovering _ _ _ _ = return ()

267

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

268−-- Check if, in a given type n, the constructor cn : ty is strictly positive,

269+-- the constructor cn : ty is strictly positive,

269-- and update the context accordingly

270-- and update the context accordingly

270

271

271−checkPositive :: Name -> (Name, Type) -> Idris ()

272+checkPositive :: [Name] -> (Name, Type) -> Idris Totality

272−checkPositive n (cn, ty')

273+checkPositive mut_ns (cn, ty')

273− = do let ty = delazy ty'

274+ = do let ty = delazy' True ty'

274 let p = cp ty

275 let p = cp ty

275 i <- getIState

276 i <- getIState

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

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

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

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

278 putIState (i { tt_ctxt = ctxt' })

279 putIState (i { tt_ctxt = ctxt' })

279− logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot

280+ logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot ++ " with " ++ show mut_ns

280 addIBC (IBCTotal cn tot)

281 addIBC (IBCTotal cn tot)

282+ return tot

281 where

283 where

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

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

283

285

284 cp (Bind n (Pi aty) sc) = posArg aty && cp sc

286 cp (Bind n (Pi aty) sc) = posArg aty && cp sc

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

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

285− cp t = True

289+ cp _ = True

286

290

287 posArg (Bind _ (Pi nty) sc)

291 posArg (Bind _ (Pi nty) sc)

288 | (P _ n' _, args) <- unApply nty

292 | (P _ n' _, args) <- unApply nty

289− = n /= n' && posArg sc

293+ = n' `notElem` mut_ns && all noRec args && posArg sc

290− posArg t = True

294+ posArg t | (P _ n' _, args) <- unApply t,

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

296+ posArg _ = True

297+

298+ noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)

299+

291

300

292calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality

301calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality

293calcProd i fc topn pats

302calcProd i fc topn pats

@@ -335,7 +344,7 @@ calcProd i fc topn pats

335 cotype (DCon _ _) n ty

344 cotype (DCon _ _) n ty

336 | (P _ t _, _) <- unApply (getRetTy ty)

345 | (P _ t _, _) <- unApply (getRetTy ty)

337 = case lookupCtxt t (idris_datatypes i) of

346 = case lookupCtxt t (idris_datatypes i) of

338− [TI _ True _ _] -> True

347+ [TI _ True _ _ _] -> True

339 _ -> False

348 _ -> False

340 cotype nt n ty = False

349 cotype nt n ty = False

341

350

@@ -383,6 +392,14 @@ checkTotality path fc n

383 setTotality n t'

392 setTotality n t'

384 addIBC (IBCTotal n t')

393 addIBC (IBCTotal n t')

385 return t'

394 return t'

395+ [TyDecl (DCon _ _) ty] ->

396+ case unApply (getRetTy ty) of

397+ (P _ tyn _, _) -> do

398+ let ms = case lookupCtxt tyn (idris_datatypes i) of

399+ [TI _ _ _ _ xs@(_:_)] -> xs

400+ ts -> [tyn]

401+ checkPositive ms (n, ty)

402+ _-> return $ Total []

386 _ -> return $ Total []

403 _ -> return $ Total []

387 x -> return x

404 x -> return x

388 case t' of

405 case t' of

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

556

573

557 isInductive (P _ nty _) (P _ nty' _) =

574 isInductive (P _ nty _) (P _ nty' _) =

558 let co = case lookupCtxt nty (idris_datatypes ist) of

575 let co = case lookupCtxt nty (idris_datatypes ist) of

559− [TI _ x _ _] -> x

576+ [TI _ x _ _ _] -> x

560 _ -> False in

577 _ -> False in

561 nty == nty' && not co

578 nty == nty' && not co

562 isInductive _ _ = False

579 isInductive _ _ = False

@@ -639,7 +656,7 @@ checkMP ist i mp = if i > 0

639 = case lookupTotal f (tt_ctxt ist) of

656 = case lookupTotal f (tt_ctxt ist) of

640 [Total _] -> Unchecked -- okay so far

657 [Total _] -> Unchecked -- okay so far

641 [Partial _] -> Partial (Other [f])

658 [Partial _] -> Partial (Other [f])

642− x -> error (show x)

659+ x -> error $ "CAN'T HAPPEN: " ++ (show x)

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

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

644 = Total []

661 = Total []

645 tryPath desc path (e@(f, args) : es) arg

662 tryPath desc path (e@(f, args) : es) arg

src/Idris/DeepSeq.hs+3−3

@@ -290,7 +290,7 @@ instance NFData OptInfo where

290 = rnf x1 `seq` rnf x2 `seq` ()

291

292instance NFData TypeInfo where

293− rnf (TI x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

293+ rnf (TI x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

294

295instance (NFData t) => NFData (DSL' t) where

296 rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

@@ -321,11 +321,11 @@ instance NFData Using where

321

322

323instance NFData SyntaxInfo where

324− rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9)

324+ rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

325 = rnf x1 `seq`

326 rnf x2 `seq`

327 rnf x3 `seq`

328− rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

328+ rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()

329

330

331

src/Idris/ElabDecls.hs+22−4

@@ -125,7 +125,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

125 let (t, _) = unApply (getRetTy nty')

126 let corec = case t of

127 P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of

128− [TI _ True _ _] -> True

128+ [TI _ True _ _ _] -> True

129 _ -> False

130 _ -> False

131 -- Productivity checking now via checking for guarded 'Delay'

@@ -256,8 +256,10 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

256 let as = map (const Nothing) (getArgTys cty)

257 let params = findParams (map snd cons)

258 logLvl 2 $ "Parameters : " ++ show params

259+ -- TI contains information about mutually declared types - this will

260+ -- be updated when the mutual block is complete

259 putIState (i { idris_datatypes =

261 putIState (i { idris_datatypes =

260− addDef n (TI (map fst cons) codata opts params)

262+ addDef n (TI (map fst cons) codata opts params [n])

261 (idris_datatypes i) })

263 (idris_datatypes i) })

262 addIBC (IBCDef n)

264 addIBC (IBCDef n)

263 addIBC (IBCData n)

265 addIBC (IBCData n)

@@ -269,7 +271,8 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

269 -- TMP HACK! Make this a data option

271 -- TMP HACK! Make this a data option

270 updateContext (addDatatype (Data n ttag cty cons))

272 updateContext (addDatatype (Data n ttag cty cons))

271 updateContext (setMetaInformation n metainf)

273 updateContext (setMetaInformation n metainf)

274+ mapM_ totcheck (zip (repeat fc) (map fst cons))

272− mapM_ (checkPositive n) cons

275+-- mapM_ (checkPositive n) cons

273

276

274 -- if there's exactly one constructor,

277 -- if there's exactly one constructor,

275 -- mark both the type and the constructor as detaggable

278 -- mark both the type and the constructor as detaggable

@@ -1617,7 +1620,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1617 rev <- case ret_fam of

1620 rev <- case ret_fam of

1618 P _ rfamn _ ->

1621 P _ rfamn _ ->

1619 case lookupCtxt rfamn (idris_datatypes i) of

1622 case lookupCtxt rfamn (idris_datatypes i) of

1620− [TI _ _ dopts _] ->

1623+ [TI _ _ dopts _ _] ->

1621 return (DataErrRev `elem` dopts)

1624 return (DataErrRev `elem` dopts)

1622 _ -> return False

1625 _ -> return False

1623 _ -> return False

1626 _ -> return False

@@ -2340,6 +2343,11 @@ elabDecl' what info (PMutual f ps)

2340 [p] -> elabDecl what info p

2343 [p] -> elabDecl what info p

2341 _ -> do mapM_ (elabDecl ETypes info) ps

2344 _ -> do mapM_ (elabDecl ETypes info) ps

2342 mapM_ (elabDecl EDefns info) ps

2345 mapM_ (elabDecl EDefns info) ps

2346+ -- record mutually defined data definitions

2347+ let datans = concatMap declared (filter isDataDecl ps)

2348+ mapM_ (setMutData datans) datans

2349+ iLOG $ "Rechecking for positivity " ++ show datans

2350+ mapM_ (\x -> do setTotality x Unchecked) datans

2343 -- Do totality checking after entire mutual block

2351 -- Do totality checking after entire mutual block

2344 i <- get

2352 i <- get

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

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

@@ -2348,6 +2356,16 @@ elabDecl' what info (PMutual f ps)

2348 mapM_ buildSCG (idris_totcheck i)

2356 mapM_ buildSCG (idris_totcheck i)

2349 mapM_ checkDeclTotality (idris_totcheck i)

2357 mapM_ checkDeclTotality (idris_totcheck i)

2350 clear_totcheck

2358 clear_totcheck

2359+ where isDataDecl (PData _ _ _ _ _ _) = True

2360+ isDataDecl _ = False

2361+

2362+ setMutData ns n

2363+ = do i <- getIState

2364+ case lookupCtxt n (idris_datatypes i) of

2365+ [x] -> do let x' = x { mutual_types = ns }

2366+ putIState $ i { idris_datatypes

2367+ = addDef n x' (idris_datatypes i) }

2368+ _ -> return ()

2351

2369

2352elabDecl' what info (PParams f ns ps)

2370elabDecl' what info (PParams f ns ps)

2353 = do i <- getIState

2371 = do i <- getIState

src/Idris/ElabTerm.hs+24−5

@@ -66,9 +66,11 @@ build ist info pattern opts fn tm

66 ctxt <- get_context

67 probs <- get_probs

68 u <- getUnifyLog

69+ hs <- get_holes

69

70

70 when (not pattern) $

71 when (not pattern) $

72+ traceWhen u ("Remaining holes:\n" ++ show hs ++ "\n" ++

71− traceWhen u ("Remaining problems:\n" ++ show probs) $

73+ "Remaining problems:\n" ++ show probs) $

72 do unify_all; matchProblems True; unifyProblems

74 do unify_all; matchProblems True; unifyProblems

73

75

74 probs <- get_probs

76 probs <- get_probs

@@ -265,7 +267,8 @@ elab ist info pattern opts fn tm

265 ty <- goal

267 ty <- goal

266 ctxt <- get_context

268 ctxt <- get_context

267 let (tc, _) = unApply ty

269 let (tc, _) = unApply ty

270+ env <- get_env

268− let as' = pruneByType tc ctxt as

271+ let as' = pruneByType (map fst env) tc ctxt as

269-- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $

272-- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $

270 tryAll (zip (map (elab' ina) as') (map showHd as'))

273 tryAll (zip (map (elab' ina) as') (map showHd as'))

271 where showHd (PApp _ (PRef _ n) _) = show n

274 where showHd (PApp _ (PRef _ n) _) = show n

@@ -695,6 +698,9 @@ elab ist info pattern opts fn tm

695 addImpl ist (PApp fc (PRef fc (sUN "Delay"))

698 addImpl ist (PApp fc (PRef fc (sUN "Delay"))

696 [pexp t])

699 [pexp t])

697

700

701+ -- case is tricky enough without implicit coercions! If they are needed,

702+ -- they can go in the branches separately.

703+ insertCoerce ina t@(PCase _ _ _) = return t

698 insertCoerce ina t =

704 insertCoerce ina t =

699 do ty <- goal

705 do ty <- goal

700 -- Check for possible coercions to get to the goal

706 -- Check for possible coercions to get to the goal

@@ -785,8 +791,21 @@ pruneAlt xs = map prune xs

785

791

786-- Rule out alternatives that don't return the same type as the head of the goal

792-- Rule out alternatives that don't return the same type as the head of the goal

787-- (If there are none left as a result, do nothing)

793-- (If there are none left as a result, do nothing)

788−pruneByType :: Term -> Context -> [PTerm] -> [PTerm]

794+pruneByType :: [Name] -> Term -> Context -> [PTerm] -> [PTerm]

795+-- if an alternative has a locally bound name at the head, take it

789−pruneByType (P _ n _) c as

796+pruneByType env t c as

797+ | Just a <- locallyBound as = [a]

798+ where

799+ locallyBound [] = Nothing

800+ locallyBound (t:ts)

801+ | Just n <- getName t,

802+ n `elem` env = Just t

803+ | otherwise = locallyBound ts

804+ getName (PRef _ n) = Just n

805+ getName (PApp _ f _) = getName f

806+ getName _ = Nothing

807+

808+pruneByType env (P _ n _) c as

790-- if the goal type is polymorphic, keep e

809-- if the goal type is polymorphic, keep e

791 | [] <- lookupTy n c = as

810 | [] <- lookupTy n c = as

792 | otherwise

811 | otherwise

@@ -812,7 +831,7 @@ pruneByType (P _ n _) c as

812 _ -> False

831 _ -> False

813 _ -> False

832 _ -> False

814

833

815−pruneByType t _ as = as

834+pruneByType _ t _ as = as

816

835

817findInstances :: IState -> Term -> [Name]

836findInstances :: IState -> Term -> [Name]

818findInstances ist t

837findInstances ist t

src/Idris/IBC.hs+10−8

@@ -30,7 +30,7 @@ import Codec.Compression.Zlib (compress)

30import Util.Zlib (decompressEither)

31

32ibcVersion :: Word8

33−ibcVersion = 73

33+ibcVersion = 74

34

35data IBCFile = IBCFile { ver :: Word8,

36 sourcefile :: FilePath,

@@ -1582,7 +1582,7 @@ instance Binary Using where

1582 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)

1583

1584instance Binary SyntaxInfo where

1585− put (Syn x1 x2 x3 x4 _ x5 x6 _ x7)

1585+ put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7)

1586 = do put x1

1587 put x2

1588 put x3

@@ -1598,7 +1598,7 @@ instance Binary SyntaxInfo where

1598 x5 <- get

1599 x6 <- get

1600 x7 <- get

1601− return (Syn x1 x2 x3 x4 id x5 x6 Nothing x7)

1601+ return (Syn x1 x2 x3 x4 id x5 x6 Nothing 0 x7)

1602

1603instance (Binary t) => Binary (PClause' t) where

1604 put x

@@ -2152,15 +2152,17 @@ instance Binary OptInfo where

2152 return (Optimise x1 x2)

2153

2154instance Binary TypeInfo where

2155− put (TI x1 x2 x3 x4) = do put x1

2155+ put (TI x1 x2 x3 x4 x5) = do put x1

2156− put x2

2156+ put x2

2157− put x3

2157+ put x3

2158− put x4

2158+ put x4

2159+ put x5

2159 get = do x1 <- get

2160 get = do x1 <- get

2160 x2 <- get

2161 x2 <- get

2161 x3 <- get

2162 x3 <- get

2162 x4 <- get

2163 x4 <- get

2164+ x5 <- get

2163− return (TI x1 x2 x3 x4)

2165+ return (TI x1 x2 x3 x4 x5)

2164

2166

2165instance Binary SynContext where

2167instance Binary SynContext where

2166 put x

2168 put x

src/Idris/Parser.hs+2−2

@@ -163,7 +163,7 @@ decl syn = do fc <- getFC

163 let continue = case maxline syn of

164 Nothing -> True

165 Just l -> if fst (fc_end fc) > l

166− then False

166+ then mut_nesting syn /= 0

167 else True

168 if continue then do notEndBlock

169 declBody

@@ -502,7 +502,7 @@ mutual syn =

502 do reserved "mutual"

503 openBlock

504 let pvars = syn_params syn

505− ds <- many (decl syn)

505+ ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))

506 closeBlock

507 fc <- getFC

508 return [PMutual fc (concat ds)]

test/totality008/expectednew file+1

@@ -0,0 +1 @@

1+totality008.idr:7:1:Main.ElimT is possibly not total due to: Main.c2

test/totality008/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ totality008.idr --check

3+rm -f *.ibc

test/totality008/totality008.idrnew file+8

@@ -0,0 +1,8 @@

1+ data T : Type -> Type where

2+ c1 : T Nat

3+ c2 : T (T Nat)

4+

5+total

6+ElimT : (A : Type) -> T A -> A

7+ElimT _ c1 = 3

8+ElimT _ c2 = c1