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