2cfcbcf · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Positivity checking under parameters

Need to check indices don't contain the type being defined - parameters are okay. Fixes #1833 Also a totality error message fix.

commit2cfcbcf0e5dc729f9e0498a8b69a7519fdcf3a37 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 18 May 2016, 15:44 (10 years ago) parentc326d84

9 files changed+51−13

compare with master

unifiedsplit

idris.cabal+3 src/Idris/AbsSyntaxTree.hs+1 src/Idris/Coverage.hs+20−11 src/Idris/Directives.hs+5 src/Idris/Parser.hs+4 src/Idris/REPL.hs+6−2 test/totality014/expected+2 test/totality014/run+3 test/totality014/totality014.idr+7

idris.cabal+3

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

824824 test/totality013/run

825825 test/totality013/*.idr

826826 test/totality013/expected

827+ test/totality014/run

828+ test/totality014/*.idr

829+ test/totality014/expected

827830

828831 test/tutorial001/run

829832 test/tutorial001/*.idr

src/Idris/AbsSyntaxTree.hs+1

@@ -820,6 +820,7 @@ data Directive = DLib Codegen String

820820 | DHide Name

821821 | DFreeze Name

822822 | DInjective Name

823+ | DSetTotal Name -- assert totality after checking

823824 | DAccess Accessibility

824825 | DDefault DefaultTotality

825826 | DLogging Integer

src/Idris/Coverage.hs+20−11

@@ -342,7 +342,7 @@ checkPositive :: [Name] -- ^ the group of type declarations

342342checkPositive mut_ns (cn, ty')

343343 = do i <- getIState

344344 let ty = delazy' True (normalise (tt_ctxt i) [] ty')

345− let p = cp ty

345+ let p = cp i ty

346346 let tot = if p then Total (args ty) else Partial NotPositive

347347 let ctxt' = setTotal cn tot (tt_ctxt i)

348348 putIState (i { tt_ctxt = ctxt' })

@@ -352,20 +352,29 @@ checkPositive mut_ns (cn, ty')

352352 where

353353 args t = [0..length (getArgTys t)-1]

354354

355− cp (Bind n (Pi _ aty _) sc) = posArg aty && cp sc

356− cp t | (P _ n' _, args) <- unApply t,

357− n' `elem` mut_ns = all noRec args

358− cp _ = True

355+ cp i (Bind n (Pi _ aty _) sc)

356+ = posArg i aty && cp i sc

357+ cp i t | (P _ n' _ , args) <- unApply t,

358+ n' `elem` mut_ns = all noRec args

359+ cp i _ = True

359360

360− posArg (Bind _ (Pi _ nty _) sc)

361− | (P _ n' _, args) <- unApply nty

362− = n' `notElem` mut_ns && all noRec args && posArg sc

363− posArg t | (P _ n' _, args) <- unApply t,

364− n' `elem` mut_ns = all noRec args

365− posArg _ = True

361+ posArg ist (Bind _ (Pi _ nty _) sc) = noRec nty && posArg ist sc

362+ posArg ist t = posParams ist t

366363

367364 noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)

368365

366+ -- If the type appears recursively in a parameter argument, that's

367+ -- fine, otherwise if it appears in an argument it's not fine.

368+ posParams ist t | (P _ n _, args) <- unApply t

369+ = case lookupCtxtExact n (idris_datatypes ist) of

370+ Just ti -> checkParamsOK (param_pos ti) 0 args

371+ Nothing -> and (map (posParams ist) args)

372+ posParams ist t = noRec t

373+

374+ checkParamsOK ppos i [] = True

375+ checkParamsOK ppos i (p : ps)

376+ | i `elem` ppos = checkParamsOK ppos (i + 1) ps

377+ | otherwise = noRec p && checkParamsOK ppos (i + 1) ps

369378

370379-- | Calculate the totality of a function from its patterns. Either

371380-- follow the size change graph (if inductive) or check for

src/Idris/Directives.hs+5

@@ -47,6 +47,11 @@ directiveAction (DInjective n') = do

4747 mapM_ (\n -> do

4848 setInjectivity n True

4949 addIBC (IBCInjective n True)) ns

50+directiveAction (DSetTotal n') = do

51+ ns <- allNamespaces n'

52+ mapM_ (\n -> do

53+ setTotality n (Total [])

54+ addIBC (IBCTotal n (Total []))) ns

5055

5156directiveAction (DAccess acc) = do updateIState (\i -> i { default_access = acc })

5257

src/Idris/Parser.hs+4

@@ -1382,6 +1382,10 @@ directive syn = do try (lchar '%' *> reserved "lib")

13821382 -- only, and won't be documented/could be removed at any point

13831383 <|> do try (lchar '%' *> reserved "assert_injective"); n <- fst <$> fnName

13841384 return [PDirective (DInjective n)]

1385+ -- Assert totality of something after definition. This is

1386+ -- here as a debugging aid, so commented out...

1387+-- <|> do try (lchar '%' *> reserved "assert_set_total"); n <- fst <$> fnName

1388+-- return [PDirective (DSetTotal n)]

13851389 <|> do try (lchar '%' *> reserved "access")

13861390 acc <- accessibility

13871391 ist <- get

src/Idris/REPL.hs+6−2

@@ -1454,9 +1454,13 @@ showTotal t@(Partial (Mutual ns)) i

14541454showTotal t i = text (show t)

14551455

14561456showTotalN :: IState -> Name -> Doc OutputAnnotation

1457−showTotalN i n = case lookupTotal n (tt_ctxt i) of

1458− [t] -> showTotal t i

1457+showTotalN ist n = case lookupTotal n (tt_ctxt ist) of

1458+ [t] -> showN n <> text ", which is" <+> showTotal t ist

14591459 _ -> empty

1460+ where

1461+ ppo = ppOptionIst ist

1462+ showN n = annotate (AnnName n Nothing Nothing Nothing) . text $

1463+ showName (Just ist) [] ppo False n

14601464

14611465displayHelp = let vstr = showVersion version in

14621466 "\nIdris version " ++ vstr ++ "\n" ++

test/totality014/expectednew file+2

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

1+totality014.idr:6:1:

2+Main.runCon2 is possibly not total due to: Main.MkCon2

test/totality014/runnew file+3

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

1+#!/usr/bin/env bash

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

3+rm -f *.ibc

test/totality014/totality014.idrnew file+7

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

1+data Con2 : Type where

2+ MkCon2 : (a : Type) -> Con2 = a -> (a -> Void) -> Con2

4+total

5+runCon2 : Con2 -> (Con2 -> Void)

6+runCon2 (MkCon2 _ Refl f) = f