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