Skip to content

Commit

Permalink
Slightly better hashing function for interfaces
Browse files Browse the repository at this point in the history
The previous one would have given the same result if swapping a name and
a type... oops!
  • Loading branch information
edwinb committed Oct 24, 2018
1 parent ed80b7d commit 8362faa
Show file tree
Hide file tree
Showing 3 changed files with 15 additions and 7 deletions.
7 changes: 7 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,10 @@
# New in next version

## Tool updates
+ Modules no longer require building if imports have changed but all
interfaces (i.e. types for names declared `export` and definitions of names
declared `public export`) are unchanged.

# New in 1.3.1

## Tool updates
Expand Down
11 changes: 6 additions & 5 deletions src/Idris/IBC.hs
Original file line number Diff line number Diff line change
Expand Up @@ -257,19 +257,20 @@ qhash :: Int -> String -> Int
qhash hash [] = abs hash `mod` 0xffffffff
qhash hash (x:xs) = qhash (hash * 33 + fromIntegral (fromEnum x)) xs

hashTerm :: Term -> Int
hashTerm t = qhash 5381 (show t)
hashTerm :: Int -> Term -> Int
hashTerm i t = qhash (i * 5381) (show t)

hashName :: Name -> Int
hashName n = qhash 5381 (show n)
hashName :: Int -> Name -> Int
hashName i n = qhash (i * 5381) (show n)

calculateHash :: IState -> IBCFile -> Int
calculateHash ist f
= let acc = L.filter exported (ibc_access f) in
mkHashFrom (map fst acc) (getDefs acc)
where
mkHashFrom :: [Name] -> [Term] -> Int
mkHashFrom ns tms = sum (map hashName ns) + sum (map hashTerm tms)
mkHashFrom ns tms = sum (L.zipWith hashName [1..] ns) +
sum (L.zipWith hashTerm [1..] tms)

exported (_, Public) = True
exported (_, Frozen) = True
Expand Down
4 changes: 2 additions & 2 deletions src/Idris/Parser.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1683,8 +1683,9 @@ loadSource lidr f toline
(sort impHashes /= sort (mapMaybe id newHashes))

if not needLoad
then iReport 1 $ "Loading " ++ f
then pure ()
else do
iReport 1 $ "Type checking " ++ f
mapM_ (\ (re, f, ns, nfc) ->
do fp <- findImport ids ibcsd f
case fp of
Expand Down Expand Up @@ -1765,7 +1766,6 @@ loadSource lidr f toline
logLvl 10 (show (toAlist (idris_implicits i)))
logLvl 3 (show (idris_infixes i))
-- Now add all the declarations to the context
iReport 1 $ "Type checking " ++ f
-- we totality check after every Mutual block, so if
-- anything is a single definition, wrap it in a
-- mutual block on its own
Expand Down

0 comments on commit 8362faa

Please sign in to comment.