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 Idris.Core.TT

12import IRTS.Bytecode

13import IRTS.CodegenCommon

14import IRTS.Defunctionalise

15import IRTS.Lang

16import IRTS.Simplified

17import IRTS.System

18

19import Util.System

20

21import Control.Monad

22import Data.Bits

23import Data.Char

24import Data.List (intercalate, nubBy)

25import Debug.Trace

26import Numeric

27import System.Directory

28import System.Exit

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

30import System.IO

31import System.Process

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 <- getIdrisCRTSDir

70 mprog <- readFile (d </> "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 (FOREIGNCALL l rty _ args) = error "Foreign Function calls cannot be partially applied, without being inlined."

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

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

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

347

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

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

350-- a foreign type description for c_irts and irts_c

351toAType (FCon i)

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

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

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

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

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

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

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

359

360toFType (FCon c)

361 | c == sUN "C_Str" = FString

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

363 | c == sUN "C_Ptr" = FPtr

364 | c == sUN "C_MPtr" = FManagedPtr

365 | c == sUN "C_CData" = FCData

366 | c == sUN "C_Unit" = FUnit

367toFType (FApp c [_,ity])

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

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

370toFType (FApp c [_])

371 | c == sUN "C_Any" = FAny

372toFType t = FAny

373

374toFunType (FApp c [_,ity])

375 | c == sUN "C_FnBase" = FFunction

376 | c == sUN "C_FnIO" = FFunctionIO

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

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

379toFunType _ = FAny

380

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

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

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

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

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

386c_irts FUnit l x = x

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

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

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

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

391c_irts FAny l x = l ++ x

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

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

394

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

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

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

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

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

400irts_c FUnit x = x

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

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

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

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

405irts_c FAny x = x

406irts_c FFunctionIO x = wrapped x

407irts_c FFunction x = wrapped x

408

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

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

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

412

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

414

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

416

417bitCoerce v op input output arg

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

419

420signedTy :: NativeTy -> String

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

422

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

446

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

470

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

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

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

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

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

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

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

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

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

480

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

498

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

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

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

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

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

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

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

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

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

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

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

510

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

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

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

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

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

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

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

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

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

520

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

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

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

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

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

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

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

528

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

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

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

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

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

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

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

536

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

559doOp v (LZExt ITNative ITBig) [x]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

577

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

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

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

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

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

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

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

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

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

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

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

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

590

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

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

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

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

595

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

597doOp v LWriteStr [_,s]

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

599 ++ ",GETSTR("

600 ++ creg s ++ "))))"

601

602

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

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

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

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

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

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

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

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

611

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

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

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

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

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

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

618

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

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

621

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

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

624 | rf == sUN "prim__readFile"

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

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

627 | wf == sUN "prim__writeFile"

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

629 ++ "),GETSTR("

630 ++ creg s ++ "))))"

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 vm) [_] | vm == sUN "prim__vm" = v ++ "MKPTR(vm, vm)"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

678

679

680flUnOp :: String -> String -> String

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

682

683-------------------- Interface file generation

684

685-- First, the wrappers in the C file

686

687ifaceC :: Export -> String

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

689ifaceC (ExportFun n cn ret args)

690 = ctype ret ++ " " ++ cdesc cn ++

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

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

693 where showArgs [] = ""

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

695 showArgs ts

696

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

698

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

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

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

702 where push i [] = ""

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

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

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

706

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

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

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

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

711

712 retval (FIO t)

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

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

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

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

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

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

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

720 retval t

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

722

723ctype (FCon c)

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

725 | c == sUN "C_Float" = "float"

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

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

728 | c == sUN "C_Unit" = "void"

729ctype (FApp c [_,ity])

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

731ctype (FApp c [_])

732 | c == sUN "C_Any" = "VAL"

733ctype (FStr s) = s

734ctype FUnknown = "void*"

735ctype (FIO t) = ctype t

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

737

738carith (FCon i)

739 | i == sUN "C_IntChar" = "char"

740 | i == sUN "C_IntNative" = "int"

741 | i == sUN "C_IntBits8" = "uint8_t"

742 | i == sUN "C_IntBits16" = "uint16_t"

743 | i == sUN "C_IntBits32" = "uint32_t"

744 | i == sUN "C_IntBits64" = "uint64_t"

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

746

747cdesc (FStr s) = s

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

749

750-- Then, the header files

751

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

753codegenH es = mapM_ writeIFace es

754

755writeIFace :: ExportIFace -> IO ()

756writeIFace (Export ffic hdr exps)

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

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

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

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

761 concatMap hdr_export exps ++ "\n" ++

762 "#endif\n\n"

763 writeFile hdr hfile

764 | otherwise = return ()

765

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

767 where hchar x | isAlphaNum x = toUpper x

768 hchar _ = '_'

769

770hdr_export :: Export -> String

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

772hdr_export (ExportFun n cn ret args)

773 = ctype ret ++ " " ++ cdesc cn ++

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

775 where showArgs [] = ""

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

777 showArgs ts

778

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

780

781------------------ Callback wrapper generation ----------------

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

783-- correct wrapper function to pass.

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

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

786-- functions with correct arity or do flow analysis

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

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

789genWrappers bcs = let

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

791 in

792 case tags of

793 [] -> ""

794 t -> concatMap genWrapper t ++ genDispatcher t

795

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

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

798 "{\n" ++

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

800 concatMap makeSwitch tags ++

801 indent 1 ++ "}\n" ++

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

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

804 "}\n\n"

805 where

806 makeSwitch (_, tag) =

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

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

809

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

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

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

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

814 renderArgs argList ++")\n" ++

815 "{\n" ++

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

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

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

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

820 indent 1 ++ "}\n" ++

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

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

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

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

825 applyArgs argList ++

826 if ret /= "void"

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

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

829 else "}\n\n"

830 where

831 (ret, ft) = rty desc

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

833 len = length argList

834

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

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

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

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

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

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

841 applyArgs (y:xs)

842 applyArgs x = push 1 x ++

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

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

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

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

847 renderArgs [] = "void"

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

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

850 renderArgs xs

851 rty (FApp c [_,ty])

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

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

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

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

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

857 rty x = ("", x)

858 args (FApp c [_,ty])

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

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

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

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

863 | toFType ty == FUnit = []

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

865 args _ = []

866 push i [] = ""

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

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

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

870

871wrapperName :: Int -> String

872wrapperName tag = "_idris_wrapper_" ++ show tag

873

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

875getCallback bc = getCallback' (reverse bc)

876 where

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

878 [] -> getCallback' xs

879 cbs -> case findCons cbs xs of

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

881 x -> x

882 getCallback' [] = []

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

884 findCons [] _ = []

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

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

887 findCon c [] = []

888

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

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

891 where

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

893 FFunction -> True

894 FFunctionIO -> True

895 _ -> False

896hasCallback _ = []