Store a hash of the interface in .ttc files

Calculated from exported types, public exported definitions, and
publicly imported interfaces. This saves rebuilding a module if its
imports have changed but have the same interface.

src/Core/Binary.idr

@@ -2,6 +2,7 @@ module Core.Binary
 
 import Core.Context
 import Core.Core
+import Core.Hash
 import Core.Options
 import Core.TT
 import Core.TTC
@@ -23,7 +24,7 @@ import Data.Buffer
 -- *and* the 'annot' type are the same, or there are no holes/constraints
 export
 ttcVersion : Int
-ttcVersion = 19
+ttcVersion = 20
 
 export
 checkTTCVersion : Int -> Int -> Core annot ()
@@ -37,6 +38,8 @@ checkTTCVersion ver exp
 record TTCFile annot extra where
   constructor MkTTCFile
   version : Int
+  ifaceHash : Int
+  importHashes : List (List String, Int)
   holes : List (annot, Name)
   constraints : Context (Constraint annot)
   context : Defs
@@ -48,6 +51,8 @@ record TTCFile annot extra where
   toBuf b file
       = do toBuf b "TTC"
            toBuf b (version file)
+           toBuf b (ifaceHash file)
+           toBuf b (importHashes file)
            toBuf b (holes file)
            toBuf b (constraints file)
            toBuf b (context file)
@@ -58,11 +63,14 @@ record TTCFile annot extra where
            when (hdr /= "TTC") $ corrupt "TTC header"
            ver <- fromBuf s b
            checkTTCVersion ver ttcVersion
+           ifaceHash <- fromBuf s b
+           importHashes <- fromBuf s b
            holes <- fromBuf s b
            constraints <- fromBuf s b
            defs <- fromBuf s b
            ex <- fromBuf s b
-           pure (MkTTCFile ver holes constraints defs ex)
+           pure (MkTTCFile ver ifaceHash importHashes 
+                           holes constraints defs ex)
 
 -- Update the various fields in Defs affected by the name's flags
 processFlags : Name -> List DefFlag -> Defs -> Defs
@@ -108,15 +116,16 @@ writeToTTC extradata fname
                                    cgdirectives = cgdirectives defs
                                  } initCtxt)
                          defs
