ee32989 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Search in current elaboration stack for instances

That is, keep a stack of what is currently being elaborated (parents of where clauses, case blocks, etc) so that the most local type class instance is always chosen when resolving. In particular, this means when defining named instances, the instance being defined is always used rather than the global instance. Fixes #871

commitee32989828090fecf310d4be6f6be49e4b5d5b6c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 1 Jan 2015, 21:51 (12 years ago) parente57170d

4 files changed+25−10

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+10 src/Idris/AbsSyntaxTree.hs+3−2 src/Idris/Elab/Clause.hs+2 src/Idris/ElabTerm.hs+10−8

src/Idris/AbsSyntax.hs+10

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

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

316316addToCalledG n ns = return () -- TODO

317317

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+

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

319329-- list so they are resolved by default.

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

src/Idris/AbsSyntaxTree.hs+3−2

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

214214 idris_postulates :: S.Set Name,

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

216216 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

218219 }

219220

220221-- Required for parsers library, and therefore trifecta

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

295296 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

296297 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

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

298− AutomaticWidth S.empty Nothing Nothing []

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

299300

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

301302-- 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 [])

554554 return (Left ptm, lhs)

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

556556 = do let tcgen = Dictionary `elem` opts

557+ push_estack fname

557558 ctxt <- getContext

558559 let (lhs_in, rhs_in) = desugarAs lhs_in_as rhs_in_as

559560

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

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

720721 addIBC (IBCErrRev (crhs, clhs))

721722 addErrRev (crhs, clhs)

723+ pop_estack

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

723725 where

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

src/Idris/ElabTerm.hs+10−8

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

510510 g <- goal

511511 hs <- get_holes

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

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

514513 then try (resolveTC True 7 g fn ist)

515514 (movelast n)

516515 else movelast n)

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

658657 env <- get_env

659658 hs <- get_holes

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

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

662660 then try (resolveTC False 7 g fn ist)

663661 (movelast n)

664662 else movelast n)

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

12301228 proofSearch rec prv ambigok (not prv) depth

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

12321230

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).

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

12341235resolveTC = resTC' []

12351236

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

12461247 (do t <- goal

12471248 let (tc, ttypes) = unApply t

12481249 scopeOnly <- needsDefault t tc ttypes

1250+ let stk = elab_stack ist

12491251 let insts_in = findInstances ist t

12501252 let insts = if scopeOnly then filter chaser insts_in

12511253 else insts_in

12521254 tm <- get_term

12531255 let depth' = if scopeOnly then 2 else depth

1254− blunderbuss t depth' insts) True

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

12551257 where

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

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

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

12781280 boundVar (P Bound _ _) = True

12791281 boundVar _ = False

12801282

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

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

12821284 -- ps <- get_probs

12831285 lift $ tfail $ CantResolve topg

1284− blunderbuss t d (n:ns)

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

1286− (blunderbuss t d ns) True

1287− | otherwise = blunderbuss t d ns

1286+ blunderbuss t d stk (n:ns)

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

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

1289+ | otherwise = blunderbuss t d stk ns

12881290

12891291 resolve n depth

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