git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Idris/ProofSearch.hs
226 lines 9.6 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.ProofSearch(trivial, 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 elab ist = try' (do elab (PRefl (fileFC "prf") Placeholder)
26 return ())
27 (do env <- get_env
28 g <- goal
29 tryAll env
30 return ()) True
31 where
32 tryAll [] = fail "No trivial solution"
33 tryAll ((x, b):xs)
34 = do -- if type of x has any holes in it, move on
35 hs <- get_holes
36 g <- goal
37 if all (\n -> not (n `elem` hs)) (freeNames (binderTy b))
38 then try' (elab (PRef (fileFC "prf") x))
39 (tryAll xs) True
40 else tryAll xs
42cantSolveGoal :: ElabD a
43cantSolveGoal = do g <- goal
44 env <- get_env
45 lift $ tfail $
46 CantSolveGoal g (map (\(n,b) -> (n, binderTy b)) env)
48proofSearch :: Bool -> -- recursive search (False for 'refine')
49 Bool -> -- invoked from a tactic proof. If so, making
50 -- new metavariables is meaningless, and there shoudl
51 -- be an error reported instead.
52 Bool -> -- ambiguity ok
53 Bool -> -- defer on failure
54 Int -> -- maximum depth
55 (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->
56 IState -> ElabD ()
57proofSearch False fromProver ambigok deferonfail depth elab _ nroot [fn] ist
58 = do -- get all possible versions of the name, take the first one that
59 -- works
60 let all_imps = lookupCtxtName fn (idris_implicits ist)
61 tryAllFns all_imps
62 where
63 -- if nothing worked, make a new metavariable
64 tryAllFns [] | fromProver = cantSolveGoal
65 tryAllFns [] = do attack; defer [] nroot; solve
66 tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True
68 tryFn (f, args) = do let imps = map isImp args
69 ps <- get_probs
70 hs <- get_holes
71 args <- map snd <$> try' (apply (Var f) imps)
72 (match_apply (Var f) imps) True
73 ps' <- get_probs
74-- when (length ps < length ps') $ fail "Can't apply constructor"
75 -- Make metavariables for new holes
76 hs' <- get_holes
77 ptm <- get_term
78 if fromProver then cantSolveGoal
79 else do
80 mapM_ (\ h -> do focus h
81 attack; defer [] nroot; solve)
82 (hs' \\ hs)
83-- (filter (\ (x, y) -> not x) (zip (map fst imps) args))
84 solve
86 isImp (PImp p _ _ _ _) = (True, p)
87 isImp arg = (True, priority arg) -- try to get all of them by unification
88proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
89 = do compute
90 ty <- goal
91 argsok <- conArgsOK ty
92 if ambigok || argsok then
93 case lookupCtxt nroot (idris_tyinfodata ist) of
94 [TISolution ts] -> findInferredTy ts
95 _ -> psRec rec maxDepth [] S.empty
96 else autoArg (sUN "auto") -- not enough info in the type yet
97 where
98 findInferredTy (t : _) = elab (delab ist (toUN t))
100 conArgsOK ty
101 = let (f, as) = unApply ty in
102 case f of
103 P _ n _ -> case lookupCtxtExact n (idris_datatypes ist) of
104 Just t -> do rs <- mapM (conReady as) (con_names t)
105 return (and rs)
106 Nothing -> -- local variable, go for it
107 return True
108 TType _ -> return True
109 _ -> fail "Not a data type"
111 conReady :: [Term] -> Name -> ElabD Bool
112 conReady as n
113 = case lookupTyExact n (tt_ctxt ist) of
114 Just ty -> do let (_, cs) = unApply (getRetTy ty)
115 -- if any metavariables in 'as' correspond to
116 -- a constructor form in 'cs', then we're not
117 -- ready to run auto yet. Otherwise, go for it
118 hs <- get_holes
119 return $ and (map (notHole hs) (zip as cs))
120 Nothing -> fail "Can't happen"
122 notHole hs (P _ n _, c)
123 | (P _ cn _, _) <- unApply c,
124 n `elem` hs && isConName cn (tt_ctxt ist) = False
125 | Constant _ <- c = not (n `elem` hs)
126 notHole _ _ = True
128 toUN t@(P nt (MN i n) ty)
129 | ('_':xs) <- str n = t
130 | otherwise = P nt (UN n) ty
131 toUN (App f a) = App (toUN f) (toUN a)
132 toUN t = t
134 -- psRec counts depth and the local variable applications we're under
135 -- (so we don't try a pointless application of something to itself,
136 -- which obviously won't work anyway but might lead us on a wild
137 -- goose chase...)
138 -- Also keep track of the types we've proved so far in this branch
139 -- (if we get back to one we've been to before, we're just in a cycle and
140 -- that's no use)
141 psRec :: Bool -> Int -> [Name] -> S.Set Type -> ElabD ()
142 psRec _ 0 locs tys | fromProver = cantSolveGoal
143 psRec rec 0 locs tys = do attack; defer [] nroot; solve --fail "Maximum depth reached"
144 psRec False d locs tys = tryCons d locs tys hints
145 psRec True d locs tys
146 = do compute
147 ty <- goal
148 when (S.member ty tys) $ fail "Been here before"
149 let tys' = S.insert ty tys
150 try' (trivial elab ist)
151 (try' (try' (resolveByCon (d - 1) locs tys')
152 (resolveByLocals (d - 1) locs tys')
153 True)
154 -- if all else fails, make a new metavariable
155 (if fromProver
156 then fail "cantSolveGoal"
157 else do attack; defer [] nroot; solve) True) True
159 getFn d Nothing = []
160 getFn d (Just f) | d < maxDepth-1 = [f]
161 | otherwise = []
163 resolveByCon d locs tys
164 = do t <- goal
165 let (f, _) = unApply t
166 case f of
167 P _ n _ ->
168 do let autohints = case lookupCtxtExact n (idris_autohints ist) of
169 Nothing -> []
170 Just hs -> hs
171 case lookupCtxtExact n (idris_datatypes ist) of
172 Just t -> tryCons d locs tys
173 (hints ++
174 con_names t ++
175 autohints ++
176 getFn d fn)
177 Nothing -> fail "Not a data type"
178 _ -> fail "Not a data type"
180 -- if there are local variables which have a function type, try
181 -- applying them too
182 resolveByLocals d locs tys
183 = do env <- get_env
184 tryLocals d locs tys env
186 tryLocals d locs tys [] = fail "Locals failed"
187 tryLocals d locs tys ((x, t) : xs)
188 | x `elem` locs = tryLocals d locs tys xs
189 | otherwise = try' (tryLocal d (x : locs) tys x t)
190 (tryLocals d locs tys xs) True
192 tryCons d locs tys [] = fail "Constructors failed"
193 tryCons d locs tys (c : cs)
194 = try' (tryCon d locs tys c) (tryCons d locs tys cs) True
196 tryLocal d locs tys n t
197 = do let a = getPArity (delab ist (binderTy t))
198 tryLocalArg d locs tys n a
200 tryLocalArg d locs tys n 0 = elab (PRef (fileFC "prf") n)
201 tryLocalArg d locs tys n i
202 = simple_app False (tryLocalArg d locs tys n (i - 1))
203 (psRec True d locs tys) "proof search local apply"
205 -- Like type class resolution, but searching with constructors
206 tryCon d locs tys n =
207 do ty <- goal
208 let imps = case lookupCtxtExact n (idris_implicits ist) of
209 Nothing -> []
210 Just args -> map isImp args
211 ps <- get_probs
212 hs <- get_holes
213 args <- map snd <$> try' (apply (Var n) imps)
214 (match_apply (Var n) imps) True
215 ps' <- get_probs
216 hs' <- get_holes
217 when (length ps < length ps') $ fail "Can't apply constructor"
218 mapM_ (\ (_, h) -> do focus h
219 aty <- goal
220 psRec True d locs tys)
221 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
222 solve
224 isImp (PImp p _ _ _ _) = (True, p)
225 isImp arg = (False, priority arg)