git.iko.soy/Idris-dev
on fd6898e help sign in
Idris-dev/src/Idris/Core/ProofTerm.hs
365 lines 16 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}
3{- | Implements a proof state, some primitive tactics for manipulating
4proofs, and some high level commands for introducing new theorems,
5evaluation/checking inside the proof system, etc.
6-}
8module Idris.Core.ProofTerm(ProofTerm, Goal(..), mkProofTerm, getProofTerm,
9 resetProofTerm,
10 updateSolved, updateSolvedTerm, updateSolvedTerm',
11 bound_in, bound_in_term, refocus, updsubst,
12 Hole, RunTactic',
13 goal, atHole) where
15import Idris.Core.Typecheck
16import Idris.Core.Evaluate
17import Idris.Core.TT
19import Control.Monad.State.Strict
20import Data.List
21import Debug.Trace
23-- | A zipper over terms, in order to efficiently update proof terms.
24data TermPath = Top
25 | AppL (AppStatus Name) TermPath Term
26 | AppR (AppStatus Name) Term TermPath
27 | InBind Name BinderPath Term
28 | InScope Name (Binder Term) TermPath
29 deriving Show
31-- | A zipper over binders, because terms and binders are mutually defined.
32data BinderPath = Binder (Binder TermPath)
33 | LetT TermPath Term
34 | LetV Term TermPath
35 | GuessT TermPath Term
36 | GuessV Term TermPath
37 deriving Show
39-- | Replace the top of a term path with another term path. In other
40-- words, "graft" one term path into another.
41replaceTop :: TermPath -> TermPath -> TermPath
42replaceTop p Top = p
43replaceTop p (AppL s l t) = AppL s (replaceTop p l) t
44replaceTop p (AppR s t r) = AppR s t (replaceTop p r)
45replaceTop p (InBind n bp sc) = InBind n (replaceTopB p bp) sc
46 where
47 replaceTopB p (Binder b) = Binder (fmap (replaceTop p) b)
48 replaceTopB p (LetT t v) = LetT (replaceTop p t) v
49 replaceTopB p (LetV t v) = LetV t (replaceTop p v)
50 replaceTopB p (GuessT t v) = GuessT (replaceTop p t) v
51 replaceTopB p (GuessV t v) = GuessV t (replaceTop p v)
52replaceTop p (InScope n b sc) = InScope n b (replaceTop p sc)
54-- | Build a term from a zipper, given something to put in the hole.
55rebuildTerm :: Term -> TermPath -> Term
56rebuildTerm tm Top = tm
57rebuildTerm tm (AppL s p a) = App s (rebuildTerm tm p) a
58rebuildTerm tm (AppR s f p) = App s f (rebuildTerm tm p)
59rebuildTerm tm (InScope n b p) = Bind n b (rebuildTerm tm p)
60rebuildTerm tm (InBind n bp sc) = Bind n (rebuildBinder tm bp) sc
62-- | Build a binder from a zipper, given something to put in the hole.
63rebuildBinder :: Term -> BinderPath -> Binder Term
64rebuildBinder tm (Binder p) = fmap (rebuildTerm tm) p
65rebuildBinder tm (LetT p t) = Let (rebuildTerm tm p) t
66rebuildBinder tm (LetV v p) = Let v (rebuildTerm tm p)
67rebuildBinder tm (GuessT p t) = Guess (rebuildTerm tm p) t
68rebuildBinder tm (GuessV v p) = Guess v (rebuildTerm tm p)
70-- | Find the binding of a hole in a term. If present, return the path
71-- to the hole's binding, the environment extended by the binders that
72-- are crossed, and the actual binding term.
73findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)
74findHole n env t = fh' env Top t where
75 fh' env path tm@(Bind x h sc)
76 | hole h && n == x = Just (path, env, tm)
77 fh' env path (App Complete _ _) = Nothing
78 fh' env path (App s f a)
79 | Just (p, env', tm) <- fh' env path a = Just (AppR s f p, env', tm)
80 | Just (p, env', tm) <- fh' env path f = Just (AppL s p a, env', tm)
81 fh' env path (Bind x b sc)
82 | Just (bp, env', tm) <- fhB env path b = Just (InBind x bp sc, env', tm)
83 | Just (p, env', tm) <- fh' ((x,b):env) path sc = Just (InScope x b p, env', tm)
84 fh' _ _ _ = Nothing
86 fhB env path (Let t v)
87 | Just (p, env', tm) <- fh' env path t = Just (LetT p v, env', tm)
88 | Just (p, env', tm) <- fh' env path v = Just (LetV t p, env', tm)
89 fhB env path (Guess t v)
90 | Just (p, env', tm) <- fh' env path t = Just (GuessT p v, env', tm)
91 | Just (p, env', tm) <- fh' env path v = Just (GuessV t p, env', tm)
92 fhB env path b
93 | Just (p, env', tm) <- fh' env path (binderTy b)
94 = Just (Binder (fmap (\_ -> p) b), env', tm)
95 fhB _ _ _ = Nothing
97data ProofTerm = PT { -- wholeterm :: Term,
98 path :: TermPath,
99 subterm_env :: Env,
100 subterm :: Term,
101 updates :: [(Name, Term)] }
102 deriving Show
104type RunTactic' a = Context -> Env -> Term -> StateT a TC Term
105type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
107-- | Refocus the proof term zipper on a particular hole, if it
108-- exists. If not, return the original proof term.
109refocus :: Hole -> ProofTerm -> ProofTerm
110refocus h t = let res = refocus' h t in res
111-- trace ("OLD: " ++ show t ++ "\n" ++
112-- "REFOCUSSED " ++ show h ++ ": " ++ show res) res
113refocus' (Just n) pt@(PT path env tm ups)
114 -- First look for the hole in the proof term as-is
115 | Just (p', env', tm') <- findHole n env tm
116 = PT (replaceTop p' path) env' tm' ups
117 -- If it's not there, rebuild and look from the top
118 | Just (p', env', tm') <- findHole n [] (rebuildTerm tm (updateSolvedPath ups path))
119 = PT p' env' tm' []
120 | otherwise = pt
121refocus' _ pt = pt
123data Goal = GD { premises :: Env,
124 goalType :: Binder Term
125 }
127mkProofTerm :: Term -> ProofTerm
128mkProofTerm tm = PT Top [] tm []
130getProofTerm :: ProofTerm -> Term
131getProofTerm (PT path _ sub ups) = rebuildTerm sub (updateSolvedPath ups path)
133resetProofTerm :: ProofTerm -> ProofTerm
134resetProofTerm = mkProofTerm . getProofTerm
136same :: Eq a => Maybe a -> a -> Bool
137same Nothing n = True
138same (Just x) n = x == n
140-- | Is a particular binder a hole or a guess?
141hole :: Binder b -> Bool
142hole (Hole _) = True
143hole (Guess _ _) = True
144hole _ = False
146-- | Given a list of solved holes, fill out the solutions in a term
147updateSolvedTerm :: [(Name, Term)] -> Term -> Term
148updateSolvedTerm xs x = fst $ updateSolvedTerm' xs x
150-- | Given a list of solved holes, fill out the solutions in a
151-- term. Return whether updates were performed, to facilitate sharing
152-- when there are no updates.
153updateSolvedTerm' :: [(Name, Term)] -> Term -> (Term, Bool)
154updateSolvedTerm' [] x = (x, False)
155updateSolvedTerm' xs x = updateSolved' xs x where
156 -- This version below saves allocations, because it doesn't need to reallocate
157 -- the term if there are no updates to do.
158 -- The Bool is ugly, and probably 'Maybe' would be less ugly, but >>= is
159 -- the wrong combinator. Feel free to tidy up as long as it's still as cheap :).
160 updateSolved' [] x = (x, False)
161 updateSolved' xs (Bind n (Hole ty) t)
162 | Just v <- lookup n xs
163 = case xs of
164 [_] -> (updsubst n v t, True) -- some may be Vs! Can't assume
165 -- explicit names
166 _ -> let (t', _) = updateSolved' xs t in
167 (updsubst n v t', True)
168 updateSolved' xs tm@(Bind n b t)
169 | otherwise = let (t', ut) = updateSolved' xs t
170 (b', ub) = updateSolvedB' xs b in
171 if ut || ub then (Bind n b' t', True)
172 else (tm, False)
173 updateSolved' xs t@(App Complete f a) = (t, False)
174 updateSolved' xs t@(App s f a)
175 = let (f', uf) = updateSolved' xs f
176 (a', ua) = updateSolved' xs a in
177 if uf || ua then (App s f' a', True)
178 else (t, False)
179 updateSolved' xs t@(P _ n@(MN _ _) _)
180 | Just v <- lookup n xs = (v, True)
181 updateSolved' xs t@(P nt n ty)
182 = let (ty', ut) = updateSolved' xs ty in
183 if ut then (P nt n ty', True) else (t, False)
184 updateSolved' xs t = (t, False)
186 updateSolvedB' xs b@(Let t v) = let (t', ut) = updateSolved' xs t
187 (v', uv) = updateSolved' xs v in
188 if ut || uv then (Let t' v', True)
189 else (b, False)
190 updateSolvedB' xs b@(Guess t v) = let (t', ut) = updateSolved' xs t
191 (v', uv) = updateSolved' xs v in
192 if ut || uv then (Guess t' v', True)
193 else (b, False)
194 updateSolvedB' xs b = let (ty', u) = updateSolved' xs (binderTy b) in
195 if u then (b { binderTy = ty' }, u) else (b, False)
197 noneOf ns (P _ n _) | n `elem` ns = False
198 noneOf ns (App s f a) = noneOf ns a && noneOf ns f
199 noneOf ns (Bind n (Hole ty) t) = n `notElem` ns && noneOf ns ty && noneOf ns t
200 noneOf ns (Bind n b t) = noneOf ns t && noneOfB ns b
201 where
202 noneOfB ns (Let t v) = noneOf ns t && noneOf ns v
203 noneOfB ns (Guess t v) = noneOf ns t && noneOf ns v
204 noneOfB ns b = noneOf ns (binderTy b)
205 noneOf ns _ = True
207-- | As 'subst', in TT, but takes advantage of knowing not to substitute
208-- under Complete applications.
209updsubst :: Eq n => n {-^ The id to replace -} ->
210 TT n {-^ The replacement term -} ->
211 TT n {-^ The term to replace in -} ->
212 TT n
213-- subst n v tm = instantiate v (pToV n tm)
214updsubst n v tm = fst $ subst' 0 tm
215 where
216 -- keep track of updates to save allocations - this is a big win on
217 -- large terms in particular
218 -- ('Maybe' would be neater here, but >>= is not the right combinator.
219 -- Feel free to tidy up, as long as it still saves allocating when no
220 -- substitution happens...)
221 subst' i (V x) | i == x = (v, True)
222 subst' i (P _ x _) | n == x = (v, True)
223 subst' i t@(P nt x ty)
224 = let (ty', ut) = subst' i ty in
225 if ut then (P nt x ty', True) else (t, False)
226 subst' i t@(Bind x b sc) | x /= n
227 = let (b', ub) = substB' i b
228 (sc', usc) = subst' (i+1) sc in
229 if ub || usc then (Bind x b' sc', True) else (t, False)
230 subst' i t@(App Complete f a) = (t, False)
231 subst' i t@(App s f a) = let (f', uf) = subst' i f
232 (a', ua) = subst' i a in
233 if uf || ua then (App s f' a', True) else (t, False)
234 subst' i t@(Proj x idx) = let (x', u) = subst' i x in
235 if u then (Proj x' idx, u) else (t, False)
236 subst' i t = (t, False)
238 substB' i b@(Let t v) = let (t', ut) = subst' i t
239 (v', uv) = subst' i v in
240 if ut || uv then (Let t' v', True)
241 else (b, False)
242 substB' i b@(Guess t v) = let (t', ut) = subst' i t
243 (v', uv) = subst' i v in
244 if ut || uv then (Guess t' v', True)
245 else (b, False)
246 substB' i b = let (ty', u) = subst' i (binderTy b) in
247 if u then (b { binderTy = ty' }, u) else (b, False)
250-- | Apply solutions to an environment.
251updateEnv :: [(Name, Term)] -> Env -> Env
252updateEnv [] e = e
253updateEnv ns [] = []
254updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env
256-- | Fill out solved holes in a term zipper.
257updateSolvedPath :: [(Name, Term)] -> TermPath -> TermPath
258updateSolvedPath [] t = t
259updateSolvedPath ns Top = Top
260updateSolvedPath ns t@(AppL Complete _ _) = t
261updateSolvedPath ns t@(AppR Complete _ _) = t
262updateSolvedPath ns (AppL s p r) = AppL s (updateSolvedPath ns p) (updateSolvedTerm ns r)
263updateSolvedPath ns (AppR s l p) = AppR s (updateSolvedTerm ns l) (updateSolvedPath ns p)
264updateSolvedPath ns (InBind n b sc)
265 = InBind n (updateSolvedPathB b) (updateSolvedTerm ns sc)
266 where
267 updateSolvedPathB (Binder b) = Binder (fmap (updateSolvedPath ns) b)
268 updateSolvedPathB (LetT p v) = LetT (updateSolvedPath ns p) (updateSolvedTerm ns v)
269 updateSolvedPathB (LetV v p) = LetV (updateSolvedTerm ns v) (updateSolvedPath ns p)
270 updateSolvedPathB (GuessT p v) = GuessT (updateSolvedPath ns p) (updateSolvedTerm ns v)
271 updateSolvedPathB (GuessV v p) = GuessV (updateSolvedTerm ns v) (updateSolvedPath ns p)
272updateSolvedPath ns (InScope n (Hole ty) t)
273 | Just v <- lookup n ns = case ns of
274 [_] -> updateSolvedPath [(n,v)] t
275 _ -> updateSolvedPath ns $
276 updateSolvedPath [(n,v)] t
277updateSolvedPath ns (InScope n b sc)
278 = InScope n (fmap (updateSolvedTerm ns) b) (updateSolvedPath ns sc)
280updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm
281updateSolved xs pt@(PT path env sub ups)
282 = PT path -- (updateSolvedPath xs path)
283 (updateEnv xs (filter (\(n, t) -> n `notElem` map fst xs) env))
284 (updateSolvedTerm xs sub)
285 (ups ++ xs)
287goal :: Hole -> ProofTerm -> TC Goal
288goal h pt@(PT path env sub ups)
289-- | OK ginf <- g env sub = return ginf
290 | otherwise = g [] (rebuildTerm sub (updateSolvedPath ups path))
291 where
292 g :: Env -> Term -> TC Goal
293 g env (Bind n b@(Guess _ _) sc)
294 | same h n = return $ GD env b
295 | otherwise
296 = gb env b `mplus` g ((n, b):env) sc
297 g env (Bind n b sc) | hole b && same h n = return $ GD env b
298 | otherwise
299 = g ((n, b):env) sc `mplus` gb env b
300 g env (App Complete f a) = fail "Can't find hole"
301 g env (App _ f a) = g env a `mplus` g env f
302 g env t = fail "Can't find hole"
304 gb env (Let t v) = g env v `mplus` g env t
305 gb env (Guess t v) = g env v `mplus` g env t
306 gb env t = g env (binderTy t)
308atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm ->
309 StateT a TC (ProofTerm, Bool)
310atHole h f c e pt -- @(PT path env sub)
311 = do let PT path env sub ups = refocus h pt
312 (tm, u) <- atH f c env sub
313 return (PT path env tm ups, u)
314-- if u then return (PT path env tm ups, u)
315-- else do let PT path env sub ups = refocus h pt
316-- (tm, u) <- atH f c env sub
317-- return (PT path env tm ups, u)
318 where
319 updated o = do o' <- o
320 return (o', True)
322 ulift2 f c env op a b
323 = do (b', u) <- atH f c env b
324 if u then return (op a b', True)
325 else do (a', u) <- atH f c env a
326 return (op a' b', u)
328 -- Search the things most likely to contain the binding first!
330 atH :: RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
331 atH f c env binder@(Bind n b@(Guess t v) sc)
332 | same h n = updated (f c env binder)
333 | otherwise
334 = do -- binder first
335 (b', u) <- ulift2 f c env Guess t v
336 if u then return (Bind n b' sc, True)
337 else do (sc', u) <- atH f c ((n, b) : env) sc
338 return (Bind n b' sc', u)
339 atH f c env binder@(Bind n b sc)
340 | hole b && same h n = updated (f c env binder)
341 | otherwise -- scope first
342 = do (sc', u) <- atH f c ((n, b) : env) sc
343 if u then return (Bind n b sc', True)
344 else do (b', u) <- atHb f c env b
345 return (Bind n b' sc', u)
346 atH tac c env (App s f a) = ulift2 tac c env (App s) f a
347 atH tac c env t = return (t, False)
349 atHb f c env (Let t v) = ulift2 f c env Let t v
350 atHb f c env (Guess t v) = ulift2 f c env Guess t v
351 atHb f c env t = do (ty', u) <- atH f c env (binderTy t)
352 return (t { binderTy = ty' }, u)
354bound_in :: ProofTerm -> [Name]
355bound_in (PT path _ tm ups) = bound_in_term (rebuildTerm tm (updateSolvedPath ups path))
357bound_in_term :: Term -> [Name]
358bound_in_term (Bind n b sc) = n : bi b ++ bound_in_term sc
359 where
360 bi (Let t v) = bound_in_term t ++ bound_in_term v
361 bi (Guess t v) = bound_in_term t ++ bound_in_term v
362 bi b = bound_in_term (binderTy b)
363bound_in_term (App _ f a) = bound_in_term f ++ bound_in_term a
364bound_in_term _ = []