git.iko.soy/Idris-dev
on master help sign in
Improve speed of type checking by spotting unification failure quicker
commit611dd972453910afc68a3fc8ba675abfdb68a475 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 2 Oct 2012, 10:52 (14 years ago) parentb74161f
2 files changed+45−3
compare with master
unifiedsplit
src/Core/ProofState.hs+11−1 src/Core/Unify.hs+34−2
src/Core/ProofState.hs+11−1
@@ -425,11 +425,21 @@ rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
425425 _ -> fail "Not an equality type"
426426 where
427427 -- to make the P for rewrite, replace syntactic occurrences of l in ty with
428− -- and x, and put \x : lt in front
428+ -- an x, and put \x : lt in front
429429 mkP lt l r ty | l == ty = lt
430430 mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
431431 a' = if (r /= a) then mkP lt l r a else a in
432432 App f' a'
433+ mkP lt l r (Bind n b sc)
434+ = let b' = mkPB b
435+ sc' = if (r /= sc) then mkP lt l r sc else sc in
436+ Bind n b' sc'
437+ where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t
438+ v' = if (r /= v) then mkP lt l r v else v in
439+ Let t' v'
440+ mkPB b = let ty = binderTy b
441+ ty' = if (r /= ty) then mkP lt l r ty else ty in
442+ b { binderTy = ty' }
433443 mkP lt l r x = x
434444
435445 rname = MN 0 "replaced"
src/Core/Unify.hs+34−2
@@ -31,6 +31,7 @@ unify ctxt env topx topy
3131 -- trace ("Unifying " ++ show (topx, topy)) $
3232 let topxn = normalise ctxt env topx
3333 topyn = normalise ctxt env topy in
34+-- trace ("Unifying " ++ show (topxn, topyn)) $
3435 case runStateT (un' False [] topxn topyn)
3536 (UI 0 [] []) of
3637 OK (v, UI _ inj fails) -> return (filter notTrivial v, inj, reverse fails)
@@ -61,6 +62,15 @@ unify ctxt env topx topy
6162 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
6263 StateT UInfo
6364 TC [(Name, TT Name)]
65+ un' fn names x y | x == y = return [] -- shortcut
66+ un' fn names topx@(P (DCon _ _) x _) topy@(P (DCon _ _) y _)
67+ | x /= y = unifyFail topx topy
68+ un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)
69+ | x /= y = unifyFail topx topy
70+ un' fn names topx@(P (DCon _ _) x _) topy@(P (TCon _ _) y _)
71+ = unifyFail topx topy
72+ un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _) y _)
73+ = unifyFail topx topy
6474 un' fn bnames (P Bound x _) (P Bound y _)
6575 | (x,y) `elem` bnames = do sc 1; return []
6676 un' fn bnames (P Bound x _) tm
@@ -78,8 +88,11 @@ unify ctxt env topx topy
7888 un' fn bnames (P Bound x _) (V i)
7989 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
8090
81− un' fn bnames (App fx ax) (App fy ay)
82− = do uplus -- do the second one if the first adds any errors
91+ un' fn bnames appx@(App fx ax) appy@(App fy ay)
92+ = do let (headx, _) = unApply fx
93+ let (heady, _) = unApply fy
94+ checkHeads headx heady
95+ uplus -- do the second one if the first adds any errors
8396 (do hf <- un' True bnames fx fy
8497 let ax' = hnormalise hf ctxt env (substNames hf ax)
8598 let ay' = hnormalise hf ctxt env (substNames hf ay)
@@ -94,6 +107,16 @@ unify ctxt env topx topy
94107 combine bnames hf ha)
95108 where hnormalise [] _ _ t = t
96109 hnormalise ns ctxt env t = normalise ctxt env t
110+ checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)
111+ | x /= y = unifyFail appx appy
112+ checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)
113+ | x /= y = unifyFail appx appy
114+ checkHeads (P (DCon _ _) x _) (P (TCon _ _) y _)
115+ = unifyFail appx appy
116+ checkHeads (P (TCon _ _) x _) (P (DCon _ _) y _)
117+ = unifyFail appx appy
118+ checkHeads _ _ = return []
119+
97120 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
98121 | n == n' = un' False bnames x y
99122 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
@@ -111,6 +134,15 @@ unify ctxt env topx topy
111134 put (UI s i ((x, y, env, err) : f))
112135 return [] -- lift $ tfail err
113136
137+ -- shortcut failure, if we *know* nothing can fix it
138+ unifyFail x y = do UI s i f <- get
139+ let r = recoverable x y
140+ let err = CantUnify r
141+ topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s
142+ put (UI s i ((x, y, env, err) : f))
143+ lift $ tfail err
144+
145+
114146 uB bnames (Let tx vx) (Let ty vy)
115147 = do h1 <- un' False bnames tx ty
116148 h2 <- un' False bnames ty vy