323a109 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Use exact name lookup when building from ibc

323a109Edwin Brady12 years ago

src/Idris/Core/Evaluate.hs+10−1

compare with master

unifiedsplit

@@ -8,7 +8,8 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

8 Context, initContext, ctxtAlist, uconstraints, next_tvar,

9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

10 addDatatype, addCasedef, simplifyCasedef, addOperator,

11− lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,

11+ lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

12+ lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

12 mapDefCtxt,

13 mapDefCtxt,

13 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

14 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

14 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

15 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

@@ -977,6 +978,14 @@ lookupDefAcc n mkpublic ctxt

977 where mkp (d, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))

978 where mkp (d, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))

978 then (d, Public) else (d, a)

979 then (d, Public) else (d, a)

979

980

981+lookupDefAccExact :: Name -> Bool -> Context ->

982+ Maybe (Def, Accessibility)

983+lookupDefAccExact n mkpublic ctxt

984+ = fmap mkp $ lookupCtxtExact n (definitions ctxt)

985+ -- io_bind a special case for REPL prettiness

986+ where mkp (d, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))

987+ then (d, Public) else (d, a)

988+

980lookupTotal :: Name -> Context -> [Totality]

989lookupTotal :: Name -> Context -> [Totality]

981lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)

990lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)

982 where mkt (d, a, t, m) = t

991 where mkt (d, a, t, m) = t

src/Idris/Coverage.hs+2−2

@@ -468,8 +468,8 @@ buildSCG :: (FC, Name) -> Idris ()

468buildSCG (_, n) = do

469 ist <- getIState

470 case lookupCtxt n (idris_callgraph ist) of

471− [cg] -> case lookupDef n (tt_ctxt ist) of

471+ [cg] -> case lookupDefExact n (tt_ctxt ist) of

472− [CaseOp _ _ _ pats _ cd] ->

472+ Just (CaseOp _ _ _ pats _ cd) ->

473 let (args, sc) = cases_totcheck cd in

474 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"

475 ++ show pats ++ "\n" ++ show sc

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

@@ -653,7 +653,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

653 borrowedB b = borrowedNames env (binderTy b)

654 borrowedNames _ _ = []

655

656− mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []

656+ mkLHSapp t@(PRef _ _) = PApp fc t []

657 mkLHSapp t = t

658

659 decorate (NS x ns)

src/Idris/IBC.hs+28−27

@@ -124,29 +124,29 @@ mkIBC (i:is) f = do ist <- getIState

124

125ibc :: IState -> IBCWrite -> IBCFile -> Idris IBCFile

126ibc i (IBCFix d) f = return f { ibc_fixes = d : ibc_fixes f }

127−ibc i (IBCImp n) f = case lookupCtxt n (idris_implicits i) of

127+ibc i (IBCImp n) f = case lookupCtxtExact n (idris_implicits i) of

128− [v] -> return f { ibc_implicits = (n,v): ibc_implicits f }

128+ Just v -> return f { ibc_implicits = (n,v): ibc_implicits f }

129 _ -> ifail "IBC write failed"

130ibc i (IBCStatic n) f

131− = case lookupCtxt n (idris_statics i) of

131+ = case lookupCtxtExact n (idris_statics i) of

132− [v] -> return f { ibc_statics = (n,v): ibc_statics f }

132+ Just v -> return f { ibc_statics = (n,v): ibc_statics f }

133 _ -> ifail "IBC write failed"

134ibc i (IBCClass n) f

135− = case lookupCtxt n (idris_classes i) of

135+ = case lookupCtxtExact n (idris_classes i) of

136− [v] -> return f { ibc_classes = (n,v): ibc_classes f }

136+ Just v -> return f { ibc_classes = (n,v): ibc_classes f }

137 _ -> ifail "IBC write failed"

138ibc i (IBCInstance int n ins) f

139 = return f { ibc_instances = (int,n,ins): ibc_instances f }

140ibc i (IBCDSL n) f

141− = case lookupCtxt n (idris_dsls i) of

141+ = case lookupCtxtExact n (idris_dsls i) of

142− [v] -> return f { ibc_dsls = (n,v): ibc_dsls f }

142+ Just v -> return f { ibc_dsls = (n,v): ibc_dsls f }

143 _ -> ifail "IBC write failed"

144ibc i (IBCData n) f

145− = case lookupCtxt n (idris_datatypes i) of

145+ = case lookupCtxtExact n (idris_datatypes i) of

146− [v] -> return f { ibc_datatypes = (n,v): ibc_datatypes f }

146+ Just v -> return f { ibc_datatypes = (n,v): ibc_datatypes f }

