adam@8: (* This module implements imperative processing of XML feeds.
adam@8:  *
adam@8:  * Module author: Adam Chlipala
adam@8:  *)
adam@8: 
adam@1: con pattern :: Type -> Type -> Type
adam@8: (* A pattern describes a set of XML subtrees, mapping each element of the set to
adam@8:  * a data value.  A value of type [pattern internal result] uses values of type
adam@8:  * [internal] internally, but this API exposes no details of that usage.  The
adam@8:  * type [result] gives the type used in mappings of matched subtrees. *)
adam@8: 
adam@8: val null : pattern unit (variant [])
adam@8: (* A null pattern matches nothing, returning a value of the impossible empty
adam@8:  * type if it ever does match. *)
adam@1: 
adam@1: con tagInternal :: {Unit} -> Type
adam@1: 
adam@1: val tag : attrs ::: {Unit} -> folder attrs -> string -> $(mapU string attrs)
adam@1:           -> pattern (tagInternal attrs) {Attrs : $(mapU string attrs), Cdata : option string}
adam@8: (* A basic [tag] pattern matches a single tag with a number of required
adam@8:  * attributes.  A result value gives the attribute values and an optional
adam@8:  * CDATA value for the text content of the tag.  The [string] argument is the
adam@8:  * tag name, and the following argument gives attribute names. *)
adam@1: 
adam@3: val tagA : attrs ::: {Unit} -> folder attrs -> string -> $(mapU string attrs)
adam@3:           -> pattern (tagInternal attrs) $(mapU string attrs)
adam@8: (* A version of [tag] that ignores CDATA *)
adam@8: 
kkallio@9: val tagAV : attrs ::: {Unit} -> folder attrs -> string -> $(mapU (string * option string) attrs)
kkallio@9:             -> pattern (tagInternal attrs) $(mapU string attrs)
kkallio@9: (* Extension of tagA with optional specification of values which attributes must
kkallio@9:  * bear in order to count as a match. *)
kkallio@9: 
adam@6: val tagAO : attrs ::: {Unit} -> folder attrs -> string -> $(mapU string attrs)
adam@6:             -> pattern (tagInternal attrs) $(mapU (option string) attrs)
adam@8: (* A version of [tagA] that makes each attribute optional *)
adam@6: 
adam@3: val tagC : string -> pattern (tagInternal []) string
adam@8: (* A version of [tag] that only matches tags with nonempty CDATA and returns
adam@8:  * only that text *)
adam@3: 
adam@1: con childrenInternal :: Type -> {Type} -> Type
adam@1: 
adam@1: val children : parentI ::: Type -> parent ::: Type -> children ::: {(Type * Type)}
adam@1:                -> pattern parentI parent -> $(map (fn (i, d) => pattern i d) children) -> folder children
adam@1:                -> pattern (childrenInternal parentI (map fst children)) (parent * $(map snd children))
adam@8: (* A combinator that takes in a pattern for a parent node and a set of patterns
adam@8:  * that must be matched against children of the parent.  This combinator will
adam@8:  * find at most one match per matching parent node. *)
adam@8: 
adam@6: val childrenO : parentI ::: Type -> parent ::: Type -> children ::: {(Type * Type)}
adam@6:                 -> pattern parentI parent -> $(map (fn (i, d) => pattern i d) children) -> folder children
adam@6:                 -> pattern (childrenInternal parentI (map fst children)) (parent * $(map (fn (i, d) => option d) children))
adam@8: (* A version of [children] where each child pattern need not be matched *)
adam@1: 
kkallio@11: datatype required t = Required of t | Optional of t
kkallio@11: (* Used for marking items as required or optional. *)
kkallio@11: 
kkallio@11: val childrenO' : parentI ::: Type -> parent ::: Type -> children ::: {(Type * Type)}
kkallio@11:                  -> pattern parentI parent -> $(map (fn (i, d) => required (pattern i d)) children) -> folder children
kkallio@11:                  -> pattern (childrenInternal parentI (map fst children)) (parent * $(map (fn (i, d) => option d) children))
kkallio@11: (* A version of [children] where the caller marks each child pattern
kkallio@11:  * as either required or optional. *)
kkallio@11: 
adam@4: con treeInternal :: Type -> Type -> Type
adam@4: 
adam@4: val tree : parentI ::: Type -> parent ::: Type -> childI ::: Type -> child ::: Type
adam@4:            -> pattern parentI parent -> pattern childI child
adam@4:            -> pattern (treeInternal parentI childI) (parent * child)
adam@8: (* A combinator that takes in a pattern for a parent node and another pattern to
adam@8:  * be matched at any depth within the parent's subtree.  Unlike [children],
adam@8:  * [tree] finds as many subtree matches per parent node as possible. *)
adam@4: 
adam@5: type document
adam@7: val show_document : show document
adam@8: (* Type of uninterpreted XML documents *)
adam@5: 
adam@8: val fetch : string -> transaction document
adam@8: (* Retrieve a document by URL. *)
adam@8: 
kkallio@10: val app' : internal ::: Type -> data ::: Type -> acc ::: Type -> pattern internal data 
kkallio@10:            -> (data -> acc -> transaction acc) -> document -> acc -> transaction acc
kkallio@10: (* Find all matches of a pattern in a document, running an imperative function
kkallio@10:  * on the data returned by each match while threading through some state. *)
kkallio@10: 
adam@5: val app : internal ::: Type -> data ::: Type -> pattern internal data -> (data -> transaction {}) -> document -> transaction {}
adam@8: (* Find all matches of a pattern in a document, running an imperative function
adam@8:  * on the data returned by each match. *)