Mercurial > urweb
annotate lib/ur/string.ur @ 1205:7cd11380cdf1
WHERE-dependent checking
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 04 Apr 2010 17:18:41 -0400 |
| parents | 9df124fcab3d |
| children | 56bd4a4f6e66 |
| rev | line source |
|---|---|
| adamc@821 | 1 type t = Basis.string |
| adamc@821 | 2 |
| adamc@1023 | 3 val str = Basis.str1 |
| adamc@1023 | 4 |
| adamc@828 | 5 val length = Basis.strlen |
| adamc@828 | 6 val append = Basis.strcat |
| adamc@828 | 7 |
| adamc@821 | 8 val sub = Basis.strsub |
| adamc@821 | 9 val suffix = Basis.strsuffix |
| adamc@829 | 10 |
| adamc@829 | 11 val index = Basis.strindex |
| adamc@829 | 12 val atFirst = Basis.strchr |
| adamc@829 | 13 |
| adamc@831 | 14 fun mindex {Haystack = s, Needle = chs} = Basis.strcspn s chs |
| adamc@831 | 15 |
| adamc@829 | 16 fun substring s {Start = start, Len = len} = Basis.substring s start len |
| adamc@829 | 17 |
| adamc@829 | 18 fun split s ch = |
| adamc@829 | 19 case index s ch of |
| adamc@829 | 20 None => None |
| adamc@829 | 21 | Some i => Some (substring s {Start = 0, Len = i}, |
| adamc@829 | 22 substring s {Start = i + 1, Len = length s - i - 1}) |
| adamc@831 | 23 fun msplit {Haystack = s, Needle = chs} = |
| adamc@831 | 24 case mindex {Haystack = s, Needle = chs} of |
| adamc@831 | 25 None => None |
| adamc@831 | 26 | Some i => Some (substring s {Start = 0, Len = i}, |
| adamc@831 | 27 sub s i, |
| adamc@831 | 28 substring s {Start = i + 1, Len = length s - i - 1}) |
| adamc@1057 | 29 |
| adamc@1057 | 30 fun all f s = |
| adamc@1057 | 31 let |
| adamc@1057 | 32 val len = length s |
| adamc@1057 | 33 |
| adamc@1057 | 34 fun al i = |
| adamc@1057 | 35 i >= len |
| adamc@1057 | 36 || (f (sub s i) && al (i + 1)) |
| adamc@1057 | 37 in |
| adamc@1057 | 38 al 0 |
| adamc@1057 | 39 end |
| adamc@1122 | 40 |
| adamc@1131 | 41 fun mp f s = |
| adamc@1131 | 42 let |
| adamc@1131 | 43 fun mp' i acc = |
| adamc@1131 | 44 if i < 0 then |
| adamc@1131 | 45 acc |
| adamc@1131 | 46 else |
| adamc@1131 | 47 mp' (i - 1) (str (f (sub s i)) ^ acc) |
| adamc@1131 | 48 in |
| adamc@1131 | 49 mp' (length s - 1) "" |
| adamc@1131 | 50 end |
| adamc@1131 | 51 |
| adamc@1122 | 52 fun newlines [ctx] [[Body] ~ ctx] s : xml ([Body] ++ ctx) [] [] = |
| adamc@1122 | 53 case split s #"\n" of |
| adamc@1122 | 54 None => cdata s |
| adamc@1122 | 55 | Some (s1, s2) => <xml>{[s1]}<br/>{newlines s2}</xml> |
| adamc@1174 | 56 |
| adamc@1174 | 57 fun isPrefix {Full = f, Prefix = p} = |
| adamc@1174 | 58 length f >= length p && substring f {Start = 0, Len = length p} = p |