annotate src/ur/feed.ur @ 7:05a28a77f6fe

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