1 
 <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_state，因为它不是空的Element ("", _, _, 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类型或其他方式？等非常感谢您的帮助。

4

0 回答 0