38732d8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Heuristic for picking best error message when overloaded alternatives all fail

38732d8Edwin Brady15 years ago

src/Core/Elaborate.hs+8−4

compare with master

unifiedsplit

@@ -404,23 +404,27 @@ try t1 t2 = do s <- get

404

405-- Try a selection of tactics. Exactly one must work, all others must fail

406tryAll :: [(Elab' aux a, String)] -> Elab' aux a

407−tryAll xs = tryAll' [] (fail "Nothing to try") (map fst xs)

407+tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs)

408 where

409 cantResolve :: Elab' aux a

410 cantResolve = fail $ "Couldn't resolve alternative: "

411 ++ showSep ", " (map snd xs)

412

413 tryAll' :: [Elab' aux a] -> -- successes

414− Elab' aux a -> -- last failure

414+ (Elab' aux a, Int) -> -- smallest failure

415 [Elab' aux a] -> -- still to try

416 Elab' aux a

417 tryAll' [res] _ [] = res

418 tryAll' (_:_) _ [] = cantResolve

419− tryAll' [] f [] = f

419+ tryAll' [] (f, _) [] = f

420 tryAll' cs f (x:xs) = do s <- get

421 case runStateT x s of

422 OK (v, s') -> tryAll' ((do put s'

423 return v):cs) f xs

424 Error err -> do put s

425+ tryAll' cs (better err f) xs

426+

427+ better err (f, i) = let s = score err in

425− tryAll' cs (lift (tfail err)) xs

428+ if (s > i) then (lift (tfail err), s)

429+ else (f, i)

426

430

src/Core/TT.hs+8−1

@@ -38,7 +38,7 @@ instance Show FC where

38 show (FC f l) = f ++ ":" ++ show l

40data Err = Msg String

41− | CantUnify Term Term Err

41+ | CantUnify Term Term Err Int -- Int is 'score' - how much we did unify

42 | NotInjective Term Term Term

43 | IncompleteTerm Term

44 | UniverseError

@@ -46,8 +46,15 @@ data Err = Msg String

46 | At FC Err

47 deriving Eq

49+score :: Err -> Int

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

51+score _ = 0

52+

49instance Show Err where

53instance Show Err where

50 show (Msg s) = s

54 show (Msg s) = s

55+ show (CantUnify l r e i) = "CantUnify " ++ show l ++ " " ++ show r ++ " "

56+ ++ show e ++ " " ++ show i

57+ show _ = "Error"

52data TC a = OK a

59data TC a = OK a

53 | Error Err

60 | Error Err

src/Core/Unify.hs+32−18

@@ -14,16 +14,19 @@ import Debug.Trace

15-- terms which need to be injective, with the things we're trying to unify

16-- at the time

17+

17−type UInfo = [(TT Name, TT Name, TT Name)]

18+type Injs = [(TT Name, TT Name, TT Name)]

19+

20+data UInfo = UI Int Injs

19unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)],

22unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)],

20− UInfo)

23+ Injs)

21unify ctxt env topx topy

24unify ctxt env topx topy

22 = case runStateT

25 = case runStateT

23 (un' False [] (normalise ctxt env topx) (normalise ctxt env topy))

26 (un' False [] (normalise ctxt env topx) (normalise ctxt env topy))

24− [] of

27+ (UI 0 []) of

25− OK (v, inj) -> return (filter notTrivial v, inj)

28+ OK (v, (UI _ inj)) -> return (filter notTrivial v, inj)

26− Error e -> tfail $ CantUnify topx topy e

29+ Error e -> tfail $ CantUnify topx topy e 0

27 where

30 where

28 notTrivial (x, P _ x' _) = x /= x'

31 notTrivial (x, P _ x' _) = x /= x'

29 notTrivial _ = True

32 notTrivial _ = True

@@ -36,34 +39,41 @@ unify ctxt env topx topy

36 notP (P _ _ _) = False

39 notP (P _ _ _) = False

37 notP _ = True

40 notP _ = True

42+ sc i = do UI s x <- get

43+ put (UI (s+i) x)

44+

39 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->

45 un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->

40 StateT UInfo

46 StateT UInfo

41 TC [(Name, TT Name)]

47 TC [(Name, TT Name)]

42 un' fn bnames (P Bound x _) (P Bound y _)

48 un' fn bnames (P Bound x _) (P Bound y _)

43− | (x,y) `elem` bnames = return []

49+ | (x,y) `elem` bnames = do sc 1; return []

44 un' fn bnames (P Bound x _) tm

50 un' fn bnames (P Bound x _) tm

45− | holeIn env x = do i <- get

51+ | holeIn env x = do UI s i <- get

46− when (notP tm && fn) $ put ((tm, topx, topy) : i)

52+ when (notP tm && fn) $ put (UI s ((tm, topx, topy) : i))

53+ sc 1

47 return [(x, tm)]

54 return [(x, tm)]

48 un' fn bnames tm (P Bound y _)

55 un' fn bnames tm (P Bound y _)

49− | holeIn env y = do i <- get

56+ | holeIn env y = do UI s i <- get

50− when (notP tm && fn) $ put ((tm, topx, topy) : i)

57+ when (notP tm && fn) $ put (UI s ((tm, topx, topy) : i))

58+ sc 1

51 return [(y, tm)]

59 return [(y, tm)]

52 un' fn bnames (V i) (P Bound x _)

60 un' fn bnames (V i) (P Bound x _)

53− | fst (bnames!!i) == x || snd (bnames!!i) == x = return []

61+ | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

54 un' fn bnames (P Bound x _) (V i)

62 un' fn bnames (P Bound x _) (V i)

55− | fst (bnames!!i) == x || snd (bnames!!i) == x = return []

63+ | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

57 un' fn bnames (App fx ax) (App fy ay)

65 un' fn bnames (App fx ax) (App fy ay)

58 = mplus (do hf <- un' True bnames fx fy

66 = mplus (do hf <- un' True bnames fx fy

59 let ax' = normalise ctxt env (substNames hf ax)

67 let ax' = normalise ctxt env (substNames hf ax)

60 let ay' = normalise ctxt env (substNames hf ay)

68 let ay' = normalise ctxt env (substNames hf ay)

61 ha <- un' False bnames ax' ay'

69 ha <- un' False bnames ax' ay'

70+ sc 1

62 combine bnames hf ha)

71 combine bnames hf ha)

63 (do ha <- un' False bnames ax ay

72 (do ha <- un' False bnames ax ay

64 let fx' = normalise ctxt env (substNames ha fx)

73 let fx' = normalise ctxt env (substNames ha fx)

65 let fy' = normalise ctxt env (substNames ha fy)

74 let fy' = normalise ctxt env (substNames ha fy)

66 hf <- un' False bnames fx' fy'

75 hf <- un' False bnames fx' fy'

76+ sc 1

67 combine bnames hf ha)

77 combine bnames hf ha)

69 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))

79 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))

