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

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

compare with master

unifiedsplit

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

27EXCEPTION t = MkEff () (Exception t)

28

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

30−raise err = Raise err

30+raise err = effect $ 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 = Open f m

110+open f m = effect $ Open f m

111

112

113||| Close a file.

114close : Handler FileIO e =>

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

116−close = Close

116+close = effect $ Close

117

118||| Read a line from the file.

119readLine : Handler FileIO e =>

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

121−readLine = ReadLine

121+readLine = effect $ ReadLine

122

123||| Write a line to a file.

124writeLine : Handler FileIO e =>

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

126−writeLine str = WriteLine str

126+writeLine str = effect $ WriteLine str

127

128||| End of file?

129eof : Handler FileIO e =>

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

131−eof = EOF

131+eof = effect $ 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 = Allocate size

105+allocate size = effect $ 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 = Initialize c size prf

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

115

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

117−free = Free

117+free = effect 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 = Peek offset size prf

124+peek offset size prf = effect $ 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 = Poke offset content prf

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

134

135private

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

137−getRawPtr = GetRawPtr

137+getRawPtr = effect $ 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− = 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

153

154data MoveDescriptor = Dst | Src

155

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

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

9using (m : Type -> Type)

10 instance Handler Random m where

11 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

13 k seed' seed'

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

15

@@ -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 <- getRandom

21+rndInt lower upper = do v <- effect $ 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 = !getRandom `prim__sremBigInt` (cast (S k))

28+rndFin k = do let v = assert_total $ !(effect 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 = setSeed n

46+srand n = effect $ 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 = Select xs

22+select xs = effect $ 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 = Get

20+get = effect $ Get

21

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

23−put val = Put val

23+put val = effect $ Put val

24

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

26−putM val = Put val

26+putM val = effect $ 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 = PutStr s

43+putStr s = effect $ PutStr s

44

45||| Write a character to standard output.

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

47−putChar c = PutCh c

47+putChar c = effect $ 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 = GetStr

55+getStr = effect $ GetStr

56

57||| Read a character from standard input.

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

59−getChar = GetCh

59+getChar = effect $ 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 = Args

31+getArgs = effect Args

32

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

34−time = Time

34+time = effect Time

35

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

37−getEnv s = GetEnv s

37+getEnv s = effect $ GetEnv s

38

libs/effects/Effects.idr+19−19

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

31 |||

32 ||| @ r The resource being handled.

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

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

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

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

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

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

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

37

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

39resourceType : EFFECT -> Type

@@ -144,11 +144,11 @@ 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− effect : (prf : EffElem e a xs) ->

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

148 (eff : e t a b) ->

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

150

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

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

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

153 newInit : Handler e m =>

154 res ->

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

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

205eff env (prog `ebind` c) k

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

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

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

208−eff env (lift prf effP) k

208+eff env (liftP prf effP) k

209 = let env' = dropEnv env prf in

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

211eff env (newInit r prog) k

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

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

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

235

236−implicit

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

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

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

238− {default tactics { search 100; }

238+ {default tactics { search 100; }

239− prf : SubList ys xs} ->

239+ prf : EffElem e a xs} ->

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

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

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

241+effect e {prf} = effectP prf e

242

243implicit

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

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

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

246− {default tactics { search 100; }

245+ {default tactics { search 100; }

247− prf : EffElem e a xs} ->

246+ prf : SubList ys xs} ->

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

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

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

248+lift e {prf} = liftP prf e

249+

250

251new : Handler e m =>

252 {default default r : res} ->

src/IRTS/Simplified.hs+16−14

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

125 return xs'

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

127 = 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)

129 xs' <- checkDefs ctxt xs

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

131

132lvar v = do i <- get

133 put (max i v)

134

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

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

136−scopecheck ctxt envTop tm = sc envTop tm where

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

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

138+

137 sc env (SV (Glob n)) =

139 sc env (SV (Glob n)) =

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

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

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

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

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

141 Just (DConstructor _ i ar) ->

143 Just (DConstructor _ i ar) ->

142 if True -- ar == 0

144 if True -- ar == 0

143 then return (SCon i n [])

145 then return (SCon i n [])

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

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

