fbdd59b · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+4−3

compare with master

unifiedsplit

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

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

344addToCalledG n ns = return () -- TODO

345

346−push_estack :: Name -> Idris ()

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

347+push_estack n inst

347−push_estack n = do i <- getIState

348+ = do i <- getIState

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

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

349

350

350pop_estack :: Idris ()

351pop_estack :: Idris ()

351pop_estack = do i <- getIState

352pop_estack = do i <- getIState

src/Idris/AbsSyntaxTree.hs+2−1

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

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

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

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

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

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

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

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

240 }

241 }

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

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

514 return (Left ptm, lhs)

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

516 = do let tcgen = Dictionary `elem` opts

517− push_estack fname

517+ push_estack fname False

518 ctxt <- getContext

519 let (lhs_in, rhs_in) = desugarAs lhs_in_as rhs_in_as

520

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

140 let idecls = [PClauses fc [Dictionary] iname

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

142 iLOG (show idecls)

143+ push_estack iname True

143 mapM_ (rec_elabDecl info EAll info) idecls

144 mapM_ (rec_elabDecl info EAll info) idecls

145+ pop_estack

144 ist <- getIState

146 ist <- getIState

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

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

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

148 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

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

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

355 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

357 elab' ina fc (PResolveTC fc')

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

359 instanceArg c

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

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

1505 try' (trivialHoles' okholes ist)

1506 (do addDefault t tc ttypes

1507− let stk = elab_stack ist

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

1508 let insts = findInstances ist t

1509− tm <- get_term

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

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

1511 where

1510 where

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

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