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

idris.cabal+3

compare with master

unifiedsplit

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

824 test/totality013/run

825 test/totality013/*.idr

826 test/totality013/expected

827+ test/totality014/run

828+ test/totality014/*.idr

829+ test/totality014/expected

827

830

828 test/tutorial001/run

831 test/tutorial001/run

829 test/tutorial001/*.idr

832 test/tutorial001/*.idr

src/Idris/AbsSyntaxTree.hs+1

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

820 | DHide Name

821 | DFreeze Name

822 | DInjective Name

823+ | DSetTotal Name -- assert totality after checking

823 | DAccess Accessibility

824 | DAccess Accessibility

824 | DDefault DefaultTotality

825 | DDefault DefaultTotality

825 | DLogging Integer

826 | DLogging Integer

src/Idris/Coverage.hs+20−11

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

342checkPositive mut_ns (cn, ty')

343 = do i <- getIState

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

345− let p = cp ty

345+ let p = cp i ty

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

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

348 putIState (i { tt_ctxt = ctxt' })

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

352 where

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

354

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

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

356+ = posArg i aty && cp i sc

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

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

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

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

358− cp _ = True

359+ cp i _ = True

359

360

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

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

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

362+ posArg ist t = posParams ist t

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

366

363

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

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

368

365

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

369

378

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

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

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

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

src/Idris/Directives.hs+5

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

47 mapM_ (\n -> do

48 setInjectivity n True

49 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

50

55

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

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

52

57

src/Idris/Parser.hs+4

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

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

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

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

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

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

1386 acc <- accessibility

1390 acc <- accessibility

1387 ist <- get

1391 ist <- get

src/Idris/REPL.hs+6−2

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

1454showTotal t i = text (show t)

1455

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

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

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

1458− [t] -> showTotal t i

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

1459 _ -> empty

1460+ where

1461+ ppo = ppOptionIst ist

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

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

1460

1464

1461displayHelp = let vstr = showVersion version in

1465displayHelp = let vstr = showVersion version in

1462 "\nIdris version " ++ vstr ++ "\n" ++

1466 "\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

3+

4+total

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

6+runCon2 (MkCon2 _ Refl f) = f

7+