以 Coq 格式打印等价类

Question

按照我上一个问题的反例：Error when convert to Boolean matrix。

let entries = [("name", ["string"]); ("label", ["nonNegativeInteger"; "symbol"]);
("symbol", ["name"; "symbol"; "symbol"; "label"]); ("var", ["string"]);
("term", ["var"; "symbol"; "term"]); ("rule", ["term"; "term"]);
("rules", ["rule"]); ("dps", ["rules"]); ("trs", ["rules"]);
("usableRules", ["rules"]);
("number", ["integer"; "integer"; "positiveInteger"]);
("coefficient",["number"; "minusInfinity"; "plusInfinity"; "vector"; "matrix"])
("vector", ["coefficient"]); ("matrix", ["vector"])]

let defined = ["name"; "label"; "symbol"; "var"; "term"; "rule"; "rules"; 
"dps"; "trs"; "usableRules"; "number"; "coefficient"; "vector"; "matrix"]

let undefined = ["string"; "nonNegativeInteger"; "integer"; "positiveInteger";
"minusInfinity"; "plusInfinity"]

我使用这些函数进行了计算：（更多详细信息请参见此处：Transitive closure and equivalence classes 和 Asking about return type, list and set data structure in OCaml）

let rec position x = function
| [] -> raise Not_found
| y :: ys -> if x = y then 0 else 1 + position x ys

let len_undefined = List.length undefined

let num_of_name xsds undefined len_undefined s =
  try (position s xsds) + len_undefined;
  with Not_found -> position s undefined

let name_of_num xsds undefined len_undefined k =
  if k < len_undefined then
    List.nth undefined k else
    List.nth xsds (k - len_undefined)

let matrix =
  let len = List.length defined + len_undefined in
  let boolmat = Array.make_matrix len len false in
  List.iter (fun (s, strs) ->
    let pos1 = num_of_name defined undefined len_undefined s in
      List.iter (fun t ->
    let pos2 = num_of_name defined undefined len_undefined t in
    boolmat.(pos1).(pos2) <- true) strs) entries;
    boolmat

let transClosure m =
  let n = Array.length m in
  for k = 0 to n - 1 do
    let mk = m.(k) in
    for i = 0 to n - 1 do
      let mi = m.(i) in
      for j = 0 to n - 1 do
    mi.(j) <- max mi.(j) (min mi.(k) mk.(j))
      done;
    done;
  done;
  m;;

let eq_class m i =
  let column = m.(i)
  and set = ref [] in
  Array.iteri begin fun j l ->
    if j = i || column.(j) && m.(j).(i) then
      set := j :: !set else ignore l
  end column;
  !set;;

let eq_classes m =
  let classes = ref [] in
  Array.iteri begin fun e _ ->
    if not (List.exists (List.mem e) !classes) then
      classes := eq_class m e :: !classes
  end m;
  !classes;;

let cmp_classes m c c' = if c = c' then 0 else
  match c, c' with
    | i :: _, j :: _ -> if m.(i).(j) then 1 else -1
    | _ -> assert false

let sort_eq_classes m = List.sort (cmp_classes m);;

let order_xsds =
  let tc_xsds = transClosure matrix in
  let eq_xsds = eq_classes tc_xsds in
  let sort_eq_xsds = sort_eq_classes tc_xsds eq_xsds in
  sort_eq_xsds

let print =
let f elem =
  print_int elem ; print_string " "
in List.iter f (List.flatten order_xsds);;

let xsds_of_int =
  List.map (List.map (name_of_num defined undefined len_undefined))

let xsds_sort = xsds_of_int order_xsds

let print_string =
let f elem =
  print_string elem ; print_string " \n"
in List.iter f (List.flatten xsds_sort);;

我尝试打印结果以查看已排序的等价类：

var name symbol label plusInfinity minusInfinity positiveInteger integer number 
matrix vector coefficient nonNegativeInteger string term rule rules usableRules 
trs dps 

因为我必须以 Coq 格式打印，所以我必须使文件输出组合，所以当看到等价类时，我想按等价类的结果顺序打印结果（“标签”-“符号”；“系数”-“矩阵”-“向量”）它应该打印：

编辑：

Inductive label := all the type label depends
with symbol := all the type symbol depends.

例如：

   Inductive label :=
    | Label : nonNegativeInteger -> symbol -> label
   with symbol :=
    | Symbol : name -> symbol -> symbol -> label -> symbol.

当它是一种类型时，它会为我打印，例如：

Definition name := string.

当它超过 2 个时，取决于类型，

Inductive numer := all the type number depends.

例如：

Inductive number := 
 |Number : integer -> integer -> positiveInteger -> number.

我认为undefined类型中的类型列表应该在排序前后打印在列表的结果中（并且undefined列表的所有类型都不应该打印再次），例如我期望的结果是这样的：

Definition string := string.
Definition nonNegative := int.
...
Definition var := string.
Definition name := string.
Inductive label := ...
with symbol := ...

等等

你能帮帮我吗？

Answer 1

我可能会感到困惑，但我认为您只是在寻找 Printf 模块和 String.concat？例如

List.iter
    (fun name ->
        Printf.printf "Definition %s := %s.\n" name (defn_of name))
    undefined;
List.iter
    (fun eqvclass ->
        Printf.printf "Inductive %s.\n"
            (String.concat "\nwith "
                (List.map
                    (fun name ->
                        Printf.sprintf "%s := %s" name (defn_of name))
                    eqvclass)))
    order_xsds

（defn_of 为您提供定义的右侧）。