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