git.iko.soy/Idris-dev
on master help sign in
add TT to CodegenInfo
commit2339c666880ab6652703b292a6479039eca331dc authorjoe9 <joe9mail@gmail.com> dateFri 20 Jan 2017, 12:31 (10 years ago) parent3b95b07
3 files changed+28−1
compare with master
unifiedsplit
src/IRTS/CodegenCommon.hs+2 src/IRTS/Compiler.hs+8 src/IRTS/Portable.hs+18−1
src/IRTS/CodegenCommon.hs+2
@@ -8,6 +8,7 @@ Maintainer : The Idris Community.
88-}
99module IRTS.CodegenCommon where
1010
11+import Idris.Core.Evaluate
1112import Idris.Core.TT
1213import IRTS.Defunctionalise
1314import IRTS.Simplified
@@ -39,6 +40,7 @@ data CodegenInfo = CodegenInfo {
3940 , liftDecls :: [(Name, LDecl)]
4041 , interfaces :: Bool
4142 , exportDecls :: [ExportIFace]
43+ , ttDecls :: [(Name, (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation))]
4244 }
4345
4446type CodeGenerator = CodegenInfo -> IO ()
src/IRTS/Compiler.hs+8
@@ -74,6 +74,7 @@ compile codegen f mtm = do
7474 flags <- getFlags codegen
7575 hdrs <- getHdrs codegen
7676 impdirs <- allImportDirs
77+ ttDeclarations <- getDeclarations reachableNames
7778 defsIn <- mkDecls reachableNames
7879 -- if no 'main term' given, generate interface files
7980 let iface = case mtm of
@@ -119,6 +120,7 @@ compile codegen f mtm = do
119120 hdrs impdirs objs libs flags
120121 NONE c (toAlist defuns)
121122 tagged iface exports
123+ ttDeclarations
122124 Error e -> ierror e
123125 where checkMVs = do i <- getIState
124126 case map fst (idris_metavars i) \\ primDefs of
@@ -164,6 +166,12 @@ mkDecls used
164166 decls <- mapM build ds
165167 return decls
166168
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+
167175showCaseTrees :: [(Name, LDecl)] -> String
168176showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)
169177 where
src/IRTS/Portable.hs+18−1
@@ -9,6 +9,7 @@ Maintainer : The Idris Community.
99module IRTS.Portable (writePortable) where
1010
1111import Idris.Core.CaseTree
12+import Idris.Core.Evaluate
1213import Idris.Core.TT
1314import IRTS.Bytecode
1415import IRTS.CodegenCommon
@@ -53,7 +54,8 @@ instance ToJSON CodegenInfo where
5354 "lift-decls" .= (liftDecls ci),
5455 "defun-decls" .= (defunDecls ci),
5556 "simple-decls" .= (simpleDecls ci),
56− "bytecode" .= (map toBC (simpleDecls ci))]
57+ "bytecode" .= (map toBC (simpleDecls ci)),
58+ "tt-decls" .= (ttDecls ci)]
5759
5860instance ToJSON Name where
5961 toJSON n = toJSON $ showCG n
@@ -279,3 +281,18 @@ instance ToJSON Reg where
279281 toJSON (T i) = object ["T" .= i]
280282 toJSON (L i) = object ["L" .= i]
281283 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]