git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/Idris/Core/ProofTerm.hs
285 lines 12 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}
3{- Implements a proof state, some primitive tactics for manipulating
4 proofs, and some high level commands for introducing new theorems,
5 evaluation/checking inside the proof system, etc. --}
7module Idris.Core.ProofTerm(ProofTerm, Goal(..), mkProofTerm, getProofTerm,
8 updateSolved, updateSolvedTerm,
9 bound_in, bound_in_term, refocus,
10 Hole, RunTactic',
11 goal, atHole) where
13import Idris.Core.Typecheck
14import Idris.Core.Evaluate
15import Idris.Core.TT
17import Control.Monad.State.Strict
18import Data.List
19import Debug.Trace
21data TermPath = Top
22 | AppL TermPath Term
23 | AppR Term TermPath
24 | InBind Name BinderPath Term
25 | InScope Name (Binder Term) TermPath
26 deriving Show
28data BinderPath = Binder (Binder TermPath)
29 | LetT TermPath Term
30 | LetV Term TermPath
31 | GuessT TermPath Term
32 | GuessV Term TermPath
33 deriving Show
35replaceTop :: TermPath -> TermPath -> TermPath
36replaceTop p Top = p
37replaceTop p (AppL l t) = AppL (replaceTop p l) t
38replaceTop p (AppR t r) = AppR t (replaceTop p r)
39replaceTop p (InBind n bp sc) = InBind n (replaceTopB p bp) sc
40 where
41 replaceTopB p (Binder b) = Binder (fmap (replaceTop p) b)
42 replaceTopB p (LetT t v) = LetT (replaceTop p t) v
43 replaceTopB p (LetV t v) = LetV t (replaceTop p v)
44 replaceTopB p (GuessT t v) = GuessT (replaceTop p t) v
45 replaceTopB p (GuessV t v) = GuessV t (replaceTop p v)
46replaceTop p (InScope n b sc) = InScope n b (replaceTop p sc)
48rebuildTerm :: Term -> TermPath -> Term
49rebuildTerm tm Top = tm
50rebuildTerm tm (AppL p a) = App (rebuildTerm tm p) a
51rebuildTerm tm (AppR f p) = App f (rebuildTerm tm p)
52rebuildTerm tm (InScope n b p) = Bind n b (rebuildTerm tm p)
53rebuildTerm tm (InBind n bp sc) = Bind n (rebuildBinder tm bp) sc
55rebuildBinder :: Term -> BinderPath -> Binder Term
56rebuildBinder tm (Binder p) = fmap (rebuildTerm tm) p
57rebuildBinder tm (LetT p t) = Let (rebuildTerm tm p) t
58rebuildBinder tm (LetV v p) = Let v (rebuildTerm tm p)
59rebuildBinder tm (GuessT p t) = Guess (rebuildTerm tm p) t
60rebuildBinder tm (GuessV v p) = Guess v (rebuildTerm tm p)
62findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)
63findHole n env t = fh' env Top t where
64 fh' env path tm@(Bind x h sc)
65 | hole h && n == x = Just (path, env, tm)
66 fh' env path (App f a)
67 | Just (p, env', tm) <- fh' env path a = Just (AppR f p, env', tm)
68 | Just (p, env', tm) <- fh' env path f = Just (AppL p a, env', tm)
69 fh' env path (Bind x b sc)
70 | Just (bp, env', tm) <- fhB env path b = Just (InBind x bp sc, env', tm)
71 | Just (p, env', tm) <- fh' ((x,b):env) path sc = Just (InScope x b p, env', tm)
72 fh' _ _ _ = Nothing
74 fhB env path (Let t v)
75 | Just (p, env', tm) <- fh' env path t = Just (LetT p v, env', tm)
76 | Just (p, env', tm) <- fh' env path v = Just (LetV t p, env', tm)
77 fhB env path (Guess t v)
78 | Just (p, env', tm) <- fh' env path t = Just (GuessT p v, env', tm)
79 | Just (p, env', tm) <- fh' env path v = Just (GuessV t p, env', tm)
80 fhB env path b
81 | Just (p, env', tm) <- fh' env path (binderTy b)
82 = Just (Binder (fmap (\_ -> p) b), env', tm)
83 fhB _ _ _ = Nothing
85data ProofTerm = PT { -- wholeterm :: Term,
86 path :: TermPath,
87 subterm_env :: Env,
88 subterm :: Term,
89 updates :: [(Name, Term)] }
90 deriving Show
92type RunTactic' a = Context -> Env -> Term -> StateT a TC Term
93type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
95refocus :: Hole -> ProofTerm -> ProofTerm
96refocus h t = let res = refocus' h t in res
97-- trace ("OLD: " ++ show t ++ "\n" ++
98-- "REFOCUSSED " ++ show h ++ ": " ++ show res) res
99refocus' (Just n) pt@(PT path env tm ups)
100 | Just (p', env', tm') <- findHole n env tm
101 = PT (replaceTop p' path) env' tm' ups
102 | Just (p', env', tm') <- findHole n [] (rebuildTerm tm (updateSolvedPath ups path))
103 = PT p' env' tm' []
104 | otherwise = pt
105refocus' _ pt = pt
107data Goal = GD { premises :: Env,
108 goalType :: Binder Term
109 }
111mkProofTerm :: Term -> ProofTerm
112mkProofTerm tm = PT Top [] tm []
114getProofTerm :: ProofTerm -> Term
115getProofTerm (PT path _ sub ups) = rebuildTerm sub (updateSolvedPath ups path)
117same :: Eq a => Maybe a -> a -> Bool
118same Nothing n = True
119same (Just x) n = x == n
121hole :: Binder b -> Bool
122hole (Hole _) = True
123hole (Guess _ _) = True
124hole _ = False
126updateSolvedTerm :: [(Name, Term)] -> Term -> Term
127updateSolvedTerm [] x = x
128updateSolvedTerm xs x = -- updateSolved' xs x where
129-- This version below saves allocations, because it doesn't need to reallocate
130-- the term if there are no updates to do.
131-- The Bool is ugly, and probably 'Maybe' would be less ugly, but >>= is
132-- the wrong combinator. Feel free to tidy up as long as it's still as cheap :).
133 fst $ updateSolved' xs x where
134 updateSolved' [] x = (x, False)
135 updateSolved' xs (Bind n (Hole ty) t)
136 | Just v <- lookup n xs
137 = case xs of
138 [_] -> (subst n v t, True) -- some may be Vs! Can't assume
139 -- explicit names
140 _ -> let (t', _) = updateSolved' xs t in
141 (subst n v t', True)
142 updateSolved' xs tm@(Bind n b t)
143 | otherwise = let (t', ut) = updateSolved' xs t
144 (b', ub) = updateSolvedB' xs b in
145 if ut || ub then (Bind n b' t', True)
146 else (tm, False)
147 updateSolved' xs t@(App f a)
148 = let (f', uf) = updateSolved' xs f
149 (a', ua) = updateSolved' xs a in
150 if uf || ua then (App f' a', True)
151 else (t, False)
152 updateSolved' xs t@(P _ n@(MN _ _) _)
153 | Just v <- lookup n xs = (v, True)
154 updateSolved' xs t = (t, False)
156 updateSolvedB' xs b@(Let t v) = let (t', ut) = updateSolved' xs t
157 (v', uv) = updateSolved' xs v in
158 if ut || uv then (Let t' v', True)
159 else (b, False)
160 updateSolvedB' xs b@(Guess t v) = let (t', ut) = updateSolved' xs t
161 (v', uv) = updateSolved' xs v in
162 if ut || uv then (Guess t' v', True)
163 else (b, False)
164 updateSolvedB' xs b = let (ty', u) = updateSolved' xs (binderTy b) in
165 if u then (b { binderTy = ty' }, u) else (b, False)
167 noneOf ns (P _ n _) | n `elem` ns = False
168 noneOf ns (App f a) = noneOf ns a && noneOf ns f
169 noneOf ns (Bind n (Hole ty) t) = n `notElem` ns && noneOf ns ty && noneOf ns t
170 noneOf ns (Bind n b t) = noneOf ns t && noneOfB ns b
171 where
172 noneOfB ns (Let t v) = noneOf ns t && noneOf ns v
173 noneOfB ns (Guess t v) = noneOf ns t && noneOf ns v
174 noneOfB ns b = noneOf ns (binderTy b)
175 noneOf ns _ = True
177updateEnv [] e = e
178updateEnv ns [] = []
179updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env
181updateSolvedPath [] t = t
182updateSolvedPath ns Top = Top
183updateSolvedPath ns (AppL p r) = AppL p (updateSolvedTerm ns r)
184updateSolvedPath ns (AppR l p) = AppR (updateSolvedTerm ns l) p
185updateSolvedPath ns (InBind n b sc)
186 = InBind n (updateSolvedPathB b) (updateSolvedTerm ns sc)
187 where
188 updateSolvedPathB (Binder b) = Binder (fmap (updateSolvedPath ns) b)
189 updateSolvedPathB (LetT p v) = LetT (updateSolvedPath ns p) (updateSolvedTerm ns v)
190 updateSolvedPathB (LetV v p) = LetV (updateSolvedTerm ns v) (updateSolvedPath ns p)
191 updateSolvedPathB (GuessT p v) = GuessT (updateSolvedPath ns p) (updateSolvedTerm ns v)
192 updateSolvedPathB (GuessV v p) = GuessV (updateSolvedTerm ns v) (updateSolvedPath ns p)
193updateSolvedPath ns (InScope n (Hole ty) t)
194 | Just v <- lookup n ns = case ns of
195 [_] -> updateSolvedPath [(n,v)] t
196 _ -> updateSolvedPath ns $
197 updateSolvedPath [(n,v)] t
198updateSolvedPath ns (InScope n b sc)
199 = InScope n (fmap (updateSolvedTerm ns) b) (updateSolvedPath ns sc)
201updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm
202updateSolved xs pt@(PT path env sub ups)
203 = PT path -- (updateSolvedPath xs path)
204 (updateEnv xs (filter (\(n, t) -> n `notElem` map fst xs) env))
205 (updateSolvedTerm xs sub)
206 (ups ++ xs)
208goal :: Hole -> ProofTerm -> TC Goal
209goal h pt@(PT path env sub ups)
210-- | OK ginf <- g env sub = return ginf
211 | otherwise = g [] (rebuildTerm sub (updateSolvedPath ups path))
212 where
213 g :: Env -> Term -> TC Goal
214 g env (Bind n b@(Guess _ _) sc)
215 | same h n = return $ GD env b
216 | otherwise
217 = gb env b `mplus` g ((n, b):env) sc
218 g env (Bind n b sc) | hole b && same h n = return $ GD env b
219 | otherwise
220 = g ((n, b):env) sc `mplus` gb env b
221 g env (App f a) = g env a `mplus` g env f
222 g env t = fail "Can't find hole"
224 gb env (Let t v) = g env v `mplus` g env t
225 gb env (Guess t v) = g env v `mplus` g env t
226 gb env t = g env (binderTy t)
228atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm ->
229 StateT a TC (ProofTerm, Bool)
230atHole h f c e pt -- @(PT path env sub)
231 = do let PT path env sub ups = refocus h pt
232 (tm, u) <- atH f c env sub
233 return (PT path env tm ups, u)
234-- if u then return (PT path env tm ups, u)
235-- else do let PT path env sub ups = refocus h pt
236-- (tm, u) <- atH f c env sub
237-- return (PT path env tm ups, u)
238 where
239 updated o = do o' <- o
240 return (o', True)
242 ulift2 f c env op a b
243 = do (b', u) <- atH f c env b
244 if u then return (op a b', True)
245 else do (a', u) <- atH f c env a
246 return (op a' b', u)
248 -- Search the things most likely to contain the binding first!
250 atH :: RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
251 atH f c env binder@(Bind n b@(Guess t v) sc)
252 | same h n = updated (f c env binder)
253 | otherwise
254 = do -- binder first
255 (b', u) <- ulift2 f c env Guess t v
256 if u then return (Bind n b' sc, True)
257 else do (sc', u) <- atH f c ((n, b) : env) sc
258 return (Bind n b' sc', u)
259 atH f c env binder@(Bind n b sc)
260 | hole b && same h n = updated (f c env binder)
261 | otherwise -- scope first
262 = do (sc', u) <- atH f c ((n, b) : env) sc
263 if u then return (Bind n b sc', True)
264 else do (b', u) <- atHb f c env b
265 return (Bind n b' sc', u)
266 atH tac c env (App f a) = ulift2 tac c env App f a
267 atH tac c env t = return (t, False)
269 atHb f c env (Let t v) = ulift2 f c env Let t v
270 atHb f c env (Guess t v) = ulift2 f c env Guess t v
271 atHb f c env t = do (ty', u) <- atH f c env (binderTy t)
272 return (t { binderTy = ty' }, u)
274bound_in :: ProofTerm -> [Name]
275bound_in (PT path _ tm ups) = bound_in_term (rebuildTerm tm (updateSolvedPath ups path))
277bound_in_term :: Term -> [Name]
278bound_in_term (Bind n b sc) = n : bi b ++ bound_in_term sc
279 where
280 bi (Let t v) = bound_in_term t ++ bound_in_term v
281 bi (Guess t v) = bound_in_term t ++ bound_in_term v
282 bi b = bound_in_term (binderTy b)
283bound_in_term (App f a) = bound_in_term f ++ bound_in_term a
284bound_in_term _ = []