Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Remove the unused arg from lookup functions

Previously, there was an ignored argument to lookupCtxtName and its
derivatives. This has been removed to prevent confusion.
  • Loading branch information...
commit a807a34ac9f597456e9e2be42ba5693871cba1ff 1 parent 17b9f43
@david-christiansen david-christiansen authored
View
6 src/Core/Elaborate.hs
@@ -171,7 +171,7 @@ checkInjective (tm, l, r) = do ctxt <- get_context
if isInj ctxt tm then return ()
else lift $ tfail (NotInjective tm l r)
where isInj ctxt (P _ n _)
- | isConName Nothing n ctxt = True
+ | isConName n ctxt = True
isInj ctxt (App f a) = isInj ctxt f
isInj ctxt (Constant _) = True
isInj ctxt (TType _) = True
@@ -210,7 +210,7 @@ unique_hole' reusable n
uniqueNameCtxt :: Context -> Name -> [Name] -> Elab' aux Name
uniqueNameCtxt ctxt n hs
| n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs
- | [_] <- lookupTy Nothing n ctxt = uniqueNameCtxt ctxt (nextName n) hs
+ | [_] <- lookupTy n ctxt = uniqueNameCtxt ctxt (nextName n) hs
| otherwise = return n
elog :: String -> Elab' aux ()
@@ -356,7 +356,7 @@ prepare_apply fn imps =
mkClaims _ _ _ _
| Var n <- fn
= do ctxt <- get_context
- case lookupTy Nothing n ctxt of
+ case lookupTy n ctxt of
[] -> lift $ tfail $ NoSuchVariable n
_ -> fail $ "Too many arguments for " ++ show fn
| otherwise = fail $ "Too many arguments for " ++ show fn
View
64 src/Core/Evaluate.hs
@@ -149,7 +149,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
ev ntimes_in stk top env (P Ref n ty)
| not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
| (True, ntimes) <- usable simpl n ntimes_in
- = do let val = lookupDefAcc Nothing n atRepl ctxt
+ = do let val = lookupDefAcc n atRepl ctxt
case val of
[(Function _ tm, Public)] ->
ev ntimes (n:stk) True env tm
@@ -220,7 +220,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
_ -> return $ unload env f args
| (True, ntimes) <- usable simpl n ntimes_in
= traceWhen traceon (show stk) $
- do let val = lookupDefAcc Nothing n atRepl ctxt
+ do let val = lookupDefAcc n atRepl ctxt
case val of
[(CaseOp inl inr _ _ _ ns tree _ _, acc)]
| acc == Public -> -- unoptimised version
@@ -243,7 +243,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
apply ntimes stk top env f [] = return f
-- specApply stk env f@(VP Ref n ty) args
--- = case lookupCtxt Nothing n statics of
+-- = case lookupCtxt n statics of
-- [as] -> if or as
-- then trace (show (n, map fst (filter (\ (_, s) -> s) (zip args as)))) $
-- return $ unload env f args
@@ -397,7 +397,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where
ev :: [HNF] -> TT Name -> Eval HNF
ev env (P _ n ty)
| Just (Let t v) <- lookup n genv = ev env v
- ev env (P Ref n ty) = case lookupDef Nothing n ctxt of
+ ev env (P Ref n ty) = case lookupDef n ctxt of
[Function _ t] -> ev env t
[TyDecl nt ty] -> return $ HP nt n ty
[CaseOp inl _ _ _ _ [] tree _ _] ->
@@ -430,7 +430,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where
app <- apply env sc' as
wknH (-1) app
apply env (HP Ref n ty) args
- | [CaseOp _ _ _ _ _ ns tree _ _] <- lookupDef Nothing n ctxt
+ | [CaseOp _ _ _ _ _ ns tree _ _] <- lookupDef n ctxt
= do c <- evCase env ns args tree
case c of
(Nothing, _, env') -> return $ unload env' (HP Ref n ty) args
@@ -565,7 +565,7 @@ convEq ctxt = ceq [] where
caseeq ps (UnmatchedCase _) (UnmatchedCase _) = return True
caseeq ps _ _ = return False
- sameDefs ps x y = case (lookupDef Nothing x ctxt, lookupDef Nothing y ctxt) of
+ sameDefs ps x y = case (lookupDef x ctxt, lookupDef y ctxt) of
([Function _ xdef], [Function _ ydef])
-> ceq ((x,y):ps) xdef ydef
([CaseOp _ _ _ _ _ _ xdef _ _],
@@ -730,7 +730,7 @@ addCasedef :: Name -> Bool -> Bool -> Bool -> Bool ->
Type -> Context -> Context
addCasedef n alwaysInline tcase covering asserted ps_in ps psrt ty uctxt
= let ctxt = definitions uctxt
- access = case lookupDefAcc Nothing n False uctxt of
+ access = case lookupDefAcc n False uctxt of
[(_, acc)] -> acc
_ -> Public
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
simplifyCasedef :: Name -> Context -> Context
simplifyCasedef n uctxt
= let ctxt = definitions uctxt
- ctxt' = case lookupCtxt Nothing n ctxt of
+ ctxt' = case lookupCtxt n ctxt of
[(CaseOp inl inr ty [] ps args sc args' sc', acc, tot)] ->
ctxt -- nothing to simplify (or already done...)
[(CaseOp inl inr ty ps_in ps args sc args' sc', acc, tot)] ->
@@ -780,40 +780,40 @@ addOperator n ty a op uctxt
tfst (a, _, _) = a
-lookupNames :: Maybe [String] -> Name -> Context -> [Name]
-lookupNames root n ctxt
- = let ns = lookupCtxtName root n (definitions ctxt) in
+lookupNames :: Name -> Context -> [Name]
+lookupNames n ctxt
+ = let ns = lookupCtxtName n (definitions ctxt) in
map fst ns
-lookupTy :: Maybe [String] -> Name -> Context -> [Type]
-lookupTy root n ctxt
- = do def <- lookupCtxt root n (definitions ctxt)
+lookupTy :: Name -> Context -> [Type]
+lookupTy n ctxt
+ = do def <- lookupCtxt n (definitions ctxt)
case tfst def of
(Function ty _) -> return ty
(TyDecl _ ty) -> return ty
(Operator ty _ _) -> return ty
(CaseOp _ _ ty _ _ _ _ _ _) -> return ty
-isConName :: Maybe [String] -> Name -> Context -> Bool
-isConName root n ctxt
- = or $ do def <- lookupCtxt root n (definitions ctxt)
+isConName :: Name -> Context -> Bool
+isConName n ctxt
+ = or $ do def <- lookupCtxt n (definitions ctxt)
case tfst def of
(TyDecl (DCon _ _) _) -> return True
(TyDecl (TCon _ _) _) -> return True
_ -> return False
-isFnName :: Maybe [String] -> Name -> Context -> Bool
-isFnName root n ctxt
- = or $ do def <- lookupCtxt root n (definitions ctxt)
+isFnName :: Name -> Context -> Bool
+isFnName n ctxt
+ = or $ do def <- lookupCtxt n (definitions ctxt)
case tfst def of
(Function _ _) -> return True
(Operator _ _ _) -> return True
(CaseOp _ _ _ _ _ _ _ _ _) -> return True
_ -> return False
-lookupP :: Maybe [String] -> Name -> Context -> [Term]
-lookupP root n ctxt
- = do def <- lookupCtxt root n (definitions ctxt)
+lookupP :: Name -> Context -> [Term]
+lookupP n ctxt
+ = do def <- lookupCtxt n (definitions ctxt)
p <- case def of
(Function ty tm, a, _) -> return (P Ref n ty, a)
(TyDecl nt ty, a, _) -> return (P nt n ty, a)
@@ -823,22 +823,22 @@ lookupP root n ctxt
Hidden -> []
_ -> return (fst p)
-lookupDef :: Maybe [String] -> Name -> Context -> [Def]
-lookupDef root n ctxt = map tfst $ lookupCtxt root n (definitions ctxt)
+lookupDef :: Name -> Context -> [Def]
+lookupDef n ctxt = map tfst $ lookupCtxt n (definitions ctxt)
-lookupDefAcc :: Maybe [String] -> Name -> Bool -> Context ->
+lookupDefAcc :: Name -> Bool -> Context ->
[(Def, Accessibility)]
-lookupDefAcc root n mkpublic ctxt
- = map mkp $ lookupCtxt root n (definitions ctxt)
+lookupDefAcc n mkpublic ctxt
+ = map mkp $ lookupCtxt n (definitions ctxt)
where mkp (d, a, _) = if mkpublic then (d, Public) else (d, a)
lookupTotal :: Name -> Context -> [Totality]
-lookupTotal n ctxt = map mkt $ lookupCtxt Nothing n (definitions ctxt)
+lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)
where mkt (d, a, t) = t
-lookupVal :: Maybe [String] -> Name -> Context -> [Value]
-lookupVal root n ctxt
- = do def <- lookupCtxt root n (definitions ctxt)
+lookupVal :: Name -> Context -> [Value]
+lookupVal n ctxt
+ = do def <- lookupCtxt n (definitions ctxt)
case tfst def of
(Function _ htm) -> return (veval ctxt [] htm)
(TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))
View
2  src/Core/ProofShell.hs
@@ -41,7 +41,7 @@ processCommand (Eval t) state =
(state, show nf ++ " : " ++ show ty)
err -> (state, show err)
processCommand (Print n) state =
- case lookupDef Nothing n (ctxt state) of
+ case lookupDef n (ctxt state) of
[tm] -> (state, show tm)
_ -> (state, "No such name")
processCommand (Tac e) state
View
10 src/Core/TT.hs
@@ -244,8 +244,8 @@ addDef n v ctxt = case Map.lookup (nsroot n) ctxt of
-}
-lookupCtxtName :: Maybe [String] -> Name -> Ctxt a -> [(Name, a)]
-lookupCtxtName nspace n ctxt = case Map.lookup (nsroot n) ctxt of
+lookupCtxtName :: Name -> Ctxt a -> [(Name, a)]
+lookupCtxtName n ctxt = case Map.lookup (nsroot n) ctxt of
Just xs -> filterNS (Map.toList xs)
Nothing -> []
where
@@ -258,12 +258,12 @@ lookupCtxtName nspace n ctxt = case Map.lookup (nsroot n) ctxt of
nsmatch (NS _ _) _ = False
nsmatch looking found = True
-lookupCtxt :: Maybe [String] -> Name -> Ctxt a -> [a]
-lookupCtxt ns n ctxt = map snd (lookupCtxtName ns n ctxt)
+lookupCtxt :: Name -> Ctxt a -> [a]
+lookupCtxt n ctxt = map snd (lookupCtxtName n ctxt)
updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a
updateDef n f ctxt
- = let ds = lookupCtxtName Nothing n ctxt in
+ = let ds = lookupCtxtName n ctxt in
foldr (\ (n, t) c -> addDef n (f t) c) ctxt ds
toAlist :: Ctxt a -> [(Name, a)]
View
2  src/Core/Typecheck.hs
@@ -60,7 +60,7 @@ check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)
check' holes ctxt env top = chk env top where
chk env (Var n)
| Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)
- | (P nt n' ty : _) <- lookupP Nothing n ctxt = return (P nt n' ty, ty)
+ | (P nt n' ty : _) <- lookupP n ctxt = return (P nt n' ty, ty)
| otherwise = do lift $ tfail $ NoSuchVariable n
chk env (RApp f a)
= do (fv, fty) <- chk env f
View
6 src/IRTS/Compiler.hs
@@ -98,7 +98,7 @@ irMain tm = do i <- ir tm
allNames :: [Name] -> Name -> Idris [Name]
allNames ns n | n `elem` ns = return []
allNames ns n = do i <- getIState
- case lookupCtxt Nothing n (idris_callgraph i) of
+ case lookupCtxt n (idris_callgraph i) of
[ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
return (nub (n : concat more))
_ -> return [n]
@@ -205,12 +205,12 @@ instance ToIR (TT Name) where
Just tm -> return tm
_ -> do
let collapse
- = case lookupCtxt Nothing n
+ = case lookupCtxt n
(idris_optimisation i) of
[oi] -> collapsible oi
_ -> False
let unused
- = case lookupCtxt Nothing n
+ = case lookupCtxt n
(idris_callgraph i) of
[CGInfo _ _ _ _ unusedpos] ->
unusedpos
View
4 src/IRTS/Defunctionalise.hs
@@ -80,14 +80,14 @@ addApps defs (n, LFun _ _ args e)
-- aa env e@(LApp tc (MN 0 "EVAL") [a]) = e
aa env (LApp tc (LV (Glob n)) args)
= do args' <- mapM (aa env) args
- case lookupCtxt Nothing n defs of
+ case lookupCtxt n defs of
[LConstructor _ i ar] -> return $ DApp tc n args'
[LFun _ _ as _] -> let arity = length as in
fixApply tc n args' arity
[] -> return $ chainAPPLY (DV (Glob n)) args'
aa env (LLazyApp n args)
= do args' <- mapM (aa env) args
- case lookupCtxt Nothing n defs of
+ case lookupCtxt n defs of
[LConstructor _ i ar] -> return $ DApp False n args'
[LFun _ _ as _] -> let arity = length as in
fixLazyApply n args' arity
View
14 src/IRTS/Simplified.hs
@@ -46,7 +46,7 @@ simplify :: Bool -> DExp -> State (DDefs, Int) SExp
simplify tl (DV (Loc i)) = return (SV (Loc i))
simplify tl (DV (Glob x))
= do ctxt <- ldefs
- case lookupCtxt Nothing x ctxt of
+ case lookupCtxt x ctxt of
[DConstructor _ t 0] -> return $ SCon t x []
_ -> return $ SV (Glob x)
simplify tl (DApp tc n args) = do args' <- mapM sVar args
@@ -88,7 +88,7 @@ simplify tl (DError str) = return $ SError str
sVar (DV (Glob x))
= do ctxt <- ldefs
- case lookupCtxt Nothing x ctxt of
+ case lookupCtxt x ctxt of
[DConstructor _ t 0] -> sVar (DC t x [])
_ -> return (Glob x, Nothing)
sVar (DV x) = return (x, Nothing)
@@ -136,7 +136,7 @@ scopecheck ctxt envTop tm = sc envTop tm where
sc env (SV (Glob n)) =
case lookup n (reverse env) of -- most recent first
Just i -> do lvar i; return (SV (Loc i))
- Nothing -> case lookupCtxt Nothing n ctxt of
+ Nothing -> case lookupCtxt n ctxt of
[DConstructor _ i ar] ->
if True -- ar == 0
then return (SCon i n [])
@@ -146,7 +146,7 @@ scopecheck ctxt envTop tm = sc envTop tm where
[] -> fail $ "Codegen error: No such variable " ++ show n
sc env (SApp tc f args)
= do args' <- mapM (scVar env) args
- case lookupCtxt Nothing f ctxt of
+ case lookupCtxt f ctxt of
[DConstructor n tag ar] ->
if True -- (ar == length args)
then return $ SCon tag n args'
@@ -160,7 +160,7 @@ scopecheck ctxt envTop tm = sc envTop tm where
return $ SForeign l ty f args'
sc env (SCon tag f args)
= do args' <- mapM (scVar env) args
- case lookupCtxt Nothing f ctxt of
+ case lookupCtxt f ctxt of
[DConstructor n tag ar] ->
if True -- (ar == length args)
then return $ SCon tag n args'
@@ -197,7 +197,7 @@ scopecheck ctxt envTop tm = sc envTop tm where
scVar env (Glob n) =
case lookup n (reverse env) of -- most recent first
Just i -> do lvar i; return (Loc i)
- Nothing -> case lookupCtxt Nothing n ctxt of
+ Nothing -> case lookupCtxt n ctxt of
[DConstructor _ i ar] ->
fail $ "Codegen error : can't pass constructor here"
[_] -> return (Glob n)
@@ -207,7 +207,7 @@ scopecheck ctxt envTop tm = sc envTop tm where
scalt env (SConCase _ i n args e)
= do let env' = env ++ zip args [length env..]
- tag <- case lookupCtxt Nothing n ctxt of
+ tag <- case lookupCtxt n ctxt of
[DConstructor _ i ar] ->
if True -- (length args == ar)
then return i
View
24 src/Idris/AbsSyntax.hs
@@ -88,7 +88,7 @@ getCoercionsTo i ty =
findCoercions fn cs
where findCoercions t [] = []
findCoercions t (n : ns) =
- let ps = case lookupTy Nothing n (tt_ctxt i) of
+ let ps = case lookupTy n (tt_ctxt i) of
[ty] -> case unApply (getRetTy ty) of
(t', _) ->
if t == t' then [n] else []
@@ -119,7 +119,7 @@ addToCalledG n ns = return () -- TODO
addInstance :: Bool -> Name -> Name -> Idris ()
addInstance int n i
= do ist <- getIState
- case lookupCtxt Nothing n (idris_classes ist) of
+ case lookupCtxt n (idris_classes ist) of
[CI a b c d ins] ->
do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
putIState $ ist { idris_classes = cs }
@@ -139,7 +139,7 @@ addInstance int n i
addClass :: Name -> ClassInfo -> Idris ()
addClass n i
= do ist <- getIState
- let i' = case lookupCtxt Nothing n (idris_classes ist) of
+ let i' = case lookupCtxt n (idris_classes ist) of
[c] -> c { class_instances = class_instances i }
_ -> i
putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
@@ -193,7 +193,7 @@ getName = do i <- getIState;
checkUndefined :: FC -> Name -> Idris ()
checkUndefined fc n
= do i <- getContext
- case lookupTy Nothing n i of
+ case lookupTy n i of
(_:_) -> fail $ show fc ++ ":" ++
show n ++ " already defined"
_ -> return ()
@@ -201,7 +201,7 @@ checkUndefined fc n
isUndefined :: FC -> Name -> Idris Bool
isUndefined fc n
= do i <- getContext
- case lookupTy Nothing n i of
+ case lookupTy n i of
(_:_) -> return False
_ -> return True
@@ -641,7 +641,7 @@ getPriority :: IState -> PTerm -> Int
getPriority i tm = 1 -- pri tm
where
pri (PRef _ n) =
- case lookupP Nothing n (tt_ctxt i) of
+ case lookupP n (tt_ctxt i) of
((P (DCon _ _) _ _):_) -> 1
((P (TCon _ _) _ _):_) -> 1
((P Ref _ _):_) -> 1
@@ -882,9 +882,9 @@ addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm
aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
aiFn inpat True ist fc f []
- = case lookupDef Nothing f (tt_ctxt ist) of
+ = case lookupDef f (tt_ctxt ist) of
[] -> Right $ PPatvar fc f
- alts -> let ialts = lookupCtxt Nothing f (idris_implicits ist) in
+ alts -> let ialts = lookupCtxt f (idris_implicits ist) in
-- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
if (not (vname f) || tcname f
|| any constructor alts || any allImp ialts)
@@ -904,7 +904,7 @@ aiFn inpat expat ist fc f as
| f `elem` primNames = Right $ PApp fc (PRef fc f) as
aiFn inpat expat ist fc f as
-- This is where namespaces get resolved by adding PAlternative
- = case lookupCtxtName Nothing f (idris_implicits ist) of
+ = case lookupCtxtName f (idris_implicits ist) of
[(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
[] -> if f `elem` idris_metavars ist
then Right $ PApp fc (PRef fc f) as
@@ -949,7 +949,7 @@ stripLinear :: IState -> PTerm -> PTerm
stripLinear i tm = evalState (sl tm) [] where
sl :: PTerm -> State [Name] PTerm
sl (PRef fc f)
- | (_:_) <- lookupTy Nothing f (tt_ctxt i)
+ | (_:_) <- lookupTy f (tt_ctxt i)
= return $ PRef fc f
| otherwise = do ns <- get
if (f `elem` ns)
@@ -1077,11 +1077,11 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
match (PApp _ x []) (PRef f n) = match x (PRef f n)
match (PRef _ n) tm@(PRef _ n')
| n == n' && not names &&
- (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
+ (not (isConName n (tt_ctxt i)) || tm == Placeholder)
= return [(n, tm)]
| n == n' = return []
match (PRef _ n) tm
- | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
+ | not names && (not (isConName n (tt_ctxt i)) || tm == Placeholder)
= return [(n, tm)]
match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
mr <- match' r r'
View
4 src/Idris/AbsSyntaxTree.hs
@@ -1128,7 +1128,7 @@ namesIn uvars ist tm = nub $ ni [] tm
where
ni env (PRef _ n)
| not (n `elem` env)
- = case lookupTy Nothing n (tt_ctxt ist) of
+ = case lookupTy n (tt_ctxt ist) of
[] -> [n]
_ -> if n `elem` (map fst uvars) then [n] else []
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
where
ni env (PRef _ n)
| n `elem` vars && not (n `elem` env)
- = case lookupTy Nothing n (tt_ctxt ist) of
+ = case lookupTy n (tt_ctxt ist) of
[] -> [n]
_ -> []
ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
View
50 src/Idris/Coverage.hs
@@ -38,7 +38,7 @@ mkPatTm t = do i <- getIState
evalStateT (toTT timp) 0
where
toTT (PRef _ n) = do i <- lift getIState
- case lookupDef Nothing n (tt_ctxt i) of
+ case lookupDef n (tt_ctxt i) of
[TyDecl nt _] -> return $ P nt n Erased
_ -> return $ P Ref n Erased
toTT (PApp _ t args) = do t' <- toTT t
@@ -107,9 +107,9 @@ expandAlts :: IState -> [CaseAlt] -> SC -> Idris [CaseAlt]
expandAlts i all@(ConstCase c _ : alts) def
= return $ all ++ [DefaultCase def]
expandAlts i all@(ConCase n _ _ _ : alts) def
- | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)
+ | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)
= do let tyn = getTy n (tt_ctxt i)
- case lookupCtxt Nothing tyn (idris_datatypes i) of
+ case lookupCtxt tyn (idris_datatypes i) of
(TI ns _ _: _) -> do let ps = map mkPat ns
return $ addAlts ps (altsFor all) all
_ -> return all
@@ -127,13 +127,13 @@ expandAlts i all@(ConCase n _ _ _ : alts) def
argList i = take i (map (\x -> (MN x "ign")) [0..])
getTy n ctxt
- = case lookupTy Nothing n ctxt of
+ = case lookupTy n ctxt of
(t : _) -> case unApply (getRetTy t) of
(P _ tyn _, _) -> tyn
x -> error $ "Can't happen getTy 1 " ++ show (n, x)
_ -> error "Can't happen getTy 2"
- mkPat x = case lookupCtxt Nothing x (idris_implicits i) of
+ mkPat x = case lookupCtxt x (idris_implicits i) of
(pargs : _)
-> (x, length pargs)
_ -> error "Can't happen - genAll"
@@ -160,7 +160,7 @@ genClauses fc n xs given
logLvl 10 $ show argss ++ "\n" ++ show all_args
logLvl 10 $ "Original: \n" ++
showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)
- let parg = case lookupCtxt Nothing n (idris_implicits i) of
+ let parg = case lookupCtxt n (idris_implicits i) of
(p : _) -> p
_ -> repeat (pexp Placeholder)
let tryclauses = mkClauses parg all_args
@@ -217,8 +217,8 @@ genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of
[] -> [Placeholder]
xs -> nub xs
where
- conForm (PApp _ (PRef fc n) _) = isConName Nothing n (tt_ctxt i)
- conForm (PRef fc n) = isConName Nothing n (tt_ctxt i)
+ conForm (PApp _ (PRef fc n) _) = isConName n (tt_ctxt i)
+ conForm (PRef fc n) = isConName n (tt_ctxt i)
conForm _ = False
otherPats :: PTerm -> [PTerm]
@@ -227,22 +227,22 @@ genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of
otherPats arg = return Placeholder
ops fc n xs o
- | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)
+ | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)
= do xs' <- mapM otherPats (map getTm xs)
let p = PApp fc (PRef fc n) (zipWith upd xs' xs)
let tyn = getTy n (tt_ctxt i)
- case lookupCtxt Nothing tyn (idris_datatypes i) of
+ case lookupCtxt tyn (idris_datatypes i) of
(TI ns _ _ : _) -> p : map (mkPat fc) (ns \\ [n])
_ -> [p]
ops fc n arg o = return Placeholder
- getTy n ctxt = case lookupTy Nothing n ctxt of
+ getTy n ctxt = case lookupTy n ctxt of
(t : _) -> case unApply (getRetTy t) of
(P _ tyn _, _) -> tyn
x -> error $ "Can't happen getTy 1 " ++ show (n, x)
_ -> error "Can't happen getTy 2"
- mkPat fc x = case lookupCtxt Nothing x (idris_implicits i) of
+ mkPat fc x = case lookupCtxt x (idris_implicits i) of
(pargs : _)
-> PApp fc (PRef fc x) (map (upd Placeholder) pargs)
_ -> error "Can't happen - genAll"
@@ -306,7 +306,7 @@ calcProd i fc n pats = do patsprod <- mapM prodRec pats
cotype ty
| (P _ t _, _) <- unApply (getRetTy ty)
- = case lookupCtxt Nothing t (idris_datatypes i) of
+ = case lookupCtxt t (idris_datatypes i) of
[TI _ True _] -> True
_ -> False
| otherwise = False
@@ -315,7 +315,7 @@ calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)]
-> Idris Totality
calcTotality path fc n pats
= do i <- getIState
- let opts = case lookupCtxt Nothing n (idris_flags i) of
+ let opts = case lookupCtxt n (idris_flags i) of
[fs] -> fs
_ -> []
case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
@@ -339,12 +339,12 @@ checkTotality path fc n
updateContext (simplifyCasedef n)
ctxt <- getContext
i <- getIState
- let opts = case lookupCtxt Nothing n (idris_flags i) of
+ let opts = case lookupCtxt n (idris_flags i) of
[fs] -> fs
_ -> []
t' <- case t of
Unchecked ->
- case lookupDef Nothing n ctxt of
+ case lookupDef n ctxt of
[CaseOp _ _ _ _ pats _ _ _ _] ->
do t' <- if AssertTotal `elem` opts
then return $ Total []
@@ -378,7 +378,7 @@ checkTotality path fc n
warnPartial n t
= do i <- getIState
- case lookupDef Nothing n (tt_ctxt i) of
+ case lookupDef n (tt_ctxt i) of
[x] -> do
iputStrLn $ show fc ++ ":Warning - " ++ show n ++ " is " ++ show t
-- ++ "\n" ++ show x
@@ -407,8 +407,8 @@ checkDeclTotality (fc, n)
buildSCG :: (FC, Name) -> Idris ()
buildSCG (_, n) = do
ist <- getIState
- case lookupCtxt Nothing n (idris_callgraph ist) of
- [cg] -> case lookupDef Nothing n (tt_ctxt ist) of
+ case lookupCtxt n (idris_callgraph ist) of
+ [cg] -> case lookupDef n (tt_ctxt ist) of
[CaseOp _ _ _ _ _ args sc _ _] ->
do logLvl 3 $ "Building SCG for " ++ show n ++ " from\n"
++ show sc
@@ -442,7 +442,7 @@ buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $
-- how the arguments relate - either Smaller or Unknown
argRels :: Name -> [(Name, SizeChange)]
argRels n = let ctxt = tt_ctxt ist
- [ty] = lookupTy Nothing n ctxt -- must exist!
+ [ty] = lookupTy n ctxt -- must exist!
P _ nty _ = fst (unApply (getRetTy ty))
args = map snd (getArgTys ty) in
map (getRel nty) (map (fst . unApply . getRetTy) args)
@@ -503,7 +503,7 @@ buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $
checkSizeChange :: Name -> Idris Totality
checkSizeChange n = do
ist <- getIState
- case lookupCtxt Nothing n (idris_callgraph ist) of
+ case lookupCtxt n (idris_callgraph ist) of
[cg] -> do let ms = mkMultiPaths ist [] (scg cg)
logLvl 5 ("Multipath for " ++ show n ++ ":\n" ++
"from " ++ show (scg cg) ++ "\n" ++
@@ -530,7 +530,7 @@ mkMultiPaths ist path cg
where extend (nextf, args)
| (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]
| [Unchecked] <- lookupTotal nextf (tt_ctxt ist)
- = case lookupCtxt Nothing nextf (idris_callgraph ist) of
+ = case lookupCtxt nextf (idris_callgraph ist) of
[ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
_ -> [ reverse ((nextf, args) : path) ]
| otherwise = [ reverse ((nextf, args) : path) ]
@@ -538,7 +538,7 @@ mkMultiPaths ist path cg
-- do (nextf, args) <- cg
-- if ((nextf, args) `elem` path)
-- then return (reverse ((nextf, args) : path))
--- else case lookupCtxt Nothing nextf (idris_callgraph ist) of
+-- else case lookupCtxt nextf (idris_callgraph ist) of
-- [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
-- _ -> return (reverse ((nextf, args) : path))
@@ -562,12 +562,12 @@ checkMP ist i mp = if i > 0
-- = Partial BelieveMe
-- if we get to a constructor, it's fine as long as it's strictly positive
tryPath desc path ((f, _) :es) arg
- | [TyDecl (DCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)
+ | [TyDecl (DCon _ _) _] <- lookupDef f (tt_ctxt ist)
= case lookupTotal f (tt_ctxt ist) of
[Total _] -> Unchecked -- okay so far
[Partial _] -> Partial (Other [f])
x -> error (show x)
- | [TyDecl (TCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)
+ | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
= Total []
tryPath desc path (e@(f, args) : es) arg
| e `elem` es && allNothing args = Partial (Mutual [f])
View
16 src/Idris/DataOpts.hs
@@ -17,7 +17,7 @@ import Debug.Trace
forceArgs :: Name -> Type -> Idris ()
forceArgs n t = do i <- getIState
let fargs = force i 0 t
- copt <- case lookupCtxt Nothing n (idris_optimisation i) of
+ copt <- case lookupCtxt n (idris_optimisation i) of
[] -> return $ Optimise False [] []
(op:_) -> return op
let opts = addDef n (copt { forceable = fargs }) (idris_optimisation i)
@@ -38,7 +38,7 @@ forceArgs n t = do i <- getIState
collapsibleIn i t
| (P _ tn _, _) <- unApply t
- = case lookupCtxt Nothing tn (idris_optimisation i) of
+ = case lookupCtxt tn (idris_optimisation i) of
[oi] -> collapsible oi
_ -> False
| otherwise = False
@@ -68,7 +68,7 @@ collapseCons ty cons =
setCollapsible n
= do i <- getIState
iLOG $ show n ++ " collapsible"
- case lookupCtxt Nothing n (idris_optimisation i) of
+ case lookupCtxt n (idris_optimisation i) of
(oi:_) -> do let oi' = oi { collapsible = True }
let opts = addDef n oi' (idris_optimisation i)
putIState (i { idris_optimisation = opts })
@@ -79,7 +79,7 @@ collapseCons ty cons =
forceRec :: IState -> (Name, [Type]) -> Idris Bool
forceRec i (n, ts)
- = case lookupCtxt Nothing n (idris_optimisation i) of
+ = case lookupCtxt n (idris_optimisation i) of
(oi:_) -> checkFR (forceable oi) 0 ts
_ -> return False
checkFR fs i [] = return True
@@ -161,7 +161,7 @@ instance Optimisable Raw where
| (Var n, args) <- raw_unapply t -- MAGIC HERE
= do args' <- mapM applyOpts args
i <- getIState
- case lookupCtxt Nothing n (idris_optimisation i) of
+ case lookupCtxt n (idris_optimisation i) of
(oi:_) -> return $ applyDataOpt oi n args'
_ -> return (raw_apply (Var n) args')
| otherwise = do f' <- applyOpts f
@@ -202,14 +202,14 @@ applyDataOpt oi n args
instance Optimisable (TT Name) where
applyOpts c@(P (DCon t arity) n _)
= do i <- getIState
- case lookupCtxt Nothing n (idris_optimisation i) of
+ case lookupCtxt n (idris_optimisation i) of
(oi:_) -> return $ applyDataOptRT oi n t arity []
_ -> return c
applyOpts t@(App f a)
| (c@(P (DCon t arity) n _), args) <- unApply t -- MAGIC HERE
= do args' <- mapM applyOpts args
i <- getIState
- case lookupCtxt Nothing n (idris_optimisation i) of
+ case lookupCtxt n (idris_optimisation i) of
(oi:_) -> do return $ applyDataOptRT oi n t arity args'
_ -> return (mkApp c args')
| otherwise = do f' <- applyOpts f
@@ -224,7 +224,7 @@ instance Optimisable (TT Name) where
stripCollapsed (Bind n (PVar x) t) | (P _ ty _, _) <- unApply x
= do i <- getIState
- case lookupCtxt Nothing ty (idris_optimisation i) of
+ case lookupCtxt ty (idris_optimisation i) of
[oi] -> if collapsible oi
then do t' <- stripCollapsed t
return (Bind n (PVar x) (instantiate Erased t'))
View
4 src/Idris/Delaborate.hs
@@ -41,7 +41,7 @@ delab' ist tm fullname = de [] tm
de env (TType i) = PType
dens x | fullname = x
- dens ns@(NS n _) = case lookupCtxt Nothing n (idris_implicits ist) of
+ dens ns@(NS n _) = case lookupCtxt n (idris_implicits ist) of
[_] -> n -- just one thing
_ -> ns
dens n = n
@@ -62,7 +62,7 @@ delab' ist tm fullname = de [] tm
deFn env f args = PApp un (de env f) (map pexp (map (de env) args))
mkPApp n args
- | [imps] <- lookupCtxt Nothing n (idris_implicits ist)
+ | [imps] <- lookupCtxt n (idris_implicits ist)
= PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)
| otherwise = PApp un (PRef un n) (map pexp args)
View
12 src/Idris/Docs.hs
@@ -65,9 +65,9 @@ instance Show Doc where
getDocs :: Name -> Idris Doc
getDocs n
= do i <- getIState
- case lookupCtxt Nothing n (idris_classes i) of
+ case lookupCtxt n (idris_classes i) of
[ci] -> docClass n ci
- _ -> case lookupCtxt Nothing n (idris_datatypes i) of
+ _ -> case lookupCtxt n (idris_datatypes i) of
[ti] -> docData n ti
_ -> do fd <- docFun n
return (FunDoc fd)
@@ -81,7 +81,7 @@ docData n ti
docClass :: Name -> ClassInfo -> Idris Doc
docClass n ci
= do i <- getIState
- let docstr = case lookupCtxt Nothing n (idris_docstrings i) of
+ let docstr = case lookupCtxt n (idris_docstrings i) of
[str] -> str
_ -> ""
mdocs <- mapM docFun (map fst (class_methods ci))
@@ -90,13 +90,13 @@ docClass n ci
docFun :: Name -> Idris FunDoc
docFun n
= do i <- getIState
- let docstr = case lookupCtxt Nothing n (idris_docstrings i) of
+ let docstr = case lookupCtxt n (idris_docstrings i) of
[str] -> str
_ -> ""
- let ty = case lookupTy Nothing n (tt_ctxt i) of
+ let ty = case lookupTy n (tt_ctxt i) of
(t : _) -> t
let argnames = map fst (getArgTys ty)
- let args = case lookupCtxt Nothing n (idris_implicits i) of
+ let args = case lookupCtxt n (idris_implicits i) of
[args] -> zip argnames args
_ -> []
let infixes = idris_infixes i
View
38 src/Idris/ElabDecls.hs
@@ -69,7 +69,7 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in
let nty' = normalise ctxt [] nty
let (t, _) = unApply (getRetTy nty')
let corec = case t of
- P _ rcty _ -> case lookupCtxt Nothing rcty (idris_datatypes i) of
+ P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of
[TI _ True _] -> True
_ -> False
_ -> False
@@ -93,14 +93,14 @@ elabPostulate info syn doc fc opts n ty
-- make sure it's collapsible, so it is never needed at run time
-- start by getting the elaborated type
ctxt <- getContext
- fty <- case lookupTy Nothing n ctxt of
+ fty <- case lookupTy n ctxt of
[] -> tclift $ tfail $ (At fc (NoTypeDecl n)) -- can't happen!
[ty] -> return ty
ist <- getIState
let (ap, _) = unApply (getRetTy (normalise ctxt [] fty))
logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)
let postOK = case ap of
- P _ tn _ -> case lookupCtxt Nothing tn
+ P _ tn _ -> case lookupCtxt tn
(idris_optimisation ist) of
[oi] -> collapsible oi
_ -> False
@@ -219,10 +219,10 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
= do elabData info syn doc fc False (PDatadecl tyn ty [(cdoc, cn, cty, fc)])
cty' <- implicit syn cn cty
i <- getIState
- cty <- case lookupTy Nothing cn (tt_ctxt i) of
+ cty <- case lookupTy cn (tt_ctxt i) of
[t] -> return (delab i t)
_ -> fail "Something went inexplicably wrong"
- cimp <- case lookupCtxt Nothing cn (idris_implicits i) of
+ cimp <- case lookupCtxt cn (idris_implicits i) of
[imps] -> return imps
let ptys = getProjs [] (renameBs cimp cty)
let ptys_u = getProjs [] cty
@@ -363,7 +363,7 @@ elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
elabClauses info fc opts n_in cs = let n = liftname info n_in in
do ctxt <- getContext
-- Check n actually exists, with no definition yet
- let tys = lookupTy Nothing n ctxt
+ let tys = lookupTy n ctxt
checkUndefined n ctxt
unless (length tys > 1) $ do
fty <- case tys of
@@ -380,7 +380,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)
-- FIXME: Really ought to only do this for total functions!
let doNothing = case ap of
- P _ tn _ -> case lookupCtxt Nothing tn
+ P _ tn _ -> case lookupCtxt tn
(idris_optimisation ist) of
[oi] -> collapsible oi
_ -> False
@@ -388,7 +388,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
solveDeferred n
ist <- getIState
when doNothing $
- case lookupCtxt Nothing n (idris_optimisation ist) of
+ case lookupCtxt n (idris_optimisation ist) of
[oi] -> do let opts = addDef n (oi { collapsible = True })
(idris_optimisation ist)
putIState (ist { idris_optimisation = opts })
@@ -460,7 +460,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
ctxt <- getContext
ist <- getIState
putIState (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) })
- case lookupTy (namespace info) n ctxt of
+ case lookupTy n ctxt of
[ty] -> do updateContext (addCasedef n (inlinable opts)
tcase knowncovering
(AssertTotal `elem` opts)
@@ -471,7 +471,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
totcheck (fc, n)
when (tot /= Unchecked) $ addIBC (IBCTotal n tot)
i <- getIState
- case lookupDef Nothing n (tt_ctxt i) of
+ case lookupDef n (tt_ctxt i) of
(CaseOp _ _ _ _ _ scargs sc scargs' sc' : _) ->
do let calls = findCalls sc' scargs'
let used = findUsedArgs sc' scargs'
@@ -487,7 +487,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
[] -> return ()
return ()
where
- checkUndefined n ctxt = case lookupDef Nothing n ctxt of
+ checkUndefined n ctxt = case lookupDef n ctxt of
[] -> return ()
[TyDecl _ _] -> return ()
_ -> tclift $ tfail (At fc (AlreadyDefined n))
@@ -572,10 +572,10 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
-- pattern bindings
i <- getIState
-- get the parameters first, to pass through to any where block
- let fn_ty = case lookupTy Nothing fname (tt_ctxt i) of
+ let fn_ty = case lookupTy fname (tt_ctxt i) of
[t] -> t
_ -> error "Can't happen (elabClause function type)"
- let fn_is = case lookupCtxt Nothing fname (idris_implicits i) of
+ let fn_is = case lookupCtxt fname (idris_implicits i) of
[t] -> t
_ -> []
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)
= getParamsInType i (n : env) is (instantiate (P Bound n t) sc)
getParamsInType i env is tm@(App f a)
| (P _ tn _, args) <- unApply tm
- = case lookupCtxt Nothing tn (idris_datatypes i) of
+ = case lookupCtxt tn (idris_datatypes i) of
[t] -> nub $ paramNames args env (param_pos t) ++
getParamsInType i env is f ++
getParamsInType i env is a
@@ -955,7 +955,7 @@ elabClass info syn doc fc constraints tn ps ds
let conn = case con of
PRef _ n -> n
PApp _ (PRef _ n) _ -> n
- let conn' = case lookupCtxtName Nothing conn (idris_classes i) of
+ let conn' = case lookupCtxtName conn (idris_classes i) of
[(n, _)] -> n
_ -> conn
addInstance False conn' cfn
@@ -1016,7 +1016,7 @@ elabInstance :: ElabInfo -> SyntaxInfo ->
[PDecl] -> Idris ()
elabInstance info syn fc cs n ps t expn ds
= do i <- getIState
- (n, ci) <- case lookupCtxtName (namespace info) n (idris_classes i) of
+ (n, ci) <- case lookupCtxtName n (idris_classes i) of
[c] -> return c
_ -> fail $ show fc ++ ":" ++ show n ++ " is not a type class"
let constraint = PApp fc (PRef fc n) (map pexp ps)
@@ -1076,7 +1076,7 @@ elabInstance info syn fc cs n ps t expn ds
checkNotOverlapping i t n
| take 2 (show n) == "@@" = return ()
| otherwise
- = case lookupTy Nothing n (tt_ctxt i) of
+ = case lookupTy n (tt_ctxt i) of
[t'] -> let tret = getRetType t
tret' = getRetType (delab i t') in
case matchClause i tret' tret of
@@ -1113,7 +1113,7 @@ elabInstance info syn fc cs n ps t expn ds
| PRef _ n <- getTm p
= do ps' <- getWParams ps
ctxt <- getContext
- case lookupP Nothing n ctxt of
+ case lookupP n ctxt of
[] -> return (pimp n (PRef fc n) : ps')
_ -> return ps'
getWParams (_ : ps) = getWParams ps
@@ -1248,7 +1248,7 @@ elabDecl' what info d@(PClauses f o n ps)
| what /= ETypes
= do iLOG $ "Elaborating clause " ++ show n
i <- getIState -- get the type options too
- let o' = case lookupCtxt Nothing n (idris_flags i) of
+ let o' = case lookupCtxt n (idris_flags i) of
[fs] -> fs
[] -> []
elabClauses info f (o ++ o') n ps
View
26 src/Idris/ElabTerm.hs
@@ -211,7 +211,7 @@ elab ist info pattern tcgen fn tm
elab' ina (PPatvar fc n) | pattern = patvar n
elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)
= do ctxt <- get_context
- let defined = case lookupTy Nothing n ctxt of
+ let defined = case lookupTy n ctxt of
[] -> False
_ -> True
-- this is to stop us resolve type classes recursively
@@ -221,7 +221,7 @@ elab ist info pattern tcgen fn tm
then do apply (Var n) []; solve
else try (do apply (Var n) []; solve)
(patvar n)
- where inparamBlock n = case lookupCtxtName Nothing n (inblock info) of
+ where inparamBlock n = case lookupCtxtName n (inblock info) of
[] -> False
_ -> True
elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])
@@ -334,7 +334,7 @@ elab ist info pattern tcgen fn tm
elab' (ina, g) tm@(PApp fc (PRef _ f) args')
= do let args = {- case lookupCtxt f (inblock info) of
Just ps -> (map (pexp . (PRef fc)) ps ++ args')
- _ ->-} args'
+ _ -> -} args'
-- newtm <- mkSpecialised ist fc f (map getTm args') tm
env <- get_env
if (f `elem` map fst env && length args' == 1)
@@ -350,11 +350,11 @@ elab ist info pattern tcgen fn tm
let isinf = f == inferCon || tcname f
-- if f is a type class, we need to know its arguments so that
-- we can unify with them
- case lookupCtxt Nothing f (idris_classes ist) of
+ case lookupCtxt f (idris_classes ist) of
[] -> return ()
_ -> mapM_ setInjective (map getTm args')
ctxt <- get_context
- let guarded = isConName Nothing f ctxt
+ let guarded = isConName f ctxt
ns <- apply (Var f) (map isph args)
ptm <- get_term
g <- goal
@@ -547,7 +547,7 @@ pruneAlt xs = map prune xs
pruneByType :: Term -> Context -> [PTerm] -> [PTerm]
pruneByType (P _ n _) c as
-- if the goal type is polymorphic, keep e
- | [] <- lookupTy Nothing n c = as
+ | [] <- lookupTy n c = as
| otherwise
= let asV = filter (headIs True n) as
as' = filter (headIs False n) as in
@@ -563,7 +563,7 @@ pruneByType (P _ n _) c as
headIs _ _ _ = True -- keep if it's not an application
typeHead var f f'
- = case lookupTy Nothing f' c of
+ = case lookupTy f' c of
[ty] -> let ty' = normalise c [] ty in
case unApply (getRetTy ty') of
(P _ ftyn _, _) -> ftyn == f
@@ -596,7 +596,7 @@ trivial ist = try' (do elab ist toplevel False False (MN 0 "tac")
findInstances :: IState -> Term -> [Name]
findInstances ist t
| (P _ n _, _) <- unApply t
- = case lookupCtxt Nothing n (idris_classes ist) of
+ = case lookupCtxt n (idris_classes ist) of
[CI _ _ _ _ ins] -> ins
_ -> []
| otherwise = []
@@ -658,7 +658,7 @@ resolveTC depth fn ist
-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist
-- else do
-- if there's a hole in the goal, don't even try
- let imps = case lookupCtxtName Nothing n (idris_implicits ist) of
+ let imps = case lookupCtxtName n (idris_implicits ist) of
[] -> []
[args] -> map isImp (snd args) -- won't be overloaded!
ps <- get_probs
@@ -716,7 +716,7 @@ runTac autoSolve ist tac = do env <- get_env
runT (Exact tm) = do elab ist toplevel False False (MN 0 "tac") tm
when autoSolve solveAll
runT (Refine fn [])
- = do (fn', imps) <- case lookupCtxtName Nothing fn (idris_implicits ist) of
+ = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of
[] -> do a <- envArgs fn
return (fn, a)
-- FIXME: resolve ambiguities
@@ -1200,7 +1200,7 @@ solveAll = try (do solve; solveAll) (return ())
mkSpecialised :: IState -> FC -> Name -> [PTerm] -> PTerm -> ElabD PTerm
mkSpecialised i fc n args def
= do let tm' = def
- case lookupCtxt Nothing n (idris_statics i) of
+ case lookupCtxt n (idris_statics i) of
[] -> return tm'
[as] -> if (not (or as)) then return tm' else
mkSpecDecl i n (zip args as) tm'
@@ -1227,8 +1227,8 @@ mkSpecDecl i n pargs tm'
cg = idris_callgraph i
staticFnNames tm | (P _ f _, as) <- unApply tm
- = if not (isFnName Nothing f ctxt) then []
- else case lookupCtxt Nothing f cg of
+ = if not (isFnName f ctxt) then []
+ else case lookupCtxt f cg of
[ns] -> f : f : [] --(ns \\ [f])
[] -> [f,f]
_ -> []
View
18 src/Idris/IBC.hs
@@ -82,28 +82,28 @@ mkIBC (i:is) f = do ist <- getIState
mkIBC is f'
ibc i (IBCFix d) f = return f { ibc_fixes = d : ibc_fixes f }
-ibc i (IBCImp n) f = case lookupCtxt Nothing n (idris_implicits i) of
+ibc i (IBCImp n) f = case lookupCtxt n (idris_implicits i) of
[v] -> return f { ibc_implicits = (n,v): ibc_implicits f }
_ -> fail "IBC write failed"
ibc i (IBCStatic n) f
- = case lookupCtxt Nothing n (idris_statics i) of
+ = case lookupCtxt n (idris_statics i) of
[v] -> return f { ibc_statics = (n,v): ibc_statics f }
_ -> fail "IBC write failed"
ibc i (IBCClass n) f
- = case lookupCtxt Nothing n (idris_classes i) of
+ = case lookupCtxt n (idris_classes i) of
[v] -> return f { ibc_classes = (n,v): ibc_classes f }
_ -> fail "IBC write failed"
ibc i (IBCInstance int n ins) f
= return f { ibc_instances = (int,n,ins): ibc_instances f }
ibc i (IBCDSL n) f
- = case lookupCtxt Nothing n (idris_dsls i) of
+ = case lookupCtxt n (idris_dsls i) of
[v] -> return f { ibc_dsls = (n,v): ibc_dsls f }
_ -> fail "IBC write failed"
ibc i (IBCData n) f
- = case lookupCtxt Nothing n (idris_datatypes i) of
+ = case lookupCtxt n (idris_datatypes i) of
[v] -> return f { ibc_datatypes = (n,v): ibc_datatypes f }
_ -> fail "IBC write failed"
-ibc i (IBCOpt n) f = case lookupCtxt Nothing n (idris_optimisation i) of
+ibc i (IBCOpt n) f = case lookupCtxt n (idris_optimisation i) of
[v] -> return f { ibc_optimise = (n,v): ibc_optimise f }
_ -> fail "IBC write failed"
ibc 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 }
ibc i (IBCLib n) f = return f { ibc_libs = n : ibc_libs f }
ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }
ibc i (IBCHeader n) f = return f { ibc_hdrs = n : ibc_hdrs f }
-ibc i (IBCDef n) f = case lookupDef Nothing n (tt_ctxt i) of
+ibc i (IBCDef n) f = case lookupDef n (tt_ctxt i) of
[v] -> return f { ibc_defs = (n,v) : ibc_defs f }
_ -> fail "IBC write failed"
-ibc i (IBCDoc n) f = case lookupCtxt Nothing n (idris_docstrings i) of
+ibc i (IBCDoc n) f = case lookupCtxt n (idris_docstrings i) of
[v] -> return f { ibc_docstrings = (n,v) : ibc_docstrings f }
_ -> fail "IBC write failed"
-ibc i (IBCCG n) f = case lookupCtxt Nothing n (idris_callgraph i) of
+ibc i (IBCCG n) f = case lookupCtxt n (idris_callgraph i) of
[v] -> return f { ibc_cg = (n,v) : ibc_cg f }
_ -> fail "IBC write failed"
ibc i (IBCCoercion n) f = return f { ibc_coercions = n : ibc_coercions f }
View
2  src/Idris/Parser.hs
@@ -881,7 +881,7 @@ pApp syn = do f <- pSimpleExpr syn
return (dslify i $ PApp fc f args)
where
dslify i (PApp fc (PRef _ f) [a])
- | [d] <- lookupCtxt Nothing f (idris_dsls i)
+ | [d] <- lookupCtxt f (idris_dsls i)
= desugar (syn { dsl_info = d }) i (getTm a)
dslify i t = t
View
2  src/Idris/Prover.hs
@@ -26,7 +26,7 @@ prover :: Bool -> Name -> Idris ()
prover lit x =
do ctxt <- getContext
i <- getIState
- case lookupTy Nothing x ctxt of
+ case lookupTy x ctxt of
[t] -> if elem x (idris_metavars i)
then prove ctxt lit x t
else fail $ show x ++ " is not a metavariable"
View
30 src/Idris/REPL.hs
@@ -129,7 +129,7 @@ resolveProof :: Name -> Idris Name
resolveProof n'
= do i <- getIState
ctxt <- getContext
- n <- case lookupNames Nothing n' ctxt of
+ n <- case lookupNames n' ctxt of
[x] -> return x
[] -> return n'
ns -> fail $ pshow i (CantResolveAlts (map show ns))
@@ -207,7 +207,7 @@ process fn (Check (PRef _ n))
= do ctxt <- getContext
ist <- getIState
imp <- impShow
- case lookupTy Nothing n ctxt of
+ case lookupTy n ctxt of
ts@(_:_) -> mapM_ (\t -> iputStrLn $ show n ++ " : " ++
showImp imp (delab ist t)) ts
[] -> iputStrLn $ "No such variable " ++ show n
@@ -220,7 +220,7 @@ process fn (Check t) = do (tm, ty) <- elabVal toplevel False t
showImp imp (delab ist ty))
process fn (DocStr n) = do i <- getIState
- case lookupCtxtName Nothing n (idris_docstrings i) of
+ case lookupCtxtName n (idris_docstrings i) of
[] -> iputStrLn $ "No documentation for " ++ show n
ns -> mapM_ showDoc ns
where showDoc (n, d)
@@ -237,8 +237,8 @@ process fn Universes = do i <- getIState
OK _ -> iputStrLn "Universes OK"
process fn (Defn n) = do i <- getIState
iputStrLn "Compiled patterns:\n"
- liftIO $ print (lookupDef Nothing n (tt_ctxt i))
- case lookupCtxt Nothing n (idris_patdefs i) of
+ liftIO $ print (lookupDef n (tt_ctxt i))
+ case lookupCtxt n (idris_patdefs i) of
[] -> return ()
[d] -> do iputStrLn "Original definiton:\n"
mapM_ (printCase i) d
@@ -255,25 +255,25 @@ process fn (TotCheck n) = do i <- getIState
_ -> return ()
process fn (DebugInfo n)
= do i <- getIState
- let oi = lookupCtxtName Nothing n (idris_optimisation i)
+ let oi = lookupCtxtName n (idris_optimisation i)
when (not (null oi)) $ iputStrLn (show oi)
- let si = lookupCtxt Nothing n (idris_statics i)
+ let si = lookupCtxt n (idris_statics i)
when (not (null si)) $ iputStrLn (show si)
- let di = lookupCtxt Nothing n (idris_datatypes i)
+ let di = lookupCtxt n (idris_datatypes i)
when (not (null di)) $ iputStrLn (show di)
- let d = lookupDef Nothing n (tt_ctxt i)
+ let d = lookupDef n (tt_ctxt i)
when (not (null d)) $ liftIO $
do print (head d)
- let cg = lookupCtxtName Nothing n (idris_callgraph i)
+ let cg = lookupCtxtName n (idris_callgraph i)
findUnusedArgs (map fst cg)
i <- getIState
- let cg' = lookupCtxtName Nothing n (idris_callgraph i)
+ let cg' = lookupCtxtName n (idris_callgraph i)
sc <- checkSizeChange n
iputStrLn $ "Size change: " ++ show sc
when (not (null cg')) $ do iputStrLn "Call graph:\n"
iputStrLn (show cg')
process fn (Info n) = do i <- getIState
- case lookupCtxt Nothing n (idris_classes i) of
+ case lookupCtxt n (idris_classes i) of
[c] -> classInfo c
_ -> iputStrLn "Not a class"
process fn (Search t) = iputStrLn "Not implemented"
@@ -330,7 +330,7 @@ process fn (ShowProof n')
process fn (Prove n')
= do ctxt <- getContext
ist <- getIState
- n <- case lookupNames Nothing n' ctxt of
+ n <- case lookupNames n' ctxt of
[x] -> return x
[] -> return n'
ns -> fail $ pshow ist (CantResolveAlts (map show ns))
@@ -381,7 +381,7 @@ process fn (Pattelab t)
iputStrLn $ show tm ++ "\n\n : " ++ show ty
process fn (Missing n) = do i <- getIState
- case lookupDef Nothing n (tt_ctxt i) of
+ case lookupDef n (tt_ctxt i) of
[CaseOp _ _ _ _ _ args t _ _]
-> do tms <- genMissing n args t
iputStrLn (showSep "\n" (map (showImp True) tms))
@@ -431,7 +431,7 @@ dumpInstance :: Name -> Idris ()
dumpInstance n = do i <- getIState
ctxt <- getContext
imp <- impShow
- case lookupTy Nothing n ctxt of
+ case lookupTy n ctxt of
ts -> mapM_ (\t -> iputStrLn $ showImp imp (delab i t)) ts
showTotal t@(Partial (Other ns)) i
View
4 src/Idris/UnusedArgs.hs
@@ -15,7 +15,7 @@ findUnusedArgs ns = mapM_ traceUnused ns
traceUnused :: Name -> Idris ()
traceUnused n
= do i <- getIState
- case lookupCtxt Nothing n (idris_callgraph i) of
+ case lookupCtxt n (idris_callgraph i) of
[CGInfo args calls scg usedns _] ->
do let argpos = zip args [0..]
let fargs = concatMap (getFargpos calls) argpos
@@ -39,7 +39,7 @@ used path g j
| otherwise
= do logLvl 5 $ (show ((g, j) : path))
i <- getIState
- case lookupCtxt Nothing g (idris_callgraph i) of
+ case lookupCtxt g (idris_callgraph i) of
[CGInfo args calls scg usedns unused] ->
if (j >= length args)
then -- overapplied, assume used
Please sign in to comment.
Something went wrong with that request. Please try again.