67b01ec · Idris-dev · git.iko.soy

105 if ex then return f else return h

106

107irMain :: TT Name -> Idris LDecl

108−irMain tm = do i <- ir tm

108+irMain tm = do

109+ i <- irTerm M.empty [] tm

109− return $ LFun [] (sMN 0 "runMain") [] (LForce i)

110+ return $ LFun [] (sMN 0 "runMain") [] (LForce i)

110

111

111mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]

112mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]

112mkDecls t used

113mkDecls t used

126isCon (TyDecl _ _) = True

127isCon (TyDecl _ _) = True

127isCon _ = False

128isCon _ = False

128

129

129−class ToIR a where

130− ir :: a -> Idris LExp

131−

132build :: (Name, Def) -> Idris (Name, LDecl)

130build :: (Name, Def) -> Idris (Name, LDecl)

133build (n, d)

131build (n, d)

134 = do i <- getIState

132 = do i <- getIState

144declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x

142declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x

145declArgs args inl n x = LFun (if inl then [Inline] else []) n args x

143declArgs args inl n x = LFun (if inl then [Inline] else []) n args x

146

144

147−mkLDecl n (Function tm _) = do e <- ir tm

145+mkLDecl n (Function tm _)

148− return (declArgs [] True n e)

146+ = declArgs [] True n <$> irTerm M.empty [] tm

147+

149mkLDecl n (CaseOp ci _ _ _ pats cd)

148mkLDecl n (CaseOp ci _ _ _ pats cd)

150− = let (args, sc) = cases_runtime cd in

151− do e <- ir (args, sc)

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

149+ = declArgs [] (case_inlinable ci) n <$> irTree args sc

150+ where

151+ (args, sc) = cases_runtime cd

153

152

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

153mkLDecl n (TyDecl (DCon tag arity) _) =

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

154+ LConstructor n tag . erasedArity . lookup n <$> getIState

155+ where

156+ lookup n = lookupCtxtExact n . idris_callgraph

157+ erasedArity = maybe 0 (length . usedpos)

156

158

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

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

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

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

159

161

160−instance ToIR (TT Name) where

162+data VarInfo = VI

161− ir tm = ir' [] tm where

163+ { viMethod :: Maybe Name

164+ }

165+ deriving Show

166+

167+type Vars = M.Map Name VarInfo

168+

169+irTerm :: Vars -> [Name] -> Term -> Idris LExp

162− ir' env tm@(App f a)

170+irTerm vs env tm@(App f a) = case unApply tm of

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

171+ (P _ (UN m) _, args)

164− m == txt "mkForeignPrim"

172+ | m == txt "mkForeignPrim"

165− = doForeign env args

173+ -> doForeign vs env args

174+

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

175+ (P _ (UN u) _, [_, arg])

167− u == txt "unsafePerformPrimIO"

176+ | u == txt "unsafePerformPrimIO"

168− = ir' env arg

177+ -> irTerm vs env arg

178+

169− -- TMP HACK - until we get inlining.

179+ -- TMP HACK - until we get inlining.

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

180+ (P _ (UN r) _, [_, _, _, _, _, arg])

171− r == txt "replace"

181+ | r == txt "replace"

172− = ir' env arg

182+ -> irTerm vs env arg

183+

173− -- Laziness, the old way

184+ -- Laziness, the old way

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

185+ (P _ (UN l) _, [_, arg])

175− l == txt "lazy"

186+ | l == txt "lazy"

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

177− error "lazy has crept in somehow"

187+ -> error "lazy has crept in somehow"

178−-- return $ LLazyExp arg'

188+

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

189+ (P _ (UN l) _, [_, arg])

180− l == txt "force"

190+ | l == txt "force"

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

191+ -> LForce <$> irTerm vs env arg

182− return $ LForce arg'

192+

183− -- Laziness, the new way

193+ -- Laziness, the new way

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

194+ (P _ (UN l) _, [_, arg])

185− l == txt "Delay"

195+ | l == txt "Delay"

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

