200475f · Idris-dev · git.iko.soy

src/Core/Elaborate.hs+3−3

@@ -171,7 +171,7 @@ checkInjective (tm, l, r) = do ctxt <- get_context

171171 if isInj ctxt tm then return ()

172172 else lift $ tfail (NotInjective tm l r)

173173 where isInj ctxt (P _ n _)

174− | isConName Nothing n ctxt = True

174+ | isConName n ctxt = True

175175 isInj ctxt (App f a) = isInj ctxt f

176176 isInj ctxt (Constant _) = True

177177 isInj ctxt (TType _) = True

@@ -210,7 +210,7 @@ unique_hole' reusable n

210210uniqueNameCtxt :: Context -> Name -> [Name] -> Elab' aux Name

211211uniqueNameCtxt ctxt n hs

212212 | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs

213− | [_] <- lookupTy Nothing n ctxt = uniqueNameCtxt ctxt (nextName n) hs

213+ | [_] <- lookupTy n ctxt = uniqueNameCtxt ctxt (nextName n) hs

214214 | otherwise = return n

215215

216216elog :: String -> Elab' aux ()

@@ -356,7 +356,7 @@ prepare_apply fn imps =

356356 mkClaims _ _ _ _

357357 | Var n <- fn

358358 = do ctxt <- get_context

359− case lookupTy Nothing n ctxt of

359+ case lookupTy n ctxt of

360360 [] -> lift $ tfail $ NoSuchVariable n

361361 _ -> fail $ "Too many arguments for " ++ show fn

362362 | otherwise = fail $ "Too many arguments for " ++ show fn

src/Core/Evaluate.hs+32−32

@@ -149,7 +149,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

149149 ev ntimes_in stk top env (P Ref n ty)

150150 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)

151151 | (True, ntimes) <- usable simpl n ntimes_in

152− = do let val = lookupDefAcc Nothing n atRepl ctxt

152+ = do let val = lookupDefAcc n atRepl ctxt

153153 case val of

154154 [(Function _ tm, Public)] ->

155155 ev ntimes (n:stk) True env tm

@@ -220,7 +220,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

220220 _ -> return $ unload env f args

221221 | (True, ntimes) <- usable simpl n ntimes_in

222222 = traceWhen traceon (show stk) $

223− do let val = lookupDefAcc Nothing n atRepl ctxt

223+ do let val = lookupDefAcc n atRepl ctxt

224224 case val of

225225 [(CaseOp inl inr _ _ _ ns tree _ _, acc)]

226226 | acc == Public -> -- unoptimised version

@@ -243,7 +243,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

243243 apply ntimes stk top env f [] = return f

244244

245245-- specApply stk env f@(VP Ref n ty) args

246−-- = case lookupCtxt Nothing n statics of

246+-- = case lookupCtxt n statics of

247247-- [as] -> if or as

248248-- then trace (show (n, map fst (filter (\ (_, s) -> s) (zip args as)))) $

249249-- return $ unload env f args

@@ -397,7 +397,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

397397 ev :: [HNF] -> TT Name -> Eval HNF

398398 ev env (P _ n ty)

399399 | Just (Let t v) <- lookup n genv = ev env v

400− ev env (P Ref n ty) = case lookupDef Nothing n ctxt of

400+ ev env (P Ref n ty) = case lookupDef n ctxt of

401401 [Function _ t] -> ev env t

402402 [TyDecl nt ty] -> return $ HP nt n ty

403403 [CaseOp inl _ _ _ _ [] tree _ _] ->

@@ -430,7 +430,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

430430 app <- apply env sc' as

431431 wknH (-1) app

432432 apply env (HP Ref n ty) args

433− | [CaseOp _ _ _ _ _ ns tree _ _] <- lookupDef Nothing n ctxt

433+ | [CaseOp _ _ _ _ _ ns tree _ _] <- lookupDef n ctxt

434434 = do c <- evCase env ns args tree

435435 case c of

436436 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args

@@ -565,7 +565,7 @@ convEq ctxt = ceq [] where

565565 caseeq ps (UnmatchedCase _) (UnmatchedCase _) = return True

566566 caseeq ps _ _ = return False

567567

568− sameDefs ps x y = case (lookupDef Nothing x ctxt, lookupDef Nothing y ctxt) of

568+ sameDefs ps x y = case (lookupDef x ctxt, lookupDef y ctxt) of

569569 ([Function _ xdef], [Function _ ydef])

570570 -> ceq ((x,y):ps) xdef ydef

571571 ([CaseOp _ _ _ _ _ _ xdef _ _],

@@ -730,7 +730,7 @@ addCasedef :: Name -> Bool -> Bool -> Bool -> Bool ->

730730 Type -> Context -> Context

731731addCasedef n alwaysInline tcase covering asserted ps_in ps psrt ty uctxt

732732 = let ctxt = definitions uctxt

733− access = case lookupDefAcc Nothing n False uctxt of

733+ access = case lookupDefAcc n False uctxt of

734734 [(_, acc)] -> acc

735735 _ -> Public

736736 ctxt' = case (simpleCase tcase covering CompileTime (FC "" 0) ps,

@@ -747,7 +747,7 @@ addCasedef n alwaysInline tcase covering asserted ps_in ps psrt ty uctxt

747747simplifyCasedef :: Name -> Context -> Context

748748simplifyCasedef n uctxt

749749 = let ctxt = definitions uctxt

750− ctxt' = case lookupCtxt Nothing n ctxt of

750+ ctxt' = case lookupCtxt n ctxt of

751751 [(CaseOp inl inr ty [] ps args sc args' sc', acc, tot)] ->

752752 ctxt -- nothing to simplify (or already done...)

753753 [(CaseOp inl inr ty ps_in ps args sc args' sc', acc, tot)] ->

@@ -780,40 +780,40 @@ addOperator n ty a op uctxt

780780

781781tfst (a, _, _) = a

782782

783−lookupNames :: Maybe [String] -> Name -> Context -> [Name]

784−lookupNames root n ctxt

785− = let ns = lookupCtxtName root n (definitions ctxt) in

783+lookupNames :: Name -> Context -> [Name]

784+lookupNames n ctxt

785+ = let ns = lookupCtxtName n (definitions ctxt) in

786786 map fst ns

787787

788−lookupTy :: Maybe [String] -> Name -> Context -> [Type]

789−lookupTy root n ctxt

790− = do def <- lookupCtxt root n (definitions ctxt)

788+lookupTy :: Name -> Context -> [Type]

789+lookupTy n ctxt

790+ = do def <- lookupCtxt n (definitions ctxt)

791791 case tfst def of

792792 (Function ty _) -> return ty

793793 (TyDecl _ ty) -> return ty

794794 (Operator ty _ _) -> return ty

795795 (CaseOp _ _ ty _ _ _ _ _ _) -> return ty

796796

797−isConName :: Maybe [String] -> Name -> Context -> Bool

798−isConName root n ctxt

799− = or $ do def <- lookupCtxt root n (definitions ctxt)

797+isConName :: Name -> Context -> Bool

798+isConName n ctxt

799+ = or $ do def <- lookupCtxt n (definitions ctxt)

800800 case tfst def of

801801 (TyDecl (DCon _ _) _) -> return True

802802 (TyDecl (TCon _ _) _) -> return True

803803 _ -> return False

804804

805−isFnName :: Maybe [String] -> Name -> Context -> Bool

806−isFnName root n ctxt

807− = or $ do def <- lookupCtxt root n (definitions ctxt)

805+isFnName :: Name -> Context -> Bool

806+isFnName n ctxt

807+ = or $ do def <- lookupCtxt n (definitions ctxt)

808808 case tfst def of

809809 (Function _ _) -> return True

810810 (Operator _ _ _) -> return True

811811 (CaseOp _ _ _ _ _ _ _ _ _) -> return True

812812 _ -> return False

813813

814−lookupP :: Maybe [String] -> Name -> Context -> [Term]

815−lookupP root n ctxt

816− = do def <- lookupCtxt root n (definitions ctxt)

814+lookupP :: Name -> Context -> [Term]

815+lookupP n ctxt

816+ = do def <- lookupCtxt n (definitions ctxt)

817817 p <- case def of

818818 (Function ty tm, a, _) -> return (P Ref n ty, a)

819819 (TyDecl nt ty, a, _) -> return (P nt n ty, a)

@@ -823,22 +823,22 @@ lookupP root n ctxt

823823 Hidden -> []

824824 _ -> return (fst p)

825825

826−lookupDef :: Maybe [String] -> Name -> Context -> [Def]

827−lookupDef root n ctxt = map tfst $ lookupCtxt root n (definitions ctxt)

826+lookupDef :: Name -> Context -> [Def]

827+lookupDef n ctxt = map tfst $ lookupCtxt n (definitions ctxt)

828828

829−lookupDefAcc :: Maybe [String] -> Name -> Bool -> Context ->

829+lookupDefAcc :: Name -> Bool -> Context ->

830830 [(Def, Accessibility)]

831−lookupDefAcc root n mkpublic ctxt

832− = map mkp $ lookupCtxt root n (definitions ctxt)

831+lookupDefAcc n mkpublic ctxt

832+ = map mkp $ lookupCtxt n (definitions ctxt)

833833 where mkp (d, a, _) = if mkpublic then (d, Public) else (d, a)

834834

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

836−lookupTotal n ctxt = map mkt $ lookupCtxt Nothing n (definitions ctxt)

836+lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)

