Merge pull request idris-lang#3627 from joe9/master

add TT to CodegenInfo
iuliandumitru · Jan 21, 2017 · 14b5f3e · 14b5f3e
2 parents 3b95b07 + e4345f6
commit 14b5f3e
Show file tree

Hide file tree

Showing 5 changed files with 33 additions and 7 deletions.
diff --git a/src/IRTS/CodegenCommon.hs b/src/IRTS/CodegenCommon.hs
@@ -8,6 +8,7 @@ Maintainer  : The Idris Community.
 -}
 module IRTS.CodegenCommon where
 
+import Idris.Core.Evaluate
 import Idris.Core.TT
 import IRTS.Defunctionalise
 import IRTS.Simplified
@@ -39,6 +40,7 @@ data CodegenInfo = CodegenInfo {
   , liftDecls     :: [(Name, LDecl)]
   , interfaces    :: Bool
   , exportDecls   :: [ExportIFace]
+  , ttDecls       :: [(Name, TTDecl)]
   }
 
 type CodeGenerator = CodegenInfo -> IO ()
diff --git a/src/IRTS/Compiler.hs b/src/IRTS/Compiler.hs
@@ -74,6 +74,7 @@ compile codegen f mtm = do
         flags <- getFlags codegen
         hdrs <- getHdrs codegen
         impdirs <- allImportDirs
+        ttDeclarations <- getDeclarations reachableNames
         defsIn <- mkDecls reachableNames
         -- if no 'main term' given, generate interface files
         let iface = case mtm of
@@ -119,6 +120,7 @@ compile codegen f mtm = do
                                             hdrs impdirs objs libs flags
                                             NONE c (toAlist defuns)
                                             tagged iface exports
+                                            ttDeclarations
             Error e -> ierror e
   where checkMVs = do i <- getIState
                       case map fst (idris_metavars i) \\ primDefs of
@@ -164,6 +166,12 @@ mkDecls used
          decls <- mapM build ds
          return decls
 
+getDeclarations :: [Name] -> Idris ([(Name, TTDecl)])
+getDeclarations used
+    = do i <- getIState
+         let ds = filter (\(n, (d,_,_,_,_,_)) -> n `elem` used || isCon d) $ ((toAlist . definitions . tt_ctxt) i)
+         return ds
+
 showCaseTrees :: [(Name, LDecl)] -> String
 showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)
   where

diff --git a/src/IRTS/Portable.hs b/src/IRTS/Portable.hs
@@ -9,6 +9,7 @@ Maintainer  : The Idris Community.
 module IRTS.Portable (writePortable) where
 
 import Idris.Core.CaseTree
+import Idris.Core.Evaluate
 import Idris.Core.TT
 import IRTS.Bytecode
 import IRTS.CodegenCommon
@@ -29,7 +30,7 @@ data CodegenFile = CGFile {
 
 -- Update the version when the format changes
 formatVersion :: Int
-formatVersion = 2
+formatVersion = 3
 
 writePortable :: Handle -> CodegenInfo -> IO ()
 writePortable file ci = do
@@ -53,7 +54,8 @@ instance ToJSON CodegenInfo where
                         "lift-decls" .= (liftDecls ci),
                         "defun-decls" .= (defunDecls ci),
                         "simple-decls" .= (simpleDecls ci),
-                        "bytecode" .= (map toBC (simpleDecls ci))]
+                        "bytecode" .= (map toBC (simpleDecls ci)),
+                        "tt-decls" .= (ttDecls ci)]
 
 instance ToJSON Name where
     toJSON n = toJSON $ showCG n
@@ -279,3 +281,18 @@ instance ToJSON Reg where
     toJSON (T i) = object ["T" .= i]
     toJSON (L i) = object ["L" .= i]
     toJSON Tmp = object ["Tmp" .= Null]
+
+instance ToJSON RigCount where
+    toJSON r = object ["RigCount" .= show r]
+
+instance ToJSON Totality where
+    toJSON t = object ["Totality" .= show t]
+
+instance ToJSON MetaInformation where
+    toJSON m = object ["MetaInformation" .= show m]
+
+instance ToJSON Def where
+    toJSON d = object ["Def" .= show d]
+
+instance ToJSON Accessibility where
+    toJSON a = object ["Accessibility" .= show a]
diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs
@@ -292,8 +292,6 @@ data IState = IState {
   , idris_postulates             :: S.Set Name
   , idris_externs                :: S.Set (Name, Int)
   , idris_erasureUsed            :: [(Name, Int)]                  -- ^ Function/constructor name, argument position is used
-  , idris_whocalls               :: Maybe (M.Map Name [Name])
-  , idris_callswho               :: Maybe (M.Map Name [Name])
 
   -- | List of names that were defined in the repl, and can be re-/un-defined
   , idris_repl_defs              :: [Name]
@@ -413,7 +411,7 @@ idrisInit = IState initContext S.empty []
                    [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
                    [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
                    (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
-                   AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
+                   AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []
                    emptyContext S.empty M.empty emptyContext initialInteractiveOpts
 
 

diff --git a/src/Idris/Core/Evaluate.hs b/src/Idris/Core/Evaluate.hs
@@ -14,7 +14,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
                 rt_simplify, simplify, inlineSmall,
                 specialise, unfold, convEq, convEq',
                 Def(..), CaseInfo(..), CaseDefs(..),
-                Accessibility(..), Injectivity, Totality(..), PReason(..), MetaInformation(..),
+                Accessibility(..), Injectivity, Totality(..), TTDecl, PReason(..), MetaInformation(..),
                 Context, initContext, ctxtAlist, next_tvar,
                 addToCtxt, setAccess, setInjective, setTotal, setRigCount,
                 setMetaInformation, addCtxtDef, addTyDecl,
@@ -872,9 +872,10 @@ data MetaInformation =
 -- 1 in a RigW, for example)
 data Context = MkContext {
                   next_tvar       :: Int,
-                  definitions     :: Ctxt (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation)
+                  definitions     :: Ctxt TTDecl
                 } deriving (Show, Generic)
 
+type TTDecl = (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation)
 
 -- | The initial empty context
 initContext = MkContext 0 emptyContext