a807a34 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Remove the unused arg from lookup functions

a807a34David Christiansen14 years ago

src/Core/Elaborate.hs+3−3

compare with master

unifiedsplit

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

171 if isInj ctxt tm then return ()

172 else lift $ tfail (NotInjective tm l r)

173 where isInj ctxt (P _ n _)

174− | isConName Nothing n ctxt = True

174+ | isConName n ctxt = True

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

176 isInj ctxt (Constant _) = True

177 isInj ctxt (TType _) = True

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

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

211uniqueNameCtxt ctxt n hs

212 | 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

214 | otherwise = return n

215

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

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

356 mkClaims _ _ _ _

357 | Var n <- fn

358 = do ctxt <- get_context

359− case lookupTy Nothing n ctxt of

359+ case lookupTy n ctxt of

360 [] -> lift $ tfail $ NoSuchVariable n

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

362 | 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

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

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

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

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

152+ = do let val = lookupDefAcc n atRepl ctxt

153 case val of

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

155 ev ntimes (n:stk) True env tm

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

220 _ -> return $ unload env f args

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

222 = traceWhen traceon (show stk) $

223− do let val = lookupDefAcc Nothing n atRepl ctxt

223+ do let val = lookupDefAcc n atRepl ctxt

224 case val of

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

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

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

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

244

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

246−-- = case lookupCtxt Nothing n statics of

246+-- = case lookupCtxt n statics of

247-- [as] -> if or as

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

249-- return $ unload env f args

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

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

398 ev env (P _ n ty)

399 | 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

401 [Function _ t] -> ev env t

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

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

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

430 app <- apply env sc' as

431 wknH (-1) app

432 apply env (HP Ref n ty) args

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

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

434 = do c <- evCase env ns args tree

435 case c of

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

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

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

566 caseeq ps _ _ = return False

567

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

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

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

571 ([CaseOp _ _ _ _ _ _ xdef _ _],

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

730 Type -> Context -> Context

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

732 = let ctxt = definitions uctxt

733− access = case lookupDefAcc Nothing n False uctxt of

733+ access = case lookupDefAcc n False uctxt of

734 [(_, acc)] -> acc

735 _ -> Public

736 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

747simplifyCasedef :: Name -> Context -> Context

748simplifyCasedef n uctxt

749 = let ctxt = definitions uctxt

750− ctxt' = case lookupCtxt Nothing n ctxt of

750+ ctxt' = case lookupCtxt n ctxt of

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

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

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

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

780

781tfst (a, _, _) = a

782

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

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

784−lookupNames root n ctxt

784+lookupNames n ctxt

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

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

786 map fst ns

787

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

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

789−lookupTy root n ctxt

789+lookupTy n ctxt

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

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

791 case tfst def of

792 (Function ty _) -> return ty

793 (TyDecl _ ty) -> return ty

794 (Operator ty _ _) -> return ty

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

796

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

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

798−isConName root n ctxt

798+isConName n ctxt

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

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

800 case tfst def of

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

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

803 _ -> return False

804

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

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

806−isFnName root n ctxt

806+isFnName n ctxt

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

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

808 case tfst def of

809 (Function _ _) -> return True

810 (Operator _ _ _) -> return True

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

812 _ -> return False

813

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

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

815−lookupP root n ctxt

815+lookupP n ctxt

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

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

817 p <- case def of

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

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

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

823 Hidden -> []

824 _ -> return (fst p)

825

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

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

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

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

828

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

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

830 [(Def, Accessibility)]

831−lookupDefAcc root n mkpublic ctxt

831+lookupDefAcc n mkpublic ctxt

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

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

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

834

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

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

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

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

838

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

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

840−lookupVal root n ctxt

840+lookupVal n ctxt

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

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

842 case tfst def of

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

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

src/Core/ProofShell.hs+1−1

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

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

42 err -> (state, show err)

43processCommand (Print n) state =

44− case lookupDef Nothing n (ctxt state) of

44+ case lookupDef n (ctxt state) of

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

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

47processCommand (Tac e) state

src/Core/TT.hs+5−5

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

244

245-}

246

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

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

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

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

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

250 Nothing -> []

251 where

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

258 nsmatch (NS _ _) _ = False

259 nsmatch looking found = True

260

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

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

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

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

263

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

265updateDef n f ctxt

266− = let ds = lookupCtxtName Nothing n ctxt in

266+ = let ds = lookupCtxtName n ctxt in

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

