d1d672e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Collect all unification errors instead of immediately reporting failure

commitd1d672e293135eb9027a06eb1854085a1096b104 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 13 Jan 2012, 14:07 (15 years ago) parentce10256

3 files changed+44−24

compare with master

unifiedsplit

src/Core/Elaborate.hs+2−2 src/Core/ProofState.hs+10−6 src/Core/Unify.hs+32−16

src/Core/Elaborate.hs+2−2

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

425425 tryAll' cs (better err f) xs

426426

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

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

429− else (f, i)

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

429+ else (f, i)

430430

src/Core/ProofState.hs+10−6

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

101101

102102holeName i = MN i "hole"

103103

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+

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

105112getName tag = do ps <- get

106113 let n = nextname ps

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

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

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

263270 s <- get

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

265− addInj inj

271+ ns <- unify' ctxt env valty ty

266272 ps <- get

267273 let (uh, uns) = unified ps

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

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

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

281287 do let guess = forget val

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

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

284− addInj inj

289+ ns <- unify' ctxt env valty ty

285290 ps <- get

286291 let (uh, uns) = unified ps

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

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

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

310315 case t' of

311316 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

313− addInj inj

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

314318 ps <- get

315319 let (uh, uns) = unified ps

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

src/Core/Unify.hs+32−16

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

1616-- at the time

1717

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

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

1920

20−data UInfo = UI Int Injs

21+data UInfo = UI Int Injs Fails

2122

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

23− Injs)

24+ Injs, Fails)

2425unify ctxt env topx topy

2526 = case runStateT

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

27− (UI 0 []) of

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

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

28+ (UI 0 [] []) of

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

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

31+ Error e -> tfail e

3032 where

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

3234 notTrivial _ = True

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

3941 notP (P _ _ _) = False

4042 notP _ = True

4143

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

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

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

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

4453

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

4655 StateT UInfo

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

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

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

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

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

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

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

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

5362 sc 1

5463 return [(x, tm)]

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

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

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

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

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

5867 sc 1

5968 return [(y, tm)]

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

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

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

6473

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

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

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

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

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

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

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

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

8696 combine bnames h1 h2

8797 un' fn bnames x y

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

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

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

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

102+ return [] -- lift $ tfail err

91103

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

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

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

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

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

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

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

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

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

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

108124

109125 combine bnames as [] = return as

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