-         toBuf buf (MkTTCFile ttcVersion (holes ust) (constraints ust) defs'
+         toBuf buf (MkTTCFile ttcVersion (ifaceHash defs) (importHashes defs)
+                              (holes ust) (constraints ust) defs'
                               extradata)
          Right ok <- coreLift $ writeToFile fname !(get Bin)
                | Left err => throw (InternalError (fname ++ ": " ++ show err))
          pure ()
 
 -- Add definitions from a binary file to the current context
--- Returns the "extra" section of the file (user defined data) and the list
--- of additional TTCs that need importing
+-- Returns the "extra" section of the file (user defined data), the interface
+-- has and the list of additional TTCs that need importing
 -- (we need to return these, rather than do it here, because after loading
 -- the data that's when we process the extra data...)
 export
@@ -128,7 +137,7 @@ readFromTTC : (TTC annot annot, TTC annot extra) =>
               (fname : String) -> -- file containing the module
               (modNS : List String) -> -- module namespace
               (importAs : List String) -> -- namespace to import as
-              Core annot (Maybe (extra, List (List String, Bool, List String)))
+              Core annot (Maybe (extra, Int, List (List String, Bool, List String)))
 readFromTTC loc reexp fname modNS importAs
     = do defs <- get Ctxt
          -- If it's already in the context, don't load it again
@@ -155,4 +164,53 @@ readFromTTC loc reexp fname modNS importAs
          ust <- get UST
          put UST (record { holes = holes ttc,
                            constraints = constraints ttc } ust)
-         pure (Just (extraData ttc, imported (context ttc)))
+         pure (Just (extraData ttc, ifaceHash ttc, imported (context ttc)))
+
+getImportHashes : TTC annot annot =>
+                  Ref Share (StringMap String) -> Ref Bin Binary ->
+                  Core annot (List (List String, Int))
+getImportHashes s b
+    = do hdr <- fromBuf {a = String} s b
+         when (hdr /= "TTC") $ corrupt "TTC header"
+         ver <- fromBuf {a = Int} s b
+         checkTTCVersion ver ttcVersion
+         ifaceHash <- fromBuf {a = Int} s b
+         fromBuf s b
+
+getHash : TTC annot annot =>
+          Ref Share (StringMap String) -> Ref Bin Binary ->
+          Core annot Int
+getHash s b
+    = do hdr <- fromBuf {a = String} s b
+         when (hdr /= "TTC") $ corrupt "TTC header"
+         ver <- fromBuf {a = Int} s b
+         checkTTCVersion ver ttcVersion
+         fromBuf s b
+
+export
+readIFaceHash : TTC annot annot =>
+                (fname : String) -> -- file containing the module
+                Core annot Int
+readIFaceHash fname
+    = do Right buf <- coreLift $ readFromFile fname
+            | Left err => pure 0
+         b <- newRef Bin buf
+         s <- initShare
+
+         catch (getHash s b)
+               (\err => pure 0)
+
+export
+readImportHashes : TTC annot annot =>
+                (fname : String) -> -- file containing the module
+                Core annot (List (List String, Int))
+readImportHashes fname
+    = do Right buf <- coreLift $ readFromFile fname
+            | Left err => pure []
+         b <- newRef Bin buf
+         s <- initShare
+
+         catch (getImportHashes s b)
+               (\err => pure [])
+
+

src/Core/Context.idr

@@ -3,6 +3,7 @@ module Core.Context
 import Core.CaseTree
 import Core.CompileExpr
 import public Core.Core
+import public Core.Hash
 import Core.TT
 import Core.TTC
 import Core.Options
@@ -336,6 +337,8 @@ record Defs where
       toSave : SortedSet -- Definitions to write out as .tti
       imported : List (List String, Bool, List String) 
           -- imported modules, to rexport, as namespace
+      importHashes : List (List String, Int)
+          -- interface hashes of imported modules
       allImported : List (String, List String)
           -- all imported filenames/namespaces, just to avoid loading something
           -- twice unnecessarily (this is a record of all the things we've
@@ -350,6 +353,7 @@ record Defs where
       nextTag : Int -- next tag for type constructors
       nextHole : Int -- next hole/constraint id
       nextVar	: Int
+      ifaceHash : Int
 
 export
 noGam : Defs -> Defs
@@ -362,9 +366,9 @@ noGam = record { gamma = empty }
 export
 TTC annot Defs where
   toBuf b val 
-      = do toBuf b (CMap.toList (exactNames (gamma val)))
-           toBuf b (currentNS val)
+      = do toBuf b (currentNS val)
            toBuf b (imported val)
+           toBuf b (CMap.toList (exactNames (gamma val)))
            toBuf b (laziness (options val))
            toBuf b (pairnames (options val))
            toBuf b (rewritenames (options val))
@@ -373,9 +377,9 @@ TTC annot Defs where
            toBuf b (hiddenNames val)
            toBuf b (cgdirectives val)
   fromBuf s b
-      = do ns <- fromBuf s b {a = List (Name, GlobalDef)}
-           modNS <- fromBuf s b
+      = do modNS <- fromBuf s b
            imported <- fromBuf s b
+           ns <- fromBuf s b {a = List (Name, GlobalDef)}
            lazy <- fromBuf s b
            pair <- fromBuf s b
            rw <- fromBuf s b
@@ -390,7 +394,7 @@ TTC annot Defs where
                                       primnames = prim,
                                       namedirectives = ndirs
                                     } defaults)
-                            empty imported [] [] empty [] hides ds 100 0 0)
+                            empty imported [] [] [] empty [] hides ds 100 0 0 5381)
     where
       insertFrom : List (Name, GlobalDef) -> Gamma -> Gamma
       insertFrom [] ctxt = ctxt
@@ -399,7 +403,7 @@ TTC annot Defs where
 
 export
 initCtxt : Defs
-initCtxt = MkAllDefs empty ["Main"] defaults empty [] [] [] empty [] [] [] 100 0 0
+initCtxt = MkAllDefs empty ["Main"] defaults empty [] [] [] [] empty [] [] [] 100 0 0 5381
 
 export
 getSave : Defs -> List Name
@@ -524,6 +528,19 @@ clearCtxt
     = do defs <- get Ctxt
          put Ctxt (record { options = options defs } initCtxt)
 
