23ab26f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Speed improvements when code contains type errors

Identify "unrecoverable" unification failures so that type checking doesn't continue to search all the alternative overloadings and orderings.

commit23ab26fedfcc6afdbeb8f16b1d76478f9e675bb0 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 23 Sep 2012, 18:53 (14 years ago) parentef3aed2

4 files changed+39−16

compare with master

unifiedsplit

src/Core/Elaborate.hs+9−6 src/Core/TT.hs+9−6 src/Core/Unify.hs+20−3 src/Idris/Delaborate.hs+1−1

src/Core/Elaborate.hs+9−6

@@ -435,12 +435,15 @@ try t1 t2 = do s <- get

435435 case runStateT t1 s of

436436 OK (v, s') -> do put s'

437437 return v

438− Error e1 -> do put s

439− case runStateT t2 s of

440− OK (v, s') -> do put s'; return v

441− Error e2 -> if score e1 > score e2

442− then lift (tfail e1)

443− else lift (tfail e2)

438+ Error e1 -> if recoverableErr e1 then

439+ do case runStateT t2 s of

440+ OK (v, s') -> do put s'; return v

441+ Error e2 -> if score e1 > score e2

442+ then lift (tfail e1)

443+ else lift (tfail e2)

444+ else lift (tfail e1)

445+ where recoverableErr (CantUnify r _ _ _ _ _) = r

446+ recoverableErr _ = True

444447

445448tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

446449tryWhen True a b = try a b

src/Core/TT.hs+9−6

@@ -44,7 +44,10 @@ instance Show FC where

4444

4545data Err = Msg String

4646 | InternalMsg String

47− | CantUnify Term Term Err [(Name, Type)] Int -- Int is 'score' - how much we did unify

47+ | CantUnify Bool Term Term Err [(Name, Type)] Int

48+ -- Int is 'score' - how much we did unify

49+ -- Bool indicates recoverability, True indicates more info may make

50+ -- unification succeed

4851 | NoSuchVariable Name

4952 | NotInjective Term Term Term

5053 | CantResolve Term

@@ -59,7 +62,7 @@ data Err = Msg String

5962instance Sized Err where

6063 size (Msg msg) = length msg

6164 size (InternalMsg msg) = length msg

62− size (CantUnify left right err _ score) = size left + size right + size err

65+ size (CantUnify _ left right err _ score) = size left + size right + size err

6366 size (NoSuchVariable name) = size name

6467 size (NotInjective l c r) = size l + size c + size r

6568 size (CantResolve trm) = size trm

@@ -71,7 +74,7 @@ instance Sized Err where

7174 size (Inaccessible _) = 1

7275

7376score :: Err -> Int

74−score (CantUnify _ _ m _ s) = s + score m

77+score (CantUnify _ _ _ m _ s) = s + score m

7578score (CantResolve _) = 20

7679score (NoSuchVariable _) = 1000

7780score _ = 0

@@ -79,14 +82,14 @@ score _ = 0

7982instance Show Err where

8083 show (Msg s) = s

8184 show (InternalMsg s) = "Internal error: " ++ show s

82− show (CantUnify l r e sc i) = "CantUnify " ++ show l ++ " " ++ show r ++ " "

83− ++ show e ++ " in " ++ show sc ++ " " ++ show i

85+ show (CantUnify _ l r e sc i) = "CantUnify " ++ show l ++ " " ++ show r ++ " "

86+ ++ show e ++ " in " ++ show sc ++ " " ++ show i

8487 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

8588 show _ = "Error"

8689

8790instance Pretty Err where

8891 pretty (Msg m) = text m

89− pretty (CantUnify l r e _ i) =

92+ pretty (CantUnify _ l r e _ i) =

9093 if size l + size r > breakingSize then

9194 text "Cannot unify" <+> colon $$

9295 nest nestingSize (pretty l <+> text "and" <+> pretty r) $$

src/Core/Unify.hs+20−3

@@ -104,7 +104,9 @@ unify ctxt env topx topy

104104 un' fn bnames x y

105105 | OK True <- convEq' ctxt x y = do sc 1; return []

106106 | otherwise = do UI s i f <- get

107− let err = CantUnify topx topy (CantUnify x y (Msg "") [] s) (errEnv env) s

107+ let r = recoverable x y

108+ let err = CantUnify r

109+ topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

108110 put (UI s i ((x, y, env, err) : f))

109111 return [] -- lift $ tfail err

110112

@@ -123,8 +125,9 @@ unify ctxt env topx topy

123125 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty

124126 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty

125127 uB bnames x y = do UI s i f <- get

126− let err = CantUnify topx topy

127− (CantUnify (binderTy x) (binderTy y) (Msg "") [] s)

128+ let r = recoverable (binderTy x) (binderTy y)

129+ let err = CantUnify r topx topy

130+ (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s)

128131 (errEnv env) s

129132 put (UI s i ((binderTy x, binderTy y, env, err) : f))

130133 return [] -- lift $ tfail err

@@ -137,6 +140,20 @@ unify ctxt env topx topy

137140 sc 1

138141 combine bnames as bs

139142

143+ -- If there are any clashes of constructors, deem it unrecoverable, otherwise some

144+ -- more work may help.

145+

146+ recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)

147+ | x == y = True

148+ | otherwise = False

149+ recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False

150+ recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False

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

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

153+ recoverable (App f a) (App f' a')

154+ = recoverable f f' && recoverable a a'

155+ recoverable _ _ = True

156+

140157errEnv = map (\(x, b) -> (x, binderTy b))

141158

142159holeIn :: Env -> Name -> Bool

src/Idris/Delaborate.hs+1−1

@@ -75,7 +75,7 @@ pshow i (Msg s) = s

7575pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++

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

7777 "Please consider reporting at " ++ bugaddr

78−pshow i (CantUnify x y e sc s)

78+pshow i (CantUnify _ x y e sc s)

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

8080 ++ " with " ++ show (delab i y) ++

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