@@ -6,7 +6,7 @@
66
77module Idris.Core.ProofTerm(ProofTerm, Goal(..), mkProofTerm, getProofTerm,
88 updateSolved, updateSolvedTerm,
9− bound_in, bound_in_term,
9+ bound_in, bound_in_term, refocus,
1010 Hole, RunTactic',
1111 goal, atHole) where
1212
@@ -64,8 +64,8 @@ findHole n env t = fh' env Top t where
6464 fh' env path tm@(Bind x h sc)
6565 | hole h && n == x = Just (path, env, tm)
6666 fh' env path (App f a)
67− | Just (p, env', tm) <- fh' env path f = Just (AppL p a, env', tm)
6867 | 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)
6969 fh' env path (Bind x b sc)
7070 | Just (bp, env', tm) <- fhB env path b = Just (InBind x bp sc, env', tm)
7171 | Just (p, env', tm) <- fh' ((x,b):env) path sc = Just (InScope x b p, env', tm)
@@ -85,7 +85,8 @@ findHole n env t = fh' env Top t where
8585data ProofTerm = PT { -- wholeterm :: Term,
8686 path :: TermPath,
8787 subterm_env :: Env,
88− subterm :: Term }
88+ subterm :: Term,
89+ updates :: [(Name, Term)] }
8990 deriving Show
9091
9192type RunTactic' a = Context -> Env -> Term -> StateT a TC Term
@@ -95,11 +96,11 @@ refocus :: Hole -> ProofTerm -> ProofTerm
9596refocus h t = let res = refocus' h t in res
9697-- trace ("OLD: " ++ show t ++ "\n" ++
9798-- "REFOCUSSED " ++ show h ++ ": " ++ show res) res
98−refocus' (Just n) pt@(PT path env tm)
99+refocus' (Just n) pt@(PT path env tm ups)
99100 | Just (p', env', tm') <- findHole n env tm
100− = PT (replaceTop p' path) env' tm'
101− | Just (p', env', tm') <- findHole n [] (rebuildTerm tm path)
102− = PT p' 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' []
103104 | otherwise = pt
104105refocus' _ pt = pt
105106
@@ -108,10 +109,10 @@ data Goal = GD { premises :: Env,
108109 }
109110
110111mkProofTerm :: Term -> ProofTerm
111−mkProofTerm tm = PT Top [] tm
112+mkProofTerm tm = PT Top [] tm []
112113
113114getProofTerm :: ProofTerm -> Term
114−getProofTerm (PT path _ sub) = rebuildTerm sub path
115+getProofTerm (PT path _ sub ups) = rebuildTerm sub (updateSolvedPath ups path)
115116
116117same Nothing n = True
117118same (Just x) n = x == n
@@ -121,7 +122,14 @@ hole (Guess _ _) = True
121122hole _ = False
122123
123124updateSolvedTerm :: [(Name, Term)] -> Term -> Term
124−updateSolvedTerm xs x = updateSolved' xs x where
125+updateSolvedTerm [] x = x
126+updateSolvedTerm 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
125133 updateSolved' [] x = x
126134 updateSolved' xs (Bind n (Hole ty) t)
127135 | Just v <- lookup n xs
@@ -137,6 +145,16 @@ updateSolvedTerm xs x = updateSolved' xs x where
137145 | Just v <- lookup n xs = v
138146 updateSolved' xs t = t
139147
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
157+
140158updateEnv [] e = e
141159updateEnv ns [] = []
142160updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env
@@ -162,15 +180,16 @@ updateSolvedPath ns (InScope n b sc)
162180 = InScope n (fmap (updateSolvedTerm ns) b) (updateSolvedPath ns sc)
163181
164182updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm
165−updateSolved xs pt@(PT path env sub)
166− = PT (updateSolvedPath xs path)
183+updateSolved xs pt@(PT path env sub ups)
184+ = PT path -- (updateSolvedPath xs path)
167185 (updateEnv xs (filter (\(n, t) -> n `notElem` map fst xs) env))
168186 (updateSolvedTerm xs sub)
187+ (ups ++ xs)
169188
170189goal :: Hole -> ProofTerm -> TC Goal
171−goal h pt@(PT path env sub)
172− | OK ginf <- g env sub = return ginf
173− | otherwise = g [] (rebuildTerm sub path)
190+goal h pt@(PT path env sub ups)
191+-- | OK ginf <- g env sub = return ginf
192+ | otherwise = g [] (rebuildTerm sub (updateSolvedPath ups path))
174193 where
175194 g :: Env -> Term -> TC Goal
176195 g env (Bind n b@(Guess _ _) sc)
@@ -180,7 +199,7 @@ goal h pt@(PT path env sub)
180199 g env (Bind n b sc) | hole b && same h n = return $ GD env b
181200 | otherwise
182201 = g ((n, b):env) sc `mplus` gb env b
183− g env (App f a) = g env f `mplus` g env a
202+ g env (App f a) = g env a `mplus` g env f
184203 g env t = fail "Can't find hole"
185204
186205 gb env (Let t v) = g env v `mplus` g env t
@@ -190,9 +209,13 @@ goal h pt@(PT path env sub)
190209atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm ->
191210 StateT a TC (ProofTerm, Bool)
192211atHole h f c e pt -- @(PT path env sub)
193− = do let pt'@(PT path env sub) = refocus h pt
194− (tm, u) <- atH f c env sub
195− return (PT path env tm, u)
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)
196219 where
197220 updated o = do o' <- o
198221 return (o', True)
@@ -230,7 +253,7 @@ atHole h f c e pt -- @(PT path env sub)
230253 return (t { binderTy = ty' }, u)
231254
232255bound_in :: ProofTerm -> [Name]
233−bound_in (PT path _ tm) = bound_in_term (rebuildTerm tm path)
256+bound_in (PT path _ tm ups) = bound_in_term (rebuildTerm tm (updateSolvedPath ups path))
234257
235258bound_in_term :: Term -> [Name]
236259bound_in_term (Bind n b sc) = n : bi b ++ bound_in_term sc