@@ -0,0 +1,277 @@
1+{-# LANGUAGE OverloadedStrings #-}
2+
3+module IRTS.Portable (writePortable) where
4+
5+import Data.Aeson
6+import qualified Data.ByteString.Lazy as B
7+import qualified Data.Text as T
8+
9+import Idris.Core.CaseTree
10+import Idris.Core.TT
11+
12+import IRTS.Bytecode
13+import IRTS.CodegenCommon
14+import IRTS.Defunctionalise
15+import IRTS.Lang
16+import IRTS.Simplified
17+
18+import System.IO
19+
20+data CodegenFile = CGFile {
21+ fileType :: String,
22+ version :: Int,
23+ cgInfo :: CodegenInfo
24+}
25+
26+-- Update the version when the format changes
27+formatVersion :: Int
28+formatVersion = 1
29+
30+writePortable :: Handle -> CodegenInfo -> IO ()
31+writePortable file ci = do
32+ let json = encode $ CGFile "idris-codegen" formatVersion ci
33+ B.hPut file json
34+
35+instance ToJSON CodegenFile where
36+ toJSON (CGFile ft v ci) = object ["file-type" .= ft,
37+ "version" .= v,
38+ "codegen-info" .= toJSON ci]
39+
40+instance ToJSON CodegenInfo where
41+ toJSON ci = object ["output-file" .= (outputFile ci),
42+ "includes" .= (includes ci),
43+ "import-dirs" .= (importDirs ci),
44+ "compile-objs" .= (compileObjs ci),
45+ "compile-libs" .= (compileLibs ci),
46+ "compiler-flags" .= (compilerFlags ci),
47+ "interfaces" .= (interfaces ci),
48+ "exports" .= (exportDecls ci),
49+ "lift-decls" .= (liftDecls ci),
50+ "defun-decls" .= (defunDecls ci),
51+ "simple-decls" .= (simpleDecls ci),
52+ "bytecode" .= (map toBC (simpleDecls ci))]
53+
54+instance ToJSON Name where
55+ toJSON n = toJSON $ showCG n
56+
57+instance ToJSON ExportIFace where
58+ toJSON (Export n f xs) = object ["ffi-desc" .= n,
59+ "interface-file" .= f,
60+ "exports" .= xs]
61+
62+instance ToJSON FDesc where
63+ toJSON (FCon n) = object ["FCon" .= n]
64+ toJSON (FStr s) = object ["FStr" .= s]
65+ toJSON (FUnknown) = object ["FUnknown" .= Null]
66+ toJSON (FIO fd) = object ["FIO" .= fd]
67+ toJSON (FApp n xs) = object ["FApp" .= (n, xs)]
68+
69+instance ToJSON Export where
70+ toJSON (ExportData fd) = object ["ExportData" .= fd]
71+ toJSON (ExportFun n dsc ret args) = object ["ExportFun" .= (n, dsc, ret, args)]
72+
73+instance ToJSON LDecl where
74+ toJSON (LFun opts name args def) = object ["LFun" .= (opts, name, args, def)]
75+ toJSON (LConstructor name tag ar) = object ["LConstructor" .= (name, tag, ar)]
76+
77+instance ToJSON LOpt where
78+ toJSON Inline = String "Inline"
79+ toJSON NoInline = String "NoInline"
80+
81+instance ToJSON LExp where
82+ toJSON (LV lv) = object ["LV" .= lv]
83+ toJSON (LApp tail exp args) = object ["LApp" .= (tail, exp, args)]
84+ toJSON (LLazyApp name exps) = object ["LLazyApp" .= (name, exps)]
85+ toJSON (LLazyExp exp) = object ["LLazyExp" .= exp]
86+ toJSON (LForce exp) = object ["LForce" .= exp]
87+ toJSON (LLet name a b) = object ["LLet" .= (name, a, b)]
88+ toJSON (LLam args exp) = object ["LLam" .= (args, exp)]
89+ toJSON (LProj exp i) = object ["LProj" .= (exp, i)]
90+ toJSON (LCon lv i n exps) = object ["LCon" .= (lv, i, n, exps)]
91+ toJSON (LCase ct exp alts) = object ["LCase" .= (ct, exp, alts)]
92+ toJSON (LConst c) = object ["LConst" .= c]
93+ toJSON (LForeign fd ret exps) = object ["LForeign" .= (fd, ret, exps)]
94+ toJSON (LOp prim exps) = object ["LOp" .= (prim, exps)]
95+ toJSON LNothing = object ["LNothing" .= Null]
96+ toJSON (LError s) = object ["LError" .= s]
97+
98+instance ToJSON LVar where
99+ toJSON (Loc i) = object ["Loc" .= i]
100+ toJSON (Glob n) = object ["Glob" .= n]
101+
102+instance ToJSON CaseType where
103+ toJSON Updatable = String "Updatable"
104+ toJSON Shared = String "Shared"
105+
106+instance ToJSON LAlt where
107+ toJSON (LConCase i n ns exp) = object ["LConCase" .= (i, n, ns, exp)]
108+ toJSON (LConstCase c exp) = object ["LConstCase" .= (c, exp)]
109+ toJSON (LDefaultCase exp) = object ["LDefaultCase" .= exp]
110+
111+instance ToJSON Const where
112+ toJSON (I i) = object ["int" .= i]
113+ toJSON (BI i) = object ["bigint" .= (show i)]
114+ toJSON (Fl d) = object ["double" .= d]
115+ toJSON (Ch c) = object ["char" .= (show c)]
116+ toJSON (Str s) = object ["string" .= s]
117+ toJSON (B8 b) = object ["bits8" .= b]
118+ toJSON (B16 b) = object ["bits16" .= b]
119+ toJSON (B32 b) = object ["bits32" .= b]
120+ toJSON (B64 b) = object ["bits64" .= b]
121+ toJSON (AType at) = object ["atype" .= at]
122+ toJSON StrType = object ["strtype" .= Null]
123+ toJSON WorldType = object ["worldtype" .= Null]
124+ toJSON TheWorld = object ["theworld" .= Null]
125+ toJSON VoidType = object ["voidtype" .= Null]
126+ toJSON Forgot = object ["forgot" .= Null]
127+
128+instance ToJSON ArithTy where
129+ toJSON (ATInt it) = object ["ATInt" .= it]
130+ toJSON ATFloat = object ["ATFloat" .= Null]
131+
132+instance ToJSON IntTy where
133+ toJSON it = toJSON $ intTyName it
134+
135+instance ToJSON PrimFn where
136+ toJSON (LPlus aty) = object ["LPlus" .= aty]
137+ toJSON (LMinus aty) = object ["LMinus" .= aty]
138+ toJSON (LTimes aty) = object ["LTimes" .= aty]
139+ toJSON (LUDiv aty) = object ["LUDiv" .= aty]
140+ toJSON (LSDiv aty) = object ["LSDiv" .= aty]
141+ toJSON (LAnd ity) = object ["LAnd" .= ity]
142+ toJSON (LOr ity) = object ["LOr" .= ity]
143+ toJSON (LXOr ity) = object ["LXOr" .= ity]
144+ toJSON (LCompl ity) = object ["LCompl" .= ity]
145+ toJSON (LSHL ity) = object ["LSHL" .= ity]
146+ toJSON (LLSHR ity) = object ["LLSHR" .= ity]
147+ toJSON (LASHR ity) = object ["LASHR" .= ity]
148+ toJSON (LEq aty) = object ["LEq" .= aty]
149+ toJSON (LLt ity) = object ["LLt" .= ity]
150+ toJSON (LLe ity) = object ["LLe" .= ity]
151+ toJSON (LGt ity) = object ["LGt" .= ity]
152+ toJSON (LGe ity) = object ["LGe" .= ity]
153+ toJSON (LSLt aty) = object ["LSLt" .= aty]
154+ toJSON (LSLe aty) = object ["LSLe" .= aty]
155+ toJSON (LSGt aty) = object ["LSGt" .= aty]
156+ toJSON (LSGe aty) = object ["LSGe" .= aty]
157+ toJSON (LZExt from to) = object ["LZExt" .= (from, to)]
158+ toJSON (LSExt from to) = object ["LSExt" .= (from, to)]
159+ toJSON (LTrunc from to) = object ["LTrunc" .= (from, to)]
160+ toJSON LStrConcat = object ["LStrConcat" .= Null]
161+ toJSON LStrLt = object ["LStrLt" .= Null]
162+ toJSON LStrEq = object ["LStrEq" .= Null]
163+ toJSON LStrLen = object ["LStrLen" .= Null]
164+ toJSON (LIntFloat ity) = object ["LIntFloat" .= ity]
165+ toJSON (LFloatInt ity) = object ["LFloatInt" .= ity]
166+ toJSON (LIntStr ity) = object ["LIntStr" .= ity]
167+ toJSON (LStrInt ity) = object ["LStrInt" .= ity]
168+ toJSON (LIntCh ity) = object ["LIntCh" .= ity]
169+ toJSON (LChInt ity) = object ["LChInt" .= ity]
170+ toJSON LFloatStr = object ["LFloatStr" .= Null]
171+ toJSON LStrFloat = object ["LStrFloat" .= Null]
172+ toJSON (LBitCast from to) = object ["LBitCast" .= (from, to)]
173+ toJSON LFExp = object ["LFExp" .= Null]
174+ toJSON LFLog = object ["LFLog" .= Null]
175+ toJSON LFSin = object ["LFSin" .= Null]
176+ toJSON LFCos = object ["LFCos" .= Null]
177+ toJSON LFTan = object ["LFTan" .= Null]
178+ toJSON LFASin = object ["LFASin" .= Null]
179+ toJSON LFACos = object ["LFACos" .= Null]
180+ toJSON LFATan = object ["LFATan" .= Null]
181+ toJSON LFSqrt = object ["LFSqrt" .= Null]
182+ toJSON LFFloor = object ["LFFloor" .= Null]
183+ toJSON LFCeil = object ["LFCeil" .= Null]
184+ toJSON LFNegate = object ["LFNegate" .= Null]
185+ toJSON LStrHead = object ["LStrHead" .= Null]
186+ toJSON LStrTail = object ["LStrTail" .= Null]
187+ toJSON LStrCons = object ["LStrCons" .= Null]
188+ toJSON LStrIndex = object ["LStrIndex" .= Null]
189+ toJSON LStrRev = object ["LStrRev" .= Null]
190+ toJSON LStrSubstr = object ["LStrSubstr" .= Null]
191+ toJSON LReadStr = object ["LReadStr" .= Null]
192+ toJSON LWriteStr = object ["LWriteStr" .= Null]
193+ toJSON LSystemInfo = object ["LSystemInfo" .= Null]
194+ toJSON LFork = object ["LFork" .= Null]
195+ toJSON LPar = object ["LPar" .= Null]
196+ toJSON (LExternal name) = object ["LExternal" .= name]
197+ toJSON LNoOp = object ["LNoOp" .= Null]
198+
199+
200+
201+
202+
203+instance ToJSON DDecl where
204+ toJSON (DFun name args exp) = object ["DFun" .= (name, args, exp)]
205+ toJSON (DConstructor name tag arity) = object ["DConstructor" .= (name, tag, arity)]
206+
207+instance ToJSON DExp where
208+ toJSON (DV lv) = object ["DV" .= lv]
209+ toJSON (DApp tail name exps) = object ["DApp" .= (tail, name, exps)]
210+ toJSON (DLet name a b) = object ["DLet" .= (name, a, b)]
211+ toJSON (DUpdate name exp) = object ["DUpdate" .= (name,exp)]
212+ toJSON (DProj exp i) = object ["DProj" .= (exp, i)]
213+ toJSON (DC lv i name exp) = object ["DC" .= (lv, i, name, exp)]
214+ toJSON (DCase ct exp alts) = object ["DCase" .= (ct, exp, alts)]
215+ toJSON (DChkCase exp alts) = object ["DChkCase" .= (exp, alts)]
216+ toJSON (DConst c) = object ["DConst" .= c]
217+ toJSON (DForeign fd ret exps) = object ["DForeign" .= (fd, ret, exps)]
218+ toJSON (DOp prim exps) = object ["DOp" .= (prim, exps)]
219+ toJSON DNothing = object ["DNothing" .= Null]
220+ toJSON (DError s) = object ["DError" .= s]
221+
222+instance ToJSON DAlt where
223+ toJSON (DConCase i n ns exp) = object ["DConCase" .= (i, n, ns, exp)]
224+ toJSON (DConstCase c exp) = object ["DConstCase" .= (c, exp)]
225+ toJSON (DDefaultCase exp) = object ["DDefaultCase" .= exp]
226+
227+instance ToJSON SDecl where
228+ toJSON (SFun name args i exp) = object ["SFun" .= (name, args, i, exp)]
229+
230+instance ToJSON SExp where
231+ toJSON (SV lv) = object ["SV" .= lv]
232+ toJSON (SApp tail name exps) = object ["SApp" .= (tail, name, exps)]
233+ toJSON (SLet lv a b) = object ["SLet" .= (lv, a, b)]
234+ toJSON (SUpdate lv exp) = object ["SUpdate" .= (lv, exp)]
235+ toJSON (SProj lv i) = object ["DProj" .= (lv, i)]
236+ toJSON (SCon lv i name vars) = object ["SCon" .= (lv, i, name, vars)]
237+ toJSON (SCase ct lv alts) = object ["SCase" .= (ct, lv, alts)]
238+ toJSON (SChkCase lv alts) = object ["DChkCase" .= (lv, alts)]
239+ toJSON (SConst c) = object ["SConst" .= c]
240+ toJSON (SForeign fd ret exps) = object ["SForeign" .= (fd, ret, exps)]
241+ toJSON (SOp prim vars) = object ["DOp" .= (prim, vars)]
242+ toJSON SNothing = object ["SNothing" .= Null]
243+ toJSON (SError s) = object ["SError" .= s]
244+
245+instance ToJSON SAlt where
246+ toJSON (SConCase i j n ns exp) = object ["SConCase" .= (i, j, n, ns, exp)]
247+ toJSON (SConstCase c exp) = object ["SConstCase" .= (c, exp)]
248+ toJSON (SDefaultCase exp) = object ["SDefaultCase" .= exp]
249+
250+instance ToJSON BC where
251+ toJSON (ASSIGN r1 r2) = object ["ASSIGN" .= (r1, r2)]
252+ toJSON (ASSIGNCONST r c) = object ["ASSIGNCONST" .= (r, c)]
253+ toJSON (UPDATE r1 r2) = object ["UPDATE" .= (r1, r2)]
254+ toJSON (MKCON con mr i regs) = object ["MKCON" .= (con, mr, i, regs)]
255+ toJSON (CASE b r alts def) = object ["CASE" .= (b, r, alts, def)]
256+ toJSON (PROJECT r loc arity) = object ["PROJECT" .= (r, loc, arity)]
257+ toJSON (PROJECTINTO r1 r2 loc) = object ["PROJECTINTO" .= (r1, r2, loc)]
258+ toJSON (CONSTCASE r alts def) = object ["CONSTCASE" .= (r, alts, def)]
259+ toJSON (CALL name) = object ["CALL" .= name]
260+ toJSON (TAILCALL name) = object ["TAILCALL" .= name]
261+ toJSON (FOREIGNCALL r fd ret exps) = object ["FOREIGNCALL" .= (r, fd, ret, exps)]
262+ toJSON (SLIDE i) = object ["SLIDE" .= i]
263+ toJSON (RESERVE i) = object ["RESERVE" .= i]
264+ toJSON (ADDTOP i) = object ["ADDTOP" .= i]
265+ toJSON (TOPBASE i) = object ["TOPBASE" .= i]
266+ toJSON (BASETOP i) = object ["BASETOP" .= i]
267+ toJSON REBASE = object ["REBASE" .= Null]
268+ toJSON STOREOLD = object ["STOREOLD" .= Null]
269+ toJSON (OP r prim args) = object ["OP" .= (r, prim, args)]
270+ toJSON (NULL r) = object ["NULL" .= r]
271+ toJSON (ERROR s) = object ["ERROR" .= s]
272+
273+instance ToJSON Reg where
274+ toJSON RVal = object ["RVal" .= Null]
275+ toJSON (T i) = object ["T" .= i]
276+ toJSON (L i) = object ["L" .= i]
277+ toJSON Tmp = object ["Tmp" .= Null]