b51cf28 · Idris-dev · git.iko.soy

151 do e <- ir (args, sc)

152 return (declArgs [] (case_inlinable ci) n e)

153

154−mkLDecl n (TyDecl (DCon tag arity) _) = do

154+mkLDecl n (TyDecl (DCon tag arity) _) =

155− ist <- getIState

155+ LConstructor n tag . maybe arity (length . usedpos) . lookupCtxtExact n . idris_callgraph <$> getIState

156−

157− let realArity = case lookupCtxt n (idris_callgraph ist) of

158− [CGInfo _ _ _ _ xs] -> length xs

159− _ -> arity

160−

161− return $ LConstructor n tag realArity

162

156

163mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a

157mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a

164mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run

158mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run

166instance ToIR (TT Name) where

160instance ToIR (TT Name) where

167 ir tm = ir' [] tm where

161 ir tm = ir' [] tm where

168 ir' env tm@(App f a)

162 ir' env tm@(App f a)

169− | (P _ (UN m) _, args) <- unApply tm,

163+ | (P _ (UN m) _, args) <- unApply tm,

170 m == txt "mkForeignPrim"

164 m == txt "mkForeignPrim"

171− = doForeign env args

165+ = doForeign env args

172− | (P _ (UN u) _, [_, arg]) <- unApply tm,

166+ | (P _ (UN u) _, [_, arg]) <- unApply tm,

173 u == txt "unsafePerformPrimIO"

167 u == txt "unsafePerformPrimIO"

174− = ir' env arg

168+ = ir' env arg

175 -- TMP HACK - until we get inlining.

169 -- TMP HACK - until we get inlining.

176− | (P _ (UN r) _, [_, _, _, _, _, arg]) <- unApply tm,

170+ | (P _ (UN r) _, [_, _, _, _, _, arg]) <- unApply tm,

177 r == txt "replace"

171 r == txt "replace"

178− = ir' env arg

172+ = ir' env arg

179− -- Laziness, the old way

173+ -- Laziness, the old way

180− | (P _ (UN l) _, [_, arg]) <- unApply tm,

174+ | (P _ (UN l) _, [_, arg]) <- unApply tm,

181 l == txt "lazy"

175 l == txt "lazy"

182− = do arg' <- ir' env arg

176+ = do arg' <- ir' env arg

183− error "lazy has crept in somehow"

177+ error "lazy has crept in somehow"

184-- return $ LLazyExp arg'

178-- return $ LLazyExp arg'

185− | (P _ (UN l) _, [_, arg]) <- unApply tm,

179+ | (P _ (UN l) _, [_, arg]) <- unApply tm,

186 l == txt "force"

180 l == txt "force"

187− = do arg' <- ir' env arg

181+ = do arg' <- ir' env arg

188− return $ LForce arg'

182+ return $ LForce arg'

189− -- Laziness, the new way

183+ -- Laziness, the new way

190− | (P _ (UN l) _, [_, arg]) <- unApply tm,

184+ | (P _ (UN l) _, [_, arg]) <- unApply tm,

191 l == txt "Delay"

185 l == txt "Delay"

192− = do arg' <- ir' env arg

186+ = do arg' <- ir' env arg

193− return $ LLazyExp arg'

187+ return $ LLazyExp arg'

194− | (P _ (UN l) _, [_, _, arg]) <- unApply tm,

188+ | (P _ (UN l) _, [_, arg]) <- unApply tm,

195 l == txt "Force"

189 l == txt "Force"

196− = do arg' <- ir' env arg

190+ = do arg' <- ir' env arg

197− return $ LForce arg'

191+ return $ LForce arg'

198− | (P _ (UN a) _, [_, _, arg]) <- unApply tm,

192+ | (P _ (UN a) _, [_, _, arg]) <- unApply tm,

199 a == txt "assert_smaller"

193 a == txt "assert_smaller"

200− = ir' env arg

194+ = ir' env arg

201− | (P _ (UN a) _, [_, arg]) <- unApply tm,

195+ | (P _ (UN a) _, [_, arg]) <- unApply tm,

202 a == txt "assert_total"

196 a == txt "assert_total"

203− = ir' env arg

197+ = ir' env arg

204− | (P _ (UN p) _, [_, arg]) <- unApply tm,

198+ | (P _ (UN p) _, [_, arg]) <- unApply tm,

205 p == txt "par"

199 p == txt "par"

206− = do arg' <- ir' env arg

200+ = do arg' <- ir' env arg

