2418336 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Save some allocations in updateSolved

2418336Edwin Brady12 years ago

src/Idris/AbsSyntaxTree.hs+1

compare with master

unifiedsplit

@@ -1635,6 +1635,7 @@ instance Sized PTerm where

1635 size (PProof tactics) = size tactics

1636 size (PElabError err) = size err

1637 size PImpossible = 1

1638+ size _ = 0

1638

1639

1639getPArity :: PTerm -> Int

1640getPArity :: PTerm -> Int

1640getPArity (PPi _ _ _ sc) = 1 + getPArity sc

1641getPArity (PPi _ _ _ sc) = 1 + getPArity sc

src/Idris/Core/Elaborate.hs+9−1

@@ -12,7 +12,8 @@ module Idris.Core.Elaborate(module Idris.Core.Elaborate,

12 module Idris.Core.ProofState) where

14import Idris.Core.ProofState

15−import Idris.Core.ProofTerm(bound_in, getProofTerm, mkProofTerm, bound_in_term)

15+import Idris.Core.ProofTerm(bound_in, getProofTerm, mkProofTerm, bound_in_term,

16+ refocus)

16import Idris.Core.TT

17import Idris.Core.TT

17import Idris.Core.Evaluate

18import Idris.Core.Evaluate

18import Idris.Core.Typecheck

19import Idris.Core.Typecheck

@@ -390,6 +391,13 @@ focus n = processTactic' (Focus n)

390movelast :: Name -> Elab' aux ()

391movelast :: Name -> Elab' aux ()

391movelast n = processTactic' (MoveLast n)

392movelast n = processTactic' (MoveLast n)

392

393

394+-- | Set the zipper in the proof state to point at the current sub term

395+-- (This currently happens automatically, so this will have no effect...)

396+zipHere :: Elab' aux ()

397+zipHere = do ES (ps, a) s m <- get

398+ let pt' = refocus (Just (head (holes ps))) (pterm ps)

