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

git.iko.soy/Idris-dev

on master help sign in

Mark 'complete' terms to save time in elaboration

8ab2814Edwin Brady12 years ago

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

compare with master

unifiedsplit

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

540 v' <- quote i v

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

542 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)

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

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

546 quote i VErased = return $ Erased

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

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

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

578 | 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)))

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

582 = 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' _)))

584 | 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

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

587

588 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)

551 recents = x : recents ps,

552 instances = instances ps \\ [x],

553 dotted = dropUnified dropdots (dotted ps) })

554− let tm' = subst x val sc in

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

555− return tm'

555+ return locked

556 where dropUnified ddots [] = []

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

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

559 = dropUnified ddots ds

560 | 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+

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

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

562 = do ps <- get

585 = do ps <- get

563 case findType x sc of

586 case findType x sc of

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

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

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

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

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

583 case t' of

606 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

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

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

586 ps <- get

609 ps <- get

587 let (uh, uns) = unified ps

610 let (uh, uns) = unified ps

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

600 _ -> hnf ctxt env t

623 _ -> hnf ctxt env t

601 case t' of

624 case t' of

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

625 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

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

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

605 _ -> lift $ tfail $ CantIntroduce t'

628 _ -> lift $ tfail $ CantIntroduce t'

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

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

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

623 (notunified ps),

646 (notunified ps),

624 injective = addInj n x (injective ps)

647 injective = addInj n x (injective ps)

625 })

648 })

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)

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

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

628 | otherwise = ps

651 | otherwise = ps

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

652patvar 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"

638

661

639expandLet :: Name -> Term -> RunTactic

662expandLet :: Name -> Term -> RunTactic

640expandLet n v ctxt env tm =

663expandLet n v ctxt env tm =

641− return $ subst n v tm

664+ return $ updsubst n v tm

642

665

643rewrite :: Raw -> RunTactic

666rewrite :: Raw -> RunTactic

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

667rewrite 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' =

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

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

751 _ -> hnf ctxt env t

774 _ -> hnf ctxt env t

752 case t' of

775 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

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

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

755 _ -> fail "Nothing to pattern bind"

778 _ -> fail "Nothing to pattern bind"

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

779patbind 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.

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

9 updateSolved, updateSolvedTerm, updateSolvedTerm',

10− bound_in, bound_in_term, refocus,

10+ bound_in, bound_in_term, refocus, updsubst,

11 Hole, RunTactic',

12 goal, atHole) where

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

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

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

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

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

76 fh' env path (App s f a)

77 fh' env path (App s f a)

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

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

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

79 | 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

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

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

157 | Just v <- lookup n xs

158 | Just v <- lookup n xs

158 = case xs of

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

160 -- explicit names

161 -- explicit names

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

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

162− (subst n v t', True)

163+ (updsubst n v t', True)

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

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

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

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

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

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

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

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

167 else (tm, False)

168 else (tm, False)

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

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

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

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

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

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

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

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

198 noneOfB ns b = noneOf ns (binderTy b)

200 noneOfB ns b = noneOf ns (binderTy b)

199 noneOf ns _ = True

201 noneOf ns _ = True

200

202

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+

201-- | Apply solutions to an environment.

246-- | Apply solutions to an environment.

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

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

203updateEnv [] e = e

248updateEnv [] e = e

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

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

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

209updateSolvedPath [] t = t

254updateSolvedPath [] t = t

210updateSolvedPath ns Top = Top

255updateSolvedPath ns Top = Top

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

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

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

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

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

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

213updateSolvedPath ns (InBind n b sc)

260updateSolvedPath ns (InBind n b sc)

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

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

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

247 | otherwise

294 | otherwise

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

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

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

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

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

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

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

251

299