git.iko.soy/Idris-dev
on 54e4e41 help sign in
Idris-dev/src/Idris/ProofSearch.hs
256 lines 11 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.ProofSearch(trivial, trivialHoles, proofSearch) where
5import Idris.Core.Elaborate hiding (Tactic(..))
6import Idris.Core.TT
7import Idris.Core.Evaluate
8import Idris.Core.CaseTree
9import Idris.Core.Typecheck
11import Idris.AbsSyntax
12import Idris.Delaborate
13import Idris.Error
15import Control.Applicative ((<$>))
16import Control.Monad
17import Control.Monad.State.Strict
18import qualified Data.Set as S
19import Data.List
20import Debug.Trace
22-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm
24trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()
25trivial = trivialHoles []
27trivialHoles :: [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
28trivialHoles ok elab ist
29 = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") [] eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])
30 return ())
31 (do env <- get_env
32 g <- goal
33 tryAll env
34 return ()) True
35 where
36 tryAll [] = fail "No trivial solution"
37 tryAll ((x, b):xs)
38 = do -- if type of x has any holes in it, move on
39 hs <- get_holes
40 let badhs = hs -- filter (flip notElem holesOK) hs
41 g <- goal
42 -- anywhere but the top is okay for a hole, if holesOK set
43 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))
44 holesOK hs (binderTy b)
45 then try' (elab (PRef (fileFC "prf") [] x))
46 (tryAll xs) True
47 else tryAll xs
49 holesOK hs ap@(App _ _ _)
50 | (P _ n _, args) <- unApply ap
51 = holeArgsOK hs n 0 args
52 holesOK hs (App _ f a) = holesOK hs f && holesOK hs a
53 holesOK hs (P _ n _) = not (n `elem` hs)
54 holesOK hs (Bind n b sc) = holesOK hs (binderTy b) &&
55 holesOK hs sc
56 holesOK hs _ = True
58 holeArgsOK hs n p [] = True
59 holeArgsOK hs n p (a : as)
60 | (n, p) `elem` ok = holeArgsOK hs n (p + 1) as
61 | otherwise = holesOK hs a && holeArgsOK hs n (p + 1) as
63cantSolveGoal :: ElabD a
64cantSolveGoal = do g <- goal
65 env <- get_env
66 lift $ tfail $
67 CantSolveGoal g (map (\(n,b) -> (n, binderTy b)) env)
69proofSearch :: Bool -> -- recursive search (False for 'refine')
70 Bool -> -- invoked from a tactic proof. If so, making
71 -- new metavariables is meaningless, and there shoudl
72 -- be an error reported instead.
73 Bool -> -- ambiguity ok
74 Bool -> -- defer on failure
75 Int -> -- maximum depth
76 (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->
77 IState -> ElabD ()
78proofSearch False fromProver ambigok deferonfail depth elab _ nroot [fn] ist
79 = do -- get all possible versions of the name, take the first one that
80 -- works
81 let all_imps = lookupCtxtName fn (idris_implicits ist)
82 tryAllFns all_imps
83 where
84 -- if nothing worked, make a new metavariable
85 tryAllFns [] | fromProver = cantSolveGoal
86 tryAllFns [] = do attack; defer [] nroot; solve
87 tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True
89 tryFn (f, args) = do let imps = map isImp args
90 ps <- get_probs
91 hs <- get_holes
92 args <- map snd <$> try' (apply (Var f) imps)
93 (match_apply (Var f) imps) True
94 ps' <- get_probs
95-- when (length ps < length ps') $ fail "Can't apply constructor"
96 -- Make metavariables for new holes
97 hs' <- get_holes
98 ptm <- get_term
99 if fromProver then cantSolveGoal
100 else do
101 mapM_ (\ h -> do focus h
102 attack; defer [] nroot; solve)
103 (hs' \\ hs)
104-- (filter (\ (x, y) -> not x) (zip (map fst imps) args))
105 solve
107 isImp (PImp p _ _ _ _) = (True, p)
108 isImp arg = (True, priority arg) -- try to get all of them by unification
109proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
110 = do compute
111 ty <- goal
112 hs <- get_holes
113 env <- get_env
114 tm <- get_term
115 argsok <- conArgsOK ty
116 if ambigok || argsok then
117 case lookupCtxt nroot (idris_tyinfodata ist) of
118 [TISolution ts] -> findInferredTy ts
119 _ -> psRec rec maxDepth [] S.empty
120 else do ptm <- get_term
121 autoArg (sUN "auto") -- not enough info in the type yet
122 where
123 findInferredTy (t : _) = elab (delab ist (toUN t))
125 conArgsOK ty
126 = let (f, as) = unApply ty in
127 case f of
128 P _ n _ ->
129 let autohints = case lookupCtxtExact n (idris_autohints ist) of
130 Nothing -> []
131 Just hs -> hs in
132 case lookupCtxtExact n (idris_datatypes ist) of
133 Just t -> do rs <- mapM (conReady as)
134 (autohints ++ con_names t)
135 return (and rs)
136 Nothing -> -- local variable, go for it
137 return True
138 TType _ -> return True
139 _ -> fail "Not a data type"
141 conReady :: [Term] -> Name -> ElabD Bool
142 conReady as n
143 = case lookupTyExact n (tt_ctxt ist) of
144 Just ty -> do let (_, cs) = unApply (getRetTy ty)
145 -- if any metavariables in 'as' correspond to
146 -- a constructor form in 'cs', then we're not
147 -- ready to run auto yet. Otherwise, go for it
148 hs <- get_holes
149 return $ and (map (notHole hs) (zip as cs))
150 Nothing -> fail "Can't happen"
152 notHole hs (P _ n _, c)
153 | (P _ cn _, _) <- unApply c,
154 n `elem` hs && isConName cn (tt_ctxt ist) = False
155 | Constant _ <- c = not (n `elem` hs)
156 notHole _ _ = True
158 toUN t@(P nt (MN i n) ty)
159 | ('_':xs) <- str n = t
160 | otherwise = P nt (UN n) ty
161 toUN (App s f a) = App s (toUN f) (toUN a)
162 toUN t = t
164 -- psRec counts depth and the local variable applications we're under
165 -- (so we don't try a pointless application of something to itself,
166 -- which obviously won't work anyway but might lead us on a wild
167 -- goose chase...)
168 -- Also keep track of the types we've proved so far in this branch
169 -- (if we get back to one we've been to before, we're just in a cycle and
170 -- that's no use)
171 psRec :: Bool -> Int -> [Name] -> S.Set Type -> ElabD ()
172 psRec _ 0 locs tys | fromProver = cantSolveGoal
173 psRec rec 0 locs tys = do attack; defer [] nroot; solve --fail "Maximum depth reached"
174 psRec False d locs tys = tryCons d locs tys hints
175 psRec True d locs tys
176 = do compute
177 ty <- goal
178 when (S.member ty tys) $ fail "Been here before"
179 let tys' = S.insert ty tys
180 try' (trivial elab ist)
181 (try' (try' (resolveByCon (d - 1) locs tys')
182 (resolveByLocals (d - 1) locs tys')
183 True)
184 -- if all else fails, make a new metavariable
185 (if fromProver
186 then fail "cantSolveGoal"
187 else do attack; defer [] nroot; solve) True) True
189 getFn d Nothing = []
190 getFn d (Just f) | d < maxDepth-1 = [f]
191 | otherwise = []
193 resolveByCon d locs tys
194 = do t <- goal
195 let (f, _) = unApply t
196 case f of
197 P _ n _ ->
198 do let autohints = case lookupCtxtExact n (idris_autohints ist) of
199 Nothing -> []
200 Just hs -> hs
201 case lookupCtxtExact n (idris_datatypes ist) of
202 Just t -> tryCons d locs tys
203 (hints ++
204 con_names t ++
205 autohints ++
206 getFn d fn)
207 Nothing -> fail "Not a data type"
208 _ -> fail "Not a data type"
210 -- if there are local variables which have a function type, try
211 -- applying them too
212 resolveByLocals d locs tys
213 = do env <- get_env
214 tryLocals d locs tys env
216 tryLocals d locs tys [] = fail "Locals failed"
217 tryLocals d locs tys ((x, t) : xs)
218 | x `elem` locs = tryLocals d locs tys xs
219 | otherwise = try' (tryLocal d (x : locs) tys x t)
220 (tryLocals d locs tys xs) True
222 tryCons d locs tys [] = fail "Constructors failed"
223 tryCons d locs tys (c : cs)
224 = try' (tryCon d locs tys c) (tryCons d locs tys cs) True
226 tryLocal d locs tys n t
227 = do let a = getPArity (delab ist (binderTy t))
228 tryLocalArg d locs tys n a
230 tryLocalArg d locs tys n 0 = elab (PRef (fileFC "prf") [] n)
231 tryLocalArg d locs tys n i
232 = simple_app False (tryLocalArg d locs tys n (i - 1))
233 (psRec True d locs tys) "proof search local apply"
235 -- Like type class resolution, but searching with constructors
236 tryCon d locs tys n =
237 do ty <- goal
238 let imps = case lookupCtxtExact n (idris_implicits ist) of
239 Nothing -> []
240 Just args -> map isImp args
241 ps <- get_probs
242 hs <- get_holes
243 args <- map snd <$> try' (apply (Var n) imps)
244 (match_apply (Var n) imps) True
245 ps' <- get_probs
246 hs' <- get_holes
247 when (length ps < length ps') $ fail "Can't apply constructor"
248 mapM_ (\ (_, h) -> do focus h
249 aty <- goal
250 psRec True d locs tys)
251 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
252 solve
254 isImp (PImp p _ _ _ _) = (True, p)
255 isImp arg = (False, priority arg)