239c8ca · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Move resolveTC to ProofSearch.hs

239c8caEdwin Brady11 years ago

idris.cabal+4

compare with master

unifiedsplit

@@ -540,6 +540,10 @@ Extra-source-files:

540 test/interactive008/run

541 test/interactive008/input

542 test/interactive008/expected

543+ test/interactive009/run

544+ test/interactive009/input

545+ test/interactive009/*.idr

546+ test/interactive009/expected

543

547

544 test/io001/run

548 test/io001/run

545 test/io001/*.idr

549 test/io001/*.idr

src/Idris/Elab/Term.hs+8−182

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

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

83 do focus n

84 g <- goal

85− try (resolveTC True False 10 g fn ist)

85+ try (resolveTC' True False 10 g fn ist)

86 (movelast n)) ivs

87 ivs <- get_instances

88 hs <- get_holes

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

91 do focus n

92 g <- goal

93 ptm <- get_term

94− resolveTC True True 10 g fn ist) ivs

94+ resolveTC' True True 10 g fn ist) ivs

95 tm <- get_term

96 ctxt <- get_context

97 probs <- get_probs

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

355 UType _ -> elab' ina (Just fc) (PRef fc [] unitTy)

356 _ -> elab' ina (Just fc) (PRef fc [] unitCon)

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

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

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

359 elab' ina fc (PResolveTC fc')

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

361 instanceArg c

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

699 g <- goal

700 hs <- get_holes

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

702− then try (resolveTC True False 10 g fn ist)

702+ then try (resolveTC' True False 10 g fn ist)

703 (movelast n)

704 else movelast n)

705 (ivs' \\ ivs)

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

871 env <- get_env

872 hs <- get_holes

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

874− then try (resolveTC False False 10 g fn ist)

874+ then try (resolveTC' False False 10 g fn ist)

875 (movelast n)

876 else movelast n)

877 (ivs' \\ ivs)

@@ -1603,20 +1603,6 @@ findHighlight n = do ctxt <- get_context

1603 Nothing -> lift . tfail . InternalMsg $

1604 "Can't find name" ++ show n

1605

1606−-- | Find the names of instances that have been designeated for

1607−-- searching (i.e. non-named instances or instances from Elab scripts)

1608−findInstances :: IState -> Term -> [Name]

1609−findInstances ist t

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

1611− = case lookupCtxt n (idris_classes ist) of

1612− [CI _ _ _ _ _ ins _] ->

1613− [n | (n, True) <- ins, accessible n]

1614− _ -> []

1615− | otherwise = []

1616− where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of

1617− Just (_, Hidden) -> False

1618− _ -> True

1619−

1620-- Try again to solve auto implicits

1606-- Try again to solve auto implicits

1621solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()

1607solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()

1622solveAuto ist fn ambigok n

1608solveAuto ist fn ambigok n

@@ -1642,168 +1628,8 @@ proofSearch' ist rec ambigok depth prv top n psns hints

1642 = do unifyProblems

1628 = do unifyProblems

1643 proofSearch rec prv ambigok (not prv) depth

1629 proofSearch rec prv ambigok (not prv) depth

1644 (elab ist toplevel ERHS [] (sMN 0 "tac")) top n psns hints ist

1630 (elab ist toplevel ERHS [] (sMN 0 "tac")) top n psns hints ist

1645−

1631+resolveTC' di mv depth tm n ist

1646−-- | Resolve type classes. This will only pick up 'normal' instances, never

1632+ = resolveTC di mv depth tm n (elab ist toplevel ERHS [] (sMN 0 "tac")) ist

1647−-- named instances (which is enforced by 'findInstances').

1648−resolveTC :: Bool -- ^ using default Int

1649− -> Bool -- ^ allow metavariables in the goal

1650− -> Int -- ^ depth

1651− -> Term -- ^ top level goal, for error messages

1652− -> Name -- ^ top level function name, to prevent loops

1653− -> IState -> ElabD ()

1654−resolveTC def mvok depth top fn ist

1655− = do hs <- get_holes

1656− resTC' [] def hs depth top fn ist

1657−

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

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

1660−resTC' tcs defaultOn topholes depth topg fn ist

1661− = do compute

1662− g <- goal

1663− -- Resolution can proceed only if there is something concrete in the

1664− -- determining argument positions. Keep track of the holes in the

1665− -- non-determining position, because it's okay for 'trivial' to solve

1666− -- those holes and no others.

1667− let (argsok, okholePos) = case tcArgsOK g topholes of

1668− Nothing -> (False, [])

1669− Just hs -> (True, hs)

1670− if not argsok -- && not mvok)

1671− then lift $ tfail $ CantResolve True topg

1672− else do

1673− ptm <- get_term

1674− ulog <- getUnifyLog

1675− hs <- get_holes

1676− env <- get_env

1677− t <- goal

1678− let (tc, ttypes) = unApply (getRetTy t)

1679− let okholes = case tc of

1680− P _ n _ -> zip (repeat n) okholePos

1681− _ -> []

1682−

1683− traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $

1684− try' (trivialHoles' [] okholes ist)

1685− (do addDefault t tc ttypes

1686− let stk = map fst (filter snd $ elab_stack ist)

1687− let insts = findInstances ist t

1688− blunderbuss t depth stk (stk ++ insts)) True

1689− where

1690− -- returns Just hs if okay, where hs are holes which are okay in the

1691− -- goal, or Nothing if not okay to proceed

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

1693− = Just []

1694− tcArgsOK ty hs -- if any determining arguments are metavariables, postpone

1695− = let (f, as) = unApply (getRetTy ty) in

1696− case f of

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

1698− Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as

1699− Nothing -> if any (isMeta hs) as

1700− then Nothing

1701− else Just []

1702− _ -> if any (isMeta hs) as

1703− then Nothing

1704− else Just []

1705−

1706− -- return the list of argument positions which can safely be a hole

1707− -- or Nothing if one of the determining arguments is a hole

1708− tcDetArgsOK i ds hs (x : xs)

1709− | i `elem` ds = if isMeta hs x

1710− then Nothing

1711− else tcDetArgsOK (i + 1) ds hs xs

1712− | otherwise = do rs <- tcDetArgsOK (i + 1) ds hs xs

1713− case x of

1714− P _ n _ -> Just (i : rs)

1715− _ -> Just rs

1716− tcDetArgsOK _ _ _ [] = Just []

1717−

1718− isMeta :: [Name] -> Term -> Bool

1719− isMeta ns (P _ n _) = n `elem` ns

1720− isMeta _ _ = False

1721−

1722− notHole hs (P _ n _, c)

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

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

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

1726− notHole _ _ = True

1727−

1728− -- HACK! Rather than giving a special name, better to have some kind

1729− -- of flag in ClassInfo structure

1730− chaser (UN nm)

1731− | ('@':'@':_) <- str nm = True -- old way

1732− chaser (SN (ParentN _ _)) = True

1733− chaser (NS n _) = chaser n

1734− chaser _ = False

1735−

1736− numclass = sNS (sUN "Num") ["Classes","Prelude"]

1737−

1738− addDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn

1739− = do focus a

1740− fill (RConstant (AType (ATInt ITBig))) -- default Integer

1741− solve

1742− addDefault t f as

1743− | all boundVar as = return () -- True -- fail $ "Can't resolve " ++ show t

1744− addDefault t f a = return () -- trace (show t) $ return ()

1745−

1746− boundVar (P Bound _ _) = True

1747− boundVar _ = False

1748−

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

1750− -- ps <- get_probs

1751− lift $ tfail $ CantResolve False topg

1752− blunderbuss t d stk (n:ns)

1753− | n /= fn -- && (n `elem` stk)

1754− = tryCatch (resolve n d)

1755− (\e -> case e of

1756− CantResolve True _ -> lift $ tfail e

1757− _ -> blunderbuss t d stk ns)

1758− | otherwise = blunderbuss t d stk ns

1759−

1760− introImps = do g <- goal

1761− case g of

1762− (Bind _ (Pi _ _ _) sc) -> do attack; intro Nothing

1763− num <- introImps

1764− return (num + 1)

1765− _ -> return 0

1766−

1767− solven 0 = return ()

1768− solven n = do solve; solven (n - 1)

1769−

1770− resolve n depth

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

1772− | otherwise

1773− = do lams <- introImps

1774− t <- goal

1775− let (tc, ttypes) = trace (show t) $ unApply (getRetTy t)

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

1777−-- else do

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

1779− let imps = case lookupCtxtName n (idris_implicits ist) of

1780− [] -> []

1781− [args] -> map isImp (snd args) -- won't be overloaded!

1782− xs -> error "The impossible happened - overloading is not expected here!"

1783− ps <- get_probs

1784− tm <- get_term

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

1786− (match_apply (Var n) imps) True

1787− solven lams -- close any implicit lambdas we introduced

1788− ps' <- get_probs

1789− when (length ps < length ps' || unrecoverable ps') $

1790− fail "Can't apply type class"

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

1792− mapM_ (\ (_,n) -> do focus n

1793− t' <- goal

1794− let (tc', ttype) = unApply (getRetTy t')

1795− let got = fst (unApply (getRetTy t))

1796− let depth' = if tc' `elem` tcs

1797− then depth - 1 else depth

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

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

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

1801− hs <- get_holes

1802− ulog <- getUnifyLog

1803− solve

1804− traceWhen ulog ("Got " ++ show n) $ return ()

1805− where isImp (PImp p _ _ _ _) = (True, p)

1806− isImp arg = (False, priority arg)

1807

1633

1808collectDeferred :: Maybe Name -> [Name] -> Context ->

1634collectDeferred :: Maybe Name -> [Name] -> Context ->

1809 Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term

1635 Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term

@@ -2127,7 +1953,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

2127 | n == tacN "prim__ResolveTC", [fn] <- args

1953 | n == tacN "prim__ResolveTC", [fn] <- args

2128 = do g <- goal

1954 = do g <- goal

2129 fn <- reifyTTName fn

1955 fn <- reifyTTName fn

2130− resolveTC False True 100 g fn ist

1956+ resolveTC' False True 100 g fn ist

2131 returnUnit

1957 returnUnit

2132 | n == tacN "prim__Search", [depth, hints] <- args

1958 | n == tacN "prim__Search", [depth, hints] <- args

2133 = do d <- eval depth

1959 = do d <- eval depth

src/Idris/ProofSearch.hs+245−12

@@ -1,9 +1,10 @@

1{-# LANGUAGE PatternGuards #-}

3−module Idris.ProofSearch(trivial, trivialHoles, proofSearch) where

3+module Idris.ProofSearch(trivial, trivialHoles, proofSearch, resolveTC) where

5import Idris.Core.Elaborate hiding (Tactic(..))

6import Idris.Core.TT

7+import Idris.Core.Unify

7import Idris.Core.Evaluate

8import Idris.Core.Evaluate

8import Idris.Core.CaseTree

9import Idris.Core.CaseTree

9import Idris.Core.Typecheck

10import Idris.Core.Typecheck

@@ -24,14 +25,16 @@ import Debug.Trace

24trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()

25trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()

25trivial = trivialHoles [] []

26trivial = trivialHoles [] []

28+trivialHoles :: [Name] -> -- user visible names, when working

29+ -- in interactive mode

27−trivialHoles :: [Name] -> [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()

30+ [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()

28trivialHoles psnames ok elab ist

31trivialHoles psnames ok elab ist

29− = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") [] eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])

32+ = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") [] eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])

30− return ())

33+ return ())

31− (do env <- get_env

34+ (do env <- get_env

32− g <- goal

35+ g <- goal

33− tryAll env

36+ tryAll env

34− return ()) True

37+ return ()) True

35 where

38 where

36 tryAll [] = fail "No trivial solution"

39 tryAll [] = fail "No trivial solution"

37 tryAll ((x, b):xs)

40 tryAll ((x, b):xs)

@@ -41,7 +44,7 @@ trivialHoles psnames ok elab ist

41 g <- goal

44 g <- goal

42 -- anywhere but the top is okay for a hole, if holesOK set

45 -- anywhere but the top is okay for a hole, if holesOK set

43 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))

46 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))

44− holesOK hs (binderTy b) && (null psnames || x `elem` psnames)

47+ (holesOK hs (binderTy b) && (null psnames || x `elem` psnames))

45 then try' (elab (PRef (fileFC "prf") [] x))

48 then try' (elab (PRef (fileFC "prf") [] x))

46 (tryAll xs) True

49 (tryAll xs) True

47 else tryAll xs

50 else tryAll xs

@@ -60,6 +63,50 @@ trivialHoles psnames ok elab ist

60 | (n, p) `elem` ok = holeArgsOK hs n (p + 1) as

63 | (n, p) `elem` ok = holeArgsOK hs n (p + 1) as

61 | otherwise = holesOK hs a && holeArgsOK hs n (p + 1) as

64 | otherwise = holesOK hs a && holeArgsOK hs n (p + 1) as

66+trivialTCs :: [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()

67+trivialTCs ok elab ist

68+ = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") [] eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])

69+ return ())

70+ (do env <- get_env

71+ g <- goal

72+ tryAll env

73+ return ()) True

74+ where

75+ tryAll [] = fail "No trivial solution"

76+ tryAll ((x, b):xs)

77+ = do -- if type of x has any holes in it, move on

78+ hs <- get_holes

79+ let badhs = hs -- filter (flip notElem holesOK) hs

80+ g <- goal

81+ env <- get_env

82+ -- anywhere but the top is okay for a hole, if holesOK set

83+ if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))

84+ (holesOK hs (binderTy b) && tcArg env (binderTy b))

85+ then try' (elab (PRef (fileFC "prf") [] x))

86+ (tryAll xs) True

87+ else tryAll xs

88+

89+ tcArg env ty

90+ | (P _ n _, args) <- unApply (getRetTy (normalise (tt_ctxt ist) env ty))

91+ = case lookupCtxtExact n (idris_classes ist) of

92+ Just _ -> True

93+ _ -> False

94+ | otherwise = False

95+

96+ holesOK hs ap@(App _ _ _)

97+ | (P _ n _, args) <- unApply ap

98+ = holeArgsOK hs n 0 args

99+ holesOK hs (App _ f a) = holesOK hs f && holesOK hs a

100+ holesOK hs (P _ n _) = not (n `elem` hs)

101+ holesOK hs (Bind n b sc) = holesOK hs (binderTy b) &&

102+ holesOK hs sc

103+ holesOK hs _ = True

104+

105+ holeArgsOK hs n p [] = True

106+ holeArgsOK hs n p (a : as)

107+ | (n, p) `elem` ok = holeArgsOK hs n (p + 1) as

108+ | otherwise = holesOK hs a && holeArgsOK hs n (p + 1) as

109+

63cantSolveGoal :: ElabD a

110cantSolveGoal :: ElabD a

64cantSolveGoal = do g <- goal

111cantSolveGoal = do g <- goal

65 env <- get_env

112 env <- get_env

@@ -179,7 +226,9 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

179 ty <- goal

226 ty <- goal

180 when (S.member ty tys) $ fail "Been here before"

227 when (S.member ty tys) $ fail "Been here before"

181 let tys' = S.insert ty tys

228 let tys' = S.insert ty tys

182− try' (trivialHoles psnames [] elab ist)

229+ try' (try' (trivialHoles psnames [] elab ist)

230+ (resolveTC False False 20 ty nroot elab ist)

231+ True)

183 (try' (try' (resolveByCon (d - 1) locs tys')

232 (try' (try' (resolveByCon (d - 1) locs tys')

184 (resolveByLocals (d - 1) locs tys')

233 (resolveByLocals (d - 1) locs tys')

185 True)

234 True)

@@ -188,9 +237,14 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

188 then fail "cantSolveGoal"

237 then fail "cantSolveGoal"

189 else do attack; defer [] nroot; solve) True) True

238 else do attack; defer [] nroot; solve) True) True

190

239

191− getFn d Nothing = []

240+ -- get recursive function name. Only user given names make sense.

192− getFn d (Just f) | d < maxDepth-1 = [f]

241+ getFn d (Just f) | d < maxDepth-1 && usersname f = [f]

193 | otherwise = []

242 | otherwise = []

243+ getFn d _ = []

244+

245+ usersname (UN _) = True

246+ usersname (NS n _) = usersname n

247+ usersname _ = False

194

248

195 resolveByCon d locs tys

249 resolveByCon d locs tys

196 = do t <- goal

250 = do t <- goal

@@ -273,3 +327,182 @@ checkConstructor ist (n : ns) =

273 any conHead args

327 any conHead args

274 conHead t | (P _ n _, _) <- unApply t = isConName n (tt_ctxt ist)

328 conHead t | (P _ n _, _) <- unApply t = isConName n (tt_ctxt ist)

275 | otherwise = False

329 | otherwise = False

330+

331+-- | Resolve type classes. This will only pick up 'normal' instances, never

332+-- named instances (which is enforced by 'findInstances').

333+resolveTC :: Bool -- ^ using default Int

334+ -> Bool -- ^ allow metavariables in the goal

335+ -> Int -- ^ depth

336+ -> Term -- ^ top level goal, for error messages

337+ -> Name -- ^ top level function name, to prevent loops

338+ -> (PTerm -> ElabD ()) -- ^ top level elaborator

339+ -> IState -> ElabD ()

340+resolveTC def mvok depth top fn elab ist

341+ = do hs <- get_holes

342+ resTC' [] def hs depth top fn elab ist

343+

344+resTC' tcs def topholes 0 topg fn elab ist = fail $ "Can't resolve type class"

345+resTC' tcs def topholes 1 topg fn elab ist = try' (trivial elab ist) (resolveTC def False 0 topg fn elab ist) True

346+resTC' tcs defaultOn topholes depth topg fn elab ist

347+ = do compute

348+ g <- goal

349+ -- Resolution can proceed only if there is something concrete in the

350+ -- determining argument positions. Keep track of the holes in the

351+ -- non-determining position, because it's okay for 'trivial' to solve

352+ -- those holes and no others.

353+ let (argsok, okholePos) = case tcArgsOK g topholes of

354+ Nothing -> (False, [])

355+ Just hs -> (True, hs)

356+ if not argsok -- && not mvok)

357+ then lift $ tfail $ CantResolve True topg

358+ else do

359+ ptm <- get_term

360+ ulog <- getUnifyLog

361+ hs <- get_holes

362+ env <- get_env

363+ t <- goal

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

365+ let okholes = case tc of

366+ P _ n _ -> zip (repeat n) okholePos

367+ _ -> []

368+

369+ traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $

370+ try' (trivialTCs okholes elab ist)

371+ (do addDefault t tc ttypes

372+ let stk = map fst (filter snd $ elab_stack ist)

373+ let insts = findInstances ist t

374+ blunderbuss t depth stk (stk ++ insts)) True

375+ where

376+ -- returns Just hs if okay, where hs are holes which are okay in the

377+ -- goal, or Nothing if not okay to proceed

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

379+ = Just []

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

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

382+ case f of

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

384+ Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as

385+ Nothing -> if any (isMeta hs) as

386+ then Nothing

387+ else Just []

388+ _ -> if any (isMeta hs) as

389+ then Nothing

390+ else Just []

391+

392+ -- return the list of argument positions which can safely be a hole

393+ -- or Nothing if one of the determining arguments is a hole

394+ tcDetArgsOK i ds hs (x : xs)

395+ | i `elem` ds = if isMeta hs x

396+ then Nothing

397+ else tcDetArgsOK (i + 1) ds hs xs

398+ | otherwise = do rs <- tcDetArgsOK (i + 1) ds hs xs

399+ case x of

400+ P _ n _ -> Just (i : rs)

401+ _ -> Just rs

402+ tcDetArgsOK _ _ _ [] = Just []

403+

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

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

406+ isMeta _ _ = False

407+

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

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

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

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

412+ notHole _ _ = True

413+

414+ -- HACK! Rather than giving a special name, better to have some kind

415+ -- of flag in ClassInfo structure

416+ chaser (UN nm)

417+ | ('@':'@':_) <- str nm = True -- old way

418+ chaser (SN (ParentN _ _)) = True

419+ chaser (NS n _) = chaser n

420+ chaser _ = False

421+

422+ numclass = sNS (sUN "Num") ["Classes","Prelude"]

423+

424+ addDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn

425+ = do focus a

426+ fill (RConstant (AType (ATInt ITBig))) -- default Integer

427+ solve

428+ addDefault t f as

429+ | all boundVar as = return () -- True -- fail $ "Can't resolve " ++ show t

430+ addDefault t f a = return () -- trace (show t) $ return ()

431+

432+ boundVar (P Bound _ _) = True

433+ boundVar _ = False

434+

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

436+ -- ps <- get_probs

437+ lift $ tfail $ CantResolve False topg

438+ blunderbuss t d stk (n:ns)

439+ | n /= fn -- && (n `elem` stk)

440+ = tryCatch (resolve n d)

441+ (\e -> case e of

442+ CantResolve True _ -> lift $ tfail e

443+ _ -> blunderbuss t d stk ns)

444+ | otherwise = blunderbuss t d stk ns

445+

446+ introImps = do g <- goal

447+ case g of

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

449+ num <- introImps

450+ return (num + 1)

451+ _ -> return 0

452+

453+ solven 0 = return ()

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

455+

456+ resolve n depth

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

458+ | otherwise

459+ = do lams <- introImps

460+ t <- goal

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

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

463+-- else do

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

465+ let imps = case lookupCtxtName n (idris_implicits ist) of

466+ [] -> []

467+ [args] -> map isImp (snd args) -- won't be overloaded!

468+ xs -> error "The impossible happened - overloading is not expected here!"

469+ ps <- get_probs

470+ tm <- get_term

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

472+ (match_apply (Var n) imps) True

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

474+ ps' <- get_probs

475+ when (length ps < length ps' || unrecoverable ps') $

476+ fail "Can't apply type class"

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

478+ mapM_ (\ (_,n) -> do focus n

479+ t' <- goal

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

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

482+ let depth' = if tc' `elem` tcs

483+ then depth - 1 else depth

484+ resTC' (got : tcs) defaultOn topholes depth' topg fn elab ist)

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

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

487+ hs <- get_holes

488+ ulog <- getUnifyLog

489+ solve

490+ traceWhen ulog ("Got " ++ show n) $ return ()

491+ where isImp (PImp p _ _ _ _) = (True, p)

492+ isImp arg = (False, priority arg)

493+

494+-- | Find the names of instances that have been designeated for

495+-- searching (i.e. non-named instances or instances from Elab scripts)

496+findInstances :: IState -> Term -> [Name]

497+findInstances ist t

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

499+ = case lookupCtxt n (idris_classes ist) of

500+ [CI _ _ _ _ _ ins _] ->

501+ [n | (n, True) <- ins, accessible n]

502+ _ -> []

503+ | otherwise = []

504+ where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of

505+ Just (_, Hidden) -> False

506+ _ -> True

507+

508+

test/interactive009/expectednew file+1

@@ -0,0 +1 @@

1+IsSetCons pf prfRec

test/interactive009/inputnew file+1

@@ -0,0 +1 @@

1+:ps 26 rec

test/interactive009/interactive009.idrnew file+27

@@ -0,0 +1,27 @@

1+import Data.Vect

3+%default total

5+data ElemBool : Eq t => t -> Vect n t -> Bool -> Type where

6+ ElemBoolNil : Eq t => ElemBool {t=t} a [] False

7+ ElemBoolCons : Eq t => ElemBool {t=t} x1 xs b -> ElemBool x1 (x2 :: xs) ((x1 == x2) || b)

9+data IsSet : Eq t => Vect n t -> Type where

10+ IsSetNil : Eq t => IsSet {t=t} []

11+ IsSetCons : Eq t => ElemBool {t=t} x xs False -> IsSet xs -> IsSet (x :: xs)

12+

13+fun_1 : Eq t => (x : t) -> (xs : Vect n t) -> (b : Bool ** ElemBool x xs b)

14+fun_1 x [] = (False ** ElemBoolNil)

15+fun_1 x1 (x2 :: xs) =

16+ let (b ** prfRec) = fun_1 x1 xs

17+ in (((x1 == x2) || b) ** (ElemBoolCons prfRec))

18+

19+fun_2 : Eq t => (xs : Vect n t) -> Maybe (IsSet xs)

20+fun_2 [] = Just IsSetNil

21+fun_2 (x :: xs) with (fun_1 x xs)

22+ fun_2 (x :: xs) | (True ** pf) = Nothing

23+ fun_2 (x :: xs) | (False ** pf) with (fun_2 xs)

24+ fun_2 (x :: xs) | (False ** pf) | Nothing = Nothing

25+ fun_2 (x :: xs) | (False ** pf) | (Just prfRec)

26+ = Just ?rec

27+

test/interactive009/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --quiet interactive009.idr < input

3+rm -f *.ibc