git.iko.soy/Idris-dev
on master help sign in
Slightly better hashing function for interfaces

The previous one would have given the same result if swapping a name and a type... oops!

commit8362faae469ebfed492635bf2219035e04b14932 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 23 Oct 2018, 22:00 (8 years ago) parented80b7d
3 files changed+15−7
compare with master
unifiedsplit
CHANGELOG.md+7 src/Idris/IBC.hs+6−5 src/Idris/Parser.hs+2−2
CHANGELOG.md+7
@@ -1,3 +1,10 @@
1+# New in next version
2+
3+## Tool updates
4++ Modules no longer require building if imports have changed but all
5+ interfaces (i.e. types for names declared `export` and definitions of names
6+ declared `public export`) are unchanged.
7+
18# New in 1.3.1
29
310## Tool updates
src/Idris/IBC.hs+6−5
@@ -257,11 +257,11 @@ qhash :: Int -> String -> Int
257257qhash hash [] = abs hash `mod` 0xffffffff
258258qhash hash (x:xs) = qhash (hash * 33 + fromIntegral (fromEnum x)) xs
259259
260−hashTerm :: Term -> Int
261−hashTerm t = qhash 5381 (show t)
260+hashTerm :: Int -> Term -> Int
261+hashTerm i t = qhash (i * 5381) (show t)
262262
263−hashName :: Name -> Int
264−hashName n = qhash 5381 (show n)
263+hashName :: Int -> Name -> Int
264+hashName i n = qhash (i * 5381) (show n)
265265
266266calculateHash :: IState -> IBCFile -> Int
267267calculateHash ist f
@@ -269,7 +269,8 @@ calculateHash ist f
269269 mkHashFrom (map fst acc) (getDefs acc)
270270 where
271271 mkHashFrom :: [Name] -> [Term] -> Int
272− mkHashFrom ns tms = sum (map hashName ns) + sum (map hashTerm tms)
272+ mkHashFrom ns tms = sum (L.zipWith hashName [1..] ns) +
273+ sum (L.zipWith hashTerm [1..] tms)
273274
274275 exported (_, Public) = True
275276 exported (_, Frozen) = True
src/Idris/Parser.hs+2−2
@@ -1683,8 +1683,9 @@ loadSource lidr f toline
16831683 (sort impHashes /= sort (mapMaybe id newHashes))
16841684
16851685 if not needLoad
1686− then iReport 1 $ "Loading " ++ f
1686+ then pure ()
16871687 else do
1688+ iReport 1 $ "Type checking " ++ f
16881689 mapM_ (\ (re, f, ns, nfc) ->
16891690 do fp <- findImport ids ibcsd f
16901691 case fp of
@@ -1765,7 +1766,6 @@ loadSource lidr f toline
17651766 logLvl 10 (show (toAlist (idris_implicits i)))
17661767 logLvl 3 (show (idris_infixes i))
17671768 -- Now add all the declarations to the context
1768− iReport 1 $ "Type checking " ++ f
17691769 -- we totality check after every Mutual block, so if
17701770 -- anything is a single definition, wrap it in a
17711771 -- mutual block on its own