196+ -> LLazyExp <$> irTerm vs env arg

187− return $ LLazyExp arg'

197+

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

198+ (P _ (UN l) _, [_, arg])

189− l == txt "Force"

199+ | l == txt "Force"

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

200+ -> LForce <$> irTerm vs env arg

191− return $ LForce arg'

201+

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

202+ (P _ (UN a) _, [_, _, arg])

193− a == txt "assert_smaller"

203+ | a == txt "assert_smaller"

194− = ir' env arg

204+ -> irTerm vs env arg

205+

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

206+ (P _ (UN a) _, [_, arg])

196− a == txt "assert_total"

207+ | a == txt "assert_total"

197− = ir' env arg

208+ -> irTerm vs env arg

209+

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

210+ (P _ (UN p) _, [_, arg])

199− p == txt "par"

211+ | p == txt "par"

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

212+ -> do arg' <- irTerm vs env arg

201− return $ LOp LPar [LLazyExp arg']

213+ return $ LOp LPar [LLazyExp arg']

214+

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

215+ (P _ (UN pf) _, [arg])

203− pf == txt "prim_fork"

216+ | pf == txt "prim_fork"

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

217+ -> do arg' <- irTerm vs env arg

205− return $ LOp LFork [LLazyExp arg']

218+ return $ LOp LFork [LLazyExp arg']

219+

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

220+ (P _ (UN m) _, [_,size,t])

207− m == txt "malloc"

221+ | m == txt "malloc"

222+ -> irTerm vs env t

223+{-

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

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

209− t' <- ir' env t

225+ t' <- ir' env t

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

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

227+-}

228+

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

229+ (P _ (UN tm) _, [_,t])

212− tm == txt "trace_malloc"

230+ | tm == txt "trace_malloc"

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

231+ -> irTerm vs env t -- TODO

214− return t' -- TODO

232+

215−

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

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

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

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

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

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

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

236+ (App (P _ (UN d') _) e)])

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

237+ | be == txt "boolElim"

238+ , d == txt "Delay"

239+ , d' == txt "Delay"

240+ -> do

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

241+ x' <- irTerm vs env x

222− t' <- ir' env t

242+ t' <- irTerm vs env t

223− e' <- ir' env e

243+ e' <- irTerm vs env e

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

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

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

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

226−

246+ ])

247+

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

248+ (P (DCon t arity) n _, args) -> do

228− ist <- getIState

249+ ist <- getIState

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

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

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

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

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

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

232−

253+

233− when (length args > arity) $

254+ when (length args > arity) $

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

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

235−

256+

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

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

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

258+ then irTerm vs env (head args') -- newtype

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

259+ else irCon vs env (length used) n args'

239−

260+

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

241− = return LNothing

261+ (P (TCon t a) n _, args) -> return LNothing

242−

262+

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

263+ (P _ n _, args) -> do

244− ist <- getIState

264+ ist <- getIState

245− case lookup n (idris_scprims ist) of

265+ case lookup n (idris_scprims ist) of

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

266+ -- if it's a primitive that is already saturated,

247− -- compile to the corresponding op here already to save work

267+ -- compile to the corresponding op here already to save work

248− Just (arity, op) | length args == arity

268+ Just (arity, op) | length args == arity

249− -> LOp op <$> mapM (ir' env) args

269+ -> LOp op <$> mapM (irTerm vs env) args

250−

270+

271+ -- otherwise, just apply the name

251− _ -> applyName n ist args

272+ _ -> applyName n ist args

252−

273+

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

274+ (f, args)

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

275+ -> LApp False

276+ <$> irTerm vs env f

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

277+ <*> mapM (irTerm vs env) args

256− return (LApp False f' args')

278+

257−

258− where

279+ where

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

280+ applyName :: Name -> IState -> [Term] -> Idris LExp

260− applyName n ist args =

281+ applyName n ist args =

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

282+ LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)

262− where

283+ where

263− erase (i, x)

284+ erase (i, x)

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

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

265− | otherwise = Erased

286+ | otherwise = Erased

266−

287+

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

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

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

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

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

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

270− [TyDecl Ref ty] -> length $ getArgTys ty

291+ [TyDecl Ref ty] -> length $ getArgTys ty

271− [Operator ty ar op] -> ar

292+ [Operator ty ar op] -> ar

272− [] -> 0 -- no definition, probably local name => can't erase anything

293+ [] -> 0 -- no definition, probably local name => can't erase anything

273− def -> error $ "unknown arity: " ++ show (n, def)

294+ def -> error $ "unknown arity: " ++ show (n, def)

274−

295+

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

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

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

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

277

298

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

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

279-- = return $ LConst (BI 0)

300-- = return $ LConst (BI 0)

301+

280− ir' env (P _ n _) = return $ LV (Glob n)

302+irTerm vs env (P _ n _) = return $ LV (Glob n)

303+irTerm vs env (V i)

281− ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))

304+ | i >= 0 && i < length env = return $ LV (Glob (env!!i))

282− | otherwise = ifail $ "IR fail " ++ show i ++ " " ++ show tm

305+ | otherwise = ifail $ "bad de bruijn index: " ++ show i

306+

283− ir' env (Bind n (Lam _) sc)

307+irTerm vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm vs (n':env) sc

284− = do let n' = uniqueName n env

308+ where

285− sc' <- ir' (n' : env) sc

309+ n' = uniqueName n env

286− return $ LLam [n'] sc'

310+

287− ir' env (Bind n (Let _ v) sc)

311+irTerm vs env (Bind n (Let _ v) sc)

288− = do sc' <- ir' (n : env) sc

312+ = LLet n <$> irTerm vs env v <*> irTerm vs (n : env) sc

289− v' <- ir' env v

313+

290− return $ LLet n v' sc'

291− ir' env (Bind _ _ _) = return $ LNothing

314+irTerm vs env (Bind _ _ _) = return $ LNothing

315+

292− ir' env (Proj t i) | i == -1

316+irTerm vs env (Proj t (-1)) = do

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

317+ t' <- irTerm vs env t

294− return $ LOp (LMinus (ATInt ITBig))

318+ return $ LOp (LMinus (ATInt ITBig))

295− [t', LConst (BI 1)]

319+ [t', LConst (BI 1)]

296− ir' env (Proj t i) = do t' <- ir' env t

320+

297− return $ LProj t' i

321+irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i

298− ir' env (Constant c) = return $ LConst c

322+irTerm vs env (Constant c) = return $ LConst c

299− ir' env (TType _) = return $ LNothing

323+irTerm vs env (TType _) = return $ LNothing

300− ir' env Erased = return $ LNothing

324+irTerm vs env Erased = return $ LNothing

301− ir' env Impossible = return $ LNothing

325+irTerm vs env Impossible = return $ LNothing

302-- ir' env _ = return $ LError "Impossible"

326-- ir' env _ = return $ LError "Impossible"

303

327

304− irCon env t arity n args

328+irCon :: Vars -> [Name] -> Int -> Name -> [Term] -> Idris LExp

329+irCon vs env arity n args

330+ | length args > arity

331+ = error $ "oversaturated data constructor: " ++ show (n, args)

332+

333+ -- saturated

334+ | length args == arity

305− | length args == arity = buildApp env (LV (Glob n)) args

335+ = buildApp (LV (Glob n)) args

306− | otherwise = let extra = satArgs (arity - length args) in

336+

307− do sc' <- irCon env t arity n

337+ -- undersaturated, wrap in lambdas

338+ | otherwise

339+ = let extraNs = [sMN i "sat" | i <- [length args .. arity-1]]

308− (args ++ map (\n -> P Bound n undefined) extra)

340+ extraTs = [P Bound n undefined | n <- extraNs]

309− return $ LLam extra sc'

341+ in LLam extraNs <$> irCon vs env arity n (args ++ extraTs)

310−

342+ where

311− satArgs n = map (\i -> sMN i "sat") [1..n]

312−

313− buildApp env e [] = return e

343+ buildApp e [] = return e

314− buildApp env e xs = do xs' <- mapM (ir' env) xs

315− return $ LApp False e xs'

344+ buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs

316−

345+

317− doForeign :: [Name] -> [TT Name] -> Idris LExp

346+doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp

318− doForeign env (_ : fgn : args)

347+doForeign vs env (_ : fgn : args)

319− | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn

348+ | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn

320− = let maybeTys = getFTypes fgnArgTys

349+ = case getFTypes fgnArgTys of

321− rty = mkIty' ret in

322− case maybeTys of

323− Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)

350+ Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)

324− Just tys -> do

351+ Just tys -> do

325− args' <- mapM (ir' env) (init args)

352+ args' <- mapM (irTerm vs env) (init args)

326− -- wrap it in a prim__IO

327− -- return $ con_ 0 @@ impossible @@

328− return $ -- LLazyExp $

329− LForeign LANG_C rty fgnName (zip tys args')

353+ return $ LForeign LANG_C (mkIty' ret) fgnName (zip tys args')

354+

330− | otherwise = ifail "Badly formed foreign function call"

355+ | otherwise = ifail "Badly formed foreign function call"

331−

356+ where

332−getFTypes :: TT Name -> Maybe [FType]

357+ getFTypes :: TT Name -> Maybe [FType]

333−getFTypes tm = case unApply tm of

358+ getFTypes tm = case unApply tm of

334− -- nil : {a : Type} -> List a

359+ -- nil : {a : Type} -> List a

335− (nil, [_]) -> Just []

360+ (nil, [_]) -> Just []

336− -- cons : {a : Type} -> a -> List a -> List a

361+ -- cons : {a : Type} -> a -> List a -> List a

337− (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs

362+ (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs

338− _ -> Nothing

363+ _ -> Nothing

339−

364+

340−mkIty' (P _ (UN ty) _) = mkIty (str ty)

365+ mkIty' (P _ (UN ty) _) = mkIty (str ty)

341−mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))

366+ mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))

367+ | fi == txt "FIntT"

342− | fi == txt "FIntT" = mkIntIty (str intTy)

368+ = mkIntIty (str intTy)

369+

343−mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))

370+ mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))

