idris 0.9.15 → 0.9.15.1

raw patch · 3 files changed

+21/−10 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• idris.cabal +1/−1
• src/Idris/Elab/Clause.hs +19/−8
• src/Idris/Transforms.hs +1/−1

@@ -1,5 +1,5 @@ Name:           idris-Version:        0.9.15+Version:        0.9.15.1 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady

@@ -338,10 +338,15 @@                 -- want to be a PE version of those next)                 let cgns' = filter (\x -> x /= n &&                                           notStatic ist x) cgns+                -- set small reduction limit on partial/productive things+                let maxred = case lookupTotal n (tt_ctxt ist) of+                                  [Total _] -> 65536+                                  [Productive] -> 16+                                  _ -> 1                 let opts = [Specialise ((if pe_simple specdecl                                              then map (\x -> (x, Nothing)) cgns'                                              else []) ++-                                         (n, Just 65536) : +                                         (n, Just maxred) :                                             mapMaybe (specName (pe_simple specdecl))                                                     (snd specapp))]                 logLvl 3 $ "Specialising application: " ++ show specapp@@ -409,18 +414,24 @@     -- get the clause of a specialised application     getSpecClause ist (n, args)        = let newnm = sUN ("PE_" ++ show (nsroot n) ++ "_" ++-                               qhash 0 (showSep "_" (map showArg args))) in +                               qhash 5381 (showSep "_" (map showArg args))) in                                 -- UN (show n ++ show (map snd args)) in              (n, newnm, mkPE_TermDecl ist newnm n args)-      where showArg (ExplicitS, n) = show n-            showArg (ImplicitS, n) = show n+      where showArg (ExplicitS, n) = qshow n+            showArg (ImplicitS, n) = qshow n             showArg _ = "" -            -- TMP for readability! This is obviously a really bad hashing-            -- function.+            qshow (Bind _ _ _) = "fn"+            qshow (App f a) = qshow f ++ qshow a+            qshow (P _ n _) = show n+            qshow (Constant c) = show c+            qshow _ = ""++            -- Simple but effective string hashing...+            -- Keep it to 32 bits for readability/debuggability             qhash :: Int -> String -> String-            qhash acc [] = showHex acc ""-            qhash acc (x:xs) = qhash (fromEnum x + acc) xs+            qhash hash [] = showHex (abs hash `mod` 0xffffffff) ""+            qhash hash (x:xs) = qhash (hash * 33 + fromEnum x) xs  -- checks if the clause is a possible left hand side. Returns the term if -- possible, otherwise Nothing.

@@ -93,7 +93,7 @@            = do fm <- doMatch ns f f'                 am <- doMatch ns a a'                 return (fm ++ am)-      doMatch ns x y | x == y = return []+      doMatch ns x y | vToP x == vToP y = return []                      | otherwise = Nothing