95d226f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix a proof of Void

Fixing the notion of 'recoverable' for function applications

commit95d226ff36baca221256135637114ff6341eda18 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 23 Mar 2017, 10:32 (10 years ago) parent9bb3386

6 files changed+30−2

compare with master

unifiedsplit

src/Idris/Coverage.hs+11−1 src/Idris/Elab/Clause.hs+2 test/TestData.hs+2−1 test/totality022/expected+1 test/totality022/run+3 test/totality022/totality022.idr+11

src/Idris/Coverage.hs+11−1

@@ -440,12 +440,22 @@ checkRec fa@(App _ _ _) fa'@(App _ _ _)

440440 (f', as') <- unApply fa'

441441 = if (length as /= length as')

442442 then checkRec f f'

443− else checkRecs (f : as) (f' : as')

443+ -- Same function but different args is recoverable,

444+ -- and vice versa, if it's an ordinary function

445+ -- If a constructor, everything has to be recoverable

446+ else do fok <- checkRec f f'

447+ argok <- checkRecs (f : as) (f : as')

448+ return (if conType f then fok && argok

449+ else fok || argok)

444450 where

445451 checkRecs [] [] = return True

446452 checkRecs (a : as) (b : bs) = do aok <- checkRec a b

447453 asok <- checkRecs as bs

448454 return (aok && asok)

455+ conType (P (DCon _ _ _) _ _) = True

456+ conType (P (TCon _ _) _ _) = True

457+ conType _ = False

458+

449459checkRec (P xt x _) (P yt y _)

450460 | x == y = return True

451461 | ntRec xt yt = return True

src/Idris/Elab/Clause.hs+2

@@ -611,6 +611,8 @@ checkPossible info fc tcgen fname lhs_in

611611 return Nothing

612612 -- if it's a recoverable error, the case may become possible

613613 Error err -> do logLvl 10 $ "Impossible case " ++ (pshow i err)

614+ ++ "\n" ++ show (recoverableCoverage ctxt err,

615+ validCoverageCase ctxt err)

614616 -- tcgen means that it was generated by genClauses,

615617 -- so only looking for an error. Otherwise, it

616618 -- needs to be the right kind of error (a type mismatch

test/TestData.hs+2−1

@@ -284,7 +284,8 @@ testFamiliesData = [

284284 ( 18, ANY ),

285285 ( 19, ANY ),

286286 ( 20, ANY ),

287− ( 21, ANY )]),

287+ ( 21, ANY ),

288+ ( 22, ANY )]),

288289 ("tutorial", "Tutorial examples",

289290 [ ( 1, ANY ),

290291 ( 2, ANY ),

test/totality022/expectednew file+1

@@ -0,0 +1 @@

1+totality022.idr:7:3:f _ [] (RSnoc _ _) is a valid case

test/totality022/runnew file+3

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

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ totality022.idr --check

3+rm -f *.ibc

test/totality022/totality022.idrnew file+11

@@ -0,0 +1,11 @@

1+data Rev : List a -> Type where

2+ RSnoc : (x : a) -> Rev xs -> Rev (xs ++ [x])

3+ RNil : Rev []

5+total

6+f : (x : a) -> (ys : List a) -> (rxs : Rev (ys ++ [x])) -> Void

7+f _ [] (RSnoc _ _) impossible -- = ?wat

8+f _ [] RNil impossible

9+f _ (_ :: _) (RSnoc _ _) impossible

10+f _ (_ :: _) RNil impossible

11+