344− | ff == txt "FFunction" && fa == txt "FAny" &&

371+ | ff == txt "FFunction"

372+ , fa == txt "FAny"

345− io == txt "IO"

373+ , io == txt "IO"

346 = FFunctionIO

374 = FFunctionIO

375+

347−mkIty' (App (App (P _ (UN ff) _) _) _)

376+ mkIty' (App (App (P _ (UN ff) _) _) _)

348− | ff == txt "FFunction" = FFunction

377+ | ff == txt "FFunction"

378+ = FFunction

379+

349−mkIty' _ = FAny

380+ mkIty' _ = FAny

350−

381+

351−-- would be better if these FInt types were evaluated at compile time

382+ -- would be better if these FInt types were evaluated at compile time

352−-- TODO: add %eval directive for such things

383+ -- TODO: add %eval directive for such things

353−

384+

354−mkIty "FFloat" = FArith ATFloat

385+ mkIty "FFloat" = FArith ATFloat

355−mkIty "FInt" = mkIntIty "ITNative"

386+ mkIty "FInt" = mkIntIty "ITNative"

356−mkIty "FChar" = mkIntIty "ITChar"

387+ mkIty "FChar" = mkIntIty "ITChar"

357−mkIty "FByte" = mkIntIty "IT8"

388+ mkIty "FByte" = mkIntIty "IT8"

