src/IRTS/CodegenC.hs · Idris-dev

1{-|

2Module : IRTS.CodegenC

3Description : The default code generator for Idris, generating C code.

4Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8module IRTS.CodegenC (codegenC) where

9

10import Idris.AbsSyntax

11import IRTS.Bytecode

12import IRTS.Lang

13import IRTS.Simplified

14import IRTS.Defunctionalise

15import IRTS.System

16import IRTS.CodegenCommon

17import Idris.Core.TT

18import Util.System

19

20import Numeric

21import Data.Char

22import Data.Bits

23import Data.List (intercalate, nubBy)

24import System.Process

25import System.Exit

26import System.IO

27import System.Directory

28import System.FilePath ((</>), (<.>))

29import Control.Monad

30

31import Debug.Trace

32

33codegenC :: CodeGenerator

34codegenC ci = do codegenC' (simpleDecls ci)

35 (outputFile ci)

36 (outputType ci)

37 (includes ci)

38 (compileObjs ci)

39 (map mkLib (compileLibs ci) ++

40 map incdir (importDirs ci))

41 (compilerFlags ci)

42 (exportDecls ci)

43 (interfaces ci)

44 (debugLevel ci)

45 when (interfaces ci) $

46 codegenH (exportDecls ci)

47

48 where mkLib l = "-l" ++ l

49 incdir i = "-I" ++ i

50

51codegenC' :: [(Name, SDecl)]

52 -> String -- ^ output file name

53 -> OutputType -- ^ generate executable if True, only .o if False

54 -> [FilePath] -- ^ include files

55 -> [String] -- ^ extra object files

56 -> [String] -- ^ extra compiler flags (libraries)

57 -> [String] -- ^ extra compiler flags (anything)

58 -> [ExportIFace]

59 -> Bool -- ^ interfaces too (so make a .o instead)

60 -> DbgLevel

61 -> IO ()

62codegenC' defs out exec incs objs libs flags exports iface dbg

63 = do -- print defs

64 let bc = map toBC defs

65 let wrappers = genWrappers bc

66 let h = concatMap toDecl (map fst bc)

67 let cc = concatMap (uncurry toC) bc

68 let hi = concatMap ifaceC (concatMap getExp exports)

69 d <- getDataDir

70 mprog <- readFile (d </> "rts" </> "idris_main" <.> "c")

71 let cout = headers incs ++ debug dbg ++ h ++ wrappers ++ cc ++

72 (if (exec == Executable) then mprog else hi)

73 case exec of

74 Raw -> writeSource out cout

75 _ -> do

76 (tmpn, tmph) <- tempfile ".c"

77 hPutStr tmph cout

78 hFlush tmph

79 hClose tmph

80 comp <- getCC

81 libFlags <- getLibFlags

82 incFlags <- getIncFlags

83 envFlags <- getEnvFlags

84 let stackFlag = if isWindows then ["-Wl,--stack,16777216"] else []

85 let args = [gccDbg dbg] ++

86 gccFlags iface ++

87 -- # Any flags defined here which alter the RTS API must also be added to config.mk

88 ["-DHAS_PTHREAD", "-DIDRIS_ENABLE_STATS",

89 "-I."] ++ objs ++ envFlags ++

90 (if (exec == Executable) then [] else ["-c"]) ++

91 [tmpn] ++

92 (if not iface then libFlags else []) ++

93 incFlags ++

94 (if not iface then libs else []) ++

95 flags ++ stackFlag ++

96 ["-o", out]

97-- putStrLn (show args)

98 exit <- rawSystem comp args

99 when (exit /= ExitSuccess) $

100 putStrLn ("FAILURE: " ++ show comp ++ " " ++ show args)

101 where

102 getExp (Export _ _ exp) = exp

103

104headers xs =

105 concatMap

106 (\h -> "#include \"" ++ h ++ "\"\n")

107 (xs ++ ["idris_rts.h", "idris_bitstring.h", "idris_stdfgn.h"])

108

109debug TRACE = "#define IDRIS_TRACE\n\n"

110debug _ = ""

111

112-- We're using signed integers now. Make sure we get consistent semantics

113-- out of them from gcc. See e.g. http://thiemonagel.de/2010/01/signed-integer-overflow/

114gccFlags i = if i then ["-fwrapv"]

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

116

117gccDbg DEBUG = "-g"

118gccDbg TRACE = "-O2"

119gccDbg _ = "-O2"

120

121cname :: Name -> String

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

123 where cchar x | isAlpha x || isDigit x = [x]

124 | otherwise = "_" ++ show (fromEnum x) ++ "_"

125

126indent :: Int -> String

127indent n = replicate (n*4) ' '

128

129creg RVal = "RVAL"

130creg (L i) = "LOC(" ++ show i ++ ")"

131creg (T i) = "TOP(" ++ show i ++ ")"

132creg Tmp = "REG1"

133

134toDecl :: Name -> String

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

136

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

138toC f code

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

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

141 indent 1 ++ "INITFRAME;\n" ++

142 concatMap (bcc 1) code ++ "}\n\n"

143

144showCStr :: String -> String

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

146 where

147 showChar :: Char -> String

148 showChar '"' = "\\\""

149 showChar '\\' = "\\\\"

150 showChar c

151 -- Note: we need the double quotes around the codes because otherwise

152 -- "\n3" would get encoded as "\x0a3", which is incorrect.

153 -- Instead, we opt for "\x0a""3" and let the C compiler deal with it.

154 | ord c < 0x10 = "\"\"\\x0" ++ showHex (ord c) "\"\""

155 | ord c < 0x20 = "\"\"\\x" ++ showHex (ord c) "\"\""

156 | ord c < 0x7f = [c] -- 0x7f = \DEL

157 | otherwise = showHexes (utf8bytes (ord c))

158

159 utf8bytes :: Int -> [Int]

160 utf8bytes x = let (h : bytes) = split [] x in

161 headHex h (length bytes) : map toHex bytes

162 where

163 split acc 0 = acc

164 split acc x = let xbits = x .&. 0x3f

165 xrest = shiftR x 6 in

166 split (xbits : acc) xrest

167

168 headHex h 1 = h + 0xc0

169 headHex h 2 = h + 0xe0

170 headHex h 3 = h + 0xf0

171 headHex h n = error "Can't happen: Invalid UTF8 character"

172

173 toHex i = i + 0x80

174

175 showHexes = foldr ((++) . showUTF8) ""

176 showUTF8 c = "\"\"\\x" ++ showHex c "\"\""

177

178bcc :: Int -> BC -> String

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

180bcc i (ASSIGNCONST l c)

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

182 where

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

184 mkConst (BI i) | i < (2^30) = "MKINT(" ++ show i ++ ")"

185 | otherwise = "MKBIGC(vm,\"" ++ show i ++ "\")"

186 mkConst (Fl f) = "MKFLOAT(vm, " ++ show f ++ ")"

187 mkConst (Ch c) = "MKINT(" ++ show (fromEnum c) ++ ")"

188 mkConst (Str s) = "MKSTR(vm, " ++ showCStr s ++ ")"

189 mkConst (B8 x) = "idris_b8const(vm, " ++ show x ++ "U)"

190 mkConst (B16 x) = "idris_b16const(vm, " ++ show x ++ "U)"

191 mkConst (B32 x) = "idris_b32const(vm, " ++ show x ++ "UL)"

192 mkConst (B64 x) = "idris_b64const(vm, " ++ show x ++ "ULL)"

193 -- if it's a type constant, we won't use it, but equally it shouldn't

194 -- report an error. These might creep into generated for various reasons

195 -- (especially if erasure is disabled).

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

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

198

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

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

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

202bcc i (MKCON l loc tag args)

203 = indent i ++ alloc loc tag ++

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

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

206

207-- "MKCON(vm, " ++ creg l ++ ", " ++ show tag ++ ", " ++

208-- show (length args) ++ concatMap showArg args ++ ");\n"

209 where showArg r = ", " ++ creg r

210 setArgs i [] = ""

211 setArgs i (x : xs) = "SETARG(" ++ creg Tmp ++ ", " ++ show i ++ ", " ++ creg x ++

212 "); " ++ setArgs (i + 1) xs

213 alloc Nothing tag

214 = "allocCon(" ++ creg Tmp ++ ", vm, " ++ show tag ++ ", " ++

215 show (length args) ++ ", 0);\n"

216 alloc (Just old) tag

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

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

219

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

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

222bcc i (PROJECTINTO r t idx)

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

224bcc i (CASE True r code def)

225 | length code < 4 = showCase i def code

226 where

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

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

229 indent i ++ "}\n"

230

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

232 showCase i Nothing [(t, c)] = indent i ++ showCode i c

233 showCase i (Just def) [] = indent i ++ showCode i def

234 showCase i def ((t, c) : cs)

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

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

237

238bcc i (CASE safe r code def)

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

240 concatMap (showCase i) code ++

241 showDef i def ++

242 indent i ++ "}\n"

243 where

244 ctag True = "CTAG"

245 ctag False = "TAG"

246

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

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

249 showDef i Nothing = ""

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

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

252bcc i (CONSTCASE r code def)

253 | intConsts code

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

255-- concatMap (showCase i) code ++

256-- showDef i def ++

257-- indent i ++ "}\n"

258 = concatMap (iCase (creg r)) code ++

259 indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"

260 | strConsts code

261 = concatMap (strCase ("GETSTR(" ++ creg r ++ ")")) code ++

262 indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"

263 | bigintConsts code

264 = concatMap (biCase (creg r)) code ++

265 indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"

266 | otherwise = error $ "Can't happen: Can't compile const case " ++ show code

267 where

268 intConsts ((I _, _ ) : _) = True

269 intConsts ((Ch _, _ ) : _) = True

270 intConsts ((B8 _, _ ) : _) = True

271 intConsts ((B16 _, _ ) : _) = True

272 intConsts ((B32 _, _ ) : _) = True

273 intConsts ((B64 _, _ ) : _) = True

274 intConsts _ = False

275

276 bigintConsts ((BI _, _ ) : _) = True

277 bigintConsts _ = False

278

279 strConsts ((Str _, _ ) : _) = True

280 strConsts _ = False

281

282 strCase sv (s, bc) =

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

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

285 biCase bv (BI b, bc) =

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

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

288 iCase v (I b, bc) =

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

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

291 iCase v (Ch b, bc) =

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

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

294 iCase v (B8 w, bc) =

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

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

297 iCase v (B16 w, bc) =

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

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

300 iCase v (B32 w, bc) =

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

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

303 iCase v (B64 w, bc) =

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

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

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

307 ++ concatMap (bcc (i+1)) bc ++

308 indent (i + 1) ++ "break;\n"

309 showDef i Nothing = ""

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

311 ++ concatMap (bcc (i+1)) c ++

312 indent (i + 1) ++ "break;\n"

313 showDefS i Nothing = ""

314 showDefS i (Just c) = concatMap (bcc (i+1)) c

315

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

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

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

319bcc i REBASE = indent i ++ "REBASE;\n"

320bcc i (RESERVE 0) = ""

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

322bcc i (ADDTOP 0) = ""

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

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

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

326bcc i STOREOLD = indent i ++ "STOREOLD;\n"

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

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

329 = indent i ++

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

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

332 = indent i ++

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

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

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

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

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

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

339bcc i (FOREIGNCALL l rty (FStr fn) args)

340 = indent i ++

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

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

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

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

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

346

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

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

349-- a foreign type description for c_irts and irts_c

350toAType (FCon i)

351 | i == sUN "C_IntChar" = ATInt ITChar

352 | i == sUN "C_IntNative" = ATInt ITNative

353 | i == sUN "C_IntBits8" = ATInt (ITFixed IT8)

354 | i == sUN "C_IntBits16" = ATInt (ITFixed IT16)

355 | i == sUN "C_IntBits32" = ATInt (ITFixed IT32)

356 | i == sUN "C_IntBits64" = ATInt (ITFixed IT64)

357toAType t = error (show t ++ " not defined in toAType")

358

359toFType (FCon c)

360 | c == sUN "C_Str" = FString

361 | c == sUN "C_Float" = FArith ATFloat

362 | c == sUN "C_Ptr" = FPtr

363 | c == sUN "C_MPtr" = FManagedPtr

364 | c == sUN "C_CData" = FCData

365 | c == sUN "C_Unit" = FUnit

366toFType (FApp c [_,ity])

367 | c == sUN "C_IntT" = FArith (toAType ity)

368 | c == sUN "C_FnT" = toFunType ity

369toFType (FApp c [_])

370 | c == sUN "C_Any" = FAny

371toFType t = FAny

372

373toFunType (FApp c [_,ity])

374 | c == sUN "C_FnBase" = FFunction

375 | c == sUN "C_FnIO" = FFunctionIO

376toFunType (FApp c [_,_,_,ity])

377 | c == sUN "C_Fn" = toFunType ity

378toFunType _ = FAny

379

380c_irts (FArith (ATInt ITNative)) l x = l ++ "MKINT((i_int)(" ++ x ++ "))"

381c_irts (FArith (ATInt ITChar)) l x = c_irts (FArith (ATInt ITNative)) l x

382c_irts (FArith (ATInt (ITFixed ity))) l x

383 = l ++ "idris_b" ++ show (nativeTyWidth ity) ++ "const(vm, " ++ x ++ ")"

384c_irts FString l x = l ++ "MKSTR(vm, " ++ x ++ ")"

385c_irts FUnit l x = x

386c_irts FPtr l x = l ++ "MKPTR(vm, " ++ x ++ ")"

387c_irts FManagedPtr l x = l ++ "MKMPTR(vm, " ++ x ++ ")"

388c_irts (FArith ATFloat) l x = l ++ "MKFLOAT(vm, " ++ x ++ ")"

389c_irts FCData l x = l ++ "MKCDATA(vm, " ++ x ++ ")"

390c_irts FAny l x = l ++ x

391c_irts FFunction l x = error "Return of function from foreign call is not supported"

392c_irts FFunctionIO l x = error "Return of function from foreign call is not supported"

393

394irts_c (FArith (ATInt ITNative)) x = "GETINT(" ++ x ++ ")"

395irts_c (FArith (ATInt ITChar)) x = irts_c (FArith (ATInt ITNative)) x

396irts_c (FArith (ATInt (ITFixed ity))) x

397 = "(" ++ x ++ "->info.bits" ++ show (nativeTyWidth ity) ++ ")"

398irts_c FString x = "GETSTR(" ++ x ++ ")"

399irts_c FUnit x = x

400irts_c FPtr x = "GETPTR(" ++ x ++ ")"

401irts_c FManagedPtr x = "GETMPTR(" ++ x ++ ")"

402irts_c (FArith ATFloat) x = "GETFLOAT(" ++ x ++ ")"

403irts_c FCData x = "GETCDATA(" ++ x ++ ")"

404irts_c FAny x = x

405irts_c FFunctionIO x = wrapped x

406irts_c FFunction x = wrapped x

407

408cFnSig name rty [] = ctype rty ++ " (*" ++ name ++ ")(void) "

409cFnSig name rty args = ctype rty ++ " (*" ++ name ++ ")("

410 ++ showSep "," (map (ctype . fst) args) ++ ") "

411

412wrapped x = "_idris_get_wrapper(" ++ x ++ ")"

413

414bitOp v op ty args = v ++ "idris_b" ++ show (nativeTyWidth ty) ++ op ++ "(vm, " ++ intercalate ", " (map creg args) ++ ")"

415

416bitCoerce v op input output arg

417 = v ++ "idris_b" ++ show (nativeTyWidth input) ++ op ++ show (nativeTyWidth output) ++ "(vm, " ++ creg arg ++ ")"

418

419signedTy :: NativeTy -> String

420signedTy t = "int" ++ show (nativeTyWidth t) ++ "_t"

421

422doOp v (LPlus (ATInt ITNative)) [l, r] = v ++ "ADD(" ++ creg l ++ ", " ++ creg r ++ ")"

423doOp v (LMinus (ATInt ITNative)) [l, r] = v ++ "INTOP(-," ++ creg l ++ ", " ++ creg r ++ ")"

424doOp v (LTimes (ATInt ITNative)) [l, r] = v ++ "MULT(" ++ creg l ++ ", " ++ creg r ++ ")"

425doOp v (LUDiv ITNative) [l, r] = v ++ "UINTOP(/," ++ creg l ++ ", " ++ creg r ++ ")"

426doOp v (LSDiv (ATInt ITNative)) [l, r] = v ++ "INTOP(/," ++ creg l ++ ", " ++ creg r ++ ")"

427doOp v (LURem ITNative) [l, r] = v ++ "UINTOP(%," ++ creg l ++ ", " ++ creg r ++ ")"

428doOp v (LSRem (ATInt ITNative)) [l, r] = v ++ "INTOP(%," ++ creg l ++ ", " ++ creg r ++ ")"

429doOp v (LAnd ITNative) [l, r] = v ++ "INTOP(&," ++ creg l ++ ", " ++ creg r ++ ")"

430doOp v (LOr ITNative) [l, r] = v ++ "INTOP(|," ++ creg l ++ ", " ++ creg r ++ ")"

431doOp v (LXOr ITNative) [l, r] = v ++ "INTOP(^," ++ creg l ++ ", " ++ creg r ++ ")"

432doOp v (LSHL ITNative) [l, r] = v ++ "INTOP(<<," ++ creg l ++ ", " ++ creg r ++ ")"

433doOp v (LLSHR ITNative) [l, r] = v ++ "UINTOP(>>," ++ creg l ++ ", " ++ creg r ++ ")"

434doOp v (LASHR ITNative) [l, r] = v ++ "INTOP(>>," ++ creg l ++ ", " ++ creg r ++ ")"

435doOp v (LCompl ITNative) [x] = v ++ "INTOP(~," ++ creg x ++ ")"

436doOp v (LEq (ATInt ITNative)) [l, r] = v ++ "INTOP(==," ++ creg l ++ ", " ++ creg r ++ ")"

437doOp v (LSLt (ATInt ITNative)) [l, r] = v ++ "INTOP(<," ++ creg l ++ ", " ++ creg r ++ ")"

438doOp v (LSLe (ATInt ITNative)) [l, r] = v ++ "INTOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"

439doOp v (LSGt (ATInt ITNative)) [l, r] = v ++ "INTOP(>," ++ creg l ++ ", " ++ creg r ++ ")"

440doOp v (LSGe (ATInt ITNative)) [l, r] = v ++ "INTOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"

441doOp v (LLt ITNative) [l, r] = v ++ "UINTOP(<," ++ creg l ++ ", " ++ creg r ++ ")"

442doOp v (LLe ITNative) [l, r] = v ++ "UINTOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"

443doOp v (LGt ITNative) [l, r] = v ++ "UINTOP(>," ++ creg l ++ ", " ++ creg r ++ ")"

444doOp v (LGe ITNative) [l, r] = v ++ "UINTOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"

445

446doOp v (LPlus (ATInt ITChar)) [l, r] = doOp v (LPlus (ATInt ITNative)) [l, r]

447doOp v (LMinus (ATInt ITChar)) [l, r] = doOp v (LMinus (ATInt ITNative)) [l, r]

448doOp v (LTimes (ATInt ITChar)) [l, r] = doOp v (LTimes (ATInt ITNative)) [l, r]

449doOp v (LUDiv ITChar) [l, r] = doOp v (LUDiv ITNative) [l, r]

450doOp v (LSDiv (ATInt ITChar)) [l, r] = doOp v (LSDiv (ATInt ITNative)) [l, r]

451doOp v (LURem ITChar) [l, r] = doOp v (LURem ITNative) [l, r]

452doOp v (LSRem (ATInt ITChar)) [l, r] = doOp v (LSRem (ATInt ITNative)) [l, r]

453doOp v (LAnd ITChar) [l, r] = doOp v (LAnd ITNative) [l, r]

454doOp v (LOr ITChar) [l, r] = doOp v (LOr ITNative) [l, r]

455doOp v (LXOr ITChar) [l, r] = doOp v (LXOr ITNative) [l, r]

456doOp v (LSHL ITChar) [l, r] = doOp v (LSHL ITNative) [l, r]

457doOp v (LLSHR ITChar) [l, r] = doOp v (LLSHR ITNative) [l, r]

458doOp v (LASHR ITChar) [l, r] = doOp v (LASHR ITNative) [l, r]

459doOp v (LCompl ITChar) [x] = doOp v (LCompl ITNative) [x]

460doOp v (LEq (ATInt ITChar)) [l, r] = doOp v (LEq (ATInt ITNative)) [l, r]

461doOp v (LSLt (ATInt ITChar)) [l, r] = doOp v (LSLt (ATInt ITNative)) [l, r]

462doOp v (LSLe (ATInt ITChar)) [l, r] = doOp v (LSLe (ATInt ITNative)) [l, r]

463doOp v (LSGt (ATInt ITChar)) [l, r] = doOp v (LSGt (ATInt ITNative)) [l, r]

464doOp v (LSGe (ATInt ITChar)) [l, r] = doOp v (LSGe (ATInt ITNative)) [l, r]

465doOp v (LLt ITChar) [l, r] = doOp v (LLt ITNative) [l, r]

466doOp v (LLe ITChar) [l, r] = doOp v (LLe ITNative) [l, r]

467doOp v (LGt ITChar) [l, r] = doOp v (LGt ITNative) [l, r]

468doOp v (LGe ITChar) [l, r] = doOp v (LGe ITNative) [l, r]

469

470doOp v (LPlus ATFloat) [l, r] = v ++ "FLOATOP(+," ++ creg l ++ ", " ++ creg r ++ ")"

471doOp v (LMinus ATFloat) [l, r] = v ++ "FLOATOP(-," ++ creg l ++ ", " ++ creg r ++ ")"

472doOp v (LTimes ATFloat) [l, r] = v ++ "FLOATOP(*," ++ creg l ++ ", " ++ creg r ++ ")"

473doOp v (LSDiv ATFloat) [l, r] = v ++ "FLOATOP(/," ++ creg l ++ ", " ++ creg r ++ ")"

474doOp v (LEq ATFloat) [l, r] = v ++ "FLOATBOP(==," ++ creg l ++ ", " ++ creg r ++ ")"

475doOp v (LSLt ATFloat) [l, r] = v ++ "FLOATBOP(<," ++ creg l ++ ", " ++ creg r ++ ")"

476doOp v (LSLe ATFloat) [l, r] = v ++ "FLOATBOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"

477doOp v (LSGt ATFloat) [l, r] = v ++ "FLOATBOP(>," ++ creg l ++ ", " ++ creg r ++ ")"

478doOp v (LSGe ATFloat) [l, r] = v ++ "FLOATBOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"

479

480doOp v (LIntFloat ITBig) [x] = v ++ "idris_castBigFloat(vm, " ++ creg x ++ ")"

481doOp v (LFloatInt ITBig) [x] = v ++ "idris_castFloatBig(vm, " ++ creg x ++ ")"

482doOp v (LPlus (ATInt ITBig)) [l, r] = v ++ "idris_bigPlus(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

483doOp v (LMinus (ATInt ITBig)) [l, r] = v ++ "idris_bigMinus(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

484doOp v (LTimes (ATInt ITBig)) [l, r] = v ++ "idris_bigTimes(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

485doOp v (LSDiv (ATInt ITBig)) [l, r] = v ++ "idris_bigDivide(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

486doOp v (LSRem (ATInt ITBig)) [l, r] = v ++ "idris_bigMod(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

487doOp v (LAnd ITBig) [l, r] = v ++ "idris_bigAnd(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

488doOp v (LOr ITBig) [l, r] = v ++ "idris_bigOr(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

489doOp v (LSHL ITBig) [l, r] = v ++ "idris_bigShiftLeft(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

490doOp v (LLSHR ITBig) [l, r] = v ++ "idris_bigLShiftRight(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

491doOp v (LASHR ITBig) [l, r] = v ++ "idris_bigAShiftRight(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

492doOp v (LEq (ATInt ITBig)) [l, r] = v ++ "idris_bigEq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

493doOp v (LSLt (ATInt ITBig)) [l, r] = v ++ "idris_bigLt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

494doOp v (LSLe (ATInt ITBig)) [l, r] = v ++ "idris_bigLe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

495doOp v (LSGt (ATInt ITBig)) [l, r] = v ++ "idris_bigGt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

496doOp v (LSGe (ATInt ITBig)) [l, r] = v ++ "idris_bigGe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

497

498doOp v (LIntFloat ITNative) [x] = v ++ "idris_castIntFloat(" ++ creg x ++ ")"

499doOp v (LFloatInt ITNative) [x] = v ++ "idris_castFloatInt(" ++ creg x ++ ")"

500doOp v (LSExt ITNative ITBig) [x] = v ++ "idris_castIntBig(vm, " ++ creg x ++ ")"

501doOp v (LTrunc ITBig ITNative) [x] = v ++ "idris_castBigInt(vm, " ++ creg x ++ ")"

502doOp v (LStrInt ITBig) [x] = v ++ "idris_castStrBig(vm, " ++ creg x ++ ")"

503doOp v (LIntStr ITBig) [x] = v ++ "idris_castBigStr(vm, " ++ creg x ++ ")"

504doOp v (LIntStr ITNative) [x] = v ++ "idris_castIntStr(vm, " ++ creg x ++ ")"

505doOp v (LStrInt ITNative) [x] = v ++ "idris_castStrInt(vm, " ++ creg x ++ ")"

506doOp v (LIntStr (ITFixed _)) [x] = v ++ "idris_castBitsStr(vm, " ++ creg x ++ ")"

507doOp v LFloatStr [x] = v ++ "idris_castFloatStr(vm, " ++ creg x ++ ")"

508doOp v LStrFloat [x] = v ++ "idris_castStrFloat(vm, " ++ creg x ++ ")"

509

510doOp v (LSLt (ATInt (ITFixed ty))) [x, y] = bitOp v "SLt" ty [x, y]

511doOp v (LSLe (ATInt (ITFixed ty))) [x, y] = bitOp v "SLte" ty [x, y]

512doOp v (LEq (ATInt (ITFixed ty))) [x, y] = bitOp v "Eq" ty [x, y]

513doOp v (LSGe (ATInt (ITFixed ty))) [x, y] = bitOp v "SGte" ty [x, y]

514doOp v (LSGt (ATInt (ITFixed ty))) [x, y] = bitOp v "SGt" ty [x, y]

515doOp v (LLt (ITFixed ty)) [x, y] = bitOp v "Lt" ty [x, y]

516doOp v (LLe (ITFixed ty)) [x, y] = bitOp v "Lte" ty [x, y]

517doOp v (LGe (ITFixed ty)) [x, y] = bitOp v "Gte" ty [x, y]

518doOp v (LGt (ITFixed ty)) [x, y] = bitOp v "Gt" ty [x, y]

519

520doOp v (LSHL (ITFixed ty)) [x, y] = bitOp v "Shl" ty [x, y]

521doOp v (LLSHR (ITFixed ty)) [x, y] = bitOp v "LShr" ty [x, y]

522doOp v (LASHR (ITFixed ty)) [x, y] = bitOp v "AShr" ty [x, y]

523doOp v (LAnd (ITFixed ty)) [x, y] = bitOp v "And" ty [x, y]

524doOp v (LOr (ITFixed ty)) [x, y] = bitOp v "Or" ty [x, y]

525doOp v (LXOr (ITFixed ty)) [x, y] = bitOp v "Xor" ty [x, y]

526doOp v (LCompl (ITFixed ty)) [x] = bitOp v "Compl" ty [x]

527

528doOp v (LPlus (ATInt (ITFixed ty))) [x, y] = bitOp v "Plus" ty [x, y]

529doOp v (LMinus (ATInt (ITFixed ty))) [x, y] = bitOp v "Minus" ty [x, y]

530doOp v (LTimes (ATInt (ITFixed ty))) [x, y] = bitOp v "Times" ty [x, y]

531doOp v (LUDiv (ITFixed ty)) [x, y] = bitOp v "UDiv" ty [x, y]

532doOp v (LSDiv (ATInt (ITFixed ty))) [x, y] = bitOp v "SDiv" ty [x, y]

533doOp v (LURem (ITFixed ty)) [x, y] = bitOp v "URem" ty [x, y]

534doOp v (LSRem (ATInt (ITFixed ty))) [x, y] = bitOp v "SRem" ty [x, y]

535

536doOp v (LSExt (ITFixed from) ITBig) [x]

537 = v ++ "MKBIGSI(vm, (" ++ signedTy from ++ ")" ++ creg x ++ "->info.bits" ++ show (nativeTyWidth from) ++ ")"

538doOp v (LSExt ITNative (ITFixed to)) [x]

539 = v ++ "idris_b" ++ show (nativeTyWidth to) ++ "const(vm, GETINT(" ++ creg x ++ "))"

540doOp v (LSExt ITChar (ITFixed to)) [x]

541 = doOp v (LSExt ITNative (ITFixed to)) [x]

542doOp v (LSExt (ITFixed from) ITNative) [x]

543 = v ++ "MKINT((i_int)((" ++ signedTy from ++ ")" ++ creg x ++ "->info.bits" ++ show (nativeTyWidth from) ++ "))"

544doOp v (LSExt (ITFixed from) ITChar) [x]

545 = doOp v (LSExt (ITFixed from) ITNative) [x]

546doOp v (LSExt (ITFixed from) (ITFixed to)) [x]

547 | nativeTyWidth from < nativeTyWidth to = bitCoerce v "S" from to x

548doOp v (LZExt ITNative (ITFixed to)) [x]

549 = v ++ "idris_b" ++ show (nativeTyWidth to) ++ "const(vm, (uintptr_t)GETINT(" ++ creg x ++ "))"

550doOp v (LZExt ITChar (ITFixed to)) [x]

551 = doOp v (LZExt ITNative (ITFixed to)) [x]

552doOp v (LZExt (ITFixed from) ITNative) [x]

553 = v ++ "MKINT((i_int)" ++ creg x ++ "->info.bits" ++ show (nativeTyWidth from) ++ ")"

554doOp v (LZExt (ITFixed from) ITChar) [x]

555 = doOp v (LZExt (ITFixed from) ITNative) [x]

556doOp v (LZExt (ITFixed from) ITBig) [x]

557 = v ++ "MKBIGUI(vm, " ++ creg x ++ "->info.bits" ++ show (nativeTyWidth from) ++ ")"

558doOp v (LZExt ITNative ITBig) [x]

559 = v ++ "MKBIGUI(vm, (uintptr_t)GETINT(" ++ creg x ++ "))"

560doOp v (LZExt (ITFixed from) (ITFixed to)) [x]

561 | nativeTyWidth from < nativeTyWidth to = bitCoerce v "Z" from to x

562doOp v (LTrunc ITNative (ITFixed to)) [x]

563 = v ++ "idris_b" ++ show (nativeTyWidth to) ++ "const(vm, GETINT(" ++ creg x ++ "))"

564doOp v (LTrunc ITChar (ITFixed to)) [x]

565 = doOp v (LTrunc ITNative (ITFixed to)) [x]

566doOp v (LTrunc (ITFixed from) ITNative) [x]

567 = v ++ "MKINT((i_int)" ++ creg x ++ "->info.bits" ++ show (nativeTyWidth from) ++ ")"

568doOp v (LTrunc (ITFixed from) ITChar) [x]

569 = doOp v (LTrunc (ITFixed from) ITNative) [x]

570doOp v (LTrunc ITBig (ITFixed IT64)) [x]

571 = v ++ "idris_b64const(vm, ISINT(" ++ creg x ++ ") ? GETINT(" ++ creg x ++ ") : idris_truncBigB64(GETMPZ(" ++ creg x ++ ")))"

572doOp v (LTrunc ITBig (ITFixed to)) [x]

573 = v ++ "idris_b" ++ show (nativeTyWidth to) ++ "const(vm, ISINT(" ++ creg x ++ ") ? GETINT(" ++ creg x ++ ") : mpz_get_ui(GETMPZ(" ++ creg x ++ ")))"

574doOp v (LTrunc (ITFixed from) (ITFixed to)) [x]

575 | nativeTyWidth from > nativeTyWidth to = bitCoerce v "T" from to x

576

577doOp v LFExp [x] = v ++ flUnOp "exp" (creg x)

578doOp v LFLog [x] = v ++ flUnOp "log" (creg x)

579doOp v LFSin [x] = v ++ flUnOp "sin" (creg x)

580doOp v LFCos [x] = v ++ flUnOp "cos" (creg x)

581doOp v LFTan [x] = v ++ flUnOp "tan" (creg x)

582doOp v LFASin [x] = v ++ flUnOp "asin" (creg x)

583doOp v LFACos [x] = v ++ flUnOp "acos" (creg x)

584doOp v LFATan [x] = v ++ flUnOp "atan" (creg x)

585doOp v LFSqrt [x] = v ++ flUnOp "sqrt" (creg x)

586doOp v LFFloor [x] = v ++ flUnOp "floor" (creg x)

587doOp v LFCeil [x] = v ++ flUnOp "ceil" (creg x)

588doOp v LFNegate [x] = v ++ "MKFLOAT(vm, -GETFLOAT(" ++ (creg x) ++ "))"

589

590-- String functions which don't need to know we're UTF8

591doOp v LStrConcat [l,r] = v ++ "idris_concat(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

592doOp v LStrLt [l,r] = v ++ "idris_strlt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

593doOp v LStrEq [l,r] = v ++ "idris_streq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

594

595doOp v LReadStr [_] = v ++ "idris_readStr(vm, stdin)"

596doOp v LWriteStr [_,s]

597 = v ++ "MKINT((i_int)(idris_writeStr(stdout"

598 ++ ",GETSTR("

599 ++ creg s ++ "))))"

600

601

602-- String functions which need to know we're UTF8

603doOp v LStrHead [x] = v ++ "idris_strHead(vm, " ++ creg x ++ ")"

604doOp v LStrTail [x] = v ++ "idris_strTail(vm, " ++ creg x ++ ")"

605doOp v LStrCons [x, y] = v ++ "idris_strCons(vm, " ++ creg x ++ "," ++ creg y ++ ")"

606doOp v LStrIndex [x, y] = v ++ "idris_strIndex(vm, " ++ creg x ++ "," ++ creg y ++ ")"

607doOp v LStrRev [x] = v ++ "idris_strRev(vm, " ++ creg x ++ ")"

608doOp v LStrLen [x] = v ++ "idris_strlen(vm, " ++ creg x ++ ")"

609doOp v LStrSubstr [x,y,z] = v ++ "idris_substr(vm, " ++ creg x ++ "," ++ creg y ++ "," ++ creg z ++ ")"

610

611doOp v LFork [x] = v ++ "MKPTR(vm, vmThread(vm, " ++ cname (sMN 0 "EVAL") ++ ", " ++ creg x ++ "))"

612doOp v LPar [x] = v ++ creg x -- "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))"

613doOp v (LChInt ITNative) args = v ++ creg (last args)

614doOp v (LChInt ITChar) args = doOp v (LChInt ITNative) args

615doOp v (LIntCh ITNative) args = v ++ creg (last args)

616doOp v (LIntCh ITChar) args = doOp v (LIntCh ITNative) args

617

618doOp v LSystemInfo [x] = v ++ "idris_systemInfo(vm, " ++ creg x ++ ")"

619doOp v LNoOp args = v ++ creg (last args)

620

621-- Pointer primitives (declared as %extern in Builtins.idr)

622doOp v (LExternal rf) [_,x]

623 | rf == sUN "prim__readFile"

624 = v ++ "idris_readStr(vm, GETPTR(" ++ creg x ++ "))"

625doOp v (LExternal wf) [_,x,s]

626 | wf == sUN "prim__writeFile"

627 = v ++ "MKINT((i_int)(idris_writeStr(GETPTR(" ++ creg x

628 ++ "),GETSTR("

629 ++ creg s ++ "))))"

630doOp v (LExternal vm) [] | vm == sUN "prim__vm" = v ++ "MKPTR(vm, vm)"

631doOp v (LExternal si) [] | si == sUN "prim__stdin" = v ++ "MKPTR(vm, stdin)"

632doOp v (LExternal so) [] | so == sUN "prim__stdout" = v ++ "MKPTR(vm, stdout)"

633doOp v (LExternal se) [] | se == sUN "prim__stderr" = v ++ "MKPTR(vm, stderr)"

634

635doOp v (LExternal nul) [] | nul == sUN "prim__null" = v ++ "MKPTR(vm, NULL)"

636doOp v (LExternal eqp) [x, y] | eqp == sUN "prim__eqPtr"

637 = v ++ "MKINT((i_int)(GETPTR(" ++ creg x ++ ") == GETPTR(" ++ creg y ++ ")))"

638doOp v (LExternal eqp) [x, y] | eqp == sUN "prim__eqManagedPtr"

639 = v ++ "MKINT((i_int)(GETMPTR(" ++ creg x ++ ") == GETMPTR(" ++ creg y ++ ")))"

640doOp v (LExternal rp) [p, i] | rp == sUN "prim__registerPtr"

641 = v ++ "MKMPTR(vm, GETPTR(" ++ creg p ++ "), GETINT(" ++ creg i ++ "))"

642doOp v (LExternal pk) [_, p, o] | pk == sUN "prim__peek8"

643 = v ++ "idris_peekB8(vm," ++ creg p ++ "," ++ creg o ++")"

644doOp v (LExternal pk) [_, p, o, x] | pk == sUN "prim__poke8"

645 = v ++ "idris_pokeB8(" ++ creg p ++ "," ++ creg o ++ "," ++ creg x ++ ")"

646doOp v (LExternal pk) [_, p, o] | pk == sUN "prim__peek16"

647 = v ++ "idris_peekB16(vm," ++ creg p ++ "," ++ creg o ++")"

648doOp v (LExternal pk) [_, p, o, x] | pk == sUN "prim__poke16"

649 = v ++ "idris_pokeB16(" ++ creg p ++ "," ++ creg o ++ "," ++ creg x ++ ")"

650doOp v (LExternal pk) [_, p, o] | pk == sUN "prim__peek32"

651 = v ++ "idris_peekB32(vm," ++ creg p ++ "," ++ creg o ++")"

652doOp v (LExternal pk) [_, p, o, x] | pk == sUN "prim__poke32"

653 = v ++ "idris_pokeB32(" ++ creg p ++ "," ++ creg o ++ "," ++ creg x ++ ")"

654doOp v (LExternal pk) [_, p, o] | pk == sUN "prim__peek64"

655 = v ++ "idris_peekB64(vm," ++ creg p ++ "," ++ creg o ++")"

656doOp v (LExternal pk) [_, p, o, x] | pk == sUN "prim__poke64"

657 = v ++ "idris_pokeB64(" ++ creg p ++ "," ++ creg o ++ "," ++ creg x ++ ")"

658doOp v (LExternal pk) [_, p, o] | pk == sUN "prim__peekPtr"

659 = v ++ "idris_peekPtr(vm," ++ creg p ++ "," ++ creg o ++")"

660doOp v (LExternal pk) [_, p, o, x] | pk == sUN "prim__pokePtr"

661 = v ++ "idris_pokePtr(" ++ creg p ++ "," ++ creg o ++ "," ++ creg x ++ ")"

662doOp v (LExternal pk) [_, p, o, x] | pk == sUN "prim__pokeDouble"

663 = v ++ "idris_pokeDouble(" ++ creg p ++ "," ++ creg o ++ "," ++ creg x ++ ")"

664doOp v (LExternal pk) [_, p, o] | pk == sUN "prim__peekDouble"

665 = v ++ "idris_peekDouble(vm," ++ creg p ++ "," ++ creg o ++")"

666doOp v (LExternal pk) [_, p, o, x] | pk == sUN "prim__pokeSingle"

667 = v ++ "idris_pokeSingle(" ++ creg p ++ "," ++ creg o ++ "," ++ creg x ++ ")"

668doOp v (LExternal pk) [_, p, o] | pk == sUN "prim__peekSingle"

669 = v ++ "idris_peekSingle(vm," ++ creg p ++ "," ++ creg o ++")"

670doOp v (LExternal pk) [] | pk == sUN "prim__sizeofPtr"

671 = v ++ "MKINT(sizeof(void*))"

672doOp v (LExternal mpt) [p] | mpt == sUN "prim__asPtr"

673 = v ++ "MKPTR(vm, GETMPTR("++ creg p ++"))"

674doOp v (LExternal offs) [p, n] | offs == sUN "prim__ptrOffset"

675 = v ++ "MKPTR(vm, GETPTR(" ++ creg p ++ ") + GETINT(" ++ creg n ++ "))"

676doOp _ op args = error $ "doOp not implemented (" ++ show (op, args) ++ ")"

677

678

679flUnOp :: String -> String -> String

680flUnOp name val = "MKFLOAT(vm, " ++ name ++ "(GETFLOAT(" ++ val ++ ")))"

681

682-------------------- Interface file generation

683

684-- First, the wrappers in the C file

685

686ifaceC :: Export -> String

687ifaceC (ExportData n) = "typedef VAL " ++ cdesc n ++ ";\n"

688ifaceC (ExportFun n cn ret args)

689 = ctype ret ++ " " ++ cdesc cn ++

690 "(VM* vm" ++ showArgs (zip argNames args) ++ ") {\n"

691 ++ mkBody n (zip argNames args) ret ++ "}\n\n"

692 where showArgs [] = ""

693 showArgs ((n, t) : ts) = ", " ++ ctype t ++ " " ++ n ++

694 showArgs ts

695

696 argNames = zipWith (++) (repeat "arg") (map show [0..])

697

698mkBody n as t = indent 1 ++ "INITFRAME;\n" ++

699 indent 1 ++ "RESERVE(" ++ show (max (length as) 3) ++ ");\n" ++

700 push 0 as ++ call n ++ retval t

701 where push i [] = ""

702 push i ((n, t) : ts) = indent 1 ++ c_irts (toFType t)

703 ("TOP(" ++ show i ++ ") = ") n

704 ++ ";\n" ++ push (i + 1) ts

705

706 call _ = indent 1 ++ "STOREOLD;\n" ++

707 indent 1 ++ "BASETOP(0);\n" ++

708 indent 1 ++ "ADDTOP(" ++ show (length as) ++ ");\n" ++

709 indent 1 ++ "CALL(" ++ cname n ++ ");\n"

710

711 retval (FIO t)

712 = indent 1 ++ "TOP(0) = NULL;\n" ++

713 indent 1 ++ "TOP(1) = NULL;\n" ++

714 indent 1 ++ "TOP(2) = RVAL;\n" ++

715 indent 1 ++ "STOREOLD;\n" ++

716 indent 1 ++ "BASETOP(0);\n" ++

717 indent 1 ++ "ADDTOP(3);\n" ++

718 indent 1 ++ "CALL(" ++ cname (sUN "call__IO") ++ ");\n" ++

719 retval t

720 retval t = indent 1 ++ "return " ++ irts_c (toFType t) "RVAL" ++ ";\n"

721

722ctype (FCon c)

723 | c == sUN "C_Str" = "char*"

724 | c == sUN "C_Float" = "float"

725 | c == sUN "C_Ptr" = "void*"

726 | c == sUN "C_MPtr" = "void*"

727 | c == sUN "C_Unit" = "void"

728ctype (FApp c [_,ity])

729 | c == sUN "C_IntT" = carith ity

730ctype (FApp c [_])

731 | c == sUN "C_Any" = "VAL"

732ctype (FStr s) = s

733ctype FUnknown = "void*"

734ctype (FIO t) = ctype t

735ctype t = error "Can't happen: Not a valid interface type " ++ show t

736

737carith (FCon i)

738 | i == sUN "C_IntChar" = "char"

739 | i == sUN "C_IntNative" = "int"

740 | i == sUN "C_IntBits8" = "uint8_t"

741 | i == sUN "C_IntBits16" = "uint16_t"

742 | i == sUN "C_IntBits32" = "uint32_t"

743 | i == sUN "C_IntBits64" = "uint64_t"

744carith t = error $ "Can't happen: Not an exportable arithmetic type " ++ show t

745

746cdesc (FStr s) = s

747cdesc s = error "Can't happen: Not a valid C name"

748

749-- Then, the header files

750

751codegenH :: [ExportIFace] -> IO ()

752codegenH es = mapM_ writeIFace es

753

754writeIFace :: ExportIFace -> IO ()

755writeIFace (Export ffic hdr exps)

756 | ffic == sNS (sUN "FFI_C") ["FFI_C"]

757 = do let hfile = "#ifndef " ++ hdr_guard hdr ++ "\n" ++

758 "#define " ++ hdr_guard hdr ++ "\n\n" ++

759 "#include <idris_rts.h>\n\n" ++

760 concatMap hdr_export exps ++ "\n" ++

761 "#endif\n\n"

762 writeFile hdr hfile

763 | otherwise = return ()

764

765hdr_guard x = "__" ++ map hchar x

766 where hchar x | isAlphaNum x = toUpper x

767 hchar _ = '_'

768

769hdr_export :: Export -> String

770hdr_export (ExportData n) = "typedef VAL " ++ cdesc n ++ ";\n"

771hdr_export (ExportFun n cn ret args)

772 = ctype ret ++ " " ++ cdesc cn ++

773 "(VM* vm" ++ showArgs (zip argNames args) ++ ");\n"

774 where showArgs [] = ""

775 showArgs ((n, t) : ts) = ", " ++ ctype t ++ " " ++ n ++

776 showArgs ts

777

778 argNames = zipWith (++) (repeat "arg") (map show [0..])

779

780------------------ Callback wrapper generation ----------------

781-- Generate callback wrappers and a function to select the

782-- correct wrapper function to pass.

783-- TODO: This is limited to functions that are specified in

784-- the foreign call. Otherwise we would have to generate wrappers for all

785-- functions with correct arity or do flow analysis

786-- to find all possible inputs to the foreign call.

787genWrappers :: [(Name, [BC])] -> String

788genWrappers bcs = let

789 tags = nubBy (\x y -> snd x == snd y) $ concatMap (getCallback . snd) bcs

790 in

791 case tags of

792 [] -> ""

793 t -> concatMap genWrapper t ++ genDispatcher t

794

795genDispatcher :: [(FDesc, Int)] -> String

796genDispatcher tags = "void* _idris_get_wrapper(VAL con)\n" ++

797 "{\n" ++

798 indent 1 ++ "switch(TAG(con)) {\n" ++

799 concatMap makeSwitch tags ++

800 indent 1 ++ "}\n" ++

801 indent 1 ++ "fprintf(stderr, \"No wrapper for callback\");\n" ++

802 indent 1 ++ "exit(-1);\n" ++

803 "}\n\n"

804 where

805 makeSwitch (_, tag) =

806 indent 1 ++ "case " ++ show tag ++ ":\n" ++

807 indent 2 ++ "return (void*) &" ++ wrapperName tag ++ ";\n"

808

809genWrapper :: (FDesc, Int) -> String

810genWrapper (desc, tag) | (toFType desc) == FFunctionIO =

811 error "Cannot create C callbacks for IO functions, wrap them with unsafePerformIO.\n"

812genWrapper (desc, tag) = ret ++ " " ++ wrapperName tag ++ "(" ++

813 renderArgs argList ++")\n" ++

814 "{\n" ++

815 (if ret /= "void" then indent 1 ++ ret ++ " ret;\n" else "") ++

816 indent 1 ++ "VM* vm = get_vm();\n" ++

817 indent 1 ++ "if (vm == NULL) {\n" ++

818 indent 2 ++ "vm = idris_vm();\n" ++

819 indent 1 ++ "}\n" ++

820 indent 1 ++ "INITFRAME;\n" ++

821 indent 1 ++ "RESERVE(" ++ show (len + 1) ++ ");\n" ++

822 indent 1 ++ "allocCon(REG1, vm, " ++ show tag ++ ",0 , 0);\n" ++

823 indent 1 ++ "TOP(0) = REG1;\n" ++

824 applyArgs argList ++

825 if ret /= "void"

826 then indent 1 ++ "ret = " ++ irts_c (toFType ft) "RVAL" ++ ";\n"

827 ++ indent 1 ++ "return ret;\n}\n\n"

828 else "}\n\n"

829 where

830 (ret, ft) = rty desc

831 argList = zip (args desc) [0..]

832 len = length argList

833

834 applyArgs (x:y:xs) = push 1 [x] ++

835 indent 1 ++ "STOREOLD;\n" ++

836 indent 1 ++ "BASETOP(0);\n" ++

837 indent 1 ++ "ADDTOP(2);\n" ++

838 indent 1 ++ "CALL(_idris__123_APPLY0_125_);\n" ++

839 indent 1 ++ "TOP(0)=REG1;\n" ++

840 applyArgs (y:xs)

841 applyArgs x = push 1 x ++

842 indent 1 ++ "STOREOLD;\n" ++

843 indent 1 ++ "BASETOP(0);\n" ++

844 indent 1 ++ "ADDTOP(" ++ show (length x + 1) ++ ");\n" ++

845 indent 1 ++ "CALL(_idris__123_APPLY0_125_);\n"

846 renderArgs [] = "void"

847 renderArgs [((s, _), n)] = s ++ " a" ++ (show n)

848 renderArgs (((s, _), n):xs) = s ++ " a" ++ (show n) ++ ", " ++

849 renderArgs xs

850 rty (FApp c [_,ty])

851 | c == sUN "C_FnBase" = (ctype ty, ty)

852 | c == sUN "C_FnIO" = (ctype ty, ty)

853 | c == sUN "C_FnT" = rty ty

854 rty (FApp c [_,_,ty,fn])

855 | c == sUN "C_Fn" = rty fn

856 rty x = ("", x)

857 args (FApp c [_,ty])

858 | c == sUN "C_FnBase" = []

859 | c == sUN "C_FnIO" = []

860 | c == sUN "C_FnT" = args ty

861 args (FApp c [_,_,ty,fn])

862 | toFType ty == FUnit = []

863 | c == sUN "C_Fn" = (ctype ty, ty) : args fn

864 args _ = []

865 push i [] = ""

866 push i (((c, t), n) : ts) = indent 1 ++ c_irts (toFType t)

867 ("TOP(" ++ show i ++ ") = ") ("a" ++ show n)

868 ++ ";\n" ++ push (i + 1) ts

869

870wrapperName :: Int -> String

871wrapperName tag = "_idris_wrapper_" ++ show tag

872

873getCallback :: [BC] -> [(FDesc, Int)]

874getCallback bc = getCallback' (reverse bc)

875 where

876 getCallback' (x:xs) = case hasCallback x of

877 [] -> getCallback' xs

878 cbs -> case findCons cbs xs of

879 [] -> error "Idris function couldn't be wrapped."

880 x -> x

881 getCallback' [] = []

882 findCons (c:cs) xs = findCon c xs ++ findCons cs xs

883 findCons [] _ = []

884 findCon c ((MKCON l loc tag args):xs) | snd c == l = [(fst c, tag)]

885 findCon c (_:xs) = findCon c xs

886 findCon c [] = []

887

888hasCallback :: BC -> [(FDesc, Reg)]

889hasCallback (FOREIGNCALL l rty (FStr fn) args) = filter isFn args

890 where

891 isFn (desc,_) = case toFType desc of

892 FFunction -> True

893 FFunctionIO -> True

894 _ -> False

895hasCallback _ = []