837837 where mkt (d, a, t) = t

838838

839−lookupVal :: Maybe [String] -> Name -> Context -> [Value]

840−lookupVal root n ctxt

841− = do def <- lookupCtxt root n (definitions ctxt)

839+lookupVal :: Name -> Context -> [Value]

840+lookupVal n ctxt

841+ = do def <- lookupCtxt n (definitions ctxt)

842842 case tfst def of

843843 (Function _ htm) -> return (veval ctxt [] htm)

844844 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))

src/Core/ProofShell.hs+1−1

@@ -41,7 +41,7 @@ processCommand (Eval t) state =

4141 (state, show nf ++ " : " ++ show ty)

4242 err -> (state, show err)

4343processCommand (Print n) state =

44− case lookupDef Nothing n (ctxt state) of

44+ case lookupDef n (ctxt state) of

4545 [tm] -> (state, show tm)

4646 _ -> (state, "No such name")

4747processCommand (Tac e) state

src/Core/TT.hs+5−5

@@ -244,8 +244,8 @@ addDef n v ctxt = case Map.lookup (nsroot n) ctxt of

244244

245245-}

246246

247−lookupCtxtName :: Maybe [String] -> Name -> Ctxt a -> [(Name, a)]

248−lookupCtxtName nspace n ctxt = case Map.lookup (nsroot n) ctxt of

247+lookupCtxtName :: Name -> Ctxt a -> [(Name, a)]

248+lookupCtxtName n ctxt = case Map.lookup (nsroot n) ctxt of

249249 Just xs -> filterNS (Map.toList xs)

250250 Nothing -> []

251251 where

@@ -258,12 +258,12 @@ lookupCtxtName nspace n ctxt = case Map.lookup (nsroot n) ctxt of

258258 nsmatch (NS _ _) _ = False

259259 nsmatch looking found = True

260260

261−lookupCtxt :: Maybe [String] -> Name -> Ctxt a -> [a]

262−lookupCtxt ns n ctxt = map snd (lookupCtxtName ns n ctxt)

261+lookupCtxt :: Name -> Ctxt a -> [a]

262+lookupCtxt n ctxt = map snd (lookupCtxtName n ctxt)

263263

264264updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a

265265updateDef n f ctxt

266− = let ds = lookupCtxtName Nothing n ctxt in

266+ = let ds = lookupCtxtName n ctxt in

267267 foldr (\ (n, t) c -> addDef n (f t) c) ctxt ds

268268

269269toAlist :: Ctxt a -> [(Name, a)]

src/Core/Typecheck.hs+1−1

@@ -60,7 +60,7 @@ check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)

6060check' holes ctxt env top = chk env top where

6161 chk env (Var n)

6262 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

63− | (P nt n' ty : _) <- lookupP Nothing n ctxt = return (P nt n' ty, ty)

63+ | (P nt n' ty : _) <- lookupP n ctxt = return (P nt n' ty, ty)

6464 | otherwise = do lift $ tfail $ NoSuchVariable n

6565 chk env (RApp f a)

6666 = do (fv, fty) <- chk env f

src/IRTS/Compiler.hs+3−3

@@ -98,7 +98,7 @@ irMain tm = do i <- ir tm

9898allNames :: [Name] -> Name -> Idris [Name]

9999allNames ns n | n `elem` ns = return []

100100allNames ns n = do i <- getIState

101− case lookupCtxt Nothing n (idris_callgraph i) of

101+ case lookupCtxt n (idris_callgraph i) of

102102 [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))

103103 return (nub (n : concat more))

104104 _ -> return [n]

@@ -205,12 +205,12 @@ instance ToIR (TT Name) where

205205 Just tm -> return tm

206206 _ -> do

207207 let collapse

208− = case lookupCtxt Nothing n

208+ = case lookupCtxt n

209209 (idris_optimisation i) of

210210 [oi] -> collapsible oi

211211 _ -> False

212212 let unused

213− = case lookupCtxt Nothing n

213+ = case lookupCtxt n

214214 (idris_callgraph i) of

215215 [CGInfo _ _ _ _ unusedpos] ->

216216 unusedpos

src/IRTS/Defunctionalise.hs+2−2

@@ -80,14 +80,14 @@ addApps defs (n, LFun _ _ args e)

8080-- aa env e@(LApp tc (MN 0 "EVAL") [a]) = e

8181 aa env (LApp tc (LV (Glob n)) args)

8282 = do args' <- mapM (aa env) args

83− case lookupCtxt Nothing n defs of

83+ case lookupCtxt n defs of

8484 [LConstructor _ i ar] -> return $ DApp tc n args'

8585 [LFun _ _ as _] -> let arity = length as in

8686 fixApply tc n args' arity

8787 [] -> return $ chainAPPLY (DV (Glob n)) args'

8888 aa env (LLazyApp n args)

8989 = do args' <- mapM (aa env) args

90− case lookupCtxt Nothing n defs of

90+ case lookupCtxt n defs of

9191 [LConstructor _ i ar] -> return $ DApp False n args'

9292 [LFun _ _ as _] -> let arity = length as in

9393 fixLazyApply n args' arity

src/IRTS/Simplified.hs+7−7

@@ -46,7 +46,7 @@ simplify :: Bool -> DExp -> State (DDefs, Int) SExp

4646simplify tl (DV (Loc i)) = return (SV (Loc i))

4747simplify tl (DV (Glob x))

4848 = do ctxt <- ldefs

49− case lookupCtxt Nothing x ctxt of

49+ case lookupCtxt x ctxt of

5050 [DConstructor _ t 0] -> return $ SCon t x []

5151 _ -> return $ SV (Glob x)

5252simplify tl (DApp tc n args) = do args' <- mapM sVar args

@@ -88,7 +88,7 @@ simplify tl (DError str) = return $ SError str

8888

8989sVar (DV (Glob x))

9090 = do ctxt <- ldefs

91− case lookupCtxt Nothing x ctxt of

91+ case lookupCtxt x ctxt of

9292 [DConstructor _ t 0] -> sVar (DC t x [])

9393 _ -> return (Glob x, Nothing)

9494sVar (DV x) = return (x, Nothing)

@@ -136,7 +136,7 @@ scopecheck ctxt envTop tm = sc envTop tm where