145 " has arity " ++ show ar

147 " has arity " ++ show ar

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

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

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

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

148 sc env (SApp tc f args)

150 sc env (SApp tc f args)

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

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

150 case lookupCtxtExact f ctxt of

152 case lookupCtxtExact f ctxt of

151 Just (DConstructor n tag ar) ->

153 Just (DConstructor n tag ar) ->

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

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

153 then return $ SCon tag n args'

155 then return $ SCon tag n args'

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

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

155 " has arity " ++ show ar

157 " has arity " ++ show ar

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

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

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

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

158 sc env (SForeign l ty f args)

160 sc env (SForeign l ty f args)

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

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

160 return (t, a')) args

162 return (t, a')) args

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

165 Just (DConstructor n tag ar) ->

167 Just (DConstructor n tag ar) ->

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

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

167 then return $ SCon tag n args'

169 then return $ SCon tag n args'

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

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

169− " has arity " ++ show ar

171+ " has arity " ++ show ar

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

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

171 sc env (SProj e i)

173 sc env (SProj e i)

172 = do e' <- scVar env e

174 = do e' <- scVar env e

173 return (SProj e' i)

175 return (SProj e' i)

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

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

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

201 Nothing -> case lookupCtxtExact n ctxt of

203 Nothing -> case lookupCtxtExact n ctxt of

202 Just (DConstructor _ i ar) ->

204 Just (DConstructor _ i ar) ->

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

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

204 Just _ -> return (Glob n)

206 Just _ -> return (Glob n)

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

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

206 " in " ++ show tm ++ " " ++ show envTop

208 " in " ++ show tm ++ " " ++ show envTop

207 scVar _ x = return x

209 scVar _ x = return x

208

210

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

212 Just (DConstructor _ i ar) ->

214 Just (DConstructor _ i ar) ->

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

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

214 then return i

216 then return i

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

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

216 " has arity " ++ show ar

218 " has arity " ++ show ar

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

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

218 e' <- sc env' e

220 e' <- sc env' e

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

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

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

222 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

1338 prettySe p bnd PImpossible = kwd "impossible"

1339 prettySe p bnd Placeholder = text "_"

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

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

1341 prettySe p bnd (PElabError s) = pretty s

1342 prettySe p bnd (PElabError s) = pretty s

1342

1343

1343 prettySe p bnd _ = text "test"

1344 prettySe p bnd _ = text "test"

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

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

695 = -- traceWhen r (show err) $

696 r || proofSearch

697 recoverableErr (CantSolveGoal _ _) = False

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

698 recoverableErr (ProofSearchFail _) = False

699 recoverableErr (ProofSearchFail _) = False

699 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

700 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

700 recoverableErr (At _ e) = recoverableErr e

701 recoverableErr (At _ e) = recoverableErr e

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

724 = do s <- get

725 = do s <- get

725 ps <- get_probs

726 ps <- get_probs

726 case prunStateT pmax True ps x s of

727 case prunStateT pmax True ps x s of

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

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

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

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

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

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

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

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

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

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

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

538

539convEq :: 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

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

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

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

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

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

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

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

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

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

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

555+ | otherwise = return False

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

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

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

558+ | otherwise = return False

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

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

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

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

557 where

561 where

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

678

682

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

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

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

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

681− | BelieveMe | Mutual [Name] | NotProductive

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

682 deriving (Show, Eq)

686 deriving (Show, Eq)

683

687

684instance Show Totality where

688instance Show Totality where

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

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

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

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

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

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

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

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

691 show (Partial NotProductive) = "not productive"

696 show (Partial NotProductive) = "not productive"

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

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

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

698 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

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

790 | Just v <- lookup n xs

791 = case xs of

792− [_] -> psubst n v t

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

793+ -- explicit names

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

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

794updateSolved' xs (Bind n b t)

795updateSolved' xs (Bind n b t)

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

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

796updateSolved' xs (App f a)

797updateSolved' xs (App f a)

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

838 y' = updateSolved ns y

839 y' = updateSolved ns y

839 err' = updateError ns err

840 err' = updateError ns err

840 env' = updateEnv ns env in

841 env' = updateEnv ns env in

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

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

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

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

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

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

844 up (ns ++ v) ps

845 up (ns ++ v) ps

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

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

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

185score (CantResolve _) = 20

186score (NoSuchVariable _) = 1000

187−score (ProofSearchFail _) = 10000

187+score (ProofSearchFail e) = score e

188−score (CantSolveGoal _ _) = 10000

188+score (CantSolveGoal _ _) = 100000

189score (InternalMsg _) = -1

190+score (At _ e) = score e

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

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

190score _ = 0

193score _ = 0

191

194

192instance Show Err where

195instance Show Err where

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

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

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

204 show x ++ ": " ++ show e

207 show x ++ ": " ++ show e

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

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

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

206 show _ = "Error"

210 show _ = "Error"

207

211

208instance Pretty Err OutputAnnotation where

212instance Pretty Err OutputAnnotation where

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

1056

1060

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

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

1058uniqueBinders ns (Bind n b sc)

1062uniqueBinders ns (Bind n b sc)

1059− = let n' = uniqueName n ns in

1063+ = let n' = uniqueName n ns

1064+ ns' = n' : ns in

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

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

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

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

1062uniqueBinders ns t = t

1067uniqueBinders ns t = t

1063

1068

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

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

85 | length bnames > i,

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

87 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

89 = do h1 <- uB bnames bx by

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

91 combine bnames h1 h2

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

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

120 return []

121

122+ notHole (Hole _) = False

123+ notHole _ = True

124+

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

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

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

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

124

127

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

173 uniqueBinders env (Bind n b sc)

176 uniqueBinders env (Bind n b sc)

174 | n `elem` env

177 | n `elem` env

175 = let n' = uniqueName n env in

178 = let n' = uniqueName n env in

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

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

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

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

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

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

179 (uniqueBinders (n:env) sc)

182 (uniqueBinders (n:env) sc)

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

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

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

186 rename n n' t = t

189 rename n n' t = t

187

190

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

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

193+ explicitHole t = t

194+

188trimSolutions ns = dropPairs ns

195trimSolutions ns = dropPairs ns

189 where dropPairs [] = []

196 where dropPairs [] = []

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

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

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

204 doSubst (_ : env) tm

211 doSubst (_ : env) tm

205 = doSubst env tm

212 = doSubst env tm

206

213

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

207

218

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

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

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

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

210unify ctxt env topx topy inj holes from =

221unify ctxt env topx topy inj holes from =

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

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

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

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

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

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

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

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

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

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

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

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

296 = unifyTmpFail tx ty

308 = unifyTmpFail tx ty

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

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

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

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

299 = do UI s f <- get

311 = do UI s f <- get

300 -- injectivity check

312 -- injectivity check

301 x <- checkCycle bnames (x, tm)

313 x <- checkCycle bnames (x, tm)

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

305 then unifyTmpFail xtm tm

317 then unifyTmpFail xtm tm

306 else do sc 1

318 else do sc 1

307 return x

319 return x

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

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

309 = do checkCycle bnames (x, tm)

321 = do checkCycle bnames (x, tm)

310 unifyTmpFail xtm tm

322 unifyTmpFail xtm tm

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

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

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

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

313 = do UI s f <- get

325 = do UI s f <- get

314 -- injectivity check

326 -- injectivity check

315 x <- checkCycle bnames (y, tm)

327 x <- checkCycle bnames (y, tm)

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

319 then unifyTmpFail tm ytm

331 then unifyTmpFail tm ytm

320 else do sc 1

332 else do sc 1

321 return x

333 return x

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

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

323 = do checkCycle bnames (y, tm)

335 = do checkCycle bnames (y, tm)

324 unifyTmpFail tm ytm

336 unifyTmpFail tm ytm

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

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

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

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

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

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

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

526

538

527− checkScope ns (x, tm) =

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

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

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

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

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

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

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

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

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

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

536 where inst [] tm = tm

548 where inst [] tm = tm

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

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

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

538

551

539 bind i ns tm

552 bind i ns tm

540 | i < 0 = tm

553 | i < 0 = tm

src/Idris/Coverage.hs+12−7

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

9import Idris.AbsSyntax

10import Idris.Delaborate

11import Idris.Error

12−import Idris.Output (iWarn)

12+import Idris.Output (iWarn, iputStrLn)

13

14import Data.List

15import Data.Either

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

255 case lookupTotal n (tt_ctxt i) of

256 [tot@(Partial NotCovering)] ->

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

258− addIBC (IBCTotCheckErr fc msg)

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

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

260− _ -> return ()

259+ addIBC (IBCTotCheckErr fc msg)

260+ [Partial _] ->

261− case lookupCtxt n (idris_callgraph i) of

261+ case lookupCtxt n (idris_callgraph i) of

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

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

263− (map fst (calls cg))

263+ (map fst (calls cg))

264+ _ -> return ()

264− _ -> return ()

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

265checkAllCovering _ _ _ _ = return ()

266checkAllCovering _ _ _ _ = return ()

266

267

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

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

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

415-- buildSCG (fc, n)

416-- buildSCG (fc, n)

416-- logLvl 2 $ "Built SCG"

417-- logLvl 2 $ "Built SCG"

417 i <- getIState

418 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

418 t <- checkTotality [] fc n

423 t <- checkTotality [] fc n

419 case t of

424 case t of

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

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

1195 force (normalisePats ctxt [] y))

1196 simple_lhs ctxt t = t

1197

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

1199

1200

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

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

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

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

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

2088

2089

2089 -- Bring variables in instance head into scope

2090 -- Bring variables in instance head into scope

2090 ist <- getIState

2091 ist <- getIState

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

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

2092− PRef _ n ->

2093+ PRef _ n ->

2093− case lookupTy n (tt_ctxt ist) of

2094+ case lookupTy n (tt_ctxt ist) of

2094− [] -> Just n

2095+ [] -> Just n

2095− _ -> Nothing

2096+ _ -> Nothing

2096− _ -> Nothing) ps

2097+ _ -> Nothing) ps

2097-- let lhs = PRef fc iname

2098-- let lhs = PRef fc iname

2098 let lhs = PApp fc (PRef fc iname)

2099 let lhs = PApp fc (PRef fc iname)

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

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

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

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

2101 (map (pexp . mkMethApp) mtys)

2102 (map (pexp . mkMethApp) mtys)

2102

2103

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

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

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

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

2105

2106

2106 let idecls = [PClauses fc [Dictionary] iname

2107 let idecls = [PClauses fc [Dictionary] iname

src/Idris/ElabTerm.hs+10−5

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

70 when (not pattern) $

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

72 do unify_all; matchProblems True; unifyProblems

73+

73 probs <- get_probs

74 probs <- get_probs

74 case probs of

75 case probs of

75 [] -> return ()

76 [] -> return ()

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

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

78+ if inf then return ()

77− else lift (Error e)

79+ else lift (Error e)

78 is <- getAux

80 is <- getAux

79 tt <- get_term

81 tt <- get_term

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

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

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

495 where alt t = case getTm t of

497 where alt t = case getTm t of

496 PAlternative False _ -> 5

498 PAlternative False _ -> 5

497 PAlternative True _ -> 1

499 PAlternative True _ -> 1

500+ PTactics _ -> 150

498 PLam _ _ _ -> 2

501 PLam _ _ _ -> 2

499 PRewrite _ _ _ _ -> 3

502 PRewrite _ _ _ _ -> 3

500 _ -> 0

503 _ -> 0

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

822trivial' ist

825trivial' ist

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

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

824proofSearch' ist rec depth prv top n hints

827proofSearch' ist rec depth prv top n hints

828+ = do unifyProblems

825− = proofSearch rec prv depth

829+ proofSearch rec prv depth

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

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

827−

828

831

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

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

830resolveTC = resTC' []

833resolveTC = resTC' []

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

1632 then handle err

1635 then handle err

1633 else applyHandlers err hs

1636 else applyHandlers err hs

1634 return (ElaboratingArg f a prev err')

1637 return (ElaboratingArg f a prev err')

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

1639+ handle (ProofSearchFail e) = handle e

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

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

1636 handle e = do ist <- getIState

1641 handle e = do ist <- getIState

1637 logLvl 2 "Starting error reflection"

1642 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]

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

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

296 where

297−

298 addTagDep = case alts of

297 addTagDep = case alts of

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

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

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

299 _ -> 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]

329 | otherwise = \j -> Nothing

328 | otherwise = \j -> Nothing

330

329

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

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

333

332

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

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

335 getDepsTerm vs bs cd (P _ n _)

334 getDepsTerm vs bs cd (P _ n _)

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

336+ | Just deps <- lookup n bs

337+ = deps cd

338+

336− -- local variables

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

337 | Just var <- M.lookup n vs

340 | Just var <- M.lookup n vs

338 = M.singleton cd (viDeps var)

341 = M.singleton cd (viDeps var)

339

342

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

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

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

349

352

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

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

352

355

353 getDepsTerm vs bs cd (Bind n bdr t)

356 getDepsTerm vs bs cd (Bind n bdr t)

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

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

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

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

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

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

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

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

358

361

359 -- let-bound variables can get partially evaluated

362 -- let-bound variables can get partially evaluated

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

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

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

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

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

363 where

366 where

364 var t cd = getDepsTerm vs bs cd t

367 var t cd = getDepsTerm vs bs cd t

365

368

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

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

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

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

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

388 P _ n _

391 P _ n _

392+ -- debruijn-bound name

393+ | Just deps <- lookup n bs

394+ -> deps cd `union` unconditionalDeps args

395+

389 -- local name that refers to a method

396 -- local name that refers to a method

390 | Just var <- M.lookup n vs

397 | Just var <- M.lookup n vs

391 , Just meth <- viMethod var

398 , Just meth <- viMethod var

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

402 -> conditionalDeps n args

409 -> conditionalDeps n args

403

410

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

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

406

413

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

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

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

415 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]

418

425

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

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

420 where

427 where

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

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

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

422

430

423 unconditionalDeps :: [Term] -> Deps

431 unconditionalDeps :: [Term] -> Deps

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

441 , viMethod = Nothing

449 , viMethod = Nothing

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

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

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

451 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]

445 cond = S.singleton (metameth, Result)

453 cond = S.singleton (metameth, Result)

446 metameth = mkFieldName ctorName methNo

454 metameth = mkFieldName ctorName methNo

447 (args, body) = unfoldLams t

455 (args, body) = unfoldLams t

src/Idris/Error.hs+4−2

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

43setAndReport :: Err -> Idris ()

44setAndReport e = do ist <- getIState

45 let h = idris_outh ist

46− case e of

46+ case (unwrap e) of

47 At fc e -> do setErrSpan fc

48 ihWarn h fc $ pprintErr ist e

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

51

53

52ifail :: String -> Idris a

54ifail :: String -> Idris a

53ifail = throwError . Msg

55ifail = throwError . Msg

src/Idris/Primitives.hs+6−5

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

28ty [] x = Constant x

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

30

31−total, partial :: Totality

31+total, partial, iopartial :: Totality

32total = Total []

33partial = Partial NotCovering

34+iopartial = Partial ExternalIO

34

35

35primitives :: [Prim]

36primitives :: [Prim]

36primitives =

37primitives =

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

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

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

165 (1, LStrRev) total,

166 (1, LStrRev) total,

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

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

167− (1, LReadStr) partial,

168+ (1, LReadStr) iopartial,

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

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

169 (0, LVMPtr) total,

170 (0, LVMPtr) total,

170 -- Streams

171 -- Streams

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

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

172− (0, LStdIn) partial,

173+ (0, LStdIn) iopartial,

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

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

174− (0, LStdOut) partial,

175+ (0, LStdOut) iopartial,

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

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

176− (0, LStdErr) partial,

177+ (0, LStdErr) iopartial,

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

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

178 (0, LNullPtr) total,

179 (0, LNullPtr) total,

179 -- Managed pointer registration

180 -- Managed pointer registration

src/Idris/REPL.hs+1−1

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

849 = do i <- getIState

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

851 case lookupCtxt n (idris_patdefs i) of

852− [] -> return ()

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

853 [(_, tms)] ->

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

855 _ -> iPrintError $ "Ambiguous name"

test/basic006/expected+2−2

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

1−When elaborating right hand side of foo:

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

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

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

3 Can't unify

4 Vect n a

5 with