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

git.iko.soy/Idris-dev

Use exact name lookup when building from ibc

commit323a1093986b2389be5023e7a837ac38bb1e4c7f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 13 Sep 2014, 16:35 (12 years ago) parent782c945

4 files changed+41−31

compare with master

unifiedsplit

src/Idris/Core/Evaluate.hs+10−1 src/Idris/Coverage.hs+2−2 src/Idris/Elab/Clause.hs+1−1 src/Idris/IBC.hs+28−27

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

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

88 Context, initContext, ctxtAlist, uconstraints, next_tvar,

99 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

1010 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,

1213 mapDefCtxt,

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

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

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

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

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

979980

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+

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

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

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

src/Idris/Coverage.hs+2−2

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

468468buildSCG (_, n) = do

469469 ist <- getIState

470470 case lookupCtxt n (idris_callgraph ist) of

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

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

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

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

473473 let (args, sc) = cases_totcheck cd in

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

475475 ++ 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)

653653 borrowedB b = borrowedNames env (binderTy b)

654654 borrowedNames _ _ = []

655655

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

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

657657 mkLHSapp t = t

658658

659659 decorate (NS x ns)

src/Idris/IBC.hs+28−27

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

124124

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

126126ibc 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

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

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

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

129129 _ -> ifail "IBC write failed"

130130ibc i (IBCStatic n) f

131− = case lookupCtxt n (idris_statics i) of

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

131+ = case lookupCtxtExact n (idris_statics i) of

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

133133 _ -> ifail "IBC write failed"

134134ibc i (IBCClass n) f

135− = case lookupCtxt n (idris_classes i) of

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

135+ = case lookupCtxtExact n (idris_classes i) of

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

137137 _ -> ifail "IBC write failed"

138138ibc i (IBCInstance int n ins) f

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

140140ibc i (IBCDSL n) f

141− = case lookupCtxt n (idris_dsls i) of

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

141+ = case lookupCtxtExact n (idris_dsls i) of

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

143143 _ -> ifail "IBC write failed"

144144ibc i (IBCData n) f

145− = case lookupCtxt n (idris_datatypes i) of

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

145+ = case lookupCtxtExact n (idris_datatypes i) of

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

147147 _ -> ifail "IBC write failed"

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

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

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

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

150150 _ -> ifail "IBC write failed"

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

152152ibc 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 }

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

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

160160ibc i (IBCDef n) f

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

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

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

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

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

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

164164 _ -> ifail "IBC write failed"

165− case lookupCtxt n (idris_patdefs i) of

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

165+ case lookupCtxtExact n (idris_patdefs i) of

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

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

168168 where

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

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

220220 update t = return t

221221

222222

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

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

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

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

225225 _ -> ifail "IBC write failed"

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

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

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

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

228228 _ -> ifail "IBC write failed"

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

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

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

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

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

338338 do i <- getIState

339− case lookupDefAcc n False (tt_ctxt i) of

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

339+ case lookupDefAccExact n False (tt_ctxt i) of

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

341341 _ -> putIState (i { idris_implicits

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

343343 imps

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

358358 do i <- getIState

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

360360 -- could have loaded in any order

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

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

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

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

363363 _ -> []

364364 let c' = c { class_instances =

365365 class_instances c ++ is }

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

433433 do let d' = updateDef d

434434 case d' of

435435 TyDecl _ _ -> return ()

436− _ -> solveDeferred n

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

437+ solveDeferred n

437438 i <- getIState

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

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

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

440441 where

441442 updateDef (CaseOp c t args o s cd)