136136 sc env (SV (Glob n)) =

137137 case lookup n (reverse env) of -- most recent first

138138 Just i -> do lvar i; return (SV (Loc i))

139− Nothing -> case lookupCtxt Nothing n ctxt of

139+ Nothing -> case lookupCtxt n ctxt of

140140 [DConstructor _ i ar] ->

141141 if True -- ar == 0

142142 then return (SCon i n [])

@@ -146,7 +146,7 @@ scopecheck ctxt envTop tm = sc envTop tm where

146146 [] -> fail $ "Codegen error: No such variable " ++ show n

147147 sc env (SApp tc f args)

148148 = do args' <- mapM (scVar env) args

149− case lookupCtxt Nothing f ctxt of

149+ case lookupCtxt f ctxt of

150150 [DConstructor n tag ar] ->

151151 if True -- (ar == length args)

152152 then return $ SCon tag n args'

@@ -160,7 +160,7 @@ scopecheck ctxt envTop tm = sc envTop tm where

160160 return $ SForeign l ty f args'

161161 sc env (SCon tag f args)

162162 = do args' <- mapM (scVar env) args

163− case lookupCtxt Nothing f ctxt of

163+ case lookupCtxt f ctxt of

164164 [DConstructor n tag ar] ->

165165 if True -- (ar == length args)

166166 then return $ SCon tag n args'

@@ -197,7 +197,7 @@ scopecheck ctxt envTop tm = sc envTop tm where

197197 scVar env (Glob n) =

198198 case lookup n (reverse env) of -- most recent first

199199 Just i -> do lvar i; return (Loc i)

200− Nothing -> case lookupCtxt Nothing n ctxt of

200+ Nothing -> case lookupCtxt n ctxt of

201201 [DConstructor _ i ar] ->

202202 fail $ "Codegen error : can't pass constructor here"

203203 [_] -> return (Glob n)

@@ -207,7 +207,7 @@ scopecheck ctxt envTop tm = sc envTop tm where

207207

208208 scalt env (SConCase _ i n args e)

209209 = do let env' = env ++ zip args [length env..]

210− tag <- case lookupCtxt Nothing n ctxt of

210+ tag <- case lookupCtxt n ctxt of

211211 [DConstructor _ i ar] ->

212212 if True -- (length args == ar)

213213 then return i

src/Idris/AbsSyntax.hs+12−12

@@ -88,7 +88,7 @@ getCoercionsTo i ty =

8888 findCoercions fn cs

8989 where findCoercions t [] = []

9090 findCoercions t (n : ns) =

91− let ps = case lookupTy Nothing n (tt_ctxt i) of

91+ let ps = case lookupTy n (tt_ctxt i) of

9292 [ty] -> case unApply (getRetTy ty) of

9393 (t', _) ->

9494 if t == t' then [n] else []

@@ -119,7 +119,7 @@ addToCalledG n ns = return () -- TODO

119119addInstance :: Bool -> Name -> Name -> Idris ()

120120addInstance int n i

121121 = do ist <- getIState

122− case lookupCtxt Nothing n (idris_classes ist) of

122+ case lookupCtxt n (idris_classes ist) of

123123 [CI a b c d ins] ->

124124 do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)

125125 putIState $ ist { idris_classes = cs }

@@ -139,7 +139,7 @@ addInstance int n i

139139addClass :: Name -> ClassInfo -> Idris ()

140140addClass n i

141141 = do ist <- getIState

142− let i' = case lookupCtxt Nothing n (idris_classes ist) of

142+ let i' = case lookupCtxt n (idris_classes ist) of

143143 [c] -> c { class_instances = class_instances i }

144144 _ -> i

145145 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }

@@ -193,7 +193,7 @@ getName = do i <- getIState;

193193checkUndefined :: FC -> Name -> Idris ()

194194checkUndefined fc n

195195 = do i <- getContext

196− case lookupTy Nothing n i of

196+ case lookupTy n i of

197197 (_:_) -> fail $ show fc ++ ":" ++

198198 show n ++ " already defined"

199199 _ -> return ()

@@ -201,7 +201,7 @@ checkUndefined fc n

201201isUndefined :: FC -> Name -> Idris Bool

202202isUndefined fc n

203203 = do i <- getContext

204− case lookupTy Nothing n i of

204+ case lookupTy n i of

205205 (_:_) -> return False

206206 _ -> return True

207207

@@ -641,7 +641,7 @@ getPriority :: IState -> PTerm -> Int

641641getPriority i tm = 1 -- pri tm

642642 where

643643 pri (PRef _ n) =

644− case lookupP Nothing n (tt_ctxt i) of

644+ case lookupP n (tt_ctxt i) of

645645 ((P (DCon _ _) _ _):_) -> 1

646646 ((P (TCon _ _) _ _):_) -> 1

647647 ((P Ref _ _):_) -> 1

@@ -882,9 +882,9 @@ addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm

882882

883883aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm

884884aiFn inpat True ist fc f []

885− = case lookupDef Nothing f (tt_ctxt ist) of

885+ = case lookupDef f (tt_ctxt ist) of

886886 [] -> Right $ PPatvar fc f

887− alts -> let ialts = lookupCtxt Nothing f (idris_implicits ist) in

887+ alts -> let ialts = lookupCtxt f (idris_implicits ist) in

888888 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $

889889 if (not (vname f) || tcname f

890890 || any constructor alts || any allImp ialts)

@@ -904,7 +904,7 @@ aiFn inpat expat ist fc f as

904904 | f `elem` primNames = Right $ PApp fc (PRef fc f) as

905905aiFn inpat expat ist fc f as

906906 -- This is where namespaces get resolved by adding PAlternative

907− = case lookupCtxtName Nothing f (idris_implicits ist) of

907+ = case lookupCtxtName f (idris_implicits ist) of

908908 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

909909 [] -> if f `elem` idris_metavars ist

910910 then Right $ PApp fc (PRef fc f) as

@@ -949,7 +949,7 @@ stripLinear :: IState -> PTerm -> PTerm

949949stripLinear i tm = evalState (sl tm) [] where

950950 sl :: PTerm -> State [Name] PTerm

951951 sl (PRef fc f)

952− | (_:_) <- lookupTy Nothing f (tt_ctxt i)

952+ | (_:_) <- lookupTy f (tt_ctxt i)

953953 = return $ PRef fc f

954954 | otherwise = do ns <- get

955955 if (f `elem` ns)

@@ -1077,11 +1077,11 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

10771077 match (PApp _ x []) (PRef f n) = match x (PRef f n)

10781078 match (PRef _ n) tm@(PRef _ n')

10791079 | n == n' && not names &&

1080− (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)

1080+ (not (isConName n (tt_ctxt i)) || tm == Placeholder)

10811081 = return [(n, tm)]

10821082 | n == n' = return []

10831083 match (PRef _ n) tm

1084− | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)

1084+ | not names && (not (isConName n (tt_ctxt i)) || tm == Placeholder)

10851085 = return [(n, tm)]

10861086 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'

10871087 mr <- match' r r'

src/Idris/AbsSyntaxTree.hs+2−2

@@ -1128,7 +1128,7 @@ namesIn uvars ist tm = nub $ ni [] tm

11281128 where

11291129 ni env (PRef _ n)

11301130 | not (n `elem` env)

1131− = case lookupTy Nothing n (tt_ctxt ist) of

1131+ = case lookupTy n (tt_ctxt ist) of

11321132 [] -> [n]

11331133 _ -> if n `elem` (map fst uvars) then [n] else []

11341134 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

@@ -1152,7 +1152,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm

11521152 where

11531153 ni env (PRef _ n)

11541154 | n `elem` vars && not (n `elem` env)

1155− = case lookupTy Nothing n (tt_ctxt ist) of

1155+ = case lookupTy n (tt_ctxt ist) of

11561156 [] -> [n]

