d1d672e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Collect all unification errors instead of immediately reporting failure

d1d672eEdwin Brady15 years ago

src/Core/Elaborate.hs+2−2

compare with master

unifiedsplit

@@ -425,6 +425,6 @@ tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs)

425 tryAll' cs (better err f) xs

426

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

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

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

429− else (f, i)

429+ else (f, i)

430

src/Core/ProofState.hs+10−6

@@ -101,6 +101,13 @@ hole _ = False

101

102holeName i = MN i "hole"

103

104+unify' :: Context -> Env -> TT Name -> TT Name -> StateT TState TC [(Name, TT Name)]

105+unify' ctxt env topx topy = do (u, inj, fails) <- lift $ unify ctxt env topx topy

106+ addInj inj

107+ case fails of

108+ [] -> return u

109+ ((_,_,err):_) -> lift $ tfail err

110+

104getName :: Monad m => String -> StateT TState m Name

111getName :: Monad m => String -> StateT TState m Name

105getName tag = do ps <- get

112getName tag = do ps <- get

106 let n = nextname ps

113 let n = nextname ps

@@ -261,8 +268,7 @@ fill :: Raw -> RunTactic

261fill guess ctxt env (Bind x (Hole ty) sc) =

268fill guess ctxt env (Bind x (Hole ty) sc) =

262 do (val, valty) <- lift $ check ctxt env guess

269 do (val, valty) <- lift $ check ctxt env guess

263 s <- get

270 s <- get

264− (ns, inj) <- lift $ unify ctxt env valty ty

271+ ns <- unify' ctxt env valty ty

265− addInj inj

266 ps <- get

272 ps <- get

267 let (uh, uns) = unified ps

273 let (uh, uns) = unified ps

268 put (ps { unified = (uh, uns ++ ns) })

274 put (ps { unified = (uh, uns ++ ns) })

@@ -280,8 +286,7 @@ complete_fill :: RunTactic

280complete_fill ctxt env (Bind x (Guess ty val) sc) =

286complete_fill ctxt env (Bind x (Guess ty val) sc) =

281 do let guess = forget val

287 do let guess = forget val

282 (val', valty) <- lift $ check ctxt env guess

288 (val', valty) <- lift $ check ctxt env guess

283− (ns, inj) <- lift $ unify ctxt env valty ty

289+ ns <- unify' ctxt env valty ty

284− addInj inj

285 ps <- get

290 ps <- get

286 let (uh, uns) = unified ps

291 let (uh, uns) = unified ps

287 put (ps { unified = (uh, uns ++ ns) })

292 put (ps { unified = (uh, uns ++ ns) })

@@ -309,8 +314,7 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

309-- ns <- lift $ unify ctxt env tyv t'

314-- ns <- lift $ unify ctxt env tyv t'

310 case t' of

315 case t' of

311 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in

316 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in

312− do (ns, inj) <- lift $ unify ctxt env s tyv

317+ do ns <- unify' ctxt env s tyv

313− addInj inj

314 ps <- get

318 ps <- get

315 let (uh, uns) = unified ps

319 let (uh, uns) = unified ps

316 put (ps { unified = (uh, uns ++ ns) })

320 put (ps { unified = (uh, uns ++ ns) })

src/Core/Unify.hs+32−16

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

16-- at the time

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

19+type Fails = [(TT Name, TT Name, Err)]

20−data UInfo = UI Int Injs

21+data UInfo = UI Int Injs Fails

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

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

23− Injs)

24+ Injs, Fails)

24unify ctxt env topx topy

25unify ctxt env topx topy

25 = case runStateT

26 = case runStateT

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

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

27− (UI 0 []) of

28+ (UI 0 [] []) of

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

29+ OK (v, UI _ inj fails) -> return (filter notTrivial v, inj, reverse fails)

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

30+-- OK (_, UI s _ ((_,_,f):fs)) -> tfail $ CantUnify topx topy f s

31+ Error e -> tfail e

30 where

32 where

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

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

32 notTrivial _ = True

34 notTrivial _ = True

@@ -39,8 +41,15 @@ unify ctxt env topx topy

39 notP (P _ _ _) = False

41 notP (P _ _ _) = False

40 notP _ = True

42 notP _ = True

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

44+ sc i = do UI s x f <- get

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

45+ put (UI (s+i) x f)

46+

47+ uplus u1 u2 = do UI s i f <- get

48+ r <- u1

49+ UI s _ f' <- get

50+ if (length f == length f')

51+ then return r

52+ else do put (UI s i f); u2

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

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

46 StateT UInfo

55 StateT UInfo

@@ -48,13 +57,13 @@ unify ctxt env topx topy

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

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

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

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

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

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

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

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

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

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

53 sc 1

62 sc 1

54 return [(x, tm)]

63 return [(x, tm)]

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

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

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

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

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

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

58 sc 1

67 sc 1

59 return [(y, tm)]

68 return [(y, tm)]

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

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

@@ -63,7 +72,8 @@ unify ctxt env topx topy

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

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

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

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

75+ = do uplus -- do the second one if the first adds any errors

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

76+ (do hf <- un' True bnames fx fy

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

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

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

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

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

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

@@ -86,8 +96,10 @@ unify ctxt env topx topy

86 combine bnames h1 h2

96 combine bnames h1 h2

87 un' fn bnames x y

97 un' fn bnames x y

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

98 | x == y = do sc 1; return []

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

99+ | otherwise = do UI s i f <- get

100+ let err = CantUnify topx topy (CantUnify x y (Msg "") s) s

101+ put (UI s i ((x, y, err) : f))

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

102+ return [] -- lift $ tfail err

103

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

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

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

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

@@ -103,8 +115,12 @@ unify ctxt env topx topy

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

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

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

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

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

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

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

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

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

119+ let err = CantUnify topx topy

120+ (CantUnify (binderTy x) (binderTy y) (Msg "") s)

121+ s

122+ put (UI s i ((binderTy x, binderTy y, err) : f))

123+ return [] -- lift $ tfail err

108

124

109 combine bnames as [] = return as

125 combine bnames as [] = return as

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

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