git.iko.soy/Idris-dev
on 85cf83f help sign in
Idris-dev/src/Idris/ProofSearch.hs
197 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 ty <- goal
89 argsok <- conArgsOK ty
90 if ambigok || argsok then
91 case lookupCtxt nroot (idris_tyinfodata ist) of
92 [TISolution ts] -> findInferredTy ts
93 _ -> psRec rec maxDepth
94 else autoArg (sUN "auto") -- not enough info in the type yet
95 where
96 findInferredTy (t : _) = elab (delab ist (toUN t))
98 conArgsOK ty
99 = let (f, as) = unApply ty in
100 case f of
101 P _ n _ -> case lookupCtxt n (idris_datatypes ist) of
102 [t] -> do rs <- mapM (conReady as) (con_names t)
103 return (and rs)
104 _ -> fail "Ambiguous name"
105 TType _ -> return True
106 _ -> fail "Not a data type"
108 conReady :: [Term] -> Name -> ElabD Bool
109 conReady as n
110 = case lookupTyExact n (tt_ctxt ist) of
111 Just ty -> do let (_, cs) = unApply (getRetTy ty)
112 -- if any metavariables in 'as' correspond to
113 -- a constructor form in 'cs', then we're not
114 -- ready to run auto yet. Otherwise, go for it
115 hs <- get_holes
116 return $ and (map (notHole hs) (zip as cs))
117 Nothing -> fail "Can't happen"
119 notHole hs (P _ n _, c)
120 | (P _ cn _, _) <- unApply c,
121 n `elem` hs && isConName cn (tt_ctxt ist) = False
122 | Constant _ <- c = not (n `elem` hs)
123 notHole _ _ = True
125 toUN t@(P nt (MN i n) ty)
126 | ('_':xs) <- str n = t
127 | otherwise = P nt (UN n) ty
128 toUN (App f a) = App (toUN f) (toUN a)
129 toUN t = t
131 psRec _ 0 | fromProver = cantSolveGoal
132 psRec rec 0 = do attack; defer [] nroot; solve --fail "Maximum depth reached"
133 psRec False d = tryCons d hints
134 psRec True d = try' (trivial elab ist)
135 (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))
136 True)
137 -- if all else fails, make a new metavariable
138 (if fromProver
139 then cantSolveGoal
140 else do attack; defer [] nroot; solve) True) True
142 getFn d Nothing = []
143 getFn d (Just f) | d < maxDepth-1 = [f]
144 | otherwise = []
146 resolveByCon d
147 = do t <- goal
148 let (f, _) = unApply t
149 case f of
150 P _ n _ -> case lookupCtxt n (idris_datatypes ist) of
151 [t] -> tryCons d (hints ++ con_names t ++
152 getFn d fn)
153 _ -> fail "Not a data type"
154 _ -> fail "Not a data type"
156 -- if there are local variables which have a function type, try
157 -- applying them too
158 resolveByLocals d
159 = do env <- get_env
160 tryLocals d env
162 tryLocals d [] = fail "Locals failed"
163 tryLocals d ((x, t) : xs) = try' (tryLocal d x t) (tryLocals d xs) True
165 tryCons d [] = fail "Constructors failed"
166 tryCons d (c : cs) = try' (tryCon d c) (tryCons d cs) True
168 tryLocal d n t = do let a = getPArity (delab ist (binderTy t))
169 tryLocalArg d n a
171 tryLocalArg d n 0 = elab (PRef (fileFC "prf") n)
172 tryLocalArg d n i = simple_app (tryLocalArg d n (i - 1))
173 (psRec True d) "proof search local apply"
175 -- Like type class resolution, but searching with constructors
176 tryCon d n =
177 do ty <- goal
178 let imps = case lookupCtxtName n (idris_implicits ist) of
179 [] -> []
180 [args] -> map isImp (snd args)
181 _ -> fail "Ambiguous name"
182 ps <- get_probs
183 hs <- get_holes
184 args <- map snd <$> try' (apply (Var n) imps)
185 (match_apply (Var n) imps) True
186 ps' <- get_probs
187 hs' <- get_holes
188 when (length ps < length ps') $ fail "Can't apply constructor"
189 mapM_ (\ (_, h) -> do focus h
190 aty <- goal
191 psRec True d)
192 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
193 solve
195 isImp (PImp p _ _ _ _) = (True, p)
196 isImp arg = (False, priority arg)