268

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

src/Core/Typecheck.hs+1−1

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

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

61 chk env (Var n)

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

64 | otherwise = do lift $ tfail $ NoSuchVariable n

65 chk env (RApp f a)

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

src/IRTS/Compiler.hs+3−3

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

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

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

100allNames ns n = do i <- getIState

101− case lookupCtxt Nothing n (idris_callgraph i) of

101+ case lookupCtxt n (idris_callgraph i) of

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

103 return (nub (n : concat more))

104 _ -> return [n]

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

205 Just tm -> return tm

206 _ -> do

207 let collapse

208− = case lookupCtxt Nothing n

208+ = case lookupCtxt n

209 (idris_optimisation i) of

210 [oi] -> collapsible oi

211 _ -> False

212 let unused

213− = case lookupCtxt Nothing n

213+ = case lookupCtxt n

214 (idris_callgraph i) of

215 [CGInfo _ _ _ _ unusedpos] ->

216 unusedpos

src/IRTS/Defunctionalise.hs+2−2

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

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

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

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

83− case lookupCtxt Nothing n defs of

83+ case lookupCtxt n defs of

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

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

86 fixApply tc n args' arity

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

88 aa env (LLazyApp n args)

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

90− case lookupCtxt Nothing n defs of

90+ case lookupCtxt n defs of

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

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

93 fixLazyApply n args' arity

src/IRTS/Simplified.hs+7−7

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

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

47simplify tl (DV (Glob x))

48 = do ctxt <- ldefs

49− case lookupCtxt Nothing x ctxt of

49+ case lookupCtxt x ctxt of

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

51 _ -> return $ SV (Glob x)

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

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

89sVar (DV (Glob x))

90 = do ctxt <- ldefs

91− case lookupCtxt Nothing x ctxt of

91+ case lookupCtxt x ctxt of

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

93 _ -> return (Glob x, Nothing)

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

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

136 sc env (SV (Glob n)) =

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

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

139− Nothing -> case lookupCtxt Nothing n ctxt of

139+ Nothing -> case lookupCtxt n ctxt of

140 [DConstructor _ i ar] ->

141 if True -- ar == 0

142 then return (SCon i n [])

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

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

147 sc env (SApp tc f args)

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

149− case lookupCtxt Nothing f ctxt of

149+ case lookupCtxt f ctxt of

150 [DConstructor n tag ar] ->

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

152 then return $ SCon tag n args'

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

160 return $ SForeign l ty f args'

161 sc env (SCon tag f args)

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

163− case lookupCtxt Nothing f ctxt of

163+ case lookupCtxt f ctxt of

164 [DConstructor n tag ar] ->

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

166 then return $ SCon tag n args'

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

197 scVar env (Glob n) =

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

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

200− Nothing -> case lookupCtxt Nothing n ctxt of

200+ Nothing -> case lookupCtxt n ctxt of

201 [DConstructor _ i ar] ->

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

203 [_] -> return (Glob n)

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

207

208 scalt env (SConCase _ i n args e)

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

210− tag <- case lookupCtxt Nothing n ctxt of

210+ tag <- case lookupCtxt n ctxt of

211 [DConstructor _ i ar] ->

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

213 then return i

src/Idris/AbsSyntax.hs+12−12

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

88 findCoercions fn cs

89 where findCoercions t [] = []

90 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

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

93 (t', _) ->

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

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

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

120addInstance int n i

121 = do ist <- getIState

122− case lookupCtxt Nothing n (idris_classes ist) of

122+ case lookupCtxt n (idris_classes ist) of

123 [CI a b c d ins] ->

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

125 putIState $ ist { idris_classes = cs }

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

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

140addClass n i

141 = do ist <- getIState

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

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

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

144 _ -> i

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

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

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

194checkUndefined fc n

195 = do i <- getContext

196− case lookupTy Nothing n i of

196+ case lookupTy n i of

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

198 show n ++ " already defined"

199 _ -> return ()

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

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

202isUndefined fc n

203 = do i <- getContext

204− case lookupTy Nothing n i of

204+ case lookupTy n i of

205 (_:_) -> return False

206 _ -> return True

207

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

641getPriority i tm = 1 -- pri tm

642 where

643 pri (PRef _ n) =

644− case lookupP Nothing n (tt_ctxt i) of

644+ case lookupP n (tt_ctxt i) of

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

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

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

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

882

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

884aiFn inpat True ist fc f []

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

885+ = case lookupDef f (tt_ctxt ist) of

886 [] -> 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

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

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

890 || any constructor alts || any allImp ialts)

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

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

