annotate lib/ur/string.ur @ 1388:3913cbfd72e9

String processing optimizations
author Adam Chlipala <adam@chlipala.net>
date Tue, 11 Jan 2011 14:03:54 -0500
parents f0afe61a6f8b
children 9a721f0722d3
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
adam@1388 6 val lengthGe = Basis.strlenGe
adamc@828 7 val append = Basis.strcat
adamc@828 8
adamc@821 9 val sub = Basis.strsub
adamc@821 10 val suffix = Basis.strsuffix
adamc@829 11
adamc@829 12 val index = Basis.strindex
adamc@829 13 val atFirst = Basis.strchr
adamc@829 14
adamc@1272 15 fun mindex {Haystack = s, Needle = chs} =
adamc@1272 16 let
adamc@1272 17 val n = Basis.strcspn s chs
adamc@1272 18 in
adamc@1272 19 if n >= length s then
adamc@1272 20 None
adamc@1272 21 else
adamc@1272 22 Some n
adamc@1272 23 end
adamc@831 24
adamc@829 25 fun substring s {Start = start, Len = len} = Basis.substring s start len
adamc@829 26
adamc@829 27 fun split s ch =
adamc@829 28 case index s ch of
adamc@829 29 None => None
adamc@829 30 | Some i => Some (substring s {Start = 0, Len = i},
adamc@829 31 substring s {Start = i + 1, Len = length s - i - 1})
adamc@831 32 fun msplit {Haystack = s, Needle = chs} =
adamc@831 33 case mindex {Haystack = s, Needle = chs} of
adamc@831 34 None => None
adamc@831 35 | Some i => Some (substring s {Start = 0, Len = i},
adamc@831 36 sub s i,
adamc@831 37 substring s {Start = i + 1, Len = length s - i - 1})
adamc@1057 38
adamc@1057 39 fun all f s =
adamc@1057 40 let
adamc@1057 41 val len = length s
adamc@1057 42
adamc@1057 43 fun al i =
adamc@1057 44 i >= len
adamc@1057 45 || (f (sub s i) && al (i + 1))
adamc@1057 46 in
adamc@1057 47 al 0
adamc@1057 48 end
adamc@1122 49
adamc@1131 50 fun mp f s =
adamc@1131 51 let
adamc@1131 52 fun mp' i acc =
adamc@1131 53 if i < 0 then
adamc@1131 54 acc
adamc@1131 55 else
adamc@1131 56 mp' (i - 1) (str (f (sub s i)) ^ acc)
adamc@1131 57 in
adamc@1131 58 mp' (length s - 1) ""
adamc@1131 59 end
adamc@1131 60
adam@1304 61 fun newlines [ctx] [[Body] ~ ctx] (s : string) : xml ([Body] ++ ctx) [] [] =
adamc@1122 62 case split s #"\n" of
adamc@1122 63 None => cdata s
adamc@1122 64 | Some (s1, s2) => <xml>{[s1]}<br/>{newlines s2}</xml>
adamc@1174 65
adamc@1174 66 fun isPrefix {Full = f, Prefix = p} =
adamc@1174 67 length f >= length p && substring f {Start = 0, Len = length p} = p