5ce7362 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Type class resolution fix

5ce7362Edwin Brady12 years ago

src/Idris/Core/Binary.hs+3−3

compare with master

unifiedsplit

@@ -91,8 +91,8 @@ instance Binary a => Binary (Err' a) where

91 put x

92 put y

93 put z

94− put (CantResolve t) = do putWord8 15

94+ put (CantResolve _ t) = do putWord8 15

95− put t

95+ put t

96 put (CantResolveAlts ns) = do putWord8 16

97 put ns

98 put (IncompleteTerm t) = do putWord8 17

@@ -172,7 +172,7 @@ instance Binary a => Binary (Err' a) where

172 13 -> fmap NoTypeDecl get

173 14 -> do x <- get ; y <- get ; z <- get

174 return $ NotInjective x y z

175− 15 -> fmap CantResolve get

175+ 15 -> fmap (CantResolve False) get

176 16 -> fmap CantResolveAlts get

177 17 -> fmap IncompleteTerm get

178 18 -> return UniverseError

src/Idris/Core/DeepSeq.hs+1−1

@@ -80,7 +80,7 @@ instance NFData Err where

80 rnf (NoTypeDecl x1) = rnf x1 `seq` ()

81 rnf (NotInjective x1 x2 x3)

82 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

83− rnf (CantResolve x1) = rnf x1 `seq` ()

83+ rnf (CantResolve x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

84 rnf (CantResolveAlts x1) = rnf x1 `seq` ()

85 rnf (IncompleteTerm x1) = rnf x1 `seq` ()

86 rnf UniverseError = ()

src/Idris/Core/Elaborate.hs+30−14

@@ -756,20 +756,20 @@ handleError p t1 t2 proofSearch

756

757try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

758try' t1 t2 proofSearch

759− = do s <- get

759+ = do s <- get

760− ps <- get_probs

760+ ps <- get_probs

761− ulog <- getUnifyLog

761+ ulog <- getUnifyLog

762− case prunStateT 999999 False ps t1 s of

762+ case prunStateT 999999 False ps t1 s of

763− OK ((v, _, _), s') -> do put s'

763+ OK ((v, _, _), s') -> do put s'

764− return $! v

764+ return $! v

765− Error e1 -> traceWhen ulog ("try failed " ++ show e1) $

765+ Error e1 -> traceWhen ulog ("try failed " ++ show e1) $

766− if recoverableErr e1 then

766+ if recoverableErr e1 then

767− do case runStateT t2 s of

767+ do case runStateT t2 s of

768− OK (v, s') -> do put s'; return $! v

768+ OK (v, s') -> do put s'; return $! v

769− Error e2 -> if score e1 >= score e2

769+ Error e2 -> if score e1 >= score e2

770− then lift (tfail e1)

770+ then lift (tfail e1)

771− else lift (tfail e2)

771+ else lift (tfail e2)

772− else lift (tfail e1)

772+ else lift (tfail e1)

773 where recoverableErr err@(CantUnify r x y _ _ _)

774 = -- traceWhen r (show err) $

775 r || proofSearch

@@ -782,6 +782,22 @@ try' t1 t2 proofSearch

782 recoverableErr (ElabDebug _ _ _) = False

783 recoverableErr _ = True

784

785+tryCatch :: Elab' aux a -> (Err -> Elab' aux a) -> Elab' aux a

786+tryCatch t1 t2

787+ = do s <- get

788+ ps <- get_probs

789+ ulog <- getUnifyLog

790+ case prunStateT 999999 False ps t1 s of

791+ OK ((v, _, _), s') -> do put s'

792+ return $! v

793+ Error e1 -> traceWhen ulog ("tryCatch failed " ++ show e1) $

794+ case runStateT (t2 e1) s of

795+ OK (v, s') -> do put s'

796+ return $! v

797+ Error e2 -> if score e1 >= score e2

798+ then lift (tfail e1)

799+ else lift (tfail e2)

800+

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

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

786tryWhen True a b = try a b

802tryWhen True a b = try a b

787tryWhen False a b = a

803tryWhen False a b = a

src/Idris/Core/TT.hs+4−3

@@ -155,7 +155,8 @@ data Err' t

155 | WithFnType t

156 | NoTypeDecl Name

157 | NotInjective t t t

158− | CantResolve t

158+ | CantResolve Bool -- ^ True if postponed, False if fatal

159+ t

159 | CantResolveAlts [Name]

160 | CantResolveAlts [Name]

160 | IncompleteTerm t

161 | IncompleteTerm t

161 | UniverseError

162 | UniverseError

@@ -231,7 +232,7 @@ instance Sized Err where

231 size (NoSuchVariable name) = size name

232 size (NoSuchVariable name) = size name

232 size (NoTypeDecl name) = size name

233 size (NoTypeDecl name) = size name

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

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

234− size (CantResolve trm) = size trm

235+ size (CantResolve _ trm) = size trm

235 size (NoRewriting trm) = size trm

236 size (NoRewriting trm) = size trm

236 size (CantResolveAlts _) = 1

237 size (CantResolveAlts _) = 1

237 size (IncompleteTerm trm) = size trm

238 size (IncompleteTerm trm) = size trm

@@ -246,7 +247,7 @@ instance Sized Err where

246

247

247score :: Err -> Int

248score :: Err -> Int

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

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

249−score (CantResolve _) = 20

250+score (CantResolve _ _) = 20

250score (NoSuchVariable _) = 1000

251score (NoSuchVariable _) = 1000

251score (ProofSearchFail e) = score e

252score (ProofSearchFail e) = score e

252score (CantSolveGoal _ _) = 100000

253score (CantSolveGoal _ _) = 100000

src/Idris/Delaborate.hs+1−1

@@ -289,7 +289,7 @@ pprintErr' i (NotInjective p x y) =

289 text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delab i p)) <+>

290 text " when unifying" <+> annTm x (pprintTerm i (delab i x)) <+> text "and" <+>

291 annTm y (pprintTerm i (delab i y))

292−pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

292+pprintErr' i (CantResolve _ c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

293pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

294 align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))

295pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

src/Idris/ElabTerm.hs+45−15

@@ -64,7 +64,7 @@ build ist info emode opts fn tm

64 mapM_ (\n -> when (n `elem` hs) $

65 do focus n

66 g <- goal

67− try (resolveTC True 7 g fn ist)

67+ try (resolveTC True False 7 g fn ist)

68 (movelast n)) ivs

69 ivs <- get_instances

70 hs <- get_holes

@@ -72,7 +72,7 @@ build ist info emode opts fn tm

72 mapM_ (\n -> when (n `elem` hs) $

73 do focus n

74 g <- goal

75− resolveTC True 7 g fn ist) ivs

75+ resolveTC True True 7 g fn ist) ivs

76 tm <- get_term

77 ctxt <- get_context

78 probs <- get_probs

@@ -321,7 +321,7 @@ elab ist info emode opts fn tm

321 UType _ -> elab' ina (Just fc) (PRef fc unitTy)

322 _ -> elab' ina (Just fc) (PRef fc unitCon)

323 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

324− = do g <- goal; resolveTC False 5 g fn ist

324+ = do g <- goal; resolveTC False False 5 g fn ist

325 elab' ina fc (PResolveTC fc')

326 = do c <- getNameFrom (sMN 0 "class")

327 instanceArg c

@@ -540,7 +540,7 @@ elab ist info emode opts fn tm

540 g <- goal

541 hs <- get_holes

542 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)

543− then try (resolveTC True 7 g fn ist)

543+ then try (resolveTC True False 7 g fn ist)

544 (movelast n)

545 else movelast n)

