fbdd59b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Mark instances on elaboration stack

Otherwise we search a lot of non-instance things when resolving instances. Fixes #2296

commitfbdd59bbabe47bde2c784559e2f22ddba6275819 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 19 May 2015, 11:11 (11 years ago) parent2c609ae

5 files changed+11−8

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+4−3 src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/Elab/Clause.hs+1−1 src/Idris/Elab/Instance.hs+2 src/Idris/Elab/Term.hs+2−3

src/Idris/AbsSyntax.hs+4−3

@@ -343,9 +343,10 @@ getNameHints i n =

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

344344addToCalledG n ns = return () -- TODO

345345

346−push_estack :: Name -> Idris ()

347−push_estack n = do i <- getIState

348− putIState (i { elab_stack = n : elab_stack i })

346+push_estack :: Name -> Bool -> Idris ()

347+push_estack n inst

348+ = do i <- getIState

349+ putIState (i { elab_stack = (n, inst) : elab_stack i })

349350

350351pop_estack :: Idris ()

351352pop_estack = do i <- getIState

src/Idris/AbsSyntaxTree.hs+2−1

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

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

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

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

237− elab_stack :: [Name], -- ^ Stack of names currently being elaborated

237+ elab_stack :: [(Name, Bool)], -- ^ Stack of names currently being elaborated, Bool set if it's an instance

238+ -- (instances appear twice; also as a funtion name)

238239 idris_symbols :: M.Map Name Name, -- ^ Symbol table (preserves sharing of names)

239240 idris_exports :: [Name] -- ^ Functions with ExportList

240241 }

src/Idris/Elab/Clause.hs+1−1

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

514514 return (Left ptm, lhs)

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

516516 = do let tcgen = Dictionary `elem` opts

517− push_estack fname

517+ push_estack fname False

518518 ctxt <- getContext

519519 let (lhs_in, rhs_in) = desugarAs lhs_in_as rhs_in_as

520520

src/Idris/Elab/Instance.hs+2

@@ -140,7 +140,9 @@ elabInstance info syn doc argDocs what fc cs n nfc ps t expn ds = do

140140 let idecls = [PClauses fc [Dictionary] iname

141141 [PClause fc iname lhs [] rhs wb]]

142142 iLOG (show idecls)

143+ push_estack iname True

143144 mapM_ (rec_elabDecl info EAll info) idecls

145+ pop_estack

144146 ist <- getIState

145147 checkInjectiveArgs fc n (class_determiners ci) (lookupTyExact iname (tt_ctxt ist))

146148 addIBC (IBCInstance intInst (isNothing expn) n iname)

src/Idris/Elab/Term.hs+2−3

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

353353 UType _ -> elab' ina (Just fc) (PRef fc unitTy)

354354 _ -> elab' ina (Just fc) (PRef fc unitCon)

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

356− = do g <- goal; resolveTC False False 10 g fn ist

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

357357 elab' ina fc (PResolveTC fc')

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

359359 instanceArg c

@@ -1504,9 +1504,8 @@ resTC' tcs defaultOn topholes depth topg fn ist

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

15051505 try' (trivialHoles' okholes ist)

15061506 (do addDefault t tc ttypes

1507− let stk = elab_stack ist

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

15081508 let insts = findInstances ist t

1509− tm <- get_term

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

15111510 where

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