git.iko.soy/Idris-dev
on 63ff875 help sign in
Idris-dev/src/Idris/ProofSearch.hs
528 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 _ -> fail "Not a data type"
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 when (not fromProver && length (con_names t) > 1)
280 -- in interactive mode,
281 -- don't just guess (fine for 'auto',
282 -- since that's part of the point...)
283 $ checkConstructor ist others
284 tryCons d locs tys (others ++ getFn d fn)
285 Nothing -> fail "Not a data type"
286 _ -> fail "Not a data type"
288 -- if there are local variables which have a function type, try
289 -- applying them too
290 resolveByLocals d locs tys
291 = do env <- get_env
292 tryLocals d locs tys env
294 tryLocals d locs tys [] = fail "Locals failed"
295 tryLocals d locs tys ((x, t) : xs)
296 | x `elem` locs || x `notElem` psnames = tryLocals d locs tys xs
297 | otherwise = try' (tryLocal d (x : locs) tys x t)
298 (tryLocals d locs tys xs) True
300 tryCons d locs tys [] = fail "Constructors failed"
301 tryCons d locs tys (c : cs)
302 = try' (tryCon d locs tys c) (tryCons d locs tys cs) True
304 tryLocal d locs tys n t
305 = do let a = getPArity (delab ist (binderTy t))
306 tryLocalArg d locs tys n a
308 tryLocalArg d locs tys n 0 = elab (PRef (fileFC "prf") [] n)
309 tryLocalArg d locs tys n i
310 = simple_app False (tryLocalArg d locs tys n (i - 1))
311 (psRec True d locs tys) "proof search local apply"
313 -- Like type class resolution, but searching with constructors
314 tryCon d locs tys n =
315 do ty <- goal
316 let imps = case lookupCtxtExact n (idris_implicits ist) of
317 Nothing -> []
318 Just args -> map isImp args
319 ps <- get_probs
320 hs <- get_holes
321 args <- map snd <$> try' (apply (Var n) imps)
322 (match_apply (Var n) imps) True
323 ps' <- get_probs
324 hs' <- get_holes
325 when (length ps < length ps') $ fail "Can't apply constructor"
326 let newhs = filter (\ (x, y) -> not x) (zip (map fst imps) args)
327 mapM_ (\ (_, h) -> do focus h
328 aty <- goal
329 psRec True d locs tys) newhs
330 solve
332 isImp (PImp p _ _ _ _) = (True, p)
333 isImp arg = (False, priority arg)
335-- In interactive mode, only search for things if there is some
336-- index to help pick a relevant constructor
337checkConstructor :: IState -> [Name] -> ElabD ()
338checkConstructor ist [] = return ()
339checkConstructor ist (n : ns) =
340 case lookupTyExact n (tt_ctxt ist) of
341 Just t -> if not (conIndexed t)
342 then fail "Overlapping constructor types"
343 else checkConstructor ist ns
344 where
345 conIndexed t = let (_, args) = unApply (getRetTy t) in
346 any conHead args
347 conHead t | (P _ n _, _) <- unApply t = case lookupDefExact n (tt_ctxt ist) of
348 Just _ -> True
349 _ -> False
350 | otherwise = False
352-- | Resolve type classes. This will only pick up 'normal' instances, never
353-- named instances (which is enforced by 'findInstances').
354resolveTC :: Bool -- ^ using default Int
355 -> Bool -- ^ allow metavariables in the goal
356 -> Int -- ^ depth
357 -> Term -- ^ top level goal, for error messages
358 -> Name -- ^ top level function name, to prevent loops
359 -> (PTerm -> ElabD ()) -- ^ top level elaborator
360 -> IState -> ElabD ()
361resolveTC def mvok depth top fn elab ist
362 = do hs <- get_holes
363 resTC' [] def hs depth top fn elab ist
365resTC' tcs def topholes 0 topg fn elab ist = fail $ "Can't resolve type class"
366resTC' tcs def topholes 1 topg fn elab ist = try' (trivial elab ist) (resolveTC def False 0 topg fn elab ist) True
367resTC' tcs defaultOn topholes depth topg fn elab ist
368 = do compute
369 g <- goal
370 -- Resolution can proceed only if there is something concrete in the
371 -- determining argument positions. Keep track of the holes in the
372 -- non-determining position, because it's okay for 'trivial' to solve
373 -- those holes and no others.
374 let (argsok, okholePos) = case tcArgsOK g topholes of
375 Nothing -> (False, [])
376 Just hs -> (True, hs)
377 if not argsok -- && not mvok)
378 then lift $ tfail $ CantResolve True topg
379 else do
380 ptm <- get_term
381 ulog <- getUnifyLog
382 hs <- get_holes
383 env <- get_env
384 t <- goal
385 let (tc, ttypes) = unApply (getRetTy t)
386 let okholes = case tc of
387 P _ n _ -> zip (repeat n) okholePos
388 _ -> []
390 traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $
391 try' (trivialTCs okholes elab ist)
392 (do addDefault t tc ttypes
393 let stk = map fst (filter snd $ elab_stack ist)
394 let insts = findInstances ist t
395 blunderbuss t depth stk (stk ++ insts)) True
396 where
397 -- returns Just hs if okay, where hs are holes which are okay in the
398 -- goal, or Nothing if not okay to proceed
399 tcArgsOK ty hs | (P _ nc _, as) <- unApply (getRetTy ty), nc == numclass && defaultOn
400 = Just []
401 tcArgsOK ty hs -- if any determining arguments are metavariables, postpone
402 = let (f, as) = unApply (getRetTy ty) in
403 case f of
404 P _ cn _ -> case lookupCtxtExact cn (idris_classes ist) of
405 Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as
406 Nothing -> if any (isMeta hs) as
407 then Nothing
408 else Just []
409 _ -> if any (isMeta hs) as
410 then Nothing
411 else Just []
413 -- return the list of argument positions which can safely be a hole
414 -- or Nothing if one of the determining arguments is a hole
415 tcDetArgsOK i ds hs (x : xs)
416 | i `elem` ds = if isMeta hs x
417 then Nothing
418 else tcDetArgsOK (i + 1) ds hs xs
419 | otherwise = do rs <- tcDetArgsOK (i + 1) ds hs xs
420 case x of
421 P _ n _ -> Just (i : rs)
422 _ -> Just rs
423 tcDetArgsOK _ _ _ [] = Just []
425 isMeta :: [Name] -> Term -> Bool
426 isMeta ns (P _ n _) = n `elem` ns
427 isMeta _ _ = False
429 notHole hs (P _ n _, c)
430 | (P _ cn _, _) <- unApply (getRetTy c),
431 n `elem` hs && isConName cn (tt_ctxt ist) = False
432 | Constant _ <- c = not (n `elem` hs)
433 notHole _ _ = True
435 -- HACK! Rather than giving a special name, better to have some kind
436 -- of flag in ClassInfo structure
437 chaser (UN nm)
438 | ('@':'@':_) <- str nm = True -- old way
439 chaser (SN (ParentN _ _)) = True
440 chaser (NS n _) = chaser n
441 chaser _ = False
443 numclass = sNS (sUN "Num") ["Classes","Prelude"]
445 addDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn
446 = do focus a
447 fill (RConstant (AType (ATInt ITBig))) -- default Integer
448 solve
449 addDefault t f as
450 | all boundVar as = return () -- True -- fail $ "Can't resolve " ++ show t
451 addDefault t f a = return () -- trace (show t) $ return ()
453 boundVar (P Bound _ _) = True
454 boundVar _ = False
456 blunderbuss t d stk [] = do -- c <- get_env
457 -- ps <- get_probs
458 lift $ tfail $ CantResolve False topg
459 blunderbuss t d stk (n:ns)
460 | n /= fn -- && (n `elem` stk)
461 = tryCatch (resolve n d)
462 (\e -> case e of
463 CantResolve True _ -> lift $ tfail e
464 _ -> blunderbuss t d stk ns)
465 | otherwise = blunderbuss t d stk ns
467 introImps = do g <- goal
468 case g of
469 (Bind _ (Pi _ _ _) sc) -> do attack; intro Nothing
470 num <- introImps
471 return (num + 1)
472 _ -> return 0
474 solven 0 = return ()
475 solven n = do solve; solven (n - 1)
477 resolve n depth
478 | depth == 0 = fail $ "Can't resolve type class"
479 | otherwise
480 = do lams <- introImps
481 t <- goal
482 let (tc, ttypes) = trace (show t) $ unApply (getRetTy t)
483-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist
484-- else do
485 -- if there's a hole in the goal, don't even try
486 let imps = case lookupCtxtName n (idris_implicits ist) of
487 [] -> []
488 [args] -> map isImp (snd args) -- won't be overloaded!
489 xs -> error "The impossible happened - overloading is not expected here!"
490 ps <- get_probs
491 tm <- get_term
492 args <- map snd <$> apply (Var n) imps
493 solven lams -- close any implicit lambdas we introduced
494 ps' <- get_probs
495 when (length ps < length ps' || unrecoverable ps') $
496 fail "Can't apply type class"
497-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
498 mapM_ (\ (_,n) -> do focus n
499 t' <- goal
500 let (tc', ttype) = unApply (getRetTy t')
501 let got = fst (unApply (getRetTy t))
502 let depth' = if tc' `elem` tcs
503 then depth - 1 else depth
504 resTC' (got : tcs) defaultOn topholes depth' topg fn elab ist)
505 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
506 -- if there's any arguments left, we've failed to resolve
507 hs <- get_holes
508 ulog <- getUnifyLog
509 solve
510 traceWhen ulog ("Got " ++ show n) $ return ()
511 where isImp (PImp p _ _ _ _) = (True, p)
512 isImp arg = (False, priority arg)
514-- | Find the names of instances that have been designeated for
515-- searching (i.e. non-named instances or instances from Elab scripts)
516findInstances :: IState -> Term -> [Name]
517findInstances ist t
518 | (P _ n _, _) <- unApply (getRetTy t)
519 = case lookupCtxt n (idris_classes ist) of
520 [CI _ _ _ _ _ ins _] ->
521 [n | (n, True) <- ins, accessible n]
522 _ -> []
523 | otherwise = []
524 where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of
525 Just (_, Hidden) -> False
526 _ -> True