Распечатать классы эквивалентности в формате Coq

Question

Следуйте примеру счетчика из моего предыдущего вопроса: Ошибка при преобразовании в булеву матрицу .

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"]

Я вычислил с помощью этих функций: (подробности см. Здесь: Классы транзитивного замыкания и эквивалентности и Запрос о типе возврата, списке и структуре данных в 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, мне нужно объединить вывод файла, поэтому результат, который я хочу распечатать, должен отображаться в порядке результатов классов эквивалентности, когда он видит классы эквивалентности ("label" - "). символ ";" коэффициент "-" матрица "-" вектор ") должен быть напечатан:

EDIT:

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 дает вам правую часть определений).