8d090c0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

A couple of small improvements to termination checking

* inlining to help out * %assert_total doesn't allow inlining so as not to break totality for functions which rely on the asserted function * bug fix for mutual recursion - build size graphs before doing any totality checking

commit8d090c096cd57eab6cd627a3786fe8cf73beade7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 16 Dec 2012, 14:47 (14 years ago) parentbf1c22e

7 files changed+30−14

compare with master

unifiedsplit

lib/Prelude/Strings.idr+10−1 src/Core/CaseTree.hs+2−1 src/Core/Evaluate.hs+10−6 src/Idris/Coverage.hs+3−3 src/Idris/ElabDecls.hs+3−1 src/Idris/Parser.hs+1−1 src/Idris/Prover.hs+1−1

lib/Prelude/Strings.idr+10−1

@@ -28,10 +28,15 @@ strM x with (choose (not (x == "")))

2828 strM x | (Left p) = believe_me $ StrCons (strHead' x p) (strTail' x p)

2929 strM x | (Right p) = believe_me StrNil

3030

31+-- annoyingly, we need these assert_totals because StrCons doesn't have

32+-- a recursive argument, therefore the termination checker doesn't believe

33+-- the string is guaranteed smaller. It makes a good point.

34+

35+%assert_total

3136unpack : String -> List Char

3237unpack s with (strM s)

3338 unpack "" | StrNil = []

34− unpack (strCons x xs) | (StrCons _ _) = x :: unpack xs

39+ unpack (strCons x xs) | (StrCons _ xs) = x :: unpack xs

3540

3641pack : List Char -> String

3742pack [] = ""

@@ -49,6 +54,7 @@ instance Semigroup String where

4954instance Monoid String where

5055 neutral = ""

5156

57+%assert_total

5258span : (Char -> Bool) -> String -> (String, String)

5359span p xs with (strM xs)

5460 span p "" | StrNil = ("", "")

@@ -63,6 +69,7 @@ break p = span (not . p)

6369split : (Char -> Bool) -> String -> List String

6470split p xs = map pack (split p (unpack xs))

6571

72+%assert_total

6673ltrim : String -> String

6774ltrim xs with (strM xs)

6875 ltrim "" | StrNil = ""

@@ -72,6 +79,7 @@ ltrim xs with (strM xs)

7279trim : String -> String

7380trim xs = ltrim (reverse (ltrim (reverse xs)))

7481

82+%assert_total

7583words' : List Char -> List (List Char)

7684words' s = case dropWhile isSpace s of

7785 [] => []

@@ -81,6 +89,7 @@ words' s = case dropWhile isSpace s of

8189words : String -> List String

8290words s = map pack $ words' $ unpack s

8391

92+%assert_total

8493lines' : List Char -> List (List Char)

8594lines' s = case dropWhile isNL s of

8695 [] => []

src/Core/CaseTree.hs+2−1

@@ -78,7 +78,8 @@ instance TermSize CaseAlt where

7878

7979small :: Name -> [Name] -> SC -> Bool

8080small n args t = let as = findAllUsedArgs t args in

81− length as == length (nub as) && termsize n t < 50

81+ length as == length (nub as) &&

82+ termsize n t < 6

8283

8384namesUsed :: SC -> [Name]

8485namesUsed sc = nub $ nu' [] sc where

src/Core/Evaluate.hs+10−6

@@ -615,10 +615,12 @@ instance Show Def where

615615 show (Function ty tm) = "Function: " ++ show (ty, tm)

616616 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty

617617 show (Operator ty _ _) = "Operator: " ++ show ty

618− show (CaseOp _ _ ty ps_in ps ns sc ns' sc')

618+ show (CaseOp inlc inlr ty ps_in ps ns sc ns' sc')

619619 = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++

620620 show ns ++ " " ++ show sc ++ "\n" ++

621− show ns' ++ " " ++ show sc'

621+ show ns' ++ " " ++ show sc' ++ "\n" ++

622+ if inlc then "Inlinable\n" else "Not inlinable\n"

623+

622624-- We need this for serialising Def. Fortunately, it never gets used because

623625-- we'll never serialise a primitive operator

624626

