f7f8d92 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Tail calls via trampolines in C back end

f7f8d92Edwin Brady8 years ago

rts/idris_main.c+1−1

compare with master

unifiedsplit

@@ -3,7 +3,7 @@

3#include "idris_rts.h"

4#include "idris_stats.h"

6−void _idris__123_runMain_95_0_125_(VM* vm, VAL* oldbase);

6+void* _idris__123_runMain_95_0_125_(VM* vm, VAL* oldbase);

8#ifdef _WIN32

rts/idris_rts.h+10−5

@@ -212,7 +212,7 @@ void init_threadkeys(void);

212

213// Functions all take a pointer to their VM, and previous stack base,

214// and return nothing.

215−typedef void(*func)(VM*, VAL*);

215+typedef void*(*func)(VM*, VAL*);

216

217// Register access

218

@@ -282,9 +282,10 @@ typedef intptr_t i_int;

282#endif

283

284#define INITFRAME TRACE\

285− __attribute__((unused)) VAL* myoldbase

285+ __attribute__((unused)) VAL* myoldbase;\

286+ void* callres

286

287

287−#define REBASE vm->valstack_base = oldbase

288+#define REBASE vm->valstack_base = oldbase; return NULL

288#define RESERVE(x) do { \

289#define RESERVE(x) do { \

289 if (vm->valstack_top+(x) > vm->stack_max) { stackOverflow(); } \

290 if (vm->valstack_top+(x) > vm->stack_max) { stackOverflow(); } \

290 else { memset(vm->valstack_top, 0, (x)*sizeof(VAL)); } \

291 else { memset(vm->valstack_top, 0, (x)*sizeof(VAL)); } \

@@ -293,8 +294,12 @@ typedef intptr_t i_int;

293#define TOPBASE(x) vm->valstack_top = vm->valstack_base + (x)

294#define TOPBASE(x) vm->valstack_top = vm->valstack_base + (x)

294#define BASETOP(x) vm->valstack_base = vm->valstack_top + (x)

295#define BASETOP(x) vm->valstack_base = vm->valstack_top + (x)

295#define STOREOLD myoldbase = vm->valstack_base

296#define STOREOLD myoldbase = vm->valstack_base

297+

296−#define CALL(f) f(vm, myoldbase);

298+#define CALL(f) callres = f(vm, myoldbase); \

299+ while(callres!=NULL) { \

300+ callres = ((func)(callres))(vm, myoldbase); \

301+ }

297−#define TAILCALL(f) f(vm, oldbase);

302+#define TAILCALL(f) return (void*)(f);

298

303

299// Creating new values (each value placed at the top of the stack)

304// Creating new values (each value placed at the top of the stack)

300VAL MKFLOAT(VM* vm, double val);

305VAL MKFLOAT(VM* vm, double val);

src/IRTS/CodegenC.hs+56−57

@@ -117,11 +117,7 @@ gccFlags i = if i then ["-fwrapv"]

117 else ["-fwrapv", "-fno-strict-overflow"]

118

119gccDbg DEBUG = ["-g"]

120−-- clang optimises sibling calls in O1, but gcc doesn't

120+gccDbg _ = []

121−-- on the other hand, O1 compiles significantly faster in clang without

122−-- any noticeable performance hit.

123−gccDbg TRACE = ["-O1", "-foptimize-sibling-calls"]

124−gccDbg _ = ["-O1", "-foptimize-sibling-calls"]

125

121

126cname :: Name -> String

122cname :: Name -> String

127cname n = "_idris_" ++ concatMap cchar (showCG n)

123cname n = "_idris_" ++ concatMap cchar (showCG n)

@@ -137,14 +133,14 @@ creg (T i) = "TOP(" ++ show i ++ ")"

137creg Tmp = "REG1"

133creg Tmp = "REG1"

138

134

139toDecl :: Name -> String

135toDecl :: Name -> String

140−toDecl f = "void " ++ cname f ++ "(VM*, VAL*);\n"

136+toDecl f = "void* " ++ cname f ++ "(VM*, VAL*);\n"

141

137

142toC :: Name -> [BC] -> String