358−mkIty "FShort" = mkIntIty "IT16"

389+ mkIty "FShort" = mkIntIty "IT16"

359−mkIty "FLong" = mkIntIty "IT64"

390+ mkIty "FLong" = mkIntIty "IT64"

360−mkIty "FBits8" = mkIntIty "IT8"

391+ mkIty "FBits8" = mkIntIty "IT8"

361−mkIty "FBits16" = mkIntIty "IT16"

392+ mkIty "FBits16" = mkIntIty "IT16"

362−mkIty "FBits32" = mkIntIty "IT32"

393+ mkIty "FBits32" = mkIntIty "IT32"

363−mkIty "FBits64" = mkIntIty "IT64"

394+ mkIty "FBits64" = mkIntIty "IT64"

364−mkIty "FString" = FString

395+ mkIty "FString" = FString

365−mkIty "FPtr" = FPtr

396+ mkIty "FPtr" = FPtr

366−mkIty "FManagedPtr" = FManagedPtr

397+ mkIty "FManagedPtr" = FManagedPtr

367−mkIty "FUnit" = FUnit

398+ mkIty "FUnit" = FUnit

368−mkIty "FFunction" = FFunction

399+ mkIty "FFunction" = FFunction

369−mkIty "FFunctionIO" = FFunctionIO

