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

git.iko.soy/Idris-dev

on master help sign in

Totality checker improvements (soundness)

58a12c1Edwin Brady13 years ago

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

compare with master

unifiedsplit

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

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

60last' [] = Nothing

61−last' (x::xs) =

61+last' (x::xs) =

62 case xs of

63− [] => Just x

63+ [] => Just x

64− y::ys => last' xs

64+ y :: ys => last' xs

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

67init [] refl impossible

src/Idris/Coverage.hs+11−8

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

630 = let res = tryPath d path mp arg in

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

632

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

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

634 tryPath desc path [] _ = Total []

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

636-- = Partial BelieveMe

637 -- 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

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

640 = case lookupTotal f (tt_ctxt ist) of

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

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

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

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

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

649− | Just d <- lookup e path

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

650 = if desc > 0

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

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

653 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]))

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

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

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

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

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

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

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

664 -- rest definitely terminates without

667 -- rest definitely terminates without

665 -- any cycles with route so far,

668 -- any cycles with route so far,

666 -- then we might yet be total

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

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

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

669 Total _ -> return Unchecked

672 Total _ -> return Unchecked

670 x -> return x

673 x -> return x

671 Just (nextarg, sc) ->

674 Just (nextarg, sc) ->

672 if nextarg == arg then

675 if nextarg == arg then

673 case sc of

676 case sc of

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

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

675 es pos

678 es pos

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

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

677− ((e, desc):path)

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

678 es

681 es

679 pos

682 pos

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

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

681 return (Partial Itself)

684 return (Partial Itself)

682 else return Unchecked in

685 else return Unchecked in

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

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

684− collapse' Unchecked pathres

687+ collapse' Unchecked pathres

685

688

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

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

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

690 | [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

705 pdef pdef pdef_inl pdef' ty)

706 addIBC (IBCDef n)

707 setTotality n tot

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

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

709+ defer_totcheck (fc, n)

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

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

710 i <- getIState

711 i <- getIState

711 case lookupDef n (tt_ctxt i) of

712 case lookupDef n (tt_ctxt i) of

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

1006 addDeferred def''

1007 addDeferred def''

1007

1008

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

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

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

1010− defer_totcheck (fc, fname)

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

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

1012

1011

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

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

test/reg006/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ reg006.idr -o reg006

2+idris $@ reg006.idr --check

3rm -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)

20ordElim (Sup f) P mZ mSuc mSup =

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

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

24+

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

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

24−myplus : Nat -> Nat -> Nat

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

25−

27+--

26−myplus Z y = y

28+-- myplus Z y = y

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

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

28−

30+--

29−myplus' Z y = y

31+-- myplus' Z y = y

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

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

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

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

33mnubBy = nubBy' []

35mnubBy = nubBy' []