ee32989 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Search in current elaboration stack for instances

ee32989Edwin Brady12 years ago

src/Idris/AbsSyntax.hs+10

compare with master

unifiedsplit

@@ -315,6 +315,16 @@ getNameHints i n =

315addToCalledG :: Name -> [Name] -> Idris ()

316addToCalledG n ns = return () -- TODO

317

318+push_estack :: Name -> Idris ()

319+push_estack n = do i <- getIState

320+ putIState (i { elab_stack = n : elab_stack i })

321+

322+pop_estack :: Idris ()

323+pop_estack = do i <- getIState

324+ putIState (i { elab_stack = ptail (elab_stack i) })

325+ where ptail [] = []

326+ ptail (x : xs) = xs

327+

318-- Add a class instance function. Dodgy hack: Put integer instances first in the

328-- Add a class instance function. Dodgy hack: Put integer instances first in the

319-- list so they are resolved by default.

329-- list so they are resolved by default.

320-- Dodgy hack 2: put constraint chasers (@@) last

330-- Dodgy hack 2: put constraint chasers (@@) last

src/Idris/AbsSyntaxTree.hs+3−2

@@ -214,7 +214,8 @@ data IState = IState {

214 idris_postulates :: S.Set Name,

215 idris_whocalls :: Maybe (M.Map Name [Name]),

216 idris_callswho :: Maybe (M.Map Name [Name]),

217− idris_repl_defs :: [Name] -- ^ List of names that were defined in the repl, and can be re-/un-defined

217+ idris_repl_defs :: [Name], -- ^ List of names that were defined in the repl, and can be re-/un-defined

218+ elab_stack :: [Name] -- ^ Stack of names currently being elaborated

218 }

219 }

219

220

220-- Required for parsers library, and therefore trifecta

221-- Required for parsers library, and therefore trifecta

@@ -295,7 +296,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

295 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

296 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

296 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

297 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

297 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

298 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

298− AutomaticWidth S.empty Nothing Nothing []

299+ AutomaticWidth S.empty Nothing Nothing [] []

299

300

300-- | The monad for the main REPL - reading and processing files and updating

301-- | The monad for the main REPL - reading and processing files and updating

301-- global state (hence the IO inner monad).

302-- global state (hence the IO inner monad).

src/Idris/Elab/Clause.hs+2

@@ -554,6 +554,7 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

554 return (Left ptm, lhs)

555elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock)

556 = do let tcgen = Dictionary `elem` opts

557+ push_estack fname

557 ctxt <- getContext

558 ctxt <- getContext

558 let (lhs_in, rhs_in) = desugarAs lhs_in_as rhs_in_as

559 let (lhs_in, rhs_in) = desugarAs lhs_in_as rhs_in_as

559

560

@@ -719,6 +720,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

719 when (rev || ErrorReverse `elem` opts) $ do

720 when (rev || ErrorReverse `elem` opts) $ do

720 addIBC (IBCErrRev (crhs, clhs))

721 addIBC (IBCErrRev (crhs, clhs))

721 addErrRev (crhs, clhs)

722 addErrRev (crhs, clhs)

723+ pop_estack

722 return $ (Right (clhs, crhs), lhs)

724 return $ (Right (clhs, crhs), lhs)

723 where

725 where

724 pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo

726 pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo

src/Idris/ElabTerm.hs+10−8

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

510 g <- goal

511 hs <- get_holes

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

513− -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))

514 then try (resolveTC True 7 g fn ist)

513 then try (resolveTC True 7 g fn ist)

515 (movelast n)

514 (movelast n)

516 else movelast n)

515 else movelast n)

@@ -658,7 +657,6 @@ elab ist info emode opts fn tm

658 env <- get_env

657 env <- get_env

659 hs <- get_holes

658 hs <- get_holes

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

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

661− -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))

662 then try (resolveTC False 7 g fn ist)

660 then try (resolveTC False 7 g fn ist)

663 (movelast n)

661 (movelast n)

664 else movelast n)

662 else movelast n)

@@ -1230,6 +1228,9 @@ proofSearch' ist rec ambigok depth prv top n hints

1230 proofSearch rec prv ambigok (not prv) depth

1228 proofSearch rec prv ambigok (not prv) depth

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

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

1232

1230

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

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

1233+-- name).

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

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

1234resolveTC = resTC' []

1235resolveTC = resTC' []

1235

1236

@@ -1246,12 +1247,13 @@ resTC' tcs defaultOn depth topg fn ist

1246 (do t <- goal

1247 (do t <- goal

1247 let (tc, ttypes) = unApply t

1248 let (tc, ttypes) = unApply t

1248 scopeOnly <- needsDefault t tc ttypes

1249 scopeOnly <- needsDefault t tc ttypes

1250+ let stk = elab_stack ist

1249 let insts_in = findInstances ist t

1251 let insts_in = findInstances ist t

1250 let insts = if scopeOnly then filter chaser insts_in

1252 let insts = if scopeOnly then filter chaser insts_in

1251 else insts_in

1253 else insts_in

1252 tm <- get_term

1254 tm <- get_term

1253 let depth' = if scopeOnly then 2 else depth

1255 let depth' = if scopeOnly then 2 else depth

1254− blunderbuss t depth' insts) True

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

1255 where

1257 where

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

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

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

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

@@ -1278,13 +1280,13 @@ resTC' tcs defaultOn depth topg fn ist

1278 boundVar (P Bound _ _) = True

1280 boundVar (P Bound _ _) = True

1279 boundVar _ = False

1281 boundVar _ = False

1280

1282

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

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

1282 -- ps <- get_probs

1284 -- ps <- get_probs

1283 lift $ tfail $ CantResolve topg

1285 lift $ tfail $ CantResolve topg

1284− blunderbuss t d (n:ns)

1286+ blunderbuss t d stk (n:ns)

1285− | n /= fn && tcname n = try' (resolve n d)

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

1286− (blunderbuss t d ns) True

1288+ = try' (resolve n d) (blunderbuss t d stk ns) True

1287− | otherwise = blunderbuss t d ns

1289+ | otherwise = blunderbuss t d stk ns

1288

1290

1289 resolve n depth

1291 resolve n depth

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

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