2315ddf · Idris-dev · git.iko.soy

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

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

2727EXCEPTION t = MkEff () (Exception t)

2828

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

30−raise err = Raise err

30+raise err = effect $ Raise err

3131

3232

3333

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

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

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

108108 then OpenFile m

109109 else ())] } Eff e Bool

110−open f m = Open f m

110+open f m = effect $ Open f m

111111

112112

113113||| Close a file.

114114close : Handler FileIO e =>

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

116−close = Close

116+close = effect $ Close

117117

118118||| Read a line from the file.

119119readLine : Handler FileIO e =>

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

121−readLine = ReadLine

121+readLine = effect $ ReadLine

122122

123123||| Write a line to a file.

124124writeLine : Handler FileIO e =>

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

126−writeLine str = WriteLine str

126+writeLine str = effect $ WriteLine str

127127

128128||| End of file?

129129eof : Handler FileIO e =>

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

131−eof = EOF

131+eof = effect $ EOF

132132

133133-- --------------------------------------------------------------------- [ EOF ]

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

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

102102

103103allocate : (n : Nat) ->

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

105−allocate size = Allocate size

105+allocate size = effect $ Allocate size

106106

107107initialize : {i : Nat} ->

108108 {n : Nat} ->

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

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

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

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

114−initialize c size prf = Initialize c size prf

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

115115

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

117−free = Free

117+free = effect Free

118118

119119peek : {i : Nat} ->

120120 (offset : Nat) ->

121121 (size : Nat) ->

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

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

124−peek offset size prf = Peek offset size prf

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

125125

126126poke : {n : Nat} ->

127127 {i : Nat} ->

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

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

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

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

133−poke offset content prf = Poke offset content prf

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

134134

135135private

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

137−getRawPtr = GetRawPtr

137+getRawPtr = effect $ GetRawPtr

138138

139139private

140140move' : {dst_size : Nat} ->

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

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

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

151151move' src_ptr dst_offset src_offset size dst_bounds src_bounds

152− = Move 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

153153

154154data MoveDescriptor = Dst | Src

155155

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

@@ -9,7 +9,7 @@ data Random : Effect where

99using (m : Type -> Type)

1010 instance Handler Random m where

1111 handle seed getRandom k

12− = let seed' = (1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32) in

12+ = let seed' = assert_total ((1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32)) in

1313 k seed' seed'

1414 handle seed (setSeed n) k = k () n

1515

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

1818

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

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

21−rndInt lower upper = do v <- getRandom

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

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

2323

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

2525|||

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

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

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

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

2929 return (toFin v)

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

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

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

4343

4444||| Sets the random seed

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

46−srand n = setSeed n

46+srand n = effect $ setSeed n

4747

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

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

1919SELECT = MkEff () Selection

2020

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

22−select xs = Select xs

22+select xs = effect $ Select xs

2323

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

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

1717STATE t = MkEff t State

1818

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

20−get = Get

20+get = effect $ Get

2121

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

23−put val = Put val

23+put val = effect $ Put val

2424

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

26−putM val = Put val

26+putM val = effect $ Put val

2727

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

2929update f = put (f !get)

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

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

4040

4141||| Write a string to standard output.

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

43−putStr s = PutStr s

43+putStr s = effect $ PutStr s

4444

4545||| Write a character to standard output.

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

47−putChar c = PutCh c

47+putChar c = effect $ PutCh c

4848

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

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

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

5252

5353||| Read a string from standard input.

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

55−getStr = GetStr

55+getStr = effect $ GetStr

5656

5757||| Read a character from standard input.

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

59−getChar = GetCh

59+getChar = effect $ GetCh

6060

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

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

2828SYSTEM = MkEff () System

2929

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

31−getArgs = Args

31+getArgs = effect Args

3232

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

34−time = Time

34+time = effect Time

3535

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

37−getEnv s = GetEnv s

37+getEnv s = effect $ GetEnv s

3838

libs/effects/Effects.idr+19−19

@@ -31,9 +31,9 @@ class Handler (e : Effect) (m : Type -> Type) where

3131 |||

3232 ||| @ r The resource being handled.

3333 ||| @ eff The effect to be applied.

34− ||| @ ctxt The context in which to handle the effect.

35− handle : (r : res) -> (eff : e t res resk) ->

36− (ctxt : ((x : t) -> resk x -> m a)) -> m a

34+ ||| @ k The continuation to pass the result of the effect