905aiFn inpat expat ist fc f as

906 -- 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

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

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

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

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

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

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

951 sl (PRef fc f)

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

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

953 = return $ PRef fc f

954 | otherwise = do ns <- get

955 if (f `elem` ns)

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

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

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

1079 | n == n' && not names &&

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

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

1081 = return [(n, tm)]

1082 | n == n' = return []

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

1085 = return [(n, tm)]

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

1087 mr <- match' r r'

src/Idris/AbsSyntaxTree.hs+2−2

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

1128 where

1129 ni env (PRef _ n)

1130 | not (n `elem` env)

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

1131+ = case lookupTy n (tt_ctxt ist) of

1132 [] -> [n]

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

1134 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

1152 where

1153 ni env (PRef _ n)

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

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

1155+ = case lookupTy n (tt_ctxt ist) of

1156 [] -> [n]

1157 _ -> []

1158 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

38 evalStateT (toTT timp) 0

39 where

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

41− case lookupDef Nothing n (tt_ctxt i) of

41+ case lookupDef n (tt_ctxt i) of

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

43 _ -> return $ P Ref n Erased

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

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

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

108 = return $ all ++ [DefaultCase def]

109expandAlts 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)

111 = 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

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

114 return $ addAlts ps (altsFor all) all

115 _ -> return all

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

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

128

129 getTy n ctxt

130− = case lookupTy Nothing n ctxt of

130+ = case lookupTy n ctxt of

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

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

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

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

135

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

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

137 (pargs : _)

138 -> (x, length pargs)

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

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

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

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

162 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

164 (p : _) -> p

165 _ -> repeat (pexp Placeholder)

166 let tryclauses = mkClauses parg all_args

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

217 [] -> [Placeholder]

218 xs -> nub xs

219 where