138toC :: Name -> [BC] -> String

143toC f code

139toC f code

144 = -- "/* " ++ show code ++ "*/\n\n" ++

140 = -- "/* " ++ show code ++ "*/\n\n" ++

145− "void " ++ cname f ++ "(VM* vm, VAL* oldbase) {\n" ++

141+ "void* " ++ cname f ++ "(VM* vm, VAL* oldbase) {\n" ++

146− indent 1 ++ "INITFRAME;\n" ++

142+ indent 1 ++ "INITFRAME;\nloop:\n" ++

147− concatMap (bcc 1) code ++ "}\n\n"

143+ concatMap (bcc f 1) code ++ "}\n\n"

148

144

149showCStr :: String -> String

145showCStr :: String -> String

150showCStr s = '"' : foldr ((++) . showChar) "\"" s

146showCStr s = '"' : foldr ((++) . showChar) "\"" s

@@ -180,9 +176,9 @@ showCStr s = '"' : foldr ((++) . showChar) "\"" s

180 2 -> s

176 2 -> s

181 _ -> error $ "Can't happen: String of invalid length " ++ show s

177 _ -> error $ "Can't happen: String of invalid length " ++ show s

182

178

183−bcc :: Int -> BC -> String

179+bcc :: Name -> Int -> BC -> String

184−bcc i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"

180+bcc f i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"

185−bcc i (ASSIGNCONST l c)

181+bcc f i (ASSIGNCONST l c)

186 = indent i ++ creg l ++ " = " ++ mkConst c ++ ";\n"

182 = indent i ++ creg l ++ " = " ++ mkConst c ++ ";\n"

187 where

183 where

188 mkConst (I i) = "MKINT(" ++ show i ++ ")"

184 mkConst (I i) = "MKINT(" ++ show i ++ ")"

@@ -203,10 +199,10 @@ bcc i (ASSIGNCONST l c)

203 mkConst c | isTypeConst c = "MKINT(42424242)"

199 mkConst c | isTypeConst c = "MKINT(42424242)"

204 mkConst c = error $ "mkConst of (" ++ show c ++ ") not implemented"

200 mkConst c = error $ "mkConst of (" ++ show c ++ ") not implemented"

205

201

