git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/Idris/ProofSearch.hs
162 lines 6.5 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 ()
42cantSolveGoal = do g <- goal
43 env <- get_env
44 lift $ tfail $
45 CantSolveGoal g (map (\(n,b) -> (n, binderTy b)) env)
47proofSearch :: Bool ->
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 Int -> -- maximum depth
52 (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->
53 IState -> ElabD ()
54proofSearch False fromProver depth elab _ nroot [fn] ist
55 = do -- get all possible versions of the name, take the first one that
56 -- works
57 let all_imps = lookupCtxtName fn (idris_implicits ist)
58 tryAllFns all_imps
59 where
60 -- if nothing worked, make a new metavariable
61 tryAllFns [] | fromProver = cantSolveGoal
62 tryAllFns [] = do attack; defer [] nroot; solve
63 tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True
65 tryFn (f, args) = do let imps = map isImp args
66 ps <- get_probs
67 hs <- get_holes
68 args <- map snd <$> try' (apply (Var f) imps)
69 (match_apply (Var f) imps) True
70 ps' <- get_probs
71-- when (length ps < length ps') $ fail "Can't apply constructor"
72 -- Make metavariables for new holes
73 hs' <- get_holes
74 ptm <- get_term
75 if fromProver then cantSolveGoal
76 else do
77 mapM_ (\ h -> do focus h
78 attack; defer [] nroot; solve)
79 (hs' \\ hs)
80-- (filter (\ (x, y) -> not x) (zip (map fst imps) args))
81 solve
83 isImp (PImp p _ _ _ _) = (True, p)
84 isImp arg = (True, priority arg) -- try to get all of them by unification
85proofSearch rec fromProver maxDepth elab fn nroot hints ist
86 = case lookupCtxt nroot (idris_tyinfodata ist) of
87 [TISolution ts] -> findInferredTy ts
88 _ -> psRec rec maxDepth
89 where
90 findInferredTy (t : _) = elab (delab ist (toUN t))
92 toUN t@(P nt (MN i n) ty)
93 | ('_':xs) <- str n = t
94 | otherwise = P nt (UN n) ty
95 toUN (App f a) = App (toUN f) (toUN a)
96 toUN t = t
98 psRec _ 0 | fromProver = cantSolveGoal
99 psRec rec 0 = do attack; defer [] nroot; solve --fail "Maximum depth reached"
100 psRec False d = tryCons d hints
101 psRec True d = try' (trivial elab ist)
102 (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))
103 True)
104 -- if all else fails, make a new metavariable
105 (if fromProver
106 then cantSolveGoal
107 else do attack; defer [] nroot; solve) True) True
109 getFn d Nothing = []
110 getFn d (Just f) | d < maxDepth-1 = [f]
111 | otherwise = []
113 resolveByCon d
114 = do t <- goal
115 let (f, _) = unApply t
116 case f of
117 P _ n _ -> case lookupCtxt n (idris_datatypes ist) of
118 [t] -> tryCons d (hints ++ con_names t ++
119 getFn d fn)
120 _ -> fail "Not a data type"
121 _ -> fail "Not a data type"
123 -- if there are local variables which have a function type, try
124 -- applying them too
125 resolveByLocals d
126 = do env <- get_env
127 tryLocals d env
129 tryLocals d [] = fail "Locals failed"
130 tryLocals d ((x, t) : xs) = try' (tryLocal d x t) (tryLocals d xs) True
132 tryCons d [] = fail "Constructors failed"
133 tryCons d (c : cs) = try' (tryCon d c) (tryCons d cs) True
135 tryLocal d n t = do let a = getPArity (delab ist (binderTy t))
136 tryLocalArg d n a
138 tryLocalArg d n 0 = elab (PRef (fileFC "prf") n)
139 tryLocalArg d n i = simple_app (tryLocalArg d n (i - 1))
140 (psRec True d) "proof search local apply"
142 -- Like type class resolution, but searching with constructors
143 tryCon d n =
144 do let imps = case lookupCtxtName n (idris_implicits ist) of
145 [] -> []
146 [args] -> map isImp (snd args)
147 _ -> fail "Ambiguous name"
148 ps <- get_probs
149 hs <- get_holes
150 args <- map snd <$> try' (apply (Var n) imps)
151 (match_apply (Var n) imps) True
152 ps' <- get_probs
153 hs' <- get_holes
154 when (length ps < length ps') $ fail "Can't apply constructor"
155 mapM_ (\ (_, h) -> do focus h
156 psRec True d)
157 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
158 solve
160 isImp (PImp p _ _ _ _) = (True, p)
161 isImp arg = (False, priority arg)