@@ -48,13 +48,13 @@ trivialHoles psnames ok elab ist
4848 then try' (elab (PRef (fileFC "prf") [] x))
4949 (tryAll xs) True
5050 else tryAll xs
51−
51+
5252 holesOK hs ap@(App _ _ _)
5353 | (P _ n _, args) <- unApply ap
5454 = holeArgsOK hs n 0 args
5555 holesOK hs (App _ f a) = holesOK hs f && holesOK hs a
5656 holesOK hs (P _ n _) = not (n `elem` hs)
57− holesOK hs (Bind n b sc) = holesOK hs (binderTy b) &&
57+ holesOK hs (Bind n b sc) = holesOK hs (binderTy b) &&
5858 holesOK hs sc
5959 holesOK hs _ = True
6060
@@ -85,8 +85,8 @@ trivialTCs ok elab ist
8585 then try' (elab (PRef (fileFC "prf") [] x))
8686 (tryAll xs) True
8787 else tryAll xs
88−
89− tcArg env ty
88+
89+ tcArg env ty
9090 | (P _ n _, args) <- unApply (getRetTy (normalise (tt_ctxt ist) env ty))
9191 = case lookupCtxtExact n (idris_classes ist) of
9292 Just _ -> True
@@ -98,7 +98,7 @@ trivialTCs ok elab ist
9898 = holeArgsOK hs n 0 args
9999 holesOK hs (App _ f a) = holesOK hs f && holesOK hs a
100100 holesOK hs (P _ n _) = not (n `elem` hs)
101− holesOK hs (Bind n b sc) = holesOK hs (binderTy b) &&
101+ holesOK hs (Bind n b sc) = holesOK hs (binderTy b) &&
102102 holesOK hs sc
103103 holesOK hs _ = True
104104
@@ -111,16 +111,16 @@ cantSolveGoal :: ElabD a
111111cantSolveGoal = do g <- goal
112112 env <- get_env
113113 lift $ tfail $
114− CantSolveGoal g (map (\(n,b) -> (n, binderTy b)) env)
114+ CantSolveGoal g (map (\(n,b) -> (n, binderTy b)) env)
115115
116−proofSearch :: Bool -> -- recursive search (False for 'refine')
116+proofSearch :: Bool -> -- recursive search (False for 'refine')
117117 Bool -> -- invoked from a tactic proof. If so, making
118118 -- new metavariables is meaningless, and there shoudl
119119 -- be an error reported instead.
120120 Bool -> -- ambiguity ok
121121 Bool -> -- defer on failure
122122 Int -> -- maximum depth
123− (PTerm -> ElabD ()) -> Maybe Name -> Name ->
123+ (PTerm -> ElabD ()) -> Maybe Name -> Name ->
124124 [Name] ->
125125 [Name] ->
126126 IState -> ElabD ()
@@ -131,7 +131,7 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot psnames [fn]
131131 tryAllFns all_imps
132132 where
133133 -- if nothing worked, make a new metavariable
134− tryAllFns [] | fromProver = cantSolveGoal
134+ tryAllFns [] | fromProver = cantSolveGoal
135135 tryAllFns [] = do attack; defer [] nroot; solve
136136 tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True
137137
@@ -142,20 +142,20 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot psnames [fn]
142142 (match_apply (Var f) imps) True
143143 ps' <- get_probs
144144-- when (length ps < length ps') $ fail "Can't apply constructor"
145− -- Make metavariables for new holes
145+ -- Make metavariables for new holes
146146 hs' <- get_holes
147147 ptm <- get_term
148148 if fromProver then cantSolveGoal
149149 else do
150150 mapM_ (\ h -> do focus h
151− attack; defer [] nroot; solve)
151+ attack; defer [] nroot; solve)
152152 (hs' \\ hs)
153153-- (filter (\ (x, y) -> not x) (zip (map fst imps) args))
154154 solve
155155
156156 isImp (PImp p _ _ _ _) = (True, p)
157157 isImp arg = (True, priority arg) -- try to get all of them by unification
158−proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hints ist
158+proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hints ist
159159 = do compute
160160 ty <- goal
161161 hs <- get_holes
@@ -172,7 +172,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
172172 (autoArg (sUN "auto"))
173173 else autoArg (sUN "auto") -- not enough info in the type yet
174174 where
175− findInferredTy (t : _) = elab (delab ist (toUN t))
175+ findInferredTy (t : _) = elab (delab ist (toUN t))
176176
177177 cantsolve (InternalMsg _) = True
178178 cantsolve (CantSolveGoal _ _) = True
@@ -185,12 +185,12 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
185185 conArgsOK ty
186186 = let (f, as) = unApply ty in
187187 case f of
188− P _ n _ ->
188+ P _ n _ ->
189189 let autohints = case lookupCtxtExact n (idris_autohints ist) of
190190 Nothing -> []
191191 Just hs -> hs in
192192 case lookupCtxtExact n (idris_datatypes ist) of
193− Just t -> do rs <- mapM (conReady as)
193+ Just t -> do rs <- mapM (conReady as)
194194 (autohints ++ con_names t)
195195 return (and rs)
196196 Nothing -> -- local variable, go for it
@@ -199,7 +199,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
199199 _ -> typeNotSearchable ty
200200
201201 conReady :: [Term] -> Name -> ElabD Bool
202− conReady as n
202+ conReady as n
203203 = case lookupTyExact n (tt_ctxt ist) of
204204 Just ty -> do let (_, cs) = unApply (getRetTy ty)
205205 -- if any metavariables in 'as' correspond to
@@ -223,7 +223,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
223223 inHS hs (P _ n _) = n `elem` hs
224224 isHS _ _ = False
225225
226− toUN t@(P nt (MN i n) ty)
226+ toUN t@(P nt (MN i n) ty)
227227 | ('_':xs) <- str n = t
228228 | otherwise = P nt (UN n) ty
229229 toUN (App s f a) = App s (toUN f) (toUN a)
@@ -239,7 +239,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
239239 psRec :: Bool -> Int -> [Name] -> S.Set Type -> ElabD ()
240240 psRec _ 0 locs tys | fromProver = cantSolveGoal
241241 psRec rec 0 locs tys = do attack; defer [] nroot; solve --fail "Maximum depth reached"
242− psRec False d locs tys = tryCons d locs tys hints
242+ psRec False d locs tys = tryCons d locs tys hints
243243 psRec True d locs tys
244244 = do compute
245245 ty <- goal
@@ -248,11 +248,11 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
248248 try' (try' (trivialHoles psnames [] elab ist)
249249 (resolveTC False False 20 ty nroot elab ist)
250250 True)
251− (try' (try' (resolveByCon (d - 1) locs tys')
251+ (try' (try' (resolveByCon (d - 1) locs tys')
252252 (resolveByLocals (d - 1) locs tys')
253253 True)
254254 -- if all else fails, make a new metavariable
255− (if fromProver
255+ (if fromProver
256256 then fail "cantSolveGoal"
257257 else do attack; defer [] nroot; solve) True) True
258258
@@ -269,7 +269,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
269269 = do t <- goal
270270 let (f, _) = unApply t
271271 case f of
272− P _ n _ ->
272+ P _ n _ ->
273273 do let autohints = case lookupCtxtExact n (idris_autohints ist) of
274274 Nothing -> []
275275 Just hs -> hs
@@ -292,26 +292,26 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
292292 tryLocals d locs tys env
293293
294294 tryLocals d locs tys [] = fail "Locals failed"
295− tryLocals d locs tys ((x, t) : xs)
295+ tryLocals d locs tys ((x, t) : xs)
296296 | x `elem` locs || x `notElem` psnames = tryLocals d locs tys xs
297− | otherwise = try' (tryLocal d (x : locs) tys x t)
297+ | otherwise = try' (tryLocal d (x : locs) tys x t)
298298 (tryLocals d locs tys xs) True
299299
300300 tryCons d locs tys [] = fail "Constructors failed"
301− tryCons d locs tys (c : cs)
301+ tryCons d locs tys (c : cs)
302302 = try' (tryCon d locs tys c) (tryCons d locs tys cs) True
303303
304− tryLocal d locs tys n t
304+ tryLocal d locs tys n t
305305 = do let a = getPArity (delab ist (binderTy t))
306306 tryLocalArg d locs tys n a
307307
308308 tryLocalArg d locs tys n 0 = elab (PRef (fileFC "prf") [] n)
309− tryLocalArg d locs tys n i
309+ tryLocalArg d locs tys n i
310310 = simple_app False (tryLocalArg d locs tys n (i - 1))
311311 (psRec True d locs tys) "proof search local apply"
312312
313313 -- Like type class resolution, but searching with constructors
314− tryCon d locs tys n =
314+ tryCon d locs tys n =
315315 do ty <- goal
316316 let imps = case lookupCtxtExact n (idris_implicits ist) of
317317 Nothing -> []
@@ -341,7 +341,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
341341 (Bind _ (Pi _ _ _) _) -> [TextPart "In particular, function types are not supported."]
342342 _ -> []
343343
344−-- In interactive mode, only search for things if there is some
344+-- In interactive mode, only search for things if there is some
345345-- index to help pick a relevant constructor
346346checkConstructor :: IState -> [Name] -> ElabD ()
347347checkConstructor ist [] = return ()
@@ -397,7 +397,7 @@ resTC' tcs defaultOn topholes depth topg fn elab ist
397397 _ -> []
398398
399399 traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $
400− try' (trivialTCs okholes elab ist)
400+ try' (trivialTCs okholes elab ist)
401401 (do addDefault t tc ttypes
402402 let stk = map fst (filter snd $ elab_stack ist)
403403 let insts = findInstances ist t
@@ -432,7 +432,7 @@ resTC' tcs defaultOn topholes depth topg fn elab ist
432432 tcDetArgsOK _ _ _ [] = Just []
433433
434434 isMeta :: [Name] -> Term -> Bool
435− isMeta ns (P _ n _) = n `elem` ns
435+ isMeta ns (P _ n _) = n `elem` ns
436436 isMeta _ _ = False
437437
438438 notHole hs (P _ n _, c)
@@ -449,7 +449,7 @@ resTC' tcs defaultOn topholes depth topg fn elab ist
449449 chaser (NS n _) = chaser n
450450 chaser _ = False
451451
452− numclass = sNS (sUN "Num") ["Classes","Prelude"]
452+ numclass = sNS (sUN "Num") ["Interfaces","Prelude"]
453453
454454 addDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn
455455 = do focus a
@@ -530,5 +530,3 @@ findInstances ist t
530530 where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of
531531 Just (_, Hidden) -> False
532532 _ -> True
533−
534−