git.iko.soy/Idris-dev
on master help sign in
Remove %assert_total from Nat and Strings
f650e7eEdwin Brady
libs/prelude/Prelude/Nat.idr+3−6
compare with master
unifiedsplit
@@ -41,12 +41,11 @@ total mult : Nat -> Nat -> Nat
41mult Z right = Z
41mult Z right = Z
42mult (S left) right = plus right $ mult left right
42mult (S left) right = plus right $ mult left right
43
43
44−%assert_total
45fromIntegerNat : Integer -> Nat
44fromIntegerNat : Integer -> Nat
46fromIntegerNat 0 = Z
45fromIntegerNat 0 = Z
47fromIntegerNat n =
46fromIntegerNat n =
48 if (n > 0) then
47 if (n > 0) then
49− S (fromIntegerNat (n - 1))
48+ S (fromIntegerNat (assert_smaller n (n - 1)))
50 else
49 else
51 Z
50 Z
52
51
@@ -259,19 +258,17 @@ instance Integral Nat where
259 div = divNat
258 div = divNat
260 mod = modNat
259 mod = modNat
261
260
262−%assert_total
263log2 : Nat -> Nat
261log2 : Nat -> Nat
264log2 Z = Z
262log2 Z = Z
265log2 (S Z) = Z
263log2 (S Z) = Z
266−log2 n = S (log2 (n `divNat` 2))
264+log2 n = S (log2 (assert_smaller n (n `divNat` 2)))
267
265
268--------------------------------------------------------------------------------
266--------------------------------------------------------------------------------
269-- GCD and LCM
267-- GCD and LCM
270--------------------------------------------------------------------------------
268--------------------------------------------------------------------------------
271−%assert_total
272gcd : Nat -> Nat -> Nat
269gcd : Nat -> Nat -> Nat
273gcd a Z = a
270gcd a Z = a
274−gcd a b = gcd b (a `modNat` b)
271+gcd a b = assert_total (gcd b (a `modNat` b))
275
272
276total lcm : Nat -> Nat -> Nat
273total lcm : Nat -> Nat -> Nat
277lcm _ Z = Z
274lcm _ Z = Z
libs/prelude/Prelude/Strings.idr+11−19
@@ -43,31 +43,28 @@ data StrM : String -> Type where
43 StrNil : StrM ""
43 StrNil : StrM ""
44 StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)
44 StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)
45
45
46−%assert_total
47strHead' : (x : String) -> so (not (x == "")) -> Char
46strHead' : (x : String) -> so (not (x == "")) -> Char
48−strHead' x p = prim__strHead x
47+strHead' x p = assert_total $ prim__strHead x
49
48
50−%assert_total
51strTail' : (x : String) -> so (not (x == "")) -> String
49strTail' : (x : String) -> so (not (x == "")) -> String
52−strTail' x p = prim__strTail x
50+strTail' x p = assert_total $ prim__strTail x
53
51
54-- we need the 'believe_me' because the operations are primitives
52-- we need the 'believe_me' because the operations are primitives
55−
56−%assert_total
57strM : (x : String) -> StrM x
53strM : (x : String) -> StrM x
58strM x with (choose (not (x == "")))
54strM 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))
60 strM x | (Right p) = really_believe_me StrNil
58 strM x | (Right p) = really_believe_me StrNil
61
59
62-- annoyingly, we need these assert_totals because StrCons doesn't have
60-- annoyingly, we need these assert_totals because StrCons doesn't have
63-- a recursive argument, therefore the termination checker doesn't believe
61-- a recursive argument, therefore the termination checker doesn't believe
64-- the string is guaranteed smaller. It makes a good point.
62-- the string is guaranteed smaller. It makes a good point.
65
63
66−%assert_total
67unpack : String -> List Char
64unpack : String -> List Char
68unpack s with (strM s)
65unpack s with (strM s)
69 unpack "" | StrNil = []
66 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)
71
68
72pack : (Foldable t) => t Char -> String
69pack : (Foldable t) => t Char -> String
73pack = foldr strCons ""
70pack = foldr strCons ""
@@ -90,12 +87,11 @@ instance Semigroup String where
90instance Monoid String where
87instance Monoid String where
91 neutral = ""
88 neutral = ""
92
89
93−%assert_total
94span : (Char -> Bool) -> String -> (String, String)
90span : (Char -> Bool) -> String -> (String, String)
95span p xs with (strM xs)
91span p xs with (strM xs)
96 span p "" | StrNil = ("", "")
92 span p "" | StrNil = ("", "")
97 span p (strCons x xs) | (StrCons _ _) with (p x)
93 span p (strCons x xs) | (StrCons _ _) with (p x)
98− | True with (span p xs)
94+ | True with (assert_total (span p xs))
99 | (ys, zs) = (strCons x ys, zs)
95 | (ys, zs) = (strCons x ys, zs)
100 | False = ("", strCons x xs)
96 | False = ("", strCons x xs)
101
97
@@ -105,32 +101,29 @@ break p = span (not . p)
105split : (Char -> Bool) -> String -> List String
101split : (Char -> Bool) -> String -> List String
106split p xs = map pack (split p (unpack xs))
102split p xs = map pack (split p (unpack xs))
107
103
108−%assert_total
109ltrim : String -> String
104ltrim : String -> String
110ltrim xs with (strM xs)
105ltrim xs with (strM xs)
111 ltrim "" | StrNil = ""
106 ltrim "" | StrNil = ""
112 ltrim (strCons x xs) | StrCons _ _
107 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)
114
109
115trim : String -> String
110trim : String -> String
116trim xs = ltrim (reverse (ltrim (reverse xs)))
111trim xs = ltrim (reverse (ltrim (reverse xs)))
117
112
118−%assert_total
119words' : List Char -> List (List Char)
113words' : List Char -> List (List Char)
120words' s = case dropWhile isSpace s of
114words' s = case dropWhile isSpace s of
121 [] => []
115 [] => []
122 s' => let (w, s'') = break isSpace s'
116 s' => let (w, s'') = break isSpace s'
123− in w :: words' s''
117+ in w :: words' (assert_smaller s s'')
124
118
125words : String -> List String
119words : String -> List String
126words s = map pack $ words' $ unpack s
120words s = map pack $ words' $ unpack s
127
121
128−%assert_total
129lines' : List Char -> List (List Char)
122lines' : List Char -> List (List Char)
130lines' s = case dropWhile isNL s of
123lines' s = case dropWhile isNL s of
131 [] => []
124 [] => []
132 s' => let (w, s'') = break isNL s'
125 s' => let (w, s'') = break isNL s'
133− in w :: lines' s''
126+ in w :: lines' (assert_smaller s s'')
134
127
135lines : String -> List String
128lines : String -> List String
136lines s = map pack $ lines' $ unpack s
129lines s = map pack $ lines' $ unpack s
@@ -140,10 +133,9 @@ foldr1 : (a -> a -> a) -> List a -> a
140foldr1 f [x] = x
133foldr1 f [x] = x
141foldr1 f (x::xs) = f x (foldr1 f xs)
134foldr1 f (x::xs) = f x (foldr1 f xs)
142
135
143−%assert_total -- due to foldr1, but used safely
144unwords' : List (List Char) -> List Char
136unwords' : List (List Char) -> List Char
145unwords' [] = []
137unwords' [] = []
146−unwords' ws = (foldr1 addSpace ws)
138+unwords' ws = assert_total (foldr1 addSpace ws)
147 where
139 where
148 addSpace : List Char -> List Char -> List Char
140 addSpace : List Char -> List Char -> List Char
149 addSpace w s = w ++ (' ' :: s)
141 addSpace w s = w ++ (' ' :: s)