3ed4dcf · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow scoped implicits in instance declarations

3ed4dcfEdwin Brady12 years ago

libs/prelude/Prelude.idr+3

compare with master

unifiedsplit

@@ -134,6 +134,9 @@ instance Show a => Show (Maybe a) where

134 show Nothing = "Nothing"

135 show (Just x) = "Just " ++ show x

136

137+instance (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where

138+ show (y ** prf) = show y ++ " ** " ++ show prf

139+

137---- Functor instances

140---- Functor instances

138

141

139instance Functor PrimIO where

142instance Functor PrimIO where

src/Idris/Elab/Term.hs+23−11

@@ -1376,7 +1376,7 @@ pruneByType _ t _ as = as

1376

1377findInstances :: IState -> Term -> [Name]

1378findInstances ist t

1379− | (P _ n _, _) <- unApply t

1379+ | (P _ n _, _) <- unApply (getRetTy t)

1380 = case lookupCtxt n (idris_classes ist) of

1381 [CI _ _ _ _ _ ins _] -> filter accessible ins

1382 _ -> []

@@ -1427,17 +1427,17 @@ resTC' tcs defaultOn topholes depth topg fn ist

1427 = do compute

1428 g <- goal

1429 let argsok = tcArgsOK g topholes

1430−-- trace (show (g,hs,argsok,topholes)) $

1431 if not argsok -- && not mvok)

1430 if not argsok -- && not mvok)

1432 then lift $ tfail $ CantResolve True topg

1431 then lift $ tfail $ CantResolve True topg

1433 else do

1432 else do

1434 ptm <- get_term

1433 ptm <- get_term

1435 ulog <- getUnifyLog

1434 ulog <- getUnifyLog

1436 hs <- get_holes

1435 hs <- get_holes

1436+ env <- get_env

1437− traceWhen ulog ("Resolving class " ++ show g) $

1437+ traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env) $

1438 try' (trivial' ist)

1439 (do t <- goal

1440− let (tc, ttypes) = unApply t

1440+ let (tc, ttypes) = unApply (getRetTy t)

1441 scopeOnly <- needsDefault t tc ttypes

1442 let stk = elab_stack ist

1443 let insts_in = findInstances ist t

@@ -1447,10 +1447,10 @@ resTC' tcs defaultOn topholes depth topg fn ist

1447 let depth' = if scopeOnly then 2 else depth

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

1449 where

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

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

1451 = True

1452 tcArgsOK ty hs -- if any arguments are metavariables, postpone

1453− = let (f, as) = unApply ty in

1453+ = let (f, as) = unApply (getRetTy ty) in

1454 case f of

1455 P _ cn _ -> case lookupCtxtExact cn (idris_classes ist) of

1456 Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as

@@ -1467,7 +1467,7 @@ resTC' tcs defaultOn topholes depth topg fn ist

1467 isMeta _ _ = False

1468

1469 notHole hs (P _ n _, c)

1470− | (P _ cn _, _) <- unApply c,

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

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

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

1473 notHole _ _ = True

@@ -1508,11 +1508,22 @@ resTC' tcs defaultOn topholes depth topg fn ist

1508 _ -> blunderbuss t d stk ns)

1509 | otherwise = blunderbuss t d stk ns

1510

1511+ introImps = do g <- goal

1512+ case g of

1513+ (Bind _ (Pi _ _ _) sc) -> do attack; intro Nothing

1514+ num <- introImps

1515+ return (num + 1)

1516+ _ -> return 0

1517+

1518+ solven 0 = return ()

1519+ solven n = do solve; solven (n - 1)

1520+

1511 resolve n depth

1521 resolve n depth

1512 | depth == 0 = fail $ "Can't resolve type class"

1522 | depth == 0 = fail $ "Can't resolve type class"

1513 | otherwise

1523 | otherwise

1524+ = do lams <- introImps

1514− = do t <- goal

1525+ t <- goal

1515− let (tc, ttypes) = unApply t

1526+ let (tc, ttypes) = trace (show t) $ unApply (getRetTy t)

1516-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist

1527-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist

1517-- else do

1528-- else do

1518 -- if there's a hole in the goal, don't even try

1529 -- if there's a hole in the goal, don't even try

@@ -1524,14 +1535,15 @@ resTC' tcs defaultOn topholes depth topg fn ist

1524 tm <- get_term

1535 tm <- get_term

1525 args <- map snd <$> try' (apply (Var n) imps)

1536 args <- map snd <$> try' (apply (Var n) imps)

1526 (match_apply (Var n) imps) True

1537 (match_apply (Var n) imps) True

1538+ solven lams -- close any implicit lambdas we introduced

1527 ps' <- get_probs

1539 ps' <- get_probs

1528 when (length ps < length ps' || unrecoverable ps') $

1540 when (length ps < length ps' || unrecoverable ps') $

1529 fail "Can't apply type class"

1541 fail "Can't apply type class"

1530-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

1542-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

1531 mapM_ (\ (_,n) -> do focus n

1543 mapM_ (\ (_,n) -> do focus n

1532 t' <- goal

1544 t' <- goal

1533− let (tc', ttype) = unApply t'

1545+ let (tc', ttype) = unApply (getRetTy t')

1534− let got = fst (unApply t)

1546+ let got = fst (unApply (getRetTy t))

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

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

1536 then depth - 1 else depth

1548 then depth - 1 else depth

1537 resTC' (got : tcs) defaultOn topholes depth' topg fn ist)

1549 resTC' (got : tcs) defaultOn topholes depth' topg fn ist)

src/Idris/ParseExpr.hs+2−2

@@ -966,9 +966,9 @@ constraintList1 syn = try (do lchar '('

966 return [(defname, t)])

967 <?> "type constraint list"

968 where nexpr = try (do n <- name; lchar ':'

969− e <- expr' (disallowImp syn)

969+ e <- expr syn

970 return (n, e))

971− <|> do e <- expr' (disallowImp syn)

971+ <|> do e <- expr syn

972 return (defname, e)

973 defname = sMN 0 "constrarg"

974