git.iko.soy/Idris-dev
on c79fb21 help sign in
Idris-dev/src/Idris/Core/ProofTerm.hs
266 lines 11 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 Nothing n = True
118same (Just x) n = x == n
120hole (Hole _) = True
121hole (Guess _ _) = True
122hole _ = False
124updateSolvedTerm :: [(Name, Term)] -> Term -> Term
125updateSolvedTerm [] x = x
126updateSolvedTerm xs x = -- updateSolved' xs x where
127-- This version below saves allocations, because it doesn't need to reallocate
128-- the term if there are no updates to do, but costs an extra pass. Below
129-- version works better on larger terms...
130 if noneOf (map fst xs) x
131 then x
132 else updateSolved' xs x where
133 updateSolved' [] x = x
134 updateSolved' xs (Bind n (Hole ty) t)
135 | Just v <- lookup n xs
136 = case xs of
137 [_] -> substV v $ psubst n v t -- some may be Vs! Can't assume
138 -- explicit names
139 _ -> substV v $ psubst n v (updateSolved' xs t)
140 updateSolved' xs (Bind n b t)
141 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)
142 updateSolved' xs (App f a)
143 = App (updateSolved' xs f) (updateSolved' xs a)
144 updateSolved' xs (P _ n@(MN _ _) _)
145 | Just v <- lookup n xs = v
146 updateSolved' xs t = t
148 noneOf ns (P _ n _) | n `elem` ns = False
149 noneOf ns (App f a) = noneOf ns a && noneOf ns f
150 noneOf ns (Bind n (Hole ty) t) = n `notElem` ns && noneOf ns ty && noneOf ns t
151 noneOf ns (Bind n b t) = noneOf ns t && noneOfB ns b
152 where
153 noneOfB ns (Let t v) = noneOf ns t && noneOf ns v
154 noneOfB ns (Guess t v) = noneOf ns t && noneOf ns v
155 noneOfB ns b = noneOf ns (binderTy b)
156 noneOf ns _ = True
158updateEnv [] e = e
159updateEnv ns [] = []
160updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env
162updateSolvedPath [] t = t
163updateSolvedPath ns Top = Top
164updateSolvedPath ns (AppL p r) = AppL p (updateSolvedTerm ns r)
165updateSolvedPath ns (AppR l p) = AppR (updateSolvedTerm ns l) p
166updateSolvedPath ns (InBind n b sc)
167 = InBind n (updateSolvedPathB b) (updateSolvedTerm ns sc)
168 where
169 updateSolvedPathB (Binder b) = Binder (fmap (updateSolvedPath ns) b)
170 updateSolvedPathB (LetT p v) = LetT (updateSolvedPath ns p) (updateSolvedTerm ns v)
171 updateSolvedPathB (LetV v p) = LetV (updateSolvedTerm ns v) (updateSolvedPath ns p)
172 updateSolvedPathB (GuessT p v) = GuessT (updateSolvedPath ns p) (updateSolvedTerm ns v)
173 updateSolvedPathB (GuessV v p) = GuessV (updateSolvedTerm ns v) (updateSolvedPath ns p)
174updateSolvedPath ns (InScope n (Hole ty) t)
175 | Just v <- lookup n ns = case ns of
176 [_] -> updateSolvedPath [(n,v)] t
177 _ -> updateSolvedPath ns $
178 updateSolvedPath [(n,v)] t
179updateSolvedPath ns (InScope n b sc)
180 = InScope n (fmap (updateSolvedTerm ns) b) (updateSolvedPath ns sc)
182updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm
183updateSolved xs pt@(PT path env sub ups)
184 = PT path -- (updateSolvedPath xs path)
185 (updateEnv xs (filter (\(n, t) -> n `notElem` map fst xs) env))
186 (updateSolvedTerm xs sub)
187 (ups ++ xs)
189goal :: Hole -> ProofTerm -> TC Goal
190goal h pt@(PT path env sub ups)
191-- | OK ginf <- g env sub = return ginf
192 | otherwise = g [] (rebuildTerm sub (updateSolvedPath ups path))
193 where
194 g :: Env -> Term -> TC Goal
195 g env (Bind n b@(Guess _ _) sc)
196 | same h n = return $ GD env b
197 | otherwise
198 = gb env b `mplus` g ((n, b):env) sc
199 g env (Bind n b sc) | hole b && same h n = return $ GD env b
200 | otherwise
201 = g ((n, b):env) sc `mplus` gb env b
202 g env (App f a) = g env a `mplus` g env f
203 g env t = fail "Can't find hole"
205 gb env (Let t v) = g env v `mplus` g env t
206 gb env (Guess t v) = g env v `mplus` g env t
207 gb env t = g env (binderTy t)
209atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm ->
210 StateT a TC (ProofTerm, Bool)
211atHole h f c e pt -- @(PT path env sub)
212 = do let PT path env sub ups = refocus h pt
213 (tm, u) <- atH f c env sub
214 return (PT path env tm ups, u)
215-- if u then return (PT path env tm ups, u)
216-- else do let PT path env sub ups = refocus h pt
217-- (tm, u) <- atH f c env sub
218-- return (PT path env tm ups, u)
219 where
220 updated o = do o' <- o
221 return (o', True)
223 ulift2 f c env op a b
224 = do (b', u) <- atH f c env b
225 if u then return (op a b', True)
226 else do (a', u) <- atH f c env a
227 return (op a' b', u)
229 -- Search the things most likely to contain the binding first!
231 atH :: RunTactic' a -> Context -> Env -> Term -> StateT a TC (Term, Bool)
232 atH f c env binder@(Bind n b@(Guess t v) sc)
233 | same h n = updated (f c env binder)
234 | otherwise
235 = do -- binder first
236 (b', u) <- ulift2 f c env Guess t v
237 if u then return (Bind n b' sc, True)
238 else do (sc', u) <- atH f c ((n, b) : env) sc
239 return (Bind n b' sc', u)
240 atH f c env binder@(Bind n b sc)
241 | hole b && same h n = updated (f c env binder)
242 | otherwise -- scope first
243 = do (sc', u) <- atH f c ((n, b) : env) sc
244 if u then return (Bind n b sc', True)
245 else do (b', u) <- atHb f c env b
246 return (Bind n b' sc', u)
247 atH tac c env (App f a) = ulift2 tac c env App f a
248 atH tac c env t = return (t, False)
250 atHb f c env (Let t v) = ulift2 f c env Let t v
251 atHb f c env (Guess t v) = ulift2 f c env Guess t v
252 atHb f c env t = do (ty', u) <- atH f c env (binderTy t)
253 return (t { binderTy = ty' }, u)
255bound_in :: ProofTerm -> [Name]
256bound_in (PT path _ tm ups) = bound_in_term (rebuildTerm tm (updateSolvedPath ups path))
258bound_in_term :: Term -> [Name]
259bound_in_term (Bind n b sc) = n : bi b ++ bound_in_term sc
260 where
261 bi (Let t v) = bound_in_term t ++ bound_in_term v
262 bi (Guess t v) = bound_in_term t ++ bound_in_term v
263 bi b = bound_in_term (binderTy b)
264bound_in_term (App f a) = bound_in_term f ++ bound_in_term a
265bound_in_term _ = []