|
adam@8
|
1 (* This module implements imperative processing of XML feeds.
|
|
adam@8
|
2 *
|
|
adam@8
|
3 * Module author: Adam Chlipala
|
|
adam@8
|
4 *)
|
|
adam@8
|
5
|
|
adam@1
|
6 con pattern :: Type -> Type -> Type
|
|
adam@8
|
7 (* A pattern describes a set of XML subtrees, mapping each element of the set to
|
|
adam@8
|
8 * a data value. A value of type [pattern internal result] uses values of type
|
|
adam@8
|
9 * [internal] internally, but this API exposes no details of that usage. The
|
|
adam@8
|
10 * type [result] gives the type used in mappings of matched subtrees. *)
|
|
adam@8
|
11
|
|
adam@8
|
12 val null : pattern unit (variant [])
|
|
adam@8
|
13 (* A null pattern matches nothing, returning a value of the impossible empty
|
|
adam@8
|
14 * type if it ever does match. *)
|
|
adam@1
|
15
|
|
adam@1
|
16 con tagInternal :: {Unit} -> Type
|
|
adam@1
|
17
|
|
adam@1
|
18 val tag : attrs ::: {Unit} -> folder attrs -> string -> $(mapU string attrs)
|
|
adam@1
|
19 -> pattern (tagInternal attrs) {Attrs : $(mapU string attrs), Cdata : option string}
|
|
adam@8
|
20 (* A basic [tag] pattern matches a single tag with a number of required
|
|
adam@8
|
21 * attributes. A result value gives the attribute values and an optional
|
|
adam@8
|
22 * CDATA value for the text content of the tag. The [string] argument is the
|
|
adam@8
|
23 * tag name, and the following argument gives attribute names. *)
|
|
adam@1
|
24
|
|
adam@3
|
25 val tagA : attrs ::: {Unit} -> folder attrs -> string -> $(mapU string attrs)
|
|
adam@3
|
26 -> pattern (tagInternal attrs) $(mapU string attrs)
|
|
adam@8
|
27 (* A version of [tag] that ignores CDATA *)
|
|
adam@8
|
28
|
|
kkallio@9
|
29 val tagAV : attrs ::: {Unit} -> folder attrs -> string -> $(mapU (string * option string) attrs)
|
|
kkallio@9
|
30 -> pattern (tagInternal attrs) $(mapU string attrs)
|
|
kkallio@9
|
31 (* Extension of tagA with optional specification of values which attributes must
|
|
kkallio@9
|
32 * bear in order to count as a match. *)
|
|
kkallio@9
|
33
|
|
adam@6
|
34 val tagAO : attrs ::: {Unit} -> folder attrs -> string -> $(mapU string attrs)
|
|
adam@6
|
35 -> pattern (tagInternal attrs) $(mapU (option string) attrs)
|
|
adam@8
|
36 (* A version of [tagA] that makes each attribute optional *)
|
|
adam@6
|
37
|
|
adam@21
|
38 val tagAOR : optional ::: {Unit} -> required ::: {Unit} -> [optional ~ required]
|
|
adam@21
|
39 => folder optional -> folder required -> string
|
|
adam@21
|
40 -> $(mapU string required) -> $(mapU string optional)
|
|
adam@21
|
41 -> pattern (tagInternal (optional ++ required))
|
|
adam@21
|
42 $(mapU string required ++ mapU (option string) optional)
|
|
adam@21
|
43 (* A version of [tagAO] that does a check for mere presence of other attributes *)
|
|
adam@21
|
44
|
|
adam@3
|
45 val tagC : string -> pattern (tagInternal []) string
|
|
adam@8
|
46 (* A version of [tag] that only matches tags with nonempty CDATA and returns
|
|
adam@8
|
47 * only that text *)
|
|
adam@3
|
48
|
|
adam@1
|
49 con childrenInternal :: Type -> {Type} -> Type
|
|
adam@1
|
50
|
|
adam@1
|
51 val children : parentI ::: Type -> parent ::: Type -> children ::: {(Type * Type)}
|
|
adam@1
|
52 -> pattern parentI parent -> $(map (fn (i, d) => pattern i d) children) -> folder children
|
|
adam@1
|
53 -> pattern (childrenInternal parentI (map fst children)) (parent * $(map snd children))
|
|
adam@8
|
54 (* A combinator that takes in a pattern for a parent node and a set of patterns
|
|
adam@8
|
55 * that must be matched against children of the parent. This combinator will
|
|
adam@8
|
56 * find at most one match per matching parent node. *)
|
|
adam@8
|
57
|
|
adam@6
|
58 val childrenO : parentI ::: Type -> parent ::: Type -> children ::: {(Type * Type)}
|
|
adam@6
|
59 -> pattern parentI parent -> $(map (fn (i, d) => pattern i d) children) -> folder children
|
|
adam@6
|
60 -> pattern (childrenInternal parentI (map fst children)) (parent * $(map (fn (i, d) => option d) children))
|
|
adam@8
|
61 (* A version of [children] where each child pattern need not be matched *)
|
|
adam@1
|
62
|
|
kkallio@11
|
63 datatype required t = Required of t | Optional of t
|
|
kkallio@11
|
64 (* Used for marking items as required or optional. *)
|
|
kkallio@11
|
65
|
|
kkallio@11
|
66 val childrenO' : parentI ::: Type -> parent ::: Type -> children ::: {(Type * Type)}
|
|
kkallio@11
|
67 -> pattern parentI parent -> $(map (fn (i, d) => required (pattern i d)) children) -> folder children
|
|
kkallio@11
|
68 -> pattern (childrenInternal parentI (map fst children)) (parent * $(map (fn (i, d) => option d) children))
|
|
kkallio@11
|
69 (* A version of [children] where the caller marks each child pattern
|
|
kkallio@11
|
70 * as either required or optional. *)
|
|
kkallio@11
|
71
|
|
adam@4
|
72 con treeInternal :: Type -> Type -> Type
|
|
adam@4
|
73
|
|
adam@4
|
74 val tree : parentI ::: Type -> parent ::: Type -> childI ::: Type -> child ::: Type
|
|
adam@4
|
75 -> pattern parentI parent -> pattern childI child
|
|
adam@4
|
76 -> pattern (treeInternal parentI childI) (parent * child)
|
|
adam@8
|
77 (* A combinator that takes in a pattern for a parent node and another pattern to
|
|
adam@8
|
78 * be matched at any depth within the parent's subtree. Unlike [children],
|
|
adam@8
|
79 * [tree] finds as many subtree matches per parent node as possible. *)
|
|
adam@4
|
80
|
|
kkallio@14
|
81 con gatherInternal :: Type -> Type -> Type -> Type
|
|
kkallio@14
|
82
|
|
kkallio@14
|
83 val gather : parentI ::: Type -> parent ::: Type -> childI ::: Type -> child ::: Type
|
|
kkallio@14
|
84 -> pattern parentI parent -> pattern childI child
|
|
kkallio@14
|
85 -> pattern (gatherInternal parentI childI child) (parent * list child)
|
|
kkallio@14
|
86 (* A combinator like tree that collects matching subtree patterns into a list rather
|
|
kkallio@14
|
87 * than handling them one at a time. *)
|
|
kkallio@14
|
88
|
|
adam@5
|
89 type document
|
|
adam@7
|
90 val show_document : show document
|
|
adam@8
|
91 (* Type of uninterpreted XML documents *)
|
|
adam@5
|
92
|
|
adam@8
|
93 val fetch : string -> transaction document
|
|
adam@8
|
94 (* Retrieve a document by URL. *)
|
|
adam@8
|
95
|
|
kkallio@10
|
96 val app' : internal ::: Type -> data ::: Type -> acc ::: Type -> pattern internal data
|
|
kkallio@10
|
97 -> (data -> acc -> transaction acc) -> document -> acc -> transaction acc
|
|
kkallio@10
|
98 (* Find all matches of a pattern in a document, running an imperative function
|
|
kkallio@10
|
99 * on the data returned by each match while threading through some state. *)
|
|
kkallio@10
|
100
|
|
adam@5
|
101 val app : internal ::: Type -> data ::: Type -> pattern internal data -> (data -> transaction {}) -> document -> transaction {}
|
|
adam@8
|
102 (* Find all matches of a pattern in a document, running an imperative function
|
|
adam@8
|
103 * on the data returned by each match. *)
|
