git.iko.soy/Idris-dev
on 76ec3fe help sign in
Idris-dev/src/Idris/Core/ProofTerm.hs
313 lines 14 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 updateSolved, updateSolvedTerm, updateSolvedTerm',
10 bound_in, bound_in_term, refocus,
11 Hole, RunTactic',
12 goal, atHole) where
14import Idris.Core.Typecheck
15import Idris.Core.Evaluate
16import Idris.Core.TT
18import Control.Monad.State.Strict
19import Data.List
20import Debug.Trace
22-- | A zipper over terms, in order to efficiently update proof terms.
23data TermPath = Top
24 | AppL TermPath Term
25 | AppR Term TermPath
26 | InBind Name BinderPath Term
27 | InScope Name (Binder Term) TermPath
28 deriving Show
30-- | A zipper over binders, because terms and binders are mutually defined.
31data BinderPath = Binder (Binder TermPath)
32 | LetT TermPath Term
33 | LetV Term TermPath
34 | GuessT TermPath Term
35 | GuessV Term TermPath
36 deriving Show
38-- | Replace the top of a term path with another term path. In other
39-- words, "graft" one term path into another.
40replaceTop :: TermPath -> TermPath -> TermPath
41replaceTop p Top = p
42replaceTop p (AppL l t) = AppL (replaceTop p l) t
43replaceTop p (AppR t r) = AppR t (replaceTop p r)
44replaceTop p (InBind n bp sc) = InBind n (replaceTopB p bp) sc
45 where
46 replaceTopB p (Binder b) = Binder (fmap (replaceTop p) b)
47 replaceTopB p (LetT t v) = LetT (replaceTop p t) v
48 replaceTopB p (LetV t v) = LetV t (replaceTop p v)
49 replaceTopB p (GuessT t v) = GuessT (replaceTop p t) v
50 replaceTopB p (GuessV t v) = GuessV t (replaceTop p v)
51replaceTop p (InScope n b sc) = InScope n b (replaceTop p sc)
53-- | Build a term from a zipper, given something to put in the hole.
54rebuildTerm :: Term -> TermPath -> Term
55rebuildTerm tm Top = tm
56rebuildTerm tm (AppL p a) = App (rebuildTerm tm p) a
57rebuildTerm tm (AppR f p) = App f (rebuildTerm tm p)
58rebuildTerm tm (InScope n b p) = Bind n b (rebuildTerm tm p)
59rebuildTerm tm (InBind n bp sc) = Bind n (rebuildBinder tm bp) sc
61-- | Build a binder from a zipper, given something to put in the hole.
62rebuildBinder :: Term -> BinderPath -> Binder Term
63rebuildBinder tm (Binder p) = fmap (rebuildTerm tm) p
64rebuildBinder tm (LetT p t) = Let (rebuildTerm tm p) t
65rebuildBinder tm (LetV v p) = Let v (rebuildTerm tm p)
66rebuildBinder tm (GuessT p t) = Guess (rebuildTerm tm p) t
67rebuildBinder tm (GuessV v p) = Guess v (rebuildTerm tm p)
69-- | Find the binding of a hole in a term. If present, return the path
70-- to the hole's binding, the environment extended by the binders that
71-- are crossed, and the actual binding term.
72findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)
73findHole n env t = fh' env Top t where
74 fh' env path tm@(Bind x h sc)
75 | hole h && n == x = Just (path, env, tm)
76 fh' env path (App f a)
77 | Just (p, env', tm) <- fh' env path a = Just (AppR f p, env', tm)
78 | Just (p, env', tm) <- fh' env path f = Just (AppL p a, env', tm)
79 fh' env path (Bind x b sc)
80 | Just (bp, env', tm) <- fhB env path b = Just (InBind x bp sc, env', tm)
81 | Just (p, env', tm) <- fh' ((x,b):env) path sc = Just (InScope x b p, env', tm)
82 fh' _ _ _ = Nothing
84 fhB env path (Let t v)
85 | Just (p, env', tm) <- fh' env path t = Just (LetT p v, env', tm)
86 | Just (p, env', tm) <- fh' env path v = Just (LetV t p, env', tm)
87 fhB env path (Guess t v)
88 | Just (p, env', tm) <- fh' env path t = Just (GuessT p v, env', tm)
89 | Just (p, env', tm) <- fh' env path v = Just (GuessV t p, env', tm)
90 fhB env path b
91 | Just (p, env', tm) <- fh' env path (binderTy b)
92 = Just (Binder (fmap (\_ -> p) b), env', tm)
93 fhB _ _ _ = Nothing
95data ProofTerm = PT { -- wholeterm :: Term,
96 path :: TermPath,
97 subterm_env :: Env,
98 subterm :: Term,
99 updates :: [(Name, Term)] }
100 deriving Show
102type RunTactic' a = Context -> Env -> Term -> StateT a TC Term
103type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
105-- | Refocus the proof term zipper on a particular hole, if it
106-- exists. If not, return the original proof term.
107refocus :: Hole -> ProofTerm -> ProofTerm
108refocus h t = let res = refocus' h t in res
109-- trace ("OLD: " ++ show t ++ "\n" ++
110-- "REFOCUSSED " ++ show h ++ ": " ++ show res) res
111refocus' (Just n) pt@(PT path env tm ups)
112 -- First look for the hole in the proof term as-is
113 | Just (p', env', tm') <- findHole n env tm
114 = PT (replaceTop p' path) env' tm' ups
115 -- Next apply the updates, and look for the hole in the resulting term
116 | Just (p', env', tm') <- findHole n [] (rebuildTerm tm (updateSolvedPath ups path))
117 = PT p' env' tm' []
118 | otherwise = pt
119refocus' _ pt = pt
121data Goal = GD { premises :: Env,
122 goalType :: Binder Term
123 }
125mkProofTerm :: Term -> ProofTerm
126mkProofTerm tm = PT Top [] tm []
128getProofTerm :: ProofTerm -> Term
129getProofTerm (PT path _ sub ups) = rebuildTerm sub (updateSolvedPath ups path)
131same :: Eq a => Maybe a -> a -> Bool
132same Nothing n = True
133same (Just x) n = x == n
135-- | Is a particular binder a hole or a guess?
136hole :: Binder b -> Bool
137hole (Hole _) = True
138hole (Guess _ _) = True
139hole _ = False
141-- | Given a list of solved holes, fill out the solutions in a term
142updateSolvedTerm :: [(Name, Term)] -> Term -> Term
143updateSolvedTerm xs x = fst $ updateSolvedTerm' xs x
145-- | Given a list of solved holes, fill out the solutions in a
146-- term. Return whether updates were performed, to facilitate sharing
147-- when there are no updates.
148updateSolvedTerm' :: [(Name, Term)] -> Term -> (Term, Bool)
149updateSolvedTerm' [] x = (x, False)
150updateSolvedTerm' xs x = updateSolved' xs x where
151 -- This version below saves allocations, because it doesn't need to reallocate
152 -- the term if there are no updates to do.
153 -- The Bool is ugly, and probably 'Maybe' would be less ugly, but >>= is
154 -- the wrong combinator. Feel free to tidy up as long as it's still as cheap :).
155 updateSolved' [] x = (x, False)
156 updateSolved' xs (Bind n (Hole ty) t)
157 | Just v <- lookup n xs
158 = case xs of
159 [_] -> (subst n v t, True) -- some may be Vs! Can't assume
160 -- explicit names
161 _ -> let (t', _) = updateSolved' xs t in
162 (subst n v t', True)
163 updateSolved' xs tm@(Bind n b t)
164 | otherwise = let (t', ut) = updateSolved' xs t
165 (b', ub) = updateSolvedB' xs b in
166 if ut || ub then (Bind n b' t', True)
167 else (tm, False)
168 updateSolved' xs t@(App f a)
169 = let (f', uf) = updateSolved' xs f
170 (a', ua) = updateSolved' xs a in
171 if uf || ua then (App f' a', True)
172 else (t, False)
173 updateSolved' xs t@(P _ n@(MN _ _) _)
174 | Just v <- lookup n xs = (v, True)
175 updateSolved' xs t@(P nt n ty)
176 = let (ty', ut) = updateSolved' xs ty in
177 if ut then (P nt n ty', True) else (t, False)
178 updateSolved' xs t = (t, False)
180 updateSolvedB' xs b@(Let t v) = let (t', ut) = updateSolved' xs t
181 (v', uv) = updateSolved' xs v in
182 if ut || uv then (Let t' v', True)
183 else (b, False)
184 updateSolvedB' xs b@(Guess t v) = let (t', ut) = updateSolved' xs t
185 (v', uv) = updateSolved' xs v in
186 if ut || uv then (Guess t' v', True)
187 else (b, False)
188 updateSolvedB' xs b = let (ty', u) = updateSolved' xs (binderTy b) in
189 if u then (b { binderTy = ty' }, u) else (b, False)
191 noneOf ns (P _ n _) | n `elem` ns = False
192 noneOf ns (App f a) = noneOf ns a && noneOf ns f
193 noneOf ns (Bind n (Hole ty) t) = n `notElem` ns && noneOf ns ty && noneOf ns t
194 noneOf ns (Bind n b t) = noneOf ns t && noneOfB ns b
195 where
196 noneOfB ns (Let t v) = noneOf ns t && noneOf ns v
197 noneOfB ns (Guess t v) = noneOf ns t && noneOf ns v
198 noneOfB ns b = noneOf ns (binderTy b)
199 noneOf ns _ = True
201-- | Apply solutions to an environment.
202updateEnv :: [(Name, Term)] -> Env -> Env
203updateEnv [] e = e
204updateEnv ns [] = []
205updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env
207-- | Fill out solved holes in a term zipper.
208updateSolvedPath :: [(Name, Term)] -> TermPath -> TermPath
209updateSolvedPath [] t = t
210updateSolvedPath ns Top = Top
211updateSolvedPath ns (AppL p r) = AppL (updateSolvedPath ns p) (updateSolvedTerm ns r)
212updateSolvedPath ns (AppR l p) = AppR (updateSolvedTerm ns l) (updateSolvedPath ns p)
213updateSolvedPath ns (InBind n b sc)
214 = InBind n (updateSolvedPathB b) (updateSolvedTerm ns sc)
215 where
216 updateSolvedPathB (Binder b) = Binder (fmap (updateSolvedPath ns) b)
217 updateSolvedPathB (LetT p v) = LetT (updateSolvedPath ns p) (updateSolvedTerm ns v)
218 updateSolvedPathB (LetV v p) = LetV (updateSolvedTerm ns v) (updateSolvedPath ns p)
219 updateSolvedPathB (GuessT p v) = GuessT (updateSolvedPath ns p) (updateSolvedTerm ns v)
220 updateSolvedPathB (GuessV v p) = GuessV (updateSolvedTerm ns v) (updateSolvedPath ns p)
221updateSolvedPath ns (InScope n (Hole ty) t)
222 | Just v <- lookup n ns = case ns of
223 [_] -> updateSolvedPath [(n,v)] t
224 _ -> updateSolvedPath ns $
225 updateSolvedPath [(n,v)] t
226updateSolvedPath ns (InScope n b sc)
227 = InScope n (fmap (updateSolvedTerm ns) b) (updateSolvedPath ns sc)
229updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm
230updateSolved xs pt@(PT path env sub ups)
231 = PT path -- (updateSolvedPath xs path)
232 (updateEnv xs (filter (\(n, t) -> n `notElem` map fst xs) env))
233 (updateSolvedTerm xs sub)
234 (ups ++ xs)
236goal :: Hole -> ProofTerm -> TC Goal
237goal h pt@(PT path env sub ups)
238-- | OK ginf <- g env sub = return ginf
239 | otherwise = g [] (rebuildTerm sub (updateSolvedPath ups path))
240 where
241 g :: Env -> Term -> TC Goal
242 g env (Bind n b@(Guess _ _) sc)
243 | same h n = return $ GD env b
244 | otherwise
245 = gb env b `mplus` g ((n, b):env) sc
246 g env (Bind n b sc) | hole b && same h n = return $ GD env b
247 | otherwise
248 = g ((n, b):env) sc `mplus` gb env b
249 g env (App f a) = g env a `mplus` g env f
250 g env t = fail "Can't find hole"
252 gb env (Let t v) = g env v `mplus` g env t
253 gb env (Guess t v) = g env v `mplus` g env t
254 gb env t = g env (binderTy t)
256atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm ->
257 StateT a TC (ProofTerm, Bool)
258atHole h f c e pt -- @(PT path env sub)
259 = do let PT path env sub ups = refocus h pt
260 (tm, u) <- atH f c env sub
261 return (PT path env tm ups, u)
262-- if u then return (PT path env tm ups, u)
263-- else do let PT path env sub ups = refocus h pt
264-- (tm, u) <- atH f c env sub
265-- return (PT path env tm ups, u)
266 where
267 updated o = do o' <- o
268 return (o', True)
270 ulift2 f c env op a b
271 = do (b', u) <- atH f c env b
272 if u then return (op a b', True)
273 else do (a', u) <- atH f c env a
274 return (op a' b', u)
276 -- Search the things most likely to contain the binding first!
278 atH :: RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
279 atH f c env binder@(Bind n b@(Guess t v) sc)
280 | same h n = updated (f c env binder)
281 | otherwise
282 = do -- binder first
283 (b', u) <- ulift2 f c env Guess t v
284 if u then return (Bind n b' sc, True)
285 else do (sc', u) <- atH f c ((n, b) : env) sc
286 return (Bind n b' sc', u)
287 atH f c env binder@(Bind n b sc)
288 | hole b && same h n = updated (f c env binder)
289 | otherwise -- scope first
290 = do (sc', u) <- atH f c ((n, b) : env) sc
291 if u then return (Bind n b sc', True)
292 else do (b', u) <- atHb f c env b
293 return (Bind n b' sc', u)
294 atH tac c env (App f a) = ulift2 tac c env App f a
295 atH tac c env t = return (t, False)
297 atHb f c env (Let t v) = ulift2 f c env Let t v
298 atHb f c env (Guess t v) = ulift2 f c env Guess t v
299 atHb f c env t = do (ty', u) <- atH f c env (binderTy t)
300 return (t { binderTy = ty' }, u)
302bound_in :: ProofTerm -> [Name]
303bound_in (PT path _ tm ups) = bound_in_term (rebuildTerm tm (updateSolvedPath ups path))
305bound_in_term :: Term -> [Name]
306bound_in_term (Bind n b sc) = n : bi b ++ bound_in_term sc
307 where
308 bi (Let t v) = bound_in_term t ++ bound_in_term v
309 bi (Guess t v) = bound_in_term t ++ bound_in_term v
310 bi b = bound_in_term (binderTy b)
311bound_in_term (App f a) = bound_in_term f ++ bound_in_term a
312bound_in_term _ = []