git.iko.soy/Idris-dev
on master help sign in
Improve speed of type checking by spotting unification failure quicker
611dd97Edwin Brady
src/Core/ProofState.hs+11−1
compare with master
unifiedsplit
@@ -425,11 +425,21 @@ rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
425 _ -> fail "Not an equality type"
425 _ -> fail "Not an equality type"
426 where
426 where
427 -- to make the P for rewrite, replace syntactic occurrences of l in ty with
427 -- 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
429 mkP lt l r ty | l == ty = lt
429 mkP lt l r ty | l == ty = lt
430 mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
430 mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
431 a' = if (r /= a) then mkP lt l r a else a in
431 a' = if (r /= a) then mkP lt l r a else a in
432 App f' a'
432 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' }
433 mkP lt l r x = x
443 mkP lt l r x = x
434
444
435 rname = MN 0 "replaced"
445 rname = MN 0 "replaced"
src/Core/Unify.hs+34−2
@@ -31,6 +31,7 @@ unify ctxt env topx topy
31 -- trace ("Unifying " ++ show (topx, topy)) $
31 -- trace ("Unifying " ++ show (topx, topy)) $
32 let topxn = normalise ctxt env topx
32 let topxn = normalise ctxt env topx
33 topyn = normalise ctxt env topy in
33 topyn = normalise ctxt env topy in
34+-- trace ("Unifying " ++ show (topxn, topyn)) $
34 case runStateT (un' False [] topxn topyn)
35 case runStateT (un' False [] topxn topyn)
35 (UI 0 [] []) of
36 (UI 0 [] []) of
36 OK (v, UI _ inj fails) -> return (filter notTrivial v, inj, reverse fails)
37 OK (v, UI _ inj fails) -> return (filter notTrivial v, inj, reverse fails)
@@ -61,6 +62,15 @@ unify ctxt env topx topy
61 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
62 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
62 StateT UInfo
63 StateT UInfo
63 TC [(Name, TT Name)]
64 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
64 un' fn bnames (P Bound x _) (P Bound y _)
74 un' fn bnames (P Bound x _) (P Bound y _)
65 | (x,y) `elem` bnames = do sc 1; return []
75 | (x,y) `elem` bnames = do sc 1; return []
66 un' fn bnames (P Bound x _) tm
76 un' fn bnames (P Bound x _) tm
@@ -78,8 +88,11 @@ unify ctxt env topx topy
78 un' fn bnames (P Bound x _) (V i)
88 un' fn bnames (P Bound x _) (V i)
79 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
89 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
80
90
81− un' fn bnames (App fx ax) (App fy ay)
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
82− = do uplus -- do the second one if the first adds any errors
95+ uplus -- do the second one if the first adds any errors
83 (do hf <- un' True bnames fx fy
96 (do hf <- un' True bnames fx fy
84 let ax' = hnormalise hf ctxt env (substNames hf ax)
97 let ax' = hnormalise hf ctxt env (substNames hf ax)
85 let ay' = hnormalise hf ctxt env (substNames hf ay)
98 let ay' = hnormalise hf ctxt env (substNames hf ay)
@@ -94,6 +107,16 @@ unify ctxt env topx topy
94 combine bnames hf ha)
107 combine bnames hf ha)
95 where hnormalise [] _ _ t = t
108 where hnormalise [] _ _ t = t
96 hnormalise ns ctxt env t = normalise ctxt env t
109 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+
97 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
120 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))
98 | n == n' = un' False bnames x y
121 | n == n' = un' False bnames x y
99 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
122 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y
@@ -111,6 +134,15 @@ unify ctxt env topx topy
111 put (UI s i ((x, y, env, err) : f))
134 put (UI s i ((x, y, env, err) : f))
112 return [] -- lift $ tfail err
135 return [] -- lift $ tfail err
113
136
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+
114 uB bnames (Let tx vx) (Let ty vy)
146 uB bnames (Let tx vx) (Let ty vy)
115 = do h1 <- un' False bnames tx ty
147 = do h1 <- un' False bnames tx ty
116 h2 <- un' False bnames ty vy
148 h2 <- un' False bnames ty vy