11571157 _ -> []

11581158 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

src/Idris/Coverage.hs+25−25

@@ -38,7 +38,7 @@ mkPatTm t = do i <- getIState

3838 evalStateT (toTT timp) 0

3939 where

4040 toTT (PRef _ n) = do i <- lift getIState

41− case lookupDef Nothing n (tt_ctxt i) of

41+ case lookupDef n (tt_ctxt i) of

4242 [TyDecl nt _] -> return $ P nt n Erased

4343 _ -> return $ P Ref n Erased

4444 toTT (PApp _ t args) = do t' <- toTT t

@@ -107,9 +107,9 @@ expandAlts :: IState -> [CaseAlt] -> SC -> Idris [CaseAlt]

107107expandAlts i all@(ConstCase c _ : alts) def

108108 = return $ all ++ [DefaultCase def]

109109expandAlts i all@(ConCase n _ _ _ : alts) def

110− | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)

110+ | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)

111111 = do let tyn = getTy n (tt_ctxt i)

112− case lookupCtxt Nothing tyn (idris_datatypes i) of

112+ case lookupCtxt tyn (idris_datatypes i) of

113113 (TI ns _ _: _) -> do let ps = map mkPat ns

114114 return $ addAlts ps (altsFor all) all

115115 _ -> return all

@@ -127,13 +127,13 @@ expandAlts i all@(ConCase n _ _ _ : alts) def

127127 argList i = take i (map (\x -> (MN x "ign")) [0..])

128128

129129 getTy n ctxt

130− = case lookupTy Nothing n ctxt of

130+ = case lookupTy n ctxt of

131131 (t : _) -> case unApply (getRetTy t) of

132132 (P _ tyn _, _) -> tyn

133133 x -> error $ "Can't happen getTy 1 " ++ show (n, x)

134134 _ -> error "Can't happen getTy 2"

135135

136− mkPat x = case lookupCtxt Nothing x (idris_implicits i) of

136+ mkPat x = case lookupCtxt x (idris_implicits i) of

137137 (pargs : _)

138138 -> (x, length pargs)

139139 _ -> error "Can't happen - genAll"

@@ -160,7 +160,7 @@ genClauses fc n xs given

160160 logLvl 10 $ show argss ++ "\n" ++ show all_args

161161 logLvl 10 $ "Original: \n" ++

162162 showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)

163− let parg = case lookupCtxt Nothing n (idris_implicits i) of

163+ let parg = case lookupCtxt n (idris_implicits i) of

164164 (p : _) -> p

165165 _ -> repeat (pexp Placeholder)

166166 let tryclauses = mkClauses parg all_args

@@ -217,8 +217,8 @@ genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of

217217 [] -> [Placeholder]

218218 xs -> nub xs

219219 where

220− conForm (PApp _ (PRef fc n) _) = isConName Nothing n (tt_ctxt i)

221− conForm (PRef fc n) = isConName Nothing n (tt_ctxt i)

220+ conForm (PApp _ (PRef fc n) _) = isConName n (tt_ctxt i)

221+ conForm (PRef fc n) = isConName n (tt_ctxt i)

222222 conForm _ = False

223223

224224 otherPats :: PTerm -> [PTerm]

@@ -227,22 +227,22 @@ genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of

227227 otherPats arg = return Placeholder

228228

229229 ops fc n xs o

230− | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)

230+ | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)

231231 = do xs' <- mapM otherPats (map getTm xs)

232232 let p = PApp fc (PRef fc n) (zipWith upd xs' xs)

233233 let tyn = getTy n (tt_ctxt i)

234− case lookupCtxt Nothing tyn (idris_datatypes i) of

234+ case lookupCtxt tyn (idris_datatypes i) of

235235 (TI ns _ _ : _) -> p : map (mkPat fc) (ns \\ [n])

236236 _ -> [p]

237237 ops fc n arg o = return Placeholder

238238

239− getTy n ctxt = case lookupTy Nothing n ctxt of

239+ getTy n ctxt = case lookupTy n ctxt of

240240 (t : _) -> case unApply (getRetTy t) of

241241 (P _ tyn _, _) -> tyn

242242 x -> error $ "Can't happen getTy 1 " ++ show (n, x)

243243 _ -> error "Can't happen getTy 2"

244244

245− mkPat fc x = case lookupCtxt Nothing x (idris_implicits i) of

245+ mkPat fc x = case lookupCtxt x (idris_implicits i) of

246246 (pargs : _)

247247 -> PApp fc (PRef fc x) (map (upd Placeholder) pargs)

248248 _ -> error "Can't happen - genAll"

@@ -306,7 +306,7 @@ calcProd i fc n pats = do patsprod <- mapM prodRec pats

306306

307307 cotype ty

308308 | (P _ t _, _) <- unApply (getRetTy ty)

309− = case lookupCtxt Nothing t (idris_datatypes i) of

309+ = case lookupCtxt t (idris_datatypes i) of

310310 [TI _ True _] -> True

311311 _ -> False

312312 | otherwise = False

@@ -315,7 +315,7 @@ calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)]

315315 -> Idris Totality

316316calcTotality path fc n pats

317317 = do i <- getIState

318− let opts = case lookupCtxt Nothing n (idris_flags i) of

318+ let opts = case lookupCtxt n (idris_flags i) of

319319 [fs] -> fs

320320 _ -> []

321321 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of

@@ -339,12 +339,12 @@ checkTotality path fc n

339339 updateContext (simplifyCasedef n)

340340 ctxt <- getContext

341341 i <- getIState

342− let opts = case lookupCtxt Nothing n (idris_flags i) of

342+ let opts = case lookupCtxt n (idris_flags i) of

343343 [fs] -> fs

344344 _ -> []

345345 t' <- case t of

346346 Unchecked ->

347− case lookupDef Nothing n ctxt of

347+ case lookupDef n ctxt of

348348 [CaseOp _ _ _ _ pats _ _ _ _] ->

349349 do t' <- if AssertTotal `elem` opts

350350 then return $ Total []

@@ -378,7 +378,7 @@ checkTotality path fc n

378378

379379 warnPartial n t

380380 = do i <- getIState

381− case lookupDef Nothing n (tt_ctxt i) of

381+ case lookupDef n (tt_ctxt i) of

382382 [x] -> do

383383 iputStrLn $ show fc ++ ":Warning - " ++ show n ++ " is " ++ show t

384384-- ++ "\n" ++ show x

@@ -407,8 +407,8 @@ checkDeclTotality (fc, n)

407407buildSCG :: (FC, Name) -> Idris ()

408408buildSCG (_, n) = do

409409 ist <- getIState

410− case lookupCtxt Nothing n (idris_callgraph ist) of

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

410+ case lookupCtxt n (idris_callgraph ist) of

411+ [cg] -> case lookupDef n (tt_ctxt ist) of

412412 [CaseOp _ _ _ _ _ args sc _ _] ->

413413 do logLvl 3 $ "Building SCG for " ++ show n ++ " from\n"

414414 ++ show sc

@@ -442,7 +442,7 @@ buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $

442442 -- how the arguments relate - either Smaller or Unknown

443443 argRels :: Name -> [(Name, SizeChange)]

444444 argRels n = let ctxt = tt_ctxt ist

445− [ty] = lookupTy Nothing n ctxt -- must exist!

445+ [ty] = lookupTy n ctxt -- must exist!

446446 P _ nty _ = fst (unApply (getRetTy ty))

447447 args = map snd (getArgTys ty) in

448448 map (getRel nty) (map (fst . unApply . getRetTy) args)

@@ -503,7 +503,7 @@ buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $

503503checkSizeChange :: Name -> Idris Totality

504504checkSizeChange n = do

505505 ist <- getIState

506− case lookupCtxt Nothing n (idris_callgraph ist) of

506+ case lookupCtxt n (idris_callgraph ist) of

