git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3627 from joe9/master

add TT to CodegenInfo

commit14b5f3e3930c207ce5cab4d45abd2217d7cafd8e authorNiklas Larsson <metaniklas@gmail.com> dateSat 21 Jan 2017, 02:09 (10 years ago) parent3b95b07e4345f6
5 files changed+33−7
compare with master
unifiedsplit
src/IRTS/CodegenCommon.hs+2 src/IRTS/Compiler.hs+8 src/IRTS/Portable.hs+19−2 src/Idris/AbsSyntaxTree.hs+1−3 src/Idris/Core/Evaluate.hs+3−2
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, TTDecl)]
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, TTDecl)])
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+19−2
@@ -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
@@ -29,7 +30,7 @@ data CodegenFile = CGFile {
2930
3031-- Update the version when the format changes
3132formatVersion :: Int
32−formatVersion = 2
33+formatVersion = 3
3334
3435writePortable :: Handle -> CodegenInfo -> IO ()
3536writePortable file ci = do
@@ -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]
src/Idris/AbsSyntaxTree.hs+1−3
@@ -292,8 +292,6 @@ data IState = IState {
292292 , idris_postulates :: S.Set Name
293293 , idris_externs :: S.Set (Name, Int)
294294 , idris_erasureUsed :: [(Name, Int)] -- ^ Function/constructor name, argument position is used
295− , idris_whocalls :: Maybe (M.Map Name [Name])
296− , idris_callswho :: Maybe (M.Map Name [Name])
297295
298296 -- | List of names that were defined in the repl, and can be re-/un-defined
299297 , idris_repl_defs :: [Name]
@@ -413,7 +411,7 @@ idrisInit = IState initContext S.empty []
413411 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
414412 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
415413 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
416− AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
414+ AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []
417415 emptyContext S.empty M.empty emptyContext initialInteractiveOpts
418416
419417
src/Idris/Core/Evaluate.hs+3−2
@@ -14,7 +14,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
1414 rt_simplify, simplify, inlineSmall,
1515 specialise, unfold, convEq, convEq',
1616 Def(..), CaseInfo(..), CaseDefs(..),
17− Accessibility(..), Injectivity, Totality(..), PReason(..), MetaInformation(..),
17+ Accessibility(..), Injectivity, Totality(..), TTDecl, PReason(..), MetaInformation(..),
1818 Context, initContext, ctxtAlist, next_tvar,
1919 addToCtxt, setAccess, setInjective, setTotal, setRigCount,
2020 setMetaInformation, addCtxtDef, addTyDecl,
@@ -872,9 +872,10 @@ data MetaInformation =
872872-- 1 in a RigW, for example)
873873data Context = MkContext {
874874 next_tvar :: Int,
875− definitions :: Ctxt (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation)
875+ definitions :: Ctxt TTDecl
876876 } deriving (Show, Generic)
877877
878+type TTDecl = (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation)
878879
879880-- | The initial empty context
880881initContext = MkContext 0 emptyContext