@@ -725,12 +727,12 @@ addDatatype (Data n tag ty cons) uctxt

725727 addCons (tag+1) cons (addDef n

726728 (TyDecl (DCon tag (arity ty')) ty, Public, Unchecked) ctxt)

727729

728−addCasedef :: Name -> Bool -> Bool -> Bool ->

730+addCasedef :: Name -> Bool -> Bool -> Bool -> Bool ->

729731 [Either Term (Term, Term)] ->

730732 [([Name], Term, Term)] ->

731733 [([Name], Term, Term)] ->

732734 Type -> Context -> Context

733−addCasedef n alwaysInline tcase covering ps_in ps psrt ty uctxt

735+addCasedef n alwaysInline tcase covering asserted ps_in ps psrt ty uctxt

734736 = let ctxt = definitions uctxt

735737 access = case lookupDefAcc Nothing n False uctxt of

736738 [(_, acc)] -> acc

@@ -738,8 +740,10 @@ addCasedef n alwaysInline tcase covering ps_in ps psrt ty uctxt

738740 ctxt' = case (simpleCase tcase covering CompileTime (FC "" 0) ps,

739741 simpleCase tcase covering RunTime (FC "" 0) psrt) of

740742 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->

741− let inl = alwaysInline in

742− addDef n (CaseOp inl (inl || small n args sc')

743+ let inl = alwaysInline

744+ inlc = (inl || small n args sc') && (not asserted)

745+ inlr = inl || small n args sc' in

746+ addDef n (CaseOp inlc inlr

743747 ty ps_in ps args sc args' sc',

744748 access, Unchecked) ctxt in

745749 uctxt { definitions = ctxt' }

src/Idris/Coverage.hs+3−3

@@ -382,8 +382,8 @@ checkTotality path fc n

382382checkDeclTotality :: (FC, Name) -> Idris Totality

383383checkDeclTotality (fc, n)

384384 = do logLvl 2 $ "Checking " ++ show n ++ " for totality"

385− buildSCG (fc, n)

386− logLvl 2 $ "Built SCG"

385+-- buildSCG (fc, n)

386+-- logLvl 2 $ "Built SCG"

387387 checkTotality [] fc n

388388

389389-- Calculate the size change graph for this definition

@@ -441,7 +441,7 @@ buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $

441441 map (getRel nty) (map (fst . unApply . getRetTy) args)

442442 where

443443 getRel ty (P _ n' _) | n' == ty = (n, Smaller)

444− getRel ty _ = (n, Unknown)

444+ getRel ty t = (n, Unknown)

445445

446446 scgAlt x vars szs (ConCase n _ args sc)

447447 -- all args smaller than top variable of x in sc

src/Idris/ElabDecls.hs+3−1

@@ -396,7 +396,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

396396 put (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) })

397397 case lookupTy (namespace info) n ctxt of

398398 [ty] -> do updateContext (addCasedef n (inlinable opts)

399− tcase knowncovering pats

399+ tcase knowncovering

400+ (AssertTotal `elem` opts)

401+ pats

400402 pdef pdef' ty)

401403 addIBC (IBCDef n)

402404 setTotality n tot

src/Idris/Parser.hs+1−1

@@ -119,7 +119,7 @@ loadSource lidr f

119119 -- build size change graph from simplified definitions

120120 iLOG "Totality checking"

121121 i <- get

122− -- mapM_ buildSCG (idris_totcheck i)

122+ mapM_ buildSCG (idris_totcheck i)

123123 mapM_ checkDeclTotality (idris_totcheck i)

124124 iLOG ("Finished " ++ f)

125125 ibcsd <- valIBCSubDir i

src/Idris/Prover.hs+1−1

@@ -50,7 +50,7 @@ prove ctxt lit n ty

5050 logLvl 3 (show tree)

5151 (ptm, pty) <- recheckC (FC "proof" 0) [] tm

5252 ptm' <- applyOpts ptm

53− updateContext (addCasedef n True False True

53+ updateContext (addCasedef n True False True False

5454 [Right (P Ref n ty, ptm)]

5555 [([], P Ref n ty, ptm)]

5656 [([], P Ref n ty, ptm')] ty)