400+ mkIty "FFunctionIO" = FFunctionIO

370−mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))

401+ mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))

371−mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))

402+ mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))

372−mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))

403+ mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))

373−mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))

404+ mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))

374−mkIty x = error $ "Unknown type " ++ x

405+ mkIty x = error $ "Unknown type " ++ x

375−

406+

376−mkIntIty "ITNative" = FArith (ATInt ITNative)

407+ mkIntIty "ITNative" = FArith (ATInt ITNative)

377−mkIntIty "ITChar" = FArith (ATInt ITChar)

408+ mkIntIty "ITChar" = FArith (ATInt ITChar)

378−mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))

409+ mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))

379−mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))

410+ mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))

380−mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))

411+ mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))

381−mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))

412+ mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))

382−

413+

383−zname = sNS (sUN "Z") ["Nat","Prelude"]

414+irTree :: [Name] -> SC -> Idris LExp

384−sname = sNS (sUN "S") ["Nat","Prelude"]

415+irTree args tree = do

385−

386−instance ToIR ([Name], SC) where

387− ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree

416+ logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree

388− tree' <- ir tree

389− return $ LLam args tree'

417+ LLam args <$> irSC M.empty tree

390−

418+

391−instance ToIR SC where

419+irSC :: Vars -> SC -> Idris LExp

392− ir t = ir' t where

393−

394− ir' (STerm t) = ir t

420+irSC vs (STerm t) = irTerm vs [] t

395− ir' (UnmatchedCase str) = return $ LError str

421+irSC vs (UnmatchedCase str) = return $ LError str

396− ir' (ProjCase tm alt) = do tm' <- ir tm

422+irSC vs (ProjCase tm alt) = do

423+ tm' <- irTerm vs [] tm

397− alt' <- mkIRAlt tm' alt

424+ alt' <- irAlt vs tm' alt

398− return $ LCase tm' [alt']

425+ return $ LCase tm' [alt']

399−

426+

400− -- There are two transformations in this case:

427+-- There are two transformations in this case:

401− --

428+--

402− -- 1. Newtype-case elimination:

429+-- 1. Newtype-case elimination:

403− -- case {e0} of

430+-- case {e0} of

404− -- wrap({e1}) -> P({e1}) ==> P({e0})

431+-- wrap({e1}) -> P({e1}) ==> P({e0})

405− --

432+--

406− -- This is important because newtyped constructors are compiled away entirely

433+-- This is important because newtyped constructors are compiled away entirely

407− -- and we need to do that everywhere.

434+-- and we need to do that everywhere.

408− --

435+--

409− -- 2. Unused-case elimination:

436+-- 2. Unused-case elimination:

410− -- case {e0} of ==> P

437+-- case {e0} of ==> P

411− -- C(x,y) -> P[... x,y not used ...]

438+-- C(x,y) -> P[... x,y not used ...]

412− --

439+--

413− -- This is important for runtime because sometimes we case on irrelevant data:

440+-- This is important for runtime because sometimes we case on irrelevant data:

414− --

441+--

415− -- In the example above, {e0} will most probably have been erased

442+-- In the example above, {e0} will most probably have been erased

