9e8a976 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge remote-tracking branch 'upstream/master' into wip/tactical

9e8a976David Raymond Christiansen11 years ago

CHANGELOG+1

compare with master

unifiedsplit

@@ -29,6 +29,7 @@ New in 0.9.19:

29* Moved System.Interactive, along with getArgs to the Prelude.

30* Major improvements to reflected elaboration scripts, including the ability to run

31 them in a declaration context and many bug fixes.

32+* "decl syntax" rules to allow syntax extensions at the declaration level

33New in 0.9.18:

34New in 0.9.18:

34--------------

35--------------

idris.cabal+7

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

@@ -655,6 +659,9 @@ Extra-source-files:

655 test/syntax001/run

659 test/syntax001/run

656 test/syntax001/*.idr

660 test/syntax001/*.idr

657 test/syntax001/expected

661 test/syntax001/expected

662+ test/syntax002/run

663+ test/syntax002/*.idr

664+ test/syntax002/expected

658

665

659 test/tactics001/run

666 test/tactics001/run

660 test/tactics001/*.idr

667 test/tactics001/*.idr

src/Idris/AbsSyntaxTree.hs+5

@@ -1246,15 +1246,20 @@ deriving instance NFData SynContext

1246!-}

1247

1248data Syntax = Rule [SSymbol] PTerm SynContext

1249+ | DeclRule [SSymbol] [PDecl]

1249 deriving Show

1250 deriving Show

1250

1251

1251syntaxNames :: Syntax -> [Name]

1252syntaxNames :: Syntax -> [Name]

1252syntaxNames (Rule syms _ _) = mapMaybe ename syms

1253syntaxNames (Rule syms _ _) = mapMaybe ename syms

1253 where ename (Keyword n) = Just n

1254 where ename (Keyword n) = Just n

1254 ename _ = Nothing

1255 ename _ = Nothing

1256+syntaxNames (DeclRule syms _) = mapMaybe ename syms

1257+ where ename (Keyword n) = Just n

1258+ ename _ = Nothing

1255

1259

1256syntaxSymbols :: Syntax -> [SSymbol]

1260syntaxSymbols :: Syntax -> [SSymbol]

1257syntaxSymbols (Rule ss _ _) = ss

1261syntaxSymbols (Rule ss _ _) = ss

1262+syntaxSymbols (DeclRule ss _) = ss

1258{-!

1263{-!

1259deriving instance Binary Syntax

1264deriving instance Binary Syntax

1260deriving instance NFData Syntax

1265deriving instance NFData Syntax

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

@@ -730,7 +730,7 @@ simple_app infer fun arg str =

730 s <- getNameFrom (sMN 0 "s")

731 claim a RType

732 claim b RType

733− claim f (RBind (sMN 0 "aX") (Pi Nothing (Var a) RType) (Var b))

733+ claim f (RBind (sMN 0 "_aX") (Pi Nothing (Var a) RType) (Var b))

734 tm <- get_term

735 start_unify s

736 -- if 'infer' is set, we're assuming it's a simply typed application

src/Idris/Coverage.hs+3−3

@@ -222,7 +222,7 @@ genAll i args

222 pimp (sUN "B") Placeholder True] ++

223 [pexp l, pexp r]) o

224 otherPats o@(PDPair fc hls p t _ v)

225− = ops fc (sUN "Ex_intro")

225+ = ops fc sigmaCon

226 ([pimp (sUN "a") Placeholder True,

227 pimp (sUN "P") Placeholder True] ++

228 [pexp t,pexp v]) o

@@ -243,8 +243,8 @@ genAll i args

243 getExpTm t = getTm t

244

245 -- put it back to its original form

246− resugar (PApp _ (PRef fc hl (UN ei)) [_,_,t,v])

246+ resugar (PApp _ (PRef fc hl n) [_,_,t,v])

247− | ei == txt "Ex_intro"

247+ | n == sigmaCon

248 = PDPair fc [] TypeOrTerm (getTm t) Placeholder (getTm v)

249 resugar (PApp _ (PRef fc hl n) [_,_,l,r])

250 | n == pairCon

src/Idris/DeepSeq.hs+1

@@ -369,6 +369,7 @@ instance NFData SynContext where

369

370instance NFData Syntax where

371 rnf (Rule x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

372+ rnf (DeclRule x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

372

373

373instance NFData SSymbol where

374instance NFData SSymbol where

374 rnf (Keyword x1) = rnf x1 `seq` ()

375 rnf (Keyword x1) = rnf x1 `seq` ()

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

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

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

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

2132 = do g <- goal

1958 = do g <- goal

2133 fn <- reifyTTName fn

1959 fn <- reifyTTName fn

2134− resolveTC False True 100 g fn ist

1960+ resolveTC' False True 100 g fn ist

2135 returnUnit

1961 returnUnit

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

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

2137 = do d <- eval depth

1963 = do d <- eval depth

src/Idris/IBC.hs+17−6

@@ -40,7 +40,7 @@ import System.Directory

40import Codec.Archive.Zip

42ibcVersion :: Word16

43−ibcVersion = 117

43+ibcVersion = 118

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

@@ -2174,14 +2174,25 @@ instance Binary SynContext where

2174

2175instance Binary Syntax where

2176 put (Rule x1 x2 x3)

2177+ = do putWord8 0

2177− = do put x1

2178+ put x1

2178 put x2

2179 put x2

2179 put x3

2180 put x3

2181+ put (DeclRule x1 x2)

2182+ = do putWord8 1

2183+ put x1

2184+ put x2

2180 get

2185 get

2186+ = do i <- getWord8

2187+ case i of

2181− = do x1 <- get

2188+ 0 -> do x1 <- get

2182− x2 <- get

2189+ x2 <- get

2183− x3 <- get

2190+ x3 <- get

2184− return (Rule x1 x2 x3)

2191+ return (Rule x1 x2 x3)

2192+ 1 -> do x1 <- get

2193+ x2 <- get

2194+ return (DeclRule x1 x2)

2195+ _ -> error "Corrupted binary data for Syntax"

2185

2196

2186instance (Binary t) => Binary (DSL' t) where

2197instance (Binary t) => Binary (DSL' t) where

2187 put (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

2198 put (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

src/Idris/Interactive.hs+22−11

@@ -292,12 +292,12 @@ makeLemma fn updatefile l n

292 let isProv = checkProv tyline (show n)

293

294 ctxt <- getContext

295− mty <- case lookupTyName n ctxt of

295+ (fname, mty) <- case lookupTyName n ctxt of

296− [(_,t)] -> return t

296+ [t] -> return t

297− [] -> ierror (NoSuchVariable n)

297+ [] -> ierror (NoSuchVariable n)

298− ns -> ierror (CantResolveAlts (map fst ns))

298+ ns -> ierror (CantResolveAlts (map fst ns))

299 i <- getIState

300− margs <- case lookup n (idris_metavars i) of

300+ margs <- case lookup fname (idris_metavars i) of

301 Just (_, arity, _, _) -> return arity

302 _ -> return (-1)

303

@@ -308,7 +308,7 @@ makeLemma fn updatefile l n

308 let lem = show n ++ " : " ++

309 constraints i classes mty ++

310 showTmOpts (defaultPPOption { ppopt_pinames = True })

311− (stripMNBind skip (delab i mty))

311+ (stripMNBind skip margs (delab i mty))

312 let lem_app = show n ++ appArgs skip margs mty

313

314 if updatefile then

@@ -351,12 +351,13 @@ makeLemma fn updatefile l n

351 appArgs skip i (Bind _ (Pi _ _ _) sc) = appArgs skip (i - 1) sc

352 appArgs skip i _ = ""

353

354+ stripMNBind _ args t | args <= 0 = t

354− stripMNBind skip (PPi b n@(UN c) _ ty sc)

355+ stripMNBind skip args (PPi b n@(UN c) _ ty sc)

355− | (thead c /= '_' && n `notElem` skip) ||

356+ | n `notElem` skip ||

356 take 4 (str c) == "__pi" -- keep in type, but not in app

357 take 4 (str c) == "__pi" -- keep in type, but not in app

357− = PPi b n NoFC ty (stripMNBind skip sc)

358+ = PPi b n NoFC ty (stripMNBind skip (args - 1) sc)

358− stripMNBind skip (PPi b _ _ ty sc) = stripMNBind skip sc

359+ stripMNBind skip args (PPi b _ _ ty sc) = stripMNBind skip (args - 1) sc

359− stripMNBind skip t = t

360+ stripMNBind skip args t = t

360

361

361 constraints :: IState -> [Name] -> Type -> String

362 constraints :: IState -> [Name] -> Type -> String

362 constraints i [] ty = ""

363 constraints i [] ty = ""

@@ -374,13 +375,23 @@ makeLemma fn updatefile l n

374 -- or at the top level themselves.

375 -- or at the top level themselves.

375 -- Also, make type class instances implicit

376 -- Also, make type class instances implicit

376 guessImps :: IState -> Context -> Term -> [Name]

377 guessImps :: IState -> Context -> Term -> [Name]

378+ -- machine names aren't lifted

379+ guessImps ist ctxt (Bind n@(MN _ _) (Pi _ ty _) sc)

380+ = n : guessImps ist ctxt sc

377 guessImps ist ctxt (Bind n (Pi _ ty _) sc)

381 guessImps ist ctxt (Bind n (Pi _ ty _) sc)

378 | guarded ctxt n (substV (P Bound n Erased) sc)

382 | guarded ctxt n (substV (P Bound n Erased) sc)

379 = n : guessImps ist ctxt sc

383 = n : guessImps ist ctxt sc

380 | isClass ist ty

384 | isClass ist ty

381 = n : guessImps ist ctxt sc

385 = n : guessImps ist ctxt sc

386+ | TType _ <- ty = n : guessImps ist ctxt sc

387+ | ignoreName n = n : guessImps ist ctxt sc

382 | otherwise = guessImps ist ctxt sc

388 | otherwise = guessImps ist ctxt sc

383 guessImps ist ctxt _ = []

389 guessImps ist ctxt _ = []

390+

391+ -- TMP HACK unusable name so don't lift

392+ ignoreName n = case show n of

393+ "_aX" -> True

394+ _ -> False

384

395

385 guessClasses :: IState -> Context -> Term -> [Name]

396 guessClasses :: IState -> Context -> Term -> [Name]

386 guessClasses ist ctxt (Bind n (Pi _ ty _) sc)

397 guessClasses ist ctxt (Bind n (Pi _ ty _) sc)

src/Idris/ParseExpr.hs+12−6

@@ -128,8 +128,10 @@ extensions syn rules = extension syn [] (filter isValid rules)

128 isValid (Rule _ _ AnySyntax) = True

129 isValid (Rule _ _ PatternSyntax) = inPattern syn

130 isValid (Rule _ _ TermSyntax) = not (inPattern syn)

131+ isValid (DeclRule _ _) = False

131

132

132data SynMatch = SynTm PTerm | SynBind FC Name -- ^ the FC is for highlighting information

133data SynMatch = SynTm PTerm | SynBind FC Name -- ^ the FC is for highlighting information

134+ deriving Show

133

135

134extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm

136extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm

135extension syn ns rules =

137extension syn ns rules =

@@ -140,7 +142,7 @@ extension syn ns rules =

140 extension syn (n : ns) [Rule ss t ctx | (Rule (_:ss) t ctx) <- rs]

142 extension syn (n : ns) [Rule ss t ctx | (Rule (_:ss) t ctx) <- rs]

141 -- If we have more than one Rule in this bucket, our grammar is

143 -- If we have more than one Rule in this bucket, our grammar is

142 -- nondeterministic.

144 -- nondeterministic.

143− Rule [] ptm _ -> return (flatten (update (mapMaybe id ns) ptm))

145+ Rule [] ptm _ -> return (flatten (updateSynMatch (mapMaybe id ns) ptm))

144 where

146 where

145 ruleGroup [] [] = True

147 ruleGroup [] [] = True

146 ruleGroup (s1:_) (s2:_) = s1 == s2

148 ruleGroup (s1:_) (s2:_) = s1 == s2

@@ -159,15 +161,13 @@ extension syn ns rules =

159 extensionSymbol (Symbol s) = do fc <- symbolFC s

161 extensionSymbol (Symbol s) = do fc <- symbolFC s

160 highlightP fc AnnKeyword

162 highlightP fc AnnKeyword

161 return Nothing

163 return Nothing

162− dropn :: Name -> [(Name, a)] -> [(Name, a)]

164+

163− dropn n [] = []

164− dropn n ((x,t) : xs) | n == x = xs

165− | otherwise = (x,t):dropn n xs

166−

167 flatten :: PTerm -> PTerm -- flatten application

165 flatten :: PTerm -> PTerm -- flatten application

168 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

166 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

169 flatten t = t

167 flatten t = t

170

168

169+updateSynMatch = update

170+ where

171 updateB :: [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)

172 updateB ns (n, fc) = case lookup n ns of

173 Just (SynBind tfc t) -> (t, tfc)

@@ -251,6 +251,12 @@ extension syn ns rules =

251

252 updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)

253 updTacImp _ x = x

254+

255+ dropn :: Name -> [(Name, a)] -> [(Name, a)]

256+ dropn n [] = []

257+ dropn n ((x,t) : xs) | n == x = xs

258+ | otherwise = (x,t):dropn n xs

259+

254

260

255{- | Parses a (normal) built-in expression

261{- | Parses a (normal) built-in expression

256@

262@

src/Idris/Parser.hs+137−2

@@ -184,7 +184,13 @@ Decl ::=

184@

185-}

186decl :: SyntaxInfo -> IdrisParser [PDecl]

187+decl syn = try (externalDecl syn)

188+ <|> internalDecl syn

189+ <?> "declaration"

190+

191+internalDecl :: SyntaxInfo -> IdrisParser [PDecl]

192+internalDecl syn

187−decl syn = do fc <- getFC

193+ = do fc <- getFC

188 -- if we're after maxline, stop here

194 -- if we're after maxline, stop here

189 let continue = case maxline syn of

195 let continue = case maxline syn of

190 Nothing -> True

196 Nothing -> True

@@ -235,6 +241,124 @@ decl' syn = fixity

235 <|> runElabDecl syn

241 <|> runElabDecl syn

236 <?> "declaration"

242 <?> "declaration"

237

243

244+externalDecl :: SyntaxInfo -> IdrisParser [PDecl]

245+externalDecl syn = do i <- get

246+ notEndBlock

247+ FC fn start _ <- getFC

248+ decls <- declExtensions syn (syntaxRulesList $ syntax_rules i)

249+ FC _ _ end <- getFC

250+ let outerFC = FC fn start end

251+ return decls

252+

253+declExtensions :: SyntaxInfo -> [Syntax] -> IdrisParser [PDecl]

254+declExtensions syn rules = declExtension syn [] (filter isDeclRule rules)

255+ <?> "user-defined declaration"

256+ where

257+ isDeclRule (DeclRule _ _) = True

258+ isDeclRule _ = False

259+

260+declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax]

261+ -> IdrisParser [PDecl]

262+declExtension syn ns rules =

263+ choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->

264+ case head rs of -- can never be []

265+ DeclRule (symb:_) _ -> try $ do

266+ n <- extSymbol symb

267+ declExtension syn (n : ns) [DeclRule ss t | (DeclRule (_:ss) t) <- rs]

268+ -- If we have more than one Rule in this bucket, our grammar is

269+ -- nondeterministic.

270+ DeclRule [] dec -> let r = map (update (mapMaybe id ns)) dec in

271+ return r

272+

273+ where

274+ update :: [(Name, SynMatch)] -> PDecl -> PDecl

275+ update ns = updateNs ns . fmap (updateRefs ns) . fmap (updateSynMatch ns)

276+

277+ updateRefs ns = mapPT newref

278+ where

279+ newref (PRef fc fcs n) = PRef fc fcs (updateB ns n)

280+ newref t = t

281+

282+ -- Below is a lot of tedious boilerplate which updates any top level

283+ -- names in the declaration. It will only change names which are bound in

284+ -- the declaration (including method names in classes and field names in

285+ -- record declarations, not including pattern variables)

286+ updateB :: [(Name, SynMatch)] -> Name -> Name

287+ updateB ns (NS n mods) = NS (updateB ns n) mods

288+ updateB ns n = case lookup n ns of

289+ Just (SynBind tfc t) -> t

290+ _ -> n

291+

292+ updateNs :: [(Name, SynMatch)] -> PDecl -> PDecl

293+ updateNs ns (PTy doc argdoc s fc o n fc' t)

294+ = PTy doc argdoc s fc o (updateB ns n) fc' t

295+ updateNs ns (PClauses fc o n cs)

296+ = PClauses fc o (updateB ns n) (map (updateClause ns) cs)

297+ updateNs ns (PCAF fc n t) = PCAF fc (updateB ns n) t

298+ updateNs ns (PData ds cds s fc o dat)

299+ = PData ds cds s fc o (updateData ns dat)

300+ updateNs ns (PParams fc ps ds) = PParams fc ps (map (updateNs ns) ds)

301+ updateNs ns (PNamespace s fc ds) = PNamespace s fc (map (updateNs ns) ds)

302+ updateNs ns (PRecord doc syn fc o n fc' ps pdocs fields cname cdoc s)

303+ = PRecord doc syn fc o (updateB ns n) fc' ps pdocs

304+ (map (updateField ns) fields)

305+ (updateRecCon ns cname)

306+ cdoc

307+ s

308+ updateNs ns (PClass docs s fc cs cn fc' ps pdocs pdets ds cname cdocs)

309+ = PClass docs s fc cs (updateB ns cn) fc' ps pdocs pdets

310+ (map (updateNs ns) ds)

311+ (updateRecCon ns cname)

312+ cdocs

313+ updateNs ns (PInstance docs pdocs s fc cs cn fc' ps ity ni ds)

314+ = PInstance docs pdocs s fc cs (updateB ns cn) fc'

315+ ps ity (fmap (updateB ns) ni)

316+ (map (updateNs ns) ds)

317+ updateNs ns (PMutual fc ds) = PMutual fc (map (updateNs ns) ds)

318+ updateNs ns (PProvider docs s fc fc' pw n)

319+ = PProvider docs s fc fc' pw (updateB ns n)

320+ updateNs ns d = d

321+

322+ updateRecCon ns Nothing = Nothing

323+ updateRecCon ns (Just (n, fc)) = Just (updateB ns n, fc)

324+

325+ updateField ns (m, p, t, doc) = (updateRecCon ns m, p, t, doc)

326+

327+ updateClause ns (PClause fc n t ts t' ds)

328+ = PClause fc (updateB ns n) t ts t' (map (update ns) ds)

329+ updateClause ns (PWith fc n t ts t' m ds)

330+ = PWith fc (updateB ns n) t ts t' m (map (update ns) ds)

331+ updateClause ns (PClauseR fc ts t ds)

332+ = PClauseR fc ts t (map (update ns) ds)

333+ updateClause ns (PWithR fc ts t m ds)

334+ = PWithR fc ts t m (map (update ns) ds)

335+

336+ updateData ns (PDatadecl n fc t cs)

337+ = PDatadecl (updateB ns n) fc t (map (updateCon ns) cs)

338+ updateData ns (PLaterdecl n fc t)

339+ = PLaterdecl (updateB ns n) fc t

340+

341+ updateCon ns (cd, ads, cn, fc, ty, fc', fns)

342+ = (cd, ads, updateB ns cn, fc, ty, fc', fns)

343+

344+ ruleGroup [] [] = True

345+ ruleGroup (s1:_) (s2:_) = s1 == s2

346+ ruleGroup _ _ = False

347+

348+ extSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))

349+ extSymbol (Keyword n) = do fc <- reservedFC (show n)

350+ highlightP fc AnnKeyword

351+ return Nothing

352+ extSymbol (Expr n) = do tm <- expr syn

353+ return $ Just (n, SynTm tm)

354+ extSymbol (SimpleExpr n) = do tm <- simpleExpr syn

355+ return $ Just (n, SynTm tm)

356+ extSymbol (Binding n) = do (b, fc) <- name

357+ return $ Just (n, SynBind fc b)

358+ extSymbol (Symbol s) = do fc <- symbolFC s

359+ highlightP fc AnnKeyword

360+ return Nothing

361+

238{- | Parses a syntax extension declaration (and adds the rule to parser state)

362{- | Parses a syntax extension declaration (and adds the rule to parser state)

239

363

240@

364@

@@ -303,6 +427,17 @@ syntaxRule syn

303 tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]

427 tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]

304 terminator

428 terminator

305 return (Rule (mkSimple syms) tm sty)

429 return (Rule (mkSimple syms) tm sty)

430+ <|> do reservedHL "decl"; reservedHL "syntax"

431+ syms <- some syntaxSym

432+ when (all isExpr syms) $ unexpected "missing keywords in syntax rule"

433+ let ns = mapMaybe getName syms

434+ when (length ns /= length (nub ns))

435+ $ unexpected "repeated variable in syntax rule"

436+ lchar '='

437+ openBlock

438+ dec <- some (decl syn)

439+ closeBlock

440+ return (DeclRule (mkSimple syms) (concat dec))

306 where

441 where

307 isExpr (Expr _) = True

442 isExpr (Expr _) = True

308 isExpr _ = False

443 isExpr _ = False

@@ -317,7 +452,7 @@ syntaxRule syn

317 mkSimple es

452 mkSimple es

318 -- Can't parse a full expression followed by operator like characters due to ambiguity

453 -- Can't parse a full expression followed by operator like characters due to ambiguity

319 mkSimple' (Expr e : Symbol s : es)

454 mkSimple' (Expr e : Symbol s : es)

320− | takeWhile (`elem` opChars) ts /= "" && ts `notElem` invalidOperators = SimpleExpr e : Symbol s : mkSimple' es

455+ | takeWhile (`elem` opChars) ts /= "" = SimpleExpr e : Symbol s : mkSimple' es

321 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s

456 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s

322 mkSimple' (e : es) = e : mkSimple' es

457 mkSimple' (e : es) = e : mkSimple' es

323 mkSimple' [] = []

458 mkSimple' [] = []

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

test/syntax002/expectednew file+2

@@ -0,0 +1,2 @@

1+Nothing

2+7

test/syntax002/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ syntax002.idr -o syntax002

3+./syntax002

4+rm -f syntax002 *.ibc

test/syntax002/syntax002.idrnew file+22

@@ -0,0 +1,22 @@

2+decl syntax fun {n} ":" [ty] "=" [def]

3+ = n : ty

4+ n = def

6+decl syntax newtype {tname} "=" {conname} [tysyn]

7+ = data tname = conname tysyn

9+decl syntax EmptyShow {n} =

10+ instance Show n where

11+ show x = "Nothing"

12+

13+fun add : (Int -> Int -> Int) = \x, y => x + y

14+

15+newtype Foo = MkFoo Int

16+

17+EmptyShow Foo

18+

19+main : IO ()

20+main = do printLn (MkFoo 42)

21+ printLn (add 3 4)

22+