xml - xml から Coq 型を返し、OCaml で解析関数を書く

Question

 <xs:element name="lhs">
   <xs:complexType>
     <xs:choice>
        <xs:sequence>
           <xs:element maxOccurs="unbounded" minOccurs="0" ref="state"/>
        </xs:sequence>
         <xs:element ref="state"/>
      </xs:choice>
    </xs:complexType>
  </xs:element>

この xsds から型を返します。タグのCoq場合は型を返します。次に例を示します。<choice>Inductive

Inductive lhs = 
 | Lhs_lhs : list state -> lhs
 | Lhs_state : state -> lhs.

最初のコンストラクターで、Lhs_lhs上記のタイプのように強制的に生成します。タグ<sequence>にはタグ名がないためです。

その後、この xsds を解析する関数を次のように記述しますOCaml。

let rec lhs x = get_son "lhs" lhs_val

and lhs_val xs = match xs with
  | Element ("", _, _, xs) -> 
   let item_state, xs = parse_list state xs in
     check_emptyness xs;
   Lhs_lhs (item_state)
  | Element ("state", _, _, xs) -> Lhs_state (state_val xs)
  | x -> error_xml x "it is not a lhs";;

ここでparse_list:

let try_parse parse x = try Some (parse x) with Error _ -> None;;

(* parses the biggest prefix of `xs` with the
  (parse) function, i.e. it returns the pair `(is, xs2)` such that:
         - xs = xs1 @ xs2
         - `is = List.map parse xs1`
        `- xs1` is as big as possible *)
let parse_list parse =
  let rec aux is = function
    | [] -> List.rev is, []
    | (hd :: tl) as xs ->
    match try_parse parse hd with
      | Some i -> aux (i::is) tl
      | None -> List.rev is, xs
  in aux [];;

 (* check that there is nothing else to parse; raises an error
   otherwise. *)
    let check_emptyness = function
      | x :: _ -> error_xml x "unexpected element"
      | [] -> ();;

let get_son tag f = function
  | Element (t, _, _, x :: _) when t = tag -> f x
  | (PCData _ | Element _) as x -> error_xml x ("not a " ^ tag);;

ここに私の質問があります：最初のコンストラクターの関数では、空ではないため、lhs_val内部の関数に正しく移動できません。私はそれを次のように解析しようとしました：item_stateElement ("", _, _, xs)

and lhs_val xs = match xs with
  | xs -> 
   let item_state, xs = parse_list state xs in
     check_emptyness xs;
   Lhs_lhs (item_state)
  | Element ("state", _, _, xs) -> Lhs_state (state_val xs)

parse_list state xsであるため でエラーが発生しましたxmlが、関数は であると予想されていましたxml list。

この状況を解決する方法を見つけるのを手伝ってくれませんか? Coqタイプや他の方法を変更できるかどうか？etc. いつもお世話になっております。