58a12c1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Totality checker improvements (soundness)

When spotting a cycle, need to check that the decreasing argument is in the same position. For the moment, this means we can't spot decreasing arguments which change position across multiple calls - but soundness is more important!

commit58a12c1595888382ca59aa5cffff73823d55ca11 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 27 Nov 2013, 19:51 (13 years ago) parentec3daa4

9 files changed+66−23

compare with master

unifiedsplit

libs/prelude/Prelude/List.idr+3−3 src/Idris/Coverage.hs+11−8 src/Idris/ElabDecls.hs+2−3 test/reg006/run+1−1 test/reg028/expected+2 test/reg028/reg028.idr+8 test/reg028/reg028a.idr+25 test/reg028/run+4 test/test017/test017.idr+10−8

libs/prelude/Prelude/List.idr+3−3

@@ -58,10 +58,10 @@ last (x::y::ys) p = last (y::ys) refl

5858

5959last' : (l : List a) -> Maybe a

6060last' [] = Nothing

61−last' (x::xs) =

61+last' (x::xs) =

6262 case xs of

63− [] => Just x

64− y::ys => last' xs

63+ [] => Just x

64+ y :: ys => last' xs

6565

6666init : (l : List a) -> (isCons l = True) -> List a

6767init [] refl impossible

src/Idris/Coverage.hs+11−8

@@ -630,12 +630,12 @@ checkMP ist i mp = if i > 0

630630 = let res = tryPath d path mp arg in

631631 trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res

632632

633− tryPath :: Int -> [(SCGEntry, Int)] -> MultiPath -> Int -> Totality

633+ tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality

634634 tryPath desc path [] _ = Total []

635635-- tryPath desc path ((UN "believe_me", _) : _) arg

636636-- = Partial BelieveMe

637637 -- if we get to a constructor, it's fine as long as it's strictly positive

638− tryPath desc path ((f, _) :es) arg

638+ tryPath desc path ((f, _) : es) arg

639639 | [TyDecl (DCon _ _) _] <- lookupDef f (tt_ctxt ist)

640640 = case lookupTotal f (tt_ctxt ist) of

641641 [Total _] -> Unchecked -- okay so far

@@ -646,12 +646,15 @@ checkMP ist i mp = if i > 0

646646 tryPath desc path (e@(f, args) : es) arg

647647 | e `elem` es && allNothing args = Partial (Mutual [f])

648648 tryPath desc path (e@(f, nextargs) : es) arg

649− | Just d <- lookup e path

649+ | Just d <- lookup (e, arg) path

650650 = if desc > 0

651651 then -- trace ("Descent " ++ show (desc - d) ++ " "

652652 -- ++ show (path, e)) $

653653 Total []

654− else Partial (Mutual (map (fst . fst) path ++ [f]))

654+ else Partial (Mutual (map (fst . fst . fst) path ++ [f]))

655+ | e `elem` map (fst . fst) path

656+ && not (f `elem` map fst es)

657+ = Partial (Mutual (map (fst . fst . fst) path ++ [f]))

655658 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =

656659 let argspos = case collapseNothing (zip nextargs [0..]) of

657660 [] -> [(Nothing, 0)]

@@ -664,24 +667,24 @@ checkMP ist i mp = if i > 0

664667 -- rest definitely terminates without

665668 -- any cycles with route so far,

666669 -- then we might yet be total

667− case collapse (map (tryPath (-10000) ((e, 0):path) es)

670+ case collapse (map (tryPath 0 (((e, arg), 0):path) es)

668671 [0..length nextargs - 1]) of

669672 Total _ -> return Unchecked

670673 x -> return x

671674 Just (nextarg, sc) ->

672675 if nextarg == arg then

673676 case sc of

674− Same -> return $ tryPath desc ((e, desc) : path)

677+ Same -> return $ tryPath desc (((e, arg), desc) : path)

675678 es pos

676679 Smaller -> return $ tryPath (desc+1)

677− ((e, desc):path)

680+ (((e, arg), desc) : path)

678681 es

679682 pos

680683 _ -> trace ("Shouldn't happen " ++ show e) $

681684 return (Partial Itself)

682685 else return Unchecked in

683686-- trace (show (desc, argspos, path, es, pathres)) $

684− collapse' Unchecked pathres

687+ collapse' Unchecked pathres

685688

686689 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a

687690 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])

