8ab2814 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Mark 'complete' terms to save time in elaboration

No need to substitute/update under complete subterms. This is a small improvement (not yet sure if it's actually worth it, but let's give it a go.)

commit8ab281431ae9ec3aa57501139dfcb2dd933284da authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 12 Apr 2015, 00:11 (12 years ago) parentf987aec

3 files changed+86−15

compare with master

unifiedsplit

src/Idris/Core/Evaluate.hs+5−5 src/Idris/Core/ProofState.hs+30−7 src/Idris/Core/ProofTerm.hs+51−3

src/Idris/Core/Evaluate.hs+5−5

@@ -540,7 +540,7 @@ instance Quote Value where

540540 v' <- quote i v

541541 let sc'' = pToV (sMN vd "vlet") (addBinder sc')

542542 return (Bind n (Let t' v') sc'')

543− quote i (VApp f a) = liftM2 (App Complete) (quote i f) (quote i a)

543+ quote i (VApp f a) = liftM2 (App MaybeHoles) (quote i f) (quote i a)

544544 quote i (VType u) = return $ TType u

545545 quote i (VUType u) = return $ UType u

546546 quote i VErased = return $ Erased

@@ -576,13 +576,13 @@ convEq ctxt holes topx topy = ceq [] topx topy where

576576 | x `elem` holes || y `elem` holes = return True

577577 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

578578 | otherwise = sameDefs ps x y

579− ceq ps x (Bind n (Lam t) (App Complete y (V 0)))

579+ ceq ps x (Bind n (Lam t) (App _ y (V 0)))

580580 = ceq ps x (substV (P Bound n t) y)

581− ceq ps (Bind n (Lam t) (App Complete x (V 0))) y

581+ ceq ps (Bind n (Lam t) (App _ x (V 0))) y

582582 = ceq ps (substV (P Bound n t) x) y

583− ceq ps x (Bind n (Lam t) (App Complete y (P Bound n' _)))

583+ ceq ps x (Bind n (Lam t) (App _ y (P Bound n' _)))

584584 | n == n' = ceq ps x y

585− ceq ps (Bind n (Lam t) (App Complete x (P Bound n' _))) y

585+ ceq ps (Bind n (Lam t) (App _ x (P Bound n' _))) y

586586 | n == n' = ceq ps x y

587587

588588 ceq ps (Bind n (PVar t) sc) y = ceq ps sc y

src/Idris/Core/ProofState.hs+30−7

@@ -551,13 +551,36 @@ solve ctxt env (Bind x (Guess ty val) sc)

551551 recents = x : recents ps,

552552 instances = instances ps \\ [x],

553553 dotted = dropUnified dropdots (dotted ps) })

554− let tm' = subst x val sc in

555− return tm'

554+ let (locked, did) = tryLock (holes ps \\ [x]) (updsubst x val sc) in

555+ return locked

556556 where dropUnified ddots [] = []

557557 dropUnified ddots ((x, es) : ds)

558558 | x `elem` ddots || any (\e -> e `elem` ddots) es

559559 = dropUnified ddots ds

560560 | otherwise = (x, es) : dropUnified ddots ds

561+

562+ tryLock :: [Name] -> Term -> (Term, Bool)

563+ tryLock hs tm@(App Complete _ _) = (tm, True)

564+ tryLock hs tm@(App s f a) =

565+ let (f', fl) = tryLock hs f

566+ (a', al) = tryLock hs a in

567+ if fl && al then (App Complete f' a', True)

568+ else (App s f' a', False)

569+ tryLock hs t@(P _ n _) = (t, not $ n `elem` hs)

570+ tryLock hs t@(Bind n (Hole _) sc) = (t, False)

571+ tryLock hs t@(Bind n (Guess _ _) sc) = (t, False)

572+ tryLock hs t@(Bind n (Let ty val) sc)

573+ = let (ty', tyl) = tryLock hs ty

574+ (val', vall) = tryLock hs val

575+ (sc', scl) = tryLock hs sc in

576+ (Bind n (Let ty' val') sc', tyl && vall && scl)

577+ tryLock hs t@(Bind n b sc)

578+ = let (bt', btl) = tryLock hs (binderTy b)

579+ (val', vall) = tryLock hs val

580+ (sc', scl) = tryLock hs sc in

581+ (Bind n (b { binderTy = bt' }) sc', btl && scl)

582+ tryLock hs t = (t, True)

583+

561584solve _ _ h@(Bind x t sc)

562585 = do ps <- get

563586 case findType x sc of

@@ -581,7 +604,7 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

581604 (tyv, tyt) <- lift $ check ctxt env ty

582605-- ns <- lift $ unify ctxt env tyv t'

583606 case t' of

584− Bind y (Pi _ s _) t -> let t' = subst y (P Bound n s) t in

607+ Bind y (Pi _ s _) t -> let t' = updsubst y (P Bound n s) t in

585608 do ns <- unify' ctxt env (s, Nothing) (tyv, Nothing)

586609 ps <- get

587610 let (uh, uns) = unified ps

@@ -600,7 +623,7 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

600623 _ -> hnf ctxt env t

601624 case t' of

602625 Bind y (Pi _ s _) t -> -- trace ("in type " ++ show t') $

603− let t' = subst y (P Bound n s) t in

626+ let t' = updsubst y (P Bound n s) t in

604627 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

605628 _ -> lift $ tfail $ CantIntroduce t'

606629intro n ctxt env _ = fail "Can't introduce here."

@@ -623,7 +646,7 @@ patvar n ctxt env (Bind x (Hole t) sc) =

623646 (notunified ps),

624647 injective = addInj n x (injective ps)

625648 })

626− return $ Bind n (PVar t) (subst x (P Bound n t) sc)

649+ return $ Bind n (PVar t) (updsubst x (P Bound n t) sc)

627650 where addInj n x ps | x `elem` ps = n : ps

628651 | otherwise = ps

629652patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm

@@ -638,7 +661,7 @@ letbind n ty val ctxt env _ = fail "Can't let bind here"

638661

639662expandLet :: Name -> Term -> RunTactic

640663expandLet n v ctxt env tm =

641− return $ subst n v tm

664+ return $ updsubst n v tm

642665

643666rewrite :: Raw -> RunTactic

644667rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =

@@ -750,7 +773,7 @@ patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

750773 x@(Bind y (PVTy s) t) -> x

751774 _ -> hnf ctxt env t

752775 case t' of

753− Bind y (PVTy s) t -> let t' = subst y (P Bound n s) t in

776+ Bind y (PVTy s) t -> let t' = updsubst y (P Bound n s) t in

754777 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))

755778 _ -> fail "Nothing to pattern bind"

756779patbind n ctxt env _ = fail "Can't pattern bind here"

src/Idris/Core/ProofTerm.hs+51−3

@@ -7,7 +7,7 @@ evaluation/checking inside the proof system, etc.

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

99 updateSolved, updateSolvedTerm, updateSolvedTerm',

10− bound_in, bound_in_term, refocus,

10+ bound_in, bound_in_term, refocus, updsubst,

1111 Hole, RunTactic',

1212 goal, atHole) where

1313

@@ -73,6 +73,7 @@ findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)

7373findHole n env t = fh' env Top t where

7474 fh' env path tm@(Bind x h sc)

7575 | hole h && n == x = Just (path, env, tm)

76+ fh' env path (App Complete _ _) = Nothing

7677 fh' env path (App s f a)

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

7879 | Just (p, env', tm) <- fh' env path f = Just (AppL s p a, env', tm)

@@ -156,15 +157,16 @@ updateSolvedTerm' xs x = updateSolved' xs x where

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

157158 | Just v <- lookup n xs

158159 = case xs of

159− [_] -> (subst n v t, True) -- some may be Vs! Can't assume

160+ [_] -> (updsubst n v t, True) -- some may be Vs! Can't assume

160161 -- explicit names

161162 _ -> let (t', _) = updateSolved' xs t in

162− (subst n v t', True)

163+ (updsubst n v t', True)

163164 updateSolved' xs tm@(Bind n b t)

164165 | otherwise = let (t', ut) = updateSolved' xs t

165166 (b', ub) = updateSolvedB' xs b in

166167 if ut || ub then (Bind n b' t', True)

167168 else (tm, False)

169+ updateSolved' xs t@(App Complete f a) = (t, False)

168170 updateSolved' xs t@(App s f a)

169171 = let (f', uf) = updateSolved' xs f

170172 (a', ua) = updateSolved' xs a in

@@ -198,6 +200,49 @@ updateSolvedTerm' xs x = updateSolved' xs x where

198200 noneOfB ns b = noneOf ns (binderTy b)

199201 noneOf ns _ = True

200202

203+-- | As 'subst', in TT, but takes advantage of knowing not to substitute

204+-- under Complete applications.

205+updsubst :: Eq n => n {-^ The id to replace -} ->

206+ TT n {-^ The replacement term -} ->

207+ TT n {-^ The term to replace in -} ->

208+ TT n

209+-- subst n v tm = instantiate v (pToV n tm)

210+updsubst n v tm = fst $ subst' 0 tm

211+ where

212+ -- keep track of updates to save allocations - this is a big win on

213+ -- large terms in particular

214+ -- ('Maybe' would be neater here, but >>= is not the right combinator.

215+ -- Feel free to tidy up, as long as it still saves allocating when no

216+ -- substitution happens...)

217+ subst' i (V x) | i == x = (v, True)

218+ subst' i (P _ x _) | n == x = (v, True)

219+ subst' i t@(P nt x ty)

220+ = let (ty', ut) = subst' i ty in

221+ if ut then (P nt x ty', True) else (t, False)

222+ subst' i t@(Bind x b sc) | x /= n

223+ = let (b', ub) = substB' i b

224+ (sc', usc) = subst' (i+1) sc in

225+ if ub || usc then (Bind x b' sc', True) else (t, False)

226+ subst' i t@(App Complete f a) = (t, False)

227+ subst' i t@(App s f a) = let (f', uf) = subst' i f

228+ (a', ua) = subst' i a in

229+ if uf || ua then (App s f' a', True) else (t, False)

230+ subst' i t@(Proj x idx) = let (x', u) = subst' i x in

231+ if u then (Proj x' idx, u) else (t, False)

232+ subst' i t = (t, False)

233+

234+ substB' i b@(Let t v) = let (t', ut) = subst' i t

235+ (v', uv) = subst' i v in

236+ if ut || uv then (Let t' v', True)

237+ else (b, False)

238+ substB' i b@(Guess t v) = let (t', ut) = subst' i t

239+ (v', uv) = subst' i v in

240+ if ut || uv then (Guess t' v', True)

241+ else (b, False)

242+ substB' i b = let (ty', u) = subst' i (binderTy b) in

243+ if u then (b { binderTy = ty' }, u) else (b, False)

244+

245+

201246-- | Apply solutions to an environment.

202247updateEnv :: [(Name, Term)] -> Env -> Env

203248updateEnv [] e = e

@@ -208,6 +253,8 @@ updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns e

208253updateSolvedPath :: [(Name, Term)] -> TermPath -> TermPath

209254updateSolvedPath [] t = t

210255updateSolvedPath ns Top = Top

256+updateSolvedPath ns t@(AppL Complete _ _) = t

257+updateSolvedPath ns t@(AppR Complete _ _) = t

211258updateSolvedPath ns (AppL s p r) = AppL s (updateSolvedPath ns p) (updateSolvedTerm ns r)

212259updateSolvedPath ns (AppR s l p) = AppR s (updateSolvedTerm ns l) (updateSolvedPath ns p)

213260updateSolvedPath ns (InBind n b sc)

@@ -246,6 +293,7 @@ goal h pt@(PT path env sub ups)

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

247294 | otherwise

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

296+ g env (App Complete f a) = fail "Can't find hole"

249297 g env (App _ f a) = g env a `mplus` g env f

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

251299