507507 [cg] -> do let ms = mkMultiPaths ist [] (scg cg)

508508 logLvl 5 ("Multipath for " ++ show n ++ ":\n" ++

509509 "from " ++ show (scg cg) ++ "\n" ++

@@ -530,7 +530,7 @@ mkMultiPaths ist path cg

530530 where extend (nextf, args)

531531 | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]

532532 | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)

533− = case lookupCtxt Nothing nextf (idris_callgraph ist) of

533+ = case lookupCtxt nextf (idris_callgraph ist) of

534534 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)

535535 _ -> [ reverse ((nextf, args) : path) ]

536536 | otherwise = [ reverse ((nextf, args) : path) ]

@@ -538,7 +538,7 @@ mkMultiPaths ist path cg

538538-- do (nextf, args) <- cg

539539-- if ((nextf, args) `elem` path)

540540-- then return (reverse ((nextf, args) : path))

541−-- else case lookupCtxt Nothing nextf (idris_callgraph ist) of

541+-- else case lookupCtxt nextf (idris_callgraph ist) of

542542-- [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)

543543-- _ -> return (reverse ((nextf, args) : path))

544544

@@ -562,12 +562,12 @@ checkMP ist i mp = if i > 0

562562-- = Partial BelieveMe

563563 -- if we get to a constructor, it's fine as long as it's strictly positive

564564 tryPath desc path ((f, _) :es) arg

