git.iko.soy/Idris-dev
on 449089d help sign in
Idris-dev/src/Idris/ProofSearch.hs
517 lines 23 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.ProofSearch(trivial, trivialHoles, proofSearch, resolveTC) where
5import Idris.Core.Elaborate hiding (Tactic(..))
6import Idris.Core.TT
7import Idris.Core.Unify
8import Idris.Core.Evaluate
9import Idris.Core.CaseTree
10import Idris.Core.Typecheck
12import Idris.AbsSyntax
13import Idris.Delaborate
14import Idris.Error
16import Control.Applicative ((<$>))
17import Control.Monad
18import Control.Monad.State.Strict
19import qualified Data.Set as S
20import Data.List
21import Debug.Trace
23-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm
25trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()
26trivial = trivialHoles [] []
28trivialHoles :: [Name] -> -- user visible names, when working
29 -- in interactive mode
30 [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
31trivialHoles psnames ok elab ist
32 = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") [] eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])
33 return ())
34 (do env <- get_env
35 g <- goal
36 tryAll env
37 return ()) True
38 where
39 tryAll [] = fail "No trivial solution"
40 tryAll ((x, b):xs)
41 = do -- if type of x has any holes in it, move on
42 hs <- get_holes
43 let badhs = hs -- filter (flip notElem holesOK) hs
44 g <- goal
45 -- anywhere but the top is okay for a hole, if holesOK set
46 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))
47 (holesOK hs (binderTy b) && (null psnames || x `elem` psnames))
48 then try' (elab (PRef (fileFC "prf") [] x))
49 (tryAll xs) True
50 else tryAll xs
52 holesOK hs ap@(App _ _ _)
53 | (P _ n _, args) <- unApply ap
54 = holeArgsOK hs n 0 args
55 holesOK hs (App _ f a) = holesOK hs f && holesOK hs a
56 holesOK hs (P _ n _) = not (n `elem` hs)
57 holesOK hs (Bind n b sc) = holesOK hs (binderTy b) &&
58 holesOK hs sc
59 holesOK hs _ = True
61 holeArgsOK hs n p [] = True
62 holeArgsOK hs n p (a : as)
63 | (n, p) `elem` ok = holeArgsOK hs n (p + 1) as
64 | otherwise = holesOK hs a && holeArgsOK hs n (p + 1) as
66trivialTCs :: [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
67trivialTCs ok elab ist
68 = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") [] eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])
69 return ())
70 (do env <- get_env
71 g <- goal
72 tryAll env
73 return ()) True
74 where
75 tryAll [] = fail "No trivial solution"
76 tryAll ((x, b):xs)
77 = do -- if type of x has any holes in it, move on
78 hs <- get_holes
79 let badhs = hs -- filter (flip notElem holesOK) hs
80 g <- goal
81 env <- get_env
82 -- anywhere but the top is okay for a hole, if holesOK set
83 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))
84 (holesOK hs (binderTy b) && tcArg env (binderTy b))
85 then try' (elab (PRef (fileFC "prf") [] x))
86 (tryAll xs) True
87 else tryAll xs
89 tcArg env ty
90 | (P _ n _, args) <- unApply (getRetTy (normalise (tt_ctxt ist) env ty))
91 = case lookupCtxtExact n (idris_classes ist) of
92 Just _ -> True
93 _ -> False
94 | otherwise = False
96 holesOK hs ap@(App _ _ _)
97 | (P _ n _, args) <- unApply ap
98 = holeArgsOK hs n 0 args
99 holesOK hs (App _ f a) = holesOK hs f && holesOK hs a
100 holesOK hs (P _ n _) = not (n `elem` hs)
101 holesOK hs (Bind n b sc) = holesOK hs (binderTy b) &&
102 holesOK hs sc
103 holesOK hs _ = True
105 holeArgsOK hs n p [] = True
106 holeArgsOK hs n p (a : as)
107 | (n, p) `elem` ok = holeArgsOK hs n (p + 1) as
108 | otherwise = holesOK hs a && holeArgsOK hs n (p + 1) as
110cantSolveGoal :: ElabD a
111cantSolveGoal = do g <- goal
112 env <- get_env
113 lift $ tfail $
114 CantSolveGoal g (map (\(n,b) -> (n, binderTy b)) env)
116proofSearch :: Bool -> -- recursive search (False for 'refine')
117 Bool -> -- invoked from a tactic proof. If so, making
118 -- new metavariables is meaningless, and there shoudl
119 -- be an error reported instead.
120 Bool -> -- ambiguity ok
121 Bool -> -- defer on failure
122 Int -> -- maximum depth
123 (PTerm -> ElabD ()) -> Maybe Name -> Name ->
124 [Name] ->
125 [Name] ->
126 IState -> ElabD ()
127proofSearch False fromProver ambigok deferonfail depth elab _ nroot psnames [fn] ist
128 = do -- get all possible versions of the name, take the first one that
129 -- works
130 let all_imps = lookupCtxtName fn (idris_implicits ist)
131 tryAllFns all_imps
132 where
133 -- if nothing worked, make a new metavariable
134 tryAllFns [] | fromProver = cantSolveGoal
135 tryAllFns [] = do attack; defer [] nroot; solve
136 tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True
138 tryFn (f, args) = do let imps = map isImp args
139 ps <- get_probs
140 hs <- get_holes
141 args <- map snd <$> try' (apply (Var f) imps)
142 (match_apply (Var f) imps) True
143 ps' <- get_probs
144-- when (length ps < length ps') $ fail "Can't apply constructor"
145 -- Make metavariables for new holes
146 hs' <- get_holes
147 ptm <- get_term
148 if fromProver then cantSolveGoal
149 else do
150 mapM_ (\ h -> do focus h
151 attack; defer [] nroot; solve)
152 (hs' \\ hs)
153-- (filter (\ (x, y) -> not x) (zip (map fst imps) args))
154 solve
156 isImp (PImp p _ _ _ _) = (True, p)
157 isImp arg = (True, priority arg) -- try to get all of them by unification
158proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hints ist
159 = do compute
160 ty <- goal
161 hs <- get_holes
162 env <- get_env
163 tm <- get_term
164 argsok <- conArgsOK ty
165 if ambigok || argsok then
166 case lookupCtxt nroot (idris_tyinfodata ist) of
167 [TISolution ts] -> findInferredTy ts
168 _ -> if ambigok then psRec rec maxDepth [] S.empty
169 -- postpone if it fails early in elaboration
170 else handleError cantsolve
171 (psRec rec maxDepth [] S.empty)
172 (autoArg (sUN "auto"))
173 else autoArg (sUN "auto") -- not enough info in the type yet
174 where
175 findInferredTy (t : _) = elab (delab ist (toUN t))
177 cantsolve (InternalMsg _) = True
178 cantsolve (CantSolveGoal _ _) = True
179 cantsolve (IncompleteTerm _) = True
180 cantsolve (At _ e) = cantsolve e
181 cantsolve (Elaborating _ _ _ e) = cantsolve e
182 cantsolve (ElaboratingArg _ _ _ e) = cantsolve e
183 cantsolve err = False
185 conArgsOK ty
186 = let (f, as) = unApply ty in
187 case f of
188 P _ n _ ->
189 let autohints = case lookupCtxtExact n (idris_autohints ist) of
190 Nothing -> []
191 Just hs -> hs in
192 case lookupCtxtExact n (idris_datatypes ist) of
193 Just t -> do rs <- mapM (conReady as)
194 (autohints ++ con_names t)
195 return (and rs)
196 Nothing -> -- local variable, go for it
197 return True
198 TType _ -> return True
199 _ -> typeNotSearchable ty
201 conReady :: [Term] -> Name -> ElabD Bool
202 conReady as n
203 = case lookupTyExact n (tt_ctxt ist) of
204 Just ty -> do let (_, cs) = unApply (getRetTy ty)
205 -- if any metavariables in 'as' correspond to
206 -- a constructor form in 'cs', then we're not
207 -- ready to run auto yet. Otherwise, go for it
208 hs <- get_holes
209 return $ and (map (notHole hs) (zip as cs))
210 Nothing -> fail "Can't happen"
212 -- if n is a metavariable, and c is a constructor form, we're not ready
213 -- to run yet
214 notHole hs (P _ n _, c)
215 | (P _ cn _, _) <- unApply c,
216 n `elem` hs && isConName cn (tt_ctxt ist) = False
217 | Constant _ <- c = not (n `elem` hs)
218 -- if fa is a metavariable applied to anything, we're not ready to run yet.
219 notHole hs (fa, c)
220 | (P _ fn _, args@(_:_)) <- unApply fa = fn `notElem` hs
221 notHole _ _ = True
223 inHS hs (P _ n _) = n `elem` hs
224 isHS _ _ = False
226 toUN t@(P nt (MN i n) ty)
227 | ('_':xs) <- str n = t
228 | otherwise = P nt (UN n) ty
229 toUN (App s f a) = App s (toUN f) (toUN a)
230 toUN t = t
232 -- psRec counts depth and the local variable applications we're under
233 -- (so we don't try a pointless application of something to itself,
234 -- which obviously won't work anyway but might lead us on a wild
235 -- goose chase...)
236 -- Also keep track of the types we've proved so far in this branch
237 -- (if we get back to one we've been to before, we're just in a cycle and
238 -- that's no use)
239 psRec :: Bool -> Int -> [Name] -> S.Set Type -> ElabD ()
240 psRec _ 0 locs tys | fromProver = cantSolveGoal
241 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
243 psRec True d locs tys
244 = do compute
245 ty <- goal
246 when (S.member ty tys) $ fail "Been here before"
247 let tys' = S.insert ty tys
248 try' (try' (trivialHoles psnames [] elab ist)
249 (resolveTC False False 20 ty nroot elab ist)
250 True)
251 (try' (try' (resolveByCon (d - 1) locs tys')
252 (resolveByLocals (d - 1) locs tys')
253 True)
254 -- if all else fails, make a new metavariable
255 (if fromProver
256 then fail "cantSolveGoal"
257 else do attack; defer [] nroot; solve) True) True
259 -- get recursive function name. Only user given names make sense.
260 getFn d (Just f) | d < maxDepth-1 && usersname f = [f]
261 | otherwise = []
262 getFn d _ = []
264 usersname (UN _) = True
265 usersname (NS n _) = usersname n
266 usersname _ = False
268 resolveByCon d locs tys
269 = do t <- goal
270 let (f, _) = unApply t
271 case f of
272 P _ n _ ->
273 do let autohints = case lookupCtxtExact n (idris_autohints ist) of
274 Nothing -> []
275 Just hs -> hs
276 case lookupCtxtExact n (idris_datatypes ist) of
277 Just t -> do
278 let others = hints ++ con_names t ++ autohints
279 tryCons d locs tys (others ++ getFn d fn)
280 Nothing -> typeNotSearchable t
281 _ -> typeNotSearchable t
283 -- if there are local variables which have a function type, try
284 -- applying them too
285 resolveByLocals d locs tys
286 = do env <- get_env
287 tryLocals d locs tys env
289 tryLocals d locs tys [] = fail "Locals failed"
290 tryLocals d locs tys ((x, t) : xs)
291 | x `elem` locs || x `notElem` psnames = tryLocals d locs tys xs
292 | otherwise = try' (tryLocal d (x : locs) tys x t)
293 (tryLocals d locs tys xs) True
295 tryCons d locs tys [] = fail "Constructors failed"
296 tryCons d locs tys (c : cs)
297 = try' (tryCon d locs tys c) (tryCons d locs tys cs) True
299 tryLocal d locs tys n t
300 = do let a = getPArity (delab ist (binderTy t))
301 tryLocalArg d locs tys n a
303 tryLocalArg d locs tys n 0 = elab (PRef (fileFC "prf") [] n)
304 tryLocalArg d locs tys n i
305 = simple_app False (tryLocalArg d locs tys n (i - 1))
306 (psRec True d locs tys) "proof search local apply"
308 -- Like type class resolution, but searching with constructors
309 tryCon d locs tys n =
310 do ty <- goal
311 let imps = case lookupCtxtExact n (idris_implicits ist) of
312 Nothing -> []
313 Just args -> map isImp args
314 ps <- get_probs
315 hs <- get_holes
316 args <- map snd <$> try' (apply (Var n) imps)
317 (match_apply (Var n) imps) True
318 ps' <- get_probs
319 hs' <- get_holes
320 when (length ps < length ps') $ fail "Can't apply constructor"
321 let newhs = filter (\ (x, y) -> not x) (zip (map fst imps) args)
322 mapM_ (\ (_, h) -> do focus h
323 aty <- goal
324 psRec True d locs tys) newhs
325 solve
327 isImp (PImp p _ _ _ _) = (True, p)
328 isImp arg = (False, priority arg)
330 typeNotSearchable ty =
331 lift $ tfail $ FancyMsg $
332 [TextPart "Attempted to find an element of type",
333 TermPart ty,
334 TextPart "using proof search, but proof search only works on datatypes with constructors."] ++
335 case ty of
336 (Bind _ (Pi _ _ _) _) -> [TextPart "In particular, function types are not supported."]
337 _ -> []
339-- | Resolve type classes. This will only pick up 'normal' instances, never
340-- named instances (which is enforced by 'findInstances').
341resolveTC :: Bool -- ^ using default Int
342 -> Bool -- ^ allow metavariables in the goal
343 -> Int -- ^ depth
344 -> Term -- ^ top level goal, for error messages
345 -> Name -- ^ top level function name, to prevent loops
346 -> (PTerm -> ElabD ()) -- ^ top level elaborator
347 -> IState -> ElabD ()
348resolveTC def mvok depth top fn elab ist
349 = do hs <- get_holes
350 resTC' [] def hs depth top fn elab ist
352resTC' tcs def topholes 0 topg fn elab ist = fail $ "Can't resolve type class"
353resTC' tcs def topholes 1 topg fn elab ist = try' (trivial elab ist) (resolveTC def False 0 topg fn elab ist) True
354resTC' tcs defaultOn topholes depth topg fn elab ist
355 = do compute
356 g <- goal
357 -- Resolution can proceed only if there is something concrete in the
358 -- determining argument positions. Keep track of the holes in the
359 -- non-determining position, because it's okay for 'trivial' to solve
360 -- those holes and no others.
361 let (argsok, okholePos) = case tcArgsOK g topholes of
362 Nothing -> (False, [])
363 Just hs -> (True, hs)
364 env <- get_env
365 probs <- get_probs
366 if not argsok -- && not mvok)
367 then lift $ tfail $ CantResolve True topg (probErr probs)
368 else do
369 ptm <- get_term
370 ulog <- getUnifyLog
371 hs <- get_holes
372 env <- get_env
373 t <- goal
374 let (tc, ttypes) = unApply (getRetTy t)
375 let okholes = case tc of
376 P _ n _ -> zip (repeat n) okholePos
377 _ -> []
379 traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $
380 try' (trivialTCs okholes elab ist)
381 (do addDefault t tc ttypes
382 let stk = map fst (filter snd $ elab_stack ist)
383 let insts = findInstances ist t
384 blunderbuss t depth stk (stk ++ insts)) True
385 where
386 -- returns Just hs if okay, where hs are holes which are okay in the
387 -- goal, or Nothing if not okay to proceed
388 tcArgsOK ty hs | (P _ nc _, as) <- unApply (getRetTy ty), nc == numclass && defaultOn
389 = Just []
390 tcArgsOK ty hs -- if any determining arguments are metavariables, postpone
391 = let (f, as) = unApply (getRetTy ty) in
392 case f of
393 P _ cn _ -> case lookupCtxtExact cn (idris_classes ist) of
394 Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as
395 Nothing -> if any (isMeta hs) as
396 then Nothing
397 else Just []
398 _ -> if any (isMeta hs) as
399 then Nothing
400 else Just []
402 -- return the list of argument positions which can safely be a hole
403 -- or Nothing if one of the determining arguments is a hole
404 tcDetArgsOK i ds hs (x : xs)
405 | i `elem` ds = if isMeta hs x
406 then Nothing
407 else tcDetArgsOK (i + 1) ds hs xs
408 | otherwise = do rs <- tcDetArgsOK (i + 1) ds hs xs
409 case x of
410 P _ n _ -> Just (i : rs)
411 _ -> Just rs
412 tcDetArgsOK _ _ _ [] = Just []
414 probErr [] = Msg ""
415 probErr ((_,_,_,_,err,_,_) : _) = err
417 isMeta :: [Name] -> Term -> Bool
418 isMeta ns (P _ n _) = n `elem` ns
419 isMeta _ _ = False
421 notHole hs (P _ n _, c)
422 | (P _ cn _, _) <- unApply (getRetTy c),
423 n `elem` hs && isConName cn (tt_ctxt ist) = False
424 | Constant _ <- c = not (n `elem` hs)
425 notHole _ _ = True
427 -- HACK! Rather than giving a special name, better to have some kind
428 -- of flag in ClassInfo structure
429 chaser (UN nm)
430 | ('@':'@':_) <- str nm = True -- old way
431 chaser (SN (ParentN _ _)) = True
432 chaser (NS n _) = chaser n
433 chaser _ = False
435 numclass = sNS (sUN "Num") ["Interfaces","Prelude"]
437 addDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn
438 = do focus a
439 fill (RConstant (AType (ATInt ITBig))) -- default Integer
440 solve
441 addDefault t f as
442 | all boundVar as = return () -- True -- fail $ "Can't resolve " ++ show t
443 addDefault t f a = return () -- trace (show t) $ return ()
445 boundVar (P Bound _ _) = True
446 boundVar _ = False
448 blunderbuss t d stk [] = do ps <- get_probs
449 lift $ tfail $ CantResolve False topg (probErr ps)
450 blunderbuss t d stk (n:ns)
451 | n /= fn -- && (n `elem` stk)
452 = tryCatch (resolve n d)
453 (\e -> case e of
454 CantResolve True _ _ -> lift $ tfail e
455 _ -> blunderbuss t d stk ns)
456 | otherwise = blunderbuss t d stk ns
458 introImps = do g <- goal
459 case g of
460 (Bind _ (Pi _ _ _) sc) -> do attack; intro Nothing
461 num <- introImps
462 return (num + 1)
463 _ -> return 0
465 solven n = replicateM_ n solve
467 resolve n depth
468 | depth == 0 = fail $ "Can't resolve type class"
469 | otherwise
470 = do lams <- introImps
471 t <- goal
472 let (tc, ttypes) = trace (show t) $ unApply (getRetTy t)
473-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist
474-- else do
475 -- if there's a hole in the goal, don't even try
476 let imps = case lookupCtxtName n (idris_implicits ist) of
477 [] -> []
478 [args] -> map isImp (snd args) -- won't be overloaded!
479 xs -> error "The impossible happened - overloading is not expected here!"
480 ps <- get_probs
481 tm <- get_term
482 args <- map snd <$> apply (Var n) imps
483 solven lams -- close any implicit lambdas we introduced
484 ps' <- get_probs
485 when (length ps < length ps' || unrecoverable ps') $
486 fail "Can't apply type class"
487-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
488 mapM_ (\ (_,n) -> do focus n
489 t' <- goal
490 let (tc', ttype) = unApply (getRetTy t')
491 let got = fst (unApply (getRetTy t))
492 let depth' = if tc' `elem` tcs
493 then depth - 1 else depth
494 resTC' (got : tcs) defaultOn topholes depth' topg fn elab ist)
495 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
496 -- if there's any arguments left, we've failed to resolve
497 hs <- get_holes
498 ulog <- getUnifyLog
499 solve
500 traceWhen ulog ("Got " ++ show n) $ return ()
501 where isImp (PImp p _ _ _ _) = (True, p)
502 isImp arg = (False, priority arg)
504-- | Find the names of instances that have been designeated for
505-- searching (i.e. non-named instances or instances from Elab scripts)
506findInstances :: IState -> Term -> [Name]
507findInstances ist t
508 | (P _ n _, _) <- unApply (getRetTy t)
509 = case lookupCtxt n (idris_classes ist) of
510 [CI _ _ _ _ _ ins _] ->
511 [n | (n, True) <- ins, accessible n]
512 _ -> []
513 | otherwise = []
514 where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of
515 Just (_, Hidden) -> False
516 Just (_, Private) -> False
517 _ -> True