git.iko.soy/Idris-dev
on master help sign in
Fix traversal of size change graphs
906862aEdwin Brady
lib/Prelude/Heap.idr+2
compare with master
unifiedsplit
@@ -66,6 +66,7 @@ orderBySize left centre right =
66 largest : Nat
66 largest : Nat
67 largest = maximum (size left) $ maximum (size centre) (size right)
67 largest = maximum (size left) $ maximum (size centre) (size right)
68
68
69+%assert_total -- relies on orderBySize doing the right thing
69merge : Ord a => MaxiphobicHeap a -> MaxiphobicHeap a -> MaxiphobicHeap a
70merge : Ord a => MaxiphobicHeap a -> MaxiphobicHeap a -> MaxiphobicHeap a
70merge Empty right = right
71merge Empty right = right
71merge left Empty = left
72merge left Empty = left
@@ -103,6 +104,7 @@ toList : Ord a => MaxiphobicHeap a -> List a
103toList Empty = []
104toList Empty = []
104toList (Node s l e r) = toList' (Node s l e r) refl
105toList (Node s l e r) = toList' (Node s l e r) refl
105 where
106 where
107+ %assert_total -- relies on deleteMinimum making heap smaller
106 toList' : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> List a
108 toList' : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> List a
107 toList' heap p = findMinimum heap p :: (toList $ deleteMinimum heap p)
109 toList' heap p = findMinimum heap p :: (toList $ deleteMinimum heap p)
108
110
src/Idris/Coverage.hs+37−24
@@ -535,13 +535,17 @@ mkMultiPaths ist path cg
535-- If any route along the multipath leads to infinite descent, we're fine.
535-- If any route along the multipath leads to infinite descent, we're fine.
536-- Try a route beginning with every argument.
536-- Try a route beginning with every argument.
537-- If we reach a point we've been to before, but with a smaller value,
537-- If we reach a point we've been to before, but with a smaller value,
538−-- that means there is an infinitely descending path.
538+-- that means there is an infinitely descending path from that argument.
539
539
540checkMP :: IState -> Int -> MultiPath -> Totality
540checkMP :: IState -> Int -> MultiPath -> Totality
541checkMP ist i mp = if i > 0
541checkMP ist i mp = if i > 0
542 then collapse (map (tryPath 0 [] mp) [0..i-1])
542 then collapse (map (tryPath 0 [] mp) [0..i-1])
543 else tryPath 0 [] mp 0
543 else tryPath 0 [] mp 0
544 where
544 where
545+ tryPath' d path mp arg
546+ = let res = tryPath d path mp arg in
547+ trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res
548+
545 tryPath :: Int -> [(SCGEntry, Int)] -> MultiPath -> Int -> Totality
549 tryPath :: Int -> [(SCGEntry, Int)] -> MultiPath -> Int -> Totality
546 tryPath desc path [] _ = Total []
550 tryPath desc path [] _ = Total []
547-- tryPath desc path ((UN "believe_me", _) : _) arg
551-- tryPath desc path ((UN "believe_me", _) : _) arg
@@ -550,7 +554,7 @@ checkMP ist i mp = if i > 0
550 tryPath desc path ((f, _) :es) arg
554 tryPath desc path ((f, _) :es) arg
551 | [TyDecl (DCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)
555 | [TyDecl (DCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)
552 = case lookupTotal f (tt_ctxt ist) of
556 = case lookupTotal f (tt_ctxt ist) of
553− [Total _] -> Total []
557+ [Total _] -> Unchecked -- okay so far
554 [Partial _] -> Partial (Other [f])
558 [Partial _] -> Partial (Other [f])
555 x -> error (show x)
559 x -> error (show x)
556 | [TyDecl (TCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)
560 | [TyDecl (TCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)
@@ -561,39 +565,48 @@ checkMP ist i mp = if i > 0
561 tryPath desc path (e@(f, nextargs) : es) arg
565 tryPath desc path (e@(f, nextargs) : es) arg
562 | Just d <- lookup e path
566 | Just d <- lookup e path
563 = if (desc - d) > 0
567 = if (desc - d) > 0
568+ then -- trace ("Descent " ++ show (desc - d) ++ " "
569+ -- ++ show (path, e)) $
564− then Total []
570+ Total []
565 else Partial (Mutual (map (fst . fst) path ++ [f]))
571 else Partial (Mutual (map (fst . fst) path ++ [f]))
566 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
572 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
567 let argspos = zip nextargs [0..] in
573 let argspos = zip nextargs [0..] in
568− collapse' (Partial (Mutual (map (fst . fst) path ++ [f]))) $
574+ collapse' Unchecked $
569− do (arg, pos) <- argspos
575+ do (a, pos) <- argspos
570− case arg of
576+ case a of
571− Nothing -> -- don't know, but it's okay if the
577+ Nothing -> -- don't know, but if the
572 -- rest definitely terminates without
578 -- rest definitely terminates without
573− -- any cycles with route so far
579+ -- any cycles with route so far,
580+ -- then we might yet be total
574− map (tryPath (-10000) ((e, desc):path) es)
581+ case collapse (map (tryPath (-10000) ((e, desc):path) es)
575− [0..length nextargs - 1]
582+ [0..length nextargs - 1]) of
583+ Total _ -> return Unchecked
584+ x -> return x
576 Just (nextarg, sc) ->
585 Just (nextarg, sc) ->
586+ if nextarg == arg then
577− case sc of
587+ case sc of
578− Same -> return $ tryPath desc ((e, desc):path)
588+ Same -> return $ tryPath desc ((e, desc):path)
579− es
589+ es
580− nextarg
590+ pos
581− Smaller -> return $ tryPath (desc+1)
591+ Smaller -> return $ tryPath (desc+1)
582− ((e, desc):path)
592+ ((e, desc):path)
583− es
593+ es
584− nextarg
594+ pos
585− _ -> trace ("Shouldn't happen " ++ show e) $
595+ _ -> trace ("Shouldn't happen " ++ show e) $
586− return (Partial Itself)
596+ return (Partial Itself)
597+ else return Unchecked
587− | [Total _] <- lookupTotal f (tt_ctxt ist) = Total []
598+ | [Total _] <- lookupTotal f (tt_ctxt ist) = Unchecked
588 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
599 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
589− | otherwise = Total []
600+ | otherwise = Unchecked
590
601
591noPartial (Partial p : xs) = Partial p
602noPartial (Partial p : xs) = Partial p
592noPartial (_ : xs) = noPartial xs
603noPartial (_ : xs) = noPartial xs
593noPartial [] = Total []
604noPartial [] = Total []
594
605
595−collapse xs = collapse' (Partial Itself) xs
606+collapse xs = collapse' Unchecked xs
596−collapse' def (Total r : xs) = Total r
607+collapse' def (Total r : xs) = Total r
608+collapse' def (Unchecked : xs) = collapse' def xs
597collapse' def (d : xs) = collapse' d xs
609collapse' def (d : xs) = collapse' d xs
610+collapse' Unchecked [] = Total []
598collapse' def [] = def
611collapse' def [] = def
599
612
src/Idris/IBC.hs+1−1
@@ -21,7 +21,7 @@ import System.Directory
21import Paths_idris
21import Paths_idris
22
22
23ibcVersion :: Word8
23ibcVersion :: Word8
24−ibcVersion = 23
24+ibcVersion = 24
25
25
26data IBCFile = IBCFile { ver :: Word8,
26data IBCFile = IBCFile { ver :: Word8,
27 sourcefile :: FilePath,
27 sourcefile :: FilePath,
test/reg006/expectednew file+1
@@ -0,0 +1 @@
1+reg006.idr:17:RBTree.lookup is possibly not total due to: RBTree.lookup_case
test/reg006/reg006.idrnew file+27
@@ -0,0 +1,27 @@
1+module RBTree
2+
3+data Colour = Red | Black
4+
5+data RBTree : Type -> Type -> Nat -> Colour -> Type where
6+ Leaf : RBTree k v O Black
7+ RedBranch : k -> v -> RBTree k v n Black -> RBTree k v n Black -> RBTree k v n Red
8+ BlackBranch : k -> v -> RBTree k v n x -> RBTree k v n y -> RBTree k v (S n) Black
9+
10+toBlack : RBTree k v n c -> (m ** (RBTree k v m Black, Either (m = n) (m = (S n))))
11+toBlack (RedBranch k v l r) = (_ ** (BlackBranch k v l r, Right refl))
12+toBlack Leaf = (_ ** (Leaf, Left refl))
13+toBlack (BlackBranch k v l r) = (_ ** (BlackBranch k v l r, Left refl))
14+
15+total
16+lookup : Ord k => k -> RBTree k v n Black -> Maybe v
17+lookup k Leaf = Nothing
18+lookup k (BlackBranch k0 v0 l r) =
19+ case compare k k0 of
20+ EQ => Just v0
21+ LT =>
22+ let (_ ** (t, _)) = toBlack l in
23+ lookup k t
24+ GT =>
25+ let (_ ** (t, _)) = toBlack r in
26+ lookup k t
27+
test/reg006/runnew file+2
@@ -0,0 +1,2 @@
1+#!/bin/bash
2+idris $@ reg006.idr -o reg006