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

lib/Prelude/Strings.idr+10−1

compare with master

unifiedsplit

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

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

29 strM x | (Right p) = believe_me StrNil

30

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

31unpack : String -> List Char

36unpack : String -> List Char

32unpack s with (strM s)

37unpack s with (strM s)

33 unpack "" | StrNil = []

38 unpack "" | StrNil = []

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

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

35

40

36pack : List Char -> String

41pack : List Char -> String

37pack [] = ""

42pack [] = ""

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

49instance Monoid String where

54instance Monoid String where

50 neutral = ""

55 neutral = ""

51

56

57+%assert_total

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

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

53span p xs with (strM xs)

59span p xs with (strM xs)

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

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

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

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

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

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

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

65

71

72+%assert_total

66ltrim : String -> String

73ltrim : String -> String

67ltrim xs with (strM xs)

74ltrim xs with (strM xs)

68 ltrim "" | StrNil = ""

75 ltrim "" | StrNil = ""

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

72trim : String -> String

79trim : String -> String

73trim xs = ltrim (reverse (ltrim (reverse xs)))

80trim xs = ltrim (reverse (ltrim (reverse xs)))

74

81

82+%assert_total

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

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

76words' s = case dropWhile isSpace s of

84words' s = case dropWhile isSpace s of

77 [] => []

85 [] => []

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

81words : String -> List String

89words : String -> List String

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

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

83

91

92+%assert_total

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

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

85lines' s = case dropWhile isNL s of

94lines' s = case dropWhile isNL s of

86 [] => []

95 [] => []

src/Core/CaseTree.hs+2−1

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

78

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

80small 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

82

83

83namesUsed :: SC -> [Name]

84namesUsed :: SC -> [Name]

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

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

src/Core/Evaluate.hs+10−6

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

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

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

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

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

620 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+

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

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

623-- we'll never serialise a primitive operator

625-- we'll never serialise a primitive operator

624

626

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

725 addCons (tag+1) cons (addDef n

727 addCons (tag+1) cons (addDef n

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

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

727

729

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

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

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

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

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

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

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

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

732 Type -> Context -> Context

734 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

734 = let ctxt = definitions uctxt

736 = let ctxt = definitions uctxt

735 access = case lookupDefAcc Nothing n False uctxt of

737 access = case lookupDefAcc Nothing n False uctxt of

736 [(_, acc)] -> acc

738 [(_, acc)] -> acc

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

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

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

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

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

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

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

741− let inl = alwaysInline in

743+ let inl = alwaysInline

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

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

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

746+ addDef n (CaseOp inlc inlr

743 ty ps_in ps args sc args' sc',

747 ty ps_in ps args sc args' sc',

744 access, Unchecked) ctxt in

748 access, Unchecked) ctxt in

745 uctxt { definitions = ctxt' }

749 uctxt { definitions = ctxt' }

src/Idris/Coverage.hs+3−3

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

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

383checkDeclTotality (fc, n)

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

385− buildSCG (fc, n)

385+-- buildSCG (fc, n)

386− logLvl 2 $ "Built SCG"

386+-- logLvl 2 $ "Built SCG"

387 checkTotality [] fc n

388

389-- Calculate the size change graph for this definition

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

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

442 where

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

444− getRel ty _ = (n, Unknown)

444+ getRel ty t = (n, Unknown)

445

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

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

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

397 case lookupTy (namespace info) n ctxt of

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

399− tcase knowncovering pats

399+ tcase knowncovering

400+ (AssertTotal `elem` opts)

401+ pats

400 pdef pdef' ty)

402 pdef pdef' ty)

401 addIBC (IBCDef n)

403 addIBC (IBCDef n)

402 setTotality n tot

404 setTotality n tot

src/Idris/Parser.hs+1−1

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

119 -- build size change graph from simplified definitions

120 iLOG "Totality checking"

121 i <- get

122− -- mapM_ buildSCG (idris_totcheck i)

122+ mapM_ buildSCG (idris_totcheck i)

123 mapM_ checkDeclTotality (idris_totcheck i)

124 iLOG ("Finished " ++ f)

125 ibcsd <- valIBCSubDir i

src/Idris/Prover.hs+1−1

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

50 logLvl 3 (show tree)

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

52 ptm' <- applyOpts ptm

53− updateContext (addCasedef n True False True

53+ updateContext (addCasedef n True False True False

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

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

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