git.iko.soy/Idris-dev
on e63fcef help sign in
Idris-dev/src/Idris/ProofSearch.hs
99 lines 3.6 kB history raw
1module Idris.ProofSearch(trivial, proofSearch) where
3import Idris.Core.Elaborate hiding (Tactic(..))
4import Idris.Core.TT
5import Idris.Core.Evaluate
6import Idris.Core.CaseTree
7import Idris.Core.Typecheck
9import Idris.AbsSyntax
10import Idris.Delaborate
11import Idris.Error
13import Control.Monad
14import Debug.Trace
16-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm
18trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()
19trivial elab ist = try' (do elab (PRefl (fileFC "prf") Placeholder)
20 return ())
21 (do env <- get_env
22 g <- goal
23 tryAll env
24 return ()) True
25 where
26 tryAll [] = fail "No trivial solution"
27 tryAll ((x, b):xs)
28 = do -- if type of x has any holes in it, move on
29 hs <- get_holes
30 g <- goal
31 if all (\n -> not (n `elem` hs)) (freeNames (binderTy b))
32 then try' (elab (PRef (fileFC "prf") x))
33 (tryAll xs) True
34 else tryAll xs
36proofSearch :: (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->
37 IState -> ElabD ()
38proofSearch elab fn nroot hints ist = psRec maxDepth
39 where
40 maxDepth = 6
42 psRec 0 = do attack; defer nroot; solve --fail "Maximum depth reached"
43 psRec d = try' (trivial elab ist)
44 (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))
45 True)
46 -- if all else fails, make a new metavariable
47 (do attack; defer nroot; solve) True) True
49 getFn d Nothing = []
50 getFn d (Just f) | d < maxDepth-1 = [f]
51 | otherwise = []
53 resolveByCon d
54 = do t <- goal
55 let (f, _) = unApply t
56 case f of
57 P _ n _ -> case lookupCtxt n (idris_datatypes ist) of
58 [t] -> tryCons d (hints ++ con_names t ++
59 getFn d fn)
60 _ -> fail "Not a data type"
61 _ -> fail "Not a data type"
63 -- if there are local variables which have a function type, try
64 -- applying them too
65 resolveByLocals d
66 = do env <- get_env
67 tryLocals d env
69 tryLocals d [] = fail "Locals failed"
70 tryLocals d ((x, t) : xs) = try' (tryLocal d x t) (tryLocals d xs) True
72 tryCons d [] = fail "Constructors failed"
73 tryCons d (c : cs) = try' (tryCon d c) (tryCons d cs) True
75 tryLocal d n t = do let a = getPArity (delab ist (binderTy t))
76 tryLocalArg d n a
78 tryLocalArg d n 0 = elab (PRef (fileFC "prf") n)
79 tryLocalArg d n i = simple_app (tryLocalArg d n (i - 1))
80 (psRec d) "proof search local apply"
82 -- Like type class resolution, but searching with constructors
83 tryCon d n =
84 do let imps = case lookupCtxtName n (idris_implicits ist) of
85 [] -> []
86 [args] -> map isImp (snd args)
87 _ -> fail "Ambiguous name"
88 ps <- get_probs
89 args <- apply (Var n) imps
90 ps' <- get_probs
91 when (length ps < length ps') $ fail "Can't apply constructor"
92 mapM_ (\ (_, h) -> do focus h
93 psRec d)
94 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
95 solve
97 isImp (PImp p _ _ _ _ _) = (True, p)
98 isImp arg = (False, priority arg)