7a66adc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Make unification faster by computing HNF rather than normalising

7a66adcEdwin Brady14 years ago

src/Core/Elaborate.hs+4−1

compare with master

unifiedsplit

@@ -244,6 +244,9 @@ regret = processTactic' Regret

244compute :: Elab' aux ()

245compute = processTactic' Compute

246

247+hnf_compute :: Elab' aux ()

248+hnf_compute = processTactic' HNF_Compute

249+

247eval_in :: Raw -> Elab' aux ()

250eval_in :: Raw -> Elab' aux ()

248eval_in t = processTactic' (EvalIn t)

251eval_in t = processTactic' (EvalIn t)

249

252

@@ -406,7 +409,7 @@ apply_elab n args =

406 do ty <- get_type (Var n)

409 do ty <- get_type (Var n)

407 ctxt <- get_context

410 ctxt <- get_context

408 env <- get_env

411 env <- get_env

409− claims <- doClaims (normalise ctxt env ty) args []

412+ claims <- doClaims (finalise ty) args []

410 prep_fill n (map fst claims)

413 prep_fill n (map fst claims)

411 let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims

414 let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims

412 elabClaims [] False claims

415 elabClaims [] False claims

src/Core/Evaluate.hs+19−6

@@ -118,7 +118,9 @@ simplify ctxt runtime env t

118

119hnf :: Context -> Env -> TT Name -> TT Name

120hnf ctxt env t

121− = evalState (do val <- eval False ctxt threshold [] (map finalEntry env) (finalise t) [HNF]

121+ = evalState (do val <- eval False ctxt threshold []

122+ (map finalEntry env)

123+ (finalise t) [HNF]

122 quote 0 val) initEval

124 quote 0 val) initEval

123

125

124

126

@@ -159,6 +161,7 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

159 spec = Spec `elem` opts

161 spec = Spec `elem` opts

160 simpl = Simplify True `elem` opts

162 simpl = Simplify True `elem` opts

161 atRepl = AtREPL `elem` opts

163 atRepl = AtREPL `elem` opts

164+ hnf = HNF `elem` opts

162

165

163 canSimplify inl inr n stk

166 canSimplify inl inr n stk

164 = (Simplify False `elem` opts && (not inl || elem n stk))

167 = (Simplify False `elem` opts && (not inl || elem n stk))

@@ -168,6 +171,7 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

168 | Just (Let t v) <- lookup n genv = do when (not atRepl) $ step maxred

171 | Just (Let t v) <- lookup n genv = do when (not atRepl) $ step maxred

169 ev ntimes stk top env v

172 ev ntimes stk top env v

170 ev ntimes_in stk top env (P Ref n ty)

173 ev ntimes_in stk top env (P Ref n ty)

174+ | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)

171 | (True, ntimes) <- usable simpl n ntimes_in

175 | (True, ntimes) <- usable simpl n ntimes_in

172 = do let val = lookupDefAcc Nothing n atRepl ctxt

176 = do let val = lookupDefAcc Nothing n atRepl ctxt

173 when (not atRepl) $ step maxred

177 when (not atRepl) $ step maxred

@@ -211,7 +215,7 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

211 ev ntimes stk top env (Bind n b sc)

215 ev ntimes stk top env (Bind n b sc)

212 = do b' <- vbind env b

216 = do b' <- vbind env b

213 when (not atRepl) $ step maxred

217 when (not atRepl) $ step maxred

214− return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)

218+ return $ VBind n b' (\x -> ev ntimes stk False (x:env) sc)

215 where vbind env t

219 where vbind env t

216 | simpl

220 | simpl