416− -- so this vain projection would make the resulting program segfault

443+-- so this vain projection would make the resulting program segfault

417− -- because the code generator still emits a PROJECT(...) STG instruction.

444+-- because the code generator still emits a PROJECT(...) STG instruction.

418− --

445+--

419− -- Hence, we check whether the variables are used at all

446+-- Hence, we check whether the variables are used at all

420− -- and erase the casesplit if they are not.

447+-- and erase the casesplit if they are not.

421− ir' (Case n [alt]) = do

448+irSC vs (Case n [alt]) = do

422− replacement <- case alt of

449+ replacement <- case alt of

423− ConCase cn a ns sc -> do

450+ ConCase cn a ns sc -> do

424− detag <- maybe False detaggable . lookupCtxtExact cn . idris_optimisation <$> getIState

451+ detag <- maybe False detaggable . lookupCtxtExact cn . idris_optimisation <$> getIState

425− used <- maybe [] (map fst . usedpos) . lookupCtxtExact cn . idris_callgraph <$> getIState

452+ used <- maybe [] (map fst . usedpos) . lookupCtxtExact cn . idris_callgraph <$> getIState

426− if detag && length used == 1

453+ if detag && length used == 1

427− then return . Just $ substSC (ns !! head used) n sc

454+ then return . Just $ substSC (ns !! head used) n sc

428− else return Nothing

455+ else return Nothing

429− _ -> return Nothing

456+ _ -> return Nothing

430−

457+

431− case replacement of

458+ case replacement of

432− Just sc -> ir' sc

459+ Just sc -> irSC vs sc

433− _ -> do

460+ _ -> do

434− alt' <- mkIRAlt (LV (Glob n)) alt

461+ alt' <- irAlt vs (LV (Glob n)) alt

435− return $ case namesBoundIn alt' `usedIn` subexpr alt' of

462+ return $ case namesBoundIn alt' `usedIn` subexpr alt' of

436− [] -> subexpr alt' -- strip the unused top-most case

463+ [] -> subexpr alt' -- strip the unused top-most case

437− _ -> LCase (LV (Glob n)) [alt']

464+ _ -> LCase (LV (Glob n)) [alt']

438− where

465+ where

439− namesBoundIn :: LAlt -> [Name]

466+ namesBoundIn :: LAlt -> [Name]

440− namesBoundIn (LConCase cn i ns sc) = ns

467+ namesBoundIn (LConCase cn i ns sc) = ns

441− namesBoundIn (LConstCase c sc) = []

468+ namesBoundIn (LConstCase c sc) = []

442− namesBoundIn (LDefaultCase sc) = []

469+ namesBoundIn (LDefaultCase sc) = []

443−

470+

444− subexpr :: LAlt -> LExp

471+ subexpr :: LAlt -> LExp

445− subexpr (LConCase _ _ _ e) = e

472+ subexpr (LConCase _ _ _ e) = e

446− subexpr (LConstCase _ e) = e

473+ subexpr (LConstCase _ e) = e

447− subexpr (LDefaultCase e) = e

474+ subexpr (LDefaultCase e) = e

448−

475+

449− ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts

476+irSC vs (Case n alts) = LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts

450− return $ LCase (LV (Glob n)) alts'

451− ir' ImpossibleCase = return LNothing

477+irSC vs ImpossibleCase = return LNothing

452−

478+

479+-- zname = sNS (sUN "Z") ["Nat","Prelude"]

480+-- sname = sNS (sUN "S") ["Nat","Prelude"]

481+

453− -- special cases for Z and S

482+-- special cases for Z and S

454− -- Needs rethink: projections make this fail

483+-- Needs rethink: projections make this fail

455−-- mkIRAlt n (ConCase z _ [] rhs) | z == zname

484+-- irAlt n (ConCase z _ [] rhs) | z == zname

456−-- = mkIRAlt n (ConstCase (BI 0) rhs)

485+-- = irAlt n (ConstCase (BI 0) rhs)

457−-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname

486+-- irAlt n (ConCase s _ [arg] rhs) | s == sname

458-- = do n' <- ir n

487-- = do n' <- ir n

459-- rhs' <- ir rhs

488-- rhs' <- ir rhs

460-- return $ LDefaultCase

489-- return $ LDefaultCase

461-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])

