git.iko.soy/Idris-dev
on dda9b49 help sign in
Idris-dev/src/Idris/ProofSearch.hs
147 lines 5.7 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 Data.List
18import Debug.Trace
20-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm
22trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()
23trivial elab ist = try' (do elab (PRefl (fileFC "prf") Placeholder)
24 return ())
25 (do env <- get_env
26 g <- goal
27 tryAll env
28 return ()) True
29 where
30 tryAll [] = fail "No trivial solution"
31 tryAll ((x, b):xs)
32 = do -- if type of x has any holes in it, move on
33 hs <- get_holes
34 g <- goal
35 if all (\n -> not (n `elem` hs)) (freeNames (binderTy b))
36 then try' (elab (PRef (fileFC "prf") x))
37 (tryAll xs) True
38 else tryAll xs
40proofSearch :: Bool ->
41 (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->
42 IState -> ElabD ()
43proofSearch False elab _ nroot [fn] ist
44 = do -- get all possible versions of the name, take the first one that
45 -- works
46 let all_imps = lookupCtxtName fn (idris_implicits ist)
47 tryAllFns all_imps
48 where
49 -- if nothing worked, make a new metavariable
50 tryAllFns [] = do attack; defer nroot; solve
51 tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True
53 tryFn (f, args) = do let imps = map isImp args
54 ps <- get_probs
55 hs <- get_holes
56 args <- map snd <$> try' (apply (Var f) imps)
57 (match_apply (Var f) imps) True
58 ps' <- get_probs
59-- when (length ps < length ps') $ fail "Can't apply constructor"
60 -- Make metavariables for new holes
61 hs' <- get_holes
62 ptm <- get_term
63 mapM_ (\ h -> do focus h
64 attack; defer nroot; solve)
65 (hs' \\ hs)
66-- (filter (\ (x, y) -> not x) (zip (map fst imps) args))
67 solve
69 isImp (PImp p _ _ _ _) = (True, p)
70 isImp arg = (True, priority arg) -- try to get all of them by unification
71proofSearch rec elab fn nroot hints ist
72 = case lookupCtxt nroot (idris_tyinfodata ist) of
73 [TISolution ts] -> findInferredTy ts
74 _ -> psRec rec maxDepth
75 where
76 maxDepth = 6
78 findInferredTy (t : _) = elab (delab ist (toUN t))
80 toUN t@(P nt (MN i n) ty)
81 | ('_':xs) <- str n = t
82 | otherwise = P nt (UN n) ty
83 toUN (App f a) = App (toUN f) (toUN a)
84 toUN t = t
86 psRec rec 0 = do attack; defer nroot; solve --fail "Maximum depth reached"
87 psRec False d = tryCons d hints
88 psRec True d = try' (trivial elab ist)
89 (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))
90 True)
91 -- if all else fails, make a new metavariable
92 (do attack; defer nroot; solve) True) True
94 getFn d Nothing = []
95 getFn d (Just f) | d < maxDepth-1 = [f]
96 | otherwise = []
98 resolveByCon d
99 = do t <- goal
100 let (f, _) = unApply t
101 case f of
102 P _ n _ -> case lookupCtxt n (idris_datatypes ist) of
103 [t] -> tryCons d (hints ++ con_names t ++
104 getFn d fn)
105 _ -> fail "Not a data type"
106 _ -> fail "Not a data type"
108 -- if there are local variables which have a function type, try
109 -- applying them too
110 resolveByLocals d
111 = do env <- get_env
112 tryLocals d env
114 tryLocals d [] = fail "Locals failed"
115 tryLocals d ((x, t) : xs) = try' (tryLocal d x t) (tryLocals d xs) True
117 tryCons d [] = fail "Constructors failed"
118 tryCons d (c : cs) = try' (tryCon d c) (tryCons d cs) True
120 tryLocal d n t = do let a = getPArity (delab ist (binderTy t))
121 tryLocalArg d n a
123 tryLocalArg d n 0 = elab (PRef (fileFC "prf") n)
124 tryLocalArg d n i = simple_app (tryLocalArg d n (i - 1))
125 (psRec True d) "proof search local apply"
127 -- Like type class resolution, but searching with constructors
128 tryCon d n =
129 do let imps = case lookupCtxtName n (idris_implicits ist) of
130 [] -> []
131 [args] -> map isImp (snd args)
132 _ -> fail "Ambiguous name"
133 ps <- get_probs
134 hs <- get_holes
135 args <- map snd <$> try' (apply (Var n) imps)
136 (match_apply (Var n) imps) True
137 ps' <- get_probs
138 hs' <- get_holes
139 when (length ps < length ps') $ fail "Can't apply constructor"
140 mapM_ (\ (_, h) -> do focus h
141 psRec True d)
142 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
143 solve
145 isImp (PImp p _ _ _ _) = (True, p)
146 isImp arg = (False, priority arg)