217 = fmapMB (\tm -> ev ((MN 0 "STOP", 0) : ntimes)

221 = fmapMB (\tm -> ev ((MN 0 "STOP", 0) : ntimes)

@@ -222,7 +226,7 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

222-- | laz == UN "lazy"

226-- | laz == UN "lazy"

223-- = trace (showEnvDbg genv a) $ ev ntimes stk top env a

227-- = trace (showEnvDbg genv a) $ ev ntimes stk top env a

224 ev ntimes stk top env (App f a)

228 ev ntimes stk top env (App f a)

225− = do f' <- ev ntimes stk top env f

229+ = do f' <- ev ntimes stk False env f

226 a' <- ev ntimes stk False env a

230 a' <- ev ntimes stk False env a

227 when (not atRepl) $ step maxred

231 when (not atRepl) $ step maxred

228 evApply ntimes stk top env [a'] f'

232 evApply ntimes stk top env [a'] f'

@@ -243,7 +247,10 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

243 wknV (-1) app

247 wknV (-1) app

244-- apply ntimes stk False env f args

248-- apply ntimes stk False env f args

245-- | spec = specApply ntimes stk env f args

249-- | spec = specApply ntimes stk env f args

246− apply ntimes_in stk top env f@(VP Ref n ty) args

250+ apply ntimes_in stk top env f@(VP Ref n ty) args

251+ | not top && hnf = case args of

252+ [] -> return f

253+ _ -> return $ unload env f args

247 | (True, ntimes) <- usable simpl n ntimes_in

254 | (True, ntimes) <- usable simpl n ntimes_in

248 = traceWhen traceon (show stk) $

255 = traceWhen traceon (show stk) $

249 do let val = lookupDefAcc Nothing n atRepl ctxt

256 do let val = lookupDefAcc Nothing n atRepl ctxt

@@ -284,7 +291,8 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

284 | length ns <= length args

291 | length ns <= length args

285 = do let args' = take (length ns) args

292 = do let args' = take (length ns) args

286 let rest = drop (length ns) args

293 let rest = drop (length ns) args

287− t <- evTree ntimes stk top env (zipWith (\n t -> (n, t)) ns args') tree

294+ t <- evTree ntimes stk top env

295+ (zipWith (\n t -> (n, t)) ns args') tree

288 return (t, rest)

296 return (t, rest)

289 | otherwise = return (Nothing, args)

297 | otherwise = return (Nothing, args)

290

298

@@ -293,7 +301,8 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

293 evTree ntimes stk top env amap (UnmatchedCase str) = return Nothing

301 evTree ntimes stk top env amap (UnmatchedCase str) = return Nothing

294 evTree ntimes stk top env amap (STerm tm)

302 evTree ntimes stk top env amap (STerm tm)

295 = do let etm = pToVs (map fst amap) tm

303 = do let etm = pToVs (map fst amap) tm

304+ etm' <- ev ntimes stk (not (conHeaded tm))

296− etm' <- ev ntimes stk top (map snd amap ++ env) etm

305+ (map snd amap ++ env) etm

297 return $ Just etm'

306 return $ Just etm'

298 evTree ntimes stk top env amap (Case n alts)

307 evTree ntimes stk top env amap (Case n alts)

299 = case lookup n amap of

308 = case lookup n amap of

@@ -306,6 +315,10 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

306 _ -> return Nothing

315 _ -> return Nothing

307 _ -> return Nothing

316 _ -> return Nothing

308

317

318+ conHeaded tm@(App _ _)

319+ | (P (DCon _ _) _ _, args) <- unApply tm = True

320+ conHeaded t = False

321+

309 chooseAlt' ntimes stk env _ (f, args) alts amap

322 chooseAlt' ntimes stk env _ (f, args) alts amap

310 = do f' <- apply ntimes stk True env f args

323 = do f' <- apply ntimes stk True env f args

311 chooseAlt env f' (getValArgs f') alts amap

324 chooseAlt env f' (getValArgs f') alts amap

src/Core/ProofState.hs+11−3

@@ -54,6 +54,7 @@ data Tactic = Attack

54 | StartUnify Name

55 | EndUnify

56 | Compute

57+ | HNF_Compute

57 | EvalIn Raw

58 | EvalIn Raw

58 | CheckIn Raw

59 | CheckIn Raw

59 | Intro (Maybe Name)

60 | Intro (Maybe Name)

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

387 Nothing -> x

388 Nothing -> x

388 let t' = case t of

389 let t' = case t of

389 x@(Bind y (Pi s) _) -> x

390 x@(Bind y (Pi s) _) -> x

390− _ -> normalise ctxt env t

391+ _ -> hnf ctxt env t

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

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

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

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

393 case t' of

394 case t' of

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

407 Nothing -> x

408 Nothing -> x

408 let t' = case t of

409 let t' = case t of

409 x@(Bind y (Pi s) _) -> x

410 x@(Bind y (Pi s) _) -> x

410− _ -> normalise ctxt env t

411+ _ -> hnf ctxt env t

411 case t' of

412 case t' of

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

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

413 let t' = instantiate (P Bound n s) (pToV y t) in

414 let t' = instantiate (P Bound n s) (pToV y t) in

@@ -477,7 +478,7 @@ patbind :: Name -> RunTactic

477patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

478patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

478 do let t' = case t of

479 do let t' = case t of

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

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

480− _ -> normalise ctxt env t

481+ _ -> hnf ctxt env t

481 case t' of

482 case t' of

482 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in

483 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in

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

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

@@ -488,6 +489,12 @@ compute :: RunTactic

488compute ctxt env (Bind x (Hole ty) sc) =

489compute ctxt env (Bind x (Hole ty) sc) =

489 do return $ Bind x (Hole (normalise ctxt env ty)) sc

490 do return $ Bind x (Hole (normalise ctxt env ty)) sc

490

491

492+hnf_compute :: RunTactic

493+hnf_compute ctxt env (Bind x (Hole ty) sc) =

494+ do let ty' = hnf ctxt env ty in

495+-- trace ("HNF " ++ show (ty, ty')) $

496+ return $ Bind x (Hole ty') sc

497+

491check_in :: Raw -> RunTactic

498check_in :: Raw -> RunTactic

492check_in t ctxt env tm =

499check_in t ctxt env tm =

493 do (val, valty) <- lift $ check ctxt env t

500 do (val, valty) <- lift $ check ctxt env t

@@ -603,6 +610,7 @@ process t h = tactic (Just h) (mktac t)

603 mktac Solve = solve

610 mktac Solve = solve

604 mktac (StartUnify n) = start_unify n

611 mktac (StartUnify n) = start_unify n

605 mktac Compute = compute

612 mktac Compute = compute

613+ mktac HNF_Compute = hnf_compute

606 mktac (Intro n) = intro n

614 mktac (Intro n) = intro n

607 mktac (IntroTy ty n) = introTy ty n

615 mktac (IntroTy ty n) = introTy ty n

608 mktac (Forall n t) = forall n t

616 mktac (Forall n t) = forall n t

src/Core/Typecheck.hs+1−1

@@ -67,7 +67,7 @@ check' holes ctxt env top = chk env top where

67 let fty' = case uniqueBinders (map fst env) (finalise fty) of

68 ty@(Bind x (Pi s) t) -> ty

69 _ -> uniqueBinders (map fst env)

70− $ normalise ctxt env fty

70+ $ hnf ctxt env fty

71 case fty' of

72 Bind x (Pi s) t ->

73-- trace ("Converting " ++ show aty ++ " and " ++ show s ++

src/Core/Unify.hs+3−3

@@ -31,7 +31,7 @@ unify ctxt env topx topy =

31 _ ->

32 let topxn = normalise ctxt env topx

33 topyn = normalise ctxt env topy in

34−-- trace ("Unifying " ++ show (topxn, topyn)) $

34+-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n") $

35 case runStateT (un' False [] topxn topyn)

36 (UI 0 [] []) of

37 OK (v, UI _ inj fails) ->

@@ -112,7 +112,7 @@ unify ctxt env topx topy =

112 sc 1

113 combine bnames hf ha)

114 where hnormalise [] _ _ t = t

115− hnormalise ns ctxt env t = normalise ctxt env t

115+ hnormalise ns ctxt env t = hnf ctxt env t

116 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)

117 | x /= y = unifyFail appx appy

118 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)

@@ -200,7 +200,7 @@ unify ctxt env topx topy =

200 | otherwise = False

201-- recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False

202-- recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False

203− recoverable p@(P _ _ _) (App f a) = recoverable p f

203+ recoverable p@(P _ n _) (App f a) = recoverable p f

204 recoverable (App f a) p@(P _ _ _) = recoverable f p

205 recoverable (App f a) (App f' a')

206 = recoverable f f' && recoverable a a'

src/Idris/Delaborate.hs+6−3

@@ -77,15 +77,18 @@ pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++

77 "\nThis is probably a bug, or a missing error message.\n" ++

78 "Please consider reporting at " ++ bugaddr

79pshow i (CantUnify _ x y e sc s)

80+ = let imps = opt_showimp (idris_options i) in

80− = "Can't unify " ++ show (delab i x)

81+ "Can't unify " ++ showImp imps (delab i x)

81− ++ " with " ++ show (delab i y) ++

82+ ++ " with " ++ showImp imps (delab i y) ++

82-- " (" ++ show x ++ " and " ++ show y ++ ") " ++

83-- " (" ++ show x ++ " and " ++ show y ++ ") " ++

83 case e of

84 case e of

84 Msg "" -> ""

85 Msg "" -> ""

85 _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++

86 _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++

86 if (opt_errContext (idris_options i)) then showSc i sc else ""

87 if (opt_errContext (idris_options i)) then showSc i sc else ""

87pshow i (CantConvert x y env)

88pshow i (CantConvert x y env)

89+ = let imps = opt_showimp (idris_options i) in

88− = "Can't convert " ++ show (delab i x) ++ " with " ++ show (delab i y) ++

90+ "Can't convert " ++ showImp imps (delab i x) ++ " with "

91+ ++ showImp imps (delab i y) ++

89 if (opt_errContext (idris_options i)) then showSc i env else ""

92 if (opt_errContext (idris_options i)) then showSc i env else ""

90pshow i (InfiniteUnify x tm env)

93pshow i (InfiniteUnify x tm env)

91 = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++

94 = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++

src/Idris/ElabDecls.hs+1

@@ -440,6 +440,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

440

441 simpl rt ctxt (Right (x, y)) = Right (normalise ctxt [] x,

442 simplify ctxt rt [] y)

443+-- simpl rt ctxt (Right (x, y)) = Right (x, y)

443 simpl rt ctxt t = t

444 simpl rt ctxt t = t

444

445

445 sameLength ((_, x, _) : xs)

446 sameLength ((_, x, _) : xs)

src/Idris/ElabTerm.hs+3−4

@@ -483,7 +483,7 @@ resolveTC :: Int -> Name -> IState -> ElabD ()

483resolveTC 0 fn ist = fail $ "Can't resolve type class"

484resolveTC 1 fn ist = try (trivial ist) (resolveTC 0 fn ist)

485resolveTC depth fn ist

486− = do compute

486+ = do hnf_compute

487 try (trivial ist)

488 (do t <- goal

489 let insts = findInstances ist t

@@ -647,7 +647,6 @@ runTac autoSolve ist tac = do env <- get_env

647 (tm', ty') <- get_type_val (Var tacn)

648 ctxt <- get_context

649 env <- get_env

650− -- g <- goal

651 let tactic = normalise ctxt env tm'

650 let tactic = normalise ctxt env tm'

652 runReflected tactic

651 runReflected tactic

653-- p <- get_term

652-- p <- get_term

@@ -665,13 +664,13 @@ runTac autoSolve ist tac = do env <- get_env

665 reify (P _ n _) | n == tacm "Solve" = return Solve

664 reify (P _ n _) | n == tacm "Solve" = return Solve

666 reify f@(App _ _)

665 reify f@(App _ _)

667 | (P _ f _, args) <- unApply f = reifyAp f args

666 | (P _ f _, args) <- unApply f = reifyAp f args

668− reify t = fail "Unknown tactic"

667+ reify t = fail ("Unknown tactic " ++ show t)

669

668

670 reifyAp t [l, r] | t == tacm "Try" = liftM2 Try (reify l) (reify r)

669 reifyAp t [l, r] | t == tacm "Try" = liftM2 Try (reify l) (reify r)

671 reifyAp t [Constant (Str x)]

670 reifyAp t [Constant (Str x)]

672 | t == tacm "Refine" = return $ Refine (UN x) []

671 | t == tacm "Refine" = return $ Refine (UN x) []

673 reifyAp t [l, r] | t == tacm "Seq" = liftM2 TSeq (reify l) (reify r)

672 reifyAp t [l, r] | t == tacm "Seq" = liftM2 TSeq (reify l) (reify r)

674− reifyAp f args = fail "Unknown tactic" -- shouldn't happen

673+ reifyAp f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen

675

674

676solveAll = try (do solve; solveAll) (return ())

675solveAll = try (do solve; solveAll) (return ())

677

676

src/Idris/REPL.hs+1−1

@@ -323,7 +323,7 @@ process fn (Prove n')

323process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t

324 ctxt <- getContext

325 ist <- get

326− let tm' = simplify ctxt True [] tm

326+ let tm' = hnf ctxt [] tm

327 iputStrLn (show (delab ist tm'))

328process fn TTShell = do ist <- get

329 let shst = initState (tt_ctxt ist)