490-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])

462-- rhs')

491-- rhs')

463− mkIRAlt _ (ConCase n t args sc) = do

464− sc' <- ir sc

465− used <- maybe [] (map fst . usedpos) . lookupCtxtExact n . idris_callgraph <$> getIState

466− return $ LConCase (-1) n [a | (i,a) <- zip [0..] args, i `elem` used] sc'

467−

468− mkIRAlt _ (ConstCase x rhs)

469− | matchable x

470− = do rhs' <- ir rhs

471− return $ LConstCase x rhs'

472− | matchableTy x

473− = do rhs' <- ir rhs

474− return $ LDefaultCase rhs'

475− mkIRAlt tm (SucCase n rhs)

476− = do rhs' <- ir rhs

477− return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))

478− [tm,

479− LConst (BI 1)]) rhs')

480−-- return $ LSucCase n rhs'

481− mkIRAlt _ (ConstCase c rhs)

482− = ifail $ "Can't match on (" ++ show c ++ ")"

483− mkIRAlt _ (DefaultCase rhs)

484− = do rhs' <- ir rhs

485− return $ LDefaultCase rhs'

486−

487− matchable (I _) = True

488− matchable (BI _) = True

489− matchable (Ch _) = True

490− matchable (Str _) = True

491− matchable _ = False

492−

493− matchableTy (AType (ATInt ITNative)) = True

494− matchableTy (AType (ATInt ITBig)) = True

495− matchableTy (AType (ATInt ITChar)) = True

496− matchableTy StrType = True

497−

498− matchableTy (AType (ATInt (ITFixed IT8))) = True

499− matchableTy (AType (ATInt (ITFixed IT16))) = True

500− matchableTy (AType (ATInt (ITFixed IT32))) = True

501− matchableTy (AType (ATInt (ITFixed IT64))) = True

502−

503− matchableTy _ = False

504

492

493+irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt

494+

495+-- this leaves out all unused arguments of the constructor

496+irAlt vs _ (ConCase n t args sc) = do

497+ sc' <- irSC vs sc

498+ used <- maybe [] (map fst . usedpos) . lookupCtxtExact n . idris_callgraph <$> getIState

499+ return $ LConCase (-1) n [a | (i,a) <- zip [0..] args, i `elem` used] sc'

500+

501+irAlt vs _ (ConstCase x rhs)

502+ | matchable x = LConstCase x <$> irSC vs rhs

503+ | matchableTy x = LDefaultCase <$> irSC vs rhs

504+ where

505+ matchable (I _) = True

506+ matchable (BI _) = True

507+ matchable (Ch _) = True

508+ matchable (Str _) = True

509+ matchable _ = False

510+

511+ matchableTy (AType (ATInt ITNative)) = True

512+ matchableTy (AType (ATInt ITBig)) = True

513+ matchableTy (AType (ATInt ITChar)) = True

514+ matchableTy StrType = True

515+

516+ matchableTy (AType (ATInt (ITFixed IT8))) = True

517+ matchableTy (AType (ATInt (ITFixed IT16))) = True

518+ matchableTy (AType (ATInt (ITFixed IT32))) = True

519+ matchableTy (AType (ATInt (ITFixed IT64))) = True

520+

521+ matchableTy _ = False

522+

523+irAlt vs tm (SucCase n rhs) = do

524+ rhs' <- irSC vs rhs

525+ return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))

526+ [tm,

527+ LConst (BI 1)]) rhs')

528+

529+irAlt vs _ (ConstCase c rhs)

530+ = ifail $ "Can't match on (" ++ show c ++ ")"

531+

532+irAlt vs _ (DefaultCase rhs)

533+ = LDefaultCase <$> irSC vs rhs