220− conForm (PApp _ (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 Nothing n (tt_ctxt i)

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

222 conForm _ = False

223

224 otherPats :: PTerm -> [PTerm]

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

227 otherPats arg = return Placeholder

228

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

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

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

233 let tyn = getTy n (tt_ctxt i)

234− case lookupCtxt Nothing tyn (idris_datatypes i) of

234+ case lookupCtxt tyn (idris_datatypes i) of

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

236 _ -> [p]

237 ops fc n arg o = return Placeholder

238

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

239+ getTy n ctxt = case lookupTy n ctxt of

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

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

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

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

244

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

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

246 (pargs : _)

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

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

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

306

307 cotype ty

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

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

309+ = case lookupCtxt t (idris_datatypes i) of

310 [TI _ True _] -> True

311 _ -> False

312 | otherwise = False

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

315 -> Idris Totality

316calcTotality path fc n pats

317 = do i <- getIState

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

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

319 [fs] -> fs

320 _ -> []

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

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

339 updateContext (simplifyCasedef n)

340 ctxt <- getContext

341 i <- getIState

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

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

343 [fs] -> fs

344 _ -> []

345 t' <- case t of

346 Unchecked ->

347− case lookupDef Nothing n ctxt of

347+ case lookupDef n ctxt of

348 [CaseOp _ _ _ _ pats _ _ _ _] ->

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

350 then return $ Total []

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

378

379 warnPartial n t

380 = do i <- getIState

381− case lookupDef Nothing n (tt_ctxt i) of

381+ case lookupDef n (tt_ctxt i) of

382 [x] -> do

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

384-- ++ "\n" ++ show x

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

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

408buildSCG (_, n) = do

409 ist <- getIState

410− case lookupCtxt Nothing n (idris_callgraph ist) of

410+ case lookupCtxt n (idris_callgraph ist) of

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

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

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

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

414 ++ show sc

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

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

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

444 argRels n = let ctxt = tt_ctxt ist

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

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

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

447 args = map snd (getArgTys ty) in

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

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

503checkSizeChange :: Name -> Idris Totality

504checkSizeChange n = do

505 ist <- getIState

506− case lookupCtxt Nothing n (idris_callgraph ist) of

506+ case lookupCtxt n (idris_callgraph ist) of

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

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

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

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

530 where extend (nextf, args)

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

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

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

533+ = case lookupCtxt nextf (idris_callgraph ist) of

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

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

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

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

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

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

540-- 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

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

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

544

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

562-- = Partial BelieveMe

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

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

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

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

566 = case lookupTotal f (tt_ctxt ist) of

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

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

569 x -> error (show x)

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

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

571 = Total []

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

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

src/Idris/DataOpts.hs+8−8

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

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

18forceArgs n t = do i <- getIState

19 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

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

22 (op:_) -> return op

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

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

39 collapsibleIn i t

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

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

41+ = case lookupCtxt tn (idris_optimisation i) of

42 [oi] -> collapsible oi

43 _ -> False

44 | otherwise = False

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

68 setCollapsible n

69 = do i <- getIState

70 iLOG $ show n ++ " collapsible"

71− case lookupCtxt Nothing n (idris_optimisation i) of

71+ case lookupCtxt n (idris_optimisation i) of

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

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

74 putIState (i { idris_optimisation = opts })

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

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

81 forceRec i (n, ts)

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

82+ = case lookupCtxt n (idris_optimisation i) of

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

84 _ -> return False

85 checkFR fs i [] = return True

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

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

162 = do args' <- mapM applyOpts args

163 i <- getIState

164− case lookupCtxt Nothing n (idris_optimisation i) of

164+ case lookupCtxt n (idris_optimisation i) of

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

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

167 | otherwise = do f' <- applyOpts f

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

202instance Optimisable (TT Name) where

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

204 = do i <- getIState

205− case lookupCtxt Nothing n (idris_optimisation i) of

205+ case lookupCtxt n (idris_optimisation i) of

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

207 _ -> return c

208 applyOpts t@(App f a)

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

210 = do args' <- mapM applyOpts args

211 i <- getIState

212− case lookupCtxt Nothing n (idris_optimisation i) of

212+ case lookupCtxt n (idris_optimisation i) of

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

214 _ -> return (mkApp c args')

215 | otherwise = do f' <- applyOpts f

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

224

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

226 = do i <- getIState

227− case lookupCtxt Nothing ty (idris_optimisation i) of

227+ case lookupCtxt ty (idris_optimisation i) of

228 [oi] -> if collapsible oi

229 then do t' <- stripCollapsed t

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

src/Idris/Delaborate.hs+2−2

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

41 de env (TType i) = PType

43 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

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

46 _ -> ns

47 dens n = n

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

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

64 mkPApp n args

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

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

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

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

src/Idris/Docs.hs+6−6

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

65getDocs :: Name -> Idris Doc

66getDocs n

67 = do i <- getIState

68− case lookupCtxt Nothing n (idris_classes i) of

68+ case lookupCtxt n (idris_classes i) of

69 [ci] -> docClass n ci

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

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

71 [ti] -> docData n ti

72 _ -> do fd <- docFun n

73 return (FunDoc fd)

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

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

82docClass n ci

83 = do i <- getIState

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

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

85 [str] -> str

86 _ -> ""

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

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

90docFun :: Name -> Idris FunDoc

91docFun n

92 = do i <- getIState

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

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

94 [str] -> str

95 _ -> ""

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

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

97 (t : _) -> t

98 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

100 [args] -> zip argnames args

101 _ -> []

102 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

69 let nty' = normalise ctxt [] nty

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

71 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

73 [TI _ True _] -> True

74 _ -> False

75 _ -> False

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

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

94 -- start by getting the elaborated type

95 ctxt <- getContext

96− fty <- case lookupTy Nothing n ctxt of

96+ fty <- case lookupTy n ctxt of

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

98 [ty] -> return ty

99 ist <- getIState

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

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

102 let postOK = case ap of

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

103+ P _ tn _ -> case lookupCtxt tn

104 (idris_optimisation ist) of

105 [oi] -> collapsible oi

106 _ -> False

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

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

220 cty' <- implicit syn cn cty

221 i <- getIState

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

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

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

224 _ -> fail "Something went inexplicably wrong"

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

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

226 [imps] -> return imps

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

228 let ptys_u = getProjs [] cty

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

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

364 do ctxt <- getContext

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

366− let tys = lookupTy Nothing n ctxt

366+ let tys = lookupTy n ctxt

367 checkUndefined n ctxt

368 unless (length tys > 1) $ do

369 fty <- case tys of

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

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

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

382 let doNothing = case ap of

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

383+ P _ tn _ -> case lookupCtxt tn

384 (idris_optimisation ist) of

385 [oi] -> collapsible oi

386 _ -> False

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

388 solveDeferred n

389 ist <- getIState

390 when doNothing $

391− case lookupCtxt Nothing n (idris_optimisation ist) of

391+ case lookupCtxt n (idris_optimisation ist) of

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

393 (idris_optimisation ist)

394 putIState (ist { idris_optimisation = opts })

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

460 ctxt <- getContext

461 ist <- getIState

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

463− case lookupTy (namespace info) n ctxt of

463+ case lookupTy n ctxt of

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

465 tcase knowncovering

466 (AssertTotal `elem` opts)

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

471 totcheck (fc, n)

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

473 i <- getIState

474− case lookupDef Nothing n (tt_ctxt i) of

474+ case lookupDef n (tt_ctxt i) of

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

476 do let calls = findCalls sc' scargs'

477 let used = findUsedArgs sc' scargs'

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

487 [] -> return ()

488 return ()

489 where

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

490+ checkUndefined n ctxt = case lookupDef n ctxt of

491 [] -> return ()

492 [TyDecl _ _] -> return ()

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

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

572 -- pattern bindings

573 i <- getIState

574 -- 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

576 [t] -> t

577 _ -> 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

579 [t] -> t

580 _ -> []

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

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

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

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

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

682+ = case lookupCtxt tn (idris_datatypes i) of

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

684 getParamsInType i env is f ++

685 getParamsInType i env is a

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

955 let conn = case con of

956 PRef _ n -> n

957 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

959 [(n, _)] -> n

960 _ -> conn

961 addInstance False conn' cfn

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

1016 [PDecl] -> Idris ()

1017elabInstance info syn fc cs n ps t expn ds

1018 = 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

1020 [c] -> return c

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

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

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

1076 checkNotOverlapping i t n

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

1078 | otherwise

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

1079+ = case lookupTy n (tt_ctxt i) of

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

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

1082 case matchClause i tret' tret of

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

1113 | PRef _ n <- getTm p

1114 = do ps' <- getWParams ps

1115 ctxt <- getContext

1116− case lookupP Nothing n ctxt of

1116+ case lookupP n ctxt of

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

1118 _ -> return ps'

1119 getWParams (_ : ps) = getWParams ps

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

1248 | what /= ETypes

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

1250 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

1252 [fs] -> fs

1253 [] -> []

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

src/Idris/ElabTerm.hs+13−13

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

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

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

213 = do ctxt <- get_context

214− let defined = case lookupTy Nothing n ctxt of

214+ let defined = case lookupTy n ctxt of

215 [] -> False

216 _ -> True

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

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

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

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

223 (patvar n)

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

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

225 [] -> False

226 _ -> True

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

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

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

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

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

337− _ ->-} args'

337+ _ -> -} args'

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

339 env <- get_env

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

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

350 let isinf = f == inferCon || tcname f

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

352 -- we can unify with them

353− case lookupCtxt Nothing f (idris_classes ist) of

353+ case lookupCtxt f (idris_classes ist) of

354 [] -> return ()

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

356 ctxt <- get_context

357− let guarded = isConName Nothing f ctxt

357+ let guarded = isConName f ctxt

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

359 ptm <- get_term

360 g <- goal

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

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

548pruneByType (P _ n _) c as

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

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

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

551 | otherwise

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

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

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

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

564

565 typeHead var f f'

566− = case lookupTy Nothing f' c of

566+ = case lookupTy f' c of

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

568 case unApply (getRetTy ty') of

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

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

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

597findInstances ist t

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

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

599+ = case lookupCtxt n (idris_classes ist) of

600 [CI _ _ _ _ ins] -> ins

601 _ -> []

602 | otherwise = []

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

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

659-- else do

660 -- 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

662 [] -> []

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

664 ps <- get_probs

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

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

717 when autoSolve solveAll

718 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

720 [] -> do a <- envArgs fn

721 return (fn, a)

722 -- FIXME: resolve ambiguities

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

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

1201mkSpecialised i fc n args def

1202 = do let tm' = def

1203− case lookupCtxt Nothing n (idris_statics i) of

1203+ case lookupCtxt n (idris_statics i) of

1204 [] -> return tm'

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

1206 mkSpecDecl i n (zip args as) tm'

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

1227 cg = idris_callgraph i

1228

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

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

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

1231− else case lookupCtxt Nothing f cg of

1231+ else case lookupCtxt f cg of

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

1233 [] -> [f,f]

1234 _ -> []

src/Idris/IBC.hs+9−9

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

82 mkIBC is f'

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

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

87 _ -> fail "IBC write failed"

88ibc i (IBCStatic n) f

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

89+ = case lookupCtxt n (idris_statics i) of

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

91 _ -> fail "IBC write failed"

92ibc i (IBCClass n) f

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

93+ = case lookupCtxt n (idris_classes i) of

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

95 _ -> fail "IBC write failed"

96ibc i (IBCInstance int n ins) f

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

98ibc i (IBCDSL n) f

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

99+ = case lookupCtxt n (idris_dsls i) of

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

101 _ -> fail "IBC write failed"

102ibc i (IBCData n) f

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

103+ = case lookupCtxt n (idris_datatypes i) of

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

105 _ -> 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

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

108 _ -> fail "IBC write failed"

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

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

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

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

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

118 _ -> 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

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

121 _ -> 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

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

124 _ -> fail "IBC write failed"

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

881 return (dslify i $ PApp fc f args)

882 where

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

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

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

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

886 dslify i t = t

887

src/Idris/Prover.hs+1−1

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

26prover lit x =

27 do ctxt <- getContext

28 i <- getIState

29− case lookupTy Nothing x ctxt of

29+ case lookupTy x ctxt of

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

31 then prove ctxt lit x t

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

src/Idris/REPL.hs+15−15

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

129resolveProof n'

130 = do i <- getIState

131 ctxt <- getContext

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

132+ n <- case lookupNames n' ctxt of

133 [x] -> return x

134 [] -> return n'

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

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

207 = do ctxt <- getContext

208 ist <- getIState

209 imp <- impShow

210− case lookupTy Nothing n ctxt of

210+ case lookupTy n ctxt of

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

212 showImp imp (delab ist t)) ts

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

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

220 showImp imp (delab ist ty))

