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

git.iko.soy/Idris-dev

Add assert_smaller function

assert_smaller x y evaluates to y, and asserts to the totality checker than y is structurally smaller than x. This can be used to explain the reasoning for totality if the checker cannot work it out itself. For example: total qsort : Ord a => List a -> List a qsort [] = [] qsort (x :: xs) = qsort (assert_smaller (x :: xs) (filter (<= x) xs)) ++ (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs))) The expression 'assert_smaller (x :: xs) (filter (<= x) xs)' asserts that the result of the filter will always be smaller than the pattern (x :: xs). Using this is always preferable to %assert_total if the termination argument can be explained in this way.

commit526cd757e0c51ecaf245c331fff8f0f48e4bfa82 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 1 Feb 2014, 22:52 (13 years ago) parentec57557

9 files changed+40−14

compare with master

unifiedsplit

idris.cabal+3 libs/prelude/Builtins.idr+3 libs/prelude/Prelude/List.idr+7−11 src/Idris/Coverage.hs+3 test/runtest.pl+5−3 test/totality003/expected+1 test/totality003/run+4 test/totality003/totality003.idr+7 test/totality003/totality003a.idr+7

idris.cabal+3

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

347347 test/totality002/run

348348 test/totality002/*.idr

349349 test/totality002/expected

350+ test/totality003/run

351+ test/totality003/*.idr

352+ test/totality003/expected

350353

351354source-repository head

352355 type: git

libs/prelude/Builtins.idr+3

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

3939trace_malloc : a -> a

4040trace_malloc x = x -- compiled specially

4141

42+assert_smaller : a -> a -> a

43+assert_smaller x y = y

44+

4245abstract %assert_total -- need to pretend

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

4447believe_me x = prim__believe_me _ _ x

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

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

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

383383break p = span (not . p)

384384

385−%assert_total

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

387386split p [] = []

388387split p xs =

389388 case break p xs of

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

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

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

392391

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

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

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

432431 Nil => True

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

434433

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

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

438435mergeBy order [] right = right

439436mergeBy order left [] = left

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

441− case order x y of

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

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

438+ if order x y == LT

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

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

444441

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

446443merge = mergeBy compare

447444

448−%assert_total

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

450446sort [] = []

451447sort [x] = [x]

452−sort xs =

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

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

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

449+ merge (sort (assert_smaller xs x))

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

455451 where

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

457453 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

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

440440 checkSize a (p : ps) i

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

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

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

444+ = Just (i, Smaller)

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

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

444447 checkSize a [] i = Nothing

test/runtest.pl+5−3

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

5757 opendir my $dir, ".";

5858 my @list = readdir $dir;

5959 foreach my $file (@list) {

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

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

6161 push @tests, $file;

6262 }

6363 }

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

7272 opendir my $dir, ".";

7373 my @list = readdir $dir;

7474 foreach my $file (@list) {

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

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

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

7777 push @tests, $file;

7878 }

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

8484 @tests = sort @tests;

8585 }

8686 else {

87− push @tests, $test;

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

88+ push @tests, $test;

89+ }

8890 }

8991 @opts = @ARGV;

9092}

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

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