helm/interface/theoryParser2.ml

   1 exception IllFormedXml of int;;
   2
   3 (* Utility functions that transform a Pxp attribute into something useful *)
   4
   5 let string_of_attr a =
   6  let module T = Pxp_types in
   7   match a with
   8      T.Value s -> s
   9    | _ -> raise (IllFormedXml 0)
  10
  11 let get_theory n =
  12  let module D = Pxp_document in
  13  let module T = Theory in
  14   let rec get_theory_elem n =
  15    let ntype = n # node_type in
  16    match ntype with
  17      D.T_element "THEOREM" ->
  18        let uri = string_of_attr (n # attribute "uri") in
  19         T.Theorem uri
  20    | D.T_element "DEFINITION" ->
  21        let uri = string_of_attr (n # attribute "uri") in
  22         T.Definition uri
  23    | D.T_element "AXIOM" ->
  24       let uri = string_of_attr (n # attribute "uri") in
  25        T.Axiom uri
  26    | D.T_element "VARIABLE" ->
  27       let uri = string_of_attr (n # attribute "uri") in
  28        T.Variable uri
  29    | D.T_element "SECTION" ->
  30       let uri = string_of_attr (n # attribute "uri")
  31       and subtheory = List.map get_theory_elem (n # sub_nodes) in
  32        T.Section (uri, subtheory)
  33    | D.T_element _ | D.T_data | _ ->
  34       raise (IllFormedXml 1)
  35   in
  36    match n # node_type with
  37       D.T_element "Theory" ->
  38        let uri = string_of_attr (n # attribute "uri") in
  39         (uri, List.map get_theory_elem (n # sub_nodes))
  40     | _ -> raise (IllFormedXml 2)
  41 ;;