git.iko.soy/Idris-dev
on master help sign in
add TT to CodegenInfo
2339c66joe9
src/IRTS/CodegenCommon.hs+2
compare with master
unifiedsplit
@@ -8,6 +8,7 @@ Maintainer : The Idris Community.
8-}
8-}
9module IRTS.CodegenCommon where
9module IRTS.CodegenCommon where
10
10
11+import Idris.Core.Evaluate
11import Idris.Core.TT
12import Idris.Core.TT
12import IRTS.Defunctionalise
13import IRTS.Defunctionalise
13import IRTS.Simplified
14import IRTS.Simplified
@@ -39,6 +40,7 @@ data CodegenInfo = CodegenInfo {
39 , liftDecls :: [(Name, LDecl)]
40 , liftDecls :: [(Name, LDecl)]
40 , interfaces :: Bool
41 , interfaces :: Bool
41 , exportDecls :: [ExportIFace]
42 , exportDecls :: [ExportIFace]
43+ , ttDecls :: [(Name, (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation))]
42 }
44 }
43
45
44type CodeGenerator = CodegenInfo -> IO ()
46type CodeGenerator = CodegenInfo -> IO ()
src/IRTS/Compiler.hs+8
@@ -74,6 +74,7 @@ compile codegen f mtm = do
74 flags <- getFlags codegen
74 flags <- getFlags codegen
75 hdrs <- getHdrs codegen
75 hdrs <- getHdrs codegen
76 impdirs <- allImportDirs
76 impdirs <- allImportDirs
77+ ttDeclarations <- getDeclarations reachableNames
77 defsIn <- mkDecls reachableNames
78 defsIn <- mkDecls reachableNames
78 -- if no 'main term' given, generate interface files
79 -- if no 'main term' given, generate interface files
79 let iface = case mtm of
80 let iface = case mtm of
@@ -119,6 +120,7 @@ compile codegen f mtm = do
119 hdrs impdirs objs libs flags
120 hdrs impdirs objs libs flags
120 NONE c (toAlist defuns)
121 NONE c (toAlist defuns)
121 tagged iface exports
122 tagged iface exports
123+ ttDeclarations
122 Error e -> ierror e
124 Error e -> ierror e
123 where checkMVs = do i <- getIState
125 where checkMVs = do i <- getIState
124 case map fst (idris_metavars i) \\ primDefs of
126 case map fst (idris_metavars i) \\ primDefs of
@@ -164,6 +166,12 @@ mkDecls used
164 decls <- mapM build ds
166 decls <- mapM build ds
165 return decls
167 return decls
166
168
169+getDeclarations :: [Name] -> Idris ([(Name, (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation))])
170+getDeclarations used
171+ = do i <- getIState
172+ let ds = filter (\(n, (d,_,_,_,_,_)) -> n `elem` used || isCon d) $ ((toAlist . definitions . tt_ctxt) i)
173+ return ds
174+
167showCaseTrees :: [(Name, LDecl)] -> String
175showCaseTrees :: [(Name, LDecl)] -> String
168showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)
176showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)
169 where
177 where
src/IRTS/Portable.hs+18−1
@@ -9,6 +9,7 @@ Maintainer : The Idris Community.
9module IRTS.Portable (writePortable) where
9module IRTS.Portable (writePortable) where
10
10
11import Idris.Core.CaseTree
11import Idris.Core.CaseTree
12+import Idris.Core.Evaluate
12import Idris.Core.TT
13import Idris.Core.TT
13import IRTS.Bytecode
14import IRTS.Bytecode
14import IRTS.CodegenCommon
15import IRTS.CodegenCommon
@@ -53,7 +54,8 @@ instance ToJSON CodegenInfo where
53 "lift-decls" .= (liftDecls ci),
54 "lift-decls" .= (liftDecls ci),
54 "defun-decls" .= (defunDecls ci),
55 "defun-decls" .= (defunDecls ci),
55 "simple-decls" .= (simpleDecls ci),
56 "simple-decls" .= (simpleDecls ci),
56− "bytecode" .= (map toBC (simpleDecls ci))]
57+ "bytecode" .= (map toBC (simpleDecls ci)),
58+ "tt-decls" .= (ttDecls ci)]
57
59
58instance ToJSON Name where
60instance ToJSON Name where
59 toJSON n = toJSON $ showCG n
61 toJSON n = toJSON $ showCG n
@@ -279,3 +281,18 @@ instance ToJSON Reg where
279 toJSON (T i) = object ["T" .= i]
281 toJSON (T i) = object ["T" .= i]
280 toJSON (L i) = object ["L" .= i]
282 toJSON (L i) = object ["L" .= i]
281 toJSON Tmp = object ["Tmp" .= Null]
283 toJSON Tmp = object ["Tmp" .= Null]
284+
285+instance ToJSON RigCount where
286+ toJSON r = object ["RigCount" .= show r]
287+
288+instance ToJSON Totality where
289+ toJSON t = object ["Totality" .= show t]
290+
291+instance ToJSON MetaInformation where
292+ toJSON m = object ["MetaInformation" .= show m]
293+
294+instance ToJSON Def where
295+ toJSON d = object ["Def" .= show d]
296+
297+instance ToJSON Accessibility where
298+ toJSON a = object ["Accessibility" .= show a]