Mercurial > urweb
annotate lib/ur/string.ur @ 1326:d91f84599693
Instantiate any Unit unification variables that remain after elaboration
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Thu, 02 Dec 2010 14:11:18 -0500 |
parents | f0afe61a6f8b |
children | 3913cbfd72e9 |
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@1272 | 14 fun mindex {Haystack = s, Needle = chs} = |
adamc@1272 | 15 let |
adamc@1272 | 16 val n = Basis.strcspn s chs |
adamc@1272 | 17 in |
adamc@1272 | 18 if n >= length s then |
adamc@1272 | 19 None |
adamc@1272 | 20 else |
adamc@1272 | 21 Some n |
adamc@1272 | 22 end |
adamc@831 | 23 |
adamc@829 | 24 fun substring s {Start = start, Len = len} = Basis.substring s start len |
adamc@829 | 25 |
adamc@829 | 26 fun split s ch = |
adamc@829 | 27 case index s ch of |
adamc@829 | 28 None => None |
adamc@829 | 29 | Some i => Some (substring s {Start = 0, Len = i}, |
adamc@829 | 30 substring s {Start = i + 1, Len = length s - i - 1}) |
adamc@831 | 31 fun msplit {Haystack = s, Needle = chs} = |
adamc@831 | 32 case mindex {Haystack = s, Needle = chs} of |
adamc@831 | 33 None => None |
adamc@831 | 34 | Some i => Some (substring s {Start = 0, Len = i}, |
adamc@831 | 35 sub s i, |
adamc@831 | 36 substring s {Start = i + 1, Len = length s - i - 1}) |
adamc@1057 | 37 |
adamc@1057 | 38 fun all f s = |
adamc@1057 | 39 let |
adamc@1057 | 40 val len = length s |
adamc@1057 | 41 |
adamc@1057 | 42 fun al i = |
adamc@1057 | 43 i >= len |
adamc@1057 | 44 || (f (sub s i) && al (i + 1)) |
adamc@1057 | 45 in |
adamc@1057 | 46 al 0 |
adamc@1057 | 47 end |
adamc@1122 | 48 |
adamc@1131 | 49 fun mp f s = |
adamc@1131 | 50 let |
adamc@1131 | 51 fun mp' i acc = |
adamc@1131 | 52 if i < 0 then |
adamc@1131 | 53 acc |
adamc@1131 | 54 else |
adamc@1131 | 55 mp' (i - 1) (str (f (sub s i)) ^ acc) |
adamc@1131 | 56 in |
adamc@1131 | 57 mp' (length s - 1) "" |
adamc@1131 | 58 end |
adamc@1131 | 59 |
adam@1304 | 60 fun newlines [ctx] [[Body] ~ ctx] (s : string) : xml ([Body] ++ ctx) [] [] = |
adamc@1122 | 61 case split s #"\n" of |
adamc@1122 | 62 None => cdata s |
adamc@1122 | 63 | Some (s1, s2) => <xml>{[s1]}<br/>{newlines s2}</xml> |
adamc@1174 | 64 |
adamc@1174 | 65 fun isPrefix {Full = f, Prefix = p} = |
adamc@1174 | 66 length f >= length p && substring f {Start = 0, Len = length p} = p |