git.iko.soy/Idris-dev
on master help sign in
Export intermediate representation as JSON
80225afNiklas Larsson
idris.cabal+3−1
compare with master
unifiedsplit
@@ -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.11 && < 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+14−5
@@ -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
@@ -121,14 +122,22 @@ compile codegen f mtm
121 [] -> return ()
122 [] -> return ()
122 ((fc, msg):fs) -> ierror . At fc . Msg $ "Cannot compile:\n " ++ msg
123 ((fc, msg):fs) -> ierror . At fc . Msg $ "Cannot compile:\n " ++ msg
123
124
124−generate :: Codegen -> FilePath -> CodegenInfo -> IO ()
125+generate :: Codegen -> FilePath -> Bool -> CodegenInfo -> IO ()
125−generate codegen mainmod ir
126+generate codegen mainmod port 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 cg -> do input <- if port
132+ then do
133+ tempdir <- getTemporaryDirectory
134+ (fn, h) <- openTempFile tempdir "idris-cg.json"
135+ writePortable h ir
136+ hClose h
137+ return fn
138+ else return mainmod
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)
@@ -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+14−3
@@ -459,13 +459,13 @@ addInstance int res n i
459-- Returns the old list, so we can revert easily at the end of a block
459-- Returns the old list, so we can revert easily at the end of a block
460
460
461addOpenImpl :: [Name] -> Idris [Name]
461addOpenImpl :: [Name] -> Idris [Name]
462−addOpenImpl ns = do ist <- getIState
462+addOpenImpl ns = do ist <- getIState
463 ns' <- mapM (checkValid ist) ns
463 ns' <- mapM (checkValid ist) ns
464 let open = idris_openimpls ist
464 let open = idris_openimpls ist
465 putIState $ ist { idris_openimpls = nub (ns' ++ open) }
465 putIState $ ist { idris_openimpls = nub (ns' ++ open) }
466 return open
466 return open
467 where
467 where
468− checkValid ist n
468+ checkValid ist n
469 = case lookupCtxtName n (idris_implicits ist) of
469 = case lookupCtxtName n (idris_implicits ist) of
470 [(n', _)] -> return n'
470 [(n', _)] -> return n'
471 [] -> throwError (NoSuchVariable n)
471 [] -> throwError (NoSuchVariable n)
@@ -946,6 +946,17 @@ codegen :: Idris Codegen
946codegen = do i <- getIState
946codegen = do i <- getIState
947 return (opt_codegen (idris_options i))
947 return (opt_codegen (idris_options i))
948
948
949+setPortableCodegen :: Bool -> Idris ()
950+setPortableCodegen p = do i <- getIState
951+ let opts = idris_options i
952+ let opt' = opts { opt_portableCG = p }
953+ putIState $ i { idris_options = opt' }
954+
955+getPortableCodegen :: Idris Bool
956+getPortableCodegen = do i <- getIState
957+ let opts = idris_options i
958+ return (opt_portableCG opts)
959+
949setOutputTy :: OutputType -> Idris ()
960setOutputTy :: OutputType -> Idris ()
950setOutputTy t = do i <- getIState
961setOutputTy t = do i <- getIState
951 let opts = idris_options i
962 let opts = idris_options i
@@ -2329,7 +2340,7 @@ shadow n n' t = sm 0 t where
2329 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
2340 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)
2341 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)
2342 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)
2343+ sm 0 (PAlternative ms a as)
2333 = PAlternative (map shadowAlt ms) a (map (sm 0) as)
2344 = PAlternative (map shadowAlt ms) a (map (sm 0) as)
2334 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2345 sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
2335 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
2346 sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
src/Idris/AbsSyntaxTree.hs+4−1
@@ -85,6 +85,7 @@ data IOption = IOption {
85 , opt_nobanner :: Bool
85 , opt_nobanner :: Bool
86 , opt_quiet :: Bool
86 , opt_quiet :: Bool
87 , opt_codegen :: Codegen
87 , opt_codegen :: Codegen
88+ , opt_portableCG :: Bool
88 , opt_outputTy :: OutputType
89 , opt_outputTy :: OutputType
89 , opt_ibcsubdir :: FilePath
90 , opt_ibcsubdir :: FilePath
90 , opt_importdirs :: [FilePath]
91 , opt_importdirs :: [FilePath]
@@ -113,6 +114,7 @@ defaultOpts = IOption { opt_logLevel = 0
113 , opt_nobanner = False
114 , opt_nobanner = False
114 , opt_quiet = False
115 , opt_quiet = False
115 , opt_codegen = Via "c"
116 , opt_codegen = Via "c"
117+ , opt_portableCG = False
116 , opt_outputTy = Executable
118 , opt_outputTy = Executable
117 , opt_ibcsubdir = ""
119 , opt_ibcsubdir = ""
118 , opt_importdirs = []
120 , opt_importdirs = []
@@ -186,7 +188,7 @@ data DefaultTotality = DefaultCheckingTotal -- ^ Total
186 | DefaultCheckingPartial -- ^ Partial
188 | DefaultCheckingPartial -- ^ Partial
187 | DefaultCheckingCovering -- ^Total coverage, but may diverge
189 | DefaultCheckingCovering -- ^Total coverage, but may diverge
188 deriving (Show, Eq)
190 deriving (Show, Eq)
189−
191+
190-- | The global state used in the Idris monad
192-- | The global state used in the Idris monad
191data IState = IState {
193data IState = IState {
192 tt_ctxt :: Context, -- ^ All the currently defined names and their terms
194 tt_ctxt :: Context, -- ^ All the currently defined names and their terms
@@ -558,6 +560,7 @@ data Opt = Filename String
558 | DumpDefun String
560 | DumpDefun String
559 | DumpCases String
561 | DumpCases String
560 | UseCodegen Codegen
562 | UseCodegen Codegen
563+ | PortableCodegen
561 | CodegenArgs String
564 | CodegenArgs String
562 | OutputTy OutputType
565 | OutputTy OutputType
563 | Extension LanguageExt
566 | Extension LanguageExt
src/Idris/CmdOptions.hs+1
@@ -149,6 +149,7 @@ 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+ <|> flag' PortableCodegen (long "portable" <> help "Call codegen with json-formatted codegen info")
152 <|> (CodegenArgs <$> strOption (long "cg-opt"
153 <|> (CodegenArgs <$> strOption (long "cg-opt"
153 <> metavar "ARG"
154 <> metavar "ARG"
154 <> help "Arguments to pass to code generator"))
155 <> help "Arguments to pass to code generator"))
src/Idris/DeepSeq.hs+3−1
@@ -149,6 +149,7 @@ instance NFData Opt where
149 rnf (DumpDefun str) = rnf str `seq` ()
149 rnf (DumpDefun str) = rnf str `seq` ()
150 rnf (DumpCases str) = rnf str `seq` ()
150 rnf (DumpCases str) = rnf str `seq` ()
151 rnf (UseCodegen cg) = rnf cg `seq` ()
151 rnf (UseCodegen cg) = rnf cg `seq` ()
152+ rnf (PortableCodegen) = ()
152 rnf (CodegenArgs str) = rnf str `seq` ()
153 rnf (CodegenArgs str) = rnf str `seq` ()
153 rnf (OutputTy ot) = rnf ot `seq` ()
154 rnf (OutputTy ot) = rnf ot `seq` ()
154 rnf (Extension le) = rnf le `seq` ()
155 rnf (Extension le) = rnf le `seq` ()
@@ -187,6 +188,7 @@ instance NFData IOption where
187 opt_nobanner
188 opt_nobanner
188 opt_quiet
189 opt_quiet
189 opt_codegen
190 opt_codegen
191+ opt_portableCG
190 opt_outputTy
192 opt_outputTy
191 opt_ibcsubdir
193 opt_ibcsubdir
192 opt_importdirs
194 opt_importdirs
@@ -700,7 +702,7 @@ instance NFData DefaultTotality where
700 rnf DefaultCheckingTotal = ()
702 rnf DefaultCheckingTotal = ()
701 rnf DefaultCheckingPartial = ()
703 rnf DefaultCheckingPartial = ()
702 rnf DefaultCheckingCovering = ()
704 rnf DefaultCheckingCovering = ()
703−
705+
704instance NFData IState where
706instance 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
707 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
708 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40
src/Idris/REPL.hs+6−3
@@ -1228,7 +1228,8 @@ process fn (Execute tm)
1228 -- gcc adds .exe when it builds windows programs
1228 -- gcc adds .exe when it builds windows programs
1229 progName <- return $ if isWindows then tmpn ++ ".exe" else tmpn
1229 progName <- return $ if isWindows then tmpn ++ ".exe" else tmpn
1230 ir <- compile t tmpn (Just m)
1230 ir <- compile t tmpn (Just m)
1231+ port <- getPortableCodegen
1231− runIO $ generate t (fst (head (idris_imported ist))) ir
1232+ runIO $ generate t (fst (head (idris_imported ist))) port ir
1232 case idris_outputmode ist of
1233 case idris_outputmode ist of
1233 RawOutput h -> do runIO $ rawSystem progName []
1234 RawOutput h -> do runIO $ rawSystem progName []
1234 return ()
1235 return ()
@@ -1249,9 +1250,9 @@ process fn (Compile codegen f)
1249 [pexp $ PRef fc [] mainname])
1250 [pexp $ PRef fc [] mainname])
1250 return (Just m')
1251 return (Just m')
1251 ir <- compile codegen f m
1252 ir <- compile codegen f m
1252−
1253+ port <- getPortableCodegen
1253 i <- getIState
1254 i <- getIState
1254− runIO $ generate codegen (fst (head (idris_imported i))) ir
1255+ runIO $ generate codegen (fst (head (idris_imported i))) port ir
1255 where fc = fileFC "main"
1256 where fc = fileFC "main"
1256process fn (LogLvl i) = setLogLevel i
1257process fn (LogLvl i) = setLogLevel i
1257process fn (LogCategory cs) = setLogCats cs
1258process fn (LogCategory cs) = setLogCats cs
@@ -1690,6 +1691,7 @@ idrisMain opts =
1690 let cgn = case opt getCodegen opts of
1691 let cgn = case opt getCodegen opts of
1691 [] -> Via "c"
1692 [] -> Via "c"
1692 xs -> last xs
1693 xs -> last xs
1694+ let portable = PortableCodegen `elem` opts
1693 let cgFlags = opt getCodegenArgs opts
1695 let cgFlags = opt getCodegenArgs opts
1694
1696
1695 -- Now set/unset specifically chosen optimisations
1697 -- Now set/unset specifically chosen optimisations
@@ -1717,6 +1719,7 @@ idrisMain opts =
1717 setOutputTy outty
1719 setOutputTy outty
1718 setNoBanner nobanner
1720 setNoBanner nobanner
1719 setCodegen cgn
1721 setCodegen cgn
1722+ setPortableCodegen portable
1720 mapM_ (addFlag cgn) cgFlags
1723 mapM_ (addFlag cgn) cgFlags
1721 mapM_ makeOption opts
1724 mapM_ makeOption opts
1722 -- if we have the --bytecode flag, drop into the bytecode assembler
1725 -- if we have the --bytecode flag, drop into the bytecode assembler