8362faa · Idris-dev · git.iko.soy

CHANGELOG.md+7

compare with master

unifiedsplit

@@ -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+

1# New in 1.3.1

8# New in 1.3.1

2

9

3## Tool updates

10## Tool updates

src/Idris/IBC.hs+6−5

@@ -257,11 +257,11 @@ qhash :: Int -> String -> Int

257qhash hash [] = abs hash `mod` 0xffffffff

258qhash hash (x:xs) = qhash (hash * 33 + fromIntegral (fromEnum x)) xs

259

260−hashTerm :: Term -> Int

260+hashTerm :: Int -> Term -> Int

261−hashTerm t = qhash 5381 (show t)

261+hashTerm i t = qhash (i * 5381) (show t)

262

263−hashName :: Name -> Int

263+hashName :: Int -> Name -> Int

264−hashName n = qhash 5381 (show n)

264+hashName i n = qhash (i * 5381) (show n)

265

266calculateHash :: IState -> IBCFile -> Int

267calculateHash ist f

@@ -269,7 +269,8 @@ calculateHash ist f

269 mkHashFrom (map fst acc) (getDefs acc)

270 where

271 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)

273

274

274 exported (_, Public) = True

275 exported (_, Public) = True

275 exported (_, Frozen) = True

276 exported (_, Frozen) = True

src/Idris/Parser.hs+2−2

@@ -1683,8 +1683,9 @@ loadSource lidr f toline

1683 (sort impHashes /= sort (mapMaybe id newHashes))

1684

1685 if not needLoad

1686− then iReport 1 $ "Loading " ++ f

1686+ then pure ()

1687 else do

1688+ iReport 1 $ "Type checking " ++ f

1688 mapM_ (\ (re, f, ns, nfc) ->

1689 mapM_ (\ (re, f, ns, nfc) ->

1689 do fp <- findImport ids ibcsd f

1690 do fp <- findImport ids ibcsd f

1690 case fp of

1691 case fp of

@@ -1765,7 +1766,6 @@ loadSource lidr f toline

1765 logLvl 10 (show (toAlist (idris_implicits i)))

1766 logLvl 10 (show (toAlist (idris_implicits i)))

1766 logLvl 3 (show (idris_infixes i))

1767 logLvl 3 (show (idris_infixes i))

1767 -- Now add all the declarations to the context

1768 -- Now add all the declarations to the context

1768− iReport 1 $ "Type checking " ++ f

1769 -- we totality check after every Mutual block, so if

1770 -- anything is a single definition, wrap it in a

1771 -- mutual block on its own