207− return $ LOp LPar [LLazyExp arg']

201+ return $ LOp LPar [LLazyExp arg']

208− | (P _ (UN pf) _, [arg]) <- unApply tm,

202+ | (P _ (UN pf) _, [arg]) <- unApply tm,

209 pf == txt "prim_fork"

203 pf == txt "prim_fork"

210− = do arg' <- ir' env arg

204+ = do arg' <- ir' env arg

211− return $ LOp LFork [LLazyExp arg']

205+ return $ LOp LFork [LLazyExp arg']

212− | (P _ (UN m) _, [_,size,t]) <- unApply tm,

206+ | (P _ (UN m) _, [_,size,t]) <- unApply tm,

213 m == txt "malloc"

207 m == txt "malloc"

214− = do size' <- ir' env size

208+ = do size' <- ir' env size

215− t' <- ir' env t

209+ t' <- ir' env t

216− return t' -- TODO $ malloc_ size' t'

210+ return t' -- TODO $ malloc_ size' t'

217− | (P _ (UN tm) _, [_,t]) <- unApply tm,

211+ | (P _ (UN tm) _, [_,t]) <- unApply tm,

218 tm == txt "trace_malloc"

212 tm == txt "trace_malloc"

219− = do t' <- ir' env t

213+ = do t' <- ir' env t

220− return t' -- TODO

214+ return t' -- TODO

221

215

222− -- This case is here until we get more general inlining. It's just

216+ -- This case is here until we get more general inlining. It's just

223− -- a really common case, and the laziness hurts...

217+ -- a really common case, and the laziness hurts...

224− | (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),

218+ | (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),

225 (App (P _ (UN d') _) e)]) <- unApply tm,

219 (App (P _ (UN d') _) e)]) <- unApply tm,

226 be == txt "boolElim" && d == txt "Delay" && d' == txt "Delay"

220 be == txt "boolElim" && d == txt "Delay" && d' == txt "Delay"

227− = do x' <- ir' env x

221+ = do x' <- ir' env x

228− t' <- ir' env t

222+ t' <- ir' env t

229− e' <- ir' env e

223+ e' <- ir' env e

230− return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',

224+ return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',

231− LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])

225+ LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])

232−

226+

233− | (P (DCon t a) n _, args) <- unApply tm = do

227+ | (P (DCon t arity) n _, args) <- unApply tm = do

234− cg <- idris_callgraph <$> getIState

228+ ist <- getIState

229+ let detag = maybe False detaggable . lookupCtxtExact n $ idris_optimisation ist

235− let used = maybe [] (map fst . usedpos) $ lookupCtxtExact n cg

230+ used = maybe [] (map fst . usedpos) . lookupCtxtExact n $ idris_callgraph ist

236− args' = [if i `elem` used then a else Erased | (i,a) <- zip [0..] args]

231+ args' = [a | (i,a) <- zip [0..] args, i `elem` used]

232+

233+ when (length args > arity) $

234+ ifail ("oversaturated data ctor: " ++ show tm)

235+

236+ if length args' == 1 && detag -- detaggable

237+ then ir' env (head args') -- newtype

237− irCon env t a n args'

238+ else irCon env t (length used) n args'

238−

239+

239− | (P (TCon t a) n _, args) <- unApply tm

240+ | (P (TCon t a) n _, args) <- unApply tm

240− = return LNothing

241+ = return LNothing

241−

242+

242− | (P _ n _, args) <- unApply tm = do

243+ | (P _ n _, args) <- unApply tm = do

243 ist <- getIState

244 ist <- getIState

244 case lookup n (idris_scprims ist) of

245 case lookup n (idris_scprims ist) of

245 -- if it's a primitive which is already saturated,

246 -- if it's a primitive which is already saturated,

249

250

250 _ -> applyName n ist args

251 _ -> applyName n ist args

251

252

252−{- collapsibility is turned off for now

253− _

254− -- if it's collapsible, compile to LNothing

255− | (collapsible <$> lookupCtxtExact n (idris_optimisation ist)) == Just True

256− -> return LNothing

257−

258− -- otherwise, compile normally

259− | otherwise -> applyName n ist args

260−

261−-}

262−

263− | (f, args) <- unApply tm

253+ | (f, args) <- unApply tm

264− = do f' <- ir' env f

254+ = do f' <- ir' env f

265− args' <- mapM (ir' env) args

255+ args' <- mapM (ir' env) args

266− return (LApp False f' args')

256+ return (LApp False f' args')

267

257

268− where

258+ where

269 applyName :: Name -> IState -> [Term] -> Idris LExp

259 applyName :: Name -> IState -> [Term] -> Idris LExp

270 applyName n ist args =

260 applyName n ist args =

271 LApp False (LV $ Glob n) <$> mapM (ir' env . erase) (zip [0..] args)

261 LApp False (LV $ Glob n) <$> mapM (ir' env . erase) (zip [0..] args)

272− where

262+ where

273− erase (i, x)

263+ erase (i, x)

274− | i >= arity || i `elem` used = x

264+ | i >= arity || i `elem` used = x

275− | otherwise = Erased

265+ | otherwise = Erased

276−

266+

277− arity = case fst4 <$> lookupCtxt n (definitions . tt_ctxt $ ist) of

267+ arity = case fst4 <$> lookupCtxt n (definitions . tt_ctxt $ ist) of

278− [CaseOp ci ty tys def tot cdefs] -> length tys

268+ [CaseOp ci ty tys def tot cdefs] -> length tys

279− [TyDecl (DCon tag ar) _] -> ar

269+ [TyDecl (DCon tag ar) _] -> ar

280− [Operator ty ar op] -> ar

270+ [Operator ty ar op] -> ar

281− _ -> 0

271+ _ -> 0

282−

272+

283− used = maybe [] (map fst . usedpos) $ lookupCtxtExact n (idris_callgraph ist)

273+ used = maybe [] (map fst . usedpos) $ lookupCtxtExact n (idris_callgraph ist)

284− fst4 (x,_,_,_) = x

274+ fst4 (x,_,_,_) = x

285

275

286-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)

276-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)

287-- = return $ LConst (BI 0)

277-- = return $ LConst (BI 0)