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

git.iko.soy/Idris-dev

on master help sign in

Speed improvements when code contains type errors

23ab26fEdwin Brady14 years ago

src/Core/Elaborate.hs+9−6

compare with master

unifiedsplit

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

435 case runStateT t1 s of

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

437 return v

438− Error e1 -> do put s

438+ Error e1 -> if recoverableErr e1 then

439− case runStateT t2 s of

439+ do case runStateT t2 s of

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

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

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

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

442− then lift (tfail e1)

442+ then lift (tfail e1)

443− else lift (tfail e2)

443+ else lift (tfail e2)

444+ else lift (tfail e1)

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

446+ recoverableErr _ = True

444

447

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

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

446tryWhen True a b = try a b

449tryWhen True a b = try a b

src/Core/TT.hs+9−6

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

45data Err = Msg String

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

48 | NoSuchVariable Name

51 | NoSuchVariable Name

49 | NotInjective Term Term Term

52 | NotInjective Term Term Term

50 | CantResolve Term

53 | CantResolve Term

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

59instance Sized Err where

62instance Sized Err where

60 size (Msg msg) = length msg

63 size (Msg msg) = length msg

61 size (InternalMsg msg) = length msg

64 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

63 size (NoSuchVariable name) = size name

66 size (NoSuchVariable name) = size name

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

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

65 size (CantResolve trm) = size trm

68 size (CantResolve trm) = size trm

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

71 size (Inaccessible _) = 1

74 size (Inaccessible _) = 1

73score :: Err -> Int

76score :: Err -> Int

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

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

75score (CantResolve _) = 20

78score (CantResolve _) = 20

76score (NoSuchVariable _) = 1000

79score (NoSuchVariable _) = 1000

77score _ = 0

80score _ = 0

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

79instance Show Err where

82instance Show Err where

80 show (Msg s) = s

83 show (Msg s) = s

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

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

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

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

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

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

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

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

85 show _ = "Error"

88 show _ = "Error"

87instance Pretty Err where

90instance Pretty Err where

88 pretty (Msg m) = text m

91 pretty (Msg m) = text m

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

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

90 if size l + size r > breakingSize then

93 if size l + size r > breakingSize then

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

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

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

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

src/Core/Unify.hs+20−3

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

104 un' fn bnames x y

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

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

107+ let r = recoverable x y

108+ let err = CantUnify r

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

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

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

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

109 return [] -- lift $ tfail err

111 return [] -- lift $ tfail err

110

112

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

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

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

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

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

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

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

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

126− let err = CantUnify topx topy

129+ let err = CantUnify r topx topy

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

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

128 (errEnv env) s

131 (errEnv env) s

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

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

130 return [] -- lift $ tfail err

133 return [] -- lift $ tfail err

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

137 sc 1

140 sc 1

138 combine bnames as bs

141 combine bnames as bs

139

142

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+

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

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

141

158

142holeIn :: Env -> Name -> Bool

159holeIn :: Env -> Name -> Bool

src/Idris/Delaborate.hs+1−1

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

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

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

77 "Please consider reporting at " ++ bugaddr

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

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

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

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

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