546 (ivs' \\ ivs)

@@ -700,7 +700,7 @@ elab ist info emode opts fn tm

700 env <- get_env

701 hs <- get_holes

702 if all (\n -> not (n `elem` hs)) (freeNames g)

703− then try (resolveTC False 7 g fn ist)

703+ then try (resolveTC False False 7 g fn ist)

704 (movelast n)

705 else movelast n)

706 (ivs' \\ ivs)

@@ -1376,14 +1376,25 @@ proofSearch' ist rec ambigok depth prv top n hints

1376-- Resolve type classes. This will only pick up 'normal' instances, never

1377-- named instances (hence using 'tcname' to check it's a generated instance

1378-- name).

1379+resolveTC :: Bool -- using default Int

1380+ -> Bool -- allow metavariables in the goal

1381+ -> Int -- depth

1382+ -> Term -- top level goal

1383+ -> Name -- top level function name

1379−resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()

1384+ -> IState -> ElabD ()

1380resolveTC = resTC' []

1385resolveTC = resTC' []

1381

1386

1382−resTC' tcs def 0 topg fn ist = fail $ "Can't resolve type class"

1387+resTC' tcs def mvok 0 topg fn ist = fail $ "Can't resolve type class"

1383−resTC' tcs def 1 topg fn ist = try' (trivial' ist) (resolveTC def 0 topg fn ist) True

1388+resTC' tcs def mvok 1 topg fn ist = try' (trivial' ist) (resolveTC def mvok 0 topg fn ist) True

1384−resTC' tcs defaultOn depth topg fn ist

1389+resTC' tcs defaultOn mvok depth topg fn ist

1385− = do compute

1390+ = do compute

1386− g <- goal

1391+ g <- goal

1392+ hs <- get_holes

1393+ let argsok = tcArgsOK g hs

1394+-- trace (show (g,hs,argsok,mvok)) $

1395+ if (not argsok && not mvok)

1396+ then lift $ tfail $ CantResolve True topg

1397+ else do

1387 ptm <- get_term

1398 ptm <- get_term

1388 ulog <- getUnifyLog

1399 ulog <- getUnifyLog

1389 hs <- get_holes

1400 hs <- get_holes

@@ -1400,6 +1411,22 @@ resTC' tcs defaultOn depth topg fn ist

1400 let depth' = if scopeOnly then 2 else depth

1411 let depth' = if scopeOnly then 2 else depth

1401 blunderbuss t depth' stk (stk ++ insts)) True

1412 blunderbuss t depth' stk (stk ++ insts)) True

1402 where

1413 where

1414+ tcArgsOK ty hs | (P _ nc _, as) <- unApply ty, nc == numclass && defaultOn

1415+ = True

1416+ tcArgsOK ty hs -- if any arguments are metavariables, postpone

1417+ = let (f, as) = unApply ty in

1418+ not $ any (isMeta hs) as

1419+

1420+ isMeta :: [Name] -> Term -> Bool

1421+ isMeta ns (P _ n _) = n `elem` ns

1422+ isMeta _ _ = False

1423+

1424+ notHole hs (P _ n _, c)

1425+ | (P _ cn _, _) <- unApply c,

1426+ n `elem` hs && isConName cn (tt_ctxt ist) = False

1427+ | Constant _ <- c = not (n `elem` hs)

1428+ notHole _ _ = True

1429+

1403 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

1430 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

1404 | otherwise = (fail "Can't resolve", show n)

1431 | otherwise = (fail "Can't resolve", show n)

1405

1432

@@ -1427,10 +1454,13 @@ resTC' tcs defaultOn depth topg fn ist

1427

1454

1428 blunderbuss t d stk [] = do -- c <- get_env

1455 blunderbuss t d stk [] = do -- c <- get_env

1429 -- ps <- get_probs

1456 -- ps <- get_probs

1430− lift $ tfail $ CantResolve topg

1457+ lift $ tfail $ CantResolve False topg

1431 blunderbuss t d stk (n:ns)

1458 blunderbuss t d stk (n:ns)

1432 | n /= fn && (n `elem` stk || tcname n)

1459 | n /= fn && (n `elem` stk || tcname n)

1460+ = tryCatch (resolve n d)

1461+ (\e -> case e of

1462+ CantResolve True _ -> lift $ tfail e

1433− = try' (resolve n d) (blunderbuss t d stk ns) True

1463+ _ -> blunderbuss t d stk ns)

1434 | otherwise = blunderbuss t d stk ns

1464 | otherwise = blunderbuss t d stk ns

1435

1465

1436 resolve n depth

1466 resolve n depth

@@ -1459,7 +1489,7 @@ resTC' tcs defaultOn depth topg fn ist

1459 let got = fst (unApply t)

1489 let got = fst (unApply t)

1460 let depth' = if tc' `elem` tcs

1490 let depth' = if tc' `elem` tcs

1461 then depth - 1 else depth

1491 then depth - 1 else depth

1462− resTC' (got : tcs) defaultOn depth' topg fn ist)

1492+ resTC' (got : tcs) defaultOn mvok depth' topg fn ist)

1463 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

1493 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

1464 -- if there's any arguments left, we've failed to resolve

1494 -- if there's any arguments left, we've failed to resolve

1465 hs <- get_holes

1495 hs <- get_holes

@@ -2604,7 +2634,7 @@ reflectErr (NotInjective t1 t2 t3) =

2604 , reflect t2

2634 , reflect t2

2605 , reflect t3

2635 , reflect t3

2606 ]

2636 ]

2607−reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2637+reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2608reflectErr (CantResolveAlts ss) =

2638reflectErr (CantResolveAlts ss) =

2609 raw_apply (Var $ reflErrName "CantResolveAlts")

2639 raw_apply (Var $ reflErrName "CantResolveAlts")

2610 [rawList (Var $ reflm "TTName") (map reflectName ss)]

2640 [rawList (Var $ reflm "TTName") (map reflectName ss)]