221

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

223− case lookupCtxtName Nothing n (idris_docstrings i) of

223+ case lookupCtxtName n (idris_docstrings i) of

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

225 ns -> mapM_ showDoc ns

226 where showDoc (n, d)

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

237 OK _ -> iputStrLn "Universes OK"

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

239 iputStrLn "Compiled patterns:\n"

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

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

241− case lookupCtxt Nothing n (idris_patdefs i) of

241+ case lookupCtxt n (idris_patdefs i) of

242 [] -> return ()

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

244 mapM_ (printCase i) d

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

255 _ -> return ()

256process fn (DebugInfo n)

257 = do i <- getIState

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

258+ let oi = lookupCtxtName n (idris_optimisation i)

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

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

260+ let si = lookupCtxt n (idris_statics i)

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

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

262+ let di = lookupCtxt n (idris_datatypes i)

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

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

264+ let d = lookupDef n (tt_ctxt i)

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

266 do print (head d)

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

267+ let cg = lookupCtxtName n (idris_callgraph i)

268 findUnusedArgs (map fst cg)

269 i <- getIState

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

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

271 sc <- checkSizeChange n

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

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

274 iputStrLn (show cg')

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

276− case lookupCtxt Nothing n (idris_classes i) of

276+ case lookupCtxt n (idris_classes i) of

277 [c] -> classInfo c

278 _ -> iputStrLn "Not a class"

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

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

330process fn (Prove n')

331 = do ctxt <- getContext

332 ist <- getIState

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

333+ n <- case lookupNames n' ctxt of

334 [x] -> return x

335 [] -> return n'

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

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

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

382

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

384− case lookupDef Nothing n (tt_ctxt i) of

384+ case lookupDef n (tt_ctxt i) of

385 [CaseOp _ _ _ _ _ args t _ _]

386 -> do tms <- genMissing n args t

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

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

431dumpInstance n = do i <- getIState

432 ctxt <- getContext

433 imp <- impShow

434− case lookupTy Nothing n ctxt of

434+ case lookupTy n ctxt of

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

436

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

src/Idris/UnusedArgs.hs+2−2

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

15traceUnused :: Name -> Idris ()

16traceUnused n

17 = do i <- getIState

18− case lookupCtxt Nothing n (idris_callgraph i) of

18+ case lookupCtxt n (idris_callgraph i) of

19 [CGInfo args calls scg usedns _] ->

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

21 let fargs = concatMap (getFargpos calls) argpos

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

39 | otherwise

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

41 i <- getIState

42− case lookupCtxt Nothing g (idris_callgraph i) of

42+ case lookupCtxt g (idris_callgraph i) of

43 [CGInfo args calls scg usedns unused] ->

44 if (j >= length args)

45 then -- overapplied, assume used