147 _ -> ifail "IBC write failed"

148−ibc i (IBCOpt n) f = case lookupCtxt n (idris_optimisation i) of

148+ibc i (IBCOpt n) f = case lookupCtxtExact n (idris_optimisation i) of

149− [v] -> return f { ibc_optimise = (n,v): ibc_optimise f }

149+ Just v -> return f { ibc_optimise = (n,v): ibc_optimise f }

150 _ -> ifail "IBC write failed"

151ibc i (IBCSyntax n) f = return f { ibc_syntax = n : ibc_syntax f }

152ibc i (IBCKeyword n) f = return f { ibc_keywords = n : ibc_keywords f }

@@ -158,12 +158,12 @@ ibc i (IBCCGFlag tgt n) f = return f { ibc_cgflags = (tgt, n) : ibc_cgflags f }

158ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }

159ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }

160ibc i (IBCDef n) f

161− = do f' <- case lookupDef n (tt_ctxt i) of

161+ = do f' <- case lookupDefExact n (tt_ctxt i) of

162− [v] -> do (v', (f', _)) <- runStateT (updateDef v) (f, length (symbols f))

162+ Just v -> do (v', (f', _)) <- runStateT (updateDef v) (f, length (symbols f))

163− return f' { ibc_defs = (n,v) : ibc_defs f' }

163+ return f' { ibc_defs = (n,v) : ibc_defs f' }

164 _ -> ifail "IBC write failed"

165− case lookupCtxt n (idris_patdefs i) of

165+ case lookupCtxtExact n (idris_patdefs i) of

166− [v] -> return f' { ibc_patdefs = (n,v) : ibc_patdefs f' }

166+ Just v -> return f' { ibc_patdefs = (n,v) : ibc_patdefs f' }

167 _ -> return f' -- Not a pattern definition

168 where

169 updateDef :: Def -> StateT (IBCFile, Int) Idris Def

@@ -220,11 +220,11 @@ ibc i (IBCDef n) f

220 update t = return t

221

222

223−ibc i (IBCDoc n) f = case lookupCtxt n (idris_docstrings i) of

223+ibc i (IBCDoc n) f = case lookupCtxtExact n (idris_docstrings i) of

224− [v] -> return f { ibc_docstrings = (n,v) : ibc_docstrings f }

224+ Just v -> return f { ibc_docstrings = (n,v) : ibc_docstrings f }

225 _ -> ifail "IBC write failed"

226−ibc i (IBCCG n) f = case lookupCtxt n (idris_callgraph i) of

226+ibc i (IBCCG n) f = case lookupCtxtExact n (idris_callgraph i) of

227− [v] -> return f { ibc_cg = (n,v) : ibc_cg f }

227+ Just v -> return f { ibc_cg = (n,v) : ibc_cg f }

228 _ -> ifail "IBC write failed"

229ibc i (IBCCoercion n) f = return f { ibc_coercions = n : ibc_coercions f }

230ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

@@ -336,8 +336,8 @@ pImports fs

336pImps :: [(Name, [PArg])] -> Idris ()

337pImps imps = mapM_ (\ (n, imp) ->

338 do i <- getIState

339− case lookupDefAcc n False (tt_ctxt i) of

339+ case lookupDefAccExact n False (tt_ctxt i) of

340− [(n, Hidden)] -> return ()

340+ Just (n, Hidden) -> return ()

341 _ -> putIState (i { idris_implicits

342 = addDef n imp (idris_implicits i) }))

343 imps

@@ -358,8 +358,8 @@ pClasses cs = mapM_ (\ (n, c) ->

358 do i <- getIState

359 -- Don't lose instances from previous IBCs, which

360 -- could have loaded in any order

361− let is = case lookupCtxt n (idris_classes i) of

361+ let is = case lookupCtxtExact n (idris_classes i) of

362− [CI _ _ _ _ _ ins] -> ins

362+ Just (CI _ _ _ _ _ ins) -> ins

363 _ -> []

364 let c' = c { class_instances =

365 class_instances c ++ is }

@@ -433,9 +433,10 @@ pDefs syms ds

433 do let d' = updateDef d

434 case d' of

435 TyDecl _ _ -> return ()

436+ _ -> do iLOG $ "SOLVING " ++ show n

436− _ -> solveDeferred n

437+ solveDeferred n

437 i <- getIState

438 i <- getIState

438− logLvl 5 $ "Added " ++ show (n, d')

439+-- logLvl 1 $ "Added " ++ show (n, d')

439 putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) ds

440 putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) ds

440 where

441 where

441 updateDef (CaseOp c t args o s cd)

442 updateDef (CaseOp c t args o s cd)