+export
+addHash : {auto c : Ref Ctxt Defs} ->
+          Hashable a => a -> Core annot ()
+addHash x
+    = do defs <- get Ctxt
+         put Ctxt (record { ifaceHash = hashWithSalt (ifaceHash defs) x } defs)
+
+export
+initHash : {auto c : Ref Ctxt Defs} -> Core annot ()
+initHash
+    = do defs <- get Ctxt
+         put Ctxt (record { ifaceHash = 5381 } defs)
+
 export
 isDelayType : Name -> Defs -> Bool
 isDelayType n defs

src/Core/Hash.idr

@@ -0,0 +1,88 @@
+module Core.Hash
+
+import Core.TT
+import Data.List
+
+import Debug.Trace
+
+%default total
+
+-- This is so that we can store a hash of the interface in ttc files, to avoid
+-- the need for reloading modules when no interfaces have changed in imports.
+-- As you can probably tell, I know almost nothing about writing good hash
+-- functions, so better implementations will be very welcome...
+
+public export
+interface Hashable a where
+  hash : a -> Int
+  hashWithSalt : Int -> a -> Int
+
+  hash = hashWithSalt 5381
+  hashWithSalt h i = hash i
+
+export
+Hashable Int where
+  hash = id
+
+export
+Hashable Char where
+  hash = cast
+
+export
+Hashable a => Hashable (List a) where
+  hashWithSalt h [] = abs h
+  hashWithSalt h (x :: xs) = hashWithSalt (h * 33 + hash x) xs
+
+export
+Hashable String where
+  hashWithSalt h str = hashWithSalt h (unpack str)
+
+export
+Hashable Name where
+  hashWithSalt h (MN s _) = hashWithSalt h s
+  hashWithSalt h (DN s _) = hashWithSalt h s
+  hashWithSalt h (HN s _) = hashWithSalt h s
+  hashWithSalt h n = hashWithSalt h (show n)
+
+count : RigCount -> String
+count Rig0 = "0"
+count Rig1 = "1"
+count RigW = "w"
+
+plicity : PiInfo -> String
+plicity Implicit = "{}"
+plicity Explicit = "()"
+plicity AutoImplicit = "{a}"
+
+-- I suppose this'll do for now... TODO: Write a proper one!
+-- Converting to a string (and indeed, however we do the hash function...)
+-- we need to ignore machine generated names because they'll have different
+-- numbers depending on implementations of functions, and that doesn't affect
+-- the exported interface.
+hshow : Term vars -> String
+hshow (Local {x} _ _) = nameRoot x
+hshow (Ref _ n) = nameRoot n
+hshow (Bind x (Lam c p ty) sc) 
+   = "\\" ++ nameRoot x ++ count c ++ plicity p ++ hshow ty ++ "." ++ hshow sc
+hshow (Bind x (Let c val ty) sc) 
+   = "let " ++ nameRoot x ++ count c ++ " " ++ hshow val ++ " " ++ hshow ty ++ "."
+            ++ hshow sc
+hshow (Bind x (Pi c p ty) sc) 
+   = "pi." ++ nameRoot x ++ count c ++ plicity p ++ hshow ty ++ "." ++ hshow sc
+hshow (Bind x (PVar c ty) sc)
+   = "pvar." ++ nameRoot x ++ count c ++ hshow ty ++ "." ++ hshow sc
+hshow (Bind x (PLet c val ty) sc)
+   = "plet " ++ nameRoot x ++ count c ++ " " ++ hshow val ++ " " ++ hshow ty ++ "."
+             ++ hshow sc
+hshow (Bind x (PVTy c ty) sc)
+   = "pty." ++ nameRoot x ++ count c ++ hshow ty ++ "." ++ hshow sc
+hshow (App f a) = "(" ++ hshow f ++ " " ++ hshow a ++ ")"
+hshow (PrimVal x) = show x
+hshow TType = "#"
+hshow Erased = "_"
+
+export
+Hashable (Term vars) where
+  hashWithSalt h tm 
+     = hashWithSalt h (hshow tm)
+

src/Idris/ModTree.idr

@@ -153,10 +153,10 @@ buildMod loc num len mod
         let showMod = showSep "." (reverse (buildNS mod))
 
         if needsBuilding
-           then do iputStrLn $ show num ++ "/" ++ show len ++
+           then do let msg = show num ++ "/" ++ show len ++
                                    ": Building " ++ showMod ++
                                    " (" ++ src ++ ")"
-                   [] <- process {u} {m} src
+                   [] <- process {u} {m} msg src
                       | errs => do traverse emitError errs
                                    pure errs
                    pure []