git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3173 from melted/portable_json
5ef9bf4Niklas Larsson
codegen/idris-codegen-c/Main.hs+1−1
compare with master
unifiedsplit
@@ -40,7 +40,7 @@ c_main opts = do runIO setupBundledCC
40 mainProg <- if interface opts
40 mainProg <- if interface opts
41 then liftM Just elabMain
41 then liftM Just elabMain
42 else return Nothing
42 else return Nothing
43− ir <- compile (Via "c") (output opts) mainProg
43+ ir <- compile (Via IBCFormat "c") (output opts) mainProg
44 runIO $ codegenC ir
44 runIO $ codegenC ir
45
45
46main :: IO ()
46main :: IO ()
codegen/idris-codegen-javascript/Main.hs+1−1
@@ -34,7 +34,7 @@ jsMain :: Opts -> Idris ()
34jsMain opts = do elabPrims
34jsMain opts = do elabPrims
35 loadInputs (inputs opts) Nothing
35 loadInputs (inputs opts) Nothing
36 mainProg <- elabMain
36 mainProg <- elabMain
37− ir <- compile (Via "javascript") (output opts) (Just mainProg)
37+ ir <- compile (Via IBCFormat "javascript") (output opts) (Just mainProg)
38 runIO $ codegenJavaScript ir
38 runIO $ codegenJavaScript ir
39
39
40main :: IO ()
40main :: IO ()
codegen/idris-codegen-node/Main.hs+1−1
@@ -33,7 +33,7 @@ jsMain :: Opts -> Idris ()
33jsMain opts = do elabPrims
33jsMain opts = do elabPrims
34 loadInputs (inputs opts) Nothing
34 loadInputs (inputs opts) Nothing
35 mainProg <- elabMain
35 mainProg <- elabMain
36− ir <- compile (Via "node") (output opts) (Just mainProg)
36+ ir <- compile (Via IBCFormat "node") (output opts) (Just mainProg)
37 runIO $ codegenNode ir
37 runIO $ codegenNode ir
38
38
39main :: IO ()
39main :: IO ()
idris.cabal+3−1
@@ -606,7 +606,7 @@ Extra-source-files:
606 test/interactive013/input
606 test/interactive013/input
607 test/interactive013/run
607 test/interactive013/run
608 test/interactive013/*.idr
608 test/interactive013/*.idr
609−
609+
610 test/interfaces001/*.idr
610 test/interfaces001/*.idr
611 test/interfaces001/run
611 test/interfaces001/run
612 test/interfaces001/expected
612 test/interfaces001/expected
@@ -1031,6 +1031,7 @@ Library
1031 , IRTS.Inliner
1031 , IRTS.Inliner
1032 , IRTS.Lang
1032 , IRTS.Lang
1033 , IRTS.LangOpts
1033 , IRTS.LangOpts
1034+ , IRTS.Portable
1034 , IRTS.Simplified
1035 , IRTS.Simplified
1035 , IRTS.System
1036 , IRTS.System
1036
1037
@@ -1051,6 +1052,7 @@ Library
1051 , Tools_idris
1052 , Tools_idris
1052
1053
1053 Build-depends: base >=4 && <5
1054 Build-depends: base >=4 && <5
1055+ , aeson >= 0.6 && < 0.12
1054 , annotated-wl-pprint >= 0.7 && < 0.8
1056 , annotated-wl-pprint >= 0.7 && < 0.8
1055 , ansi-terminal < 0.7
1057 , ansi-terminal < 0.7
1056 , ansi-wl-pprint < 0.7
1058 , ansi-wl-pprint < 0.7
src/IRTS/Compiler.hs+16−7
@@ -12,6 +12,7 @@ import IRTS.DumpBC
12import IRTS.CodegenJavaScript
12import IRTS.CodegenJavaScript
13import IRTS.Inliner
13import IRTS.Inliner
14import IRTS.Exports
14import IRTS.Exports
15+import IRTS.Portable
15
16
16import Idris.AbsSyntax
17import Idris.AbsSyntax
17import Idris.AbsSyntaxTree
18import Idris.AbsSyntaxTree
@@ -125,13 +126,21 @@ generate :: Codegen -> FilePath -> CodegenInfo -> IO ()
125generate codegen mainmod ir
126generate codegen mainmod ir
126 = case codegen of
127 = case codegen of
127 -- Built-in code generators (FIXME: lift these out!)
128 -- Built-in code generators (FIXME: lift these out!)
128− Via "c" -> codegenC ir
129+ Via _ "c" -> codegenC ir
129 -- Any external code generator
130 -- Any external code generator
131+ Via fm cg -> do input <- case fm of
132+ IBCFormat -> return mainmod
133+ JSONFormat -> do
134+ tempdir <- getTemporaryDirectory
135+ (fn, h) <- openTempFile tempdir "idris-cg.json"
136+ writePortable h ir
137+ hClose h
138+ return fn
130− Via cg -> do let cmd = "idris-codegen-" ++ cg
139+ let cmd = "idris-codegen-" ++ cg
131− args = [mainmod, "-o", outputFile ir] ++ compilerFlags ir
140+ args = [input, "-o", outputFile ir] ++ compilerFlags ir
132− exit <- rawSystem cmd args
141+ exit <- rawSystem cmd args
133− when (exit /= ExitSuccess) $
142+ when (exit /= ExitSuccess) $
134− putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)
143+ putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)
135 Bytecode -> dumpBC (simpleDecls ir) (outputFile ir)
144 Bytecode -> dumpBC (simpleDecls ir) (outputFile ir)
136
145
137irMain :: TT Name -> Idris LDecl
146irMain :: TT Name -> Idris LDecl
@@ -350,7 +359,7 @@ irTerm vs env tm@(App _ f a) = do
350
359
351 -- overapplied
360 -- overapplied
352 GT -> ifail ("overapplied data constructor: " ++ show tm ++
361 GT -> ifail ("overapplied data constructor: " ++ show tm ++
353− "\nDEBUG INFO:\n" ++
362+ "\nDEBUG INFO:\n" ++
354 "Arity: " ++ show arity ++ "\n" ++
363 "Arity: " ++ show arity ++ "\n" ++
355 "Arguments: " ++ show args ++ "\n" ++
364 "Arguments: " ++ show args ++ "\n" ++
356 "Pruned arguments: " ++ show argsPruned)
365 "Pruned arguments: " ++ show argsPruned)
src/IRTS/Portable.hsnew file+277
@@ -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]
src/Idris/AbsSyntax.hs+9−4
@@ -45,7 +45,11 @@ getContext :: Idris Context
45getContext = do i <- getIState; return (tt_ctxt i)
45getContext = do i <- getIState; return (tt_ctxt i)
46
46
47forCodegen :: Codegen -> [(Codegen, a)] -> [a]
47forCodegen :: Codegen -> [(Codegen, a)] -> [a]
48−forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
48+forCodegen tgt xs = [x | (tgt', x) <- xs, eqLang tgt tgt']
49+ where
50+ eqLang (Via _ x) (Via _ y) = x == y
51+ eqLang Bytecode Bytecode = True
52+ eqLang _ _ = False
49
53
50getObjectFiles :: Codegen -> Idris [FilePath]
54getObjectFiles :: Codegen -> Idris [FilePath]
51getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
55getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
@@ -459,13 +463,13 @@ addInstance int res n i
459-- Returns the old list, so we can revert easily at the end of a block
463-- Returns the old list, so we can revert easily at the end of a block
460
464
461addOpenImpl :: [Name] -> Idris [Name]
465addOpenImpl :: [Name] -> Idris [Name]
462−addOpenImpl ns = do ist <- getIState
466+addOpenImpl ns = do ist <- getIState
463 ns' <- mapM (checkValid ist) ns
467 ns' <- mapM (checkValid ist) ns
464 let open = idris_openimpls ist
468 let open = idris_openimpls ist
465 putIState $ ist { idris_openimpls = nub (ns' ++ open) }
469 putIState $ ist { idris_openimpls = nub (ns' ++ open) }
466 return open
470 return open
467 where
471 where
468− checkValid ist n
472+ checkValid ist n
469 = case lookupCtxtName n (idris_implicits ist) of
473 = case lookupCtxtName n (idris_implicits ist) of
470 [(n', _)] -> return n'
474 [(n', _)] -> return n'
471 [] -> throwError (NoSuchVariable n)
475 [] -> throwError (NoSuchVariable n)
@@ -946,6 +950,7 @@ codegen :: Idris Codegen
946codegen = do i <- getIState
950codegen = do i <- getIState
947 return (opt_codegen (idris_options i))
951 return (opt_codegen (idris_options i))
948
952
953+
949setOutputTy :: OutputType -> Idris ()
954setOutputTy :: OutputType -> Idris ()
950setOutputTy t = do i <- getIState
955setOutputTy t = do i <- getIState
951 let opts = idris_options i
956 let opts = idris_options i
@@ -2329,7 +2334,7 @@ shadow n n' t = sm 0 t where
2329 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
2334 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
2330 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)
2335 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)
2331 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)
2336 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)
2332− sm 0 (PAlternative ms a as)
2337+ sm 0 (PAlternative ms a as)
2333 = PAlternative (map shadowAlt ms) a (map (sm 0) as)
2338 = PAlternative (map shadowAlt ms) a (map (sm 0) as)
2334 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2339 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2335 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
2340 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
src/Idris/AbsSyntaxTree.hs+5−8
@@ -112,7 +112,7 @@ defaultOpts = IOption { opt_logLevel = 0
112 , opt_verbose = True
112 , opt_verbose = True
113 , opt_nobanner = False
113 , opt_nobanner = False
114 , opt_quiet = False
114 , opt_quiet = False
115− , opt_codegen = Via "c"
115+ , opt_codegen = Via IBCFormat "c"
116 , opt_outputTy = Executable
116 , opt_outputTy = Executable
117 , opt_ibcsubdir = ""
117 , opt_ibcsubdir = ""
118 , opt_importdirs = []
118 , opt_importdirs = []
@@ -186,7 +186,7 @@ data DefaultTotality = DefaultCheckingTotal -- ^ Total
186 | DefaultCheckingPartial -- ^ Partial
186 | DefaultCheckingPartial -- ^ Partial
187 | DefaultCheckingCovering -- ^Total coverage, but may diverge
187 | DefaultCheckingCovering -- ^Total coverage, but may diverge
188 deriving (Show, Eq)
188 deriving (Show, Eq)
189−
189+
190-- | The global state used in the Idris monad
190-- | The global state used in the Idris monad
191data IState = IState {
191data IState = IState {
192 tt_ctxt :: Context, -- ^ All the currently defined names and their terms
192 tt_ctxt :: Context, -- ^ All the currently defined names and their terms
@@ -386,18 +386,15 @@ throwError = Trans.lift . throwE
386
386
387-- Commands in the REPL
387-- Commands in the REPL
388
388
389−data Codegen = Via String
389+data Codegen = Via IRFormat String
390−-- | ViaC
391−-- | ViaJava
392−-- | ViaNode
393−-- | ViaJavaScript
394−-- | ViaLLVM
395 | Bytecode
390 | Bytecode
396 deriving (Show, Eq)
391 deriving (Show, Eq)
397{-!
392{-!
398deriving instance NFData Codegen
393deriving instance NFData Codegen
399!-}
394!-}
400
395
396+data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq)
397+
401data HowMuchDocs = FullDocs | OverviewDocs
398data HowMuchDocs = FullDocs | OverviewDocs
402
399
403-- | REPL commands
400-- | REPL commands
src/Idris/CmdOptions.hs+8−1
@@ -149,6 +149,12 @@ parseFlags = many $
149 <|> ((\s -> UseCodegen $ parseCodegen s) <$> strOption (long "codegen"
149 <|> ((\s -> UseCodegen $ parseCodegen s) <$> strOption (long "codegen"
150 <> metavar "TARGET"
150 <> metavar "TARGET"
151 <> help "Select code generator: C, Javascript, Node and bytecode are bundled with Idris"))
151 <> help "Select code generator: C, Javascript, Node and bytecode are bundled with Idris"))
152+
153+
154+ <|> ((\s -> UseCodegen $ Via JSONFormat s) <$> strOption (long "portable-codegen"
155+ <> metavar "TARGET"
156+ <> help "Pass the name of the code generator. This option is for codegens that take JSON formatted IR."))
157+
152 <|> (CodegenArgs <$> strOption (long "cg-opt"
158 <|> (CodegenArgs <$> strOption (long "cg-opt"
153 <> metavar "ARG"
159 <> metavar "ARG"
154 <> help "Arguments to pass to code generator"))
160 <> help "Arguments to pass to code generator"))
@@ -206,7 +212,8 @@ preProcOpts (x:xs) ys = preProcOpts xs (x:ys)
206
212
207parseCodegen :: String -> Codegen
213parseCodegen :: String -> Codegen
208parseCodegen "bytecode" = Bytecode
214parseCodegen "bytecode" = Bytecode
209−parseCodegen cg = Via (map toLower cg)
215+parseCodegen cg = Via IBCFormat (map toLower cg)
216+
210
217
211parseLogCats :: Monad m => String -> m [LogCat]
218parseLogCats :: Monad m => String -> m [LogCat]
212parseLogCats s =
219parseLogCats s =
src/Idris/DeepSeq.hs+5−2
@@ -361,9 +361,12 @@ instance NFData FnInfo where
361 rnf (FnInfo x1) = rnf x1 `seq` ()
361 rnf (FnInfo x1) = rnf x1 `seq` ()
362
362
363instance NFData Codegen where
363instance NFData Codegen where
364− rnf (Via x1) = rnf x1 `seq` ()
364+ rnf (Via x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
365 rnf Bytecode = ()
365 rnf Bytecode = ()
366
366
367+instance NFData IRFormat where
368+ rnf _ = ()
369+
367instance NFData LogCat where
370instance NFData LogCat where
368 rnf _ = ()
371 rnf _ = ()
369
372
@@ -700,7 +703,7 @@ instance NFData DefaultTotality where
700 rnf DefaultCheckingTotal = ()
703 rnf DefaultCheckingTotal = ()
701 rnf DefaultCheckingPartial = ()
704 rnf DefaultCheckingPartial = ()
702 rnf DefaultCheckingCovering = ()
705 rnf DefaultCheckingCovering = ()
703−
706+
704instance NFData IState where
707instance NFData IState where
705 rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20
708 rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20
706 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40
709 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40
src/Idris/IBC.hs+16−4
@@ -40,7 +40,7 @@ import System.Directory
40import Codec.Archive.Zip
40import Codec.Archive.Zip
41
41
42ibcVersion :: Word16
42ibcVersion :: Word16
43−ibcVersion = 142
43+ibcVersion = 143
44
44
45-- When IBC is being loaded - we'll load different things (and omit different
45-- When IBC is being loaded - we'll load different things (and omit different
46-- structures/definitions) depending on which phase we're in
46-- structures/definitions) depending on which phase we're in
@@ -2461,13 +2461,25 @@ instance Binary SSymbol where
2461instance Binary Codegen where
2461instance Binary Codegen where
2462 put x
2462 put x
2463 = case x of
2463 = case x of
2464− Via str -> do putWord8 0
2464+ Via ir str -> do putWord8 0
2465+ put ir
2465− put str
2466+ put str
2466 Bytecode -> putWord8 1
2467 Bytecode -> putWord8 1
2467 get
2468 get
2468 = do i <- getWord8
2469 = do i <- getWord8
2469 case i of
2470 case i of
2470 0 -> do x1 <- get
2471 0 -> do x1 <- get
2472+ x2 <- get
2471− return (Via x1)
2473+ return (Via x1 x2)
2472 1 -> return Bytecode
2474 1 -> return Bytecode
2473 _ -> error "Corrupted binary data for Codegen"
2475 _ -> error "Corrupted binary data for Codegen"
2476+
2477+instance Binary IRFormat where
2478+ put x = case x of
2479+ IBCFormat -> putWord8 0
2480+ JSONFormat -> putWord8 1
2481+ get = do i <- getWord8
2482+ case i of
2483+ 0 -> return IBCFormat
2484+ 1 -> return JSONFormat
2485+ _ -> error "Corrupted binary data for IRFormat"
src/Idris/Parser.hs+6−6
@@ -781,7 +781,7 @@ params syn =
781 return [PParams fc ns' (concat ds)]
781 return [PParams fc ns' (concat ds)]
782 <?> "parameters declaration"
782 <?> "parameters declaration"
783
783
784−{- | Parses an open block
784+{- | Parses an open block
785
785
786-}
786-}
787
787
@@ -790,7 +790,7 @@ openInterface syn =
790 do reservedHL "using"
790 do reservedHL "using"
791 reservedHL "implementation"
791 reservedHL "implementation"
792 fc <- getFC
792 fc <- getFC
793− ns <- sepBy1 fnName (lchar ',')
793+ ns <- sepBy1 fnName (lchar ',')
794
794
795 openBlock
795 openBlock
796 ds <- many (decl syn)
796 ds <- many (decl syn)
@@ -799,7 +799,7 @@ openInterface syn =
799 <?> "open interface declaration"
799 <?> "open interface declaration"
800
800
801
801
802−
802+
803
803
804{- | Parses a mutual declaration (for mutually recursive functions)
804{- | Parses a mutual declaration (for mutually recursive functions)
805
805
@@ -877,7 +877,7 @@ classBlock syn = do reservedHL "where"
877 ist <- get
877 ist <- get
878 let cd' = annotate syn ist cd
878 let cd' = annotate syn ist cd
879
879
880− ds <- many (notEndBlock >> try (instance_ True syn)
880+ ds <- many (notEndBlock >> try (instance_ True syn)
881 <|> do x <- data_ syn
881 <|> do x <- data_ syn
882 return [x]
882 return [x]
883 <|> fnDecl syn)
883 <|> fnDecl syn)
@@ -1324,7 +1324,7 @@ Codegen ::= 'C'
1324-}
1324-}
1325codegen_ :: IdrisParser Codegen
1325codegen_ :: IdrisParser Codegen
1326codegen_ = do n <- fst <$> identifier
1326codegen_ = do n <- fst <$> identifier
1327− return (Via (map toLower n))
1327+ return (Via IBCFormat (map toLower n))
1328 <|> do reserved "Bytecode"; return Bytecode
1328 <|> do reserved "Bytecode"; return Bytecode
1329 <?> "code generation language"
1329 <?> "code generation language"
1330
1330
@@ -1812,7 +1812,7 @@ loadSource lidr f toline
1812 logLvl 2 $ "Totality checking " ++ show deftots
1812 logLvl 2 $ "Totality checking " ++ show deftots
1813 mapM_ (\x -> do tot <- getTotality x
1813 mapM_ (\x -> do tot <- getTotality x
1814 case tot of
1814 case tot of
1815− Total _ ->
1815+ Total _ ->
1816 do let opts = case lookupCtxtExact x (idris_flags i) of
1816 do let opts = case lookupCtxtExact x (idris_flags i) of
1817 Just os -> os
1817 Just os -> os
1818 Nothing -> []
1818 Nothing -> []
src/Idris/REPL.hs+1−2
@@ -1249,7 +1249,6 @@ process fn (Compile codegen f)
1249 [pexp $ PRef fc [] mainname])
1249 [pexp $ PRef fc [] mainname])
1250 return (Just m')
1250 return (Just m')
1251 ir <- compile codegen f m
1251 ir <- compile codegen f m
1252−
1253 i <- getIState
1252 i <- getIState
1254 runIO $ generate codegen (fst (head (idris_imported i))) ir
1253 runIO $ generate codegen (fst (head (idris_imported i))) ir
1255 where fc = fileFC "main"
1254 where fc = fileFC "main"
@@ -1688,7 +1687,7 @@ idrisMain opts =
1688 Object else Executable
1687 Object else Executable
1689 xs -> last xs
1688 xs -> last xs
1690 let cgn = case opt getCodegen opts of
1689 let cgn = case opt getCodegen opts of
1691− [] -> Via "c"
1690+ [] -> Via IBCFormat "c"
1692 xs -> last xs
1691 xs -> last xs
1693 let cgFlags = opt getCodegenArgs opts
1692 let cgFlags = opt getCodegenArgs opts
1694
1693
src/Idris/REPL/Parser.hs+2−2
@@ -358,13 +358,13 @@ cmd_pprint name = do
358
358
359cmd_compile :: String -> P.IdrisParser (Either String Command)
359cmd_compile :: String -> P.IdrisParser (Either String Command)
360cmd_compile name = do
360cmd_compile name = do
361− let defaultCodegen = Via "c"
361+ let defaultCodegen = Via IBCFormat "c"
362
362
363 let codegenOption :: P.IdrisParser Codegen
363 let codegenOption :: P.IdrisParser Codegen
364 codegenOption = do
364 codegenOption = do
365 let bytecodeCodegen = discard (P.symbol "bytecode") *> return Bytecode
365 let bytecodeCodegen = discard (P.symbol "bytecode") *> return Bytecode
366 viaCodegen = do x <- fst <$> P.identifier
366 viaCodegen = do x <- fst <$> P.identifier
367− return (Via (map toLower x))
367+ return (Via IBCFormat (map toLower x))
368 bytecodeCodegen <|> viaCodegen
368 bytecodeCodegen <|> viaCodegen
369
369
370 let hasOneArg = do
370 let hasOneArg = do