git.iko.soy/Idris-dev
on dd09721 help sign in
Idris-dev/src/Idris/ProofSearch.hs
114 lines 4.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 Debug.Trace
19-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm
21trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()
22trivial elab ist = try' (do elab (PRefl (fileFC "prf") Placeholder)
23 return ())
24 (do env <- get_env
25 g <- goal
26 tryAll env
27 return ()) True
28 where
29 tryAll [] = fail "No trivial solution"
30 tryAll ((x, b):xs)
31 = do -- if type of x has any holes in it, move on
32 hs <- get_holes
33 g <- goal
34 if all (\n -> not (n `elem` hs)) (freeNames (binderTy b))
35 then try' (elab (PRef (fileFC "prf") x))
36 (tryAll xs) True
37 else tryAll xs
39proofSearch :: (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->
40 IState -> ElabD ()
41proofSearch elab fn nroot hints ist
42 = case lookupCtxt nroot (idris_tyinfodata ist) of
43 [TISolution ts] -> findInferredTy ts
44 _ -> psRec maxDepth
45 where
46 maxDepth = 6
48 findInferredTy (t : _) = elab (delab ist (toUN t))
50 toUN t@(P nt (MN i n) ty)
51 | ('_':xs) <- str n = t
52 | otherwise = P nt (UN n) ty
53 toUN (App f a) = App (toUN f) (toUN a)
54 toUN t = t
56 psRec 0 = do attack; defer nroot; solve --fail "Maximum depth reached"
57 psRec d = try' (trivial elab ist)
58 (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))
59 True)
60 -- if all else fails, make a new metavariable
61 (do attack; defer nroot; solve) True) True
63 getFn d Nothing = []
64 getFn d (Just f) | d < maxDepth-1 = [f]
65 | otherwise = []
67 resolveByCon d
68 = do t <- goal
69 let (f, _) = unApply t
70 case f of
71 P _ n _ -> case lookupCtxt n (idris_datatypes ist) of
72 [t] -> tryCons d (hints ++ con_names t ++
73 getFn d fn)
74 _ -> fail "Not a data type"
75 _ -> fail "Not a data type"
77 -- if there are local variables which have a function type, try
78 -- applying them too
79 resolveByLocals d
80 = do env <- get_env
81 tryLocals d env
83 tryLocals d [] = fail "Locals failed"
84 tryLocals d ((x, t) : xs) = try' (tryLocal d x t) (tryLocals d xs) True
86 tryCons d [] = fail "Constructors failed"
87 tryCons d (c : cs) = try' (tryCon d c) (tryCons d cs) True
89 tryLocal d n t = do let a = getPArity (delab ist (binderTy t))
90 tryLocalArg d n a
92 tryLocalArg d n 0 = elab (PRef (fileFC "prf") n)
93 tryLocalArg d n i = simple_app (tryLocalArg d n (i - 1))
94 (psRec d) "proof search local apply"
96 -- Like type class resolution, but searching with constructors
97 tryCon d n =
98 do let imps = case lookupCtxtName n (idris_implicits ist) of
99 [] -> []
100 [args] -> map isImp (snd args)
101 _ -> fail "Ambiguous name"
102 ps <- get_probs
103 args <- map snd <$> try' (apply (Var n) imps)
104 (match_apply (Var n) imps) True
105 ps' <- get_probs
106 when (length ps < length ps') $ fail "Can't apply constructor"
107 mapM_ (\ (_, h) -> do focus h
108 psRec d)
109 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
110 solve
112 isImp (PImp p _ _ _ _) = (True, p)
113 isImp arg = (False, priority arg)