src/Idris/ElabDecls.hs+2−3

@@ -705,7 +705,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

705705 pdef pdef pdef_inl pdef' ty)

706706 addIBC (IBCDef n)

707707 setTotality n tot

708− when (not reflect) $ totcheck (fc, n)

708+ when (not reflect) $ do totcheck (fc, n)

709+ defer_totcheck (fc, n)

709710 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

710711 i <- getIState

711712 case lookupDef n (tt_ctxt i) of

@@ -1006,8 +1007,6 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

10061007 addDeferred def''

10071008

10081009 when (not (null def')) $ do

1009− -- check these at the end, when definitions are complete

1010− defer_totcheck (fc, fname)

10111010 mapM_ defer_totcheck (map (\x -> (fc, fst x)) def'')

10121011

10131012 -- Now the remaining deferred (i.e. no type declarations) clauses

test/reg006/run+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−idris $@ reg006.idr -o reg006

2+idris $@ reg006.idr --check

33rm -f *.ibc

test/reg028/expectednew file+2

@@ -0,0 +1,2 @@

1+reg028.idr:5:1:tbad.bad is possibly not total due to: {tbad.bad12}

2+reg028a.idr:11:1:tbad.qsort' is possibly not total due to: {tbad.qsort'14}

test/reg028/reg028.idrnew file+8

@@ -0,0 +1,8 @@

1+module tbad

3+total

4+bad : Nat -> Nat

5+bad Z = Z

6+bad (S m) with (succ m)

7+ bad _ | j = bad j

test/reg028/reg028a.idrnew file+25

@@ -0,0 +1,25 @@

1+module tbad

3+partial

4+qsort : Ord a => List a -> List a

5+qsort [] = []

6+qsort (x::xs) with (partition (<x) xs)

7+ qsort (x::xs) | (ys, zs) = qsort ys ++ [x] ++ qsort zs

9+total

10+qsort' : Ord a => List a -> List a

11+qsort' [] = []

12+qsort' (x::xs) with (partition (<x) xs)

13+ qsort' (x::xs) | (ys, zs) = ?qsortLemma

14+

15+---------- Proofs ----------

16+

17+qsortLemma = proof

18+ intros

19+ let ys' = qsort' ys

20+ let zs' = qsort' zs

21+ let ws = ys' ++ [x] ++ zs'

22+ trivial

23+

24+

25+

test/reg028/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ reg028.idr --check

3+idris $@ reg028a.idr --check

4+rm -f *.ibc

test/test017/test017.idr+10−8

@@ -20,14 +20,16 @@ ordElim (Suc o) P mZ mSuc mSup = mSuc o (ordElim o P mZ mSuc mSup)

2020ordElim (Sup f) P mZ mSuc mSup =

2121 mSup f (\n => ordElim (f n) P mZ mSuc mSup)

2222

23−myplus' : Nat -> Nat -> Nat

24−myplus : Nat -> Nat -> Nat

25−

26−myplus Z y = y

27−myplus (S k) y = S (myplus' k y)

28−

29−myplus' Z y = y

30−myplus' (S k) y = S (myplus y k)

23+-- For now, not going to support this

24+

25+-- myplus' : Nat -> Nat -> Nat

26+-- myplus : Nat -> Nat -> Nat

27+--

28+-- myplus Z y = y

29+-- myplus (S k) y = S (myplus' k y)

30+--

31+-- myplus' Z y = y

32+-- myplus' (S k) y = S (myplus y k)

3133

3234mnubBy : (a -> a -> Bool) -> List a -> List a

3335mnubBy = nubBy' []