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