565− | [TyDecl (DCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)

565+ | [TyDecl (DCon _ _) _] <- lookupDef f (tt_ctxt ist)

566566 = case lookupTotal f (tt_ctxt ist) of

567567 [Total _] -> Unchecked -- okay so far

568568 [Partial _] -> Partial (Other [f])

569569 x -> error (show x)

570− | [TyDecl (TCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)

570+ | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)

571571 = Total []

572572 tryPath desc path (e@(f, args) : es) arg

573573 | e `elem` es && allNothing args = Partial (Mutual [f])

src/Idris/DataOpts.hs+8−8

@@ -17,7 +17,7 @@ import Debug.Trace

1717forceArgs :: Name -> Type -> Idris ()

1818forceArgs n t = do i <- getIState

1919 let fargs = force i 0 t

20− copt <- case lookupCtxt Nothing n (idris_optimisation i) of

20+ copt <- case lookupCtxt n (idris_optimisation i) of

2121 [] -> return $ Optimise False [] []

2222 (op:_) -> return op

2323 let opts = addDef n (copt { forceable = fargs }) (idris_optimisation i)

@@ -38,7 +38,7 @@ forceArgs n t = do i <- getIState

3838

3939 collapsibleIn i t

4040 | (P _ tn _, _) <- unApply t

41− = case lookupCtxt Nothing tn (idris_optimisation i) of

41+ = case lookupCtxt tn (idris_optimisation i) of

4242 [oi] -> collapsible oi

4343 _ -> False

4444 | otherwise = False

@@ -68,7 +68,7 @@ collapseCons ty cons =

6868 setCollapsible n

6969 = do i <- getIState

7070 iLOG $ show n ++ " collapsible"

71− case lookupCtxt Nothing n (idris_optimisation i) of

71+ case lookupCtxt n (idris_optimisation i) of

7272 (oi:_) -> do let oi' = oi { collapsible = True }

7373 let opts = addDef n oi' (idris_optimisation i)

7474 putIState (i { idris_optimisation = opts })

@@ -79,7 +79,7 @@ collapseCons ty cons =

7979

8080 forceRec :: IState -> (Name, [Type]) -> Idris Bool

8181 forceRec i (n, ts)

82− = case lookupCtxt Nothing n (idris_optimisation i) of

82+ = case lookupCtxt n (idris_optimisation i) of

8383 (oi:_) -> checkFR (forceable oi) 0 ts

8484 _ -> return False

8585 checkFR fs i [] = return True

@@ -161,7 +161,7 @@ instance Optimisable Raw where

161161 | (Var n, args) <- raw_unapply t -- MAGIC HERE

162162 = do args' <- mapM applyOpts args

163163 i <- getIState

164− case lookupCtxt Nothing n (idris_optimisation i) of

164+ case lookupCtxt n (idris_optimisation i) of

165165 (oi:_) -> return $ applyDataOpt oi n args'

166166 _ -> return (raw_apply (Var n) args')

167167 | otherwise = do f' <- applyOpts f

@@ -202,14 +202,14 @@ applyDataOpt oi n args

202202instance Optimisable (TT Name) where

203203 applyOpts c@(P (DCon t arity) n _)

204204 = do i <- getIState

205− case lookupCtxt Nothing n (idris_optimisation i) of

205+ case lookupCtxt n (idris_optimisation i) of

206206 (oi:_) -> return $ applyDataOptRT oi n t arity []

207207 _ -> return c

208208 applyOpts t@(App f a)

209209 | (c@(P (DCon t arity) n _), args) <- unApply t -- MAGIC HERE

210210 = do args' <- mapM applyOpts args

211211 i <- getIState

212− case lookupCtxt Nothing n (idris_optimisation i) of

212+ case lookupCtxt n (idris_optimisation i) of

213213 (oi:_) -> do return $ applyDataOptRT oi n t arity args'

214214 _ -> return (mkApp c args')

215215 | otherwise = do f' <- applyOpts f

@@ -224,7 +224,7 @@ instance Optimisable (TT Name) where

224224

225225 stripCollapsed (Bind n (PVar x) t) | (P _ ty _, _) <- unApply x

226226 = do i <- getIState

227− case lookupCtxt Nothing ty (idris_optimisation i) of

227+ case lookupCtxt ty (idris_optimisation i) of

228228 [oi] -> if collapsible oi

229229 then do t' <- stripCollapsed t

230230 return (Bind n (PVar x) (instantiate Erased t'))

src/Idris/Delaborate.hs+2−2

@@ -41,7 +41,7 @@ delab' ist tm fullname = de [] tm

4141 de env (TType i) = PType

4242

4343 dens x | fullname = x

44− dens ns@(NS n _) = case lookupCtxt Nothing n (idris_implicits ist) of

44+ dens ns@(NS n _) = case lookupCtxt n (idris_implicits ist) of

4545 [_] -> n -- just one thing

4646 _ -> ns

4747 dens n = n

@@ -62,7 +62,7 @@ delab' ist tm fullname = de [] tm

6262 deFn env f args = PApp un (de env f) (map pexp (map (de env) args))

6363

6464 mkPApp n args

65− | [imps] <- lookupCtxt Nothing n (idris_implicits ist)

65+ | [imps] <- lookupCtxt n (idris_implicits ist)

6666 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

6767 | otherwise = PApp un (PRef un n) (map pexp args)

6868

src/Idris/Docs.hs+6−6

@@ -65,9 +65,9 @@ instance Show Doc where

6565getDocs :: Name -> Idris Doc

6666getDocs n

6767 = do i <- getIState

68− case lookupCtxt Nothing n (idris_classes i) of

68+ case lookupCtxt n (idris_classes i) of

6969 [ci] -> docClass n ci

70− _ -> case lookupCtxt Nothing n (idris_datatypes i) of

70+ _ -> case lookupCtxt n (idris_datatypes i) of

7171 [ti] -> docData n ti

7272 _ -> do fd <- docFun n

7373 return (FunDoc fd)

@@ -81,7 +81,7 @@ docData n ti

8181docClass :: Name -> ClassInfo -> Idris Doc

8282docClass n ci

8383 = do i <- getIState

84− let docstr = case lookupCtxt Nothing n (idris_docstrings i) of

84+ let docstr = case lookupCtxt n (idris_docstrings i) of

8585 [str] -> str

8686 _ -> ""

8787 mdocs <- mapM docFun (map fst (class_methods ci))

@@ -90,13 +90,13 @@ docClass n ci

9090docFun :: Name -> Idris FunDoc

9191docFun n

9292 = do i <- getIState

93− let docstr = case lookupCtxt Nothing n (idris_docstrings i) of

93+ let docstr = case lookupCtxt n (idris_docstrings i) of

9494 [str] -> str

9595 _ -> ""

96− let ty = case lookupTy Nothing n (tt_ctxt i) of

96+ let ty = case lookupTy n (tt_ctxt i) of

9797 (t : _) -> t

9898 let argnames = map fst (getArgTys ty)

99− let args = case lookupCtxt Nothing n (idris_implicits i) of

99+ let args = case lookupCtxt n (idris_implicits i) of

100100 [args] -> zip argnames args

101101 _ -> []

102102 let infixes = idris_infixes i

src/Idris/ElabDecls.hs+19−19

@@ -69,7 +69,7 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

6969 let nty' = normalise ctxt [] nty

7070 let (t, _) = unApply (getRetTy nty')

7171 let corec = case t of

72− P _ rcty _ -> case lookupCtxt Nothing rcty (idris_datatypes i) of

72+ P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of

7373 [TI _ True _] -> True

7474 _ -> False

7575 _ -> False

@@ -93,14 +93,14 @@ elabPostulate info syn doc fc opts n ty

9393 -- make sure it's collapsible, so it is never needed at run time

9494 -- start by getting the elaborated type

9595 ctxt <- getContext

96− fty <- case lookupTy Nothing n ctxt of

96+ fty <- case lookupTy n ctxt of

9797 [] -> tclift $ tfail $ (At fc (NoTypeDecl n)) -- can't happen!

9898 [ty] -> return ty

9999 ist <- getIState

100100 let (ap, _) = unApply (getRetTy (normalise ctxt [] fty))

101101 logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)

102102 let postOK = case ap of

103− P _ tn _ -> case lookupCtxt Nothing tn

103+ P _ tn _ -> case lookupCtxt tn

104104 (idris_optimisation ist) of

105105 [oi] -> collapsible oi

106106 _ -> False

@@ -219,10 +219,10 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

219219 = do elabData info syn doc fc False (PDatadecl tyn ty [(cdoc, cn, cty, fc)])

220220 cty' <- implicit syn cn cty

221221 i <- getIState

222− cty <- case lookupTy Nothing cn (tt_ctxt i) of

222+ cty <- case lookupTy cn (tt_ctxt i) of

223223 [t] -> return (delab i t)

224224 _ -> fail "Something went inexplicably wrong"

225− cimp <- case lookupCtxt Nothing cn (idris_implicits i) of

225+ cimp <- case lookupCtxt cn (idris_implicits i) of

226226 [imps] -> return imps

227227 let ptys = getProjs [] (renameBs cimp cty)

228228 let ptys_u = getProjs [] cty

@@ -363,7 +363,7 @@ elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

363363elabClauses info fc opts n_in cs = let n = liftname info n_in in

364364 do ctxt <- getContext

365365 -- Check n actually exists, with no definition yet

366− let tys = lookupTy Nothing n ctxt

366+ let tys = lookupTy n ctxt

367367 checkUndefined n ctxt

368368 unless (length tys > 1) $ do

369369 fty <- case tys of

@@ -380,7 +380,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

380380 logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)

381381 -- FIXME: Really ought to only do this for total functions!

382382 let doNothing = case ap of

383− P _ tn _ -> case lookupCtxt Nothing tn

383+ P _ tn _ -> case lookupCtxt tn

384384 (idris_optimisation ist) of

385385 [oi] -> collapsible oi

386386 _ -> False

@@ -388,7 +388,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

388388 solveDeferred n

389389 ist <- getIState

390390 when doNothing $

391− case lookupCtxt Nothing n (idris_optimisation ist) of

391+ case lookupCtxt n (idris_optimisation ist) of

392392 [oi] -> do let opts = addDef n (oi { collapsible = True })

393393 (idris_optimisation ist)

394394 putIState (ist { idris_optimisation = opts })

@@ -460,7 +460,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

460460 ctxt <- getContext

461461 ist <- getIState

462462 putIState (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) })

463− case lookupTy (namespace info) n ctxt of

463+ case lookupTy n ctxt of

464464 [ty] -> do updateContext (addCasedef n (inlinable opts)

465465 tcase knowncovering

466466 (AssertTotal `elem` opts)

@@ -471,7 +471,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

471471 totcheck (fc, n)

472472 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

473473 i <- getIState

474− case lookupDef Nothing n (tt_ctxt i) of

474+ case lookupDef n (tt_ctxt i) of

475475 (CaseOp _ _ _ _ _ scargs sc scargs' sc' : _) ->

476476 do let calls = findCalls sc' scargs'

477477 let used = findUsedArgs sc' scargs'

@@ -487,7 +487,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

487487 [] -> return ()

488488 return ()

489489 where

490− checkUndefined n ctxt = case lookupDef Nothing n ctxt of

490+ checkUndefined n ctxt = case lookupDef n ctxt of

491491 [] -> return ()

492492 [TyDecl _ _] -> return ()

493493 _ -> tclift $ tfail (At fc (AlreadyDefined n))

@@ -572,10 +572,10 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

572572 -- pattern bindings

573573 i <- getIState

574574 -- get the parameters first, to pass through to any where block

575− let fn_ty = case lookupTy Nothing fname (tt_ctxt i) of

575+ let fn_ty = case lookupTy fname (tt_ctxt i) of

576576 [t] -> t

577577 _ -> error "Can't happen (elabClause function type)"

578− let fn_is = case lookupCtxt Nothing fname (idris_implicits i) of

578+ let fn_is = case lookupCtxt fname (idris_implicits i) of

579579 [t] -> t

580580 _ -> []

581581 let params = getParamsInType i [] fn_is fn_ty

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

679679 = getParamsInType i (n : env) is (instantiate (P Bound n t) sc)

680680 getParamsInType i env is tm@(App f a)

681681 | (P _ tn _, args) <- unApply tm

682− = case lookupCtxt Nothing tn (idris_datatypes i) of

682+ = case lookupCtxt tn (idris_datatypes i) of

683683 [t] -> nub $ paramNames args env (param_pos t) ++

684684 getParamsInType i env is f ++

685685 getParamsInType i env is a

@@ -955,7 +955,7 @@ elabClass info syn doc fc constraints tn ps ds

955955 let conn = case con of

956956 PRef _ n -> n

957957 PApp _ (PRef _ n) _ -> n

958− let conn' = case lookupCtxtName Nothing conn (idris_classes i) of

958+ let conn' = case lookupCtxtName conn (idris_classes i) of

959959 [(n, _)] -> n

960960 _ -> conn

961961 addInstance False conn' cfn

@@ -1016,7 +1016,7 @@ elabInstance :: ElabInfo -> SyntaxInfo ->

10161016 [PDecl] -> Idris ()

10171017elabInstance info syn fc cs n ps t expn ds

10181018 = do i <- getIState

1019− (n, ci) <- case lookupCtxtName (namespace info) n (idris_classes i) of

1019+ (n, ci) <- case lookupCtxtName n (idris_classes i) of

10201020 [c] -> return c

10211021 _ -> fail $ show fc ++ ":" ++ show n ++ " is not a type class"

10221022 let constraint = PApp fc (PRef fc n) (map pexp ps)

@@ -1076,7 +1076,7 @@ elabInstance info syn fc cs n ps t expn ds

10761076 checkNotOverlapping i t n

10771077 | take 2 (show n) == "@@" = return ()

10781078 | otherwise

1079− = case lookupTy Nothing n (tt_ctxt i) of

1079+ = case lookupTy n (tt_ctxt i) of

10801080 [t'] -> let tret = getRetType t

10811081 tret' = getRetType (delab i t') in

10821082 case matchClause i tret' tret of

@@ -1113,7 +1113,7 @@ elabInstance info syn fc cs n ps t expn ds

11131113 | PRef _ n <- getTm p

11141114 = do ps' <- getWParams ps

11151115 ctxt <- getContext

1116− case lookupP Nothing n ctxt of

1116+ case lookupP n ctxt of

11171117 [] -> return (pimp n (PRef fc n) : ps')

11181118 _ -> return ps'

11191119 getWParams (_ : ps) = getWParams ps

@@ -1248,7 +1248,7 @@ elabDecl' what info d@(PClauses f o n ps)

12481248 | what /= ETypes

12491249 = do iLOG $ "Elaborating clause " ++ show n

12501250 i <- getIState -- get the type options too

1251− let o' = case lookupCtxt Nothing n (idris_flags i) of

1251+ let o' = case lookupCtxt n (idris_flags i) of

12521252 [fs] -> fs

12531253 [] -> []

12541254 elabClauses info f (o ++ o') n ps

src/Idris/ElabTerm.hs+13−13

@@ -211,7 +211,7 @@ elab ist info pattern tcgen fn tm

211211 elab' ina (PPatvar fc n) | pattern = patvar n

212212 elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

213213 = do ctxt <- get_context

214− let defined = case lookupTy Nothing n ctxt of

214+ let defined = case lookupTy n ctxt of

215215 [] -> False

216216 _ -> True

217217 -- this is to stop us resolve type classes recursively

@@ -221,7 +221,7 @@ elab ist info pattern tcgen fn tm

221221 then do apply (Var n) []; solve

222222 else try (do apply (Var n) []; solve)

223223 (patvar n)

224− where inparamBlock n = case lookupCtxtName Nothing n (inblock info) of

224+ where inparamBlock n = case lookupCtxtName n (inblock info) of

225225 [] -> False

226226 _ -> True

227227 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])

@@ -334,7 +334,7 @@ elab ist info pattern tcgen fn tm

334334 elab' (ina, g) tm@(PApp fc (PRef _ f) args')

335335 = do let args = {- case lookupCtxt f (inblock info) of

336336 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

337− _ ->-} args'

337+ _ -> -} args'

338338-- newtm <- mkSpecialised ist fc f (map getTm args') tm

339339 env <- get_env

340340 if (f `elem` map fst env && length args' == 1)

@@ -350,11 +350,11 @@ elab ist info pattern tcgen fn tm

350350 let isinf = f == inferCon || tcname f

351351 -- if f is a type class, we need to know its arguments so that

352352 -- we can unify with them

353− case lookupCtxt Nothing f (idris_classes ist) of

353+ case lookupCtxt f (idris_classes ist) of

354354 [] -> return ()

355355 _ -> mapM_ setInjective (map getTm args')

356356 ctxt <- get_context

357− let guarded = isConName Nothing f ctxt

357+ let guarded = isConName f ctxt

358358 ns <- apply (Var f) (map isph args)

359359 ptm <- get_term

360360 g <- goal

@@ -547,7 +547,7 @@ pruneAlt xs = map prune xs

547547pruneByType :: Term -> Context -> [PTerm] -> [PTerm]

548548pruneByType (P _ n _) c as

549549-- if the goal type is polymorphic, keep e

550− | [] <- lookupTy Nothing n c = as

550+ | [] <- lookupTy n c = as

551551 | otherwise

552552 = let asV = filter (headIs True n) as

553553 as' = filter (headIs False n) as in

@@ -563,7 +563,7 @@ pruneByType (P _ n _) c as

563563 headIs _ _ _ = True -- keep if it's not an application

564564

565565 typeHead var f f'

566− = case lookupTy Nothing f' c of

566+ = case lookupTy f' c of

567567 [ty] -> let ty' = normalise c [] ty in

568568 case unApply (getRetTy ty') of

569569 (P _ ftyn _, _) -> ftyn == f

@@ -596,7 +596,7 @@ trivial ist = try' (do elab ist toplevel False False (MN 0 "tac")

596596findInstances :: IState -> Term -> [Name]

597597findInstances ist t

598598 | (P _ n _, _) <- unApply t

599− = case lookupCtxt Nothing n (idris_classes ist) of

599+ = case lookupCtxt n (idris_classes ist) of

600600 [CI _ _ _ _ ins] -> ins

601601 _ -> []

602602 | otherwise = []

@@ -658,7 +658,7 @@ resolveTC depth fn ist

658658-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist

659659-- else do

660660 -- if there's a hole in the goal, don't even try

661− let imps = case lookupCtxtName Nothing n (idris_implicits ist) of

661+ let imps = case lookupCtxtName n (idris_implicits ist) of

662662 [] -> []

663663 [args] -> map isImp (snd args) -- won't be overloaded!

664664 ps <- get_probs

@@ -716,7 +716,7 @@ runTac autoSolve ist tac = do env <- get_env

716716 runT (Exact tm) = do elab ist toplevel False False (MN 0 "tac") tm

717717 when autoSolve solveAll

718718 runT (Refine fn [])

719− = do (fn', imps) <- case lookupCtxtName Nothing fn (idris_implicits ist) of

719+ = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of

720720 [] -> do a <- envArgs fn

721721 return (fn, a)

722722 -- FIXME: resolve ambiguities

@@ -1200,7 +1200,7 @@ solveAll = try (do solve; solveAll) (return ())

12001200mkSpecialised :: IState -> FC -> Name -> [PTerm] -> PTerm -> ElabD PTerm

12011201mkSpecialised i fc n args def

12021202 = do let tm' = def

1203− case lookupCtxt Nothing n (idris_statics i) of

1203+ case lookupCtxt n (idris_statics i) of

12041204 [] -> return tm'

12051205 [as] -> if (not (or as)) then return tm' else

12061206 mkSpecDecl i n (zip args as) tm'

@@ -1227,8 +1227,8 @@ mkSpecDecl i n pargs tm'

12271227 cg = idris_callgraph i

12281228

12291229 staticFnNames tm | (P _ f _, as) <- unApply tm

1230− = if not (isFnName Nothing f ctxt) then []

1231− else case lookupCtxt Nothing f cg of

1230+ = if not (isFnName f ctxt) then []

1231+ else case lookupCtxt f cg of

12321232 [ns] -> f : f : [] --(ns \\ [f])

12331233 [] -> [f,f]

12341234 _ -> []

src/Idris/IBC.hs+9−9

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

8282 mkIBC is f'

8383

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

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

85+ibc i (IBCImp n) f = case lookupCtxt n (idris_implicits i) of

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

8787 _ -> fail "IBC write failed"

8888ibc i (IBCStatic n) f

89− = case lookupCtxt Nothing n (idris_statics i) of

89+ = case lookupCtxt n (idris_statics i) of

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

9191 _ -> fail "IBC write failed"

9292ibc i (IBCClass n) f

93− = case lookupCtxt Nothing n (idris_classes i) of

93+ = case lookupCtxt n (idris_classes i) of

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

9595 _ -> fail "IBC write failed"

9696ibc i (IBCInstance int n ins) f

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

9898ibc i (IBCDSL n) f

99− = case lookupCtxt Nothing n (idris_dsls i) of

99+ = case lookupCtxt n (idris_dsls i) of

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

101101 _ -> fail "IBC write failed"

102102ibc i (IBCData n) f

103− = case lookupCtxt Nothing n (idris_datatypes i) of

103+ = case lookupCtxt n (idris_datatypes i) of

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

105105 _ -> fail "IBC write failed"

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

106+ibc i (IBCOpt n) f = case lookupCtxt n (idris_optimisation i) of

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

108108 _ -> fail "IBC write failed"

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

@@ -113,13 +113,13 @@ ibc i (IBCObj n) f = return f { ibc_objs = n : ibc_objs f }

113113ibc i (IBCLib n) f = return f { ibc_libs = n : ibc_libs f }

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

115115ibc i (IBCHeader n) f = return f { ibc_hdrs = n : ibc_hdrs f }

116−ibc i (IBCDef n) f = case lookupDef Nothing n (tt_ctxt i) of

116+ibc i (IBCDef n) f = case lookupDef n (tt_ctxt i) of

117117 [v] -> return f { ibc_defs = (n,v) : ibc_defs f }

118118 _ -> fail "IBC write failed"

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

119+ibc i (IBCDoc n) f = case lookupCtxt n (idris_docstrings i) of

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

121121 _ -> fail "IBC write failed"

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

122+ibc i (IBCCG n) f = case lookupCtxt n (idris_callgraph i) of

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

124124 _ -> fail "IBC write failed"

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

src/Idris/Parser.hs+1−1

@@ -881,7 +881,7 @@ pApp syn = do f <- pSimpleExpr syn

881881 return (dslify i $ PApp fc f args)

882882 where

883883 dslify i (PApp fc (PRef _ f) [a])

884− | [d] <- lookupCtxt Nothing f (idris_dsls i)

884+ | [d] <- lookupCtxt f (idris_dsls i)

885885 = desugar (syn { dsl_info = d }) i (getTm a)

886886 dslify i t = t

887887

src/Idris/Prover.hs+1−1

@@ -26,7 +26,7 @@ prover :: Bool -> Name -> Idris ()

2626prover lit x =

2727 do ctxt <- getContext

2828 i <- getIState

29− case lookupTy Nothing x ctxt of

29+ case lookupTy x ctxt of

3030 [t] -> if elem x (idris_metavars i)

3131 then prove ctxt lit x t

3232 else fail $ show x ++ " is not a metavariable"

src/Idris/REPL.hs+15−15

@@ -129,7 +129,7 @@ resolveProof :: Name -> Idris Name

129129resolveProof n'

130130 = do i <- getIState

131131 ctxt <- getContext

132− n <- case lookupNames Nothing n' ctxt of

132+ n <- case lookupNames n' ctxt of

133133 [x] -> return x

134134 [] -> return n'

135135 ns -> fail $ pshow i (CantResolveAlts (map show ns))

@@ -207,7 +207,7 @@ process fn (Check (PRef _ n))

207207 = do ctxt <- getContext

208208 ist <- getIState

209209 imp <- impShow

210− case lookupTy Nothing n ctxt of

210+ case lookupTy n ctxt of

211211 ts@(_:_) -> mapM_ (\t -> iputStrLn $ show n ++ " : " ++

212212 showImp imp (delab ist t)) ts

213213 [] -> iputStrLn $ "No such variable " ++ show n

@@ -220,7 +220,7 @@ process fn (Check t) = do (tm, ty) <- elabVal toplevel False t

220220 showImp imp (delab ist ty))

221221

222222process fn (DocStr n) = do i <- getIState

223− case lookupCtxtName Nothing n (idris_docstrings i) of

223+ case lookupCtxtName n (idris_docstrings i) of

224224 [] -> iputStrLn $ "No documentation for " ++ show n

225225 ns -> mapM_ showDoc ns

226226 where showDoc (n, d)

@@ -237,8 +237,8 @@ process fn Universes = do i <- getIState

237237 OK _ -> iputStrLn "Universes OK"

238238process fn (Defn n) = do i <- getIState

239239 iputStrLn "Compiled patterns:\n"

240− liftIO $ print (lookupDef Nothing n (tt_ctxt i))

241− case lookupCtxt Nothing n (idris_patdefs i) of

240+ liftIO $ print (lookupDef n (tt_ctxt i))

241+ case lookupCtxt n (idris_patdefs i) of

242242 [] -> return ()

243243 [d] -> do iputStrLn "Original definiton:\n"

244244 mapM_ (printCase i) d

@@ -255,25 +255,25 @@ process fn (TotCheck n) = do i <- getIState

255255 _ -> return ()

256256process fn (DebugInfo n)

257257 = do i <- getIState

258− let oi = lookupCtxtName Nothing n (idris_optimisation i)

258+ let oi = lookupCtxtName n (idris_optimisation i)

259259 when (not (null oi)) $ iputStrLn (show oi)

260− let si = lookupCtxt Nothing n (idris_statics i)

260+ let si = lookupCtxt n (idris_statics i)

261261 when (not (null si)) $ iputStrLn (show si)

262− let di = lookupCtxt Nothing n (idris_datatypes i)

262+ let di = lookupCtxt n (idris_datatypes i)

263263 when (not (null di)) $ iputStrLn (show di)

264− let d = lookupDef Nothing n (tt_ctxt i)

264+ let d = lookupDef n (tt_ctxt i)

265265 when (not (null d)) $ liftIO $

266266 do print (head d)

267− let cg = lookupCtxtName Nothing n (idris_callgraph i)

267+ let cg = lookupCtxtName n (idris_callgraph i)

268268 findUnusedArgs (map fst cg)

269269 i <- getIState

270− let cg' = lookupCtxtName Nothing n (idris_callgraph i)

270+ let cg' = lookupCtxtName n (idris_callgraph i)

271271 sc <- checkSizeChange n

272272 iputStrLn $ "Size change: " ++ show sc

273273 when (not (null cg')) $ do iputStrLn "Call graph:\n"

274274 iputStrLn (show cg')

275275process fn (Info n) = do i <- getIState

276− case lookupCtxt Nothing n (idris_classes i) of

276+ case lookupCtxt n (idris_classes i) of

277277 [c] -> classInfo c

278278 _ -> iputStrLn "Not a class"

279279process fn (Search t) = iputStrLn "Not implemented"

@@ -330,7 +330,7 @@ process fn (ShowProof n')

330330process fn (Prove n')

331331 = do ctxt <- getContext

332332 ist <- getIState

333− n <- case lookupNames Nothing n' ctxt of

333+ n <- case lookupNames n' ctxt of

334334 [x] -> return x

335335 [] -> return n'

336336 ns -> fail $ pshow ist (CantResolveAlts (map show ns))

@@ -381,7 +381,7 @@ process fn (Pattelab t)

381381 iputStrLn $ show tm ++ "\n\n : " ++ show ty

382382

383383process fn (Missing n) = do i <- getIState

384− case lookupDef Nothing n (tt_ctxt i) of

384+ case lookupDef n (tt_ctxt i) of

385385 [CaseOp _ _ _ _ _ args t _ _]

386386 -> do tms <- genMissing n args t

387387 iputStrLn (showSep "\n" (map (showImp True) tms))

@@ -431,7 +431,7 @@ dumpInstance :: Name -> Idris ()

431431dumpInstance n = do i <- getIState

432432 ctxt <- getContext

433433 imp <- impShow

434− case lookupTy Nothing n ctxt of

434+ case lookupTy n ctxt of

435435 ts -> mapM_ (\t -> iputStrLn $ showImp imp (delab i t)) ts

436436

437437showTotal t@(Partial (Other ns)) i

src/Idris/UnusedArgs.hs+2−2

@@ -15,7 +15,7 @@ findUnusedArgs ns = mapM_ traceUnused ns

1515traceUnused :: Name -> Idris ()

1616traceUnused n

1717 = do i <- getIState

18− case lookupCtxt Nothing n (idris_callgraph i) of

18+ case lookupCtxt n (idris_callgraph i) of

1919 [CGInfo args calls scg usedns _] ->

2020 do let argpos = zip args [0..]

2121 let fargs = concatMap (getFargpos calls) argpos

@@ -39,7 +39,7 @@ used path g j

3939 | otherwise

4040 = do logLvl 5 $ (show ((g, j) : path))

4141 i <- getIState

42− case lookupCtxt Nothing g (idris_callgraph i) of

42+ case lookupCtxt g (idris_callgraph i) of

4343 [CGInfo args calls scg usedns unused] ->

4444 if (j >= length args)

4545 then -- overapplied, assume used