e9c9297 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make lookupCtxtExact return Maybe instead of List

commite9c9297445d9c930018d93fb091600fde6253424 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 23 Jan 2014, 13:50 (13 years ago) parent1f67398

5 files changed+30−29

compare with master

unifiedsplit

src/IRTS/Compiler.hs+3−3 src/IRTS/Defunctionalise.hs+8−8 src/IRTS/Simplified.hs+14−14 src/Idris/AbsSyntax.hs+2−2 src/Idris/Core/TT.hs+3−2

src/IRTS/Compiler.hs+3−3

@@ -218,13 +218,13 @@ instance ToIR (TT Name) where

218218 let collapse

219219 = case lookupCtxtExact n

220220 (idris_optimisation i) of

221− [oi] -> collapsible oi

221+ Just oi -> collapsible oi

222222 _ -> False

223223 let unused

224224 = case lookupCtxtExact n

225225 (idris_callgraph i) of

226− [CGInfo _ _ _ _ unusedpos] ->

227− unusedpos

226+ Just (CGInfo _ _ _ _ unusedpos) ->

227+ unusedpos

228228 _ -> []

229229 if collapse

230230 then return LNothing

src/IRTS/Defunctionalise.hs+8−8

@@ -81,17 +81,17 @@ addApps defs (n, LFun _ _ args e)

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

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

8383 case lookupCtxtExact 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'

84+ Just (LConstructor _ i ar) -> return $ DApp tc n args'

85+ Just (LFun _ _ as _) -> let arity = length as in

86+ fixApply tc n args' arity

87+ Nothing -> return $ chainAPPLY (DV (Glob n)) args'

8888 aa env (LLazyApp n args)

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

9090 case lookupCtxtExact 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

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

91+ Just (LConstructor _ i ar) -> return $ DApp False n args'

92+ Just (LFun _ _ as _) -> let arity = length as in

93+ fixLazyApply n args' arity

94+ Nothing -> return $ chainAPPLY (DV (Glob n)) args'

9595 aa env (LForce (LLazyApp n args)) = aa env (LApp False (LV (Glob n)) args)

9696 aa env (LForce e) = liftM eEVAL (aa env e)

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

4848simplify tl (DV (Glob x))

4949 = do ctxt <- ldefs

5050 case lookupCtxtExact x ctxt of

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

51+ Just (DConstructor _ t 0) -> return $ SCon t x []

5252 _ -> return $ SV (Glob x)

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

5454 mkapp (SApp (tl || tc) n) args'

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

9090sVar (DV (Glob x))

9191 = do ctxt <- ldefs

9292 case lookupCtxtExact x ctxt of

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

93+ Just (DConstructor _ t 0) -> sVar (DC t x [])

9494 _ -> return (Glob x, Nothing)

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

9696sVar e = do e' <- simplify False e

@@ -138,23 +138,23 @@ scopecheck ctxt envTop tm = sc envTop tm where

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

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

140140 Nothing -> case lookupCtxtExact n ctxt of

141− [DConstructor _ i ar] ->

141+ Just (DConstructor _ i ar) ->

142142 if True -- ar == 0

143143 then return (SCon i n [])

144144 else fail $ "Codegen error: Constructor " ++ show n ++

145145 " has arity " ++ show ar

146− [_] -> return (SV (Glob n))

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

146+ Just _ -> return (SV (Glob n))

147+ Nothing -> fail $ "Codegen error: No such variable " ++ show n

148148 sc env (SApp tc f args)

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

150150 case lookupCtxtExact f ctxt of

151− [DConstructor n tag ar] ->

151+ Just (DConstructor n tag ar) ->

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

153153 then return $ SCon tag n args'

154154 else fail $ "Codegen error: Constructor " ++ show f ++

155155 " has arity " ++ show ar

156− [_] -> return $ SApp tc f args'

157− [] -> fail $ "Codegen error: No such variable " ++ show f

156+ Just _ -> return $ SApp tc f args'

157+ Nothing -> fail $ "Codegen error: No such variable " ++ show f

158158 sc env (SForeign l ty f args)

159159 = do args' <- mapM (\ (t, a) -> do a' <- scVar env a

160160 return (t, a')) args

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

162162 sc env (SCon tag f args)

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

164164 case lookupCtxtExact f ctxt of

165− [DConstructor n tag ar] ->

165+ Just (DConstructor n tag ar) ->

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

167167 then return $ SCon tag n args'

168168 else fail $ "Codegen error: Constructor " ++ show f ++

@@ -199,17 +199,17 @@ scopecheck ctxt envTop tm = sc envTop tm where

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

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

201201 Nothing -> case lookupCtxtExact n ctxt of

202− [DConstructor _ i ar] ->

202+ Just (DConstructor _ i ar) ->

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

204− [_] -> return (Glob n)

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

206− " in " ++ show tm ++ " " ++ show envTop

204+ Just _ -> return (Glob n)

205+ Nothing -> fail $ "Codegen error: No such variable " ++ show n ++

206+ " in " ++ show tm ++ " " ++ show envTop

207207 scVar _ x = return x

208208

209209 scalt env (SConCase _ i n args e)

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

211211 tag <- case lookupCtxtExact n ctxt of

212− [DConstructor _ i ar] ->

212+ Just (DConstructor _ i ar) ->

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

214214 then return i

215215 else fail $ "Codegen error: Constructor " ++ show n ++

src/Idris/AbsSyntax.hs+2−2

@@ -166,8 +166,8 @@ allNames :: [Name] -> Name -> Idris [Name]

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

167167allNames ns n = do i <- getIState

168168 case lookupCtxtExact n (idris_callgraph i) of

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

170− return (nub (n : concat more))

169+ Just ns' -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))

170+ return (nub (n : concat more))

171171 _ -> return [n]

172172

173173addCoercion :: Name -> Idris ()

src/Idris/Core/TT.hs+3−2

@@ -29,6 +29,7 @@ import qualified Data.Map.Strict as Map

2929import Data.Char

3030import qualified Data.Text as T

3131import Data.List

32+import Data.Maybe (listToMaybe)

3233import Data.Vector.Unboxed (Vector)

3334import qualified Data.Vector.Unboxed as V

3435import qualified Data.Binary as B

@@ -389,8 +390,8 @@ lookupCtxtName n ctxt = case Map.lookup (nsroot n) ctxt of

389390lookupCtxt :: Name -> Ctxt a -> [a]

390391lookupCtxt n ctxt = map snd (lookupCtxtName n ctxt)

391392

392−lookupCtxtExact :: Name -> Ctxt a -> [a]

393−lookupCtxtExact n ctxt = [ v | (nm, v) <- lookupCtxtName n ctxt, nm == n]

393+lookupCtxtExact :: Name -> Ctxt a -> Maybe a

394+lookupCtxtExact n ctxt = listToMaybe [ v | (nm, v) <- lookupCtxtName n ctxt, nm == n]

394395

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

396397updateDef n f ctxt