206−bcc i (UPDATE l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"

202+bcc f i (UPDATE l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"

207−bcc i (MKCON l loc tag []) | tag < 256

203+bcc f i (MKCON l loc tag []) | tag < 256

208 = indent i ++ creg l ++ " = NULL_CON(" ++ show tag ++ ");\n"

204 = indent i ++ creg l ++ " = NULL_CON(" ++ show tag ++ ");\n"

209−bcc i (MKCON l loc tag args)

205+bcc f i (MKCON l loc tag args)

210 = indent i ++ alloc loc tag ++

206 = indent i ++ alloc loc tag ++

211 indent i ++ setArgs 0 args ++ "\n" ++

207 indent i ++ setArgs 0 args ++ "\n" ++

212 indent i ++ creg l ++ " = " ++ creg Tmp ++ ";\n"

208 indent i ++ creg l ++ " = " ++ creg Tmp ++ ";\n"

@@ -220,21 +216,21 @@ bcc i (MKCON l loc tag args)

220 = "updateCon(" ++ creg Tmp ++ ", " ++ creg old ++ ", " ++ show tag ++ ", " ++

216 = "updateCon(" ++ creg Tmp ++ ", " ++ creg old ++ ", " ++ show tag ++ ", " ++

221 show (length args) ++ ");\n"

217 show (length args) ++ ");\n"

222

218

223−bcc i (PROJECT l loc a) = indent i ++ "PROJECT(vm, " ++ creg l ++ ", " ++ show loc ++

219+bcc f i (PROJECT l loc a) = indent i ++ "PROJECT(vm, " ++ creg l ++ ", " ++ show loc ++

224 ", " ++ show a ++ ");\n"

220 ", " ++ show a ++ ");\n"

225−bcc i (PROJECTINTO r t idx)

221+bcc f i (PROJECTINTO r t idx)

226 = indent i ++ creg r ++ " = GETARG(" ++ creg t ++ ", " ++ show idx ++ ");\n"

222 = indent i ++ creg r ++ " = GETARG(" ++ creg t ++ ", " ++ show idx ++ ");\n"

227−bcc i (CASE True r [(_, alt)] Nothing)

223+bcc f i (CASE True r [(_, alt)] Nothing)

228 = indent i ++ showCode i alt

224 = indent i ++ showCode i alt

229 where

225 where

230 showCode :: Int -> [BC] -> String

226 showCode :: Int -> [BC] -> String

231− showCode i bc = "{\n" ++ concatMap (bcc (i + 1)) bc ++

227+ showCode i bc = "{\n" ++ concatMap (bcc f (i + 1)) bc ++

232 indent i ++ "}\n"

228 indent i ++ "}\n"

233−bcc i (CASE True r code def)

229+bcc f i (CASE True r code def)

234 | length code < 6 && length code > 1 = showCase i def code

230 | length code < 6 && length code > 1 = showCase i def code

235 where

231 where

236 showCode :: Int -> [BC] -> String

232 showCode :: Int -> [BC] -> String

237− showCode i bc = "{\n" ++ concatMap (bcc (i + 1)) bc ++

233+ showCode i bc = "{\n" ++ concatMap (bcc f (i + 1)) bc ++

238 indent i ++ "}\n"

234 indent i ++ "}\n"

239

235

240 showCase :: Int -> Maybe [BC] -> [(Int, [BC])] -> String

236 showCase :: Int -> Maybe [BC] -> [(Int, [BC])] -> String

@@ -244,7 +240,7 @@ bcc i (CASE True r code def)

244 = indent i ++ "if (CTAG(" ++ creg r ++ ") == " ++ show t ++ ") " ++ showCode i c

240 = indent i ++ "if (CTAG(" ++ creg r ++ ") == " ++ show t ++ ") " ++ showCode i c

245 ++ indent i ++ "else\n" ++ showCase i def cs

241 ++ indent i ++ "else\n" ++ showCase i def cs

246

242

247−bcc i (CASE safe r code def)

243+bcc f i (CASE safe r code def)

248 = indent i ++ "switch(" ++ ctag safe ++ "(" ++ creg r ++ ")) {\n" ++

244 = indent i ++ "switch(" ++ ctag safe ++ "(" ++ creg r ++ ")) {\n" ++

249 concatMap (showCase i) code ++

245 concatMap (showCase i) code ++

250 showDef i def ++

246 showDef i def ++

@@ -254,11 +250,12 @@ bcc i (CASE safe r code def)

254 ctag False = "TAG"

250 ctag False = "TAG"

255

251

256 showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"

252 showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"

257− ++ concatMap (bcc (i+1)) bc ++ indent (i + 1) ++ "break;\n"

253+ ++ concatMap (bcc f (i+1)) bc ++ indent (i + 1) ++ "break;\n"

258− showDef i Nothing = ""

254+ showDef i Nothing = indent i ++ "default:\n" ++

255+ indent (i + 1) ++ "return NULL;\n"

259 showDef i (Just c) = indent i ++ "default:\n"

256 showDef i (Just c) = indent i ++ "default:\n"

260− ++ concatMap (bcc (i+1)) c ++ indent (i + 1) ++ "break;\n"

257+ ++ concatMap (bcc f (i+1)) c ++ indent (i + 1) ++ "break;\n"

261−bcc i (CONSTCASE r code def)

258+bcc f i (CONSTCASE r code def)

262 | intConsts code

259 | intConsts code

263-- = indent i ++ "switch(GETINT(" ++ creg r ++ ")) {\n" ++

260-- = indent i ++ "switch(GETINT(" ++ creg r ++ ")) {\n" ++

264-- concatMap (showCase i) code ++

261-- concatMap (showCase i) code ++

@@ -290,65 +287,67 @@ bcc i (CONSTCASE r code def)

290

287

291 strCase sv (s, bc) =

288 strCase sv (s, bc) =

292 indent i ++ "if (strcmp(" ++ sv ++ ", " ++ show s ++ ") == 0) {\n" ++

289 indent i ++ "if (strcmp(" ++ sv ++ ", " ++ show s ++ ") == 0) {\n" ++

293− concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"

290+ concatMap (bcc f (i+1)) bc ++ indent i ++ "} else\n"

294 biCase bv (BI b, bc) =

291 biCase bv (BI b, bc) =

295 indent i ++ "if (bigEqConst(" ++ bv ++ ", " ++ show b ++ ")) {\n"

292 indent i ++ "if (bigEqConst(" ++ bv ++ ", " ++ show b ++ ")) {\n"

296− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"

293+ ++ concatMap (bcc f (i+1)) bc ++ indent i ++ "} else\n"

297 iCase v (I b, bc) =

294 iCase v (I b, bc) =

298 indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show b ++ ") {\n"

295 indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show b ++ ") {\n"

299− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"

296+ ++ concatMap (bcc f (i+1)) bc ++ indent i ++ "} else\n"

300 iCase v (Ch b, bc) =

297 iCase v (Ch b, bc) =

301 indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show (fromEnum b) ++ ") {\n"

298 indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show (fromEnum b) ++ ") {\n"

302− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"

299+ ++ concatMap (bcc f (i+1)) bc ++ indent i ++ "} else\n"

303 iCase v (B8 w, bc) =

300 iCase v (B8 w, bc) =

304 indent i ++ "if (GETBITS8(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"

301 indent i ++ "if (GETBITS8(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"

305− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"

302+ ++ concatMap (bcc f (i+1)) bc ++ indent i ++ "} else\n"

306 iCase v (B16 w, bc) =

303 iCase v (B16 w, bc) =

307 indent i ++ "if (GETBITS16(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"

304 indent i ++ "if (GETBITS16(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"

308− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"

305+ ++ concatMap (bcc f (i+1)) bc ++ indent i ++ "} else\n"

309 iCase v (B32 w, bc) =

306 iCase v (B32 w, bc) =

310 indent i ++ "if (GETBITS32(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"

307 indent i ++ "if (GETBITS32(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"

311− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"

308+ ++ concatMap (bcc f (i+1)) bc ++ indent i ++ "} else\n"

312 iCase v (B64 w, bc) =

309 iCase v (B64 w, bc) =

313 indent i ++ "if (GETBITS64(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"

310 indent i ++ "if (GETBITS64(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"

314− ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"

311+ ++ concatMap (bcc f (i+1)) bc ++ indent i ++ "} else\n"

315 showDefS i Nothing = ""

312 showDefS i Nothing = ""

316− showDefS i (Just c) = concatMap (bcc (i+1)) c

313+ showDefS i (Just c) = concatMap (bcc f (i+1)) c

317−

314+

318−bcc i (CALL n) = indent i ++ "CALL(" ++ cname n ++ ");\n"

315+bcc f i (CALL n) = indent i ++ "CALL(" ++ cname n ++ ");\n"

319−bcc i (TAILCALL n) = indent i ++ "TAILCALL(" ++ cname n ++ ");\n"

316+bcc f i (TAILCALL n)

317+ | f == n = indent i ++ "goto loop;\n"

318+ | otherwise = indent i ++ "TAILCALL(" ++ cname n ++ ");\n"

320−bcc i (SLIDE n) = indent i ++ "SLIDE(vm, " ++ show n ++ ");\n"

319+bcc f i (SLIDE n) = indent i ++ "SLIDE(vm, " ++ show n ++ ");\n"

321−bcc i REBASE = indent i ++ "REBASE;\n"

320+bcc f i REBASE = indent i ++ "REBASE;\n"

322−bcc i (RESERVE 0) = ""

321+bcc f i (RESERVE 0) = ""

323−bcc i (RESERVE n) = indent i ++ "RESERVE(" ++ show n ++ ");\n"

322+bcc f i (RESERVE n) = indent i ++ "RESERVE(" ++ show n ++ ");\n"

324−bcc i (ADDTOP 0) = ""

323+bcc f i (ADDTOP 0) = ""

325−bcc i (ADDTOP n) = indent i ++ "ADDTOP(" ++ show n ++ ");\n"

324+bcc f i (ADDTOP n) = indent i ++ "ADDTOP(" ++ show n ++ ");\n"

326−bcc i (TOPBASE n) = indent i ++ "TOPBASE(" ++ show n ++ ");\n"

325+bcc f i (TOPBASE n) = indent i ++ "TOPBASE(" ++ show n ++ ");\n"

327−bcc i (BASETOP n) = indent i ++ "BASETOP(" ++ show n ++ ");\n"

326+bcc f i (BASETOP n) = indent i ++ "BASETOP(" ++ show n ++ ");\n"

328−bcc i STOREOLD = indent i ++ "STOREOLD;\n"

327+bcc f i STOREOLD = indent i ++ "STOREOLD;\n"

329−bcc i (OP l fn args) = indent i ++ doOp (creg l ++ " = ") fn args ++ ";\n"

328+bcc f i (OP l fn args) = indent i ++ doOp (creg l ++ " = ") fn args ++ ";\n"

330−bcc i (FOREIGNCALL l rty (FStr ('#':name)) [])

329+bcc f i (FOREIGNCALL l rty (FStr ('#':name)) [])

331 = indent i ++

330 = indent i ++

332 c_irts (toFType rty) (creg l ++ " = ") name ++ ";\n"

331 c_irts (toFType rty) (creg l ++ " = ") name ++ ";\n"

333−bcc i (FOREIGNCALL l rty (FStr fn@('&':name)) [])

332+bcc f i (FOREIGNCALL l rty (FStr fn@('&':name)) [])

334 = indent i ++

333 = indent i ++

335 c_irts (toFType rty) (creg l ++ " = ") fn ++ ";\n"

334 c_irts (toFType rty) (creg l ++ " = ") fn ++ ";\n"

336−bcc i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%wrapper"

335+bcc f i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%wrapper"

337 = indent i ++

336 = indent i ++

338 c_irts (toFType rty) (creg l ++ " = ")

337 c_irts (toFType rty) (creg l ++ " = ")

339 ("_idris_get_wrapper(" ++ creg (snd x) ++ ")") ++ ";\n"

338 ("_idris_get_wrapper(" ++ creg (snd x) ++ ")") ++ ";\n"

340−bcc i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%dynamic"

339+bcc f i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%dynamic"

341 = indent i ++ c_irts (toFType rty) (creg l ++ " = ")

340 = indent i ++ c_irts (toFType rty) (creg l ++ " = ")

342 ("(*(" ++ cFnSig "" rty xs ++ ") GETPTR(" ++ creg (snd x) ++ "))" ++

341 ("(*(" ++ cFnSig "" rty xs ++ ") GETPTR(" ++ creg (snd x) ++ "))" ++

343 "(" ++ showSep "," (map fcall xs) ++ ")") ++ ";\n"

342 "(" ++ showSep "," (map fcall xs) ++ ")") ++ ";\n"

344−bcc i (FOREIGNCALL l rty (FStr fn) args)

343+bcc f i (FOREIGNCALL l rty (FStr fn) args)

345 = indent i ++

344 = indent i ++

346 c_irts (toFType rty) (creg l ++ " = ")

345 c_irts (toFType rty) (creg l ++ " = ")

347 (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"

346 (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"

348−bcc i (FOREIGNCALL l rty _ args) = error "Foreign Function calls cannot be partially applied, without being inlined."

347+bcc f i (FOREIGNCALL l rty _ args) = error "Foreign Function calls cannot be partially applied, without being inlined."

349−bcc i (NULL r) = indent i ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed

348+bcc f i (NULL r) = indent i ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed

350−bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1);\n"

349+bcc f i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1);\n"

351−-- bcc i c = error (show c) -- indent i ++ "// not done yet\n"

350+-- bcc f i c = error (show c) -- indent i ++ "// not done yet\n"

352

351

353fcall (t, arg) = irts_c (toFType t) (creg arg)

352fcall (t, arg) = irts_c (toFType t) (creg arg)

354-- Deconstruct the Foreign type in the defunctionalised expression and build

353-- Deconstruct the Foreign type in the defunctionalised expression and build

src/IRTS/LangOpts.hs+18−9

@@ -113,6 +113,8 @@ eval stk env rec defs (LProj exp i)

113 = unload stk <$> (LProj <$> eval [] env rec defs exp <*> return i)

114eval stk env rec defs (LCon loc i n es)

115 = unload stk <$> (LCon loc i n <$> mapM (eval [] env rec defs) es)

116+eval stk env rec defs (LCase ty e [])

117+ = pure LNothing

116eval stk env rec defs (LCase ty e alts)

118eval stk env rec defs (LCase ty e alts)

117 = do e' <- eval [] env rec defs e

119 = do e' <- eval [] env rec defs e

118 case evalAlts e' alts of

120 case evalAlts e' alts of

@@ -184,19 +186,24 @@ apply stk env rec defs var args body

184 = eval stk env rec defs (LLam args body)

186 = eval stk env rec defs (LLam args body)

185

187

186dropArgs :: [Name] -> LAlt -> State Int LAlt

188dropArgs :: [Name] -> LAlt -> State Int LAlt

187−dropArgs as (LConCase i n es (LLam args rhs))

189+dropArgs as (LConCase i n es t)

188− = do let old = take (length as) args

190+ = do rhs' <- dropArgsTm as t

189− rhs' <- eval [] (zipWith (\ o n -> (o, LV n)) old as) [] emptyContext rhs

190 return (LConCase i n es rhs')

191 return (LConCase i n es rhs')

191−dropArgs as (LConstCase c (LLam args rhs))

192+dropArgs as (LConstCase c t)

192− = do let old = take (length as) args

193+ = do rhs' <- dropArgsTm as t

193− rhs' <- eval [] (zipWith (\ o n -> (o, LV n)) old as) [] emptyContext rhs

194 return (LConstCase c rhs')

195−dropArgs as (LDefaultCase (LLam args rhs))

195+dropArgs as (LDefaultCase t)

196− = do let old = take (length as) args

196+ = do rhs' <- dropArgsTm as t

197− rhs' <- eval [] (zipWith (\ o n -> (o, LV n)) old as) [] emptyContext rhs

198 return (LDefaultCase rhs')

197 return (LDefaultCase rhs')

199

198

199+dropArgsTm as (LLam args rhs)

200+ = do let old = take (length as) args

201+ eval [] (zipWith (\ o n -> (o, LV n)) old as) [] emptyContext rhs

202+dropArgsTm as (LLet n val rhs)

203+ = do rhs' <- dropArgsTm as rhs

204+ pure (LLet n val rhs')

205+dropArgsTm as tm = return tm

206+

200caseFloat :: LExp -> LExp

207caseFloat :: LExp -> LExp

201caseFloat (LApp tc e es) = LApp tc (caseFloat e) (map caseFloat es)

208caseFloat (LApp tc e es) = LApp tc (caseFloat e) (map caseFloat es)

202caseFloat (LLazyExp e) = LLazyExp (caseFloat e)

209caseFloat (LLazyExp e) = LLazyExp (caseFloat e)

@@ -292,12 +299,14 @@ getRHS (LDefaultCase rhs) = rhs

292

299

293getLams [] = []

300getLams [] = []

294getLams (LLam args tm : cs) = getLamPrefix args cs

301getLams (LLam args tm : cs) = getLamPrefix args cs

302+getLams (LLet n val exp : cs) = getLams (exp : cs)

295getLams _ = []

303getLams _ = []

296

304

297getLamPrefix as [] = as

305getLamPrefix as [] = as

298getLamPrefix as (LLam args tm : cs)

306getLamPrefix as (LLam args tm : cs)

299 | length args < length as = getLamPrefix args cs

307 | length args < length as = getLamPrefix args cs

300 | otherwise = getLamPrefix as cs

308 | otherwise = getLamPrefix as cs

309+getLamPrefix as (LLet n val exp : cs) = getLamPrefix as (exp : cs)

301getLamPrefix as (_ : cs) = []

310getLamPrefix as (_ : cs) = []

302

311

303-- eta contract ('\x -> f x' can just be compiled as 'f' when f is local)

312-- eta contract ('\x -> f x' can just be compiled as 'f' when f is local)