@@ -43,31 +43,28 @@ data StrM : String -> Type where
4343 StrNil : StrM ""
4444 StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)
4545
46−%assert_total
4746strHead' : (x : String) -> so (not (x == "")) -> Char
48−strHead' x p = prim__strHead x
47+strHead' x p = assert_total $ prim__strHead x
4948
50−%assert_total
5149strTail' : (x : String) -> so (not (x == "")) -> String
52−strTail' x p = prim__strTail x
50+strTail' x p = assert_total $ prim__strTail x
5351
5452-- we need the 'believe_me' because the operations are primitives
55−
56−%assert_total
5753strM : (x : String) -> StrM x
5854strM x with (choose (not (x == "")))
59− strM x | (Left p) = really_believe_me $ StrCons (strHead' x p) (strTail' x p)
55+ strM x | (Left p) = really_believe_me $
56+ StrCons (assert_total (strHead' x p))
57+ (assert_total (strTail' x p))
6058 strM x | (Right p) = really_believe_me StrNil
6159
6260-- annoyingly, we need these assert_totals because StrCons doesn't have
6361-- a recursive argument, therefore the termination checker doesn't believe
6462-- the string is guaranteed smaller. It makes a good point.
6563
66−%assert_total
6764unpack : String -> List Char
6865unpack s with (strM s)
6966 unpack "" | StrNil = []
70− unpack (strCons x xs) | (StrCons x xs) = x :: unpack xs
67+ unpack (strCons x xs) | (StrCons x xs) = x :: assert_total (unpack xs)
7168
7269pack : (Foldable t) => t Char -> String
7370pack = foldr strCons ""
@@ -90,12 +87,11 @@ instance Semigroup String where
9087instance Monoid String where
9188 neutral = ""
9289
93−%assert_total
9490span : (Char -> Bool) -> String -> (String, String)
9591span p xs with (strM xs)
9692 span p "" | StrNil = ("", "")
9793 span p (strCons x xs) | (StrCons _ _) with (p x)
98− | True with (span p xs)
94+ | True with (assert_total (span p xs))
9995 | (ys, zs) = (strCons x ys, zs)
10096 | False = ("", strCons x xs)
10197
@@ -105,32 +101,29 @@ break p = span (not . p)
105101split : (Char -> Bool) -> String -> List String
106102split p xs = map pack (split p (unpack xs))
107103
108−%assert_total
109104ltrim : String -> String
110105ltrim xs with (strM xs)
111106 ltrim "" | StrNil = ""
112107 ltrim (strCons x xs) | StrCons _ _
113− = if (isSpace x) then (ltrim xs) else (strCons x xs)
108+ = if (isSpace x) then assert_total (ltrim xs) else (strCons x xs)
114109
115110trim : String -> String
116111trim xs = ltrim (reverse (ltrim (reverse xs)))
117112
118−%assert_total
119113words' : List Char -> List (List Char)
120114words' s = case dropWhile isSpace s of
121115 [] => []
122116 s' => let (w, s'') = break isSpace s'
123− in w :: words' s''
117+ in w :: words' (assert_smaller s s'')
124118
125119words : String -> List String
126120words s = map pack $ words' $ unpack s
127121
128−%assert_total
129122lines' : List Char -> List (List Char)
130123lines' s = case dropWhile isNL s of
131124 [] => []
132125 s' => let (w, s'') = break isNL s'
133− in w :: lines' s''
126+ in w :: lines' (assert_smaller s s'')
134127
135128lines : String -> List String
136129lines s = map pack $ lines' $ unpack s
@@ -140,10 +133,9 @@ foldr1 : (a -> a -> a) -> List a -> a
140133foldr1 f [x] = x
141134foldr1 f (x::xs) = f x (foldr1 f xs)
142135
143−%assert_total -- due to foldr1, but used safely
144136unwords' : List (List Char) -> List Char
145137unwords' [] = []
146−unwords' ws = (foldr1 addSpace ws)
138+unwords' ws = assert_total (foldr1 addSpace ws)
147139 where
148140 addSpace : List Char -> List Char -> List Char
149141 addSpace w s = w ++ (' ' :: s)