@@ -75,29 +85,33 @@ unify ctxt env topx topy

75 h2 <- un' False ((x,y):bnames) sx sy

85 h2 <- un' False ((x,y):bnames) sx sy

76 combine bnames h1 h2

86 combine bnames h1 h2

77 un' fn bnames x y

87 un' fn bnames x y

78− | x == y = return []

88+ | x == y = do sc 1; return []

79− | otherwise = fail $ "Can't unify " ++ show x ++ " and " ++ show y

89+ | otherwise = do UI s _ <- get

80− ++ " " ++ show bnames ++ " " ++ show env

90+ lift $ tfail (CantUnify x y (Msg "") s)

82 uB bnames (Let tx vx) (Let ty vy)

92 uB bnames (Let tx vx) (Let ty vy)

83 = do h1 <- un' False bnames tx ty

93 = do h1 <- un' False bnames tx ty

84 h2 <- un' False bnames ty vy

94 h2 <- un' False bnames ty vy

95+ sc 1

85 combine bnames h1 h2

96 combine bnames h1 h2

86 uB bnames (Guess tx vx) (Guess ty vy)

97 uB bnames (Guess tx vx) (Guess ty vy)

87 = do h1 <- un' False bnames tx ty

98 = do h1 <- un' False bnames tx ty

88 h2 <- un' False bnames ty vy

99 h2 <- un' False bnames ty vy

100+ sc 1

89 combine bnames h1 h2

101 combine bnames h1 h2

90− uB bnames (Lam tx) (Lam ty) = un' False bnames tx ty

102+ uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty

91− uB bnames (Pi tx) (Pi ty) = un' False bnames tx ty

103+ uB bnames (Pi tx) (Pi ty) = do sc 1; un' False bnames tx ty

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

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

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

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

94− uB bnames _ _ = fail "Can't unify"

106+ uB bnames x y = do UI s _ <- get

107+ lift $ tfail (CantUnify (binderTy x) (binderTy y) (Msg "") s)

108

96 combine bnames as [] = return as

109 combine bnames as [] = return as

97 combine bnames as ((n, t) : bs)

110 combine bnames as ((n, t) : bs)

98 = case lookup n as of

111 = case lookup n as of

99 Nothing -> combine bnames (as ++ [(n,t)]) bs

112 Nothing -> combine bnames (as ++ [(n,t)]) bs

100 Just t' -> do un' False bnames t t'

113 Just t' -> do un' False bnames t t'

114+ sc 1

101 combine bnames as bs

115 combine bnames as bs

102

116

103holeIn :: Env -> Name -> Bool

117holeIn :: Env -> Name -> Bool

src/Idris/Delaborate.hs+1−1

@@ -64,7 +64,7 @@ delab' ist tm fullname = de [] tm

65pshow :: IState -> Err -> String

66pshow i (Msg s) = s

67−pshow i (CantUnify x y e) = "Can't unify " ++ show (delab i x)

67+pshow i (CantUnify x y e s) = "Can't unify " ++ show (delab i x)

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

69-- ++ "\n\t(" ++ pshow i e ++ ")"

70pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++