526cd75 · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -347,6 +347,9 @@ Extra-source-files:

347 test/totality002/run

348 test/totality002/*.idr

349 test/totality002/expected

350+ test/totality003/run

351+ test/totality003/*.idr

352+ test/totality003/expected

350

353

351source-repository head

354source-repository head

352 type: git

355 type: git

libs/prelude/Builtins.idr+3

@@ -39,6 +39,9 @@ malloc size x = x -- compiled specially

39trace_malloc : a -> a

40trace_malloc x = x -- compiled specially

41

42+assert_smaller : a -> a -> a

43+assert_smaller x y = y

44+

42abstract %assert_total -- need to pretend

45abstract %assert_total -- need to pretend

43believe_me : a -> b -- compiled specially as id, use with care!

46believe_me : a -> b -- compiled specially as id, use with care!

44believe_me x = prim__believe_me _ _ x

47believe_me x = prim__believe_me _ _ x

libs/prelude/Prelude/List.idr+7−11

@@ -382,13 +382,12 @@ span p (x::xs) =

382break : (a -> Bool) -> List a -> (List a, List a)

383break p = span (not . p)

384

385−%assert_total

386split : (a -> Bool) -> List a -> List (List a)

385split : (a -> Bool) -> List a -> List (List a)

387split p [] = []

386split p [] = []

388split p xs =

387split p xs =

389 case break p xs of

388 case break p xs of

390 (chunk, []) => [chunk]

389 (chunk, []) => [chunk]

391− (chunk, (c :: rest)) => chunk :: split p rest

390+ (chunk, (c :: rest)) => chunk :: split p (assert_smaller xs rest)

392

391

393partition : (a -> Bool) -> List a -> (List a, List a)

392partition : (a -> Bool) -> List a -> (List a, List a)

394partition p [] = ([], [])

393partition p [] = ([], [])

@@ -432,26 +431,23 @@ sorted (x::xs) =

432 Nil => True

431 Nil => True

433 (y::ys) => x <= y && sorted (y::ys)

432 (y::ys) => x <= y && sorted (y::ys)

434

433

435−%assert_total -- can't work this out, because in the case which is lifted out

436− -- y::ys and x::xs are bigger than the inputs...

437mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a

434mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a

438mergeBy order [] right = right

435mergeBy order [] right = right

439mergeBy order left [] = left

436mergeBy order left [] = left

440mergeBy order (x::xs) (y::ys) =

437mergeBy order (x::xs) (y::ys) =

441− case order x y of

438+ if order x y == LT

442− LT => x :: mergeBy order xs (y::ys)

439+ then x :: mergeBy order xs (y::ys)

443− _ => y :: mergeBy order (x::xs) ys

440+ else y :: mergeBy order (x::xs) ys

444

441

445merge : Ord a => List a -> List a -> List a

442merge : Ord a => List a -> List a -> List a

446merge = mergeBy compare

443merge = mergeBy compare

447

444

448−%assert_total

449sort : Ord a => List a -> List a

445sort : Ord a => List a -> List a

450sort [] = []

446sort [] = []

451sort [x] = [x]

447sort [x] = [x]

452−sort xs =

453− let (x, y) = split xs in

448+sort xs = let (x, y) = split xs in

449+ merge (sort (assert_smaller xs x))

454− merge (sort x) (sort y) -- not structurally smaller, hence assert

450+ (sort (assert_smaller xs y)) -- not structurally smaller, hence assert

455 where

451 where

456 splitRec : List a -> List a -> (List a -> List a) -> (List a, List a)

452 splitRec : List a -> List a -> (List a -> List a) -> (List a, List a)

457 splitRec (_::_::xs) (y::ys) zs = splitRec xs ys (zs . ((::) y))

453 splitRec (_::_::xs) (y::ys) zs = splitRec xs ys (zs . ((::) y))

src/Idris/Coverage.hs+3

@@ -439,6 +439,9 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

439 -- find which argument in pargs <a> is smaller than, if any

440 checkSize a (p : ps) i

441 | a == p = Just (i, Same)

442+ | (P _ (UN as) _, [_,arg,_]) <- unApply a,

443+ as == txt "assert_smaller" && arg == p

444+ = Just (i, Smaller)

442 | smaller Nothing a (p, Nothing) = Just (i, Smaller)

445 | smaller Nothing a (p, Nothing) = Just (i, Smaller)

443 | otherwise = checkSize a ps (i + 1)

446 | otherwise = checkSize a ps (i + 1)

444 checkSize a [] i = Nothing

447 checkSize a [] i = Nothing

test/runtest.pl+5−3

@@ -57,7 +57,7 @@ if ($#ARGV>=0) {

57 opendir my $dir, ".";

58 my @list = readdir $dir;

59 foreach my $file (@list) {

60− if ($file =~ /[0-9][0-9][0-9]/) {

60+ if ($file =~ /[0-9][0-9][0-9]$/) {

61 push @tests, $file;

62 }

63 }

@@ -72,7 +72,7 @@ if ($#ARGV>=0) {

72 opendir my $dir, ".";

73 my @list = readdir $dir;

74 foreach my $file (@list) {

75− if ($file =~ /[0-9][0-9][0-9]/) {

75+ if ($file =~ /[0-9][0-9][0-9]$/) {

76 if (!(grep ($_ eq $file, @without))) {

77 push @tests, $file;

78 }

@@ -84,7 +84,9 @@ if ($#ARGV>=0) {

84 @tests = sort @tests;

85 }

86 else {

87+ if ($test =~ /[0-9][0-9][0-9]$/) {

87− push @tests, $test;

88+ push @tests, $test;

89+ }

88 }

90 }

89 @opts = @ARGV;

91 @opts = @ARGV;

90}

92}

test/totality003/expectednew file+1

@@ -0,0 +1 @@

1+totality003a.idr:5:1:smaller.qsort is possibly not total due to recursive path smaller.qsort --> smaller.qsort --> smaller.qsort

test/totality003/runnew file+4

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

1+#!/usr/bin/env bash

2+idris $@ totality003.idr --check

3+idris $@ totality003a.idr --check

4+rm -f *.ibc

test/totality003/totality003.idrnew file+7

@@ -0,0 +1,7 @@

1+module smaller

2+

3+total

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

5+qsort [] = []

6+qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (<= x) xs)) ++

7+ (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs)))

test/totality003/totality003a.idrnew file+7