git.iko.soy/Idris-dev
on master help sign in
Make lookupCtxtExact return Maybe instead of List
e9c9297David Raymond Christiansen
src/IRTS/Compiler.hs+3−3
compare with master
unifiedsplit
@@ -218,13 +218,13 @@ instance ToIR (TT Name) where
218 let collapse
218 let collapse
219 = case lookupCtxtExact n
219 = case lookupCtxtExact n
220 (idris_optimisation i) of
220 (idris_optimisation i) of
221− [oi] -> collapsible oi
221+ Just oi -> collapsible oi
222 _ -> False
222 _ -> False
223 let unused
223 let unused
224 = case lookupCtxtExact n
224 = case lookupCtxtExact n
225 (idris_callgraph i) of
225 (idris_callgraph i) of
226− [CGInfo _ _ _ _ unusedpos] ->
226+ Just (CGInfo _ _ _ _ unusedpos) ->
227− unusedpos
227+ unusedpos
228 _ -> []
228 _ -> []
229 if collapse
229 if collapse
230 then return LNothing
230 then return LNothing
src/IRTS/Defunctionalise.hs+8−8
@@ -81,17 +81,17 @@ addApps defs (n, LFun _ _ args e)
81 aa env (LApp tc (LV (Glob n)) args)
81 aa env (LApp tc (LV (Glob n)) args)
82 = do args' <- mapM (aa env) args
82 = do args' <- mapM (aa env) args
83 case lookupCtxtExact n defs of
83 case lookupCtxtExact n defs of
84− [LConstructor _ i ar] -> return $ DApp tc n args'
84+ Just (LConstructor _ i ar) -> return $ DApp tc n args'
85− [LFun _ _ as _] -> let arity = length as in
85+ Just (LFun _ _ as _) -> let arity = length as in
86− fixApply tc n args' arity
86+ fixApply tc n args' arity
87− [] -> return $ chainAPPLY (DV (Glob n)) args'
87+ Nothing -> return $ chainAPPLY (DV (Glob n)) args'
88 aa env (LLazyApp n args)
88 aa env (LLazyApp n args)
89 = do args' <- mapM (aa env) args
89 = do args' <- mapM (aa env) args
90 case lookupCtxtExact n defs of
90 case lookupCtxtExact n defs of
91− [LConstructor _ i ar] -> return $ DApp False n args'
91+ Just (LConstructor _ i ar) -> return $ DApp False n args'
92− [LFun _ _ as _] -> let arity = length as in
92+ Just (LFun _ _ as _) -> let arity = length as in
93− fixLazyApply n args' arity
93+ fixLazyApply n args' arity
94− [] -> return $ chainAPPLY (DV (Glob n)) args'
94+ Nothing -> return $ chainAPPLY (DV (Glob n)) args'
95 aa env (LForce (LLazyApp n args)) = aa env (LApp False (LV (Glob n)) args)
95 aa env (LForce (LLazyApp n args)) = aa env (LApp False (LV (Glob n)) args)
96 aa env (LForce e) = liftM eEVAL (aa env e)
96 aa env (LForce e) = liftM eEVAL (aa env e)
97 aa env (LLet n v sc) = liftM2 (DLet n) (aa env v) (aa (n : env) sc)
97 aa env (LLet n v sc) = liftM2 (DLet n) (aa env v) (aa (n : env) sc)
src/IRTS/Simplified.hs+14−14
@@ -48,7 +48,7 @@ simplify tl (DV (Loc i)) = return (SV (Loc i))
48simplify tl (DV (Glob x))
48simplify tl (DV (Glob x))
49 = do ctxt <- ldefs
49 = do ctxt <- ldefs
50 case lookupCtxtExact x ctxt of
50 case lookupCtxtExact x ctxt of
51− [DConstructor _ t 0] -> return $ SCon t x []
51+ Just (DConstructor _ t 0) -> return $ SCon t x []
52 _ -> return $ SV (Glob x)
52 _ -> return $ SV (Glob x)
53simplify tl (DApp tc n args) = do args' <- mapM sVar args
53simplify tl (DApp tc n args) = do args' <- mapM sVar args
54 mkapp (SApp (tl || tc) n) args'
54 mkapp (SApp (tl || tc) n) args'
@@ -90,7 +90,7 @@ simplify tl (DError str) = return $ SError str
90sVar (DV (Glob x))
90sVar (DV (Glob x))
91 = do ctxt <- ldefs
91 = do ctxt <- ldefs
92 case lookupCtxtExact x ctxt of
92 case lookupCtxtExact x ctxt of
93− [DConstructor _ t 0] -> sVar (DC t x [])
93+ Just (DConstructor _ t 0) -> sVar (DC t x [])
94 _ -> return (Glob x, Nothing)
94 _ -> return (Glob x, Nothing)
95sVar (DV x) = return (x, Nothing)
95sVar (DV x) = return (x, Nothing)
96sVar e = do e' <- simplify False e
96sVar e = do e' <- simplify False e
@@ -138,23 +138,23 @@ scopecheck ctxt envTop tm = sc envTop tm where
138 case lookup n (reverse env) of -- most recent first
138 case lookup n (reverse env) of -- most recent first
139 Just i -> do lvar i; return (SV (Loc i))
139 Just i -> do lvar i; return (SV (Loc i))
140 Nothing -> case lookupCtxtExact n ctxt of
140 Nothing -> case lookupCtxtExact n ctxt of
141− [DConstructor _ i ar] ->
141+ Just (DConstructor _ i ar) ->
142 if True -- ar == 0
142 if True -- ar == 0
143 then return (SCon i n [])
143 then return (SCon i n [])
144 else fail $ "Codegen error: Constructor " ++ show n ++
144 else fail $ "Codegen error: Constructor " ++ show n ++
145 " has arity " ++ show ar
145 " has arity " ++ show ar
146− [_] -> return (SV (Glob n))
146+ Just _ -> return (SV (Glob n))
147− [] -> fail $ "Codegen error: No such variable " ++ show n
147+ Nothing -> fail $ "Codegen error: No such variable " ++ show n
148 sc env (SApp tc f args)
148 sc env (SApp tc f args)
149 = do args' <- mapM (scVar env) args
149 = do args' <- mapM (scVar env) args
150 case lookupCtxtExact f ctxt of
150 case lookupCtxtExact f ctxt of
151− [DConstructor n tag ar] ->
151+ Just (DConstructor n tag ar) ->
152 if True -- (ar == length args)
152 if True -- (ar == length args)
153 then return $ SCon tag n args'
153 then return $ SCon tag n args'
154 else fail $ "Codegen error: Constructor " ++ show f ++
154 else fail $ "Codegen error: Constructor " ++ show f ++
155 " has arity " ++ show ar
155 " has arity " ++ show ar
156− [_] -> return $ SApp tc f args'
156+ Just _ -> return $ SApp tc f args'
157− [] -> fail $ "Codegen error: No such variable " ++ show f
157+ Nothing -> fail $ "Codegen error: No such variable " ++ show f
158 sc env (SForeign l ty f args)
158 sc env (SForeign l ty f args)
159 = do args' <- mapM (\ (t, a) -> do a' <- scVar env a
159 = do args' <- mapM (\ (t, a) -> do a' <- scVar env a
160 return (t, a')) args
160 return (t, a')) args
@@ -162,7 +162,7 @@ scopecheck ctxt envTop tm = sc envTop tm where
162 sc env (SCon tag f args)
162 sc env (SCon tag f args)
163 = do args' <- mapM (scVar env) args
163 = do args' <- mapM (scVar env) args
164 case lookupCtxtExact f ctxt of
164 case lookupCtxtExact f ctxt of
165− [DConstructor n tag ar] ->
165+ Just (DConstructor n tag ar) ->
166 if True -- (ar == length args)
166 if True -- (ar == length args)
167 then return $ SCon tag n args'
167 then return $ SCon tag n args'
168 else fail $ "Codegen error: Constructor " ++ show f ++
168 else fail $ "Codegen error: Constructor " ++ show f ++
@@ -199,17 +199,17 @@ scopecheck ctxt envTop tm = sc envTop tm where
199 case lookup n (reverse env) of -- most recent first
199 case lookup n (reverse env) of -- most recent first
200 Just i -> do lvar i; return (Loc i)
200 Just i -> do lvar i; return (Loc i)
201 Nothing -> case lookupCtxtExact n ctxt of
201 Nothing -> case lookupCtxtExact n ctxt of
202− [DConstructor _ i ar] ->
202+ Just (DConstructor _ i ar) ->
203 fail $ "Codegen error : can't pass constructor here"
203 fail $ "Codegen error : can't pass constructor here"
204− [_] -> return (Glob n)
204+ Just _ -> return (Glob n)
205− [] -> fail $ "Codegen error: No such variable " ++ show n ++
205+ Nothing -> fail $ "Codegen error: No such variable " ++ show n ++
206− " in " ++ show tm ++ " " ++ show envTop
206+ " in " ++ show tm ++ " " ++ show envTop
207 scVar _ x = return x
207 scVar _ x = return x
208
208
209 scalt env (SConCase _ i n args e)
209 scalt env (SConCase _ i n args e)
210 = do let env' = env ++ zip args [length env..]
210 = do let env' = env ++ zip args [length env..]
211 tag <- case lookupCtxtExact n ctxt of
211 tag <- case lookupCtxtExact n ctxt of
212− [DConstructor _ i ar] ->
212+ Just (DConstructor _ i ar) ->
213 if True -- (length args == ar)
213 if True -- (length args == ar)
214 then return i
214 then return i
215 else fail $ "Codegen error: Constructor " ++ show n ++
215 else fail $ "Codegen error: Constructor " ++ show n ++
src/Idris/AbsSyntax.hs+2−2
@@ -166,8 +166,8 @@ allNames :: [Name] -> Name -> Idris [Name]
166allNames ns n | n `elem` ns = return []
166allNames ns n | n `elem` ns = return []
167allNames ns n = do i <- getIState
167allNames ns n = do i <- getIState
168 case lookupCtxtExact n (idris_callgraph i) of
168 case lookupCtxtExact n (idris_callgraph i) of
169− [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
169+ Just ns' -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
170− return (nub (n : concat more))
170+ return (nub (n : concat more))
171 _ -> return [n]
171 _ -> return [n]
172
172
173addCoercion :: Name -> Idris ()
173addCoercion :: Name -> Idris ()
src/Idris/Core/TT.hs+3−2
@@ -29,6 +29,7 @@ import qualified Data.Map.Strict as Map
29import Data.Char
29import Data.Char
30import qualified Data.Text as T
30import qualified Data.Text as T
31import Data.List
31import Data.List
32+import Data.Maybe (listToMaybe)
32import Data.Vector.Unboxed (Vector)
33import Data.Vector.Unboxed (Vector)
33import qualified Data.Vector.Unboxed as V
34import qualified Data.Vector.Unboxed as V
34import qualified Data.Binary as B
35import qualified Data.Binary as B
@@ -389,8 +390,8 @@ lookupCtxtName n ctxt = case Map.lookup (nsroot n) ctxt of
389lookupCtxt :: Name -> Ctxt a -> [a]
390lookupCtxt :: Name -> Ctxt a -> [a]
390lookupCtxt n ctxt = map snd (lookupCtxtName n ctxt)
391lookupCtxt n ctxt = map snd (lookupCtxtName n ctxt)
391
392
392−lookupCtxtExact :: Name -> Ctxt a -> [a]
393+lookupCtxtExact :: Name -> Ctxt a -> Maybe a
393−lookupCtxtExact n ctxt = [ v | (nm, v) <- lookupCtxtName n ctxt, nm == n]
394+lookupCtxtExact n ctxt = listToMaybe [ v | (nm, v) <- lookupCtxtName n ctxt, nm == n]
394
395
395updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a
396updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a
396updateDef n f ctxt
397updateDef n f ctxt