annotate src/ur/feed.ur @ 4:af95d9d73eb5

Feed.tree
author Adam Chlipala <adam@chlipala.net>
date Tue, 11 Jan 2011 18:04:15 -0500
parents ea0ca570c121
children 2717458d8951
rev   line source
adam@0 1 task initialize = fn () => FeedFfi.init
adam@0 2
adam@4 3 con pattern internal output = {Initial : internal,
adam@4 4 EnterTag : {Tag : string, Attrs : list (string * string), Cdata : option string} -> internal -> option internal,
adam@4 5 ExitTag : internal -> option internal,
adam@4 6 Finished : internal -> option (output * bool)}
adam@4 7
adam@4 8 val null : pattern unit (variant []) =
adam@4 9 {Initial = (),
adam@4 10 EnterTag = fn _ () => Some (),
adam@4 11 ExitTag = fn () => Some (),
adam@4 12 Finished = fn () => None}
adam@1 13
adam@1 14 con tagInternal (attrs :: {Unit}) = option {Attrs : $(mapU string attrs), Cdata : option string}
adam@1 15
adam@3 16 fun tagG [attrs ::: {Unit}] [t ::: Type] (fl : folder attrs) (accept : {Attrs : $(mapU string attrs), Cdata : option string} -> option t)
adam@3 17 (name : string) (attrs : $(mapU string attrs))
adam@3 18 : pattern (tagInternal attrs) t =
adam@4 19 {Initial = None,
adam@4 20 EnterTag = fn tinfo _ =>
adam@4 21 if tinfo.Tag <> name then
adam@4 22 None
adam@4 23 else
adam@4 24 case @foldUR [string] [fn r => option $(mapU string r)]
adam@4 25 (fn [nm ::_] [r ::_] [[nm] ~ r] aname ro =>
adam@4 26 case ro of
adam@4 27 None => None
adam@4 28 | Some r =>
adam@4 29 case List.assoc aname tinfo.Attrs of
adam@4 30 None => None
adam@4 31 | Some v => Some ({nm = v} ++ r))
adam@4 32 (Some {}) fl attrs of
adam@4 33 None => None
adam@4 34 | Some vs =>
adam@4 35 let
adam@4 36 val v = {Attrs = vs, Cdata = tinfo.Cdata}
adam@4 37 in
adam@4 38 case accept v of
adam@4 39 None => None
adam@4 40 | Some _ => Some (Some v)
adam@4 41 end,
adam@4 42 ExitTag = fn _ => None,
adam@4 43 Finished = fn state => case state of
adam@4 44 None => None
adam@4 45 | Some state =>
adam@4 46 case accept state of
adam@4 47 None => None
adam@4 48 | Some v => Some (v, False)}
adam@3 49
adam@3 50 fun tag [attrs ::: {Unit}] (fl : folder attrs) (name : string) (attrs : $(mapU string attrs))
adam@3 51 : pattern (tagInternal attrs) {Attrs : $(mapU string attrs), Cdata : option string} =
adam@3 52 @tagG fl Some name attrs
adam@3 53
adam@3 54 fun tagA [attrs ::: {Unit}] (fl : folder attrs) (name : string) (attrs : $(mapU string attrs))
adam@3 55 : pattern (tagInternal attrs) $(mapU string attrs) =
adam@3 56 @tagG fl (fn r => Some r.Attrs) name attrs
adam@3 57
adam@3 58 fun tagC (name : string) : pattern (tagInternal []) string =
adam@3 59 tagG (fn r => r.Cdata) name {}
adam@1 60
adam@4 61 datatype status a = Initial | Pending of a | Matched of a
adam@1 62
adam@1 63 con childrenInternal (parent :: Type) (children :: {Type}) = option (parent * int * $(map status children))
adam@1 64
adam@1 65 fun children [parentI ::: Type] [parent ::: Type] [children ::: {(Type * Type)}]
adam@4 66 (parent : pattern parentI parent) (children : $(map (fn (i, d) => pattern i d) children)) (fl : folder children)
adam@1 67 : pattern (childrenInternal parentI (map fst children)) (parent * $(map snd children)) =
adam@4 68 {Initial = None,
adam@4 69 EnterTag = fn tinfo state =>
adam@4 70 case state of
adam@4 71 None =>
adam@4 72 (case parent.EnterTag tinfo parent.Initial of
adam@4 73 None => None
adam@4 74 | Some pstate => Some (Some (pstate, 1, @map0 [status] (fn [t ::_] => Initial)
adam@4 75 (@@Folder.mp [fst] [_] fl))))
adam@4 76 | Some (pstate, depth, cstates) =>
adam@4 77 Some (Some (pstate,
adam@4 78 depth+1,
adam@4 79 @map2 [fn (i, d) => pattern i d] [fn (i, d) => status i] [fn (i, d) => status i]
adam@4 80 (fn [p] (ch : pattern p.1 p.2) (cstate : status p.1) =>
adam@4 81 case cstate of
adam@4 82 Initial =>
adam@4 83 (case ch.EnterTag tinfo ch.Initial of
adam@4 84 None => Initial
adam@4 85 | Some v =>
adam@4 86 case ch.Finished v of
adam@4 87 None => Pending v
adam@4 88 | _ => Matched v)
adam@4 89 | Pending cstate =>
adam@4 90 (case ch.EnterTag tinfo cstate of
adam@4 91 None => Initial
adam@4 92 | Some v =>
adam@4 93 case ch.Finished v of
adam@4 94 None => Pending v
adam@4 95 | _ => Matched v)
adam@4 96 | v => v)
adam@4 97 fl children cstates)),
adam@4 98 ExitTag = fn state =>
adam@4 99 case state of
adam@4 100 None => None
adam@4 101 | Some (pstate, 1, cstates) =>
adam@4 102 (case parent.ExitTag pstate of
adam@4 103 None => None
adam@4 104 | Some pstate => Some (Some (pstate, 0, cstates)))
adam@4 105 | Some (pstate, depth, cstates) =>
adam@4 106 Some (Some (pstate, depth-1,
adam@4 107 @map2 [fn (i, d) => pattern i d] [fn (i, d) => status i] [fn (i, d) => status i]
adam@4 108 (fn [p] (ch : pattern p.1 p.2) (cstate : status p.1) =>
adam@4 109 case cstate of
adam@4 110 Pending cstate =>
adam@4 111 (case ch.ExitTag cstate of
adam@4 112 None => Initial
adam@4 113 | Some cstate' =>
adam@4 114 case ch.Finished cstate' of
adam@4 115 None => Pending cstate'
adam@4 116 | _ => Matched cstate')
adam@4 117 | _ => cstate)
adam@4 118 fl children cstates)),
adam@4 119 Finished = fn state =>
adam@4 120 case state of
adam@4 121 Some (pstate, _, cstates) =>
adam@4 122 (case parent.Finished pstate of
adam@4 123 None => None
adam@4 124 | Some (pdata, pcont) =>
adam@4 125 case @foldR2 [fn (i, d) => pattern i d] [fn (i, d) => status i] [fn cs => option $(map snd cs)]
adam@4 126 (fn [nm ::_] [p ::_] [r ::_] [[nm] ~ r] (ch : pattern p.1 p.2) (cstate : status p.1) acc =>
adam@4 127 case acc of
adam@4 128 None => None
adam@4 129 | Some acc =>
adam@4 130 case cstate of
adam@4 131 Matched cstate =>
adam@4 132 (case ch.Finished cstate of
adam@1 133 None => None
adam@4 134 | Some (cdata, _) => Some ({nm = cdata} ++ acc))
adam@4 135 | _ => None)
adam@4 136 (Some {}) fl children cstates of
adam@4 137 None => None
adam@4 138 | Some cdata => Some ((pdata, cdata), pcont))
adam@4 139 | _ => None}
adam@1 140
adam@4 141 con treeInternal (parent :: Type) (child :: Type) = option (parent * int * option child)
adam@4 142
adam@4 143 fun tree [parentI ::: Type] [parent ::: Type] [childI ::: Type] [child ::: Type]
adam@4 144 (parent : pattern parentI parent) (child : pattern childI child)
adam@4 145 : pattern (treeInternal parentI childI) (parent * child) =
adam@4 146 {Initial = None,
adam@4 147 EnterTag = fn tinfo state =>
adam@4 148 case state of
adam@4 149 None =>
adam@4 150 (case parent.EnterTag tinfo parent.Initial of
adam@4 151 None => None
adam@4 152 | Some pstate => Some (Some (pstate, 1, None)))
adam@4 153 | Some (pstate, depth, cstate) =>
adam@4 154 Some (Some (pstate,
adam@4 155 depth+1,
adam@4 156 child.EnterTag tinfo (Option.get child.Initial cstate))),
adam@4 157 ExitTag = fn state =>
adam@4 158 case state of
adam@4 159 None => None
adam@4 160 | Some (pstate, 1, cstate) =>
adam@4 161 (case parent.ExitTag pstate of
adam@4 162 None => None
adam@4 163 | Some pstate => Some (Some (pstate, 0, cstate)))
adam@4 164 | Some (pstate, depth, cstate) =>
adam@4 165 Some (Some (pstate, depth-1, Option.bind child.ExitTag cstate)),
adam@4 166 Finished = fn state =>
adam@4 167 case state of
adam@4 168 None => None
adam@4 169 | Some (pstate, _, cstate) =>
adam@4 170 case parent.Finished pstate of
adam@4 171 None => None
adam@4 172 | Some (pdata, _) =>
adam@4 173 case cstate of
adam@4 174 None => None
adam@4 175 | Some cstate =>
adam@4 176 case child.Finished cstate of
adam@4 177 None => None
adam@4 178 | Some (cdata, _) => Some ((pdata, cdata), True)}
adam@4 179
adam@4 180 fun app [internal ::: Type] [data ::: Type] (p : pattern internal data) (f : data -> transaction {}) (url : string) : transaction {} =
adam@1 181 let
adam@1 182 fun recur xml state =
adam@4 183 case String.seek xml #"<" of
adam@1 184 None => return ()
adam@4 185 | Some xml =>
adam@1 186 if xml <> "" && String.sub xml 0 = #"/" then
adam@4 187 case String.seek xml #"\x3E" of
adam@1 188 None => return ()
adam@4 189 | Some xml =>
adam@1 190 case p.ExitTag state of
adam@1 191 None => recur xml p.Initial
adam@1 192 | Some state =>
adam@1 193 case p.Finished state of
adam@1 194 None => recur xml state
adam@4 195 | Some (data, cont) =>
adam@1 196 f data;
adam@4 197 recur xml (if cont then state else p.Initial)
adam@1 198 else if xml <> "" && String.sub xml 0 = #"?" then
adam@4 199 case String.seek xml #"\x3E" of
adam@1 200 None => return ()
adam@4 201 | Some xml => recur xml state
adam@1 202 else if xml <> "" && String.sub xml 0 = #"!" then
adam@2 203 if String.lengthGe xml 3 && String.sub xml 1 = #"-" && String.sub xml 2 = #"-" then
adam@1 204 let
adam@1 205 fun skipper xml =
adam@4 206 case String.seek xml #"-" of
adam@1 207 None => xml
adam@4 208 | Some xml =>
adam@2 209 if String.lengthGe xml 2 && String.sub xml 0 = #"-" && String.sub xml 1 = #"\x3E" then
adam@1 210 String.suffix xml 2
adam@1 211 else
adam@1 212 skipper xml
adam@1 213 in
adam@1 214 recur (skipper (String.suffix xml 3)) state
adam@1 215 end
adam@1 216 else
adam@4 217 case String.seek xml #"]" of
adam@1 218 None => return ()
adam@4 219 | Some xml =>
adam@4 220 case String.seek xml #"\x3E" of
adam@1 221 None => return ()
adam@4 222 | Some xml => recur xml state
adam@1 223 else
adam@1 224 case String.msplit {Needle = " >/", Haystack = xml} of
adam@1 225 None => return ()
adam@1 226 | Some (tagName, ch, xml) =>
adam@1 227 let
adam@1 228 fun readAttrs ch xml acc =
adam@1 229 case ch of
adam@1 230 #"\x3E" => (xml, acc, False)
adam@1 231 | #"/" =>
adam@4 232 (case String.seek xml #"\x3E" of
adam@1 233 None => (xml, acc, True)
adam@4 234 | Some xml => (xml, acc, True))
adam@1 235 | _ =>
adam@2 236 if String.lengthGe xml 2 && Char.isSpace (String.sub xml 0) then
adam@1 237 readAttrs (String.sub xml 0) (String.suffix xml 1) acc
adam@1 238 else if xml <> "" && String.sub xml 0 = #"\x3E" then
adam@1 239 (String.suffix xml 1, acc, False)
adam@1 240 else if xml <> "" && String.sub xml 0 = #"/" then
adam@4 241 (case String.seek xml #"\x3E" of
adam@1 242 None => (xml, acc, True)
adam@4 243 | Some xml => (xml, acc, True))
adam@1 244 else
adam@1 245 case String.split xml #"=" of
adam@1 246 None => (xml, acc, False)
adam@1 247 | Some (aname, xml) =>
adam@1 248 if xml = "" || String.sub xml 0 <> #"\"" then
adam@1 249 (xml, (aname, "") :: acc, False)
adam@1 250 else
adam@1 251 case String.split (String.suffix xml 1) #"\"" of
adam@1 252 None => (xml, (aname, "") :: acc, False)
adam@1 253 | Some (value, xml) =>
adam@1 254 if xml = "" then
adam@1 255 (xml, (aname, value) :: acc, False)
adam@1 256 else
adam@1 257 readAttrs (String.sub xml 0) (String.suffix xml 1) ((aname, value) :: acc)
adam@1 258
adam@1 259 val (xml, attrs, ended) = readAttrs ch xml []
adam@1 260
adam@1 261 fun skipSpaces xml =
adam@1 262 if xml <> "" && Char.isSpace (String.sub xml 0) then
adam@1 263 skipSpaces (String.suffix xml 1)
adam@1 264 else
adam@1 265 xml
adam@1 266
adam@1 267 val xml = skipSpaces xml
adam@1 268
adam@1 269 val (xml, cdata) =
adam@1 270 if ended then
adam@1 271 (xml, None)
adam@1 272 else if String.isPrefix {Prefix = "<![CDATA[", Full = xml} then
adam@1 273 let
adam@1 274 fun skipper xml acc =
adam@1 275 case String.split xml #"]" of
adam@1 276 None => (acc ^ xml, None)
adam@1 277 | Some (pre, xml) =>
adam@2 278 if String.lengthGe xml 2 && String.sub xml 0 = #"]" && String.sub xml 1 = #"\x3E" then
adam@1 279 (String.suffix xml 2, Some (acc ^ pre))
adam@1 280 else
adam@1 281 skipper xml (acc ^ "]" ^ pre)
adam@1 282 in
adam@1 283 skipper (String.suffix xml 9) ""
adam@1 284 end
adam@1 285 else
adam@4 286 case String.split' xml #"<" of
adam@1 287 None => (xml, None)
adam@4 288 | Some (cdata, xml) => (xml, Some cdata)
adam@1 289 in
adam@1 290 case p.EnterTag {Tag = tagName, Attrs = attrs, Cdata = cdata} state of
adam@1 291 None => recur xml p.Initial
adam@1 292 | Some state =>
adam@4 293 case p.Finished state of
adam@4 294 None =>
adam@4 295 (case (if ended then p.ExitTag state else Some state) of
adam@4 296 None => recur xml p.Initial
adam@4 297 | Some state =>
adam@4 298 case p.Finished state of
adam@4 299 None => recur xml state
adam@4 300 | Some (data, cont) =>
adam@4 301 f data;
adam@4 302 recur xml (if cont then state else p.Initial))
adam@4 303 | Some (data, cont) =>
adam@4 304 f data;
adam@4 305 recur xml (if cont then state else p.Initial)
adam@1 306 end
adam@1 307 in
adam@1 308 xml <- FeedFfi.fetch url;
adam@1 309 recur xml p.Initial
adam@1 310 end