git.iko.soy/Idris-dev
on 465cc1c help sign in
Idris-dev/src/Idris/ProofSearch.hs
199 lines 8.1 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 Data.List
19import Debug.Trace
21-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm
23trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()
24trivial elab ist = try' (do elab (PRefl (fileFC "prf") Placeholder)
25 return ())
26 (do env <- get_env
27 g <- goal
28 tryAll env
29 return ()) True
30 where
31 tryAll [] = fail "No trivial solution"
32 tryAll ((x, b):xs)
33 = do -- if type of x has any holes in it, move on
34 hs <- get_holes
35 g <- goal
36 if all (\n -> not (n `elem` hs)) (freeNames (binderTy b))
37 then try' (elab (PRef (fileFC "prf") x))
38 (tryAll xs) True
39 else tryAll xs
41cantSolveGoal :: ElabD a
42cantSolveGoal = do g <- goal
43 env <- get_env
44 lift $ tfail $
45 CantSolveGoal g (map (\(n,b) -> (n, binderTy b)) env)
47proofSearch :: Bool -> -- recursive search (False for 'refine')
48 Bool -> -- invoked from a tactic proof. If so, making
49 -- new metavariables is meaningless, and there shoudl
50 -- be an error reported instead.
51 Bool -> -- ambiguity ok
52 Bool -> -- defer on failure
53 Int -> -- maximum depth
54 (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->
55 IState -> ElabD ()
56proofSearch False fromProver ambigok deferonfail depth elab _ nroot [fn] ist
57 = do -- get all possible versions of the name, take the first one that
58 -- works
59 let all_imps = lookupCtxtName fn (idris_implicits ist)
60 tryAllFns all_imps
61 where
62 -- if nothing worked, make a new metavariable
63 tryAllFns [] | fromProver = cantSolveGoal
64 tryAllFns [] = do attack; defer [] nroot; solve
65 tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True
67 tryFn (f, args) = do let imps = map isImp args
68 ps <- get_probs
69 hs <- get_holes
70 args <- map snd <$> try' (apply (Var f) imps)
71 (match_apply (Var f) imps) True
72 ps' <- get_probs
73-- when (length ps < length ps') $ fail "Can't apply constructor"
74 -- Make metavariables for new holes
75 hs' <- get_holes
76 ptm <- get_term
77 if fromProver then cantSolveGoal
78 else do
79 mapM_ (\ h -> do focus h
80 attack; defer [] nroot; solve)
81 (hs' \\ hs)
82-- (filter (\ (x, y) -> not x) (zip (map fst imps) args))
83 solve
85 isImp (PImp p _ _ _ _) = (True, p)
86 isImp arg = (True, priority arg) -- try to get all of them by unification
87proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
88 = do compute
89 ty <- goal
90 argsok <- conArgsOK ty
91 if ambigok || argsok then
92 case lookupCtxt nroot (idris_tyinfodata ist) of
93 [TISolution ts] -> findInferredTy ts
94 _ -> psRec rec maxDepth
95 else autoArg (sUN "auto") -- not enough info in the type yet
96 where
97 findInferredTy (t : _) = elab (delab ist (toUN t))
99 conArgsOK ty
100 = let (f, as) = unApply ty in
101 case f of
102 P _ n _ -> case lookupCtxt n (idris_datatypes ist) of
103 [t] -> do rs <- mapM (conReady as) (con_names t)
104 return (and rs)
105 _ -> fail "Ambiguous name"
106 TType _ -> return True
107 _ -> fail "Not a data type"
109 conReady :: [Term] -> Name -> ElabD Bool
110 conReady as n
111 = case lookupTyExact n (tt_ctxt ist) of
112 Just ty -> do let (_, cs) = unApply (getRetTy ty)
113 -- if any metavariables in 'as' correspond to
114 -- a constructor form in 'cs', then we're not
115 -- ready to run auto yet. Otherwise, go for it
116 hs <- get_holes
117 return $ and (map (notHole hs) (zip as cs))
118 Nothing -> fail "Can't happen"
120 notHole hs (P _ n _, c)
121 | (P _ cn _, _) <- unApply c,
122 n `elem` hs && isConName cn (tt_ctxt ist) = False
123 | Constant _ <- c = not (n `elem` hs)
124 notHole _ _ = True
126 toUN t@(P nt (MN i n) ty)
127 | ('_':xs) <- str n = t
128 | otherwise = P nt (UN n) ty
129 toUN (App f a) = App (toUN f) (toUN a)
130 toUN t = t
132 psRec _ 0 | fromProver = cantSolveGoal
133 psRec rec 0 = do attack; defer [] nroot; solve --fail "Maximum depth reached"
134 psRec False d = tryCons d hints
135 psRec True d = do compute
136 try' (trivial elab ist)
137 (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))
138 True)
139 -- if all else fails, make a new metavariable
140 (if fromProver
141 then fail "cantSolveGoal"
142 else do attack; defer [] nroot; solve) True) True
144 getFn d Nothing = []
145 getFn d (Just f) | d < maxDepth-1 = [f]
146 | otherwise = []
148 resolveByCon d
149 = do t <- goal
150 let (f, _) = unApply t
151 case f of
152 P _ n _ -> case lookupCtxt n (idris_datatypes ist) of
153 [t] -> tryCons d (hints ++ con_names t ++
154 getFn d fn)
155 _ -> fail "Not a data type"
156 _ -> fail "Not a data type"
158 -- if there are local variables which have a function type, try
159 -- applying them too
160 resolveByLocals d
161 = do env <- get_env
162 tryLocals d env
164 tryLocals d [] = fail "Locals failed"
165 tryLocals d ((x, t) : xs) = try' (tryLocal d x t) (tryLocals d xs) True
167 tryCons d [] = fail "Constructors failed"
168 tryCons d (c : cs) = try' (tryCon d c) (tryCons d cs) True
170 tryLocal d n t = do let a = getPArity (delab ist (binderTy t))
171 tryLocalArg d n a
173 tryLocalArg d n 0 = elab (PRef (fileFC "prf") n)
174 tryLocalArg d n i = simple_app False (tryLocalArg d n (i - 1))
175 (psRec True d) "proof search local apply"
177 -- Like type class resolution, but searching with constructors
178 tryCon d n =
179 do ty <- goal
180 let imps = case lookupCtxtName n (idris_implicits ist) of
181 [] -> []
182 [args] -> map isImp (snd args)
183 _ -> fail "Ambiguous name"
184 ps <- get_probs
185 hs <- get_holes
186 args <- map snd <$> try' (apply (Var n) imps)
187 (match_apply (Var n) imps) True
188 ps' <- get_probs
189 hs' <- get_holes
190 when (length ps < length ps') $ fail "Can't apply constructor"
191 mapM_ (\ (_, h) -> do focus h
192 aty <- goal
193 psRec True d)
194 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
195 solve
197 isImp (PImp p _ _ _ _) = (True, p)
198 isImp arg = (False, priority arg)