35+ covering handle : (r : res) -> (eff : e t res resk) ->

36+ (k : ((x : t) -> resk x -> m a)) -> m a

3737

3838||| Get the resource type (handy at the REPL to find out about an effect)

3939resourceType : EFFECT -> Type

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

144144 Eff m a xs xs'

145145 ebind : Eff m a xs xs' ->

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

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

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

148148 (eff : e t a b) ->

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

150150

151− lift : (prf : SubList ys xs) ->

151+ liftP : (prf : SubList ys xs) ->

152152 Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)

153153 newInit : Handler e m =>

154154 res ->

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

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

205205eff env (prog `ebind` c) k

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

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

208−eff env (lift prf effP) k

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

208+eff env (liftP prf effP) k

209209 = let env' = dropEnv env prf in

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

211211eff env (newInit r prog) k

@@ -233,20 +233,20 @@ syntax MkDefaultEnv = with Env

233233 [default, default, default, default, default, default, default],

234234 [default, default, default, default, default, default, default, default] |)

235235

236−implicit

237−lift' : Eff m t ys ys' ->

238− {default tactics { search 100; }

239− prf : SubList ys xs} ->

240− Eff m t xs (\v => updateWith (ys' v) xs prf)

241−lift' e {prf} = lift prf e

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

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

238+ {default tactics { search 100; }

239+ prf : EffElem e a xs} ->

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

241+effect e {prf} = effectP prf e

242242

243243implicit

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

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

246− {default tactics { search 100; }

247− prf : EffElem e a xs} ->

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

249−effect' e {prf} = effect prf e

244+lift : Eff m t ys ys' ->

245+ {default tactics { search 100; }

246+ prf : SubList ys xs} ->

247+ Eff m t xs (\v => updateWith (ys' v) xs prf)

248+lift e {prf} = liftP prf e

249+

250250

251251new : Handler e m =>

252252 {default default r : res} ->

src/IRTS/Simplified.hs+16−14

@@ -125,15 +125,17 @@ checkDefs ctxt (con@(n, DConstructor _ _ _) : xs)

125125 return xs'

126126checkDefs ctxt ((n, DFun n' args exp) : xs)

127127 = do let sexp = evalState (simplify True exp) (ctxt, 0)

128− (exp', locs) <- runStateT (scopecheck ctxt (zip args [0..]) sexp) (length args)

128+ (exp', locs) <- runStateT (scopecheck n ctxt (zip args [0..]) sexp) (length args)

129129 xs' <- checkDefs ctxt xs

130130 return ((n, SFun n' args ((locs + 1) - length args) exp') : xs')

131131

132132lvar v = do i <- get

133133 put (max i v)

134134

135−scopecheck :: DDefs -> [(Name, Int)] -> SExp -> StateT Int TC SExp

136−scopecheck ctxt envTop tm = sc envTop tm where

135+scopecheck :: Name -> DDefs -> [(Name, Int)] -> SExp -> StateT Int TC SExp

136+scopecheck fn ctxt envTop tm = sc envTop tm where

137+ failsc err = fail $ "Codegen error in " ++ show fn ++ ":" ++ err

138+

137139 sc env (SV (Glob n)) =

138140 case lookup n (reverse env) of -- most recent first

139141 Just i -> do lvar i; return (SV (Loc i))

@@ -141,20 +143,20 @@ scopecheck ctxt envTop tm = sc envTop tm where

141143 Just (DConstructor _ i ar) ->

142144 if True -- ar == 0

143145 then return (SCon i n [])

144− else fail $ "Codegen error: Constructor " ++ show n ++

146+ else failsc $ "Constructor " ++ show n ++

145147 " has arity " ++ show ar

146148 Just _ -> return (SV (Glob n))

147− Nothing -> fail $ "Codegen error: No such variable " ++ show n

149+ Nothing -> failsc $ "No such variable " ++ show n

148150 sc env (SApp tc f args)

149151 = do args' <- mapM (scVar env) args

150152 case lookupCtxtExact f ctxt of

151153 Just (DConstructor n tag ar) ->

152154 if True -- (ar == length args)

153155 then return $ SCon tag n args'

154− else fail $ "Codegen error: Constructor " ++ show f ++

156+ else failsc $ "Constructor " ++ show f ++

155157 " has arity " ++ show ar

156158 Just _ -> return $ SApp tc f args'

157− Nothing -> fail $ "Codegen error: No such variable " ++ show f

159+ Nothing -> failsc $ "No such variable " ++ show f

158160 sc env (SForeign l ty f args)

159161 = do args' <- mapM (\ (t, a) -> do a' <- scVar env a

160162 return (t, a')) args

@@ -165,9 +167,9 @@ scopecheck ctxt envTop tm = sc envTop tm where

165167 Just (DConstructor n tag ar) ->

166168 if True -- (ar == length args)

167169 then return $ SCon tag n args'

168− else fail $ "Codegen error: Constructor " ++ show f ++

169− " has arity " ++ show ar

170− _ -> fail $ "Codegen error: No such constructor " ++ show f

170+ else failsc $ "Constructor " ++ show f ++

171+ " has arity " ++ show ar

172+ _ -> failsc $ "No such constructor " ++ show f

171173 sc env (SProj e i)

172174 = do e' <- scVar env e

173175 return (SProj e' i)

@@ -200,9 +202,9 @@ scopecheck ctxt envTop tm = sc envTop tm where

200202 Just i -> do lvar i; return (Loc i)

201203 Nothing -> case lookupCtxtExact n ctxt of

202204 Just (DConstructor _ i ar) ->

203− fail $ "Codegen error : can't pass constructor here"

205+ failsc $ "can't pass constructor here"

204206 Just _ -> return (Glob n)

205− Nothing -> fail $ "Codegen error: No such variable " ++ show n ++

207+ Nothing -> failsc $ "No such variable " ++ show n ++

206208 " in " ++ show tm ++ " " ++ show envTop

207209 scVar _ x = return x

208210

@@ -212,9 +214,9 @@ scopecheck ctxt envTop tm = sc envTop tm where

212214 Just (DConstructor _ i ar) ->

213215 if True -- (length args == ar)

214216 then return i

215− else fail $ "Codegen error: Constructor " ++ show n ++

217+ else failsc $ "Constructor " ++ show n ++

216218 " has arity " ++ show ar

217− _ -> fail $ "Codegen error: No constructor " ++ show n

219+ _ -> failsc $ "No constructor " ++ show n

218220 e' <- sc env' e

219221 return (SConCase (length env) tag n args e')

220222 scalt env (SConstCase c e) = do e' <- sc env e

src/Idris/AbsSyntaxTree.hs+1

@@ -1338,6 +1338,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

13381338 prettySe p bnd PImpossible = kwd "impossible"

13391339 prettySe p bnd Placeholder = text "_"

13401340 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"

1341+ prettySe p bnd (PCoerced t) = prettySe p bnd t

13411342 prettySe p bnd (PElabError s) = pretty s

13421343

13431344 prettySe p bnd _ = text "test"

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

@@ -695,6 +695,7 @@ try' t1 t2 proofSearch

695695 = -- traceWhen r (show err) $

696696 r || proofSearch

697697 recoverableErr (CantSolveGoal _ _) = False

698+ recoverableErr (ProofSearchFail (Msg _)) = True

698699 recoverableErr (ProofSearchFail _) = False

699700 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

700701 recoverableErr (At _ e) = recoverableErr e

@@ -724,7 +725,7 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

724725 = do s <- get

725726 ps <- get_probs

726727 case prunStateT pmax True ps x s of

727− OK ((v, newps, probs), s') ->

728+ OK ((v, newps, probs), s') ->

728729 do let cs' = if (newps < pmax)

729730 then [do put s'; return $! v]

730731 else (do put s'; return $! v) : cs

src/Idris/Core/Evaluate.hs+9−4

@@ -537,7 +537,7 @@ wknV i t = return t

537537convEq' ctxt hs x y = evalStateT (convEq ctxt hs x y) (0, [])

538538

539539convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

540−convEq ctxt holes = ceq [] where

540+convEq ctxt holes topx topy = ceq [] topx topy where

541541 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

542542 ceq ps (P xt x _) (P yt y _)

543543 | x `elem` holes || y `elem` holes = return True

@@ -550,8 +550,12 @@ convEq ctxt holes = ceq [] where

550550 ceq ps (Bind n (Lam t) (App x (P Bound n' _))) y

551551 | n == n' = ceq ps x y

552552 ceq ps (V x) (V y) = return (x == y)

553− ceq ps (V x) (P _ y _) = return (fst (ps!!x) == y)

554− ceq ps (P _ x _) (V y) = return (x == snd (ps!!y))

553+ ceq ps (V x) (P _ y _)

554+ | x >= 0 && length ps > x = return (fst (ps!!x) == y)

555+ | otherwise = return False

556+ ceq ps (P _ x _) (V y)

557+ | y >= 0 && length ps > y = return (x == snd (ps!!y))

558+ | otherwise = return False

555559 ceq ps (Bind n xb xs) (Bind n' yb ys)

556560 = liftM2 (&&) (ceqB ps xb yb) (ceq ((n,n'):ps) xs ys)

557561 where

@@ -678,7 +682,7 @@ data Totality = Total [Int] -- ^ well-founded arguments

678682

679683-- | Reasons why a function may not be total

680684data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name

681− | BelieveMe | Mutual [Name] | NotProductive

685+ | ExternalIO | BelieveMe | Mutual [Name] | NotProductive

682686 deriving (Show, Eq)

683687

684688instance Show Totality where

@@ -688,6 +692,7 @@ instance Show Totality where

688692 show (Partial Itself) = "possibly not total as it is not well founded"

689693 show (Partial NotCovering) = "not total as there are missing cases"

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

695+ show (Partial ExternalIO) = "an external IO primitive"

691696 show (Partial NotProductive) = "not productive"

692697 show (Partial BelieveMe) = "not total due to use of believe_me in proof"

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

src/Idris/Core/ProofState.hs+4−3

@@ -789,8 +789,9 @@ updateSolved' [] x = x

789789updateSolved' xs (Bind n (Hole ty) t)

790790 | Just v <- lookup n xs

791791 = case xs of

792− [_] -> psubst n v t

793− _ -> psubst n v (updateSolved' xs t)

792+ [_] -> substV v $ psubst n v t -- some may be Vs! Can't assume

793+ -- explicit names

794+ _ -> substV v $ psubst n v (updateSolved' xs t)

794795updateSolved' xs (Bind n b t)

795796 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)

796797updateSolved' xs (App f a)

@@ -838,7 +839,7 @@ updateProblems ctxt ns ps inj holes = up ns ps where

838839 y' = updateSolved ns y

839840 err' = updateError ns err

840841 env' = updateEnv ns env in

841−-- trace ("Updating " ++ show (x',y')) $

842+-- trace ("Updating " ++ show (x',y')) $

842843 case unify ctxt env' x' y' inj holes while of

843844 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

844845 up (ns ++ v) ps

src/Idris/Core/TT.hs+9−4

@@ -184,9 +184,12 @@ score :: Err -> Int

184184score (CantUnify _ _ _ m _ s) = s + score m

185185score (CantResolve _) = 20

186186score (NoSuchVariable _) = 1000

187−score (ProofSearchFail _) = 10000

188−score (CantSolveGoal _ _) = 10000

187+score (ProofSearchFail e) = score e

188+score (CantSolveGoal _ _) = 100000

189189score (InternalMsg _) = -1

190+score (At _ e) = score e

191+score (ElaboratingArg _ _ _ e) = score e

192+score (Elaborating _ _ e) = score e

190193score _ = 0

191194

192195instance Show Err where

@@ -203,6 +206,7 @@ instance Show Err where

203206 show (ElaboratingArg f x prev e) = "Elaborating " ++ show f ++ " arg " ++

204207 show x ++ ": " ++ show e

205208 show (Elaborating what n e) = "Elaborating " ++ what ++ show n ++ ":" ++ show e

209+ show (ProofSearchFail e) = "Proof search fail: " ++ show e

206210 show _ = "Error"

207211

208212instance Pretty Err OutputAnnotation where

@@ -1056,8 +1060,9 @@ uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs

10561060

10571061uniqueBinders :: [Name] -> TT Name -> TT Name

10581062uniqueBinders ns (Bind n b sc)

1059− = let n' = uniqueName n ns in

1060− Bind n' (fmap (uniqueBinders (n':ns)) b) (uniqueBinders ns sc)

1063+ = let n' = uniqueName n ns

1064+ ns' = n' : ns in

1065+ Bind n' (fmap (uniqueBinders ns') b) (uniqueBinders ns' sc)

10611066uniqueBinders ns (App f a) = App (uniqueBinders ns f) (uniqueBinders ns a)

10621067uniqueBinders ns t = t

10631068

src/Idris/Core/Unify.hs+21−8

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

8585 | length bnames > i,

8686 fst (fst (bnames!!i)) == x ||

8787 snd (fst (bnames!!i)) == x = do sc 1; return []

88− un bnames (Bind x bx sx) (Bind y by sy)

88+ un bnames (Bind x bx sx) (Bind y by sy) | notHole bx && notHole by

8989 = do h1 <- uB bnames bx by

9090 h2 <- un (((x, y), binderTy bx) : bnames) sx sy

9191 combine bnames h1 h2

@@ -119,6 +119,9 @@ match_unify ctxt env topx topy inj holes from =

119119 put (UI s ((binderTy x, binderTy y, env, err, from, Match) : f))

120120 return []

121121

122+ notHole (Hole _) = False

123+ notHole _ = True

124+

122125 -- TODO: there's an annoying amount of repetition between this and the

123126 -- main unification function. Consider lifting it out.

124127

@@ -173,7 +176,7 @@ renameBindersTm env tm = uniqueBinders (map fst env) tm

173176 uniqueBinders env (Bind n b sc)

174177 | n `elem` env

175178 = let n' = uniqueName n env in

176− Bind n' (fmap (uniqueBinders env) b)

179+ explicitHole $ Bind n' (fmap (uniqueBinders env) b)

177180 (uniqueBinders (n':env) (rename n n' sc))

178181 | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)

179182 (uniqueBinders (n:env) sc)

@@ -185,6 +188,10 @@ renameBindersTm env tm = uniqueBinders (map fst env) tm

185188 rename n n' (App f a) = App (rename n n' f) (rename n n' a)

186189 rename n n' t = t

187190

191+ explicitHole (Bind n (Hole ty) sc)

192+ = Bind n (Hole ty) (instantiate (P Bound n ty) sc)

193+ explicitHole t = t

194+

188195trimSolutions ns = dropPairs ns

189196 where dropPairs [] = []

190197 dropPairs (n@(x, P _ x' _) : ns)

@@ -204,11 +211,16 @@ expandLets env (x, tm) = (x, doSubst (reverse env) tm)

204211 doSubst (_ : env) tm

205212 = doSubst env tm

206213

214+hasv (V x) = True

215+hasv (App f a) = hasv f || hasv a

216+hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

217+hasv _ = False

207218

208219unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] -> [FailContext] ->

209220 TC ([(Name, TT Name)], Fails)

210221unify ctxt env topx topy inj holes from =

211−-- trace ("Unifying " ++ show (topx, topy)) $

222+-- traceWhen (hasv topx || hasv topy)

223+-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $

212224 -- don't bother if topx and topy are different at the head

213225 case runStateT (un False [] (renameBindersTm env topx)

214226 (renameBindersTm env topy)) (UI 0 []) of

@@ -295,7 +307,7 @@ unify ctxt env topx topy inj holes from =

295307 | injective ty && not (holeIn env x || x `elem` holes)

296308 = unifyTmpFail tx ty

297309 un' fn bnames xtm@(P _ x _) tm

298− | holeIn env x || x `elem` holes

310+ | pureTerm tm, holeIn env x || x `elem` holes

299311 = do UI s f <- get

300312 -- injectivity check

301313 x <- checkCycle bnames (x, tm)

@@ -305,11 +317,11 @@ unify ctxt env topx topy inj holes from =

305317 then unifyTmpFail xtm tm

306318 else do sc 1

307319 return x

308− | not (injective xtm) && injective tm

320+ | pureTerm tm, not (injective xtm) && injective tm

309321 = do checkCycle bnames (x, tm)

310322 unifyTmpFail xtm tm

311323 un' fn bnames tm ytm@(P _ y _)

312− | holeIn env y || y `elem` holes

324+ | pureTerm tm, holeIn env y || y `elem` holes

313325 = do UI s f <- get

314326 -- injectivity check

315327 x <- checkCycle bnames (y, tm)

@@ -319,7 +331,7 @@ unify ctxt env topx topy inj holes from =

319331 then unifyTmpFail tm ytm

320332 else do sc 1

321333 return x

322− | not (injective ytm) && injective tm

334+ | pureTerm tm, not (injective ytm) && injective tm

323335 = do checkCycle bnames (y, tm)

324336 unifyTmpFail tm ytm

325337 un' fn bnames (V i) (P _ x _)

@@ -524,7 +536,7 @@ unify ctxt env topx topy inj holes from =

524536 | not (x `elem` freeNames tm) = checkScope ns (x, tm)

525537 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))

526538

527− checkScope ns (x, tm) =

539+ checkScope ns (x, tm) | pureTerm tm =

528540-- case boundVs (envPos x 0 env) tm of

529541-- [] -> return [(x, tm)]

530542-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))

@@ -535,6 +547,7 @@ unify ctxt env topx topy inj holes from =

535547 else return [(x, bind v ns tm)]

536548 where inst [] tm = tm

537549 inst (((n, _), _) : ns) tm = inst ns (substV (P Bound n Erased) tm)

550+ checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")

538551

539552 bind i ns tm

540553 | i < 0 = tm

src/Idris/Coverage.hs+12−7

@@ -9,7 +9,7 @@ import Idris.Core.CaseTree

99import Idris.AbsSyntax

1010import Idris.Delaborate

1111import Idris.Error

12−import Idris.Output (iWarn)

12+import Idris.Output (iWarn, iputStrLn)

1313

1414import Data.List

1515import Data.Either

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

255255 case lookupTotal n (tt_ctxt i) of

256256 [tot@(Partial NotCovering)] ->

257257 do let msg = show top ++ " is " ++ show tot ++ " due to " ++ show n

258− addIBC (IBCTotCheckErr fc msg)

259258 putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i }

260− _ -> return ()

261− case lookupCtxt n (idris_callgraph i) of

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

263− (map fst (calls cg))

264− _ -> return ()

259+ addIBC (IBCTotCheckErr fc msg)

260+ [Partial _] ->

261+ case lookupCtxt n (idris_callgraph i) of

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

263+ (map fst (calls cg))

264+ _ -> return ()

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

265266checkAllCovering _ _ _ _ = return ()

266267

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

@@ -415,6 +416,10 @@ checkDeclTotality (fc, n)

415416-- buildSCG (fc, n)

416417-- logLvl 2 $ "Built SCG"

417418 i <- getIState

419+ let opts = case lookupCtxt n (idris_flags i) of

420+ [fs] -> fs

421+ _ -> []

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

418423 t <- checkTotality [] fc n

419424 case t of

420425 -- if it's not total, it can't reduce, to keep

src/Idris/ElabDecls.hs+9−8

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

11951195 force (normalisePats ctxt [] y))

11961196 simple_lhs ctxt t = t

11971197

1198− simple_rt ctxt (p, x, y) = (p, x, force (rt_simplify ctxt [] y))

1198+ simple_rt ctxt (p, x, y) = (p, x, force (uniqueBinders p

1199+ (rt_simplify ctxt [] y)))

11991200

12001201 -- this is so pattern types are in the right form for erasure

12011202 normalisePats ctxt env (Bind n (PVar t) sc)

@@ -2088,19 +2089,19 @@ elabInstance info syn what fc cs n ps t expn ds = do

20882089

20892090 -- Bring variables in instance head into scope

20902091 ist <- getIState

2091− let headVars = mapMaybe (\p -> case p of

2092− PRef _ n ->

2093− case lookupTy n (tt_ctxt ist) of

2094− [] -> Just n

2095− _ -> Nothing

2096− _ -> Nothing) ps

2092+ let headVars = nub $ mapMaybe (\p -> case p of

2093+ PRef _ n ->

2094+ case lookupTy n (tt_ctxt ist) of

2095+ [] -> Just n

2096+ _ -> Nothing

2097+ _ -> Nothing) ps

20972098-- let lhs = PRef fc iname

20982099 let lhs = PApp fc (PRef fc iname)

20992100 (map (\n -> pimp n (PRef fc n) True) headVars)

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

21012102 (map (pexp . mkMethApp) mtys)

21022103

2103− logLvl 5 $ "Instance LHS " ++ show lhs

2104+ logLvl 5 $ "Instance LHS " ++ show lhs ++ " " ++ show headVars

21042105 logLvl 5 $ "Instance RHS " ++ show rhs

21052106

21062107 let idecls = [PClauses fc [Dictionary] iname

src/Idris/ElabTerm.hs+10−5

@@ -70,11 +70,13 @@ build ist info pattern opts fn tm

7070 when (not pattern) $

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

7272 do unify_all; matchProblems True; unifyProblems

73+

7374 probs <- get_probs

7475 case probs of

7576 [] -> return ()

76− ((_,_,_,e,_,_):es) -> if inf then return ()

77− else lift (Error e)

77+ ((_,_,_,e,_,_):es) -> traceWhen u ("Final problems:\n" ++ show probs) $

78+ if inf then return ()

79+ else lift (Error e)

7880 is <- getAux

7981 tt <- get_term

8082 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

@@ -495,6 +497,7 @@ elab ist info pattern opts fn tm

495497 where alt t = case getTm t of

496498 PAlternative False _ -> 5

497499 PAlternative True _ -> 1

500+ PTactics _ -> 150

498501 PLam _ _ _ -> 2

499502 PRewrite _ _ _ _ -> 3

500503 _ -> 0

@@ -822,9 +825,9 @@ findInstances ist t

822825trivial' ist

823826 = trivial (elab ist toplevel False [] (sMN 0 "tac")) ist

824827proofSearch' ist rec depth prv top n hints

825− = proofSearch rec prv depth

826− (elab ist toplevel False [] (sMN 0 "tac")) top n hints ist

827−

828+ = do unifyProblems

829+ proofSearch rec prv depth

830+ (elab ist toplevel False [] (sMN 0 "tac")) top n hints ist

828831

829832resolveTC :: Int -> Term -> Name -> IState -> ElabD ()

830833resolveTC = resTC' []

@@ -1632,6 +1635,8 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

16321635 then handle err

16331636 else applyHandlers err hs

16341637 return (ElaboratingArg f a prev err')

1638+ -- ProofSearchFail is an internal detail - so don't expose it

1639+ handle (ProofSearchFail e) = handle e

16351640 -- TODO: argument-specific error handlers go here for ElaboratingArg

16361641 handle e = do ist <- getIState

16371642 logLvl 2 "Starting error reflection"

src/Idris/Erasure.hs+18−10

@@ -294,7 +294,6 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

294294 -- that the result of this function is used at all

295295 = addTagDep $ unionMap (getDepsAlt fn es vs casedVar) alts -- coming from the whole subtree

296296 where

297−

298297 addTagDep = case alts of

299298 [_] -> id -- single branch, tag not used

300299 _ -> M.insertWith (M.unionWith S.union) (S.singleton (fn, Result)) (viDeps casedVar)

@@ -329,11 +328,15 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

329328 | otherwise = \j -> Nothing

330329

331330 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps

332− getDepsTerm :: Vars -> [Cond -> Deps] -> Cond -> Term -> Deps

331+ getDepsTerm :: Vars -> [(Name, Cond -> Deps)] -> Cond -> Term -> Deps

333332

334333 -- named variables introduce dependencies as described in `vs'

335334 getDepsTerm vs bs cd (P _ n _)

336− -- local variables

335+ -- de bruijns (lambda-bound, let-bound vars)

336+ | Just deps <- lookup n bs

337+ = deps cd

338+

339+ -- ctor-bound/arg-bound variables

337340 | Just var <- M.lookup n vs

338341 = M.singleton cd (viDeps var)

339342

@@ -348,18 +351,18 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

348351 specialMNs = map (sMN 0 . ("__" ++)) $ words "Unit True False II"

349352

350353 -- dependencies of de bruijn variables are described in `bs'

351− getDepsTerm vs bs cd (V i) = (bs !! i) cd

354+ getDepsTerm vs bs cd (V i) = snd (bs !! i) cd

352355

353356 getDepsTerm vs bs cd (Bind n bdr t)

354357 -- here we just push IM.empty on the de bruijn stack

355358 -- the args will be marked as used at the usage site

356− | Lam ty <- bdr = getDepsTerm vs (const M.empty : bs) cd t

357− | Pi ty <- bdr = getDepsTerm vs (const M.empty : bs) cd t

359+ | Lam ty <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd t

360+ | Pi ty <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd t

358361

359362 -- let-bound variables can get partially evaluated

360363 -- it is sufficient just to plug the Cond in when the bound names are used

361− | Let ty t <- bdr = getDepsTerm vs (var t : bs) cd t

362− | NLet ty t <- bdr = getDepsTerm vs (var t : bs) cd t

364+ | Let ty t <- bdr = getDepsTerm vs ((n, var t) : bs) cd t

365+ | NLet ty t <- bdr = getDepsTerm vs ((n, var t) : bs) cd t

363366 where

364367 var t cd = getDepsTerm vs bs cd t

365368

@@ -386,6 +389,10 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

386389 -- a bound variable might draw in additional dependencies,

387390 -- think: f x = x 0 <-- here, `x' _is_ used

388391 P _ n _

392+ -- debruijn-bound name

393+ | Just deps <- lookup n bs

394+ -> deps cd `union` unconditionalDeps args

395+

389396 -- local name that refers to a method

390397 | Just var <- M.lookup n vs

391398 , Just meth <- viMethod var

@@ -402,7 +409,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

402409 -> conditionalDeps n args

403410

404411 -- TODO: could we somehow infer how bound variables use their arguments?

405− V i -> M.unionWith (M.unionWith S.union) ((bs !! i) cd) (unconditionalDeps args)

412+ V i -> snd (bs !! i) cd `union` unconditionalDeps args

406413

407414 -- we interpret applied lambdas as lets in order to reuse code here

408415 Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)

@@ -418,6 +425,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

418425

419426 _ -> error $ "cannot analyse application of " ++ show fun ++ " to " ++ show args

420427 where

428+ union = M.unionWith $ M.unionWith S.union

421429 ins = M.insertWith (M.unionWith S.union) cd

422430

423431 unconditionalDeps :: [Term] -> Deps

@@ -441,7 +449,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

441449 , viMethod = Nothing

442450 }) | (v, i) <- zip args [0..]]

443451 deps i = M.singleton (metameth, Arg i) S.empty

444− bruijns = reverse [\cd -> M.singleton cd (deps i) | i <- [0 .. length args - 1]]

452+ bruijns = reverse [(n, \cd -> M.singleton cd (deps i)) | (i, n) <- zip [0..] args]

445453 cond = S.singleton (metameth, Result)

446454 metameth = mkFieldName ctorName methNo

447455 (args, body) = unfoldLams t

src/Idris/Error.hs+4−2

@@ -43,11 +43,13 @@ idrisCatch = catchError

4343setAndReport :: Err -> Idris ()

4444setAndReport e = do ist <- getIState

4545 let h = idris_outh ist

46− case e of

46+ case (unwrap e) of

4747 At fc e -> do setErrSpan fc

4848 ihWarn h fc $ pprintErr ist e

4949 _ -> do setErrSpan (getErrSpan e)

50− ihputStrLn h $ pshow ist e

50+ ihWarn h emptyFC $ pprintErr ist e

51+ where unwrap (ProofSearchFail e) = e -- remove bookkeeping constructor

52+ unwrap e = e

5153

5254ifail :: String -> Idris a

5355ifail = throwError . Msg

src/Idris/Primitives.hs+6−5

@@ -28,9 +28,10 @@ ty :: [Const] -> Const -> Type

2828ty [] x = Constant x

2929ty (t:ts) x = Bind (sMN 0 "T") (Pi (Constant t)) (ty ts x)

3030

31−total, partial :: Totality

31+total, partial, iopartial :: Totality

3232total = Total []

3333partial = Partial NotCovering

34+iopartial = Partial ExternalIO

3435

3536primitives :: [Prim]

3637primitives =

@@ -164,16 +165,16 @@ primitives =

164165 Prim (sUN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

165166 (1, LStrRev) total,

166167 Prim (sUN "prim__readString") (ty [PtrType] StrType) 1 (p_cantreduce)

167− (1, LReadStr) partial,

168+ (1, LReadStr) iopartial,

168169 Prim (sUN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)

169170 (0, LVMPtr) total,

170171 -- Streams

171172 Prim (sUN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

172− (0, LStdIn) partial,

173+ (0, LStdIn) iopartial,

173174 Prim (sUN "prim__stdout") (ty [] PtrType) 0 (p_cantreduce)

174− (0, LStdOut) partial,

175+ (0, LStdOut) iopartial,

175176 Prim (sUN "prim__stderr") (ty [] PtrType) 0 (p_cantreduce)

176− (0, LStdErr) partial,

177+ (0, LStdErr) iopartial,

177178 Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)

178179 (0, LNullPtr) total,

179180 -- Managed pointer registration

src/Idris/REPL.hs+1−1

@@ -849,7 +849,7 @@ process h fn (Missing n)

849849 = do i <- getIState

850850 let i' = i { idris_options = (idris_options i) { opt_showimp = True } }

851851 case lookupCtxt n (idris_patdefs i) of

852− [] -> return ()

852+ [] -> ihPrintError h $ "Unknown operator " ++ show n

853853 [(_, tms)] ->

854854 iPrintResult (showSep "\n" (map (showTm i') tms))

855855 _ -> iPrintError $ "Ambiguous name"

test/basic006/expected+2−2

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

1−When elaborating right hand side of foo:

2−test020a.idr:14:18:When elaborating an application of function Prelude.List.reverse:

1+test020a.idr:14:18:When elaborating right hand side of foo:

2+When elaborating an application of function Prelude.List.reverse:

33 Can't unify

44 Vect n a

55 with