399+ put (ES (ps { pterm = pt' }, a) s m)

400+

393matchProblems :: Bool -> Elab' aux ()

401matchProblems :: Bool -> Elab' aux ()

394matchProblems all = processTactic' (MatchProblems all)

402matchProblems all = processTactic' (MatchProblems all)

395

403

src/Idris/Core/ProofTerm.hs+43−20

@@ -6,7 +6,7 @@

7module Idris.Core.ProofTerm(ProofTerm, Goal(..), mkProofTerm, getProofTerm,

8 updateSolved, updateSolvedTerm,

9− bound_in, bound_in_term,

9+ bound_in, bound_in_term, refocus,

10 Hole, RunTactic',

11 goal, atHole) where

@@ -64,8 +64,8 @@ findHole 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 f = Just (AppL p a, env', tm)

68 | Just (p, env', tm) <- fh' env path a = Just (AppR f p, env', tm)

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)

@@ -85,7 +85,8 @@ findHole n env t = fh' env Top t where

85data ProofTerm = PT { -- wholeterm :: Term,

86 path :: TermPath,

87 subterm_env :: Env,

88− subterm :: Term }

88+ subterm :: Term,

89+ updates :: [(Name, Term)] }

89 deriving Show

90 deriving Show

91type RunTactic' a = Context -> Env -> Term -> StateT a TC Term

92type RunTactic' a = Context -> Env -> Term -> StateT a TC Term

@@ -95,11 +96,11 @@ refocus :: Hole -> ProofTerm -> ProofTerm

95refocus h t = let res = refocus' h t in res

96refocus h t = let res = refocus' h t in res

96-- trace ("OLD: " ++ show t ++ "\n" ++

97-- trace ("OLD: " ++ show t ++ "\n" ++

97-- "REFOCUSSED " ++ show h ++ ": " ++ show res) res

98-- "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)

99 | Just (p', env', tm') <- findHole n env tm

100 | Just (p', env', tm') <- findHole n env tm

100− = PT (replaceTop p' path) env' tm'

101+ = PT (replaceTop p' path) env' tm' ups

101− | Just (p', env', tm') <- findHole n [] (rebuildTerm tm path)

102+ | Just (p', env', tm') <- findHole n [] (rebuildTerm tm (updateSolvedPath ups path))

102− = PT p' env' tm'

103+ = PT p' env' tm' []

103 | otherwise = pt

104 | otherwise = pt

104refocus' _ pt = pt

105refocus' _ pt = pt

105

106

@@ -108,10 +109,10 @@ data Goal = GD { premises :: Env,

108 }

109 }

109

110

110mkProofTerm :: Term -> ProofTerm

111mkProofTerm :: Term -> ProofTerm

111−mkProofTerm tm = PT Top [] tm

112+mkProofTerm tm = PT Top [] tm []

112

113

113getProofTerm :: ProofTerm -> Term

114getProofTerm :: ProofTerm -> Term

114−getProofTerm (PT path _ sub) = rebuildTerm sub path

115+getProofTerm (PT path _ sub ups) = rebuildTerm sub (updateSolvedPath ups path)

115

116

116same Nothing n = True

117same Nothing n = True

117same (Just x) n = x == n

118same (Just x) n = x == n

@@ -121,7 +122,14 @@ hole (Guess _ _) = True

121hole _ = False

122hole _ = False

122

123

123updateSolvedTerm :: [(Name, Term)] -> Term -> Term

124updateSolvedTerm :: [(Name, Term)] -> Term -> Term

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

124−updateSolvedTerm xs x = updateSolved' xs x where

132+ else updateSolved' xs x where

125 updateSolved' [] x = x

133 updateSolved' [] x = x

126 updateSolved' xs (Bind n (Hole ty) t)

134 updateSolved' xs (Bind n (Hole ty) t)

127 | Just v <- lookup n xs

135 | Just v <- lookup n xs

@@ -137,6 +145,16 @@ updateSolvedTerm xs x = updateSolved' xs x where

137 | Just v <- lookup n xs = v

145 | Just v <- lookup n xs = v

138 updateSolved' xs t = t

146 updateSolved' xs t = t

139

147

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+

140updateEnv [] e = e

158updateEnv [] e = e

141updateEnv ns [] = []

159updateEnv ns [] = []

142updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env

160updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env

@@ -162,15 +180,16 @@ updateSolvedPath ns (InScope n b sc)

162 = InScope n (fmap (updateSolvedTerm ns) b) (updateSolvedPath ns sc)

180 = InScope n (fmap (updateSolvedTerm ns) b) (updateSolvedPath ns sc)

163

181

164updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm

182updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm

165−updateSolved xs pt@(PT path env sub)

183+updateSolved xs pt@(PT path env sub ups)

166− = PT (updateSolvedPath xs path)

184+ = PT path -- (updateSolvedPath xs path)

167 (updateEnv xs (filter (\(n, t) -> n `notElem` map fst xs) env))

185 (updateEnv xs (filter (\(n, t) -> n `notElem` map fst xs) env))

168 (updateSolvedTerm xs sub)

186 (updateSolvedTerm xs sub)

187+ (ups ++ xs)

169

188

170goal :: Hole -> ProofTerm -> TC Goal

189goal :: Hole -> ProofTerm -> TC Goal

171−goal h pt@(PT path env sub)

190+goal h pt@(PT path env sub ups)

172− | OK ginf <- g env sub = return ginf

191+-- | OK ginf <- g env sub = return ginf

173− | otherwise = g [] (rebuildTerm sub path)

192+ | otherwise = g [] (rebuildTerm sub (updateSolvedPath ups path))

174 where

193 where

175 g :: Env -> Term -> TC Goal

194 g :: Env -> Term -> TC Goal

176 g env (Bind n b@(Guess _ _) sc)

195 g env (Bind n b@(Guess _ _) sc)

@@ -180,7 +199,7 @@ goal h pt@(PT path env sub)

180 g env (Bind n b sc) | hole b && same h n = return $ GD env b

199 g env (Bind n b sc) | hole b && same h n = return $ GD env b

181 | otherwise

200 | otherwise

182 = g ((n, b):env) sc `mplus` gb env b

201 = 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

184 g env t = fail "Can't find hole"

203 g env t = fail "Can't find hole"

185

204

186 gb env (Let t v) = g env v `mplus` g env t

205 gb env (Let t v) = g env v `mplus` g env t

@@ -190,9 +209,13 @@ goal h pt@(PT path env sub)

190atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm ->

209atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm ->

191 StateT a TC (ProofTerm, Bool)

210 StateT a TC (ProofTerm, Bool)

192atHole h f c e pt -- @(PT path env sub)

211atHole h f c e pt -- @(PT path env sub)

193− = do let pt'@(PT path env sub) = refocus h pt

212+ = do let PT path env sub ups = refocus h pt

194− (tm, u) <- atH f c env sub

213+ (tm, u) <- atH f c env sub

195− return (PT path env tm, u)

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)

196 where

219 where

197 updated o = do o' <- o

220 updated o = do o' <- o

198 return (o', True)

221 return (o', True)

@@ -230,7 +253,7 @@ atHole h f c e pt -- @(PT path env sub)

230 return (t { binderTy = ty' }, u)

253 return (t { binderTy = ty' }, u)

231

254

232bound_in :: ProofTerm -> [Name]

255bound_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))

234

257

235bound_in_term :: Term -> [Name]

258bound_in_term :: Term -> [Name]

236bound_in_term (Bind n b sc) = n : bi b ++ bound_in_term sc

259bound_in_term (Bind n b sc) = n : bi b ++ bound_in_term sc

src/Idris/ElabTerm.hs+2−1

@@ -17,6 +17,7 @@ import Idris.Core.Unify

17import Idris.Core.Typecheck (check, recheck)

18import Idris.ErrReverse (errReverse)

19import Idris.ElabQuasiquote (extractUnquotes)

20+import qualified Util.Pretty as U

21import Control.Applicative ((<$>))

22import Control.Applicative ((<$>))

22import Control.Monad

23import Control.Monad

@@ -905,7 +906,7 @@ elab ist info emode opts fn tm

905 elabArgs ist ina failed fc r f (n:ns) force (Placeholder : args)

906 elabArgs ist ina failed fc r f (n:ns) force (Placeholder : args)

906 = elabArgs ist ina failed fc r f ns force args

907 = elabArgs ist ina failed fc r f ns force args

907 elabArgs ist ina failed fc r f ((argName, holeName):ns) force (t : args)

908 elabArgs ist ina failed fc r f ((argName, holeName):ns) force (t : args)

908− = do elabArg argName holeName t

909+ = elabArg argName holeName t

909 where elabArg argName holeName t =

910 where elabArg argName holeName t =

910 do now_elaborating fc f argName

911 do now_elaborating fc f argName

911 wrapErr f argName $ do

912 wrapErr f argName $ do