compiler: stable names generation (#322)

[skip lemma]

cogent/Main.hs

@@ -81,6 +81,7 @@ import Control.Monad.Trans.Except (runExceptT)
 -- import Control.Monad.Cont
 -- import Control.Monad.Except (runExceptT)
 -- import Control.Monad.Trans.Either (eitherT, runEitherT)
+import Data.Binary (encodeFile, decodeFileOrFail)
 import Data.Char (isSpace)
 import Data.Either (isLeft, fromLeft)
 import Data.Foldable (fold, foldrM)
@@ -452,6 +453,7 @@ flags =
   , Option []         ["ext-types"]      1 (ReqArg set_flag_extTypes "FILE")               "give external type names to C parser"
   , Option []         ["infer-c-funcs"]  1 (ReqArg (set_flag_inferCFunc . words) "FILE..") "infer Cogent abstract function definitions"
   , Option []         ["infer-c-types"]  1 (ReqArg (set_flag_inferCType . words) "FILE..") "infer Cogent abstract type definitions"
+  , Option []         ["name-cache"]     1 (ReqArg set_flag_nameCache "FILE")              "specify the name cache file to use"
   , Option []         ["proof-input-c"]  1 (ReqArg set_flag_proofInputC "FILE")            "specify input C file to generate proofs (default to the same base name as input Cogent file)"
   , Option []         ["prune-call-graph"] 2 (ReqArg set_flag_pruneCallGraph "FILE")       "specify Cogent entry-point definitions"
   -- external programs
@@ -792,7 +794,16 @@ parseArgs args = case getOpt' Permute options args of
           hscName = mkOutputName' toHsModName source (Just __cogent_suffix_of_ffi_types)
           hsName  = mkOutputName' toHsModName source (Just __cogent_suffix_of_ffi)
           cNames  = map (\n -> takeBaseName n ++ __cogent_suffix_of_pp ++ __cogent_suffix_of_inferred <.> __cogent_ext_of_c) __cogent_infer_c_func_files
-          (h,c,atm,ct,hsc,hs,genst) = cgen hName cNames hscName hsName monoed ctygen log
+          cacheFile = __cogent_name_cache
+      cacheExists <- doesFileExist __cogent_name_cache
+      if cacheExists then putProgressLn ("Using existing name cache file: " ++ __cogent_name_cache)
+                     else putProgressLn ("No name cache file found: " ++ __cogent_name_cache)
+      mcache <- if cacheExists then do decodeResult <- decodeFileOrFail __cogent_name_cache
+                                       case decodeResult of
+                                         Left (_, err) -> hPutStrLn stderr ("Decoding name cache file failed: " ++ err) >> exitFailure
+                                         Right cache -> return $ Just cache
+                               else return Nothing
+      let (h,c,atm,ct,hsc,hs,genst) = cgen hName cNames hscName hsName monoed mcache ctygen log
       when (TableAbsTypeMono `elem` cmds) $ do
         let atmfile = mkFileName source Nothing __cogent_ext_of_atm
         putProgressLn "Generating table for monomorphised asbtract types..."
@@ -824,6 +835,8 @@ parseArgs args = case getOpt' Permute options args of
         output cf $ flip M.hPutDoc (ppr c </> M.line)       -- .c file gen
         unless (null $ __cogent_infer_c_func_files ++ __cogent_infer_c_type_files) $
           glue cmds tced tcst typedefs fts insts genst buildinfo log
+        putProgressLn ("Writing name cache file: " ++ __cogent_name_cache)
+        encodeFile __cogent_name_cache genst
 
     c_refinement source monoed insts log (False,False,False) = return ()
     c_refinement source monoed insts log (ac,cs,cp) = do

cogent/cogent.cabal

@@ -139,6 +139,7 @@ library
   build-depends:
                 ansi-wl-pprint >= 0.6
               , base >= 4.10
+              , binary
               , bytestring >= 0.10 
               , containers >= 0.5.8
               , cpphs >= 1.19
@@ -208,6 +209,7 @@ Executable cogent
               , ansi-wl-pprint >= 0.6
               , atomic-write >= 0.2.0.4
               , base >= 4.10
+              , binary
               , containers >= 0.5
               , directory >=1.2
               , filepath >= 1.4.0.0

cogent/src/Cogent/C/Compile.hs

@@ -13,6 +13,7 @@
 {- LANGUAGE AllowAmbiguousTypes -}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -50,6 +51,7 @@ import           Cogent.Isabelle.Deep
 import           Cogent.Mono                  (Instance)
 import           Cogent.Normal                (isAtom)
 import           Cogent.Util           (decap, extTup2l, extTup3r, first3, secondM, toCName, whenM, flip3)
+import           Data.Binary
 import qualified Data.DList          as DList
 import           Data.Nat            as Nat
 import           Data.Vec            as Vec hiding (repeat, zipWith)
@@ -73,6 +75,7 @@ import qualified Data.Set            as S
 import           Data.String
 import           Data.Traversable             (mapM)
 import           Data.Tuple                   (swap)
+import           GHC.Generics                 (Generic)
 #if __GLASGOW_HASKELL__ < 709
 import           Prelude             as P    hiding (mapM, mapM_)
 #else
@@ -110,7 +113,9 @@ data GenState  = GenState { _cTypeDefs    :: [(StrlType, CId)]
                             -- ^ A map containing functions that need to generate C FFI functions. 
                             --   The map is from the original function names (before prefixing with @\"ffi_\"@ to a pair of @(marshallable_arg_type, marshallable_ret_type)@.
                             --   This map is needed when we generate the Haskell side of the FFI.
-                          }
+                          } deriving (Generic)
+
+instance Binary GenState
 
 makeLenses ''GenState
 
@@ -1124,6 +1129,7 @@ genDefinition _ = return []
 -- * top-level function
 
 compile :: [Definition TypedExpr VarName]
+        -> Maybe GenState      -- cached state
         -> [(Type 'Zero, String)]
         -> ( [CExtDecl]  -- enum definitions
            , [CExtDecl]  -- type definitions
@@ -1136,22 +1142,25 @@ compile :: [Definition TypedExpr VarName]
            , [TypeName]
            , GenState
            )
-compile defs ctygen =
+compile defs mcache ctygen =
   let (tdefs, fdefs) = L.partition isTypeDef defs
+      state = case mcache of
+                Nothing -> GenState { _cTypeDefs    = []
+                                    , _cTypeDefMap  = M.empty
+                                    , _typeSynonyms = M.empty
+                                    , _typeCorres   = DList.empty
+                                    , _absTypes     = M.empty
+                                    , _custTypeGen  = M.fromList $ P.map (second $ (,CTGI)) ctygen
+                                    , _funClasses   = M.empty
+                                    , _localOracle  = 0
+                                    , _globalOracle = 0
+                                    , _varPool      = M.empty
+                                    , _ffiFuncs     = M.empty
+                                    }
+                Just cache -> cache & custTypeGen <>~ (M.fromList $ P.map (second $ (,CTGI)) ctygen)
       (extDecls, st, ()) = runRWS (runGen $
         concat <$> mapM genDefinition (fdefs ++ tdefs)  -- `fdefs' will collect the types that are used in the program, and `tdefs' can generate synonyms
-        ) Nil (GenState { _cTypeDefs    = []
-                        , _cTypeDefMap  = M.empty
-                        , _typeSynonyms = M.empty
-                        , _typeCorres   = DList.empty
-                        , _absTypes     = M.empty
-                        , _custTypeGen  = M.fromList $ P.map (second $ (,CTGI)) ctygen
-                        , _funClasses   = M.empty
-                        , _localOracle  = 0
-                        , _globalOracle = 0
-                        , _varPool      = M.empty
-                        , _ffiFuncs     = M.empty
-                        })
+        ) Nil state
       (enum, st', _) = runRWS (runGen $ (mappend <$> genLetTrueEnum <*> genEnum)) Nil st  -- `LET_TRUE', `LETBANG_TRUE' & `_tag' enums
       ((funclasses,tns), st'', _) = runRWS (runGen genFunClasses) Nil st'  -- fun_enums & dispatch functions
       (dispfs, fenums) = L.partition isFnDefn funclasses where isFnDefn (CFnDefn {}) = True; isFnDefn _ = False

cogent/src/Cogent/C/Syntax.hs

@@ -10,6 +10,7 @@
 -- @TAG(DATA61_GPL)
 --
 
+{-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PackageImports #-}
 {-# LANGUAGE StandaloneDeriving #-}
@@ -27,18 +28,24 @@ module Cogent.C.Syntax (
 import Cogent.Common.Syntax
 import Cogent.Common.Types
 
+import Data.Binary (Binary)
 import Data.Map as M
+import GHC.Generics (Generic)
 import qualified "language-c-quote" Language.C as C
 
 type CId = String
 
 data CIntType = CCharT | CShortT | CIntT | CLongT | CLongLongT
-              deriving (Eq, Ord, Show)
+              deriving (Eq, Ord, Show, Generic)
+
+instance Binary CIntType
 
 data CArraySize = CArraySize CExpr
                 | CNoArraySize
                 | CPtrToArray
-                deriving (Eq, Ord, Show)
+                deriving (Eq, Ord, Show, Generic)
+
+instance Binary CArraySize
 
 -- The type parameter has been striped off
 data CType = CInt Bool CIntType      -- ^ 'True' is signed
@@ -54,15 +61,21 @@ data CType = CInt Bool CIntType      -- ^ 'True' is signed
            | CIdent CId
            | CFunction CType CType
            | CVoid
-           deriving (Eq, Ord, Show)
+           deriving (Eq, Ord, Show, Generic)
+
+instance Binary CType
 
 data Radix = BIN | OCT | DEC | HEX
-              deriving (Eq, Ord, Show)
+              deriving (Eq, Ord, Show, Generic)
+
+instance Binary Radix
 
 data CLitConst = CNumConst Integer CType Radix
                | CCharConst Char
                | CStringConst String
-               deriving (Eq, Ord, Show)
+               deriving (Eq, Ord, Show, Generic)
+
+instance Binary CLitConst
 
 data CExpr = CBinOp CBinOp CExpr CExpr
            | CUnOp  CUnOp CExpr
@@ -80,21 +93,33 @@ data CExpr = CBinOp CBinOp CExpr CExpr
            | CCompLit CType [([CDesignator], CInitializer)]
            -- \ | CArbitrary (CType CExpr)
            | CMKBOOL CExpr
-           deriving (Eq, Ord, Show)
+           deriving (Eq, Ord, Show, Generic)
 
+instance Binary CExpr
 
 data CInitializer = CInitE CExpr
                   | CInitList [([CDesignator], CInitializer)]
-                  deriving (Eq, Ord, Show)
+                  deriving (Eq, Ord, Show, Generic)
 
+instance Binary CInitializer
 
 data CDesignator = CDesignE CExpr
                  | CDesignFld CId
-                 deriving (Eq, Ord, Show)
+                 deriving (Eq, Ord, Show, Generic)
+
+instance Binary CDesignator
 
 type CBinOp    = C.BinOp
 type CUnOp     = C.UnOp
 
+-- Orphans
+
+deriving instance Generic C.BinOp
+deriving instance Generic C.UnOp
+
+instance Binary C.BinOp
+instance Binary C.UnOp
+
 -- data CTrappable = CBreakT | CContinueT
 
 data CStmt = CAssign CExpr CExpr
@@ -164,5 +189,7 @@ data StrlType = Record  [(CId, CType)] Bool  -- ^ @(fieldname ↦ fieldtype
               | Function CType CType
               | AbsType CId
               | Array CType (Maybe Int)
-              deriving (Eq, Ord, Show)
+              deriving (Eq, Ord, Show, Generic)
+
+instance Binary StrlType
 

cogent/src/Cogent/CodeGen.hs

@@ -39,11 +39,12 @@ cgen :: FilePath
      -> FilePath
      -> FilePath
      -> [Definition TypedExpr VarName]
+     -> Maybe GenState
      -> [(Type 'Zero, String)]
      -> String
      -> ([C.Definition], [C.Definition], [(TypeName, S.Set [CId])], [TableCTypes], Leijen.Doc, String, GenState)
-cgen hName cNames hscName hsName defs ctygen log =
-  let (enums,tydefns,fndecls,disps,tysyms,fndefns,absts,corres,fclsts,st) = compile defs ctygen
+cgen hName cNames hscName hsName defs mcache ctygen log =
+  let (enums,tydefns,fndecls,disps,tysyms,fndefns,absts,corres,fclsts,st) = compile defs mcache ctygen
       (h,c) = render hName (enums++tydefns++fndecls++disps++tysyms) fndefns log
 #ifdef WITH_HASKELL
       hsc = ffiHsc hscName cNames tydefns enums absts fclsts log

cogent/src/Cogent/Common/Repr.hs

@@ -10,17 +10,22 @@
 -- @TAG(DATA61_GPL)
 --
 
+{-# LANGUAGE DeriveGeneric #-}
 module Cogent.Common.Repr where
 
 import Cogent.Common.Syntax
 -- import qualified Cogent.Surface as S
 
+import Data.Binary (Binary)
 import qualified Data.Map as M
+import GHC.Generics (Generic)
 
 data Representation = Bits { allocSize :: Int, allocOffset :: Int } -- in bits 
                     | Variant { tagSize :: Int, tagOffset :: Int, alternatives :: M.Map TagName (Integer, Representation) }
                     | Record { fields :: M.Map FieldName Representation }
-                    deriving (Show, Eq, Ord)
+                    deriving (Show, Eq, Ord, Generic)
+
+instance Binary Representation
 
 -- Once we have repr in the surface lang, this can be removed.
 dummyRepr = Bits 0 0

cogent/src/Cogent/Common/Syntax.hs

@@ -1,16 +1,19 @@
 -- @LICENSE(NICTA_CORE)
 
 {-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveGeneric #-}
 
 module Cogent.Common.Syntax where
 
 import Cogent.Compiler
 
+import Data.Binary (Binary)
 import Data.Data hiding (Prefix)
 #if __GLASGOW_HASKELL__ < 709
 import Data.Monoid
 #endif
 import Data.Word
+import GHC.Generics (Generic)
 import Text.PrettyPrint.ANSI.Leijen
 
 type RepName     = String
@@ -147,7 +150,9 @@ tagFail    = "Fail"    :: TagName
 -- ----------------------------------------------------------------------------
 -- custTyGen
 
-data CustTyGenInfo = CTGI  deriving (Show) -- TODO: info like field mapping, etc.
+data CustTyGenInfo = CTGI  deriving (Show, Generic) -- TODO: info like field mapping, etc.
+
+instance Binary CustTyGenInfo
 
 -- ex1 :: M.Map (Type 'Zero) (String, CustTypeGenInfo)
 -- ex1 = M.singleton (TRecord [("f1", (TCon "A" [] Unboxed, False)), 

cogent/src/Cogent/Common/Types.hs

@@ -13,21 +13,26 @@
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveGeneric #-}
 
 module Cogent.Common.Types where
 
 import Cogent.Common.Syntax
+import Data.Binary (Binary)
 import Data.Data
 #if __GLASGOW_HASKELL__ < 709
 import Data.Monoid
 #endif
+import GHC.Generics (Generic)
 import Text.PrettyPrint.ANSI.Leijen hiding (tupled,indent)
 
 type ReadOnly = Bool  -- True for r/o
 
 data Sigil r = Boxed ReadOnly r  -- 0- or 1-kinded
              | Unboxed  -- 2-kinded
-             deriving (Show, Data, Eq, Ord, Functor)
+             deriving (Show, Data, Eq, Ord, Functor, Generic)
+
+instance Binary r => Binary (Sigil r)
 
 bangSigil :: Sigil r -> Sigil r
 bangSigil (Boxed _ r)  = Boxed True r
@@ -48,7 +53,9 @@ unboxed :: Sigil r -> Bool
 unboxed Unboxed = True
 unboxed _ = False
 
-data PrimInt = U8 | U16 | U32 | U64 | Boolean deriving (Show, Data, Eq, Ord)
+data PrimInt = U8 | U16 | U32 | U64 | Boolean deriving (Show, Data, Eq, Ord, Generic)
+
+instance Binary PrimInt
 
 isSubtypePrim :: PrimInt -> PrimInt -> Bool
 isSubtypePrim U8  U8  = True

cogent/src/Cogent/Compiler.hs

@@ -182,6 +182,7 @@ set_flag_fwrapPutInLet = writeIORef __cogent_fwrap_put_in_let_ref True
 set_flag_inferCFunc = writeIORef __cogent_infer_c_func_files_ref
 set_flag_inferCType = writeIORef __cogent_infer_c_type_files_ref
 set_flag_interactive = writeIORef __cogent_interactive_ref True
+set_flag_nameCache = writeIORef __cogent_name_cache_ref
 set_flag_O Nothing = return ()
 set_flag_O (Just n :: Maybe String)
   | n == "0" = do set_flag_fnormalisation Nothing
@@ -660,6 +661,13 @@ __cogent_interactive_ref :: IORef Bool
 {-# NOINLINE __cogent_interactive_ref #-}
 __cogent_interactive_ref = unsafePerformIO $ newIORef False
 
+__cogent_name_cache :: FilePath
+__cogent_name_cache = unsafePerformIO $ readIORef __cogent_name_cache_ref
+
+__cogent_name_cache_ref :: IORef FilePath
+{-# NOINLINE __cogent_name_cache_ref #-}
+__cogent_name_cache_ref = unsafePerformIO $ newIORef ".name-cache"
+
 __cogent_output_name :: Maybe String
 __cogent_output_name = unsafePerformIO $ readIORef __cogent_output_name_ref