git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/IRTS/Portable.hs
363 lines 16 kB history raw
1{-|
2Module : IRTS.Portable
3Description : Serialise Idris' IR to JSON.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE FlexibleInstances, OverloadedStrings, TypeSynonymInstances #-}
9module IRTS.Portable (writePortable) where
11import Idris.Core.CaseTree
12import Idris.Core.Evaluate
13import Idris.Core.TT
14import IRTS.Bytecode
15import IRTS.CodegenCommon
16import IRTS.Defunctionalise
17import IRTS.Simplified
19import Data.Aeson
20import qualified Data.ByteString.Lazy as B
21import System.IO
23data CodegenFile = CGFile {
24 fileType :: String,
25 version :: Int,
26 cgInfo :: CodegenInfo
29-- Update the version when the format changes
30formatVersion :: Int
31formatVersion = 3
33writePortable :: Handle -> CodegenInfo -> IO ()
34writePortable file ci = do
35 let json = encode $ CGFile "idris-codegen" formatVersion ci
36 B.hPut file json
38instance ToJSON CodegenFile where
39 toJSON (CGFile ft v ci) = object ["file-type" .= ft,
40 "version" .= v,
41 "codegen-info" .= toJSON ci]
43instance ToJSON CodegenInfo where
44 toJSON ci = object ["output-file" .= (outputFile ci),
45 "includes" .= (includes ci),
46 "import-dirs" .= (importDirs ci),
47 "compile-objs" .= (compileObjs ci),
48 "compile-libs" .= (compileLibs ci),
49 "compiler-flags" .= (compilerFlags ci),
50 "interfaces" .= (interfaces ci),
51 "exports" .= (exportDecls ci),
52 "lift-decls" .= (liftDecls ci),
53 "defun-decls" .= (defunDecls ci),
54 "simple-decls" .= (simpleDecls ci),
55 "bytecode" .= (map toBC (simpleDecls ci)),
56 "tt-decls" .= (ttDecls ci)]
58instance ToJSON Name where
59 toJSON n = toJSON $ showCG n
61instance ToJSON ExportIFace where
62 toJSON (Export n f xs) = object ["ffi-desc" .= n,
63 "interface-file" .= f,
64 "exports" .= xs]
66instance ToJSON FDesc where
67 toJSON (FCon n) = object ["FCon" .= n]
68 toJSON (FStr s) = object ["FStr" .= s]
69 toJSON (FUnknown) = object ["FUnknown" .= Null]
70 toJSON (FIO fd) = object ["FIO" .= fd]
71 toJSON (FApp n xs) = object ["FApp" .= (n, xs)]
73instance ToJSON Export where
74 toJSON (ExportData fd) = object ["ExportData" .= fd]
75 toJSON (ExportFun n dsc ret args) = object ["ExportFun" .= (n, dsc, ret, args)]
77instance ToJSON LDecl where
78 toJSON (LFun opts name args def) = object ["LFun" .= (opts, name, args, def)]
79 toJSON (LConstructor name tag ar) = object ["LConstructor" .= (name, tag, ar)]
81instance ToJSON LOpt where
82 toJSON Inline = String "Inline"
83 toJSON NoInline = String "NoInline"
85instance ToJSON LExp where
86 toJSON (LV lv) = object ["LV" .= lv]
87 toJSON (LApp tail exp args) = object ["LApp" .= (tail, exp, args)]
88 toJSON (LLazyApp name exps) = object ["LLazyApp" .= (name, exps)]
89 toJSON (LLazyExp exp) = object ["LLazyExp" .= exp]
90 toJSON (LForce exp) = object ["LForce" .= exp]
91 toJSON (LLet name a b) = object ["LLet" .= (name, a, b)]
92 toJSON (LLam args exp) = object ["LLam" .= (args, exp)]
93 toJSON (LProj exp i) = object ["LProj" .= (exp, i)]
94 toJSON (LCon lv i n exps) = object ["LCon" .= (lv, i, n, exps)]
95 toJSON (LCase ct exp alts) = object ["LCase" .= (ct, exp, alts)]
96 toJSON (LConst c) = object ["LConst" .= c]
97 toJSON (LForeign fd ret exps) = object ["LForeign" .= (fd, ret, exps)]
98 toJSON (LOp prim exps) = object ["LOp" .= (prim, exps)]
99 toJSON LNothing = object ["LNothing" .= Null]
100 toJSON (LError s) = object ["LError" .= s]
102instance ToJSON LVar where
103 toJSON (Loc i) = object ["Loc" .= i]
104 toJSON (Glob n) = object ["Glob" .= n]
106instance ToJSON CaseType where
107 toJSON Updatable = String "Updatable"
108 toJSON Shared = String "Shared"
110instance ToJSON LAlt where
111 toJSON (LConCase i n ns exp) = object ["LConCase" .= (i, n, ns, exp)]
112 toJSON (LConstCase c exp) = object ["LConstCase" .= (c, exp)]
113 toJSON (LDefaultCase exp) = object ["LDefaultCase" .= exp]
115instance ToJSON Const where
116 toJSON (I i) = object ["int" .= i]
117 toJSON (BI i) = object ["bigint" .= (show i)]
118 toJSON (Fl d) = object ["double" .= d]
119 toJSON (Ch c) = object ["char" .= (show c)]
120 toJSON (Str s) = object ["string" .= s]
121 toJSON (B8 b) = object ["bits8" .= b]
122 toJSON (B16 b) = object ["bits16" .= b]
123 toJSON (B32 b) = object ["bits32" .= b]
124 toJSON (B64 b) = object ["bits64" .= b]
125 toJSON (AType at) = object ["atype" .= at]
126 toJSON StrType = object ["strtype" .= Null]
127 toJSON WorldType = object ["worldtype" .= Null]
128 toJSON TheWorld = object ["theworld" .= Null]
129 toJSON VoidType = object ["voidtype" .= Null]
130 toJSON Forgot = object ["forgot" .= Null]
132instance ToJSON ArithTy where
133 toJSON (ATInt it) = object ["ATInt" .= it]
134 toJSON ATFloat = object ["ATFloat" .= Null]
136instance ToJSON IntTy where
137 toJSON it = toJSON $ intTyName it
139instance ToJSON PrimFn where
140 toJSON (LPlus aty) = object ["LPlus" .= aty]
141 toJSON (LMinus aty) = object ["LMinus" .= aty]
142 toJSON (LTimes aty) = object ["LTimes" .= aty]
143 toJSON (LUDiv aty) = object ["LUDiv" .= aty]
144 toJSON (LSDiv aty) = object ["LSDiv" .= aty]
145 toJSON (LURem ity) = object ["LURem" .= ity]
146 toJSON (LSRem aty) = object ["LSRem" .= aty]
147 toJSON (LAnd ity) = object ["LAnd" .= ity]
148 toJSON (LOr ity) = object ["LOr" .= ity]
149 toJSON (LXOr ity) = object ["LXOr" .= ity]
150 toJSON (LCompl ity) = object ["LCompl" .= ity]
151 toJSON (LSHL ity) = object ["LSHL" .= ity]
152 toJSON (LLSHR ity) = object ["LLSHR" .= ity]
153 toJSON (LASHR ity) = object ["LASHR" .= ity]
154 toJSON (LEq aty) = object ["LEq" .= aty]
155 toJSON (LLt ity) = object ["LLt" .= ity]
156 toJSON (LLe ity) = object ["LLe" .= ity]
157 toJSON (LGt ity) = object ["LGt" .= ity]
158 toJSON (LGe ity) = object ["LGe" .= ity]
159 toJSON (LSLt aty) = object ["LSLt" .= aty]
160 toJSON (LSLe aty) = object ["LSLe" .= aty]
161 toJSON (LSGt aty) = object ["LSGt" .= aty]
162 toJSON (LSGe aty) = object ["LSGe" .= aty]
163 toJSON (LZExt from to) = object ["LZExt" .= (from, to)]
164 toJSON (LSExt from to) = object ["LSExt" .= (from, to)]
165 toJSON (LTrunc from to) = object ["LTrunc" .= (from, to)]
166 toJSON LStrConcat = object ["LStrConcat" .= Null]
167 toJSON LStrLt = object ["LStrLt" .= Null]
168 toJSON LStrEq = object ["LStrEq" .= Null]
169 toJSON LStrLen = object ["LStrLen" .= Null]
170 toJSON (LIntFloat ity) = object ["LIntFloat" .= ity]
171 toJSON (LFloatInt ity) = object ["LFloatInt" .= ity]
172 toJSON (LIntStr ity) = object ["LIntStr" .= ity]
173 toJSON (LStrInt ity) = object ["LStrInt" .= ity]
174 toJSON (LIntCh ity) = object ["LIntCh" .= ity]
175 toJSON (LChInt ity) = object ["LChInt" .= ity]
176 toJSON LFloatStr = object ["LFloatStr" .= Null]
177 toJSON LStrFloat = object ["LStrFloat" .= Null]
178 toJSON (LBitCast from to) = object ["LBitCast" .= (from, to)]
179 toJSON LFExp = object ["LFExp" .= Null]
180 toJSON LFLog = object ["LFLog" .= Null]
181 toJSON LFSin = object ["LFSin" .= Null]
182 toJSON LFCos = object ["LFCos" .= Null]
183 toJSON LFTan = object ["LFTan" .= Null]
184 toJSON LFASin = object ["LFASin" .= Null]
185 toJSON LFACos = object ["LFACos" .= Null]
186 toJSON LFATan = object ["LFATan" .= Null]
187 toJSON LFATan2 = object ["LFATan2" .= Null]
188 toJSON LFSqrt = object ["LFSqrt" .= Null]
189 toJSON LFFloor = object ["LFFloor" .= Null]
190 toJSON LFCeil = object ["LFCeil" .= Null]
191 toJSON LFNegate = object ["LFNegate" .= Null]
192 toJSON LStrHead = object ["LStrHead" .= Null]
193 toJSON LStrTail = object ["LStrTail" .= Null]
194 toJSON LStrCons = object ["LStrCons" .= Null]
195 toJSON LStrIndex = object ["LStrIndex" .= Null]
196 toJSON LStrRev = object ["LStrRev" .= Null]
197 toJSON LStrSubstr = object ["LStrSubstr" .= Null]
198 toJSON LReadStr = object ["LReadStr" .= Null]
199 toJSON LWriteStr = object ["LWriteStr" .= Null]
200 toJSON LSystemInfo = object ["LSystemInfo" .= Null]
201 toJSON LFork = object ["LFork" .= Null]
202 toJSON LPar = object ["LPar" .= Null]
203 toJSON (LExternal name) = object ["LExternal" .= name]
204 toJSON LCrash = object ["LCrash" .= Null]
205 toJSON LNoOp = object ["LNoOp" .= Null]
207instance ToJSON DDecl where
208 toJSON (DFun name args exp) = object ["DFun" .= (name, args, exp)]
209 toJSON (DConstructor name tag arity) = object ["DConstructor" .= (name, tag, arity)]
211instance ToJSON DExp where
212 toJSON (DV lv) = object ["DV" .= lv]
213 toJSON (DApp tail name exps) = object ["DApp" .= (tail, name, exps)]
214 toJSON (DLet name a b) = object ["DLet" .= (name, a, b)]
215 toJSON (DUpdate name exp) = object ["DUpdate" .= (name,exp)]
216 toJSON (DProj exp i) = object ["DProj" .= (exp, i)]
217 toJSON (DC lv i name exp) = object ["DC" .= (lv, i, name, exp)]
218 toJSON (DCase ct exp alts) = object ["DCase" .= (ct, exp, alts)]
219 toJSON (DChkCase exp alts) = object ["DChkCase" .= (exp, alts)]
220 toJSON (DConst c) = object ["DConst" .= c]
221 toJSON (DForeign fd ret exps) = object ["DForeign" .= (fd, ret, exps)]
222 toJSON (DOp prim exps) = object ["DOp" .= (prim, exps)]
223 toJSON DNothing = object ["DNothing" .= Null]
224 toJSON (DError s) = object ["DError" .= s]
226instance ToJSON DAlt where
227 toJSON (DConCase i n ns exp) = object ["DConCase" .= (i, n, ns, exp)]
228 toJSON (DConstCase c exp) = object ["DConstCase" .= (c, exp)]
229 toJSON (DDefaultCase exp) = object ["DDefaultCase" .= exp]
231instance ToJSON SDecl where
232 toJSON (SFun name args i exp) = object ["SFun" .= (name, args, i, exp)]
234instance ToJSON SExp where
235 toJSON (SV lv) = object ["SV" .= lv]
236 toJSON (SApp tail name exps) = object ["SApp" .= (tail, name, exps)]
237 toJSON (SLet lv a b) = object ["SLet" .= (lv, a, b)]
238 toJSON (SUpdate lv exp) = object ["SUpdate" .= (lv, exp)]
239 toJSON (SProj lv i) = object ["SProj" .= (lv, i)]
240 toJSON (SCon lv i name vars) = object ["SCon" .= (lv, i, name, vars)]
241 toJSON (SCase ct lv alts) = object ["SCase" .= (ct, lv, alts)]
242 toJSON (SChkCase lv alts) = object ["SChkCase" .= (lv, alts)]
243 toJSON (SConst c) = object ["SConst" .= c]
244 toJSON (SForeign fd ret exps) = object ["SForeign" .= (fd, ret, exps)]
245 toJSON (SOp prim vars) = object ["SOp" .= (prim, vars)]
246 toJSON SNothing = object ["SNothing" .= Null]
247 toJSON (SError s) = object ["SError" .= s]
249instance ToJSON SAlt where
250 toJSON (SConCase i j n ns exp) = object ["SConCase" .= (i, j, n, ns, exp)]
251 toJSON (SConstCase c exp) = object ["SConstCase" .= (c, exp)]
252 toJSON (SDefaultCase exp) = object ["SDefaultCase" .= exp]
254instance ToJSON BC where
255 toJSON (ASSIGN r1 r2) = object ["ASSIGN" .= (r1, r2)]
256 toJSON (ASSIGNCONST r c) = object ["ASSIGNCONST" .= (r, c)]
257 toJSON (UPDATE r1 r2) = object ["UPDATE" .= (r1, r2)]
258 toJSON (MKCON con mr i regs) = object ["MKCON" .= (con, mr, i, regs)]
259 toJSON (CASE b r alts def) = object ["CASE" .= (b, r, alts, def)]
260 toJSON (PROJECT r loc arity) = object ["PROJECT" .= (r, loc, arity)]
261 toJSON (PROJECTINTO r1 r2 loc) = object ["PROJECTINTO" .= (r1, r2, loc)]
262 toJSON (CONSTCASE r alts def) = object ["CONSTCASE" .= (r, alts, def)]
263 toJSON (CALL name) = object ["CALL" .= name]
264 toJSON (TAILCALL name) = object ["TAILCALL" .= name]
265 toJSON (FOREIGNCALL r fd ret exps) = object ["FOREIGNCALL" .= (r, fd, ret, exps)]
266 toJSON (SLIDE i) = object ["SLIDE" .= i]
267 toJSON (RESERVE i) = object ["RESERVE" .= i]
268 toJSON (RESERVENOALLOC i) = object ["RESERVENOALLOC" .= i]
269 toJSON (ADDTOP i) = object ["ADDTOP" .= i]
270 toJSON (TOPBASE i) = object ["TOPBASE" .= i]
271 toJSON (BASETOP i) = object ["BASETOP" .= i]
272 toJSON REBASE = object ["REBASE" .= Null]
273 toJSON STOREOLD = object ["STOREOLD" .= Null]
274 toJSON (OP r prim args) = object ["OP" .= (r, prim, args)]
275 toJSON (NULL r) = object ["NULL" .= r]
276 toJSON (ERROR s) = object ["ERROR" .= s]
278instance ToJSON Reg where
279 toJSON RVal = object ["RVal" .= Null]
280 toJSON (T i) = object ["T" .= i]
281 toJSON (L i) = object ["L" .= i]
282 toJSON Tmp = object ["Tmp" .= Null]
284instance ToJSON RigCount where
285 toJSON r = object ["RigCount" .= show r]
287instance ToJSON Totality where
288 toJSON t = object ["Totality" .= show t]
290instance ToJSON MetaInformation where
291 toJSON m = object ["MetaInformation" .= show m]
293instance ToJSON Def where
294 toJSON (Function ty tm) = object ["Function" .= (ty, tm)]
295 toJSON (TyDecl nm ty) = object ["TyDecl" .= (nm, ty)]
296 toJSON (Operator ty n f) = Null -- Operator and CaseOp omits same values as in IBC.hs
297 toJSON (CaseOp info ty argTy _ _ cdefs) = object ["CaseOp" .= (info, ty, argTy, cdefs)]
299instance (ToJSON t) => ToJSON (TT t) where
300 toJSON (P nt name term) = object ["P" .= (nt, name, term)]
301 toJSON (V n) = object ["V" .= n]
302 toJSON (Bind n b tt) = object ["Bind" .= (n, b, tt)]
303 toJSON (App s t1 t2) = object ["App" .= (s, t1, t2)]
304 toJSON (Constant c) = object ["Constant" .= c]
305 toJSON (Proj tt n) = object ["Proj" .= (tt, n)]
306 toJSON Erased = object ["Erased" .= Null]
307 toJSON Impossible = object ["Impossible" .= Null]
308 toJSON (Inferred tt) = object ["Inferred" .= tt]
309 toJSON (TType u) = object ["TType" .= u]
310 toJSON (UType u) = object ["UType" .= (show u)]
312instance ToJSON UExp where
313 toJSON (UVar src n) = object ["UVar" .= (src, n)]
314 toJSON (UVal n) = object ["UVal" .= n]
317instance (ToJSON t) => ToJSON (AppStatus t) where
318 toJSON Complete = object ["Complete" .= Null]
319 toJSON MaybeHoles = object ["MaybeHoles" .= Null]
320 toJSON (Holes ns) = object ["Holes" .= ns]
322instance (ToJSON t) => ToJSON (Binder t) where
323 toJSON (Lam rc bty) = object ["Lam" .= (rc, bty)]
324 toJSON (Pi c i t k) = object ["Pi" .= (c, i, t, k)]
325 toJSON (Let rc t v) = object ["Let" .= (t, v)]
326 toJSON (NLet t v) = object ["NLet" .= (t, v)]
327 toJSON (Hole t) = object ["Hole" .= (t)]
328 toJSON (GHole l ns t) = object ["GHole" .= (l, ns, t)]
329 toJSON (Guess t v) = object ["Guess" .= (t, v)]
330 toJSON (PVar rc t) = object ["PVar" .= (rc, t)]
331 toJSON (PVTy t) = object ["PVTy" .= (t)]
333instance ToJSON ImplicitInfo where
334 toJSON (Impl a b c) = object ["Impl" .= (a, b, c)]
336instance ToJSON NameType where
337 toJSON Bound = object ["Bound" .= Null]
338 toJSON Ref = object ["Ref" .= Null]
339 toJSON (DCon a b c) = object ["DCon" .= (a, b, c)]
340 toJSON (TCon a b) = object ["TCon" .= (a, b)]
342instance ToJSON CaseDefs where
343 toJSON (CaseDefs rt ct) = object ["Runtime" .= rt, "Compiletime" .= ct]
345instance (ToJSON t) => ToJSON (SC' t) where
346 toJSON (Case ct n alts) = object ["Case" .= (ct, n, alts)]
347 toJSON (ProjCase t alts) = object ["ProjCase" .= (t, alts)]
348 toJSON (STerm t) = object ["STerm" .= t]
349 toJSON (UnmatchedCase s) = object ["UnmatchedCase" .= s]
350 toJSON ImpossibleCase = object ["ImpossibleCase" .= Null]
352instance (ToJSON t) => ToJSON (CaseAlt' t) where
353 toJSON (ConCase n c ns sc) = object ["ConCase" .= (n, c, ns, sc)]
354 toJSON (FnCase n ns sc) = object ["FnCase" .= (n, ns, sc)]
355 toJSON (ConstCase c sc) = object ["ConstCase" .= (c, sc)]
356 toJSON (SucCase n sc) = object ["SucCase" .= (n, sc)]
357 toJSON (DefaultCase sc) = object ["DefaultCase" .= sc]
359instance ToJSON CaseInfo where
360 toJSON (CaseInfo a b c) = object ["CaseInfo" .= (a, b, c)]
362instance ToJSON Accessibility where
363 toJSON a = object ["Accessibility" .= show a]